simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-28 04:14:50 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Bug fixed (hopefully)

Browse source
This commit is contained in:
Guillaume Bury 2015-01-24 21:43:23 +01:00
parent 8fcf90b5c9
commit 51339eccf8
1 changed files with 7 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
solver/mcsolver.ml
View file

@ -281,8 +281,6 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
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)
@ -301,15 +299,15 @@ 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 (%d): %a" (nb_assigns ()) pp_atom a; Vec.push env.trail (Either.mk_right a);
Vec.push env.trail (Either.mk_right a) L.debug 2 "Enqueue (%d): %a" (nb_assigns ()) pp_atom 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 (%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) L.debug 2 "Enqueue (%d): %a" (nb_assigns ()) St.pp_semantic_var v
(* conflict analysis *) (* conflict analysis *)
let max_lvl_atoms l = let max_lvl_atoms l =
@ -638,12 +636,10 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
}) })
let rec theory_propagate () = let rec theory_propagate () =
let head = nb_assigns () in let slice = current_slice () in
L.debug 5 "Propagating to theory (with head = %d)" head; env.tatoms_qhead <- nb_assigns ();
match Th.assume (current_slice ()) with match Th.assume slice with
| Th.Sat -> | Th.Sat ->
L.debug 5 "env.tatoms_qhead : %d -> %d" env.tatoms_qhead head;
env.tatoms_qhead <- head;
propagate () propagate ()
| Th.Unsat (l, p) -> | Th.Unsat (l, p) ->
let l = List.rev_map St.add_atom l in let l = List.rev_map St.add_atom l in