Added some debug logging

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

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 *)

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
 
 

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