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

[bugfix] when picking a new term to be assigned, it is possible it is

Browse source 
already assigned
This commit is contained in:
Guillaume Bury 2015-01-13 18:08:19 +01:00
parent b05b21ac34
commit 24b9362b30
1 changed files with 12 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
solver/mcsolver.ml
View file

@ -261,7 +261,8 @@ module Make (E : Expr_intf.S)
Either.destruct (Vec.get env.trail c) Either.destruct (Vec.get env.trail c)
(fun v -> (fun v ->
v.tag.assigned <- None; v.tag.assigned <- None;
v.level <- -1 v.level <- -1;
insert_var_order (Either.mk_left v)
) )
(fun a -> (fun a ->
if a.var.level <= lvl then begin if a.var.level <= lvl then begin
@ -744,13 +745,16 @@ module Make (E : Expr_intf.S)
let max = Iheap.remove_min f_weight env.order in let max = Iheap.remove_min f_weight env.order in
Either.destruct (St.get_var max) Either.destruct (St.get_var max)
(fun v -> (fun v ->
let value = Th.assign v.tag.term in if v.level >= 0 then
env.decisions <- env.decisions + 1; pick_branch_lit ()
new_decision_level(); else begin
let current_level = decision_level () in let value = Th.assign v.tag.term in
assert (v.level < 0); env.decisions <- env.decisions + 1;
Log.debug 5 "Deciding on %a" St.pp_semantic_var v; new_decision_level();
enqueue_assign v value current_level) let current_level = decision_level () in
Log.debug 5 "Deciding on %a" St.pp_semantic_var v;
enqueue_assign v value current_level
end)
(fun v -> (fun v ->
if v.level >= 0 then begin if v.level >= 0 then begin
assert (v.tag.pa.is_true || v.tag.na.is_true); assert (v.tag.pa.is_true || v.tag.na.is_true);
@ -760,7 +764,6 @@ module Make (E : Expr_intf.S)
env.decisions <- env.decisions + 1; env.decisions <- env.decisions + 1;
new_decision_level(); new_decision_level();
let current_level = decision_level () in let current_level = decision_level () in
assert (v.level < 0);
Log.debug 5 "Deciding on %a" St.pp_atom v.tag.pa; Log.debug 5 "Deciding on %a" St.pp_atom v.tag.pa;
enqueue_bool v.tag.pa current_level (Bcp None) enqueue_bool v.tag.pa current_level (Bcp None)
| Th.Valued (b, lvl) -> | Th.Valued (b, lvl) ->