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

fix(th-bool-dyn): do not propagate, just add clauses depending on polarity

Browse source
This commit is contained in:
Simon Cruanes 2022-08-16 21:37:56 -04:00
parent e4acb2cfca
commit b61ec35451
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 5 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/th-bool-dyn/Sidekick_th_bool_dyn.ml
View file

@ -21,7 +21,6 @@ end = struct
n_simplify: int Stat.counter;
n_expanded: int Stat.counter;
n_clauses: int Stat.counter;
n_propagate: int Stat.counter;
}
let create ~stat tst : state =
@ -31,7 +30,6 @@ end = struct
n_simplify = Stat.mk_int stat "th.bool.simplified";
n_expanded = Stat.mk_int stat "th.bool.expanded";
n_clauses = Stat.mk_int stat "th.bool.clauses";
n_propagate = Stat.mk_int stat "th.bool.propagations";
}
let[@inline] not_ tst t = A.mk_bool tst (B_not t)
@ -232,11 +230,11 @@ end = struct
let subs = List.map Lit.atom [ a; b ] in
if Lit.sign lit then
(* propagate [(and …t_i) => t_i] *)
(* assert [(and …t_i) => t_i] *)
List.iter
(fun sub ->
Stat.incr self.n_propagate;
SI.propagate_l solver acts sub [ lit ]
add_axiom
[ Lit.neg lit; sub ]
( mk_step_ @@ fun () ->
Proof_rules.lemma_bool_c "and-e" [ t; Lit.term sub ] ))
subs
@ -253,8 +251,8 @@ end = struct
(* propagate [¬sub_i \/ lit] *)
List.iter
(fun sub ->
Stat.incr self.n_propagate;
SI.propagate_l solver acts (Lit.neg sub) [ lit ]
add_axiom
[ Lit.neg lit; Lit.neg sub ]
( mk_step_ @@ fun () ->
Proof_rules.lemma_bool_c "or-i" [ t; Lit.term sub ] ))
subs