From 0550f6fcfad67500d062e24d1d291c0c3991f108 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 9 Oct 2021 00:51:15 -0400 Subject: [PATCH] wip: proof production --- src/core/Sidekick_core.ml | 3 + src/smt-solver/Sidekick_smt_solver.ml | 10 +- src/th-bool-static/Sidekick_th_bool_static.ml | 116 ++++++++++-------- 3 files changed, 76 insertions(+), 53 deletions(-) diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index 26726dff..37714868 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -786,6 +786,9 @@ module type SOLVER_INTERNAL = sig module type PREPROCESS_ACTS = sig val proof : proof + val mk_lit_nopreproc : ?sign:bool -> term -> lit + (** [mk_lit t] creates a new literal for a boolean term [t]. *) + val mk_lit : ?sign:bool -> term -> lit * proof_step option (** [mk_lit t] creates a new literal for a boolean term [t]. Also returns an optional proof of preprocessing, which if present diff --git a/src/smt-solver/Sidekick_smt_solver.ml b/src/smt-solver/Sidekick_smt_solver.ml index ae260af2..6e73f1fc 100644 --- a/src/smt-solver/Sidekick_smt_solver.ml +++ b/src/smt-solver/Sidekick_smt_solver.ml @@ -187,6 +187,7 @@ module Make(A : ARG) module type PREPROCESS_ACTS = sig val proof : proof + val mk_lit_nopreproc : ?sign:bool -> term -> lit val mk_lit : ?sign:bool -> term -> lit * proof_step option val add_clause : lit list -> proof_step -> unit val add_lit : ?default_pol:bool -> lit -> unit @@ -282,7 +283,7 @@ module Make(A : ARG) this calls all the preprocessing hooks on subterms, ensuring a fixpoint. *) let preprocess_term_ (self:t) (module A0:PREPROCESS_ACTS) (t:term) : term * proof_step option = - let mk_lit_nopreproc t = Lit.atom self.tst t in (* no further simplification *) + let mk_lit_nopreproc ?sign t = Lit.atom ?sign self.tst t in (* no further simplification *) (* compute and cache normal form [u] of [t]. @@ -384,10 +385,13 @@ module Make(A : ARG) and pacts = lazy ( (module struct let proof = A0.proof + let add_lit ?default_pol lit = (* just drop the proof *) + (* TODO: add a clause instead [lit => preprocess(lit)]? *) let lit = preprocess_lit ~steps:(ref []) lit in A0.add_lit ?default_pol lit + let add_clause c pr_c = Stat.incr self.count_preprocess_clause; let steps = ref [] in @@ -398,6 +402,8 @@ module Make(A : ARG) in A0.add_clause c' pr_c' + let mk_lit_nopreproc = mk_lit_nopreproc + let mk_lit = mk_lit end : PREPROCESS_ACTS) ) in @@ -441,6 +447,7 @@ module Make(A : ARG) let preprocess_acts_of_acts (self:t) (acts:theory_actions) : preprocess_actions = (module struct let proof = self.proof + let mk_lit_nopreproc ?sign t = Lit.atom self.tst ?sign t let mk_lit ?sign t = Lit.atom self.tst ?sign t, None let add_clause = add_clause_ self acts let add_lit = add_lit self acts @@ -693,6 +700,7 @@ module Make(A : ARG) (self:t) : (module Solver_internal.PREPROCESS_ACTS) = (module struct let proof = self.proof + let mk_lit_nopreproc ?sign t = Lit.atom ?sign self.si.tst t let mk_lit ?sign t = Lit.atom ?sign self.si.tst t, None let add_lit ?default_pol lit = Sat_solver.add_lit self.solver ?default_pol lit diff --git a/src/th-bool-static/Sidekick_th_bool_static.ml b/src/th-bool-static/Sidekick_th_bool_static.ml index 6fa88936..6178ed41 100644 --- a/src/th-bool-static/Sidekick_th_bool_static.ml +++ b/src/th-bool-static/Sidekick_th_bool_static.ml @@ -126,7 +126,7 @@ module Make(A : ARG) : S with module A = A = struct in (* proof is [t <=> u] *) let ret_bequiv t1 u = - add_step_ @@ SI.Simplify.with_proof simp (A.lemma_bool_equiv t1 u); + add_step_ @@ A.lemma_bool_equiv t1 u @@ SI.Simplify.proof simp; ret u in @@ -152,13 +152,13 @@ module Make(A : ARG) : S with module A = A = struct (* directly simplify [a] so that maybe we never will simplify one of the branches *) let a, prf_a = SI.Simplify.normalize_t simp a in - Iter.iter add_step_ prf_a; + CCOpt.iter add_step_ prf_a; begin match A.view_as_bool a with | B_bool true -> - add_step_ @@ SI.Simplify.with_proof simp (A.lemma_ite_true ~a ~ite:t); + add_step_ @@ A.lemma_ite_true ~a ~ite:t @@ SI.Simplify.proof simp; ret b | B_bool false -> - add_step_ @@ SI.Simplify.with_proof simp (A.lemma_ite_false ~a ~ite:t); + add_step_ @@ A.lemma_ite_false ~a ~ite:t @@ SI.Simplify.proof simp; ret c | _ -> None @@ -189,13 +189,10 @@ module Make(A : ARG) : S with module A = A = struct let proxy = fresh_term ~for_t ~pre self (Ty.bool self.ty_st) in proxy, mk_lit proxy - let p1_opt s1 s2 p : SI.proof_step = - let s2 = s2 p in + let pr_p1_opt p s1 s2 : SI.proof_step = CCOpt.map_or ~default:s2 (fun s1 -> SI.P.proof_p1 s1 s2 p) s1 - let p1_map s1 s2 p = - let s2 = s2 p in - SI.P.proof_p1 s1 s2 p + let pr_p1 p s1 s2 = SI.P.proof_p1 s1 s2 p (* preprocess "ite" away *) let preproc_ite self si (module PA:SI.PREPROCESS_ACTS) (t:T.t) : (T.t * SI.proof_step Iter.t) option = @@ -211,60 +208,66 @@ module Make(A : ARG) : S with module A = A = struct begin match A.view_as_bool a' with | B_bool true -> (* [a=true |- ite a b c=b], [|- a=true] ==> [|- t=b] *) - add_step_ @@ SI.with_proof si (A.lemma_ite_true ~a:a' ~ite:t); + add_step_ @@ A.lemma_ite_true ~a:a' ~ite:t PA.proof; ret b | B_bool false -> (* [a=false |- ite a b c=c], [|- a=false] ==> [|- t=c] *) - add_step_ @@ SI.with_proof si (A.lemma_ite_false ~a:a' ~ite:t); + add_step_ @@ A.lemma_ite_false ~a:a' ~ite:t PA.proof; ret c | _ -> let t_ite = fresh_term self ~for_t:t ~pre:"ite" (T.ty b) in SI.define_const si ~const:t_ite ~rhs:t; - let pr_def = SI.with_proof si (SI.P.define_term t_ite t) in - let lit_a = PA.mk_lit a' in + let pr_def = SI.P.define_term t_ite t PA.proof in + let lit_a = PA.mk_lit_nopreproc a' in (* TODO: use unit paramod on each clause with side t=t_ite and on a=a' *) - PA.add_clause [Lit.neg lit_a; PA.mk_lit (eq self.tst t_ite b)] - (p1_map pr_def @@ p1_opt pr_a (A.lemma_ite_true ~a:a' ~ite:t)); - PA.add_clause [lit_a; PA.mk_lit (eq self.tst t_ite c)] - (p1_map pr_def @@ p1_opt pr_a (A.lemma_ite_false ~a:a' ~ite:t)); + PA.add_clause [Lit.neg lit_a; PA.mk_lit_nopreproc (eq self.tst t_ite b)] + (pr_p1 PA.proof pr_def @@ pr_p1_opt PA.proof pr_a @@ + A.lemma_ite_true ~a:a' ~ite:t PA.proof); + PA.add_clause [lit_a; PA.mk_lit_nopreproc (eq self.tst t_ite c)] + (pr_p1 PA.proof pr_def @@ pr_p1_opt PA.proof pr_a @@ + A.lemma_ite_false ~a:a' ~ite:t PA.proof); ret t_ite end | _ -> None (* TODO: polarity? *) - let cnf (self:state) (si:SI.t) (module PA:SI.PREPROCESS_ACTS) (t:T.t) : T.t option = + let cnf (self:state) (si:SI.t) (module PA:SI.PREPROCESS_ACTS) + (t:T.t) : (T.t * _ Iter.t) option = Log.debugf 50 (fun k->k"(@[th-bool.cnf@ %a@])" T.pp t); - - let mk_lit = PA.mk_lit in + let steps = ref [] in + let[@inline] add_step s = steps := s :: !steps in (* handle boolean equality *) let equiv_ si ~is_xor ~for_t t_a t_b : Lit.t = - let a = mk_lit t_a in - let b = mk_lit t_b in + let a = PA.mk_lit_nopreproc t_a in + let b = PA.mk_lit_nopreproc t_b in let a = if is_xor then Lit.neg a else a in (* [a xor b] is [(¬a) = b] *) - let t_proxy, proxy = fresh_lit ~for_t ~mk_lit:PA.mk_lit ~pre:"equiv_" self in + let t_proxy, proxy = fresh_lit ~for_t ~mk_lit:PA.mk_lit_nopreproc ~pre:"equiv_" self in SI.define_const si ~const:t_proxy ~rhs:for_t; - let pr_def = SI.with_proof si (SI.P.define_term t_proxy for_t) in + let pr_def = SI.P.define_term t_proxy for_t PA.proof in + add_step pr_def; - let add_clause c pr = - PA.add_clause c pr - in + let[@inline] add_clause c pr = PA.add_clause c pr in (* proxy => a<=> b, ¬proxy => a xor b *) add_clause [Lit.neg proxy; Lit.neg a; b] - (if is_xor then A.lemma_bool_c "xor-e+" [t_proxy] - else A.lemma_bool_c "eq-e" [t_proxy; t_a]); + (pr_p1 PA.proof pr_def @@ + if is_xor then A.lemma_bool_c "xor-e+" [for_t] PA.proof + else A.lemma_bool_c "eq-e" [for_t; t_a] PA.proof); add_clause [Lit.neg proxy; Lit.neg b; a] - (if is_xor then A.lemma_bool_c "xor-e-" [t_proxy] - else A.lemma_bool_c "eq-e" [t_proxy; t_b]); + (pr_p1 PA.proof pr_def @@ + if is_xor then A.lemma_bool_c "xor-e-" [for_t] PA.proof + else A.lemma_bool_c "eq-e" [for_t; t_b] PA.proof); add_clause [proxy; a; b] - (if is_xor then A.lemma_bool_c "xor-i" [t_proxy; t_a] - else A.lemma_bool_c "eq-i+" [t_proxy]); + (pr_p1 PA.proof pr_def @@ + if is_xor then A.lemma_bool_c "xor-i" [for_t; t_a] PA.proof + else A.lemma_bool_c "eq-i+" [for_t] PA.proof); add_clause [proxy; Lit.neg a; Lit.neg b] - (if is_xor then A.lemma_bool_c "xor-i" [t_proxy; t_b] - else A.lemma_bool_c "eq-i-" [t_proxy]); + (pr_p1 PA.proof pr_def @@ + if is_xor then A.lemma_bool_c "xor-i" [for_t; t_b] PA.proof + else A.lemma_bool_c "eq-i-" [for_t] PA.proof); proxy in @@ -279,57 +282,66 @@ module Make(A : ARG) : S with module A = A = struct | B_and l -> let t_subs = Iter.to_list l in - let subs = List.map mk_lit t_subs in - let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit:PA.mk_lit ~pre:"and_" self in + let subs = List.map PA.mk_lit_nopreproc t_subs in + let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit:PA.mk_lit_nopreproc ~pre:"and_" self in SI.define_const si ~const:t_proxy ~rhs:t; - SI.with_proof si (SI.P.define_term t_proxy t); + let pr_def = SI.P.define_term t_proxy t PA.proof in + add_step pr_def; + (* add clauses *) List.iter2 (fun t_u u -> PA.add_clause [Lit.neg proxy; u] - (A.lemma_bool_c "and-e" [t_proxy; t_u])) + (pr_p1 PA.proof pr_def @@ A.lemma_bool_c "and-e" [t; t_u] PA.proof)) t_subs subs; PA.add_clause (proxy :: List.map Lit.neg subs) - (A.lemma_bool_c "and-i" [t_proxy]); + (pr_p1 PA.proof pr_def @@ A.lemma_bool_c "and-i" [t] PA.proof); Some proxy | B_or l -> let t_subs = Iter.to_list l in - let subs = List.map mk_lit t_subs in - let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit:PA.mk_lit ~pre:"or_" self in + let subs = List.map PA.mk_lit_nopreproc t_subs in + let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit:PA.mk_lit_nopreproc ~pre:"or_" self in SI.define_const si ~const:t_proxy ~rhs:t; - SI.with_proof si (SI.P.define_term t_proxy t); + let pr_def = SI.P.define_term t_proxy t PA.proof in + add_step pr_def; + (* add clauses *) List.iter2 (fun t_u u -> PA.add_clause [Lit.neg u; proxy] - (A.lemma_bool_c "or-i" [t_proxy; t_u])) + (pr_p1 PA.proof pr_def @@ + A.lemma_bool_c "or-i" [t; t_u] PA.proof)) t_subs subs; PA.add_clause (Lit.neg proxy :: subs) - (A.lemma_bool_c "or-e" [t_proxy]); + (pr_p1 PA.proof pr_def @@ A.lemma_bool_c "or-e" [t] PA.proof); Some proxy | B_imply (t_args, t_u) -> (* transform into [¬args \/ u] on the fly *) let t_args = Iter.to_list t_args in - let args = List.map (fun t -> Lit.neg (mk_lit t)) t_args in - let u = mk_lit t_u in + let args = List.map (fun t -> Lit.neg (PA.mk_lit_nopreproc t)) t_args in + let u = PA.mk_lit_nopreproc t_u in let subs = u :: args in (* now the or-encoding *) - let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit:PA.mk_lit ~pre:"implies_" self in + let t_proxy, proxy = + fresh_lit ~for_t:t ~mk_lit:PA.mk_lit_nopreproc ~pre:"implies_" self in SI.define_const si ~const:t_proxy ~rhs:t; - SI.with_proof si (SI.P.define_term t_proxy t); + let pr_def = SI.P.define_term t_proxy t PA.proof in + add_step pr_def; (* add clauses *) List.iter2 (fun t_u u -> PA.add_clause [Lit.neg u; proxy] - (A.lemma_bool_c "imp-i" [t_proxy; t_u])) + (pr_p1 PA.proof pr_def @@ + A.lemma_bool_c "imp-i" [t_proxy; t_u] PA.proof)) (t_u::t_args) subs; PA.add_clause (Lit.neg proxy :: subs) - (A.lemma_bool_c "imp-e" [t_proxy]); + (pr_p1 PA.proof pr_def @@ + A.lemma_bool_c "imp-e" [t_proxy] PA.proof); Some proxy | B_ite _ | B_eq _ | B_neq _ -> None @@ -344,7 +356,7 @@ module Make(A : ARG) : S with module A = A = struct let u = Lit.term lit in (* put sign back as a "not" *) let u = if Lit.sign lit then u else A.mk_bool self.tst (B_not u) in - if T.equal u t then None else Some u + if T.equal u t then None else Some (u, Iter.of_list !steps) end (* check if new terms were added to the congruence closure, that can be turned