From ef3fa2b7a74e86071bfd08e161256c72e97e1021 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 9 Jun 2021 20:46:23 -0400 Subject: [PATCH] use newer quip format, with bool-c taking terms --- src/base-term/Proof.ml | 52 +++++++------ src/base-term/Proof.mli | 2 +- src/cc/Sidekick_cc.ml | 12 ++- src/core/Sidekick_core.ml | 2 +- src/lra/sidekick_arith_lra.ml | 4 +- src/msat-solver/Sidekick_msat_solver.ml | 2 +- src/th-bool-static/Sidekick_th_bool_static.ml | 76 +++++++++++-------- 7 files changed, 87 insertions(+), 63 deletions(-) diff --git a/src/base-term/Proof.ml b/src/base-term/Proof.ml index 5e0e3776..cc2a9e56 100644 --- a/src/base-term/Proof.ml +++ b/src/base-term/Proof.ml @@ -6,29 +6,25 @@ type term = T.t type ty = Ty.t type lit = - | L_eq of term * term - | L_neq of term * term - | L_a of term - | L_na of term + | L_eq of bool * term * term + | L_a of bool * term 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 - | L_na t -> L_a t + | L_eq (sign,a,b) -> L_eq(not sign,a,b) + | L_a (sign,t) -> L_a (not sign,t) -let pp_lit_with ~pp_t out = function - | L_eq (t,u) -> Fmt.fprintf out "(@[+@ (@[=@ %a@ %a@])@])" pp_t t pp_t u - | L_neq (t,u) -> Fmt.fprintf out "(@[-@ (@[=@ %a@ %a@])@])" pp_t t pp_t u - | L_a t -> Fmt.fprintf out "(@[+@ %a@])" pp_t t - | L_na t -> Fmt.fprintf out "(@[-@ %a@])" pp_t t +let pp_lit_with ~pp_t out = + let strsign = function true -> "+" | false -> "-" in + function + | L_eq (b,t,u) -> Fmt.fprintf out "(@[%s@ (@[=@ %a@ %a@])@])" (strsign b) pp_t t pp_t u + | L_a (b,t) -> Fmt.fprintf out "(@[%s@ %a@])" (strsign b) pp_t t let pp_lit = pp_lit_with ~pp_t:Term.pp -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 +let lit_a t = L_a (true,t) +let lit_na t = L_a (false,t) +let lit_eq t u = L_eq (true,t,u) +let lit_neq t u = L_eq (false,t,u) +let lit_mk b t = L_a (b,t) type clause = lit list @@ -49,7 +45,7 @@ type t = | Bool_true_is_true | Bool_true_neq_false | Bool_eq of term * term (* equal by pure boolean reasoning *) - | Bool_c of bool_c_name * clause (* boolean tautology *) + | Bool_c of bool_c_name * term list (* boolean tautology *) | Ite_true of term (* given [if a b c] returns [a=T |- if a b c=b] *) | Ite_false of term | LRA of clause @@ -135,15 +131,17 @@ let true_neq_false : t = Bool_true_neq_false let bool_eq a b : t = Bool_eq (a,b) let bool_c name c : t = Bool_c (name, c) -let hres_l c l : t = Hres (c,l) -let hres_iter c i : t = Hres (c, Iter.to_list i) +let hres_l p l : t = + let l = List.filter (function (P1 (Refl _)) -> false | _ -> true) l in + if l=[] then p else Hres (p,l) +let hres_iter c i : t = hres_l c (Iter.to_list i) let lra_l c : t = LRA c let lra c = LRA (Iter.to_rev_list c) let iter_lit ~f_t = function - | L_eq (a,b) | L_neq (a,b) -> f_t a; f_t b - | L_a t | L_na t -> f_t t + | L_eq (_,a,b) -> f_t a; f_t b + | L_a (_,t) -> f_t t let iter_p (p:t) ~f_t ~f_step ~f_clause ~f_p : unit = match p with @@ -168,7 +166,7 @@ let iter_p (p:t) ~f_t ~f_step ~f_clause ~f_p : unit = | DT_cstor_inj (_, _c, ts, us) -> List.iter f_t ts; List.iter f_t us | Bool_true_is_true | Bool_true_neq_false -> () | Bool_eq (t, u) -> f_t t; f_t u - | Bool_c (_,c) -> f_clause c + | Bool_c (_, ts) -> List.iter f_t ts | Ite_true t | Ite_false t -> f_t t | LRA c -> f_clause c | Composite { assumptions; steps } -> @@ -295,6 +293,9 @@ module Quip = struct TODO: make sure we print terms properly *) + (* TODO: print into a buffer, without Format (should be faster) *) + (* TODO: print as C-sexp *) + let pp_l ppx out l = Fmt.(list ~sep:(return "@ ") ppx) out l let pp_a ppx out l = Fmt.(array ~sep:(return "@ ") ppx) out l let pp_cl ~pp_t out c = Fmt.fprintf out "(@[cl@ %a@])" (pp_l (pp_lit_with ~pp_t)) c @@ -319,7 +320,8 @@ module Quip = struct | Bool_eq (a,b) -> Fmt.fprintf out "(@[bool-eq@ %a@ %a@])" pp_t a pp_t b - | Bool_c (name,c) -> Fmt.fprintf out "(@[bool-c %s@ %a@])" name pp_cl c + | Bool_c (name,ts) -> + Fmt.fprintf out "(@[bool-c %s@ %a@])" name (pp_l pp_t) ts | Assertion t -> Fmt.fprintf out "(@[assert@ %a@])" pp_t t | Assertion_c c -> Fmt.fprintf out "(@[assert-c@ %a@])" pp_cl c diff --git a/src/base-term/Proof.mli b/src/base-term/Proof.mli index 6a0df914..347bc339 100644 --- a/src/base-term/Proof.mli +++ b/src/base-term/Proof.mli @@ -9,7 +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 : string -> lit list -> t +val bool_c : string -> term 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 50b3bbfa..2135192d 100644 --- a/src/cc/Sidekick_cc.ml +++ b/src/cc/Sidekick_cc.ml @@ -661,7 +661,9 @@ module Make (A: CC_ARG) let proof = let lits = Iter.of_list lits - |> Iter.map (fun lit -> P.lit_not @@ P.lit_st (Lit.signed_term lit)) + |> Iter.map (fun lit -> + let t, sign = Lit.signed_term lit in + P.lit_mk (not sign) t) in P.cc_lemma lits in @@ -783,7 +785,9 @@ module Make (A: CC_ARG) let p = A.P.cc_lemma (Iter.of_list lits - |> Iter.map (fun l -> A.P.(lit_st (Lit.signed_term l)))) + |> Iter.map (fun lit -> + let t, sign = Lit.signed_term lit in + A.P.(lit_mk sign t))) in lits, p ) in @@ -855,7 +859,9 @@ 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 -> + let t, sign = Lit.signed_term lit in + P.lit_mk sign t) in P.cc_lemma lits in diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index 96cea297..837536cd 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -172,7 +172,7 @@ module type PROOF = sig val pp_lit : lit Fmt.printer val lit_a : term -> lit val lit_na : term -> lit - val lit_st : term * bool -> lit + val lit_mk : bool -> term -> lit val lit_eq : term -> term -> lit val lit_neq : term -> term -> lit val lit_not : lit -> lit diff --git a/src/lra/sidekick_arith_lra.ml b/src/lra/sidekick_arith_lra.ml index 1d69e82f..be1b9de5 100644 --- a/src/lra/sidekick_arith_lra.ml +++ b/src/lra/sidekick_arith_lra.ml @@ -416,7 +416,9 @@ module Make(A : ARG) : S with module A = A = struct module Q_map = CCMap.Make(Q) - let plit_of_lit lit = A.S.P.lit_st (Lit.signed_term lit) + let plit_of_lit lit = + let t, sign = Lit.signed_term lit in + A.S.P.lit_mk sign t (* raise conflict from certificate *) let fail_with_cert si acts cert : 'a = diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml index 4df166dd..a2e086f5 100644 --- a/src/msat-solver/Sidekick_msat_solver.ml +++ b/src/msat-solver/Sidekick_msat_solver.ml @@ -576,7 +576,7 @@ module Make(A : ARG) let tr_atom a : P.lit = let sign = Sat_solver.Atom.sign a in let t = Lit.term (Sat_solver.Atom.formula a) in - P.lit_st (t,sign) + P.lit_mk sign t in let concl = List.rev_map tr_atom @@ Sat_solver.Clause.atoms_l c in diff --git a/src/th-bool-static/Sidekick_th_bool_static.ml b/src/th-bool-static/Sidekick_th_bool_static.ml index c842f761..7089f0f7 100644 --- a/src/th-bool-static/Sidekick_th_bool_static.ml +++ b/src/th-bool-static/Sidekick_th_bool_static.ml @@ -37,7 +37,7 @@ module type ARG = sig 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 -> S.P.lit list -> S.P.t + val proof_bool_c : string -> term 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. *) @@ -205,14 +205,8 @@ module Make(A : ARG) : S with module A = A = struct end | _ -> None - let[@inline] pr_lit lit = SI.P.(lit_st (Lit.signed_term lit)) let[@inline] pr_def_refl _proxy t = SI.P.(refl t) - (* prove clause [l] by boolean lemma *) - let pr_bool_c name _proxy l : SI.P.t = - let cl = List.rev_map pr_lit l in - (A.proof_bool_c name cl) - (* 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 = @@ -242,16 +236,24 @@ module Make(A : ARG) : S with module A = A = struct 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 ~elim c = - add_clause c (pr_bool_c (if elim then "eq-e" else "eq-i") t_proxy c) + let add_clause c pr = + add_clause c pr in (* proxy => a<=> b, ¬proxy => a xor b *) - add_clause ~elim:true [Lit.neg proxy; Lit.neg a; b]; - add_clause ~elim:true [Lit.neg proxy; Lit.neg b; a]; - add_clause ~elim:false [proxy; a; b]; - add_clause ~elim:false [proxy; Lit.neg a; Lit.neg 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]); + 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]); + 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]); + 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_ (* make a literal for [t], with a proof of [|- abs(t) = abs(lit)] *) @@ -266,11 +268,6 @@ module Make(A : ARG) : S with module A = A = struct lit in - let add_clause_by_def_ name proxy c : unit = - let pr = pr_bool_c name 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 @@ -279,29 +276,41 @@ module Make(A : ARG) : S with module A = A = struct Lit.neg lit, pr | B_and l -> - let subs = l |> Iter.map get_lit |> Iter.to_list in + 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 SI.define_const si ~const:t_proxy ~rhs:t; (* add clauses *) - List.iter - (fun u -> add_clause_by_def_ "and-e" t_proxy [Lit.neg proxy; u]) - subs; - add_clause_by_def_ "and-i" t_proxy (proxy :: List.map Lit.neg subs); + List.iter2 + (fun t_u u -> + add_clause + [Lit.neg proxy; u] + (A.proof_bool_c "and-i" [t_proxy; t_u])) + t_subs subs; + add_clause (proxy :: List.map Lit.neg subs) + (A.proof_bool_c "and-e" [t_proxy]); proxy, pr_def_refl t_proxy t | B_or l -> - let subs = l |> Iter.map get_lit |> Iter.to_list in + 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 SI.define_const si ~const:t_proxy ~rhs:t; (* add clauses *) - List.iter (fun u -> add_clause_by_def_ "or-i" t_proxy [Lit.neg u; proxy]) subs; - add_clause_by_def_ "or-e" t_proxy (Lit.neg proxy :: subs); + List.iter2 + (fun t_u u -> + add_clause [Lit.neg u; proxy] + (A.proof_bool_c "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 - | B_imply (args, u) -> + | B_imply (t_args, t_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 t_args = Iter.to_list t_args in + let args = List.map (fun t -> Lit.neg (get_lit t)) t_args in + let u = get_lit t_u in let subs = u :: args in (* now the or-encoding *) @@ -309,8 +318,13 @@ module Make(A : ARG) : S with module A = A = struct SI.define_const si ~const:t_proxy ~rhs:t; (* add clauses *) - List.iter (fun u -> add_clause_by_def_ "imp-i" t_proxy [Lit.neg u; proxy]) subs; - add_clause_by_def_ "imp-e" t_proxy (Lit.neg proxy :: subs); + List.iter2 + (fun t_u u -> + add_clause [Lit.neg u; proxy] + (A.proof_bool_c "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 | B_ite _ | B_eq _ | B_neq _ -> mk_lit t, SI.P.refl t