From d40ce304ae327e0b79c6667ede1e4070a36c57a8 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 17 Aug 2021 09:29:46 -0400 Subject: [PATCH] wip: refactor proofs into traces --- src/cc/Sidekick_cc.ml | 31 ++-- src/cc/Sidekick_cc.mli | 2 +- src/core/Sidekick_core.ml | 109 +++++++----- src/msat-solver/Sidekick_msat_solver.ml | 8 +- src/th-bool-static/Sidekick_th_bool_static.ml | 157 ++++++++++-------- 5 files changed, 174 insertions(+), 133 deletions(-) diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml index de98a67f..7fc3faff 100644 --- a/src/cc/Sidekick_cc.ml +++ b/src/cc/Sidekick_cc.ml @@ -15,7 +15,7 @@ module type S = Sidekick_core.CC_S module Make (A: CC_ARG) : S with module T = A.T and module Lit = A.Lit - and type lemma = A.lemma + and type proof = A.proof and module Actions = A.Actions = struct module T = A.T @@ -26,7 +26,8 @@ module Make (A: CC_ARG) type term_store = T.Term.store type lit = Lit.t type fun_ = T.Fun.t - type lemma = A.lemma + type proof = A.proof + type dproof = proof -> unit type actions = Actions.t module Term = T.Term @@ -280,7 +281,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 * P.lemma) -> unit + and ev_on_propagate = t -> lit -> (unit -> lit list * (proof -> unit)) -> unit and ev_on_is_subterm = N.t -> term -> unit let[@inline] size_ (r:repr) = r.n_size @@ -307,10 +308,6 @@ module Make (A: CC_ARG) Invariant: [in_cc t ∧ do_cc t => forall u subterm t, in_cc u] *) let[@inline] mem (cc:t) (t:term): bool = T_tbl.mem cc.tbl t - let ret_cc_lemma _what (_lits:lit list) (p_lits:lit Iter.t) = - let p = P.lemma_cc p_lits in - p - (* print full state *) let pp_full out (cc:t) : unit = let pp_next out n = @@ -661,10 +658,10 @@ module Make (A: CC_ARG) let lits = explain_decompose_expl cc ~th [] e_ab in let lits = explain_equal cc ~th lits a ra in let lits = explain_equal cc ~th lits b rb in - let proof = + let emit_proof p = let p_lits = Iter.of_list lits |> Iter.map Lit.neg in - ret_cc_lemma "true-eq-false" lits p_lits in - raise_conflict_ cc ~th:!th acts (List.rev_map Lit.neg lits) proof + P.lemma_cc p p_lits in + raise_conflict_ cc ~th:!th acts (List.rev_map Lit.neg lits) emit_proof ); (* We will merge [r_from] into [r_into]. we try to ensure that [size ra <= size rb] in general, but always @@ -779,12 +776,12 @@ module Make (A: CC_ARG) let e = lazy ( let lazy (th, acc) = half_expl in let lits = explain_equal cc ~th acc u1 t1 in - let p_lits = + let emit_proof p = (* make a tautology, not a true guard *) - Iter.cons lit (Iter.of_list lits |> Iter.map Lit.neg) + let p_lits = Iter.cons lit (Iter.of_list lits |> Iter.map Lit.neg) in + P.lemma_cc p p_lits in - let p = ret_cc_lemma "bool-parent" lits p_lits in - lits, p + lits, emit_proof ) in fun () -> Lazy.force e in @@ -851,11 +848,11 @@ module Make (A: CC_ARG) let th = ref true in let lits = explain_decompose_expl cc ~th [] expl in let lits = List.rev_map Lit.neg lits in - let proof = + let emit_proof p = let p_lits = Iter.of_list lits in - ret_cc_lemma "from-expl" lits p_lits + P.lemma_cc p p_lits in - raise_conflict_ cc ~th:!th acts lits proof + raise_conflict_ cc ~th:!th acts lits emit_proof let merge cc n1 n2 expl = Log.debugf 5 diff --git a/src/cc/Sidekick_cc.mli b/src/cc/Sidekick_cc.mli index 21566fc7..8e9cdb95 100644 --- a/src/cc/Sidekick_cc.mli +++ b/src/cc/Sidekick_cc.mli @@ -6,5 +6,5 @@ module type S = Sidekick_core.CC_S module Make (A: CC_ARG) : S with module T = A.T and module Lit = A.Lit - and type lemma = A.lemma + and type proof = A.proof and module Actions = A.Actions diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index 69fc3256..8a7a5eb0 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -147,15 +147,14 @@ end (** Proofs for the congruence closure *) module type CC_PROOF = sig + type t type lit - type lemma - val lemma_cc : lit Iter.t -> lemma + val lemma_cc : t -> lit Iter.t -> unit + (** [lemma_cc proof lits] asserts that [lits] form a tautology for the theory + of uninterpreted functions. *) end -(* TODO: use same proofs as Sidekick_sat? - - but give more precise type to [lemma]? *) (** Proofs of unsatisfiability. We use DRUP(T)-style traces where we simply emit clauses as we go, @@ -167,15 +166,33 @@ module type PROOF = sig a clause to be {b valid} (true in every possible interpretation of the problem's assertions, and the theories) *) - type lemma - + type term type lit include CC_PROOF - with type lemma := lemma + with type t := t and type lit := lit + val begin_subproof : t -> unit + (** Begins a subproof. The result of this will only be the + clause with which {!end_subproof} is called; all other intermediate + steps will be discarded. *) + + val end_subproof : t -> lit Iter.t -> unit + (** [end_subproof p lits] ends the current active subproof, which {b must} + prove the clause [lits] by RUP. *) + + val define_term : t -> term -> term -> unit + (** [define_term p cst u] defines the new constant [cst] as being equal + to [u]. *) + + val lemma_preprocess : t -> term -> term -> unit + (** [lemma_preprocess p t u] asserts that [t = u] is a tautology + and that [t] has been preprocessed into [u]. + From now on, [t] and [u] will be used interchangeably. *) + val enabled : t -> bool + (** Is proof production enabled? *) end (** Literals @@ -222,21 +239,22 @@ module type CC_ACTIONS = sig module T : TERM module Lit : LIT with module T = T - type lemma - module P : CC_PROOF with type lit = Lit.t and type lemma = lemma + type proof + type dproof = proof -> unit + module P : CC_PROOF with type lit = Lit.t and type t = proof type t (** An action handle. It is used by the congruence closure to perform the actions below. How it performs the actions is not specified and is solver-specific. *) - val raise_conflict : t -> Lit.t list -> lemma -> 'a + val raise_conflict : t -> Lit.t list -> dproof -> 'a (** [raise_conflict acts c pr] declares that [c] is a tautology of the theory of congruence. This does not return (it should raise an exception). @param pr the proof of [c] being a tautology *) - val propagate : t -> Lit.t -> reason:(unit -> Lit.t list * lemma) -> unit + val propagate : t -> Lit.t -> reason:(unit -> Lit.t list * dproof) -> unit (** [propagate acts lit ~reason pr] declares that [reason() => lit] is a tautology. @@ -251,12 +269,12 @@ end module type CC_ARG = sig module T : TERM module Lit : LIT with module T = T - type lemma - module P : CC_PROOF with type lit = Lit.t and type lemma = lemma + type proof + module P : CC_PROOF with type lit = Lit.t and type t = proof module Actions : CC_ACTIONS with module T=T and module Lit = Lit - and type lemma = lemma + and type proof = proof val cc_view : T.Term.t -> (T.Fun.t, T.Term.t, T.Term.t Iter.t) CC_view.t (** View the term through the lens of the congruence closure *) @@ -283,12 +301,13 @@ module type CC_S = sig module T : TERM module Lit : LIT with module T = T - type lemma - module P : CC_PROOF with type lit = Lit.t and type lemma = lemma + type proof + type dproof = proof -> unit + module P : CC_PROOF with type lit = Lit.t and type t = proof module Actions : CC_ACTIONS with module T = T and module Lit = Lit - and type lemma = lemma + and type proof = proof type term_store = T.Term.store type term = T.Term.t type fun_ = T.Fun.t @@ -429,7 +448,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 * P.lemma) -> unit + type ev_on_propagate = t -> lit -> (unit -> lit list * dproof) -> unit (** [ev_on_propagate cc lit reason] is called whenever [reason() => lit] is a propagated lemma. See {!CC_ACTIONS.propagate}. *) @@ -580,6 +599,9 @@ module type SOLVER_INTERNAL = sig type term = T.Term.t type term_store = T.Term.store type ty_store = T.Ty.store + type proof + type dproof = proof -> unit + (** Delayed proof. This is used to build a proof step on demand. *) (** {3 Literals} @@ -589,9 +611,7 @@ module type SOLVER_INTERNAL = sig module Lit : LIT with module T = T (** {3 Proofs} *) - type lemma - module P : PROOF with type lit = Lit.t and type lemma = lemma - type proof = P.t + module P : PROOF with type lit = Lit.t and type term = term and type t = proof (** {3 Main type for a solver} *) type t @@ -621,8 +641,8 @@ module type SOLVER_INTERNAL = sig module CC : CC_S with module T = T and module Lit = Lit - and type lemma = lemma - and type P.lemma = lemma + and type proof = proof + and type P.t = proof and type P.lit = lit and type Actions.t = actions @@ -641,19 +661,19 @@ module type SOLVER_INTERNAL = sig val clear : t -> unit (** Reset internal cache, etc. *) - type hook = t -> term -> (term * proof) option + type hook = t -> term -> (term * dproof) 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], and if [t] is [app "+" (const x) (const y)] where [x] and [y] are number, returns [Some (const (x+y))], and [None] otherwise. *) - val normalize : t -> term -> (term * P.t) option + val normalize : t -> term -> (term * dproof) option (** 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 + val normalize_t : t -> term -> term * dproof (** Normalize a term using all the hooks, along with a proof that the simplification is correct. returns [t, refl t] if no simplification occurred. *) @@ -666,18 +686,18 @@ module type SOLVER_INTERNAL = sig val simplifier : t -> Simplify.t - val simplify_t : t -> term -> (term * proof) option + val simplify_t : t -> term -> (term * dproof) option (** Simplify input term, returns [Some (u, |- t=u)] if some simplification occurred. *) - val simp_t : t -> term -> term * proof + val simp_t : t -> term -> term * dproof (** [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 raise_conflict : t -> actions -> lit list -> proof -> 'a + val raise_conflict : t -> actions -> lit list -> dproof -> 'a (** Give a conflict clause to the solver *) val push_decision : t -> actions -> lit -> unit @@ -686,19 +706,19 @@ module type SOLVER_INTERNAL = sig If the SAT solver backtracks, this (potential) decision is removed and forgotten. *) - val propagate: t -> actions -> lit -> reason:(unit -> lit list * proof) -> unit + val propagate: t -> actions -> lit -> reason:(unit -> lit list * dproof) -> 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 -> proof -> unit + val propagate_l: t -> actions -> lit -> lit list -> dproof -> 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 -> proof -> unit + val add_clause_temp : t -> actions -> lit list -> dproof -> 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 -> proof -> unit + val add_clause_permanent : t -> actions -> lit list -> dproof -> unit (** Add toplevel clause to the SAT solver. This clause will not be backtracked. *) @@ -706,7 +726,7 @@ module type SOLVER_INTERNAL = sig (** Create a literal. This automatically preprocesses the term. *) val preprocess_term : - t -> add_clause:(Lit.t list -> proof -> unit) -> term -> term * proof + t -> add_clause:(Lit.t list -> proof -> unit) -> term -> term * dproof (** Preprocess a term. *) val add_lit : t -> actions -> lit -> unit @@ -762,7 +782,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 * proof) -> unit) -> unit + val on_cc_propagate : t -> (CC.t -> lit -> (unit -> lit list * dproof) -> unit) -> unit (** Callback called on every CC propagation *) val on_partial_check : t -> (t -> actions -> lit Iter.t -> unit) -> unit @@ -789,8 +809,8 @@ module type SOLVER_INTERNAL = sig type preprocess_hook = t -> mk_lit:(term -> lit) -> - add_clause:(lit list -> proof -> unit) -> - term -> (term * proof) option + add_clause:(lit list -> dproof -> unit) -> + term -> (term * dproof) 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. @@ -833,14 +853,14 @@ end module type SOLVER = sig module T : TERM module Lit : LIT with module T = T - type lemma - module P : PROOF with type lit = Lit.t and type lemma = lemma + type proof + module P : PROOF with type lit = Lit.t and type t = proof and type term = T.Term.t module Solver_internal : SOLVER_INTERNAL with module T = T and module Lit = Lit - and type lemma = lemma + and type proof = proof and module P = P (** Internal solver, available to theories. *) @@ -851,7 +871,8 @@ module type SOLVER = sig type term = T.Term.t type ty = T.Ty.t type lit = Lit.t - type proof = P.t + type dproof = proof -> unit + (** Delayed proof. This is used to build a proof step on demand. *) (** {3 A theory} @@ -997,7 +1018,7 @@ module type SOLVER = sig val add_theory_l : t -> theory list -> unit - val mk_atom_lit : t -> lit -> Atom.t * P.t + val mk_atom_lit : t -> lit -> Atom.t (** [mk_atom_lit _ lit] returns [atom, pr] where [atom] is an internal atom for the solver, and [pr] is a proof of [|- lit = atom] *) @@ -1005,7 +1026,7 @@ module type SOLVER = sig val mk_atom_lit' : t -> lit -> Atom.t (** Like {!mk_atom_t} but skips the proof *) - val mk_atom_t : t -> ?sign:bool -> term -> Atom.t * P.t + val mk_atom_t : t -> ?sign:bool -> term -> Atom.t (** [mk_atom_t _ ~sign t] returns [atom, pr] where [atom] is an internal representation of [± t], and [pr] is a proof of [|- atom = (± t)] *) diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml index 0f64c96e..59d5a653 100644 --- a/src/msat-solver/Sidekick_msat_solver.ml +++ b/src/msat-solver/Sidekick_msat_solver.ml @@ -11,7 +11,8 @@ module type ARG = sig open Sidekick_core module T : TERM - module P : PROOF with type term = T.Term.t + type proof + module P : PROOF with type term = T.Term.t and type t = proof val cc_view : T.Term.t -> (T.Fun.t, T.Term.t, T.Term.t Iter.t) CC_view.t @@ -26,6 +27,7 @@ module type S = Sidekick_core.SOLVER module Make(A : ARG) : S with module T = A.T + and type proof = A.proof and module P = A.P = struct module T = A.T @@ -81,6 +83,7 @@ module Make(A : ARG) module T = T module P = P module Lit = Lit_ + type nonrec proof = proof let cc_view = A.cc_view module Actions = struct @@ -516,6 +519,8 @@ module Make(A : ARG) (** the parametrized SAT Solver *) module Sat_solver = Sidekick_sat.Make_cdcl_t(Solver_internal) + (* TODO: move somewhere else? where it can be used to implement the new + proof module? module Pre_proof = struct module SP = Sat_solver.Proof module SC = Sat_solver.Clause @@ -643,6 +648,7 @@ module Make(A : ARG) let pp_debug out self = P.pp_debug ~sharing:false out (to_proof self) let output oc (self:t) = P.Quip.output oc (to_proof self) end + *) (* main solver state *) type t = { diff --git a/src/th-bool-static/Sidekick_th_bool_static.ml b/src/th-bool-static/Sidekick_th_bool_static.ml index a5bcf600..9989a000 100644 --- a/src/th-bool-static/Sidekick_th_bool_static.ml +++ b/src/th-bool-static/Sidekick_th_bool_static.ml @@ -27,18 +27,6 @@ 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 - - (** Basic boolean logic for [|- a=b] *) - val proof_bool_eq : S.T.Term.t -> S.T.Term.t -> S.P.t - - (** Basic boolean logic for a clause [|- c] *) - val proof_bool_c : string -> term list -> S.P.t - val mk_bool : S.T.Term.store -> (term, term IArray.t) bool_view -> term (** Make a term from the given boolean view. *) @@ -48,6 +36,22 @@ module type ARG = sig Only enable if some theories are susceptible to create boolean formulas during the proof search. *) + val lemma_bool_tauto : S.P.t -> S.Lit.t Iter.t -> unit + (** Boolean tautology lemma (clause) *) + + val lemma_bool_c : S.P.t -> string -> term list -> unit + (** Basic boolean logic lemma for a clause [|- c]. + [proof_bool_c b name cs] is the rule designated by [name]. *) + + val lemma_bool_equiv : S.P.t -> term -> term -> unit + (** Boolean tautology lemma (equivalence) *) + + val lemma_ite_true : S.P.t -> a:term -> ite:term -> unit + (** lemma [a => ite a b c = b] *) + + val lemma_ite_false : S.P.t -> a:term -> ite:term -> unit + (** lemma [¬a => ite a b c = c] *) + (** Fresh symbol generator. The theory needs to be able to create new terms with fresh names, @@ -98,7 +102,7 @@ module Make(A : ARG) : S with module A = A = struct type state = { tst: T.store; ty_st: Ty.store; - cnf: (Lit.t * SI.P.t) T.Tbl.t; (* tseitin CNF *) + cnf: (Lit.t * SI.dproof) T.Tbl.t; (* tseitin CNF *) gensym: A.Gensym.t; } @@ -114,9 +118,15 @@ 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 * SI.P.t) option = + let simplify (self:state) (simp:SI.Simplify.t) (t:T.t) : (T.t * SI.dproof) option = let tst = self.tst in - let ret u = Some (u, A.proof_bool_eq t u) in + let ret u = + let emit_proof p = + A.lemma_bool_equiv p t u; + A.S.P.lemma_preprocess p t u; + in + Some (u, emit_proof) + in match A.view_as_bool t with | B_bool _ -> None | B_not u when is_true u -> ret (T.bool tst false) @@ -141,11 +151,11 @@ module Make(A : ARG) : S with module A = A = struct let a, pr_a = SI.Simplify.normalize_t simp a in begin match A.view_as_bool a with | B_bool true -> - let pr = SI.P.(hres_l (A.proof_ite_true t) [r1 pr_a]) in - Some (b, pr) + let emit_proof p = pr_a p; A.lemma_ite_true p ~a ~ite:t in + Some (b, emit_proof) | B_bool false -> - let pr = SI.P.(hres_l (A.proof_ite_false t) [r1 pr_a]) in - Some (c, pr) + let emit_proof p = pr_a p; A.lemma_ite_false p ~a ~ite:t in + Some (c, emit_proof) | _ -> None end @@ -163,49 +173,47 @@ module Make(A : ARG) : S with module A = A = struct | B_eq _ | B_neq _ -> None | B_atom _ -> None - let fresh_term self ~for_ ~pre ty = + let fresh_term self ~for_t ~pre ty = let u = A.Gensym.fresh_term self.gensym ~pre ty in Log.debugf 20 (fun k->k "(@[sidekick.bool.proxy@ :t %a@ :for %a@])" - T.pp u T.pp for_); + T.pp u T.pp for_t); assert (Ty.equal ty (T.ty u)); u - let fresh_lit (self:state) ~for_ ~mk_lit ~pre : T.t * Lit.t = - let proxy = fresh_term ~for_ ~pre self (Ty.bool self.ty_st) in + let fresh_lit (self:state) ~for_t ~mk_lit ~pre : T.t * Lit.t = + let proxy = fresh_term ~for_t ~pre self (Ty.bool self.ty_st) in proxy, mk_lit proxy (* preprocess "ite" away *) - let preproc_ite self si ~mk_lit ~add_clause (t:T.t) : (T.t * SI.P.t) option = + let preproc_ite self si ~mk_lit ~add_clause (t:T.t) : (T.t * SI.dproof) option = match A.view_as_bool t with | B_ite (a,b,c) -> let a, pr_a = SI.simp_t si a in begin match A.view_as_bool a with | 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) + let emit_proof p = pr_a p; A.lemma_ite_true p ~a ~ite:t in + Some (b, emit_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 emit_proof p = pr_a p; A.lemma_ite_false p ~a ~ite:t in + Some (c, emit_proof) | _ -> - let t_ite = fresh_term self ~for_:t ~pre:"ite" (T.ty b) in + 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 lit_a = mk_lit a in add_clause [Lit.neg lit_a; mk_lit (eq self.tst t_ite b)] - (A.proof_ite_true t); + (fun p -> A.lemma_ite_true p ~a ~ite:t); add_clause [lit_a; mk_lit (eq self.tst t_ite c)] - (A.proof_ite_false t); - Some (t_ite, SI.P.(refl t)) + (fun p -> A.lemma_ite_false p ~a ~ite:t); + Some (t_ite, fun p -> SI.P.define_term p t_ite t) end | _ -> None - let[@inline] pr_def_refl _proxy t = SI.P.(refl t) - (* TODO: polarity? *) - 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 cnf (self:state) (si:SI.t) ~mk_lit ~add_clause (t:T.t) : (T.t * SI.dproof) option = + let rec get_lit_and_proof_ (t:T.t) : Lit.t * _ = let t_abs, t_sign = T.abs self.tst t in let lit_abs, pr = match T.Tbl.find self.cnf t_abs with @@ -225,13 +233,13 @@ module Make(A : ARG) : S with module A = A = struct let lit = if t_sign then lit_abs else Lit.neg lit_abs in lit, pr - and equiv_ si ~get_lit ~is_xor ~for_ t_a t_b : Lit.t * SI.P.t = + and equiv_ si ~get_lit ~is_xor ~for_t t_a t_b : Lit.t * SI.dproof = let a = get_lit t_a in let b = get_lit 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_ ~mk_lit ~pre:"equiv_" self in + let t_proxy, proxy = fresh_lit ~for_t ~mk_lit ~pre:"equiv_" self in - SI.define_const si ~const:t_proxy ~rhs:for_; + SI.define_const si ~const:t_proxy ~rhs:for_t; let add_clause c pr = add_clause c pr in @@ -239,21 +247,24 @@ module Make(A : ARG) : S with module A = A = struct (* proxy => a<=> b, ¬proxy => a xor b *) add_clause [Lit.neg proxy; Lit.neg a; b] - (if is_xor then A.proof_bool_c "xor-e+" [t_proxy] - else A.proof_bool_c "eq-e" [t_proxy; t_a]); + (fun p -> + if is_xor then A.lemma_bool_c p "xor-e+" [t_proxy] + else A.lemma_bool_c p "eq-e" [t_proxy; t_a]); add_clause [Lit.neg proxy; Lit.neg b; a] - (if is_xor then A.proof_bool_c "xor-e-" [t_proxy] - else A.proof_bool_c "eq-e" [t_proxy; t_b]); + (fun p -> + if is_xor then A.lemma_bool_c p "xor-e-" [t_proxy] + else A.lemma_bool_c p "eq-e" [t_proxy; t_b]); add_clause [proxy; a; b] - (if is_xor then A.proof_bool_c "xor-i" [t_proxy; t_a] - else A.proof_bool_c "eq-i+" [t_proxy]); + (fun p -> if is_xor then A.lemma_bool_c p "xor-i" [t_proxy; t_a] + else A.lemma_bool_c p "eq-i+" [t_proxy]); add_clause [proxy; Lit.neg a; Lit.neg b] - (if is_xor then A.proof_bool_c "xor-i" [t_proxy; t_b] - else A.proof_bool_c "eq-i-" [t_proxy]); - proxy, pr_def_refl t_proxy for_ + (fun p -> + if is_xor then A.lemma_bool_c p "xor-i" [t_proxy; t_b] + else A.lemma_bool_c p "eq-i-" [t_proxy]); + proxy, (fun p->SI.P.define_term p t_proxy for_t) (* make a literal for [t], with a proof of [|- abs(t) = abs(lit)] *) - and get_lit_uncached si t : Lit.t * SI.P.t = + and get_lit_uncached si t : Lit.t * SI.dproof = let sub_p = ref [] in let get_lit t = @@ -265,8 +276,8 @@ module Make(A : ARG) : S with module A = A = struct in match A.view_as_bool t with - | 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_bool b -> mk_lit (T.bool self.tst b), (fun _->()) + | B_opaque_bool t -> mk_lit t, (fun _->()) | B_not u -> let lit, pr = get_lit_and_proof_ u in Lit.neg lit, pr @@ -274,33 +285,37 @@ 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 get_lit t_subs in - let t_proxy, proxy = fresh_lit ~for_:t ~mk_lit ~pre:"and_" self in + let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit ~pre:"and_" self in SI.define_const si ~const:t_proxy ~rhs:t; (* add clauses *) List.iter2 (fun t_u u -> add_clause [Lit.neg proxy; u] - (A.proof_bool_c "and-e" [t_proxy; t_u])) + (fun p -> A.lemma_bool_c p "and-e" [t_proxy; t_u])) t_subs subs; add_clause (proxy :: List.map Lit.neg subs) - (A.proof_bool_c "and-i" [t_proxy]); - proxy, pr_def_refl t_proxy t + (fun p -> A.lemma_bool_c p "and-i" [t_proxy]); + let emit_proof p = + SI.P.define_term p t_proxy t; + in + proxy, emit_proof | B_or l -> let t_subs = Iter.to_list l in let subs = List.map get_lit t_subs in - let t_proxy, proxy = fresh_lit ~for_:t ~mk_lit ~pre:"or_" self in + let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit ~pre:"or_" self in SI.define_const si ~const:t_proxy ~rhs:t; (* add clauses *) List.iter2 (fun t_u u -> add_clause [Lit.neg u; proxy] - (A.proof_bool_c "or-i" [t_proxy; t_u])) + (fun p -> A.lemma_bool_c p "or-i" [t_proxy; t_u])) t_subs subs; add_clause (Lit.neg proxy :: subs) - (A.proof_bool_c "or-e" [t_proxy]); - proxy, pr_def_refl t_proxy t + (fun p -> A.lemma_bool_c p "or-e" [t_proxy]); + let emit_proof p = SI.P.define_term p t_proxy t in + proxy, emit_proof | B_imply (t_args, t_u) -> (* transform into [¬args \/ u] on the fly *) @@ -310,23 +325,24 @@ module Make(A : ARG) : S with module A = A = struct let subs = u :: args in (* now the or-encoding *) - let t_proxy, proxy = fresh_lit ~for_:t ~mk_lit ~pre:"implies_" self in + let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit ~pre:"implies_" self in SI.define_const si ~const:t_proxy ~rhs:t; (* add clauses *) List.iter2 (fun t_u u -> add_clause [Lit.neg u; proxy] - (A.proof_bool_c "imp-i" [t_proxy; t_u])) + (fun p -> A.lemma_bool_c p "imp-i" [t_proxy; t_u])) (t_u::t_args) subs; add_clause (Lit.neg proxy :: subs) - (A.proof_bool_c "imp-e" [t_proxy]); - proxy, pr_def_refl t_proxy t + (fun p -> A.lemma_bool_c p "imp-e" [t_proxy]); + let emit_proof p = SI.P.define_term p t_proxy t in + proxy, emit_proof - | B_ite _ | B_eq _ | B_neq _ -> mk_lit t, SI.P.refl t - | B_equiv (a,b) -> equiv_ si ~get_lit ~for_:t ~is_xor:false a b - | B_xor (a,b) -> equiv_ si ~get_lit ~for_:t ~is_xor:true a b - | B_atom u -> mk_lit u, SI.P.refl u + | B_ite _ | B_eq _ | B_neq _ -> mk_lit t, (fun _ ->()) + | B_equiv (a,b) -> equiv_ si ~get_lit ~for_t:t ~is_xor:false a b + | B_xor (a,b) -> equiv_ si ~get_lit ~for_t:t ~is_xor:true a b + | B_atom u -> mk_lit u, (fun _->()) in let lit, pr = get_lit_and_proof_ t in @@ -353,10 +369,11 @@ module Make(A : ARG) : S with module A = A = struct all_terms (fun t -> match cnf_of t with | None -> () - | Some (u, pr_t_u) -> + | Some (u, _pr_t_u) -> + (* FIXME: what to do with pr_t_u? emit it? *) Log.debugf 5 - (fun k->k "(@[th-bool-static.final-check.cnf@ %a@ :yields %a@ :pr %a@])" - T.pp t T.pp u (SI.P.pp_debug ~sharing:false) pr_t_u); + (fun k->k "(@[th-bool-static.final-check.cnf@ %a@ :yields %a@])" + T.pp t T.pp u); SI.CC.merge_t cc_ t u (SI.CC.Expl.mk_list []); ()); end;