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

[bugfix] subterm insertion in forgetful propagation

Browse source
This commit is contained in:
Guillaume Bury 2017-01-29 13:33:24 +01:00
parent 44509c6f8d
commit 8acf02cb74
1 changed files with 7 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/core/internal.ml
View file

@ -231,6 +231,9 @@ module Make
Iheap.insert f_weight env.order l.lid Iheap.insert f_weight env.order l.lid
| E_var v -> | E_var v ->
Iheap.insert f_weight env.order v.vid; Iheap.insert f_weight env.order v.vid;
insert_subterms_order v
and insert_subterms_order v =
iter_sub (fun t -> insert_var_order (elt_of_lit t)) v iter_sub (fun t -> insert_var_order (elt_of_lit t)) v
(* Add new litterals/atoms on which to decide on, even if there is no (* Add new litterals/atoms on which to decide on, even if there is no
@ -935,8 +938,11 @@ module Make
if p.is_true then () if p.is_true then ()
else if p.neg.is_true then else if p.neg.is_true then
Stack.push c env.clauses_to_add Stack.push c env.clauses_to_add
else else begin
Iheap.grow_to_at_least env.order (St.nb_elt ());
insert_subterms_order p.var;
enqueue_bool p (decision_level ()) (Bcp c) enqueue_bool p (decision_level ()) (Bcp c)
end
else else
raise (Invalid_argument "Msat.Internal.slice_propagate") raise (Invalid_argument "Msat.Internal.slice_propagate")