From 27e775ee048ed5a56cc3da200f4446da4ee5ee4d Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 12 Aug 2021 22:05:49 -0400 Subject: [PATCH] wip: refactor proofs for SMT --- src/backend/Backend_intf.ml | 29 --- src/backend/Dot.ml | 156 ---------------- src/backend/Dot.mli | 67 ------- src/backend/dune | 7 - src/cc/Sidekick_cc.ml | 47 ++--- src/cc/Sidekick_cc.mli | 4 +- src/core/Sidekick_core.ml | 153 ++++++---------- src/msat-solver/dune | 2 +- src/sat/Solver.ml | 283 +----------------------------- src/sat/Solver.mli | 6 +- src/sat/Solver_intf.ml | 188 ++++++++------------ src/smtlib/dune | 3 +- src/th-cstor/Sidekick_th_cstor.ml | 1 + 13 files changed, 152 insertions(+), 794 deletions(-) delete mode 100644 src/backend/Backend_intf.ml delete mode 100644 src/backend/Dot.ml delete mode 100644 src/backend/Dot.mli delete mode 100644 src/backend/dune diff --git a/src/backend/Backend_intf.ml b/src/backend/Backend_intf.ml deleted file mode 100644 index b83b5acb..00000000 --- a/src/backend/Backend_intf.ml +++ /dev/null @@ -1,29 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -(** Backend interface - - This modules defines the interface of the modules providing - export of proofs. -*) - -module type S = sig - (** Proof exporting - - Currently, exporting a proof means printing it into a file - according to the conventions of a given format. - *) - - type store - - type t - (** The type of proofs. *) - - val pp : store -> Format.formatter -> t -> unit - (** A function for printing proofs in the desired format. *) - -end - diff --git a/src/backend/Dot.ml b/src/backend/Dot.ml deleted file mode 100644 index e8f2f8e1..00000000 --- a/src/backend/Dot.ml +++ /dev/null @@ -1,156 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -(** Output interface for the backend *) -module type S = Backend_intf.S - -(** Input module for the backend *) -module type Arg = sig - - type atom - (* Type of atoms *) - - type store - type hyp - type lemma - type assumption - (** Types for hypotheses, lemmas, and assumptions. *) - - val print_atom : store -> Format.formatter -> atom -> unit - (** Printing function for atoms *) - - val hyp_info : store -> hyp -> string * string option * (Format.formatter -> unit -> unit) list - val lemma_info : store -> lemma -> string * string option * (Format.formatter -> unit -> unit) list - val assumption_info : store -> assumption -> string * string option * (Format.formatter -> unit -> unit) list - (** Functions to return information about hypotheses and lemmas *) - -end - -module Default(S : Sidekick_sat.S) = struct - module Atom = S.Atom - module Clause = S.Clause - - type store = S.solver - let print_atom = S.Atom.pp - - let hyp_info store c = - "hypothesis", Some "LIGHTBLUE", - [ fun fmt () -> Format.fprintf fmt "%s" @@ S.Clause.short_name store c] - - let lemma_info store c = - "lemma", Some "BLUE", - [ fun fmt () -> Format.fprintf fmt "%s" @@ S.Clause.short_name store c] - - let assumption_info store c = - "assumption", Some "PURPLE", - [ fun fmt () -> Format.fprintf fmt "%s" @@ S.Clause.short_name store c] - -end - -(** Functor to provide dot printing *) -module Make(S : Sidekick_sat.S)(A : Arg with type atom := S.atom - and type hyp := S.clause - and type lemma := S.clause - and type store := S.store - and type assumption := S.clause) = struct - module Atom = S.Atom - module Clause = S.Clause - module P = S.Proof - - let node_id store n = S.Clause.short_name store n.P.conclusion - let proof_id store p = node_id store (P.expand store p) - let res_nn_id store n1 n2 = node_id store n1 ^ "_" ^ node_id store n2 ^ "_res" - let res_np_id store n1 n2 = node_id store n1 ^ "_" ^ proof_id store n2 ^ "_res" - - let print_clause store fmt c = - let v = S.Clause.atoms_a store c in - if Array.length v = 0 then - Format.fprintf fmt "⊥" - else - let n = Array.length v in - for i = 0 to n - 1 do - Format.fprintf fmt "%a" (A.print_atom store) v.(i); - if i < n - 1 then - Format.fprintf fmt ", " - done - - let print_edge fmt i j = - Format.fprintf fmt "%s -> %s;@\n" j i - - let print_edges store fmt n = - match P.(n.step) with - | P.Hyper_res {P.hr_steps=[];_} -> assert false (* NOTE: should never happen *) - | P.Hyper_res {P.hr_init; hr_steps=((_,p0)::_) as l} -> - print_edge fmt (res_np_id store n p0) (proof_id store hr_init); - List.iter - (fun (_,p2) -> print_edge fmt (res_np_id store n p2) (proof_id store p2)) - l; - | _ -> () - - let table_options fmt color = - Format.fprintf fmt "BORDER=\"0\" CELLBORDER=\"1\" CELLSPACING=\"0\" BGCOLOR=\"%s\"" color - - let table store fmt (c, rule, color, l) = - Format.fprintf fmt "%a" (print_clause store) c; - match l with - | [] -> - Format.fprintf fmt "%s" color rule - | f :: r -> - Format.fprintf fmt "%s%a" - color (List.length l) rule f (); - List.iter (fun f -> Format.fprintf fmt "%a" f ()) r - - let print_dot_node store fmt id color c rule rule_color l = - Format.fprintf fmt "%s [shape=plaintext, label=<%a
>];@\n" - id table_options color (table store) (c, rule, rule_color, l) - - let print_dot_res_node store fmt id a = - Format.fprintf fmt "%s [label=<%a>];@\n" id (A.print_atom store) a - - let ttify f c = fun fmt () -> f fmt c - - let print_contents store fmt n = - match P.(n.step) with - (* Leafs of the proof tree *) - | P.Hypothesis _ -> - let rule, color, l = A.hyp_info store P.(n.conclusion) in - let color = match color with None -> "LIGHTBLUE" | Some c -> c in - print_dot_node store fmt (node_id store n) "LIGHTBLUE" P.(n.conclusion) rule color l - | P.Assumption -> - let rule, color, l = A.assumption_info store P.(n.conclusion) in - let color = match color with None -> "LIGHTBLUE" | Some c -> c in - print_dot_node store fmt (node_id store n) "LIGHTBLUE" P.(n.conclusion) rule color l - | P.Lemma _ -> - let rule, color, l = A.lemma_info store P.(n.conclusion) in - let color = match color with None -> "YELLOW" | Some c -> c in - print_dot_node store fmt (node_id store n) "LIGHTBLUE" P.(n.conclusion) rule color l - - (* Tree nodes *) - | P.Duplicate (p, l) -> - print_dot_node store fmt (node_id store n) "GREY" P.(n.conclusion) "Duplicate" "GREY" - ((fun fmt () -> (Format.fprintf fmt "%s" (node_id store n))) :: - List.map (ttify @@ A.print_atom store) l); - print_edge fmt (node_id store n) (node_id store (P.expand store p)) - | P.Hyper_res {P.hr_steps=l; _} -> - print_dot_node store fmt (node_id store n) "GREY" P.(n.conclusion) "Resolution" "GREY" - [(fun fmt () -> (Format.fprintf fmt "%s" (node_id store n)))]; - List.iter - (fun (a,p2) -> - print_dot_res_node store fmt (res_np_id store n p2) a; - print_edge fmt (node_id store n) (res_np_id store n p2)) - l - - let print_node store fmt n = - print_contents store fmt n; - print_edges store fmt n - - let pp store fmt p = - Format.fprintf fmt "digraph proof {@\n"; - P.fold store (fun () -> print_node store fmt) () p; - Format.fprintf fmt "}@." - -end - diff --git a/src/backend/Dot.mli b/src/backend/Dot.mli deleted file mode 100644 index 11bd9a7d..00000000 --- a/src/backend/Dot.mli +++ /dev/null @@ -1,67 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -(** Dot backend for proofs - - This module provides functions to export proofs into the dot graph format. - Graphs in dot format can be used to generates images using the graphviz tool. -*) - -module type S = Backend_intf.S -(** Interface for exporting proofs. *) - -module type Arg = sig - (** Term printing for DOT - - This module defines what functions are required in order to export - a proof to the DOT format. - *) - - type atom - (** The type of atomic formuals *) - - type hyp - type lemma - type assumption - (** The type of theory-specifi proofs (also called lemmas). *) - - type store - - val print_atom : store -> Format.formatter -> atom -> unit - (** Print the contents of the given atomic formulas. - WARNING: this function should take care to escape and/or not output special - reserved characters for the dot format (such as quotes and so on). *) - - val hyp_info : store -> hyp -> string * string option * (Format.formatter -> unit -> unit) list - val lemma_info : store -> lemma -> string * string option * (Format.formatter -> unit -> unit) list - val assumption_info : store -> assumption -> string * string option * (Format.formatter -> unit -> unit) list - (** Generate some information about the leafs of the proof tree. Currently this backend - print each lemma/assumption/hypothesis as a single leaf of the proof tree. - These function should return a triplet [(rule, color, l)], such that: - - [rule] is a name for the proof (arbitrary, does not need to be unique, but - should rather be descriptive) - - [color] is a color name (optional) understood by DOT - - [l] is a list of printers that will be called to print some additional information - *) - -end - -module Default(S : Sidekick_sat.S) : Arg with type atom := S.atom - and type hyp := S.clause - and type lemma := S.clause - and type store := S.store - and type assumption := S.clause -(** Provides a reasonnable default to instantiate the [Make] functor, assuming - the original printing functions are compatible with DOT html labels. *) - -module Make(S : Sidekick_sat.S) - (A : Arg with type atom := S.atom - and type hyp := S.clause - and type lemma := S.clause - and type store := S.store - and type assumption := S.clause) - : S with type t := S.Proof.t and type store := S.store -(** Functor for making a module to export proofs to the DOT format. *) diff --git a/src/backend/dune b/src/backend/dune deleted file mode 100644 index 93b0e234..00000000 --- a/src/backend/dune +++ /dev/null @@ -1,7 +0,0 @@ -(library - (name sidekick_backend) - (public_name sidekick.backend) - (synopsis "Proof backends for sidekick") - (flags :standard -warn-error -a+8) - (libraries sidekick.sat)) - diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml index 941d5507..de98a67f 100644 --- a/src/cc/Sidekick_cc.ml +++ b/src/cc/Sidekick_cc.ml @@ -15,18 +15,18 @@ module type S = Sidekick_core.CC_S module Make (A: CC_ARG) : S with module T = A.T and module Lit = A.Lit - and module P = A.P + and type lemma = A.lemma and module Actions = A.Actions = struct module T = A.T - module P = A.P module Lit = A.Lit module Actions = A.Actions + module P = Actions.P type term = T.Term.t type term_store = T.Term.store type lit = Lit.t type fun_ = T.Fun.t - type proof = P.t + type lemma = A.lemma type actions = Actions.t module Term = T.Term @@ -95,7 +95,6 @@ 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 @@ -169,7 +168,6 @@ 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_debug ~sharing:false) p | E_and (a,b) -> Format.fprintf out "(@[and@ %a@ %a@])" pp a pp b @@ -179,7 +177,6 @@ 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 @@ -283,7 +280,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.t) -> unit + and ev_on_propagate = t -> lit -> (unit -> lit list * P.lemma) -> unit and ev_on_is_subterm = N.t -> term -> unit let[@inline] size_ (r:repr) = r.n_size @@ -310,16 +307,8 @@ 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 p_lits = - let p = P.cc_lemma p_lits in - (* useful to debug bad lemmas - let n_pos = Iter.of_list p_lits |> Iter.filter P.lit_sign |> Iter.length in - if n_pos <> 1 then ( - Log.debugf 0 (fun k->k"emit (n-pos=%d) :from %s@ %a@ :lits %a" - n_pos what - (P.pp_debug ~sharing:false) p Fmt.(Dump.list Lit.pp) lits); - ); - *) + 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 *) @@ -473,9 +462,6 @@ module Make (A: CC_ARG) | E_lit lit -> lit :: acc | E_theory e' -> th := true; explain_decompose_expl 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_equal cc ~th acc a b | E_merge_t (a,b) -> (* find nodes for [a] and [b] on the fly *) @@ -676,14 +662,8 @@ module Make (A: CC_ARG) let lits = explain_equal cc ~th lits a ra in let lits = explain_equal cc ~th lits b rb in let proof = - let p_lits = - lits - |> List.rev_map (fun lit -> - let t, sign = Lit.signed_term lit in - P.lit_mk (not sign) t) - in - ret_cc_lemma "true-eq-false" lits p_lits - in + 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 ); (* We will merge [r_from] into [r_into]. @@ -801,10 +781,7 @@ module Make (A: CC_ARG) let lits = explain_equal cc ~th acc u1 t1 in let p_lits = (* make a tautology, not a true guard *) - let tauto = lit :: List.rev_map Lit.neg lits in - tauto |> List.rev_map (fun lit -> - let t, sign = Lit.signed_term lit in - A.P.(lit_mk sign t)) + Iter.cons lit (Iter.of_list lits |> Iter.map Lit.neg) in let p = ret_cc_lemma "bool-parent" lits p_lits in lits, p @@ -875,11 +852,7 @@ module Make (A: CC_ARG) let lits = explain_decompose_expl cc ~th [] expl in let lits = List.rev_map Lit.neg lits in let proof = - let p_lits = - lits |> List.rev_map (fun lit -> - let t, sign = Lit.signed_term lit in - P.lit_mk sign t) - in + let p_lits = Iter.of_list lits in ret_cc_lemma "from-expl" lits p_lits in raise_conflict_ cc ~th:!th acts lits proof diff --git a/src/cc/Sidekick_cc.mli b/src/cc/Sidekick_cc.mli index 6201f09e..21566fc7 100644 --- a/src/cc/Sidekick_cc.mli +++ b/src/cc/Sidekick_cc.mli @@ -4,7 +4,7 @@ open Sidekick_core module type S = Sidekick_core.CC_S module Make (A: CC_ARG) - : S with module T = A.T + : S with module T = A.T and module Lit = A.Lit - and module P = A.P + and type lemma = A.lemma and module Actions = A.Actions diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index 84a58527..69fc3256 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -145,89 +145,37 @@ module type TERM = sig end end -(** Proofs of unsatisfiability *) +(** Proofs for the congruence closure *) +module type CC_PROOF = sig + type lit + type lemma + + val lemma_cc : lit Iter.t -> lemma +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, + annotating enough for the checker to reconstruct them. + This allows for low overhead proof production. *) module type PROOF = sig type t (** The abstract representation of a proof. A proof always proves a clause to be {b valid} (true in every possible interpretation of the problem's assertions, and the theories) *) - type term - type ty - - type hres_step - (** hyper-resolution steps: resolution, unit resolution; - bool paramodulation, unit bool paramodulation *) - - val r : t -> pivot:term -> hres_step - (** Resolution step on given pivot term *) - - val r1 : t -> hres_step - (** Unit resolution; pivot is obvious *) - - val p : t -> lhs:term -> rhs:term -> hres_step - (** Paramodulation using proof whose conclusion has a literal [lhs=rhs] *) - - val p1 : t -> hres_step - (** Unit paramodulation *) + type lemma type lit - (** Proof representation of literals *) - val pp_lit : lit Fmt.printer - val lit_a : term -> lit - val lit_na : term -> lit - val lit_mk : bool -> term -> lit - val lit_eq : term -> term -> lit - val lit_neq : term -> term -> lit - val lit_not : lit -> lit - val lit_sign : lit -> bool + include CC_PROOF + with type lemma := lemma + and type lit := lit - type composite_step - - val stepc : 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 - val ref_by_name : string -> t (* named clause, see {!defc} *) - val assertion_c_l : lit list -> t - val drup_res : lit list -> t (* assert clause and let DRUP take care of it *) - val hres_iter : t -> hres_step Iter.t -> t (* hyper-res *) - val hres_l : t -> hres_step list -> t (* hyper-res *) - val res : pivot:term -> t -> t -> t (* resolution with pivot *) - val res1 : t -> t -> t (* unit resolution *) - 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 nn : t -> t (* negation normalization *) - val cc_lemma : lit list -> 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 composite_iter : ?assms:(string * lit) list -> composite_step Iter.t -> t - val composite_l : ?assms:(string * lit) list -> composite_step list -> t - val sorry : t [@@alert cstor "sorry used"] (* proof hole when we don't know how to produce a proof *) - val sorry_c : lit Iter.t -> t - [@@alert cstor "sorry used"] (* proof hole when we don't know how to produce a proof *) - - val sorry_c_l : lit list -> t - - val default : t [@@alert cstor "do not use default constructor"] - - val pp_debug : sharing:bool -> t Fmt.printer - (** Pretty print a proof. - @param sharing if true, try to compact the proof by introducing - definitions for common terms, clauses, and steps as needed. Safe to ignore. *) - - module Quip : sig - val output : out_channel -> t -> unit - (** Printer in Quip format (experimental) *) - end + val enabled : t -> bool end (** Literals @@ -274,20 +222,21 @@ module type CC_ACTIONS = sig module T : TERM module Lit : LIT with module T = T - module P : PROOF with type term = T.Term.t + type lemma + module P : CC_PROOF with type lit = Lit.t and type lemma = lemma 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 -> P.t -> 'a + val raise_conflict : t -> Lit.t list -> lemma -> '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 * P.t) -> unit + val propagate : t -> Lit.t -> reason:(unit -> Lit.t list * lemma) -> unit (** [propagate acts lit ~reason pr] declares that [reason() => lit] is a tautology. @@ -301,15 +250,19 @@ end (** Arguments to a congruence closure's implementation *) module type CC_ARG = sig module T : TERM - module P : PROOF with type term = T.Term.t module Lit : LIT with module T = T - module Actions : CC_ACTIONS with module T=T and module P = P and module Lit = Lit + type lemma + module P : CC_PROOF with type lit = Lit.t and type lemma = lemma + module Actions : CC_ACTIONS + with module T=T + and module Lit = Lit + and type lemma = lemma 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 *) end -(** Main congruence closure. +(** Main congruence closure signature. The congruence closure handles the theory QF_UF (uninterpreted function symbols). @@ -329,14 +282,17 @@ module type CC_S = sig (** first, some aliases. *) module T : TERM - module P : PROOF with type term = T.Term.t module Lit : LIT with module T = T - module Actions : CC_ACTIONS with module T = T and module Lit = Lit and module P = P + type lemma + module P : CC_PROOF with type lit = Lit.t and type lemma = lemma + module Actions : CC_ACTIONS + with module T = T + and module Lit = Lit + and type lemma = lemma type term_store = T.Term.store type term = T.Term.t type fun_ = T.Fun.t type lit = Lit.t - type proof = P.t type actions = Actions.t type t @@ -421,7 +377,6 @@ 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 @@ -474,7 +429,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.t) -> unit + type ev_on_propagate = t -> lit -> (unit -> lit list * P.lemma) -> unit (** [ev_on_propagate cc lit reason] is called whenever [reason() => lit] is a propagated lemma. See {!CC_ACTIONS.propagate}. *) @@ -620,12 +575,22 @@ end new lemmas, propagate literals, access the congruence closure, etc. *) module type SOLVER_INTERNAL = sig module T : TERM - module P : PROOF with type term = T.Term.t type ty = T.Ty.t type term = T.Term.t type term_store = T.Term.store type ty_store = T.Ty.store + + (** {3 Literals} + + A literal is a (preprocessed) term along with its sign. + It is directly manipulated by the SAT solver. + *) + 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 (** {3 Main type for a solver} *) @@ -641,13 +606,6 @@ module type SOLVER_INTERNAL = sig type actions (** Handle that the theories can use to perform actions. *) - (** {3 Literals} - - A literal is a (preprocessed) term along with its sign. - It is directly manipulated by the SAT solver. - *) - module Lit : LIT with module T = T - type lit = Lit.t (** {3 Proof helpers} *) @@ -662,8 +620,10 @@ module type SOLVER_INTERNAL = sig (** Congruence closure instance *) module CC : CC_S with module T = T - and module P = P and module Lit = Lit + and type lemma = lemma + and type P.lemma = lemma + and type P.lit = lit and type Actions.t = actions val cc : t -> CC.t @@ -872,15 +832,16 @@ end Theory implementors will mostly interact with {!SOLVER_INTERNAL}. *) module type SOLVER = sig module T : TERM - module P : PROOF with type term = T.Term.t - module Lit : LIT with module T = T + type lemma + module P : PROOF with type lit = Lit.t and type lemma = lemma module Solver_internal : SOLVER_INTERNAL with module T = T - and module P = P and module Lit = Lit + and type lemma = lemma + and module P = P (** Internal solver, available to theories. *) type t diff --git a/src/msat-solver/dune b/src/msat-solver/dune index 78d55808..8e6100cd 100644 --- a/src/msat-solver/dune +++ b/src/msat-solver/dune @@ -2,5 +2,5 @@ (name Sidekick_msat_solver) (public_name sidekick.msat-solver) (libraries containers iter sidekick.core sidekick.util - sidekick.cc sidekick.sat sidekick.backend) + sidekick.cc sidekick.sat) (flags :standard -open Sidekick_util)) diff --git a/src/sat/Solver.ml b/src/sat/Solver.ml index 089e88ea..0c119711 100644 --- a/src/sat/Solver.ml +++ b/src/sat/Solver.ml @@ -34,10 +34,12 @@ end module Make(Plugin : PLUGIN) = struct module Formula = Plugin.Formula + module Proof = Plugin.Proof type formula = Formula.t type theory = Plugin.t - type lemma = Plugin.proof + type lemma = Plugin.lemma + type proof = Plugin.proof (* ### types ### *) @@ -511,279 +513,6 @@ module Make(Plugin : PLUGIN) module Var = Store.Var module Clause = Store.Clause - (* TODO: mostly, move into a functor outside that works on integers *) - module Proof = struct - exception Resolution_error of string - - type atom = Atom.t - type clause = Clause.t - type formula = Formula.t - type lemma = Plugin.proof - type nonrec store = store - - let error_res_f msg = Format.kasprintf (fun s -> raise (Resolution_error s)) msg - - let[@inline] clear_var_of_ store (a:atom) = Store.clear_var store (Atom.var a) - - (* Compute resolution of 2 clauses. - returns [pivots, resulting_atoms] *) - let resolve store (c1:clause) (c2:clause) : atom list * atom list = - (* invariants: only atoms in [c2] are marked, and the pivot is - cleared when traversing [c1] *) - Clause.iter store c2 ~f:(Atom.mark store); - let pivots = ref [] in - let l = - Clause.fold store [] c1 - ~f:(fun l a -> - if Atom.marked store a then l - else if Atom.marked store (Atom.neg a) then ( - pivots := (Atom.abs a) :: !pivots; - clear_var_of_ store a; - l - ) else a::l) - in - let l = - Clause.fold store l c2 - ~f:(fun l a -> if Atom.marked store a then a::l else l) - in - Clause.iter store c2 ~f:(clear_var_of_ store); - !pivots, l - - (* [find_dups c] returns a list of duplicate atoms, and the deduplicated list *) - let find_dups (store:store) (c:clause) : atom list * atom list = - let res = - Clause.fold store ([], []) c - ~f:(fun (dups,l) a -> - if Atom.marked store a then ( - a::dups, l - ) else ( - Atom.mark store a; - dups, a::l - )) - in - Clause.iter store c ~f:(clear_var_of_ store); - res - - (* do [c1] and [c2] have the same lits, modulo reordering and duplicates? *) - let same_lits store (c1:atom Iter.t) (c2:atom Iter.t): bool = - let subset a b = - Iter.iter (Atom.mark store) b; - let res = Iter.for_all (Atom.marked store) a in - Iter.iter (clear_var_of_ store) b; - res - in - subset c1 c2 && subset c2 c1 - - let prove (store:store) conclusion = - match Clause.premise store conclusion with - | History [] -> assert false - | Empty_premise -> raise Solver_intf.No_proof - | _ -> conclusion - - let rec set_atom_proof store a = - let aux acc b = - if Atom.equal (Atom.neg a) b then acc - else set_atom_proof store b :: acc - in - assert (Var.level store (Atom.var a) >= 0); - match Var.reason store (Atom.var a) with - | Some (Bcp c | Bcp_lazy (lazy c)) -> - Log.debugf 5 (fun k->k "(@[proof.analyze.clause@ :atom %a@ :c %a@])" - (Atom.debug store) a (Clause.debug store) c); - if Clause.n_atoms store c = 1 then ( - Log.debugf 5 (fun k -> k "(@[proof.analyze.old-reason@ %a@])" - (Atom.debug store) a); - c - ) else ( - assert (Atom.is_false store a); - let r = History (c :: (Clause.fold store [] c ~f:aux)) in - let c' = Clause.make_l store ~removable:false [Atom.neg a] r in - Var.set_reason store (Atom.var a) (Some (Bcp c')); - Log.debugf 5 - (fun k -> k "(@[proof.analyze.new-reason@ :atom %a@ :c %a@])" - (Atom.debug store) a (Clause.debug store) c'); - c' - ) - | _ -> - error_res_f "cannot prove atom %a" (Atom.debug store) a - - let prove_unsat store conflict = - if Clause.n_atoms store conflict = 0 then ( - conflict - ) else ( - Log.debugf 1 (fun k -> k "(@[sat.prove-unsat@ :from %a@])" (Clause.debug store) conflict); - let l = Clause.fold store [] conflict - ~f:(fun acc a -> set_atom_proof store a :: acc) in - let res = Clause.make_l store ~removable:false [] (History (conflict :: l)) in - Log.debugf 1 (fun k -> k "(@[sat.proof-found@ %a@])" (Clause.debug store) res); - res - ) - - let prove_atom self a = - if Atom.is_true self a && - Var.level self (Atom.var a) = 0 then - Some (set_atom_proof self a) - else - None - - type t = clause - and proof_node = { - conclusion : clause; - step : step; - } - and step = - | Hypothesis of lemma - | Assumption - | Lemma of lemma - | Duplicate of t * atom list - | Hyper_res of hyper_res_step - - and hyper_res_step = { - hr_init: t; - hr_steps: (atom * t) list; (* list of pivot+clause to resolve against [init] *) - } - - let[@inline] conclusion (p:t) : clause = p - - (* find pivots for resolving [l] with [init], and also return - the atoms of the conclusion *) - let find_pivots store (init:clause) (l:clause list) : _ * (atom * t) list = - Log.debugf 15 - (fun k->k "(@[proof.find-pivots@ :init %a@ :l %a@])" - (Clause.debug store) init (Format.pp_print_list (Clause.debug store)) l); - Clause.iter store init ~f:(Atom.mark store); - let steps = - List.map - (fun c -> - let pivot = - match - Clause.atoms_iter store c - |> Iter.filter (fun a -> Atom.marked store (Atom.neg a)) - |> Iter.to_list - with - | [a] -> a - | [] -> - error_res_f "(@[proof.expand.pivot_missing@ %a@])" (Clause.debug store) c - | pivots -> - error_res_f "(@[proof.expand.multiple_pivots@ %a@ :pivots %a@])" - (Clause.debug store) c (Atom.debug_l store) pivots - in - Clause.iter store c ~f:(Atom.mark store); (* add atoms to result *) - clear_var_of_ store pivot; - Atom.abs pivot, c) - l - in - (* cleanup *) - let res = ref [] in - let cleanup_a_ a = - if Atom.marked store a then ( - res := a :: !res; - clear_var_of_ store a - ) - in - Clause.iter store init ~f:cleanup_a_; - List.iter (fun c -> Clause.iter store c ~f:cleanup_a_) l; - !res, steps - - let expand store conclusion = - Log.debugf 5 (fun k -> k "(@[sat.proof.expand@ @[%a@]@])" (Clause.debug store) conclusion); - match Clause.premise store conclusion with - | Lemma l -> - { conclusion; step = Lemma l; } - | Local -> - { conclusion; step = Assumption; } - | Hyp l -> - { conclusion; step = Hypothesis l; } - | History [] -> - error_res_f "@[empty history for clause@ %a@]" (Clause.debug store) conclusion - | History [c] -> - let duplicates, res = find_dups store c in - assert (same_lits store (Iter.of_list res) (Clause.atoms_iter store conclusion)); - { conclusion; step = Duplicate (c, duplicates) } - | History (c :: r) -> - let res, steps = find_pivots store c r in - assert (same_lits store (Iter.of_list res) (Clause.atoms_iter store conclusion)); - { conclusion; step = Hyper_res {hr_init=c; hr_steps=steps}; } - | Empty_premise -> raise Solver_intf.No_proof - - let rec res_of_hyper_res store (hr: hyper_res_step) : _ * _ * atom = - let {hr_init=c1; hr_steps=l} = hr in - match l with - | [] -> assert false - | [a, c2] -> c1, c2, a (* done *) - | (a,c2) :: steps' -> - (* resolve [c1] with [c2], then resolve that against [steps] *) - let pivots, l = resolve store c1 c2 in - assert (match pivots with [a'] -> Atom.equal a a' | _ -> false); - let c_1_2 = Clause.make_l store ~removable:true l (History [c1; c2]) in - res_of_hyper_res store {hr_init=c_1_2; hr_steps=steps'} - - (* Proof nodes manipulation *) - let is_leaf = function - | Hypothesis _ - | Assumption - | Lemma _ -> true - | Duplicate _ - | Hyper_res _ -> false - - let parents = function - | Hypothesis _ - | Assumption - | Lemma _ -> [] - | Duplicate (p, _) -> [p] - | Hyper_res {hr_init; hr_steps} -> hr_init :: List.map snd hr_steps - - let expl = function - | Hypothesis _ -> "hypothesis" - | Assumption -> "assumption" - | Lemma _ -> "lemma" - | Duplicate _ -> "duplicate" - | Hyper_res _ -> "hyper-resolution" - - module Tbl = Clause.Tbl - - type task = - | Enter of t - | Leaving of t - - let spop s = try Some (Stack.pop s) with Stack.Empty -> None - - let rec fold_aux self s h f acc = - match spop s with - | None -> acc - | Some (Leaving c) -> - Tbl.add h c true; - fold_aux self s h f (f acc (expand self c)) - | Some (Enter c) -> - if not (Tbl.mem h c) then begin - Stack.push (Leaving c) s; - let node = expand self c in - begin match node.step with - | Duplicate (p1, _) -> - Stack.push (Enter p1) s - | Hyper_res {hr_init=p1; hr_steps=l} -> - List.iter (fun (_,p2) -> Stack.push (Enter p2) s) l; - Stack.push (Enter p1) s; - | Hypothesis _ | Assumption | Lemma _ -> () - end - end; - fold_aux self s h f acc - - let fold self f acc p = - let h = Tbl.create 42 in - let s = Stack.create () in - Stack.push (Enter p) s; - fold_aux self s h f acc - - let check_empty_conclusion store (p:t) = - if Clause.n_atoms store p > 0 then ( - error_res_f "@[<2>Proof.check: non empty conclusion for clause@ %a@]" - (Clause.debug store) p; - ) - - let check self (p:t) = fold self (fun () _ -> ()) () p - end - module H = (Heap.Make [@specialise]) (struct type store = Store.t type t = var @@ -1775,7 +1504,8 @@ module Make(Plugin : PLUGIN) let[@inline] current_slice st : _ Solver_intf.acts = let module M = struct - type nonrec proof = lemma + type nonrec proof = proof + type nonrec lemma = lemma type nonrec formula = formula let iter_assumptions=acts_iter st ~full:false st.th_head let eval_lit= acts_eval_lit st @@ -1790,7 +1520,8 @@ module Make(Plugin : PLUGIN) (* full slice, for [if_sat] final check *) let[@inline] full_slice st : _ Solver_intf.acts = let module M = struct - type nonrec proof = lemma + type nonrec proof = proof + type nonrec lemma = lemma type nonrec formula = formula let iter_assumptions=acts_iter st ~full:true st.th_head let eval_lit= acts_eval_lit st diff --git a/src/sat/Solver.mli b/src/sat/Solver.mli index c6b8e28d..1af4efd8 100644 --- a/src/sat/Solver.mli +++ b/src/sat/Solver.mli @@ -4,10 +4,12 @@ module type S = Solver_intf.S module Make_pure_sat(Th: Solver_intf.PLUGIN_SAT) : S with module Formula = Th.Formula - and type lemma = Th.proof + and type lemma = Th.lemma + and type proof = Th.proof and type theory = unit module Make_cdcl_t(Th : Solver_intf.PLUGIN_CDCL_T) : S with module Formula = Th.Formula - and type lemma = Th.proof + and type lemma = Th.lemma + and type proof = Th.proof and type theory = Th.t diff --git a/src/sat/Solver_intf.ml b/src/sat/Solver_intf.ml index 4622fc7c..cccd5f90 100644 --- a/src/sat/Solver_intf.ml +++ b/src/sat/Solver_intf.ml @@ -64,8 +64,8 @@ type negated = See {!val:Expr_intf.S.norm} for more details. *) (** The type of reasons for propagations of a formula [f]. *) -type ('formula, 'proof) reason = - | Consequence of (unit -> 'formula list * 'proof) [@@unboxed] +type ('formula, 'lemma) reason = + | Consequence of (unit -> 'formula list * 'lemma) [@@unboxed] (** [Consequence (l, p)] means that the formulas in [l] imply the propagated formula [f]. The proof should be a proof of the clause "[l] implies [f]". @@ -90,7 +90,7 @@ type lbool = L_true | L_false | L_undefined module type ACTS = sig type formula - type proof + type lemma val iter_assumptions: (formula -> unit) -> unit (** Traverse the new assumptions on the boolean trail. *) @@ -102,19 +102,19 @@ module type ACTS = sig (** Map the given formula to a literal, which will be decided by the SAT solver. *) - val add_clause: ?keep:bool -> formula list -> proof -> unit + val add_clause: ?keep:bool -> formula list -> lemma -> unit (** Add a clause to the solver. @param keep if true, the clause will be kept by the solver. Otherwise the solver is allowed to GC the clause and propose this partial model again. *) - val raise_conflict: formula list -> proof -> 'b + val raise_conflict: formula list -> lemma -> 'b (** Raise a conflict, yielding control back to the solver. The list of atoms must be a valid theory lemma that is false in the current trail. *) - val propagate: formula -> (formula, proof) reason -> unit + val propagate: formula -> (formula, lemma) reason -> unit (** Propagate a formula, i.e. the theory can evaluate the formula to be true (see the definition of {!type:eval_res} *) @@ -124,10 +124,9 @@ module type ACTS = sig Useful for theory combination. This will be undone on backtracking. *) end -(* TODO: find a way to use atoms instead of formulas here *) -type ('formula, 'proof) acts = +type ('formula, 'lemma) acts = (module ACTS with type formula = 'formula - and type proof = 'proof) + and type lemma = 'lemma) (** The type for a slice of assertions to assume/propagate in the theory. *) exception No_proof @@ -158,6 +157,45 @@ module type FORMULA = sig but one returns [Negated] and the other [Same_sign]. *) end +(** Signature for proof emission, using DRUP. + + We do not store the resolution steps, just the stream of clauses deduced. + See {!Sidekick_drup} for checking these proofs. *) +module type PROOF = sig + type t + (** The stored proof (possibly nil, possibly on disk, possibly in memory) *) + + type atom + (** A boolean atom for the proof trace *) + + type lemma + (** A theory lemma *) + + module Atom : sig + type t = atom + val sign : t -> bool + val var_int : t -> int + val make : sign:bool -> int -> t + val pp : t Fmt.printer + end + + val enabled : t -> bool + (** Do we emit proofs at all? *) + + val emit_input_clause : t -> atom Iter.t -> unit + (** Emit an input clause. *) + + val emit_lemma : t -> atom Iter.t -> lemma -> unit + (** Emit a theory lemma *) + + val emit_redundant_clause : t -> atom Iter.t -> unit + (** Emit a clause deduced by the SAT solver, redundant wrt axioms. + The clause must be RUP wrt previous clauses. *) + + val del_clause : t -> atom Iter.t -> unit + (** Forget a clause. Only useful for performance considerations. *) +end + (** Signature for theories to be given to the CDCL(T) solver *) module type PLUGIN_CDCL_T = sig type t @@ -166,6 +204,14 @@ module type PLUGIN_CDCL_T = sig module Formula : FORMULA type proof + (** Proof storage/recording *) + + type lemma + (* Theory lemmas *) + + module Proof : PROOF + with type t = proof + and type lemma = lemma val push_level : t -> unit (** Create a new backtrack level *) @@ -173,12 +219,12 @@ module type PLUGIN_CDCL_T = sig val pop_levels : t -> int -> unit (** Pop [n] levels of the theory *) - val partial_check : t -> (Formula.t, proof) acts -> unit + val partial_check : t -> (Formula.t, lemma) acts -> unit (** Assume the formulas in the slice, possibly using the [slice] to push new formulas to be propagated or to raising a conflict or to add new lemmas. *) - val final_check : t -> (Formula.t, proof) acts -> unit + val final_check : t -> (Formula.t, lemma) acts -> unit (** Called at the end of the search in case a model has been found. If no new clause is pushed, then proof search ends and "sat" is returned; if lemmas are added, search is resumed; @@ -189,111 +235,12 @@ end module type PLUGIN_SAT = sig module Formula : FORMULA + type lemma = unit type proof -end -module type PROOF = sig - (** Signature for a module handling proof by resolution from sat solving traces *) - - (** {3 Type declarations} *) - - exception Resolution_error of string - (** Raised when resolution failed. *) - - type formula - type atom - type lemma - type clause - (** Abstract types for atoms, clauses and theory-specific lemmas *) - - type store - - type t - (** Lazy type for proof trees. Proofs are persistent objects, and can be - extended to proof nodes using functions defined later. *) - - and proof_node = { - conclusion : clause; (** The conclusion of the proof *) - step : step; (** The reasoning step used to prove the conclusion *) - } - (** A proof can be expanded into a proof node, which show the first step of the proof. *) - - (** The type of reasoning steps allowed in a proof. *) - and step = - | Hypothesis of lemma - (** The conclusion is a user-provided hypothesis *) - | Assumption - (** The conclusion has been locally assumed by the user *) - | Lemma of lemma - (** The conclusion is a tautology provided by the theory, with associated proof *) - | Duplicate of t * atom list - (** The conclusion is obtained by eliminating multiple occurences of the atom in - the conclusion of the provided proof. *) - | Hyper_res of hyper_res_step - - and hyper_res_step = { - hr_init: t; - hr_steps: (atom * t) list; (* list of pivot+clause to resolve against [init] *) - } - - (** {3 Proof building functions} *) - - val prove : store -> clause -> t - (** Given a clause, return a proof of that clause. - @raise Resolution_error if it does not succeed. *) - - val prove_unsat : store -> clause -> t - (** Given a conflict clause [c], returns a proof of the empty clause. - @raise Resolution_error if it does not succeed. *) - - val prove_atom : store -> atom -> t option - (** Given an atom [a], returns a proof of the clause [[a]] if [a] is true at level 0 *) - - val res_of_hyper_res : store -> hyper_res_step -> t * t * atom - (** Turn an hyper resolution step into a resolution step. - The conclusion can be deduced by performing a resolution between the conclusions - of the two given proofs. - The atom on which to perform the resolution is also given. *) - - (** {3 Proof Nodes} *) - - val parents : step -> t list - (** Returns the parents of a proof node. *) - - val is_leaf : step -> bool - (** Returns wether the the proof node is a leaf, i.e. an hypothesis, - an assumption, or a lemma. - [true] if and only if {!parents} returns the empty list. *) - - val expl : step -> string - (** Returns a short string description for the proof step; for instance - ["hypothesis"] for a [Hypothesis] - (it currently returns the variant name in lowercase). *) - - - (** {3 Proof Manipulation} *) - - val expand : store -> t -> proof_node - (** Return the proof step at the root of a given proof. *) - - val conclusion : t -> clause - (** What is proved at the root of the clause *) - - val fold : store -> ('a -> proof_node -> 'a) -> 'a -> t -> 'a - (** [fold f acc p], fold [f] over the proof [p] and all its node. It is guaranteed that - [f] is executed exactly once on each proof node in the tree, and that the execution of - [f] on a proof node happens after the execution on the parents of the nodes. *) - - (** {3 Misc} *) - - val check_empty_conclusion : store -> t -> unit - (** Check that the proof's conclusion is the empty clause, - @raise Resolution_error otherwise *) - - val check : store -> t -> unit - (** Check the contents of a proof. Mainly for internal use. *) - - module Tbl : Hashtbl.S with type key = t + module Proof : PROOF + with type t = proof + and type lemma = lemma end (** The external interface implemented by safe solvers, such as the one @@ -317,11 +264,16 @@ module type S = sig type theory type lemma - (** A theory lemma or an input axiom *) + (** A theory lemma or an input axiom. *) + + type proof + (** A representation of a full proof *) type solver + (** The main solver type. *) type store + (** Stores atoms, clauses, etc. *) (* TODO: keep this internal *) module Atom : sig @@ -365,11 +317,9 @@ module type S = sig end module Proof : PROOF - with type clause = clause - and type atom = atom - and type formula = formula + with type atom = atom and type lemma = lemma - and type store = store + and type t = proof (** A module to manipulate proofs. *) type t = solver diff --git a/src/smtlib/dune b/src/smtlib/dune index 4476ec7a..e2b27b65 100644 --- a/src/smtlib/dune +++ b/src/smtlib/dune @@ -3,6 +3,5 @@ (public_name sidekick-bin.smtlib) (libraries containers zarith sidekick.core sidekick.util sidekick-base sidekick-base.solver - sidekick.backend smtlib-utils - sidekick.tef) + smtlib-utils sidekick.tef) (flags :standard -warn-error -a+8 -open Sidekick_util)) diff --git a/src/th-cstor/Sidekick_th_cstor.ml b/src/th-cstor/Sidekick_th_cstor.ml index d568adfa..9bfb0fec 100644 --- a/src/th-cstor/Sidekick_th_cstor.ml +++ b/src/th-cstor/Sidekick_th_cstor.ml @@ -9,6 +9,7 @@ let name = "th-cstor" module type ARG = sig module S : Sidekick_core.SOLVER val view_as_cstor : S.T.Term.t -> (S.T.Fun.t, S.T.Term.t) cstor_view + val lemma_cstor : S.Lit.t Iter.t -> S.lemma end module type S = sig