Test

src/lib/reasoners/satml.ml

@@ -47,6 +47,10 @@ type conflict_origin =
 
 let vraie_form = E.vrai
 
+let pp str =
+  if Options.get_verbose () then
+    Format.printf str
+  else Format.ifprintf Format.std_formatter str
 
 module type SAT_ML = sig
   (*module Make (Dummy : sig end) : sig*)
@@ -597,6 +601,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
     !max_lvl
 
   let enqueue env (a : Atom.atom) lvl reason =
+    pp "Enqueue! First assert.@.";
     assert (not a.is_true && not a.neg.is_true &&
             a.var.level < 0 && a.var.reason == None && lvl >= 0);
     if a.neg.is_guard then begin
@@ -610,6 +615,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
     end;
     (* Garder la reason car elle est utile pour les unsat-core *)
     (*let reason = if lvl = 0 then None else reason in*)
+    pp "Atom %a is not a guard, assigning %a to true@." Atom.pr_atom a.neg Atom.pr_atom a;
     a.is_true <- true;
     a.var.level <- lvl;
     a.var.reason <- reason;
@@ -1826,21 +1832,32 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
     env.is_unsat_cpt <- if env.is_unsat then env.is_unsat_cpt + 1 else 0
 
   let pop env =
+    pp "pop: is increm guards empty?@.";
     (assert (not (Vec.is_empty env.increm_guards)));
     let g = Vec.pop env.increm_guards in
     env.is_unsat <- env.is_unsat_cpt <> 0;
     env.is_unsat_cpt <- max 0 (env.is_unsat_cpt - 1);
     g.is_guard <- false;
     g.neg.is_guard <- false;
-    assert (not g.var.na.is_true); (* atom not false *)
+    pp "pop: is atom %a true? %b@." Atom.pr_atom g.var.na g.var.na.is_true;
+    if g.var.na.is_true then
+      begin
+        pp "Looks like so, smells bad!@.";
+        assert false
+      end;
+    (* assert (not g.var.na.is_true); (\* atom not false *\) *)
+    pp "Good, let's keep going@.";
     if g.var.pa.is_true then (* if already decided  *)
       begin
+        pp "pop: var level = %i@." g.var.level;
         (assert (g.var.level > 0));
         cancel_until env (g.var.level - 1); (* undo its decision *)
         (* all previous guards are decided *)
         env.next_dec_guard <- Vec.size env.increm_guards
       end;
-    enqueue env g.neg 0 None
+    pp "Calling enqueue@.";
+    enqueue env g.neg 0 None;
+    Format.printf "Good, let's leave pop now.@."
 
   let optimize env ~is_max obj = env.tenv <- Th.optimize env.tenv ~is_max obj
 end

tests/cram.t/run.t

@@ -27,7 +27,7 @@ Now we will test some semantic triggers.
 
 And some SMT2 action.
 
-  $ alt-ergo -o smtlib2 --prelude prelude.ae postlude.smt2 2>/dev/null
+  $ OCAMLRUNPARAM=b alt-ergo -o smtlib2 --prelude prelude.ae postlude.smt2 --verbose
 
   unknown