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

[bugfix] Allow semantic propagation of already true lits

Browse source
This commit is contained in:
Guillaume Bury 2016-12-19 15:58:48 +01:00
parent 58e6b924a8
commit f80c3b3df7
1 changed files with 8 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/core/internal.ml
View file

@ -499,11 +499,14 @@ module Make
(fun k->k (Vec.size env.elt_queue) pp_atom a)
let enqueue_semantic a terms =
let l = List.map St.add_term terms in
let lvl = List.fold_left (fun acc {l_level; _} ->
assert (l_level > 0); max acc l_level) 0 l in
Iheap.grow_to_at_least env.order (St.nb_elt ());
enqueue_bool a lvl Semantic
if a.is_true then ()
else begin
let l = List.map St.add_term terms in
let lvl = List.fold_left (fun acc {l_level; _} ->
assert (l_level > 0); max acc l_level) 0 l in
Iheap.grow_to_at_least env.order (St.nb_elt ());
enqueue_bool a lvl Semantic
end
(* MCsat semantic assignment *)
let enqueue_assign l value lvl =