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

Some more logging messages

Browse source
This commit is contained in:
Guillaume Bury 2015-01-24 21:10:01 +01:00
parent 6b70dd413c
commit f85714537e
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
solver/mcsolver.ml
View file

@ -280,7 +280,9 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
Th.backtrack (Vec.get env.tenv_queue lvl); (* recover the right tenv *) Th.backtrack (Vec.get env.tenv_queue lvl); (* recover the right tenv *)
Vec.shrink env.trail ((Vec.size env.trail) - env.qhead); Vec.shrink env.trail ((Vec.size env.trail) - env.qhead);
Vec.shrink env.trail_lim ((Vec.size env.trail_lim) - lvl); Vec.shrink env.trail_lim ((Vec.size env.trail_lim) - lvl);
Vec.shrink env.tenv_queue ((Vec.size env.tenv_queue) - lvl) Vec.shrink env.tenv_queue ((Vec.size env.tenv_queue) - lvl);
L.debug 5 "env.qhead : %d" env.qhead;
L.debug 5 "env.tatoms_qhead : %d" env.tatoms_qhead
end; end;
assert (Vec.size env.trail_lim = Vec.size env.tenv_queue) assert (Vec.size env.trail_lim = Vec.size env.tenv_queue)
@ -639,6 +641,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
let head = Vec.size env.trail in let head = Vec.size env.trail in
match Th.assume (current_slice ()) with match Th.assume (current_slice ()) with
| Th.Sat -> | Th.Sat ->
L.debug 5 "env.tatoms_qhead : %d -> %d" env.tatoms_qhead head;
env.tatoms_qhead <- head; env.tatoms_qhead <- head;
propagate () propagate ()
| Th.Unsat (l, p) -> | Th.Unsat (l, p) ->