From 79099b0bffbaf6852f1f070f13eb3bb75b4a9d86 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Wed, 23 Oct 2024 14:08:36 +0200
Subject: [PATCH] Do not display 0 candidates messages

As we load by default prelude with plenty of axioms, we got a lot of
messages about these axioms in the debugging printers of `Matching`.
This commit changes this behavior. We only print messages if there is at
least one candidate.
---
 src/lib/reasoners/adt.ml      |  2 +-
 src/lib/reasoners/matching.ml | 30 ++++++++++++++++--------------
 test.smt2                     | 10 ++++++++++
 3 files changed, 27 insertions(+), 15 deletions(-)
 create mode 100644 test.smt2

diff --git a/src/lib/reasoners/adt.ml b/src/lib/reasoners/adt.ml
index d9df614c4..cb7e16854 100644
--- a/src/lib/reasoners/adt.ml
+++ b/src/lib/reasoners/adt.ml
@@ -38,7 +38,7 @@ type 'a abstract =
       c_ty : Ty.t;
       c_args : (DE.term_cst * 'a) list
     }
-  (* [Cons { c_name; c_ty; c_args }] reprensents the application of the
+  (* [Cons { c_name; c_ty; c_args }] represents the application of the
      constructor [c_name] of the ADT [ty] with the arguments [c_args]. *)
 
   | Select of { d_name : DE.term_cst ; d_ty : Ty.t ; d_arg : 'a }
diff --git a/src/lib/reasoners/matching.ml b/src/lib/reasoners/matching.ml
index b75a1bc29..1019bca3f 100644
--- a/src/lib/reasoners/matching.ml
+++ b/src/lib/reasoners/matching.ml
@@ -165,20 +165,22 @@ module Make (X : Arg) : S with type theory = X.t = struct
 
     let candidate_substitutions pat_info res =
       let open Matching_types in
-      if Options.get_debug_matching () >= 1 then
-        print_dbg
-          ~module_name:"Matching" ~function_name:"candidate_substitutions"
-          "@[<v 2>%3d candidate substitutions for Axiom %a with trigger %a@ "
-          (List.length res)
-          E.print pat_info.trigger_orig
-          E.print_list pat_info.trigger.E.content;
-      if Options.get_debug_matching() >= 2 then
-        List.iter
-          (fun gsbt ->
-             print_dbg ~header:false
-               ">>> sbs = %a  and  sbty = %a@ "
-               (SubstE.pp E.print) gsbt.sbs Ty.print_subst gsbt.sty
-          )res
+      if not @@ Compat.List.is_empty res then begin
+        if Options.get_debug_matching () >= 1 then
+          print_dbg
+            ~module_name:"Matching" ~function_name:"candidate_substitutions"
+            "@[<v 2>%3d candidate substitutions for Axiom %a with trigger %a@ "
+            (List.length res)
+            E.print pat_info.trigger_orig
+            E.print_list pat_info.trigger.E.content;
+        if Options.get_debug_matching() >= 2 then
+          List.iter
+            (fun gsbt ->
+               print_dbg ~header:false
+                 ">>> sbs = %a  and  sbty = %a@ "
+                 (SubstE.pp E.print) gsbt.sbs Ty.print_subst gsbt.sty
+            )res
+      end
 
   end
   (*BISECT-IGNORE-END*)
diff --git a/test.smt2 b/test.smt2
new file mode 100644
index 000000000..6a8c7f2b7
--- /dev/null
+++ b/test.smt2
@@ -0,0 +1,10 @@
+(set-option :produce-models true)
+(set-logic ALL)
+(declare-datatype t ((B (i Int))))
+
+(declare-const e t)
+
+(assert ((_ is B) e))
+(assert (forall ((n Int)) (distinct e (B n))))
+(check-sat)
+(get-model)