From b61ec3545141c99f288d32ac7801c071acd0f125 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 16 Aug 2022 21:37:56 -0400 Subject: [PATCH] fix(th-bool-dyn): do not propagate, just add clauses depending on polarity --- src/th-bool-dyn/Sidekick_th_bool_dyn.ml | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/src/th-bool-dyn/Sidekick_th_bool_dyn.ml b/src/th-bool-dyn/Sidekick_th_bool_dyn.ml index 7da0f993..86c7d46d 100644 --- a/src/th-bool-dyn/Sidekick_th_bool_dyn.ml +++ b/src/th-bool-dyn/Sidekick_th_bool_dyn.ml @@ -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