From 19e083c682c291c4a1672e86cee1d09b0419aae3 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 9 Jun 2021 21:13:04 -0400 Subject: [PATCH] produce `nn` steps --- src/base-term/Proof.ml | 4 ++++ src/core/Sidekick_core.ml | 1 + src/msat-solver/Sidekick_msat_solver.ml | 1 + src/th-bool-static/Sidekick_th_bool_static.ml | 4 ++-- 4 files changed, 8 insertions(+), 2 deletions(-) diff --git a/src/base-term/Proof.ml b/src/base-term/Proof.ml index cc2a9e56..12b50946 100644 --- a/src/base-term/Proof.ml +++ b/src/base-term/Proof.ml @@ -46,6 +46,7 @@ type t = | Bool_true_neq_false | Bool_eq of term * term (* equal by pure boolean reasoning *) | Bool_c of bool_c_name * term list (* boolean tautology *) + | Nn of t (* negation normalization *) | Ite_true of term (* given [if a b c] returns [a=T |- if a b c=b] *) | Ite_false of term | LRA of clause @@ -130,6 +131,7 @@ let true_is_true : t = Bool_true_is_true let true_neq_false : t = Bool_true_neq_false let bool_eq a b : t = Bool_eq (a,b) let bool_c name c : t = Bool_c (name, c) +let nn c : t = Nn c let hres_l p l : t = let l = List.filter (function (P1 (Refl _)) -> false | _ -> true) l in @@ -167,6 +169,7 @@ let iter_p (p:t) ~f_t ~f_step ~f_clause ~f_p : unit = | Bool_true_is_true | Bool_true_neq_false -> () | Bool_eq (t, u) -> f_t t; f_t u | Bool_c (_, ts) -> List.iter f_t ts + | Nn p -> f_p p | Ite_true t | Ite_false t -> f_t t | LRA c -> f_clause c | Composite { assumptions; steps } -> @@ -322,6 +325,7 @@ module Quip = struct pp_t a pp_t b | Bool_c (name,ts) -> Fmt.fprintf out "(@[bool-c %s@ %a@])" name (pp_l pp_t) ts + | Nn p -> Fmt.fprintf out "(@[nn@ %a@])" pp_rec p | Assertion t -> Fmt.fprintf out "(@[assert@ %a@])" pp_t t | Assertion_c c -> Fmt.fprintf out "(@[assert-c@ %a@])" pp_cl c diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index 837536cd..6363162f 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -195,6 +195,7 @@ module type PROOF = sig val refl : term -> t (* proof of [| t=t] *) val true_is_true : t (* proof of [|- true] *) val true_neq_false : t (* proof of [|- not (true=false)] *) + val nn : t -> t (* negation normalization *) val cc_lemma : lit Iter.t -> t (* equality tautology, unsigned *) val cc_imply2 : t -> t -> term -> term -> t (* tautology [p1, p2 |- t=u] *) val cc_imply_l : t list -> term -> term -> t (* tautology [hyps |- t=u] *) diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml index a2e086f5..16836cdc 100644 --- a/src/msat-solver/Sidekick_msat_solver.ml +++ b/src/msat-solver/Sidekick_msat_solver.ml @@ -767,6 +767,7 @@ module Make(A : ARG) if !pr_l=[] then proof else P.(hres_l proof (List.rev_map p1 !pr_l)) in + let proof = P.nn proof in (* normalize lits *) Sat_solver.add_clause self.solver atoms proof) self.si lit diff --git a/src/th-bool-static/Sidekick_th_bool_static.ml b/src/th-bool-static/Sidekick_th_bool_static.ml index 7089f0f7..300cb827 100644 --- a/src/th-bool-static/Sidekick_th_bool_static.ml +++ b/src/th-bool-static/Sidekick_th_bool_static.ml @@ -285,10 +285,10 @@ module Make(A : ARG) : S with module A = A = struct (fun t_u u -> add_clause [Lit.neg proxy; u] - (A.proof_bool_c "and-i" [t_proxy; t_u])) + (A.proof_bool_c "and-e" [t_proxy; t_u])) t_subs subs; add_clause (proxy :: List.map Lit.neg subs) - (A.proof_bool_c "and-e" [t_proxy]); + (A.proof_bool_c "and-i" [t_proxy]); proxy, pr_def_refl t_proxy t | B_or l ->