From d681e247ed411f8cb0b0a5a1407ad7d82498256c Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Fri, 4 Nov 2016 12:19:43 +0100
Subject: [PATCH] Added some debug logging

---
 src/core/external.ml          | 12 ++++++++++++
 src/core/internal.ml          |  7 +++++--
 src/core/solver_types.ml      |  4 ++++
 src/core/solver_types_intf.ml |  1 +
 4 files changed, 22 insertions(+), 2 deletions(-)

diff --git a/src/core/external.ml b/src/core/external.ml
index b3fde322..ae2e0d92 100644
--- a/src/core/external.ml
+++ b/src/core/external.ml
@@ -56,7 +56,18 @@ module Make
     | Sat of (St.term,St.formula) sat_state
     | Unsat of (St.clause,Proof.proof) unsat_state
 
+  let pp_all lvl =
+    Log.debugf lvl
+      "@[<v>Full resume:@,@[<hov 2>Trail:@\n%a@]@,@[<hov 2>Temp:@\n%a@]@,@[<hov 2>Hyps:@\n%a@]@,@[<hov 2>Lemmas:@\n%a@]@,]@."
+      (fun k -> k
+          (Vec.print ~sep:"" St.pp) (S.trail ())
+          (Vec.print ~sep:"" St.pp_clause) (S.temp ())
+          (Vec.print ~sep:"" St.pp_clause) (S.hyps ())
+          (Vec.print ~sep:"" St.pp_clause) (S.history ())
+      )
+
   let mk_sat () : (_,_) sat_state =
+    pp_all 99;
     let t = S.trail () in
     let iter f f' =
       Vec.iter (function
@@ -72,6 +83,7 @@ module Make
     }
 
   let mk_unsat () : (_,_) unsat_state =
+    pp_all 99;
     let unsat_conflict () = match S.unsat_conflict () with
       | None -> assert false
       | Some c -> c
diff --git a/src/core/internal.ml b/src/core/internal.ml
index ab14a589..8a8b22e7 100644
--- a/src/core/internal.ml
+++ b/src/core/internal.ml
@@ -383,7 +383,9 @@ module Make
   let cancel_until lvl =
     assert (lvl >= base_level ());
     (* Nothing to do if we try to backtrack to a non-existent level. *)
-    if decision_level () > lvl then begin
+    if decision_level () <= lvl then
+      Log.debugf 5 "Already at level <= %d" (fun k -> k lvl)
+    else begin
       Log.debugf 5 "Backtracking to lvl %d" (fun k -> k lvl);
       (* We set the head of the solver and theory queue to what it was. *)
       env.elt_head <- Vec.get env.elt_levels lvl;
@@ -1167,11 +1169,12 @@ module Make
   let local l =
     let aux lit =
       let a = atom lit in
-      Log.debugf 10 "local assumption: @[%a@]" (fun k->k pp_atom a);
+      Log.debugf 10 "Local assumption: @[%a@]" (fun k-> k pp_atom a);
       assert (decision_level () = base_level ());
       if a.is_true then ()
       else
         let c = make_clause (fresh_hname ()) [a] Local in
+        Log.debugf 10 "Temp clause: @[%a@]" (fun k -> k pp_clause c);
         Vec.push env.clauses_temp c;
         if a.neg.is_true then begin
           (* conflict between assumptions: UNSAT *)
diff --git a/src/core/solver_types.ml b/src/core/solver_types.ml
index db08a2bc..fbc3ec87 100644
--- a/src/core/solver_types.ml
+++ b/src/core/solver_types.ml
@@ -311,6 +311,10 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
     in
     Format.fprintf fmt "%a0" aux atoms
 
+  let pp fmt = function
+    | Lit l -> pp_lit fmt l
+    | Atom a -> pp_atom fmt a
+
 end
 
 
diff --git a/src/core/solver_types_intf.ml b/src/core/solver_types_intf.ml
index 5e42a169..6b1dcdcf 100644
--- a/src/core/solver_types_intf.ml
+++ b/src/core/solver_types_intf.ml
@@ -139,6 +139,7 @@ module type S = sig
   val print_clause : Format.formatter -> clause -> unit
   (** Pretty printing functions for atoms and clauses *)
 
+  val pp : Format.formatter -> t -> unit
   val pp_lit : Format.formatter -> lit -> unit
   val pp_atom : Format.formatter -> atom -> unit
   val pp_clause : Format.formatter -> clause -> unit