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

Added a few debug messages

Browse source
This commit is contained in:
Guillaume Bury 2015-03-15 21:52:48 +01:00
parent 1f0fdf65fd
commit 34141f9d7d
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
solver/mcsolver.ml
View file

@ -290,9 +290,10 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
raise Unsat raise Unsat
let enqueue_bool a lvl reason = let enqueue_bool a lvl reason =
L.debug 99 "Entering enqueue_bool";
assert (not a.neg.is_true); assert (not a.neg.is_true);
if a.is_true then if a.is_true then
L.debug 10 "Litteral %a alreayd in queue" pp_atom a L.debug 10 "Litteral %a already in queue" pp_atom a
else begin else begin
assert (a.var.level < 0 && a.var.tag.reason = Bcp None && lvl >= 0); assert (a.var.level < 0 && a.var.tag.reason = Bcp None && lvl >= 0);
a.is_true <- true; a.is_true <- true;
@ -303,6 +304,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
end end
let enqueue_assign v value lvl = let enqueue_assign v value lvl =
L.debug 99 "Entering enqueue_assign";
v.tag.assigned <- Some value; v.tag.assigned <- Some value;
v.level <- lvl; v.level <- lvl;
Vec.push env.trail (Either.mk_left v); Vec.push env.trail (Either.mk_left v);