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

refactor(sat): improve style of theory propagation handler

Browse source
This commit is contained in:
Simon Cruanes 2018-08-18 19:55:30 -05:00
parent 324c9d2e36
commit c1a662e2c8
1 changed files with 15 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

25
src/sat/Internal.ml
View file

@ -1292,21 +1292,22 @@ module Make (Th : Theory_intf.S) = struct
let act_propagate (st:t) f causes proof : unit = let act_propagate (st:t) f causes proof : unit =
let l = List.rev_map (Atom.make st) causes in let l = List.rev_map (Atom.make st) causes in
if List.for_all Atom.is_true l then ( assert (
let p = Atom.make st f in if not @@ List.for_all Atom.is_true l then (
let c = Clause.make_l (p :: List.map Atom.neg l) (Lemma proof) in
if p.is_true then (
) else if p.neg.is_true then (
(* propagate other lits in the clause *)
add_clause ~permanent:false st c;
) else (
insert_var_order st p.var;
enqueue_bool st p (Bcp c);
)
) else (
Error.errorf "(@[sat.act_propagate.invalid_guard@ :guard %a@ \ Error.errorf "(@[sat.act_propagate.invalid_guard@ :guard %a@ \
:1 all lits are not true@])" :1 all lits are not true@])"
(Util.pp_list Atom.debug) l (Util.pp_list Atom.debug) l
); true);
let p = Atom.make st f in
if p.is_true then (
) else if p.neg.is_true then (
(* we got ourself a wee conflict clause *)
let c = Clause.make_l (p :: List.rev_map Atom.neg l) (Lemma proof) in
raise (Conflict c)
) else (
let c = Clause.make_l (p :: List.rev_map Atom.neg l) (Lemma proof) in
insert_var_order st p.var;
enqueue_bool st p (Bcp c);
) )
let current_slice st head : formula Theory_intf.slice_actions = let current_slice st head : formula Theory_intf.slice_actions =