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

feat: ensure the congruence closure can propagate literals

Browse source
This commit is contained in:
Simon Cruanes 2019-06-07 17:37:52 -05:00
parent 38f001b0e7
commit c9d8fd2f51
1 changed files with 6 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/msat-solver/Sidekick_msat_solver.ml
View file

@ -468,7 +468,12 @@ module Make(A : ARG)
|> Iter.iter |> Iter.iter
(fun sub -> (fun sub ->
Log.debugf 5 (fun k->k "(@[solver.map-bool-subterm-to-lit@ :subterm %a@])" T.pp sub); Log.debugf 5 (fun k->k "(@[solver.map-bool-subterm-to-lit@ :subterm %a@])" T.pp sub);
ignore (mk_atom_t_ self sub : Sat_solver.atom)) (* ensure that msat has a boolean atom for [sub] *)
let atom = mk_atom_t_ self sub in
(* also map [sub] to this atom in the congruence closure, for propagation *)
let cc = cc self in
CC.set_as_lit cc (CC.add_term cc sub ) (Sat_solver.Atom.formula atom);
())
let rec mk_atom_lit self lit : Atom.t = let rec mk_atom_lit self lit : Atom.t =
let lit = preprocess_lit_ self lit in let lit = preprocess_lit_ self lit in