simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-09 12:45:48 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Some more debug logging

Browse source
This commit is contained in:
Guillaume Bury 2015-01-24 21:31:45 +01:00
parent 8afdc59ced
commit 8fcf90b5c9
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
solver/mcsolver.ml
View file

@ -301,14 +301,14 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
a.is_true <- true; a.is_true <- true;
a.var.level <- lvl; a.var.level <- lvl;
a.var.tag.reason <- reason; a.var.tag.reason <- reason;
L.debug 2 "Enqueue: %a" pp_atom a; L.debug 2 "Enqueue (%d): %a" (nb_assigns ()) pp_atom a;
Vec.push env.trail (Either.mk_right a) Vec.push env.trail (Either.mk_right a)
end end
let enqueue_assign v value lvl = let enqueue_assign v value lvl =
v.tag.assigned <- Some value; v.tag.assigned <- Some value;
v.level <- lvl; v.level <- lvl;
L.debug 2 "Enqueue: %a" St.pp_semantic_var v; L.debug 2 "Enqueue (%d): %a" (nb_assigns ()) St.pp_semantic_var v;
Vec.push env.trail (Either.mk_left v) Vec.push env.trail (Either.mk_left v)
(* conflict analysis *) (* conflict analysis *)
@ -638,7 +638,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
}) })
let rec theory_propagate () = let rec theory_propagate () =
let head = env.qhead in let head = nb_assigns () in
L.debug 5 "Propagating to theory (with head = %d)" head; L.debug 5 "Propagating to theory (with head = %d)" head;
match Th.assume (current_slice ()) with match Th.assume (current_slice ()) with
| Th.Sat -> | Th.Sat ->