From 12ea0c3be430ad5c0aab8ed57bf5b03ce8c00c61 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 7 Jun 2019 14:58:46 -0500 Subject: [PATCH] feat: check propagations if `--check` is passed --- src/smtlib/Process.ml | 20 +++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index 7b3d0f8f..71f30ca8 100644 --- a/src/smtlib/Process.ml +++ b/src/smtlib/Process.ml @@ -411,6 +411,7 @@ module Check_cc = struct module MCC = Sidekick_mini_cc.Make(Solver_arg) let pp_c out c = Fmt.fprintf out "(@[%a@])" (Util.pp_list ~sep:" ∨ " Lit.pp) c + let pp_and out c = Fmt.fprintf out "(@[%a@])" (Util.pp_list ~sep:" ∧ " Lit.pp) c let add_cc_lit (cc:MCC.t) (lit:Lit.t) : unit = let t = Lit.term lit in @@ -425,11 +426,28 @@ module Check_cc = struct List.iter (fun lit -> add_cc_lit cc @@ Lit.neg lit) confl; if MCC.check_sat cc then ( Error.errorf "@[<2>check-cc-conflict:@ @[clause %a@]@ \ - is not a UF conflict (negation is sat)@]" pp_c confl + is not a UF tautology (negation is sat)@]" pp_c confl ) else ( Log.debugf 15 (fun k->k "(@[check-cc-conflict.ok@ %a@])" pp_c confl); ) + let check_propagation si _cc p reason : unit = + let reason = reason() in + Log.debugf 15 (fun k->k "(@[check-cc-prop@ %a@ :reason %a@])" Lit.pp p pp_and reason); + let tst = SI.tst si in + let cc = MCC.create tst in + (* add [reason & ¬lit] and check it's unsat *) + List.iter (add_cc_lit cc) reason; + add_cc_lit cc (Lit.neg p); + if MCC.check_sat cc then ( + Error.errorf "@[<2>check-cc-prop:@ @[%a => %a@]@ \ + is not a UF tautology (negation is sat)@]" pp_and reason Lit.pp p + ) else ( + Log.debugf 15 + (fun k->k "(@[check-cc-prop.ok@ @[%a => %a@]@])" pp_and reason Lit.pp p); + ) + + let theory = Solver.mk_theory ~name:"cc-check" ~create_and_setup:(fun si ->