From ff7a87f3fbb94fd358f6a956f17d93d7f27b84ec Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 15 Apr 2021 00:03:15 -0400 Subject: [PATCH] wip: feat(proof): insert proof constructs in most of sidekick --- src/cc/Sidekick_cc.ml | 21 +- src/core/Sidekick_core.ml | 72 ++++-- src/lra/sidekick_arith_lra.ml | 55 +++-- src/msat-solver/Sidekick_msat_solver.ml | 208 ++++++++++++------ src/smtlib/Process.ml | 2 +- src/smtlib/Proof.ml | 20 +- src/th-bool-static/Sidekick_th_bool_static.ml | 176 +++++++++------ src/th-data/Sidekick_th_data.ml | 11 +- 8 files changed, 385 insertions(+), 180 deletions(-) diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml index 7286c1d2..69c44f9d 100644 --- a/src/cc/Sidekick_cc.ml +++ b/src/cc/Sidekick_cc.ml @@ -95,6 +95,7 @@ module Make (A: CC_ARG) | E_congruence of node * node (* caused by normal congruence *) | E_and of explanation * explanation | E_theory of explanation + | E_proof of P.t type repr = node @@ -168,6 +169,7 @@ module Make (A: CC_ARG) | E_merge (a,b) -> Fmt.fprintf out "(@[merge@ %a@ %a@])" N.pp a N.pp b | E_merge_t (a,b) -> Fmt.fprintf out "(@[merge@ @[:n1 %a@]@ @[:n2 %a@]@])" Term.pp a Term.pp b | E_theory e -> Fmt.fprintf out "(@[th@ %a@])" pp e + | E_proof p -> Fmt.fprintf out "(@[proof@ %a@])" P.pp p | E_and (a,b) -> Format.fprintf out "(@[and@ %a@ %a@])" pp a pp b @@ -177,6 +179,7 @@ module Make (A: CC_ARG) let[@inline] mk_merge_t a b : t = if Term.equal a b then mk_reduction else E_merge_t (a,b) let[@inline] mk_lit l : t = E_lit l let mk_theory e = E_theory e + let mk_proof p = E_proof p let rec mk_list l = match l with @@ -280,7 +283,7 @@ module Make (A: CC_ARG) and ev_on_post_merge = t -> actions -> N.t -> N.t -> unit and ev_on_new_term = t -> N.t -> term -> unit and ev_on_conflict = t -> th:bool -> lit list -> unit - and ev_on_propagate = t -> lit -> (unit -> lit list) -> unit + and ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unit and ev_on_is_subterm = N.t -> term -> unit let[@inline] size_ (r:repr) = r.n_size @@ -458,6 +461,9 @@ module Make (A: CC_ARG) | E_lit lit -> lit :: acc | E_theory e' -> th := true; explain_decompose cc ~th acc e' + | E_proof _p -> + (* FIXME: need to also return pairs of [t, u, |-t=u] as part of explanation *) + assert false | E_merge (a,b) -> explain_pair cc ~th acc a b | E_merge_t (a,b) -> (* find nodes for [a] and [b] on the fly *) @@ -657,7 +663,7 @@ module Make (A: CC_ARG) Iter.of_list lits |> Iter.map (fun lit -> Lit.term lit, Lit.sign lit) in - P.make_cc lits + P.cc_lemma lits in raise_conflict_ cc ~th:!th acts (List.rev_map Lit.neg lits) proof ); @@ -773,13 +779,18 @@ module Make (A: CC_ARG) let reason = let e = lazy ( let lazy (th, acc) = half_expl in - explain_pair cc ~th acc u1 t1 + let lits = explain_pair cc ~th acc u1 t1 in + let p = + A.P.cc_lemma + (Iter.of_list lits |> Iter.map (fun l -> Lit.term l, Lit.sign l)) + in + lits, p ) in fun () -> Lazy.force e in List.iter (fun f -> f cc lit reason) cc.on_propagate; Stat.incr cc.count_props; - Actions.propagate acts lit ~reason P.default + Actions.propagate acts lit ~reason | _ -> ()) module Debug_ = struct @@ -845,7 +856,7 @@ module Make (A: CC_ARG) Iter.of_list lits |> Iter.map (fun lit -> Lit.term lit, Lit.sign lit) in - P.make_cc lits + P.cc_lemma lits in raise_conflict_ cc ~th:!th acts lits proof diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index 04057117..7100cdfe 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -147,10 +147,24 @@ end module type PROOF = sig type term + type clause type t val pp : t Fmt.printer - val default : t - val make_cc : (term*bool) Iter.t -> t + + (** hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation *) + type hres_step = | R | R1 | P | P1 + + val hres_iter : t -> (hres_step * t) Iter.t -> t (* hyper-res *) + val hres_l : t -> (hres_step * t) list -> t (* hyper-res *) + 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 cc_lemma : (term*bool) 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] *) + val sorry : t [@@alert cstor "sorry used"] (* proof hole when we don't know how to produce a proof *) + + val default : t [@@alert cstor "do not use default constructor"] end (** Literals @@ -208,7 +222,7 @@ module type CC_ACTIONS = sig exception). @param pr the proof of [c] being a tautology *) - val propagate : t -> Lit.t -> reason:(unit -> Lit.t list) -> P.t -> unit + val propagate : t -> Lit.t -> reason:(unit -> Lit.t list * P.t) -> unit (** [propagate acts lit ~reason pr] declares that [reason() => lit] is a tautology. @@ -310,6 +324,7 @@ module type CC_S = sig val mk_merge_t : term -> term -> t val mk_lit : lit -> t val mk_list : t list -> t + val mk_proof : P.t -> t val mk_theory : t -> t (* TODO: indicate what theory, or even provide a lemma *) end @@ -362,7 +377,7 @@ module type CC_S = sig participating in the conflict are purely syntactic theories like injectivity of constructors. *) - type ev_on_propagate = t -> lit -> (unit -> lit list) -> unit + type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unit (** [ev_on_propagate cc lit reason] is called whenever [reason() => lit] is a propagated lemma. See {!CC_ACTIONS.propagate}. *) @@ -437,6 +452,8 @@ module type CC_S = sig val assert_lits : t -> lit Iter.t -> unit (** Addition of many literals *) + (* FIXME: this needs to return [lit list * (term*term*P.t) list]. + the explanation is [/\_i lit_i /\ /\_j (|- t_j=u_j) |- n1=n2] *) val explain_eq : t -> N.t -> N.t -> lit list (** Explain why the two nodes are equal. Fails if they are not, in an unspecified way *) @@ -546,7 +563,7 @@ module type SOLVER_INTERNAL = sig val clear : t -> unit (** Reset internal cache, etc. *) - type hook = t -> term -> term option + type hook = t -> term -> (term * proof) option (** Given a term, try to simplify it. Return [None] if it didn't change. A simple example could be a hook that takes a term [t], @@ -557,6 +574,11 @@ module type SOLVER_INTERNAL = sig (** Normalize a term using all the hooks. This performs a fixpoint, i.e. it only stops when no hook applies anywhere inside the term. *) + + val normalize_t : t -> term -> term * P.t + (** Normalize a term using all the hooks, along with a proof that the + simplification is correct. + returns [t, refl t] if no simplification occurred. *) end type simplify_hook = Simplify.hook @@ -566,12 +588,18 @@ module type SOLVER_INTERNAL = sig val simplifier : t -> Simplify.t - val simp_t : t -> term -> term - (** Simplify the term using the solver's simplifier (see {!simplifier}) *) + val simplify_t : t -> term -> (term * proof) option + (** Simplify input term, returns [Some (u, |- t=u)] if some + simplification occurred. *) + + val simp_t : t -> term -> term * proof + (** [simp_t si t] returns [u, |- t=u] even if no simplification occurred + (in which case [t == u] syntactically). + (see {!simplifier}) *) (** {3 hooks for the theory} *) - val propagate : t -> actions -> lit -> reason:(unit -> lit list) -> proof -> unit + val propagate : t -> actions -> lit -> reason:(unit -> lit list * proof) -> unit (** Propagate a literal for a reason. This is similar to asserting the clause [reason => lit], but more lightweight, and in a way that is backtrackable. *) @@ -585,19 +613,19 @@ module type SOLVER_INTERNAL = sig If the SAT solver backtracks, this (potential) decision is removed and forgotten. *) - val propagate: t -> actions -> lit -> (unit -> lit list) -> unit + val propagate: t -> actions -> lit -> (unit -> lit list * proof) -> unit (** Propagate a boolean using a unit clause. [expl => lit] must be a theory lemma, that is, a T-tautology *) - val propagate_l: t -> actions -> lit -> lit list -> unit + val propagate_l: t -> actions -> lit -> lit list -> proof -> unit (** Propagate a boolean using a unit clause. [expl => lit] must be a theory lemma, that is, a T-tautology *) - val add_clause_temp : t -> actions -> lit list -> unit + val add_clause_temp : t -> actions -> lit list -> proof -> unit (** Add local clause to the SAT solver. This clause will be removed when the solver backtracks. *) - val add_clause_permanent : t -> actions -> lit list -> unit + val add_clause_permanent : t -> actions -> lit list -> proof -> unit (** Add toplevel clause to the SAT solver. This clause will not be backtracked. *) @@ -605,7 +633,7 @@ module type SOLVER_INTERNAL = sig (** Create a literal. This automatically preprocesses the term. *) val preprocess_term : - t -> add_clause:(Lit.t list -> unit) -> term -> term + t -> add_clause:(Lit.t list -> proof -> unit) -> term -> term * proof (** Preprocess a term. *) val add_lit : t -> actions -> lit -> unit @@ -661,7 +689,7 @@ module type SOLVER_INTERNAL = sig val on_cc_conflict : t -> (CC.t -> th:bool -> lit list -> unit) -> unit (** Callback called on every CC conflict *) - val on_cc_propagate : t -> (CC.t -> lit -> (unit -> lit list) -> unit) -> unit + val on_cc_propagate : t -> (CC.t -> lit -> (unit -> lit list * proof) -> unit) -> unit (** Callback called on every CC propagation *) val on_partial_check : t -> (t -> actions -> lit Iter.t -> unit) -> unit @@ -688,9 +716,10 @@ module type SOLVER_INTERNAL = sig type preprocess_hook = t -> mk_lit:(term -> lit) -> - add_clause:(lit list -> unit) -> - term -> term option - (** Given a term, try to preprocess it. Return [None] if it didn't change. + add_clause:(lit list -> proof -> unit) -> + term -> (term * proof) option + (** Given a term, try to preprocess it. Return [None] if it didn't change, + or [Some (u,p)] if [t=u] and [p] is a proof of [t=u]. Can also add clauses to define new terms. Preprocessing might transform terms to make them more amenable @@ -853,6 +882,11 @@ module type SOLVER = sig *) end + (** {3 Proof type} + + The representation of a full proof, including toplevel steps + with intermediate, named, clauses. Each clause is justified by + a {!P.t} lemma. *) module Proof : sig type t val check : t -> unit @@ -906,11 +940,11 @@ module type SOLVER = sig val mk_atom_t : t -> ?sign:bool -> term -> Atom.t (** Turn a boolean term, with a sign, into a SAT solver's literal. *) - val add_clause : t -> Atom.t IArray.t -> unit + val add_clause : t -> Atom.t IArray.t -> P.t -> unit (** [add_clause solver cs] adds a boolean clause to the solver. Subsequent calls to {!solve} will need to satisfy this clause. *) - val add_clause_l : t -> Atom.t list -> unit + val add_clause_l : t -> Atom.t list -> P.t -> unit (** Same as {!add_clause} but with a list of atoms. *) (** Result of solving for the current set of clauses *) diff --git a/src/lra/sidekick_arith_lra.ml b/src/lra/sidekick_arith_lra.ml index 0cecd511..3221db62 100644 --- a/src/lra/sidekick_arith_lra.ml +++ b/src/lra/sidekick_arith_lra.ml @@ -57,6 +57,9 @@ module type ARG = sig val has_ty_real : term -> bool (** Does this term have the type [Real] *) + (** TODO: actual proof *) + val proof_lra : S.lemma + module Gensym : sig type t @@ -228,12 +231,22 @@ module Make(A : ARG) : S with module A = A = struct proxy (* preprocess linear expressions away *) - let preproc_lra (self:state) si ~mk_lit ~add_clause (t:T.t) : T.t option = + let preproc_lra (self:state) si ~mk_lit ~add_clause + (t:T.t) : (T.t * _) option = Log.debugf 50 (fun k->k "lra.preprocess %a" T.pp t); let tst = SI.tst si in + let sub_proofs_ = ref [] in + (* preprocess subterm *) - let preproc_t = SI.preprocess_term ~add_clause si in + let preproc_t t = + let u, p_t_eq_u = SI.preprocess_term ~add_clause si t in + if t != u then ( + (* add [|- t=u] to hyps *) + sub_proofs_ := (t,u,p_t_eq_u) :: !sub_proofs_; + ); + u + in (* tell the CC this term exists *) let declare_term_to_cc t = @@ -255,9 +268,9 @@ module Make(A : ARG) : S with module A = A = struct let lit_t = mk_lit t in let lit_u1 = mk_lit u1 in let lit_u2 = mk_lit u2 in - add_clause [SI.Lit.neg lit_t; lit_u1]; - add_clause [SI.Lit.neg lit_t; lit_u2]; - add_clause [SI.Lit.neg lit_u1; SI.Lit.neg lit_u2; lit_t]; + add_clause [SI.Lit.neg lit_t; lit_u1] A.proof_lra; + add_clause [SI.Lit.neg lit_t; lit_u2] A.proof_lra; + add_clause [SI.Lit.neg lit_u1; SI.Lit.neg lit_u2; lit_t] A.proof_lra; ); None @@ -292,7 +305,9 @@ module Make(A : ARG) : S with module A = A = struct end; Log.debugf 10 (fun k->k "lra.preprocess:@ %a@ :into %a" T.pp t T.pp new_t); - Some new_t + (* FIXME: by def proxy + LRA *) + let proof = A.S.P.sorry in + Some (new_t, proof) | Some (coeff, v), pred -> (* [c . v <= const] becomes a direct simplex constraint [v <= const/c] *) @@ -317,7 +332,8 @@ module Make(A : ARG) : S with module A = A = struct end; Log.debugf 10 (fun k->k "lra.preprocess@ :%a@ :into %a" T.pp t T.pp new_t); - Some new_t + let proof = A.proof_lra in + Some (new_t, proof) end | LRA_op _ | LRA_mult _ -> @@ -330,7 +346,10 @@ module Make(A : ARG) : S with module A = A = struct let proxy = var_encoding_comb self ~pre:"_le" le_comb in declare_term_to_cc proxy; - Some proxy + (* TODO: proof by def of proxy *) + let proof = A.S.P.sorry in + + Some (proxy, proof) ) else ( (* a bit more complicated: we cannot just define [proxy := le_comb] because of the coefficient. @@ -355,24 +374,26 @@ module Make(A : ARG) : S with module A = A = struct add_clause [ mk_lit (A.mk_lra tst (LRA_simplex_pred (proxy2, Leq, Q.neg le_const))) - ]; + ] A.S.P.sorry; (* TODO: by-def proxy2 + LRA *) add_clause [ mk_lit (A.mk_lra tst (LRA_simplex_pred (proxy2, Geq, Q.neg le_const))) - ]; + ] A.S.P.sorry; (* TODO: by-def proxy2 + LRA *) - Some proxy + (* FIXME: actual proof *) + let proof = A.S.P.sorry in + Some (proxy, proof) ) | LRA_other t when A.has_ty_real t -> None | LRA_const _ | LRA_simplex_pred _ | LRA_simplex_var _ | LRA_other _ -> None - let simplify (self:state) (_recurse:_) (t:T.t) : T.t option = + let simplify (self:state) (_recurse:_) (t:T.t) : (T.t * SI.proof) option = match A.view_as_lra t with | LRA_op _ | LRA_mult _ -> let le = as_linexp_id t in if LE.is_const le then ( let c = LE.const le in - Some (A.mk_lra self.tst (LRA_const c)) + Some (A.mk_lra self.tst (LRA_const c), A.proof_lra) ) else None | LRA_pred (pred, l1, l2) -> let le = LE.(as_linexp_id l1 - as_linexp_id l2) in @@ -386,7 +407,7 @@ module Make(A : ARG) : S with module A = A = struct | Eq -> Q.(c = zero) | Neq -> Q.(c <> zero) in - Some (A.mk_bool self.tst is_true) + Some (A.mk_bool self.tst is_true, A.proof_lra) ) else None | _ -> None @@ -400,13 +421,15 @@ module Make(A : ARG) : S with module A = A = struct |> CCList.flat_map (Tag.to_lits si) |> List.rev_map SI.Lit.neg in - SI.raise_conflict si acts confl SI.P.default + (* TODO: more detailed proof certificate *) + SI.raise_conflict si acts confl A.proof_lra let on_propagate_ si acts lit ~reason = match lit with | Tag.Lit lit -> + (* TODO: more detailed proof certificate *) SI.propagate si acts lit - (fun() -> CCList.flat_map (Tag.to_lits si) reason) + (fun() -> CCList.flat_map (Tag.to_lits si) reason, A.proof_lra) | _ -> () let check_simplex_ self si acts : SimpSolver.Subst.t = diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml index 7ee807ca..d9f90d0b 100644 --- a/src/msat-solver/Sidekick_msat_solver.ml +++ b/src/msat-solver/Sidekick_msat_solver.ml @@ -93,8 +93,8 @@ module Make(A : ARG) type t = msat_acts let[@inline] raise_conflict a lits pr = a.Msat.acts_raise_conflict lits pr - let[@inline] propagate a lit ~reason pr = - let reason = Msat.Consequence (fun () -> reason(), pr) in + let[@inline] propagate a lit ~reason = + let reason = Msat.Consequence reason in a.Msat.acts_propagate lit reason end end @@ -134,7 +134,7 @@ module Make(A : ARG) mutable hooks: hook list; cache: Term.t Term.Tbl.t; } - and hook = t -> term -> term option + and hook = t -> term -> (term * P.t) option let create tst ty_st : t = {tst; ty_st; hooks=[]; cache=Term.Tbl.create 32;} @@ -143,9 +143,11 @@ module Make(A : ARG) let add_hook self f = self.hooks <- f :: self.hooks let clear self = Term.Tbl.clear self.cache - let normalize (self:t) (t:Term.t) : Term.t = + let normalize (self:t) (t:Term.t) : (Term.t * P.t) option = + let sub_proofs_ = ref [] in + (* compute and cache normal form of [t] *) - let rec aux t = + let rec aux t : Term.t = match Term.Tbl.find self.cache t with | u -> u | exception Not_found -> @@ -160,10 +162,23 @@ module Make(A : ARG) | h :: hooks_tl -> match h self t with | None -> aux_rec t hooks_tl - | Some u when Term.equal t u -> aux_rec t hooks_tl - | Some u -> aux u + | Some (u, _) when Term.equal t u -> aux_rec t hooks_tl + | Some (u, pr_t_u) -> + sub_proofs_ := pr_t_u :: !sub_proofs_; + aux u in - aux t + let u = aux t in + if Term.equal t u then None + else ( + (* proof: [sub_proofs |- t=u] by CC *) + let pr = P.cc_imply_l !sub_proofs_ t u in + Some (u, pr) + ) + + let normalize_t self t = + match normalize self t with + | None -> t, P.refl t + | Some (u,pr) -> u, pr end type simplify_hook = Simplify.hook @@ -180,7 +195,7 @@ module Make(A : ARG) simp: Simplify.t; mutable preprocess: preprocess_hook list; mutable mk_model: model_hook list; - preprocess_cache: Term.t Term.Tbl.t; + preprocess_cache: (Term.t * P.t) Term.Tbl.t; mutable th_states : th_states; (** Set of theories *) mutable on_partial_check: (t -> actions -> lit Iter.t -> unit) list; mutable on_final_check: (t -> actions -> lit Iter.t -> unit) list; @@ -190,8 +205,8 @@ module Make(A : ARG) and preprocess_hook = t -> mk_lit:(term -> lit) -> - add_clause:(lit list -> unit) -> - term -> term option + add_clause:(lit list -> P.t -> unit) -> + term -> (term * P.t) option and model_hook = recurse:(t -> CC.N.t -> term) -> @@ -216,7 +231,9 @@ module Make(A : ARG) let stats t = t.stat let simplifier self = self.simp - let simp_t self (t:Term.t) : Term.t = Simplify.normalize self.simp t + let simplify_t self (t:Term.t) : _ option = Simplify.normalize self.simp t + let simp_t self (t:Term.t) : Term.t * P.t = Simplify.normalize_t self.simp t + let add_simplifier (self:t) f : unit = Simplify.add_hook self.simp f let on_preprocess self f = self.preprocess <- f :: self.preprocess @@ -226,34 +243,58 @@ module Make(A : ARG) let sign = Lit.sign lit in acts.Msat.acts_add_decision_lit (Lit.abs lit) sign - let[@inline] raise_conflict self acts c : 'a = + let[@inline] raise_conflict self acts c proof : 'a = Stat.incr self.count_conflict; - acts.Msat.acts_raise_conflict c P.default + acts.Msat.acts_raise_conflict c proof - let[@inline] propagate self acts p cs : unit = + let[@inline] propagate self acts p reason : unit = Stat.incr self.count_propagate; - acts.Msat.acts_propagate p (Msat.Consequence (fun () -> cs(), P.default)) + acts.Msat.acts_propagate p (Msat.Consequence reason) - let[@inline] propagate_l self acts p cs : unit = - propagate self acts p (fun()->cs) + let[@inline] propagate_l self acts p cs proof : unit = + propagate self acts p (fun()->cs,proof) - let add_sat_clause_ self acts ~keep lits : unit = + let add_sat_clause_ self acts ~keep lits (proof:P.t) : unit = Stat.incr self.count_axiom; - acts.Msat.acts_add_clause ~keep lits P.default + acts.Msat.acts_add_clause ~keep lits proof - let preprocess_term_ (self:t) ~add_clause (t:term) : term = + let preprocess_term_ (self:t) ~add_clause (t:term) : term * proof = let mk_lit t = Lit.atom self.tst t in (* no further simplification *) (* compute and cache normal form of [t] *) - let rec aux t = + let rec aux t : term * proof = match Term.Tbl.find self.preprocess_cache t with - | u -> u + | up -> up | exception Not_found -> + let sub_p = ref [] in + (* try rewrite at root *) - let t1 = aux_rec t self.preprocess in - (* then map subterms *) - let t2 = Term.map_shallow self.tst aux t1 in (* map subterms *) - let u = if t != t2 then aux t2 (* fixpoint *) else t2 in + let t1 = aux_rec ~sub_p t self.preprocess in + + (* map subterms *) + let t2 = + Term.map_shallow self.tst + (fun t_sub -> + let u_sub, p_t = aux t_sub in + if not (Term.equal t_sub u_sub) then ( + sub_p := p_t :: !sub_p; + ); + u_sub) + t1 + in + + let u = + if not (Term.equal t t2) then ( + (* fixpoint *) + let v, p_t2_v = aux t2 in + if not (Term.equal t2 v) then ( + sub_p := p_t2_v :: !sub_p + ); + v + ) else ( + t2 + ) + in if t != u then ( Log.debugf 5 @@ -261,46 +302,77 @@ module Make(A : ARG) :from %a@ :to %a@])" Term.pp t Term.pp u); ); - Term.Tbl.add self.preprocess_cache t u; - u + let p_t_u = + if t != u then ( + P.cc_imply_l !sub_p t u (* proof: [sub_p |- t=u] *) + ) else P.refl t + in + + Term.Tbl.add self.preprocess_cache t (u,p_t_u); + u, p_t_u + (* try each function in [hooks] successively *) - and aux_rec t hooks = match hooks with + and aux_rec ~sub_p t hooks : term = + match hooks with | [] -> t | h :: hooks_tl -> match h self ~mk_lit ~add_clause t with - | None -> aux_rec t hooks_tl - | Some u -> aux u + | None -> aux_rec ~sub_p t hooks_tl + | Some (u, p_t_u) -> + sub_p := p_t_u :: !sub_p; + let v, p_u_v = aux u in + if t != v then ( + sub_p := p_u_v :: !sub_p; + ); + v in - t |> simp_t self |> aux - let preprocess_lit_ (self:t) ~add_clause (lit:lit) : lit = - let t = Lit.term lit |> preprocess_term_ self ~add_clause in + let t1, p_t_t1 = simp_t self t in + + let u, p_t1_u = aux t1 in + if t != u then ( + let pr = P.cc_imply2 p_t_t1 p_t1_u t u in + u, pr + ) else ( + u, P.refl u + ) + + (* return preprocessed lit + proof they are equal *) + let preprocess_lit_ (self:t) ~add_clause (lit:lit) : lit * proof = + let t, p = Lit.term lit |> preprocess_term_ self ~add_clause in let lit' = Lit.atom self.tst ~sign:(Lit.sign lit) t in Log.debugf 10 - (fun k->k "(@[msat-solver.preprocess.lit@ :lit %a@ :into %a@])" Lit.pp lit Lit.pp lit'); - lit' + (fun k->k "(@[msat-solver.preprocess.lit@ :lit %a@ :into %a@ :proof %a@])" + Lit.pp lit Lit.pp lit' P.pp p); + lit', p (* add a clause using [acts] *) - let add_clause_ self acts lits : unit = + let add_clause_ self acts lits (proof:P.t) : unit = Stat.incr self.count_preprocess_clause; - add_sat_clause_ self acts ~keep:true lits + add_sat_clause_ self acts ~keep:true lits proof - let mk_lit self acts ?sign t = + (* FIXME: should we store the proof somewhere? *) + let mk_lit self acts ?sign t : Lit.t = let add_clause = add_clause_ self acts in - preprocess_lit_ self ~add_clause @@ Lit.atom self.tst ?sign t + let lit, _p = + preprocess_lit_ self ~add_clause @@ Lit.atom self.tst ?sign t + in + lit - let[@inline] preprocess_term self ~add_clause (t:term) : term = + let[@inline] preprocess_term self ~add_clause (t:term) : term * proof = preprocess_term_ self ~add_clause t - let[@inline] add_clause_temp self acts lits : unit = - add_sat_clause_ self acts ~keep:false lits + let[@inline] add_clause_temp self acts lits (proof:P.t) : unit = + add_sat_clause_ self acts ~keep:false lits proof - let[@inline] add_clause_permanent self acts lits : unit = - add_sat_clause_ self acts ~keep:true lits + let[@inline] add_clause_permanent self acts lits (proof:P.t) : unit = + add_sat_clause_ self acts ~keep:true lits proof let add_lit _self acts lit : unit = acts.Msat.acts_mk_lit lit - let add_lit_t self acts ?sign t = add_lit self acts (mk_lit self acts ?sign t) + let add_lit_t self acts ?sign t = + let lit = mk_lit self acts ?sign t in + add_lit self acts lit let on_final_check self f = self.on_final_check <- f :: self.on_final_check let on_partial_check self f = self.on_partial_check <- f :: self.on_partial_check @@ -475,24 +547,29 @@ module Make(A : ARG) | Lemma l -> Fmt.fprintf out "(@[lemma@ %a@])" P.pp l | Duplicate (c, _) -> let n = find_idx_of_proof_ c in - Fmt.fprintf out "(@[dedup@ %d@])" n + Fmt.fprintf out "(@[dedup@ c%d@])" n | Hyper_res { hr_init=init; hr_steps=steps } -> let n_init = find_idx_of_proof_ init in let pp_step out (pivot,p') = + let unit_res = + Array.length (SC.atoms (conclusion p')) = 1 in let n_p' = find_idx_of_proof_ p' in - Fmt.fprintf out "(@[%d@ :pivot %a@])" n_p' pp_atom pivot + if unit_res then ( + Fmt.fprintf out "(@[r1 c%d@])" n_p' + ) else ( + Fmt.fprintf out "(@[r c%d@ :pivot %a@])" n_p' pp_atom pivot + ) in Fmt.fprintf out "(@[hres@ %d@ (@[%a@])@])" n_init Fmt.(list ~sep:(return "@ ") pp_step) steps - in - Fmt.fprintf out "(@[step %d@ (@[cl %a@])@ (@[<1>src@ %a@])@])@ " + Fmt.fprintf out "(@[defc c%d@ (@[cl %a@])@ (@[<1>src@ %a@])@])@ " idx Fmt.(list ~sep:(return "@ ") pp_atom) atoms pp_step step; ) in - Fmt.fprintf out "(@[proof@ "; + Fmt.fprintf out "(@[quip 1@ "; Sat_solver.Proof.fold pp_node () self; Fmt.fprintf out "@])@."; () @@ -564,7 +641,7 @@ module Make(A : ARG) let tst = Solver_internal.tst self.si in Sat_solver.assume self.solver [ [Lit.atom tst @@ Term.bool tst true]; - ] P.default; + ] P.true_is_true end; self @@ -600,18 +677,18 @@ module Make(A : ARG) ()) let rec mk_atom_lit self lit : Atom.t = - let lit = preprocess_lit_ self lit in + let lit, _proof = preprocess_lit_ self lit in add_bool_subterms_ self (Lit.term lit); Sat_solver.make_atom self.solver lit - and preprocess_lit_ self lit : Lit.t = - Solver_internal.preprocess_lit_ - ~add_clause:(fun lits -> - (* recursively add these sub-literals, so they're also properly processed *) - Stat.incr self.si.count_preprocess_clause; - let atoms = List.map (mk_atom_lit self) lits in - Sat_solver.add_clause self.solver atoms P.default) - self.si lit + and preprocess_lit_ self lit : Lit.t * P.t = + Solver_internal.preprocess_lit_ + ~add_clause:(fun lits proof -> + (* recursively add these sub-literals, so they're also properly processed *) + Stat.incr self.si.count_preprocess_clause; + let atoms = List.map (mk_atom_lit self) lits in + Sat_solver.add_clause self.solver atoms proof) + self.si lit let[@inline] mk_atom_t self ?sign t : Atom.t = let lit = Lit.atom (tst self) ?sign t in @@ -667,11 +744,12 @@ module Make(A : ARG) let pp_stats out (self:t) : unit = Stat.pp_all out (Stat.all @@ stats self) - let add_clause (self:t) (c:Atom.t IArray.t) : unit = + let add_clause (self:t) (c:Atom.t IArray.t) (proof:P.t) : unit = Stat.incr self.count_clause; - Log.debugf 50 (fun k->k "(@[solver.add-clause@ %a@])" (Util.pp_iarray Atom.pp) c); + Log.debugf 50 (fun k->k "(@[solver.add-clause@ %a@ :proof %a@])" + (Util.pp_iarray Atom.pp) c P.pp proof); let pb = Profile.begin_ "add-clause" in - Sat_solver.add_clause_a self.solver (c:> Atom.t array) P.default; + Sat_solver.add_clause_a self.solver (c:> Atom.t array) proof; Profile.exit pb let add_clause_l self c = add_clause self (IArray.of_list c) diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index 8688b932..3f16755e 100644 --- a/src/smtlib/Process.ml +++ b/src/smtlib/Process.ml @@ -271,7 +271,7 @@ let process_stmt ); let atom = Solver.mk_atom_t solver t in CCOpt.iter (fun h -> Vec.push h [atom]) hyps; - Solver.add_clause solver (IArray.singleton atom); + Solver.add_clause solver (IArray.singleton atom) (Proof.assertion t); E.return() | Statement.Stmt_assert_clause c -> if pp_cnf then ( diff --git a/src/smtlib/Proof.ml b/src/smtlib/Proof.ml index dadec898..98a06878 100644 --- a/src/smtlib/Proof.ml +++ b/src/smtlib/Proof.ml @@ -4,14 +4,26 @@ type term = T.t type t = | Unspecified + | Sorry of term + | CC_lemma_imply of t list * term * term | CC_lemma of (term * bool) list + | Assertion of term + let default=Unspecified +let sorry t = Sorry t let make_cc iter : t = CC_lemma (Iter.to_rev_list iter) -let pp out = function +let assertion t = Assertion t + + + +let rec pp out (self:t) : unit = + let pp_signed_t_ out (t,b) = + if b then T.pp out t else Fmt.fprintf out "(@[not@ %a@])" T.pp t + in + match self with | Unspecified -> Fmt.string out "" + | CC_lemma_imply (l,t,u) -> + Fmt.fprintf out "(@[cc-lemma@ (@[%a@])@])" | CC_lemma l -> - let pp_lit out (t,b) = - if b then T.pp out t else Fmt.fprintf out "(@[not@ %a@])" T.pp t - in Fmt.fprintf out "(@[cc-lemma@ (@[%a@])@])" Fmt.(list ~sep:(return "@ ") pp_lit) l diff --git a/src/th-bool-static/Sidekick_th_bool_static.ml b/src/th-bool-static/Sidekick_th_bool_static.ml index 6668750d..ec6a8e76 100644 --- a/src/th-bool-static/Sidekick_th_bool_static.ml +++ b/src/th-bool-static/Sidekick_th_bool_static.ml @@ -27,6 +27,15 @@ module type ARG = sig val view_as_bool : term -> (term, term Iter.t) bool_view (** Project the term into the boolean view. *) + (** [proof_ite_true (ite a b c)] is [a=true |- ite a b c = b] *) + val proof_ite_true : S.T.Term.t -> S.P.t + + (** [proof_ite_false (ite a b c)] is [a=false |- ite a b c = c] *) + val proof_ite_false : S.T.Term.t -> S.P.t + + (** By basic boolean logic to prove [a=b] *) + val proof_bool : S.T.Term.t -> S.T.Term.t -> S.P.t + val mk_bool : S.T.Term.state -> (term, term IArray.t) bool_view -> term (** Make a term from the given boolean view. *) @@ -86,13 +95,12 @@ module Make(A : ARG) : S with module A = A = struct type state = { tst: T.state; ty_st: Ty.state; - simps: T.t T.Tbl.t; (* cache *) - cnf: Lit.t T.Tbl.t; (* tseitin CNF *) + cnf: (Lit.t * SI.P.t) T.Tbl.t; (* tseitin CNF *) gensym: A.Gensym.t; } let create tst ty_st : state = - { tst; ty_st; simps=T.Tbl.create 128; + { tst; ty_st; cnf=T.Tbl.create 128; gensym=A.Gensym.create tst; } @@ -107,47 +115,52 @@ module Make(A : ARG) : S with module A = A = struct let is_true t = match T.as_bool t with Some true -> true | _ -> false let is_false t = match T.as_bool t with Some false -> true | _ -> false - let simplify (self:state) (simp:SI.Simplify.t) (t:T.t) : T.t option = + let simplify (self:state) (simp:SI.Simplify.t) (t:T.t) : (T.t * SI.P.t) option = let tst = self.tst in + let ret u = Some (u, A.proof_bool t u) in match A.view_as_bool t with | B_bool _ -> None - | B_not u when is_true u -> Some (T.bool tst false) - | B_not u when is_false u -> Some (T.bool tst true) + | B_not u when is_true u -> ret (T.bool tst false) + | B_not u when is_false u -> ret (T.bool tst true) | B_not _ -> None | B_opaque_bool _ -> None | B_and a -> - if Iter.exists is_false a then Some (T.bool tst false) - else if Iter.for_all is_true a then Some (T.bool tst true) + if Iter.exists is_false a then ret (T.bool tst false) + else if Iter.for_all is_true a then ret (T.bool tst true) else None | B_or a -> - if Iter.exists is_true a then Some (T.bool tst true) - else if Iter.for_all is_false a then Some (T.bool tst false) + if Iter.exists is_true a then ret (T.bool tst true) + else if Iter.for_all is_false a then ret (T.bool tst false) else None | B_imply (args, u) -> - if Iter.exists is_false args then Some (T.bool tst true) - else if is_true u then Some (T.bool tst true) + if Iter.exists is_false args then ret (T.bool tst true) + else if is_true u then ret (T.bool tst true) else None | B_ite (a,b,c) -> (* directly simplify [a] so that maybe we never will simplify one of the branches *) - let a = SI.Simplify.normalize simp a in + let a, pr_a = SI.Simplify.normalize_t simp a in begin match A.view_as_bool a with - | B_bool true -> Some b - | B_bool false -> Some c + | B_bool true -> + let pr = SI.P.(hres_l (A.proof_ite_true t) [R1, pr_a]) in + Some (b, pr) + | B_bool false -> + let pr = SI.P.(hres_l (A.proof_ite_false t) [R1, pr_a]) in + Some (c, pr) | _ -> None end - | B_equiv (a,b) when is_true a -> Some b - | B_equiv (a,b) when is_false a -> Some (not_ tst b) - | B_equiv (a,b) when is_true b -> Some a - | B_equiv (a,b) when is_false b -> Some (not_ tst a) - | B_xor (a,b) when is_false a -> Some b - | B_xor (a,b) when is_true a -> Some (not_ tst b) - | B_xor (a,b) when is_false b -> Some a - | B_xor (a,b) when is_true b -> Some (not_ tst a) + | B_equiv (a,b) when is_true a -> ret b + | B_equiv (a,b) when is_false a -> ret (not_ tst b) + | B_equiv (a,b) when is_true b -> ret a + | B_equiv (a,b) when is_false b -> ret (not_ tst a) + | B_xor (a,b) when is_false a -> ret b + | B_xor (a,b) when is_true a -> ret (not_ tst b) + | B_xor (a,b) when is_false b -> ret a + | B_xor (a,b) when is_true b -> ret (not_ tst a) | B_equiv _ | B_xor _ -> None - | B_eq (a,b) when T.equal a b -> Some (T.bool tst true) - | B_neq (a,b) when T.equal a b -> Some (T.bool tst true) + | B_eq (a,b) when T.equal a b -> ret (T.bool tst true) + | B_neq (a,b) when T.equal a b -> ret (T.bool tst true) | B_eq _ | B_neq _ -> None | B_atom _ -> None @@ -164,76 +177,101 @@ module Make(A : ARG) : S with module A = A = struct mk_lit proxy (* preprocess "ite" away *) - let preproc_ite self si ~mk_lit ~add_clause (t:T.t) : T.t option = + let preproc_ite self si ~mk_lit ~add_clause (t:T.t) : (T.t * SI.P.t) option = match A.view_as_bool t with | B_ite (a,b,c) -> - let a = SI.simp_t si a in + let a, pr_a = SI.simp_t si a in begin match A.view_as_bool a with - | B_bool true -> Some b - | B_bool false -> Some c + | B_bool true -> + (* [a=true |- ite a b c=b], [|- a=true] ==> [|- t=b] *) + let proof = SI.P.(hres_l (A.proof_ite_true t) [P1, pr_a]) in + Some (b, proof) + | B_bool false -> + (* [a=false |- ite a b c=c], [|- a=false] ==> [|- t=c] *) + let proof = SI.P.(hres_l (A.proof_ite_false t) [P1, pr_a]) in + Some (c, proof) | _ -> let t_ite = fresh_term self ~for_:t ~pre:"ite" (T.ty b) in let lit_a = mk_lit a in - add_clause [Lit.neg lit_a; mk_lit (eq self.tst t_ite b)]; - add_clause [lit_a; mk_lit (eq self.tst t_ite c)]; - Some t_ite + let pr = SI.P.sorry in (* FIXME: proper proof by-def(t_ite) + bool *) + add_clause [Lit.neg lit_a; mk_lit (eq self.tst t_ite b)] pr; + add_clause [lit_a; mk_lit (eq self.tst t_ite c)] pr; + (* TODO: by def t_ite + ite-true + ite-false + + case split [a=true \/ a=false] *) + Some (t_ite, SI.P.sorry) end | _ -> None (* TODO: polarity? *) - let cnf (self:state) (_si:SI.t) ~mk_lit ~add_clause (t:T.t) : T.t option = - let rec get_lit (t:T.t) : Lit.t = + let cnf (self:state) (_si:SI.t) ~mk_lit ~add_clause (t:T.t) : (T.t * SI.P.t) option = + let rec get_lit_and_proof_ (t:T.t) : Lit.t * SI.P.t = let t_abs, t_sign = T.abs self.tst t in - let lit = + let lit_abs, pr = match T.Tbl.find self.cnf t_abs with - | lit -> lit (* cached *) + | lit_pr -> lit_pr (* cached *) | exception Not_found -> (* compute and cache *) - let lit = get_lit_uncached t_abs in + let lit, pr = get_lit_uncached t_abs in if not (T.equal (Lit.term lit) t_abs) then ( - T.Tbl.add self.cnf t_abs lit; + T.Tbl.add self.cnf t_abs (lit, pr); Log.debugf 20 (fun k->k "(@[sidekick.bool.add-lit@ :lit %a@ :for-t %a@])" Lit.pp lit T.pp t_abs); ); - lit + lit, pr in - if t_sign then lit else Lit.neg lit - and equiv_ ~is_xor ~for_ a b : Lit.t = + let lit = if t_sign then lit_abs else Lit.neg lit_abs in + lit, pr + + and equiv_ ~get_lit ~is_xor ~for_ a b : Lit.t = let a = get_lit a in let b = get_lit b in let a = if is_xor then Lit.neg a else a in (* [a xor b] is [(¬a) = b] *) let proxy = fresh_lit ~for_ ~mk_lit ~pre:"equiv_" self in (* proxy => a<=> b, ¬proxy => a xor b *) - add_clause [Lit.neg proxy; Lit.neg a; b]; - add_clause [Lit.neg proxy; Lit.neg b; a]; - add_clause [proxy; a; b]; - add_clause [proxy; Lit.neg a; Lit.neg b]; + let proof = SI.P.sorry in (* FIXME: by_def(proxy) + bool *) + add_clause [Lit.neg proxy; Lit.neg a; b] proof; + add_clause [Lit.neg proxy; Lit.neg b; a] proof; + add_clause [proxy; a; b] proof; + add_clause [proxy; Lit.neg a; Lit.neg b] proof; proxy - and get_lit_uncached t : Lit.t = + (* make a literal for [t], with a proof of [|- abs(t) = abs(lit)] *) + and get_lit_uncached t : Lit.t * SI.P.t = + let sub_p = ref [] in + + let get_lit t = + let lit, pr = get_lit_and_proof_ t in + if Lit.term lit != t then ( + sub_p := pr :: !sub_p; + ); + lit + in + match A.view_as_bool t with - | B_bool b -> mk_lit (T.bool self.tst b) - | B_opaque_bool t -> mk_lit t + | B_bool b -> mk_lit (T.bool self.tst b), SI.P.refl t + | B_opaque_bool t -> mk_lit t, SI.P.refl t | B_not u -> - let lit = get_lit u in - Lit.neg lit + let lit, pr = get_lit_and_proof_ u in + Lit.neg lit, pr | B_and l -> let subs = l |> Iter.map get_lit |> Iter.to_list in let proxy = fresh_lit ~for_:t ~mk_lit ~pre:"and_" self in (* add clauses *) - List.iter (fun u -> add_clause [Lit.neg proxy; u]) subs; - add_clause (proxy :: List.map Lit.neg subs); - proxy + let proof = SI.P.sorry in (* FIXME: by_def(proxy) + bool *) + List.iter (fun u -> add_clause [Lit.neg proxy; u] proof) subs; + add_clause (proxy :: List.map Lit.neg subs) proof; + proxy, proof (* FIXME: use sub_p, by-def(proxy), A.proof_bool *) | B_or l -> let subs = l |> Iter.map get_lit |> Iter.to_list in let proxy = fresh_lit ~for_:t ~mk_lit ~pre:"or_" self in (* add clauses *) - List.iter (fun u -> add_clause [Lit.neg u; proxy]) subs; - add_clause (Lit.neg proxy :: subs); - proxy + let proof = SI.P.sorry in (* FIXME: by_def(proxy) + bool *) + List.iter (fun u -> add_clause [Lit.neg u; proxy] proof) subs; + add_clause (Lit.neg proxy :: subs) proof; + proxy, proof (* FIXME: use sub_p, by-def(proxy), A.proof_bool *) | B_imply (args, u) -> (* transform into [¬args \/ u] on the fly *) let args = args |> Iter.map get_lit |> Iter.map Lit.neg |> Iter.to_list in @@ -242,19 +280,21 @@ module Make(A : ARG) : S with module A = A = struct (* now the or-encoding *) let proxy = fresh_lit ~for_:t ~mk_lit ~pre:"implies_" self in (* add clauses *) - List.iter (fun u -> add_clause [Lit.neg u; proxy]) subs; - add_clause (Lit.neg proxy :: subs); - proxy - | B_ite _ | B_eq _ | B_neq _ -> mk_lit t - | B_equiv (a,b) -> equiv_ ~for_:t ~is_xor:false a b - | B_xor (a,b) -> equiv_ ~for_:t ~is_xor:true a b - | B_atom u -> mk_lit u + let proof = SI.P.sorry in (* FIXME: by_def(proxy) + bool *) + List.iter (fun u -> add_clause [Lit.neg u; proxy] proof) subs; + add_clause (Lit.neg proxy :: subs) proof; + proxy, proof (* FIXME: by_def(proxy) + sub_p + A.proof_bool *) + | B_ite _ | B_eq _ | B_neq _ -> mk_lit t, SI.P.refl t + | B_equiv (a,b) -> equiv_ ~get_lit ~for_:t ~is_xor:false a b, SI.P.sorry (* FIXME *) + | B_xor (a,b) -> equiv_ ~get_lit ~for_:t ~is_xor:true a b, SI.P.sorry (* FIXME *) + | B_atom u -> mk_lit u, SI.P.refl u in - let lit = get_lit t in + + let lit, pr = get_lit_and_proof_ t in 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, pr) (* check if new terms were added to the congruence closure, that can be turned into clauses *) @@ -274,10 +314,10 @@ module Make(A : ARG) : S with module A = A = struct all_terms (fun t -> match cnf_of t with | None -> () - | Some u -> + | Some (u, pr_t_u) -> Log.debugf 5 - (fun k->k "(@[th-bool-static.final-check.cnf@ %a@ :yields %a@])" - T.pp t T.pp u); + (fun k->k "(@[th-bool-static.final-check.cnf@ %a@ :yields %a@ :pr %a@])" + T.pp t T.pp u SI.P.pp pr_t_u); SI.CC.merge_t cc_ t u (SI.CC.Expl.mk_list []); ()); end; diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml index 0c3d770d..9b51f10b 100644 --- a/src/th-data/Sidekick_th_data.ml +++ b/src/th-data/Sidekick_th_data.ml @@ -24,6 +24,7 @@ let name = "th-data" module type DATA_TY = sig type t type cstor + type proof val equal : t -> t -> bool @@ -73,6 +74,10 @@ module type ARG = sig val mk_eq : S.T.Term.state -> S.T.Term.t -> S.T.Term.t -> S.T.Term.t val ty_is_finite : S.T.Ty.t -> bool val ty_set_is_finite : S.T.Ty.t -> bool -> unit + + val proof_isa_split : S.T.Term.t Iter.t -> S.P.t + val proof_isa_disj : S.T.Term.t -> S.T.Term.t -> S.P.t + val proof_cstor_inj : Cstor.t -> S.T.Term.t list -> S.T.Term.t list -> S.P.t end (** Helper to compute the cardinality of types *) @@ -565,11 +570,13 @@ module Make(A : ARG) : S with module A = A = struct lit) |> Iter.to_rev_list in - SI.add_clause_permanent solver acts c; + SI.add_clause_permanent solver acts c + (A.proof_isa_split @@ (Iter.of_list c|>Iter.map SI.Lit.term)); Iter.diagonal_l c (fun (c1,c2) -> + let proof = A.proof_isa_disj (SI.Lit.term c1) (SI.Lit.term c2) in SI.add_clause_permanent solver acts - [SI.Lit.neg c1; SI.Lit.neg c2]); + [SI.Lit.neg c1; SI.Lit.neg c2] proof); ) (* on final check, check acyclicity,