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

feat: check propagations if --check is passed

Browse source
This commit is contained in:
Simon Cruanes 2019-06-07 14:58:46 -05:00
parent ef1110925f
commit 12ea0c3be4
1 changed files with 19 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/smtlib/Process.ml
View file

@ -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 ->