From 9f01b98cde76efa4f13acc0de0e9b6f6079920b7 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 18 Aug 2021 23:59:39 -0400 Subject: [PATCH] wip: imperative proofs - getting closer to having the SMT solver compile again - dummy proof implementation - DRUP proof implementation for pure SAT solver --- src/base-solver/sidekick_base_solver.ml | 29 ++++---- src/base/Lit.ml | 2 + src/base/Lit.mli | 2 + src/base/Proof_stub.ml | 30 ++++++++ src/base/Proof_stub.mli | 20 ++++++ src/base/Sidekick_base.ml | 22 ++---- src/base/Solver_arg.ml | 6 ++ src/base/Solver_arg.mli | 15 ++++ src/base/dune | 2 +- src/core/Sidekick_core.ml | 2 + src/lra/sidekick_arith_lra.ml | 64 ++++++++--------- src/main/main.ml | 15 ++-- src/main/pure_sat_solver.ml | 83 +++++++++++++++++++---- src/mini-cc/tests/sidekick_test_minicc.ml | 2 +- src/{base => proof}/Proof.ml | 2 + src/{base => proof}/Proof.mli | 3 + src/sat/Solver.ml | 15 ++++ src/sat/Solver_intf.ml | 10 ++- src/smt-solver/Sidekick_smt_solver.ml | 6 +- src/smtlib/Process.ml | 58 +++++++--------- src/smtlib/Process.mli | 4 +- src/th-cstor/Sidekick_th_cstor.ml | 5 +- src/th-data/Sidekick_th_data.ml | 13 ++-- src/th-data/Sidekick_th_data.mli | 14 ++-- 24 files changed, 280 insertions(+), 144 deletions(-) create mode 100644 src/base/Lit.ml create mode 100644 src/base/Lit.mli create mode 100644 src/base/Proof_stub.ml create mode 100644 src/base/Proof_stub.mli create mode 100644 src/base/Solver_arg.ml create mode 100644 src/base/Solver_arg.mli rename src/{base => proof}/Proof.ml (99%) rename src/{base => proof}/Proof.mli (98%) diff --git a/src/base-solver/sidekick_base_solver.ml b/src/base-solver/sidekick_base_solver.ml index 77b82a1c..2ce8c468 100644 --- a/src/base-solver/sidekick_base_solver.ml +++ b/src/base-solver/sidekick_base_solver.ml @@ -9,21 +9,24 @@ open Sidekick_base (** Argument to the SMT solver *) module Solver_arg = struct - module T = Sidekick_base + module T = Sidekick_base.Solver_arg + module Lit = Sidekick_base.Lit let cc_view = Term.cc_view let is_valid_literal _ = true - module P = Proof + module P = Proof_stub + type proof = P.t end -(** SMT solver, obtained from {!Sidekick_msat_solver} *) -module Solver = Sidekick_msat_solver.Make(Solver_arg) +(** SMT solver, obtained from {!Sidekick_smt_solver} *) +module Solver = Sidekick_smt_solver.Make(Solver_arg) (** Theory of datatypes *) module Th_data = Sidekick_th_data.Make(struct module S = Solver open Base_types open Sidekick_th_data + module Proof = Proof_stub module Cstor = Cstor let as_datatype ty = match Ty.view ty with @@ -56,9 +59,9 @@ module Th_data = Sidekick_th_data.Make(struct let ty_is_finite = Ty.finite let ty_set_is_finite = Ty.set_finite - let proof_isa_disj = Proof.isa_disj - let proof_isa_split = Proof.isa_split - let proof_cstor_inj = Proof.cstor_inj + let lemma_isa_disj p lits = Proof.lemma_isa_disj p lits + let lemma_isa_split p lits = Proof.lemma_isa_split p lits + let lemma_cstor_inj p lits = Proof.lemma_cstor_inj p lits end) (** Reducing boolean formulas to clauses *) @@ -66,10 +69,11 @@ module Th_bool = Sidekick_th_bool_static.Make(struct module S = Solver type term = S.T.Term.t include Form - 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 + let lemma_bool_tauto = Proof_stub.lemma_bool_tauto + let lemma_bool_c = Proof_stub.lemma_bool_c + let lemma_bool_equiv = Proof_stub.lemma_bool_equiv + let lemma_ite_true = Proof_stub.lemma_ite_true + let lemma_ite_false = Proof_stub.lemma_ite_false end) (** Theory of Linear Rational Arithmetic *) @@ -91,8 +95,7 @@ module Th_lra = Sidekick_arith_lra.Make(struct let ty_lra _st = Ty.real() let has_ty_real t = Ty.equal (T.ty t) (Ty.real()) - let proof_lra = Proof.lra - let proof_lra_l = Proof.lra_l + let lemma_lra = Proof_stub.lemma_lra module Gensym = struct type t = { diff --git a/src/base/Lit.ml b/src/base/Lit.ml new file mode 100644 index 00000000..2c702501 --- /dev/null +++ b/src/base/Lit.ml @@ -0,0 +1,2 @@ + +include Sidekick_lit.Make(Solver_arg) diff --git a/src/base/Lit.mli b/src/base/Lit.mli new file mode 100644 index 00000000..50ae442c --- /dev/null +++ b/src/base/Lit.mli @@ -0,0 +1,2 @@ + +include Sidekick_core.LIT with module T = Solver_arg diff --git a/src/base/Proof_stub.ml b/src/base/Proof_stub.ml new file mode 100644 index 00000000..8c97947b --- /dev/null +++ b/src/base/Proof_stub.ml @@ -0,0 +1,30 @@ + +open Base_types + +type lit = Lit.t +type term = Term.t + +type t = unit +type dproof = t -> unit + +let create () : t = () +let enabled _ = false + +let begin_subproof _ = () +let end_subproof _ = () +let del_clause _ _ = () +let emit_redundant_clause _ _ = () +let emit_input_clause _ _ = () +let define_term _ _ _ = () +let lemma_preprocess _ _ _ = () +let lemma_true _ _ = () +let lemma_cc _ _ = () +let lemma_lra _ _ = () +let lemma_cstor_inj _ _ = () +let lemma_isa_disj _ _ = () +let lemma_isa_split _ _ = () +let lemma_bool_tauto _ _ = () +let lemma_bool_c _ _ _ = () +let lemma_bool_equiv _ _ _ = () +let lemma_ite_true _ ~a:_ ~ite:_ = () +let lemma_ite_false _ ~a:_ ~ite:_ = () diff --git a/src/base/Proof_stub.mli b/src/base/Proof_stub.mli new file mode 100644 index 00000000..8f223123 --- /dev/null +++ b/src/base/Proof_stub.mli @@ -0,0 +1,20 @@ + +(** Dummy proof module that does nothing. *) + +open Base_types + +include Sidekick_core.PROOF + with type lit = Lit.t + and type term = Term.t + +val lemma_bool_tauto : t -> Lit.t Iter.t -> unit +val lemma_bool_c : t -> string -> term list -> unit +val lemma_bool_equiv : t -> term -> term -> unit +val lemma_ite_true : t -> a:term -> ite:term -> unit +val lemma_ite_false : t -> a:term -> ite:term -> unit + +val lemma_lra : t -> Lit.t Iter.t -> unit + +val lemma_isa_split : t -> Lit.t Iter.t -> unit +val lemma_isa_disj : t -> Lit.t Iter.t -> unit +val lemma_cstor_inj : t -> Lit.t Iter.t -> unit diff --git a/src/base/Sidekick_base.ml b/src/base/Sidekick_base.ml index 29687537..58565d79 100644 --- a/src/base/Sidekick_base.ml +++ b/src/base/Sidekick_base.ml @@ -29,25 +29,11 @@ module Ty = Base_types.Ty module Statement = Base_types.Statement module Data = Base_types.Data module Select = Base_types.Select -module Proof = Proof module Form = Form +module Solver_arg = Solver_arg +module Lit = Lit +module Proof_stub = Proof_stub + (* re-export *) module IArray = IArray - -(** Concrete implementation of {!Sidekick_core.TERM} - - this module gathers most definitions above in a form - that is compatible with what Sidekick expects for terms, functions, etc. -*) -module Arg - : Sidekick_core.TERM - with type Term.t = Term.t - and type Fun.t = Fun.t - and type Ty.t = Ty.t - and type Term.store = Term.store -= struct - module Term = Term - module Fun = Fun - module Ty = Ty -end diff --git a/src/base/Solver_arg.ml b/src/base/Solver_arg.ml new file mode 100644 index 00000000..aa4b120f --- /dev/null +++ b/src/base/Solver_arg.ml @@ -0,0 +1,6 @@ + +open Base_types + +module Term = Term +module Fun = Fun +module Ty = Ty diff --git a/src/base/Solver_arg.mli b/src/base/Solver_arg.mli new file mode 100644 index 00000000..38635928 --- /dev/null +++ b/src/base/Solver_arg.mli @@ -0,0 +1,15 @@ + +(** Concrete implementation of {!Sidekick_core.TERM} + + this module gathers most definitions above in a form + that is compatible with what Sidekick expects for terms, functions, etc. +*) + +open Base_types + +include Sidekick_core.TERM + with type Term.t = Term.t + and type Fun.t = Fun.t + and type Ty.t = Ty.t + and type Term.store = Term.store + and type Ty.store = Ty.store diff --git a/src/base/dune b/src/base/dune index 8fefacc3..691c0e53 100644 --- a/src/base/dune +++ b/src/base/dune @@ -2,7 +2,7 @@ (name sidekick_base) (public_name sidekick-base) (synopsis "Base term definitions for the standalone SMT solver and library") - (libraries containers sidekick.core sidekick.util + (libraries containers sidekick.core sidekick.util sidekick.lit sidekick.arith-lra sidekick.th-bool-static sidekick.zarith zarith) (flags :standard -w -32 -open Sidekick_util)) diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index df32bdc3..c1db9fbe 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -1059,6 +1059,8 @@ module type SOLVER = sig val add_theory_l : t -> theory list -> unit + (* FIXME: do not handle atoms here, only lits *) + val mk_atom_lit : t -> lit -> Atom.t * dproof (** [mk_atom_lit _ lit] returns [atom, pr] where [atom] is an internal atom for the solver, diff --git a/src/lra/sidekick_arith_lra.ml b/src/lra/sidekick_arith_lra.ml index 41ec123e..f31285cf 100644 --- a/src/lra/sidekick_arith_lra.ml +++ b/src/lra/sidekick_arith_lra.ml @@ -60,9 +60,7 @@ module type ARG = sig val has_ty_real : term -> bool (** Does this term have the type [Real] *) - (** TODO: more accurate certificates *) - val proof_lra : S.P.lit Iter.t -> S.P.t - val proof_lra_l : S.P.lit list -> S.P.t + val lemma_lra : S.proof -> S.Lit.t Iter.t -> unit module Gensym : sig type t @@ -235,6 +233,12 @@ module Make(A : ARG) : S with module A = A = struct ); proxy + let add_clause_lra_ ~add_clause lits = + let emit_proof p = + A.lemma_lra p (Iter.of_list lits) + in + add_clause lits emit_proof + (* preprocess linear expressions away *) let preproc_lra (self:state) si ~mk_lit ~add_clause (t:T.t) : (T.t * _) option = @@ -273,10 +277,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 [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 [lit_a t; lit_na u1; lit_na u2]); + add_clause_lra_ ~add_clause [SI.Lit.neg lit_t; lit_u1]; + add_clause_lra_ ~add_clause [SI.Lit.neg lit_t; lit_u2]; + add_clause_lra_ ~add_clause + [SI.Lit.neg lit_u1; SI.Lit.neg lit_u2; lit_t]; ); None @@ -312,8 +316,7 @@ module Make(A : ARG) : S with module A = A = struct Log.debugf 10 (fun k->k "lra.preprocess:@ %a@ :into %a" T.pp t T.pp new_t); (* FIXME: by def proxy + LRA *) - let proof = A.S.P.sorry in - Some (new_t, proof) + Some (new_t, (fun _ -> ())) | Some (coeff, v), pred -> (* [c . v <= const] becomes a direct simplex constraint [v <= const/c] *) @@ -338,8 +341,9 @@ module Make(A : ARG) : S with module A = A = struct end; Log.debugf 10 (fun k->k "lra.preprocess@ :%a@ :into %a" T.pp t T.pp new_t); - let proof = A.S.P.sorry in (* TODO: some sort of equality + def? *) - Some (new_t, proof) + (* FIXME: preprocess proof *) + let emit_proof _ = () in + Some (new_t, emit_proof) end | LRA_op _ | LRA_mult _ -> @@ -352,10 +356,10 @@ module Make(A : ARG) : S with module A = A = struct let proxy = var_encoding_comb self ~pre:"_le" le_comb in declare_term_to_cc proxy; - (* TODO: proof by def of proxy *) - let proof = A.S.P.sorry in + (* FIXME: proof by def of proxy *) + let emit_proof _ = () in - Some (proxy, proof) + Some (proxy, emit_proof) ) else ( (* a bit more complicated: we cannot just define [proxy := le_comb] because of the coefficient. @@ -380,26 +384,27 @@ module Make(A : ARG) : S with module A = A = struct add_clause [ mk_lit (A.mk_lra tst (LRA_simplex_pred (proxy2, Leq, A.Q.neg le_const))) - ] A.S.P.sorry; (* TODO: by-def proxy2 + LRA *) + ] (fun _ -> ()); (* TODO: by-def proxy2 + LRA *) add_clause [ mk_lit (A.mk_lra tst (LRA_simplex_pred (proxy2, Geq, A.Q.neg le_const))) - ] A.S.P.sorry; (* TODO: by-def proxy2 + LRA *) + ] (fun _ -> ()); (* TODO: by-def proxy2 + LRA *) (* FIXME: actual proof *) - let proof = A.S.P.sorry in - Some (proxy, proof) + let emit_proof _ = () in + Some (proxy, emit_proof) ) | LRA_other t when A.has_ty_real t -> None | LRA_const _ | LRA_simplex_pred _ | LRA_simplex_var _ | LRA_other _ -> None - let simplify (self:state) (_recurse:_) (t:T.t) : (T.t * SI.proof) option = + let simplify (self:state) (_recurse:_) (t:T.t) : (T.t * SI.dproof) option = match A.view_as_lra t with | LRA_op _ | LRA_mult _ -> let le = as_linexp_id t in if LE.is_const le then ( let c = LE.const le in - Some (A.mk_lra self.tst (LRA_const c), A.S.P.sorry) + (* FIXME: proof *) + Some (A.mk_lra self.tst (LRA_const c), (fun _ -> ())) ) else None | LRA_pred (pred, l1, l2) -> let le = LE.(as_linexp_id l1 - as_linexp_id l2) in @@ -413,16 +418,13 @@ module Make(A : ARG) : S with module A = A = struct | Eq -> A.Q.(c = zero) | Neq -> A.Q.(c <> zero) in - Some (A.mk_bool self.tst is_true, A.S.P.sorry) + (* FIXME: proof *) + Some (A.mk_bool self.tst is_true, (fun _ -> ())) ) else None | _ -> None module Q_map = CCMap.Make(A.Q) - 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 = Profile.with1 "simplex.check-cert" SimpSolver._check_cert cert; @@ -431,10 +433,8 @@ module Make(A : ARG) : S with module A = A = struct |> CCList.flat_map (Tag.to_lits si) |> List.rev_map SI.Lit.neg in - (* TODO: more detailed proof certificate *) - let pr = - A.(proof_lra (Iter.of_list confl |> Iter.map plit_of_lit)) in - SI.raise_conflict si acts confl pr + let emit_proof p = A.lemma_lra p (Iter.of_list confl) in + SI.raise_conflict si acts confl emit_proof let on_propagate_ si acts lit ~reason = match lit with @@ -443,8 +443,10 @@ module Make(A : ARG) : S with module A = A = struct SI.propagate si acts lit ~reason:(fun() -> let lits = CCList.flat_map (Tag.to_lits si) reason in - let proof = A.proof_lra Iter.(cons lit (of_list lits) |> map plit_of_lit) in - CCList.flat_map (Tag.to_lits si) reason, proof) + let emit_proof p = + A.lemma_lra p Iter.(cons lit (of_list lits)) + in + CCList.flat_map (Tag.to_lits si) reason, emit_proof) | _ -> () let check_simplex_ self si acts : SimpSolver.Subst.t = diff --git a/src/main/main.ml b/src/main/main.ml index 385c9985..bfa298a7 100644 --- a/src/main/main.ml +++ b/src/main/main.ml @@ -19,7 +19,6 @@ exception Out_of_space let file = ref "" let p_cnf = ref false -let p_dot_proof = ref "" let p_proof = ref false let p_model = ref false let check = ref false @@ -32,8 +31,6 @@ let p_gc_stat = ref false let p_progress = ref false let proof_file = ref "" -let hyps : Term.t list ref = ref [] - (* Arguments parsing *) let int_arg r arg = let l = String.length arg in @@ -69,7 +66,6 @@ let argspec = Arg.align [ "--no-gc", Arg.Clear gc, " disable garbage collection"; "--restarts", Arg.Set restarts, " enable restarts"; "--no-restarts", Arg.Clear restarts, " disable restarts"; - "--dot", Arg.Set_string p_dot_proof, " if provided, print the dot proof in the given file"; "--stat", Arg.Set p_stat, " print statistics"; "--proof", Arg.Set p_proof, " print proof"; "--no-proof", Arg.Clear p_proof, " do not print proof"; @@ -97,7 +93,7 @@ let check_limits () = else if s > !size_limit then raise Out_of_space -let main_smt ~dot_proof () : _ result = +let main_smt () : _ result = let tst = Term.create ~size:4_096 () in let solver = let theories = @@ -123,13 +119,12 @@ let main_smt ~dot_proof () : _ result = (* process statements *) let res = try - let hyps = Vec.create() in E.fold_l (fun () -> Process.process_stmt - ~hyps ~gc:!gc ~restarts:!restarts ~pp_cnf:!p_cnf ?proof_file + ~gc:!gc ~restarts:!restarts ~pp_cnf:!p_cnf ?proof_file ~time:!time_limit ~memory:!size_limit - ?dot_proof ~pp_model:!p_model + ~pp_model:!p_model ~check:!check ~progress:!p_progress solver) () input @@ -203,8 +198,6 @@ let main () = Arg.usage argspec usage; exit 2 ); - let dot_proof = if !p_dot_proof = "" then None else Some !p_dot_proof in - check := !check || CCOpt.is_some dot_proof; (* dot requires a proof *) let al = Gc.create_alarm check_limits in Util.setup_gc(); let is_cnf = Filename.check_suffix !file ".cnf" in @@ -212,7 +205,7 @@ let main () = if is_cnf then ( main_cnf () ) else ( - main_smt ~dot_proof () + main_smt () ) in if !p_gc_stat then ( diff --git a/src/main/pure_sat_solver.ml b/src/main/pure_sat_solver.ml index 53d53518..8846b594 100644 --- a/src/main/pure_sat_solver.ml +++ b/src/main/pure_sat_solver.ml @@ -4,18 +4,73 @@ module E = CCResult module SS = Sidekick_sat +module Formula = struct + type t = int + let norm t = if t>0 then t, SS.Same_sign else -t, SS.Negated + let abs = abs + let sign t = t>0 + let equal = CCInt.equal + let hash = CCHash.int + let neg x = -x + let pp = Fmt.int +end + +module Proof + : Sidekick_sat.PROOF with type lit = Formula.t += struct + let bpf = Printf.bprintf + type lit = Formula.t + type t = + | Dummy + | Inner of { + buf: Buffer.t; + } + type dproof = t -> unit + + let[@inline] enabled = function + | Dummy -> false + | Inner _ -> true + + let emit_lits_ buf lits = + lits (fun i -> bpf buf "%d " i) + + let emit_input_clause self lits = + match self with + | Dummy -> () + | Inner {buf} -> + bpf buf "i "; emit_lits_ buf lits; bpf buf "0\n" + + let emit_redundant_clause self lits = + match self with + | Dummy -> () + | Inner {buf} -> + bpf buf "r "; emit_lits_ buf lits; bpf buf "0\n" + + let del_clause self lits = + match self with + | Dummy -> () + | Inner {buf} -> + bpf buf "d "; emit_lits_ buf lits; bpf buf "0\n" + + (* lifetime *) + + let dummy : t = Dummy + let create () : t = Inner {buf=Buffer.create 1_024} + + let to_string = function + | Dummy -> "" + | Inner {buf} -> Buffer.contents buf + + let to_chan oc = function + | Dummy -> () + | Inner {buf} -> Buffer.output_buffer oc buf; flush oc +end + module Arg = struct - module Formula = struct - type t = int - let norm t = if t>0 then t, SS.Same_sign else -t, SS.Negated - let abs = abs - let sign t = t>0 - let equal = CCInt.equal - let hash = CCHash.int - let neg x = -x - let pp = Fmt.int - end - type proof=unit + module Formula = Formula + type formula = Formula.t + module Proof = Proof + type proof = Proof.t end module SAT = Sidekick_sat.Make_pure_sat(Arg) @@ -35,7 +90,7 @@ module Dimacs = struct BL.Dimacs_parser.iter p (fun c -> let atoms = List.rev_map get_lit c in - SAT.add_clause solver atoms ()); + SAT.add_input_clause solver atoms); Ok ()) with e -> E.of_exn_trace e @@ -54,8 +109,8 @@ let solve ?(check=false) (solver:SAT.t) : (unit, string) result = | SAT.Unsat (module US) -> if check then ( - let pr = US.get_proof() in - SAT.Proof.check (SAT.store solver) pr; + let proof = SAT.proof solver in + Proof.check proof; ); let t3 = Sys.time () -. t2 in diff --git a/src/mini-cc/tests/sidekick_test_minicc.ml b/src/mini-cc/tests/sidekick_test_minicc.ml index 8671d1a1..f8bff6b9 100644 --- a/src/mini-cc/tests/sidekick_test_minicc.ml +++ b/src/mini-cc/tests/sidekick_test_minicc.ml @@ -2,7 +2,7 @@ open Sidekick_base module A = Alcotest module CC = Sidekick_mini_cc.Make(struct - module T = Sidekick_base.Arg + module T = Sidekick_base.Solver_arg let cc_view = Term.cc_view end) diff --git a/src/base/Proof.ml b/src/proof/Proof.ml similarity index 99% rename from src/base/Proof.ml rename to src/proof/Proof.ml index 4b682635..e5d47f0a 100644 --- a/src/base/Proof.ml +++ b/src/proof/Proof.ml @@ -1,4 +1,5 @@ +(* open Base_types module T = Term @@ -532,3 +533,4 @@ let pp_debug ~sharing out p = in let module M = Quip.Make(Out) in M.pp_debug ~sharing p out + *) diff --git a/src/base/Proof.mli b/src/proof/Proof.mli similarity index 98% rename from src/base/Proof.mli rename to src/proof/Proof.mli index 2cf5fe41..c7456fdf 100644 --- a/src/base/Proof.mli +++ b/src/proof/Proof.mli @@ -1,3 +1,5 @@ + +(* (** Proofs of unsatisfiability Proofs are used in sidekick when the problem is found {b unsatisfiable}. @@ -26,3 +28,4 @@ val ite_false : term -> t val lra : lit Iter.t -> t val lra_l : lit list -> t + *) diff --git a/src/sat/Solver.ml b/src/sat/Solver.ml index abe763f4..de6aec7d 100644 --- a/src/sat/Solver.ml +++ b/src/sat/Solver.ml @@ -1901,6 +1901,21 @@ module Make(Plugin : PLUGIN) | E_unsat (US_false c) -> self.unsat_at_0 <- Some c + (* FIXME: take lits, not atoms *) + let add_input_clause self c = + let emit_proof p = + let lits = Iter.of_list c |> Iter.map (Atom.formula (store self)) in + Proof.emit_input_clause p lits + in + add_clause self c emit_proof + + let add_input_clause_a self c = + let emit_proof p = + let lits = Iter.of_array c |> Iter.map (Atom.formula (store self)) in + Proof.emit_input_clause p lits + in + add_clause_a self c emit_proof + let solve ?(assumptions=[]) (st:t) : res = cancel_until st 0; Vec.clear st.assumptions; diff --git a/src/sat/Solver_intf.ml b/src/sat/Solver_intf.ml index f7363669..7cc51199 100644 --- a/src/sat/Solver_intf.ml +++ b/src/sat/Solver_intf.ml @@ -312,16 +312,24 @@ module type S = sig (** {2 Base operations} *) - val assume : t -> formula list list -> dproof -> unit + val assume : t -> formula list list -> unit (** Add the list of clauses to the current set of assumptions. Modifies the sat solver state in place. *) val add_clause : t -> atom list -> dproof -> unit (** Lower level addition of clauses *) + val add_input_clause : t -> atom list -> unit + (** Like {!add_clause} but with the justification of being an input clause *) + val add_clause_a : t -> atom array -> dproof -> unit (** Lower level addition of clauses *) + val add_input_clause_a : t -> atom array -> unit + (** Like {!add_clause_a} but with justification of being an input clause *) + + (* TODO: API to push/pop/clear assumptions from an inner vector *) + val solve : ?assumptions:atom list -> t -> res diff --git a/src/smt-solver/Sidekick_smt_solver.ml b/src/smt-solver/Sidekick_smt_solver.ml index a53d5a58..329dd55a 100644 --- a/src/smt-solver/Sidekick_smt_solver.ml +++ b/src/smt-solver/Sidekick_smt_solver.ml @@ -577,9 +577,9 @@ module Make(A : ARG) begin let tst = Solver_internal.tst self.si in let t_true = Term.bool tst true in - Sat_solver.assume self.solver [ - [Lit.atom tst t_true]; - ] (fun p -> P.lemma_true p t_true) + Sat_solver.add_clause self.solver + [Lit.atom tst t_true] + (fun p -> P.lemma_true p t_true) end; self diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index c8eaf058..ccf8da18 100644 --- a/src/smtlib/Process.ml +++ b/src/smtlib/Process.ml @@ -135,12 +135,10 @@ let mk_progress (_s:Solver.t) : _ -> unit = let solve ?gc:_ ?restarts:_ - ?dot_proof ?(pp_model=false) ?proof_file ?(check=false) ?time:_ ?memory:_ ?(progress=false) - ?hyps:_ ~assumptions s : unit = let t1 = Sys.time() in @@ -168,32 +166,19 @@ let solve *) let t3 = Sys.time () -. t2 in Format.printf "Sat (%.3f/%.3f/%.3f)@." t1 (t2-.t1) t3; - | Solver.Unsat {proof;_} -> - - let proof_opt = - if check||CCOpt.is_some proof_file then Lazy.force proof - else None - in + | Solver.Unsat _ -> if check then ( + () + (* FIXME: check trace? match proof_opt with | Some p -> Profile.with_ "unsat.check" (fun () -> Solver.Pre_proof.check p); | _ -> () + *) ); - begin match dot_proof, proof, Solver.Pre_proof.pp_dot with - | Some file, lazy (Some p), Some pp_dot -> - Profile.with_ "dot.proof" @@ fun () -> - CCIO.with_out file - (fun oc -> - Log.debugf 1 (fun k->k "write proof into `%s`" file); - let fmt = Format.formatter_of_out_channel oc in - pp_dot fmt p; - Format.pp_print_flush fmt (); flush oc) - | _ -> () - end; - + (* FIXME: instead, create a proof if proof file or --check is given begin match proof_file, proof with | Some file, lazy (Some p) -> Profile.with_ "proof.write-file" @@ fun () -> @@ -202,6 +187,7 @@ let solve (fun oc -> Proof.Quip.output oc p; flush oc) | _ -> () end; + *) let t3 = Sys.time () -. t2 in Format.printf "Unsat (%.3f/%.3f/%.3f)@." t1 (t2-.t1) t3; @@ -212,9 +198,8 @@ let solve (* process a single statement *) let process_stmt - ?hyps ?gc ?restarts ?(pp_cnf=false) - ?dot_proof ?proof_file ?pp_model ?(check=false) + ?proof_file ?pp_model ?(check=false) ?time ?memory ?progress (solver:Solver.t) (stmt:Statement.t) : unit or_error = @@ -230,6 +215,9 @@ let process_stmt ID.pp id (Util.pp_list Ty.pp) args Ty.pp ret); (* TODO: more? *) in + + let mk_lit ?sign t = Solver.Lit.atom (Solver.tst solver) ?sign t in + begin match stmt with | Statement.Stmt_set_logic ("QF_UF"|"QF_LRA"|"QF_UFLRA"|"QF_DT"|"QF_UFDT") -> E.return () @@ -253,9 +241,9 @@ let process_stmt l in solve - ?gc ?restarts ?dot_proof ~check ?proof_file ?pp_model + ?gc ?restarts ~check ?proof_file ?pp_model ?time ?memory ?progress - ~assumptions ?hyps + ~assumptions solver; E.return() | Statement.Stmt_ty_decl (id,n) -> @@ -270,9 +258,8 @@ let process_stmt Format.printf "(@[assert@ %a@])@." Term.pp t ); 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.(hres_l (assertion t) [p1 pr_atom]); + (fun p -> Solver.P.emit_input_clause p (Iter.singleton (mk_lit t))); E.return() | Statement.Stmt_assert_clause c_ts -> @@ -284,19 +271,22 @@ let process_stmt 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; + pr_l := pr :: !pr_l; a) c_ts in - CCOpt.iter (fun h -> Vec.push h c) hyps; - 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) + (* proof of assert-input + preprocessing *) + let emit_proof p = + let module P = Solver.P in + P.begin_subproof p; + P.emit_input_clause p (Iter.of_list c_ts |> Iter.map mk_lit); + List.iter (fun dp -> dp p) !pr_l; + P.emit_redundant_clause p + (Iter.of_list c |> Iter.map (Solver.Atom.formula solver)); + P.end_subproof p; in - Solver.add_clause solver (IArray.of_list c) proof ; + Solver.add_clause solver (IArray.of_list c) emit_proof; E.return() | Statement.Stmt_data _ -> diff --git a/src/smtlib/Process.mli b/src/smtlib/Process.mli index cc95f8d7..1e5d1104 100644 --- a/src/smtlib/Process.mli +++ b/src/smtlib/Process.mli @@ -3,7 +3,7 @@ open Sidekick_base module Solver - : Sidekick_msat_solver.S with type T.Term.t = Term.t + : Sidekick_smt_solver.S with type T.Term.t = Term.t and type T.Term.store = Term.store and type T.Ty.t = Ty.t and type T.Ty.store = Ty.store @@ -20,11 +20,9 @@ module Check_cc : sig end val process_stmt : - ?hyps:Solver.Atom.t list Vec.t -> ?gc:bool -> ?restarts:bool -> ?pp_cnf:bool -> - ?dot_proof:string -> ?proof_file:string -> ?pp_model:bool -> ?check:bool -> diff --git a/src/th-cstor/Sidekick_th_cstor.ml b/src/th-cstor/Sidekick_th_cstor.ml index 9bfb0fec..993ce743 100644 --- a/src/th-cstor/Sidekick_th_cstor.ml +++ b/src/th-cstor/Sidekick_th_cstor.ml @@ -9,7 +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 + val lemma_cstor : S.proof -> S.Lit.t Iter.t -> unit end module type S = sig @@ -53,6 +53,9 @@ module Make(A : ARG) : S with module A = A = struct (fun k->k "(@[%s.merge@ @[:c1 %a (t %a)@]@ @[:c2 %a (t %a)@]@])" name N.pp n1 T.pp v1.t N.pp n2 T.pp v2.t); (* build full explanation of why the constructor terms are equal *) + (* FIXME: add a (fun p -> A.lemma_cstor p …) here. + probably we need [Some a=Some b => a=b] as a lemma for inj, + and [Some a /= None] for Error case. *) let expl = Expl.mk_list [ e_n1_n2; diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml index 8cc873d3..9a1f4521 100644 --- a/src/th-data/Sidekick_th_data.ml +++ b/src/th-data/Sidekick_th_data.ml @@ -74,9 +74,9 @@ module type ARG = sig val ty_is_finite : S.T.Ty.t -> bool val ty_set_is_finite : S.T.Ty.t -> bool -> unit - val proof_isa_split : S.T.Ty.t -> S.T.Term.t Iter.t -> S.P.t - val proof_isa_disj : S.T.Ty.t -> S.T.Term.t -> S.T.Term.t -> S.P.t - val proof_cstor_inj : Cstor.t -> int -> S.T.Term.t list -> S.T.Term.t list -> S.P.t + val lemma_isa_split : S.proof -> S.Lit.t Iter.t -> unit + val lemma_isa_disj : S.proof -> S.Lit.t Iter.t -> unit + val lemma_cstor_inj : S.proof -> S.Lit.t Iter.t -> unit end (** Helper to compute the cardinality of types *) @@ -574,12 +574,13 @@ module Make(A : ARG) : S with module A = A = struct |> Iter.to_rev_list in SI.add_clause_permanent solver acts c - (A.proof_isa_split (T.ty t) @@ (Iter.of_list c|>Iter.map SI.Lit.term)); + (fun p -> A.lemma_isa_split p (Iter.of_list c)); Iter.diagonal_l c (fun (c1,c2) -> - let proof = A.proof_isa_disj (T.ty t) (SI.Lit.term c1) (SI.Lit.term c2) in + let emit_proof p = + A.lemma_isa_disj p (Iter.of_list [SI.Lit.neg c1; SI.Lit.neg c2]) in SI.add_clause_permanent solver acts - [SI.Lit.neg c1; SI.Lit.neg c2] proof); + [SI.Lit.neg c1; SI.Lit.neg c2] emit_proof); ) (* on final check, check acyclicity, diff --git a/src/th-data/Sidekick_th_data.mli b/src/th-data/Sidekick_th_data.mli index 60a78e2f..2a4b62f3 100644 --- a/src/th-data/Sidekick_th_data.mli +++ b/src/th-data/Sidekick_th_data.mli @@ -30,11 +30,11 @@ type ('c, 'ty) data_ty_view = module type ARG = sig module S : Sidekick_core.SOLVER -(** Constructor symbols. + (** Constructor symbols. - A constructor is an injective symbol, part of a datatype (or "sum type"). - For example, in [type option a = Some a | None], - the constructors are [Some] and [None]. *) + A constructor is an injective symbol, part of a datatype (or "sum type"). + For example, in [type option a = Some a | None], + the constructors are [Some] and [None]. *) module Cstor : sig type t (** Constructor *) @@ -74,9 +74,9 @@ module type ARG = sig (* TODO: should we store this ourself? would be simpler… *) - val proof_isa_split : S.T.Ty.t -> S.T.Term.t Iter.t -> S.P.t - val proof_isa_disj : S.T.Ty.t -> S.T.Term.t -> S.T.Term.t -> S.P.t - val proof_cstor_inj : Cstor.t -> int -> S.T.Term.t list -> S.T.Term.t list -> S.P.t + val lemma_isa_split : S.proof -> S.Lit.t Iter.t -> unit + val lemma_isa_disj : S.proof -> S.Lit.t Iter.t -> unit + val lemma_cstor_inj : S.proof -> S.Lit.t Iter.t -> unit end module type S = sig