From c02da6ce8a5668e7166ea15f4106ae474f18dd18 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 26 Apr 2021 22:06:58 -0400 Subject: [PATCH] feat(proof): progress on preprocessing; proper proofs for th-bool --- src/base-term/Proof.ml | 41 ++++--- src/base-term/Proof.mli | 1 + src/cc/Sidekick_cc.ml | 2 +- src/core/Sidekick_core.ml | 39 ++++-- src/lra/sidekick_arith_lra.ml | 7 +- src/msat-solver/Sidekick_msat_solver.ml | 116 +++++++++++------- src/smtlib/Process.ml | 36 +++++- src/th-bool-static/Sidekick_th_bool_static.ml | 111 ++++++++++------- 8 files changed, 235 insertions(+), 118 deletions(-) diff --git a/src/base-term/Proof.ml b/src/base-term/Proof.ml index f885a1e1..bb2228ee 100644 --- a/src/base-term/Proof.ml +++ b/src/base-term/Proof.ml @@ -11,7 +11,7 @@ type lit = | L_a of term | L_na of term -let not = function +let lit_not = function | L_eq (a,b) -> L_neq(a,b) | L_neq (a,b) -> L_eq(a,b) | L_a t -> L_na t @@ -23,11 +23,11 @@ let pp_lit out = function | L_a t -> Fmt.fprintf out "(@[+@ %a@])" T.pp t | L_na t -> Fmt.fprintf out "(@[-@ %a@])" T.pp t -let a t = L_a t -let na t = L_na t -let eq t u = L_eq (t,u) -let neq t u = L_neq (t,u) -let lit_st (t,b) = if b then a t else na t +let lit_a t = L_a t +let lit_na t = L_na t +let lit_eq t u = L_eq (t,u) +let lit_neq t u = L_neq (t,u) +let lit_st (t,b) = if b then lit_a t else lit_na t type clause = lit list @@ -48,8 +48,10 @@ type t = | Bool_true_is_true | Bool_true_neq_false | Bool_eq of term * term (* equal by pure boolean reasoning *) + | Bool_c of clause (* boolean tautology *) | Ite_true of term (* given [if a b c] returns [a=T |- if a b c=b] *) | Ite_false of term + | With_def of term list * t (* [with_def ts p] is [p] using definitions of [ts] *) | LRA of clause | Composite of { (* some named (atomic) assumptions *) @@ -63,11 +65,10 @@ and composite_step = res: clause; (* result of [proof] *) proof: t; (* sub-proof *) } + | S_define_t of term * term (* [const := t] *) - (* TODO: do we need that here? or is it only during printing - that it becomes important? - | S_define_t of string * term (* name this term *) - *) + (* TODO: step to name a term (not define it), to keep sharing? + or do we do that when we print/serialize the proof *) and hres_step = | R of { pivot: term; p: t} @@ -80,8 +81,12 @@ let r1 p = R1 p let p p ~lhs ~rhs : hres_step = P { p; lhs; rhs } let p1 p = P1 p -let defc ~name res proof : composite_step = - S_define_c {proof;name;res} +let defc ~name res proof : composite_step = S_define_c {proof;name;res} +let deft c rhs : composite_step = S_define_t (c,rhs) + +let is_trivial_refl = function + | Refl _ -> true + | _ -> false let default=Unspecified let sorry_c c = Sorry_c (Iter.to_rev_list c) @@ -96,6 +101,7 @@ let cc_imply2 h1 h2 t u : t = CC_lemma_imply ([h1; h2], t, u) let assertion t = Assertion t let assertion_c c = Assertion_c (Iter.to_rev_list c) let assertion_c_l c = Assertion_c c +let with_defs ts p = match ts with [] -> p | _ -> With_def (ts, p) let composite_l ?(assms=[]) steps : t = Composite {assumptions=assms; steps} let composite_iter ?(assms=[]) steps : t = @@ -111,6 +117,7 @@ let ite_false t = Ite_false t 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 c : t = Bool_c c let hres_l c l : t = Hres (c,l) let hres_iter c i : t = Hres (c, Iter.to_list i) @@ -142,11 +149,12 @@ module Quip = struct | Bool_true_is_true -> Fmt.string out "true-is-true" | Bool_true_neq_false -> Fmt.string out "(@[!= T F@])" | Bool_eq (a,b) -> Fmt.fprintf out "(@[bool-eq@ %a@ %a@])" T.pp a T.pp b + | Bool_c c -> Fmt.fprintf out "(@[bool-c@ %a@])" pp_cl c | Assertion t -> Fmt.fprintf out "(@[assert@ %a@])" T.pp t | Assertion_c c -> Fmt.fprintf out "(@[assert-c@ %a@])" pp_cl c | Hres (c, l) -> - Fmt.fprintf out "(@[hres@ (@[init@ %a@]) %a@])" pp_rec c + Fmt.fprintf out "(@[hres@ (@[init@ %a@])@ %a@])" pp_rec c (pp_l pp_hres_step) l | DT_isa_split (ty,l) -> Fmt.fprintf out "(@[dt.isa.split@ (@[ty %a@])@ (@[cases@ %a@])@])" @@ -158,6 +166,8 @@ module Quip = struct i Cstor.pp c (pp_l T.pp) ts Cstor.pp c (pp_l T.pp) us | Ite_true t -> Fmt.fprintf out "(@[ite-true@ %a@])" T.pp t | Ite_false t -> Fmt.fprintf out "(@[ite-false@ %a@])" T.pp t + | With_def (ts,p) -> + Fmt.fprintf out "(@[with-defs (@[%a@])@ %a@])" (pp_l T.pp) ts pp_rec p | LRA c -> Fmt.fprintf out "(@[lra@ %a@])" pp_cl c | Composite {steps; assumptions} -> let pp_ass out (n,a) = Fmt.fprintf out "(@[assuming@ (name %s) %a@])" n pp_lit a in @@ -166,7 +176,10 @@ module Quip = struct and pp_composite_step out = function | S_define_c {name;res;proof} -> - Fmt.fprintf out "(@[defc %s %a@ %a@])" name pp_cl res pp_rec proof + Fmt.fprintf out "(@[defc %s@ %a@ %a@])" name pp_cl res pp_rec proof + | S_define_t (c,rhs) -> + Fmt.fprintf out "(@[deft@ %a@ %a@])" Term.pp c Term.pp rhs + (* | S_define_t (name, t) -> Fmt.fprintf out "(@[deft %s %a@])" name Term.pp t diff --git a/src/base-term/Proof.mli b/src/base-term/Proof.mli index 565997b1..83c09c1b 100644 --- a/src/base-term/Proof.mli +++ b/src/base-term/Proof.mli @@ -9,6 +9,7 @@ val isa_disj : ty -> term -> term -> t val cstor_inj : Cstor.t -> int -> term list -> term list -> t val bool_eq : term -> term -> t +val bool_c : lit list -> t val ite_true : term -> t val ite_false : term -> t diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml index a983a0d3..50b3bbfa 100644 --- a/src/cc/Sidekick_cc.ml +++ b/src/cc/Sidekick_cc.ml @@ -661,7 +661,7 @@ module Make (A: CC_ARG) let proof = let lits = Iter.of_list lits - |> Iter.map (fun lit -> P.lit_st (Lit.signed_term lit)) + |> Iter.map (fun lit -> P.lit_not @@ P.lit_st (Lit.signed_term lit)) in P.cc_lemma lits in diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index fb4dff34..485190b9 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -170,15 +170,21 @@ module type PROOF = sig (** Proof representation of literals *) val pp_lit : lit Fmt.printer - val a : term -> lit - val na : term -> lit + val lit_a : term -> lit + val lit_na : term -> lit val lit_st : term * bool -> lit - val eq : term -> term -> lit - val neq : term -> term -> lit - val not : lit -> lit + val lit_eq : term -> term -> lit + val lit_neq : term -> term -> lit + val lit_not : lit -> lit type composite_step val defc : name:string -> lit list -> t -> composite_step + val deft : term -> term -> composite_step (** define a (new) atomic term *) + + val is_trivial_refl : t -> bool + (** is this a proof of [|- t=t]? This can be used to remove + some trivial steps that would build on the proof (e.g. rewriting + using [refl t] is useless). *) val assertion : term -> t val assertion_c : lit Iter.t -> t @@ -189,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 with_defs : term list -> t -> t (* proof under definition of given terms *) 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] *) @@ -585,8 +592,16 @@ module type SOLVER_INTERNAL = sig type lit = Lit.t + (** {3 Proof helpers} *) + + val define_const : t -> const:term -> rhs:term -> unit + (** [define_const si ~const ~rhs] adds the definition [const := rhs] + to the (future) proof. [const] should be a fresh constant that + occurs nowhere else, and [rhs] a term defined without [const]. *) + (** {3 Congruence Closure} *) + (** Congruence closure instance *) module CC : CC_S with module T = T and module P = P @@ -966,18 +981,22 @@ module type SOLVER = sig val add_theory_l : t -> theory list -> unit - val mk_atom_lit : t -> lit -> Atom.t - (** Turn a literal into a SAT solver literal. *) + val mk_atom_lit : t -> lit -> Atom.t * P.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] *) - val mk_atom_t : t -> ?sign:bool -> term -> Atom.t - (** Turn a boolean term, with a sign, into a SAT solver's literal. *) + val mk_atom_t : t -> ?sign:bool -> term -> Atom.t * P.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)] *) 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 -> P.t -> unit - (** Same as {!add_clause} but with a list of atoms. *) + (** Add a clause to the solver, given as a list. *) (** {2 Internal representation of proofs} diff --git a/src/lra/sidekick_arith_lra.ml b/src/lra/sidekick_arith_lra.ml index fcb5563b..1d69e82f 100644 --- a/src/lra/sidekick_arith_lra.ml +++ b/src/lra/sidekick_arith_lra.ml @@ -212,6 +212,7 @@ module Make(A : ARG) : S with module A = A = struct | exception Not_found -> (* new variable to represent [le_comb] *) let proxy = fresh_term self ~pre (A.ty_lra self.tst) in + (* TODO: define proxy *) self.encoded_le <- Comb_map.add le_comb proxy self.encoded_le; Log.debugf 50 (fun k->k "(@[lra.encode-le@ `%a`@ :into-var %a@])" LE_.Comb.pp le_comb T.pp proxy); @@ -269,10 +270,10 @@ 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] A.S.P.(A.proof_lra_l [na t; a u1]) ; - add_clause [SI.Lit.neg lit_t; lit_u2] A.S.P.(A.proof_lra_l [na t; a u2]); + add_clause [SI.Lit.neg lit_t; lit_u1] A.S.P.(A.proof_lra_l [lit_na t; lit_a u1]) ; + add_clause [SI.Lit.neg lit_t; lit_u2] A.S.P.(A.proof_lra_l [lit_na t; lit_a u2]); add_clause [SI.Lit.neg lit_u1; SI.Lit.neg lit_u2; lit_t] - A.S.P.(A.proof_lra_l [a t;na u1;na u2]); + A.S.P.(A.proof_lra_l [lit_a t; lit_na u1; lit_na u2]); ); None diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml index 298e0be9..e2cdb2d0 100644 --- a/src/msat-solver/Sidekick_msat_solver.ml +++ b/src/msat-solver/Sidekick_msat_solver.ml @@ -196,7 +196,8 @@ module Make(A : ARG) simp: Simplify.t; mutable preprocess: preprocess_hook list; mutable mk_model: model_hook list; - preprocess_cache: (Term.t * P.t) Term.Tbl.t; + preprocess_cache: (Term.t * P.t list) Term.Tbl.t; + mutable t_defs : (term*term) list; (* term definitions *) 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; @@ -231,6 +232,9 @@ module Make(A : ARG) let[@inline] ty_st t = t.ty_st let stats t = t.stat + let define_const (self:t) ~const ~rhs : unit = + self.t_defs <- (const,rhs) :: self.t_defs + let simplifier self = self.simp 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 @@ -262,12 +266,15 @@ module Make(A : ARG) 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 : term * proof = + (* compute and cache normal form [u] of [t]. + Also cache a list of proofs [ps] such + that [ps |- t=u] by CC. *) + let rec aux t : term * proof list = match Term.Tbl.find self.preprocess_cache t with - | up -> up + | u, ps -> + u, ps | exception Not_found -> - let sub_p = ref [] in + let sub_p: P.t list ref = ref [] in (* try rewrite at root *) let t1 = aux_rec ~sub_p t self.preprocess in @@ -276,9 +283,9 @@ module Make(A : ARG) let t2 = Term.map_shallow self.tst (fun t_sub -> - let u_sub, p_t = aux t_sub in + let u_sub, ps_t = aux t_sub in if not (Term.equal t_sub u_sub) then ( - sub_p := p_t :: !sub_p; + sub_p := List.rev_append ps_t !sub_p; ); u_sub) t1 @@ -287,9 +294,9 @@ module Make(A : ARG) let u = if not (Term.equal t t2) then ( (* fixpoint *) - let v, p_t2_v = aux t2 in + let v, ps_t2_v = aux t2 in if not (Term.equal t2 v) then ( - sub_p := p_t2_v :: !sub_p + sub_p := List.rev_append ps_t2_v !sub_p ); v ) else ( @@ -299,18 +306,12 @@ module Make(A : ARG) if t != u then ( Log.debugf 5 - (fun k->k "(@[msat-solver.preprocess.term@ \ - :from %a@ :to %a@])" Term.pp t Term.pp u); + (fun k->k "(@[msat-solver.preprocess.term@ :from %a@ :to %a@])" + Term.pp t Term.pp 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 + Term.Tbl.add self.preprocess_cache t (u,!sub_p); + u, !sub_p (* try each function in [hooks] successively *) and aux_rec ~sub_p t hooks : term = @@ -319,32 +320,41 @@ module Make(A : ARG) | h :: hooks_tl -> match h self ~mk_lit ~add_clause t with | 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 + | Some (u, ps_t_u) -> + sub_p := ps_t_u :: !sub_p; + let v, ps_u_v = aux u in if t != v then ( - sub_p := p_u_v :: !sub_p; + sub_p := List.rev_append ps_u_v !sub_p; ); v 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 - ) + let u, ps_t1_u = aux t1 in + + let pr_t_u = + if t != u then ( + let hyps = + if t == t1 then ps_t1_u + else p_t_t1 :: ps_t1_u in + P.cc_imply_l hyps t u + ) else P.refl u + in + + u, pr_t_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@ :proof %a@])" - Lit.pp lit Lit.pp lit' P.Quip.pp p); + + if not (Lit.equal lit lit') then ( + Log.debugf 10 + (fun k->k "(@[msat-solver.preprocess.lit@ :lit %a@ :into %a@ :proof %a@])" + Lit.pp lit Lit.pp lit' P.pp_debug p); + ); + lit', p (* add a clause using [acts] *) @@ -491,6 +501,7 @@ module Make(A : ARG) count_preprocess_clause = Stat.mk_int stat "solver.preprocess-clause"; count_propagate = Stat.mk_int stat "solver.th-propagations"; count_conflict = Stat.mk_int stat "solver.th-conflicts"; + t_defs=[]; on_partial_check=[]; on_final_check=[]; level=0; @@ -511,6 +522,7 @@ module Make(A : ARG) type t = { msat: Sat_solver.proof; + tdefs: (term*term) list; (* term definitions *) p: P.t lazy_t; } @@ -531,7 +543,7 @@ module Make(A : ARG) clause [c] under given assumptions (each assm is a lit), and return [-a1 \/ … \/ -an \/ c], discharging assumptions *) - let conv_proof (msat:Sat_solver.proof) : P.t = + let conv_proof (msat:Sat_solver.proof) (t_defs:_ list) : P.t = let assms = ref [] in let steps = ref [] in @@ -618,10 +630,13 @@ module Make(A : ARG) (* this should traverse from the leaves, so that order of [steps] is correct *) Sat_solver.Proof.fold tr_node_to_step () msat; let assms = !assms in - P.composite_l ~assms (List.rev !steps) - let make (msat: Sat_solver.proof) : t = - { msat; p=lazy (conv_proof msat) } + (* gather all term definitions *) + let t_defs = CCList.map (fun (c,rhs) -> P.deft c rhs) t_defs in + P.composite_l ~assms (CCList.append t_defs (List.rev !steps)) + + let make (msat: Sat_solver.proof) (tdefs: _ list) : t = + { msat; tdefs; p=lazy (conv_proof msat tdefs) } let check self = SP.check self.msat let pp out (self:t) = P.Quip.pp out (to_proof self) @@ -726,21 +741,36 @@ module Make(A : ARG) CC.set_as_lit cc (CC.add_term cc sub ) (Sat_solver.Atom.formula atom); ()) - let rec mk_atom_lit self lit : Atom.t = - let lit, _proof = preprocess_lit_ self lit in + let rec mk_atom_lit self lit : Atom.t * P.t = + let lit, proof = preprocess_lit_ self lit in add_bool_subterms_ self (Lit.term lit); - Sat_solver.make_atom self.solver lit + Sat_solver.make_atom self.solver lit, proof 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 + let pr_l = ref [] in + let atoms = + List.map + (fun lit -> + let a, pr = mk_atom_lit self lit in + if not (P.is_trivial_refl pr) then ( + pr_l := pr :: !pr_l; + ); + a) + lits + in + (* do paramodulation if needed *) + let proof = + if !pr_l=[] then proof + else P.(hres_l proof (List.rev_map p1 !pr_l)) + in Sat_solver.add_clause self.solver atoms proof) self.si lit - let[@inline] mk_atom_t self ?sign t : Atom.t = + let[@inline] mk_atom_t self ?sign t : Atom.t * P.t = let lit = Lit.atom (tst self) ?sign t in mk_atom_lit self lit @@ -896,7 +926,7 @@ module Make(A : ARG) try let pr = us.get_proof () in if check then Sat_solver.Proof.check pr; - Some (Pre_proof.make pr) + Some (Pre_proof.make pr (List.rev self.si.t_defs)) with Msat.Solver_intf.No_proof -> None ) in let unsat_core = lazy (us.Msat.unsat_assumptions ()) in diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index 485266b2..9bb054da 100644 --- a/src/smtlib/Process.ml +++ b/src/smtlib/Process.ml @@ -250,8 +250,13 @@ let process_stmt Log.debug 1 "exit"; raise Exit | Statement.Stmt_check_sat l -> + (* FIXME: how to map [l] to [assumptions] in proof? *) let assumptions = - List.map (fun (sign,t) -> Solver.mk_atom_t solver ~sign t) l + List.map + (fun (sign,t) -> + let a, _pr = Solver.mk_atom_t solver ~sign t in + a) + l in solve ?gc ?restarts ?dot_proof ~check ?pp_proof ?pp_model @@ -265,23 +270,41 @@ let process_stmt | Statement.Stmt_decl (f,ty_args,ty_ret) -> decl_fun f ty_args ty_ret; E.return () + | Statement.Stmt_assert t -> if pp_cnf then ( Format.printf "(@[assert@ %a@])@." Term.pp t ); - let atom = Solver.mk_atom_t solver t in + let atom, pr_atom = Solver.mk_atom_t solver t in CCOpt.iter (fun h -> Vec.push h [atom]) hyps; - Solver.add_clause solver (IArray.singleton atom) (Proof.assertion t); + Solver.add_clause solver (IArray.singleton atom) + Proof.(hres_l (assertion t) [p1 pr_atom]); E.return() + | Statement.Stmt_assert_clause c_ts -> if pp_cnf then ( Format.printf "(@[assert-clause@ %a@])@." (Util.pp_list Term.pp) c_ts ); - let c = List.map (Solver.mk_atom_t solver) c_ts in + let pr_l = ref [] in + let c = + List.map + (fun lit -> + let a, pr = Solver.mk_atom_t solver lit in + if not (Proof.is_trivial_refl pr) then pr_l := pr :: !pr_l; + a) + c_ts in CCOpt.iter (fun h -> Vec.push h c) hyps; - let proof = Proof.(assertion_c (Iter.of_list c_ts |> Iter.map (fun t->a t))) in + + let proof = + let open Proof in + let p = assertion_c (Iter.of_list c_ts |> Iter.map (fun t->lit_a t)) in + (* rewrite with preprocessing proofs *) + if !pr_l = [] then p else hres_l p (List.rev_map p1 !pr_l) + in + Solver.add_clause solver (IArray.of_list c) proof ; E.return() + | Statement.Stmt_data _ -> E.return() | Statement.Stmt_define _ -> @@ -333,7 +356,8 @@ module Th_bool = Sidekick_th_bool_static.Make(struct module S = Solver type term = S.T.Term.t include Form - let proof_bool = Proof.bool_eq + let proof_bool_eq = Proof.bool_eq + let proof_bool_c = Proof.bool_c let proof_ite_true = Proof.ite_true let proof_ite_false = Proof.ite_false end) diff --git a/src/th-bool-static/Sidekick_th_bool_static.ml b/src/th-bool-static/Sidekick_th_bool_static.ml index 7bf0b6a3..5809ecac 100644 --- a/src/th-bool-static/Sidekick_th_bool_static.ml +++ b/src/th-bool-static/Sidekick_th_bool_static.ml @@ -33,8 +33,11 @@ module type ARG = sig (** [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 + (** 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 : S.P.lit list -> 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. *) @@ -117,7 +120,7 @@ module Make(A : ARG) : S with module A = A = struct 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 + let ret u = Some (u, A.proof_bool_eq t u) in match A.view_as_bool t with | B_bool _ -> None | B_not u when is_true u -> ret (T.bool tst false) @@ -172,9 +175,9 @@ module Make(A : ARG) : S with module A = A = struct assert (Ty.equal ty (T.ty u)); u - let fresh_lit (self:state) ~for_ ~mk_lit ~pre : Lit.t = + 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 - mk_lit proxy + 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 = @@ -192,18 +195,26 @@ module Make(A : ARG) : S with module A = A = struct Some (c, proof) | _ -> let t_ite = fresh_term self ~for_:t ~pre:"ite" (T.ty b) in + SI.define_const si ~const:t_ite ~rhs:t; let lit_a = mk_lit a in - 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) + add_clause [Lit.neg lit_a; mk_lit (eq self.tst t_ite b)] + SI.P.(with_defs [t_ite] (A.proof_ite_true t)); + add_clause [lit_a; mk_lit (eq self.tst t_ite c)] + SI.P.(with_defs [t_ite] (A.proof_ite_false t)); + Some (t_ite, SI.P.(with_defs [t_ite] (refl t))) end | _ -> None + let[@inline] pr_lit lit = SI.P.(lit_st (Lit.signed_term lit)) + let[@inline] pr_def_refl proxy t = SI.P.(with_defs [proxy] (refl t)) + + (* prove clause [l] by boolean lemma *) + let pr_bool_c proxy l : SI.P.t = + let cl = List.rev_map pr_lit l in + SI.P.(with_defs [proxy] (A.proof_bool_c cl)) + (* TODO: polarity? *) - let cnf (self:state) (_si:SI.t) ~mk_lit ~add_clause (t:T.t) : (T.t * SI.P.t) option = + 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_abs, pr = @@ -211,7 +222,7 @@ module Make(A : ARG) : S with module A = A = struct | lit_pr -> lit_pr (* cached *) | exception Not_found -> (* compute and cache *) - let lit, pr = get_lit_uncached t_abs in + let lit, pr = get_lit_uncached si t_abs in if not (T.equal (Lit.term lit) t_abs) then ( T.Tbl.add self.cnf t_abs (lit, pr); Log.debugf 20 @@ -224,22 +235,27 @@ 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_ ~get_lit ~is_xor ~for_ a b : Lit.t = - let a = get_lit a in - let b = get_lit b in + and equiv_ si ~get_lit ~is_xor ~for_ t_a t_b : Lit.t * SI.P.t = + 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 proxy = fresh_lit ~for_ ~mk_lit ~pre:"equiv_" self in + let t_proxy, proxy = fresh_lit ~for_ ~mk_lit ~pre:"equiv_" self in + + SI.define_const si ~const:t_proxy ~rhs:for_; + let add_clause c = + add_clause c (pr_bool_c t_proxy c) + in + (* proxy => a<=> b, ¬proxy => a xor 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 + 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]; + proxy, pr_def_refl t_proxy for_ (* make a literal for [t], with a proof of [|- abs(t) = abs(lit)] *) - and get_lit_uncached t : Lit.t * SI.P.t = + and get_lit_uncached si t : Lit.t * SI.P.t = let sub_p = ref [] in let get_lit t = @@ -250,43 +266,56 @@ module Make(A : ARG) : S with module A = A = struct lit in + let add_clause_by_def_ proxy c : unit = + let pr = pr_bool_c proxy c in + add_clause c pr + 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_not u -> 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 + let t_proxy, proxy = fresh_lit ~for_:t ~mk_lit ~pre:"and_" self in + SI.define_const si ~const:t_proxy ~rhs:t; (* add clauses *) - 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 *) + List.iter + (fun u -> add_clause_by_def_ t_proxy [Lit.neg proxy; u]) + subs; + add_clause_by_def_ t_proxy (proxy :: List.map Lit.neg subs); + proxy, pr_def_refl t_proxy t + | 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 + let t_proxy, proxy = fresh_lit ~for_:t ~mk_lit ~pre:"or_" self in + SI.define_const si ~const:t_proxy ~rhs:t; (* add clauses *) - 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 *) + List.iter (fun u -> add_clause_by_def_ t_proxy [Lit.neg u; proxy]) subs; + add_clause_by_def_ t_proxy (Lit.neg proxy :: subs); + proxy, pr_def_refl t_proxy t + | 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 let u = get_lit u in let subs = u :: args in + (* now the or-encoding *) - let proxy = fresh_lit ~for_:t ~mk_lit ~pre:"implies_" self in + let t_proxy, proxy = fresh_lit ~for_:t ~mk_lit ~pre:"implies_" self in + SI.define_const si ~const:t_proxy ~rhs:t; + (* add clauses *) - 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 *) + List.iter (fun u -> add_clause_by_def_ t_proxy [Lit.neg u; proxy]) subs; + add_clause_by_def_ t_proxy (Lit.neg proxy :: subs); + proxy, pr_def_refl t_proxy t + | 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_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 in