From bbb995b0d54131437ee4b3e38ec15250d1af5123 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 3 Oct 2021 20:32:37 -0400 Subject: [PATCH] refactor some names related to proofs; wip add unit paramod --- src/cc/Sidekick_cc.ml | 6 +- src/cc/Sidekick_cc.mli | 2 +- src/checker/drup_check.ml | 4 +- src/core/Sidekick_core.ml | 135 ++++++++++-------- src/drup/sidekick_drup.ml | 2 +- src/lra/simplex2.ml | 2 +- src/lra/tests/test_simplex2.real.ml | 8 +- src/proof/Proof.ml | 22 +-- src/sat/Solver.ml | 80 +++++------ src/sat/Solver_intf.ml | 34 ++--- src/smt-solver/Sidekick_smt_solver.ml | 23 +-- src/th-bool-static/Sidekick_th_bool_static.ml | 95 ++++++------ 12 files changed, 219 insertions(+), 194 deletions(-) diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml index 8d9caf41..1b0c853e 100644 --- a/src/cc/Sidekick_cc.ml +++ b/src/cc/Sidekick_cc.ml @@ -16,7 +16,7 @@ module Make (A: CC_ARG) : S with module T = A.T and module Lit = A.Lit and type proof = A.proof - and type step_id = A.step_id + and type proof_step = A.proof_step and module Actions = A.Actions = struct module T = A.T @@ -28,8 +28,8 @@ module Make (A: CC_ARG) type lit = Lit.t type fun_ = T.Fun.t type proof = A.proof - type step_id = A.step_id - type pstep = proof -> step_id + type proof_step = A.proof_step + type proof_rule = proof -> proof_step type actions = Actions.t module Term = T.Term diff --git a/src/cc/Sidekick_cc.mli b/src/cc/Sidekick_cc.mli index 2d0bb9f8..c73d5c05 100644 --- a/src/cc/Sidekick_cc.mli +++ b/src/cc/Sidekick_cc.mli @@ -7,5 +7,5 @@ module Make (A: CC_ARG) : S with module T = A.T and module Lit = A.Lit and type proof = A.proof - and type step_id = A.step_id + and type proof_step = A.proof_step and module Actions = A.Actions diff --git a/src/checker/drup_check.ml b/src/checker/drup_check.ml index 8771b768..f0895514 100644 --- a/src/checker/drup_check.ml +++ b/src/checker/drup_check.ml @@ -137,7 +137,7 @@ end = struct let ok = check_op self i op in if ok then ( Log.debugf 50 - (fun k->k"(@[check.step.ok@ :idx %d@ :op %a@])" i Trace.pp_op op); + (fun k->k"(@[check.proof_rule.ok@ :idx %d@ :op %a@])" i Trace.pp_op op); (* check if op adds the empty clause *) begin match op with @@ -147,7 +147,7 @@ end = struct end; ) else ( Log.debugf 10 - (fun k->k"(@[check.step.fail@ :idx %d@ :op %a@])" i Trace.pp_op op); + (fun k->k"(@[check.proof_rule.fail@ :idx %d@ :op %a@])" i Trace.pp_op op); VecI32.push self.errors i )); diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index 8c3966bd..e009e342 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -147,11 +147,11 @@ end (** Proofs for the congruence closure *) module type CC_PROOF = sig - type step_id + type proof_step type t type lit - val lemma_cc : lit Iter.t -> t -> step_id + val lemma_cc : lit Iter.t -> t -> proof_step (** [lemma_cc proof lits] asserts that [lits] form a tautology for the theory of uninterpreted functions. *) end @@ -161,17 +161,17 @@ module type SAT_PROOF = sig type t (** The stored proof (possibly nil, possibly on disk, possibly in memory) *) - type step_id - (** identifier for a proof step *) + type proof_step + (** identifier for a proof proof_rule *) - module Step_vec : Vec_sig.S with type elt = step_id + module Step_vec : Vec_sig.S with type elt = proof_step (** A vector of steps *) type lit (** A boolean literal for the proof trace *) - type pstep = t -> step_id - (** A proof step constructor, used to obtain proofs from theories *) + type proof_rule = t -> proof_step + (** A proof proof_rule constructor, used to obtain proofs from theories *) val enabled : t -> bool (** Returns true if proof production is enabled *) @@ -179,23 +179,23 @@ module type SAT_PROOF = sig val with_proof : t -> (t -> 'a) -> 'a (** If proof is enabled, call [f] on it to emit steps. if proof is disabled, the callback won't even be called, and - a dummy step is returned. *) + a dummy proof_rule is returned. *) - val emit_input_clause : lit Iter.t -> pstep + val emit_input_clause : lit Iter.t -> proof_rule (** Emit an input clause. *) - val emit_redundant_clause : lit Iter.t -> hyps:step_id Iter.t -> pstep + val emit_redundant_clause : lit Iter.t -> hyps:proof_step Iter.t -> proof_rule (** Emit a clause deduced by the SAT solver, redundant wrt previous clauses. The clause must be RUP wrt [hyps]. *) - val emit_unsat_core : lit Iter.t -> pstep + val emit_unsat_core : lit Iter.t -> proof_rule (** Produce a proof of the empty clause given this subset of the assumptions. - FIXME: probably needs the list of step_id that disprove the lits? *) + FIXME: probably needs the list of proof_step that disprove the lits? *) - val emit_unsat : step_id -> t -> unit - (** Signal "unsat" result at the given step *) + val emit_unsat : proof_step -> t -> unit + (** Signal "unsat" result at the given proof_rule *) - val del_clause : step_id -> t -> unit + val del_clause : proof_step -> t -> unit (** Forget a clause. Only useful for performance considerations. *) end @@ -206,33 +206,39 @@ module type PROOF = sig a clause to be {b valid} (true in every possible interpretation of the problem's assertions, and the theories) *) - type step_id - (** Identifier for a proof step (like a unique ID for a clause previously + type proof_step + (** Identifier for a proof proof_rule (like a unique ID for a clause previously added/proved) *) type term type lit - type step = t -> step_id + type proof_rule = t -> proof_step include CC_PROOF with type t := t and type lit := lit - and type step_id := step_id + and type proof_step := proof_step include SAT_PROOF with type t := t and type lit := lit - and type step_id := step_id + and type proof_step := proof_step + and type proof_rule := proof_rule - val define_term : term -> term -> step + val define_term : term -> term -> proof_rule (** [define_term cst u proof] defines the new constant [cst] as being equal to [u]. The result is a proof of the clause [cst = u] *) - val lemma_true : term -> step + val proof_p1 : proof_step -> proof_step -> proof_rule + (** [proof_p1 p1 p2], where [p1] proves the unit clause [t=u] (t:bool) + and [p2] proves [C \/ t], is the rule that produces [C \/ u], + i.e unit paramodulation. *) + + val lemma_true : term -> proof_rule (** [lemma_true (true) p] asserts the clause [(true)] *) - val lemma_preprocess : term -> term -> using:step_id Iter.t -> step + val lemma_preprocess : term -> term -> using:proof_step Iter.t -> proof_rule (** [lemma_preprocess t u ~using p] asserts that [t = u] is a tautology and that [t] has been preprocessed into [u]. @@ -241,7 +247,7 @@ module type PROOF = sig a unit equality. From now on, [t] and [u] will be used interchangeably. - @return a step ID for the clause [(t=u)]. *) + @return a proof_rule ID for the clause [(t=u)]. *) end (** Literals @@ -300,8 +306,8 @@ module type CC_ACTIONS = sig module Lit : LIT with module T = T type proof - type step_id - type pstep = proof -> step_id + type proof_step + type proof_rule = proof -> proof_step module P : CC_PROOF with type lit = Lit.t and type t = proof type t @@ -309,13 +315,13 @@ module type CC_ACTIONS = sig to perform the actions below. How it performs the actions is not specified and is solver-specific. *) - val raise_conflict : t -> Lit.t list -> pstep -> 'a + val raise_conflict : t -> Lit.t list -> proof_rule -> '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 * pstep) -> unit + val propagate : t -> Lit.t -> reason:(unit -> Lit.t list * proof_rule) -> unit (** [propagate acts lit ~reason pr] declares that [reason() => lit] is a tautology. @@ -331,16 +337,16 @@ module type CC_ARG = sig module T : TERM module Lit : LIT with module T = T type proof - type step_id + type proof_step module P : CC_PROOF with type lit = Lit.t and type t = proof - and type step_id = step_id + and type proof_step = proof_step module Actions : CC_ACTIONS with module T=T and module Lit = Lit and type proof = proof - and type step_id = step_id + and type proof_step = proof_step 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 *) @@ -368,17 +374,17 @@ module type CC_S = sig module T : TERM module Lit : LIT with module T = T type proof - type step_id - type pstep = proof -> step_id + type proof_step + type proof_rule = proof -> proof_step module P : CC_PROOF with type lit = Lit.t and type t = proof - and type step_id = step_id + and type proof_step = proof_step module Actions : CC_ACTIONS with module T = T and module Lit = Lit and type proof = proof - and type step_id = step_id + and type proof_step = proof_step type term_store = T.Term.store type term = T.Term.t type fun_ = T.Fun.t @@ -519,7 +525,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 * pstep) -> unit + type ev_on_propagate = t -> lit -> (unit -> lit list * proof_rule) -> unit (** [ev_on_propagate cc lit reason] is called whenever [reason() => lit] is a propagated lemma. See {!CC_ACTIONS.propagate}. *) @@ -673,12 +679,16 @@ module type SOLVER_INTERNAL = sig type ty_store = T.Ty.store type clause_pool type proof - type step_id - type pstep = proof -> step_id - (** Delayed proof. This is used to build a proof step on demand. *) + type proof_step + type proof_rule = proof -> proof_step + (** Delayed proof. This is used to build a proof proof_rule on demand. *) (** {3 Proofs} *) - module P : PROOF with type lit = Lit.t and type term = term and type t = proof + module P : PROOF + with type lit = Lit.t + and type term = term + and type t = proof + and type proof_step = proof_step (** {3 Main type for a solver} *) type t @@ -730,24 +740,24 @@ module type SOLVER_INTERNAL = sig val clear : t -> unit (** Reset internal cache, etc. *) - val with_proof : t -> (proof -> unit) -> unit + val with_proof : t -> (proof -> 'a) -> 'a - type hook = t -> term -> term option + type hook = t -> term -> (term * proof_step Iter.t) option (** Given a term, try to simplify it. Return [None] if it didn't change. A simple example could be a hook that takes a term [t], and if [t] is [app "+" (const x) (const y)] where [x] and [y] are number, returns [Some (const (x+y))], and [None] otherwise. *) - val normalize : t -> term -> term option + val normalize : t -> term -> (term * proof_step Iter.t) option (** Normalize a term using all the hooks. This performs a fixpoint, i.e. it only stops when no hook applies anywhere inside the term. *) - val normalize_t : t -> term -> term + val normalize_t : t -> term -> term * proof_step Iter.t (** Normalize a term using all the hooks, along with a proof that the simplification is correct. - returns [t, refl t] if no simplification occurred. *) + returns [t, ø] if no simplification occurred. *) end type simplify_hook = Simplify.hook @@ -755,13 +765,11 @@ module type SOLVER_INTERNAL = sig val add_simplifier : t -> Simplify.hook -> unit (** Add a simplifier hook for preprocessing. *) - val simplifier : t -> Simplify.t - - val simplify_t : t -> term -> term option + val simplify_t : t -> term -> (term * proof_step) option (** Simplify input term, returns [Some u] if some simplification occurred. *) - val simp_t : t -> term -> term + val simp_t : t -> term -> term * proof_step option (** [simp_t si t] returns [u] even if no simplification occurred (in which case [t == u] syntactically). It emits [|- t=u]. @@ -776,7 +784,7 @@ module type SOLVER_INTERNAL = sig val mk_lit : ?sign:bool -> term -> lit (** creates a new literal for a boolean term. *) - val add_clause : lit list -> pstep -> unit + val add_clause : lit list -> proof_rule -> unit (** pushes a new clause into the SAT solver. *) val add_lit : ?default_pol:bool -> lit -> unit @@ -789,7 +797,7 @@ module type SOLVER_INTERNAL = sig type preprocess_hook = t -> preprocess_actions -> - term -> term option + term -> (term * proof_step Iter.t) option (** Given a term, try to preprocess it. Return [None] if it didn't change, or [Some (u)] if [t=u]. Can also add clauses to define new terms. @@ -809,7 +817,7 @@ module type SOLVER_INTERNAL = sig (** {3 hooks for the theory} *) - val raise_conflict : t -> theory_actions -> lit list -> pstep -> 'a + val raise_conflict : t -> theory_actions -> lit list -> proof_rule -> 'a (** Give a conflict clause to the solver *) val push_decision : t -> theory_actions -> lit -> unit @@ -818,19 +826,19 @@ module type SOLVER_INTERNAL = sig If the SAT solver backtracks, this (potential) decision is removed and forgotten. *) - val propagate: t -> theory_actions -> lit -> reason:(unit -> lit list * pstep) -> unit + val propagate: t -> theory_actions -> lit -> reason:(unit -> lit list * proof_rule) -> unit (** Propagate a boolean using a unit clause. [expl => lit] must be a theory lemma, that is, a T-tautology *) - val propagate_l: t -> theory_actions -> lit -> lit list -> pstep -> unit + val propagate_l: t -> theory_actions -> lit -> lit list -> proof_rule -> unit (** Propagate a boolean using a unit clause. [expl => lit] must be a theory lemma, that is, a T-tautology *) - val add_clause_temp : t -> theory_actions -> lit list -> pstep -> unit + val add_clause_temp : t -> theory_actions -> lit list -> proof_rule -> unit (** Add local clause to the SAT solver. This clause will be removed when the solver backtracks. *) - val add_clause_permanent : t -> theory_actions -> lit list -> pstep -> unit + val add_clause_permanent : t -> theory_actions -> lit list -> proof_rule -> unit (** Add toplevel clause to the SAT solver. This clause will not be backtracked. *) @@ -894,7 +902,7 @@ module type SOLVER_INTERNAL = sig val on_cc_conflict : t -> (CC.t -> th:bool -> lit list -> unit) -> unit (** Callback called on every CC conflict *) - val on_cc_propagate : t -> (CC.t -> lit -> (unit -> lit list * pstep) -> unit) -> unit + val on_cc_propagate : t -> (CC.t -> lit -> (unit -> lit list * proof_rule) -> unit) -> unit (** Callback called on every CC propagation *) val on_partial_check : t -> (t -> theory_actions -> lit Iter.t -> unit) -> unit @@ -941,11 +949,11 @@ module type SOLVER = sig module T : TERM module Lit : LIT with module T = T type proof - type step_id + type proof_step module P : PROOF with type lit = Lit.t and type t = proof - and type step_id = step_id + and type proof_step = proof_step and type term = T.Term.t module Solver_internal @@ -953,6 +961,7 @@ module type SOLVER = sig with module T = T and module Lit = Lit and type proof = proof + and type proof_step = proof_step and module P = P (** Internal solver, available to theories. *) @@ -963,8 +972,8 @@ module type SOLVER = sig type term = T.Term.t type ty = T.Ty.t type lit = Lit.t - type pstep = proof -> step_id - (** Proof step. *) + type proof_rule = proof -> proof_step + (** Proof proof_rule. *) (** {3 A theory} @@ -1099,11 +1108,11 @@ module type SOLVER = sig The proof of [|- lit = lit'] is directly added to the solver's proof. *) - val add_clause : t -> lit IArray.t -> pstep -> unit + val add_clause : t -> lit IArray.t -> proof_rule -> 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 -> lit list -> pstep -> unit + val add_clause_l : t -> lit list -> proof_rule -> unit (** Add a clause to the solver, given as a list. *) val assert_terms : t -> term list -> unit diff --git a/src/drup/sidekick_drup.ml b/src/drup/sidekick_drup.ml index 70e47de8..db2dc8ac 100644 --- a/src/drup/sidekick_drup.ml +++ b/src/drup/sidekick_drup.ml @@ -1,7 +1,7 @@ (** DRUP trace checker. - This module provides a checker for DRUP traces, including step-by-step + This module provides a checker for DRUP traces, including proof_rule-by-proof_rule checking for traces that interleave DRUP steps with other kinds of steps. *) diff --git a/src/lra/simplex2.ml b/src/lra/simplex2.ml index fd37b866..2b49b109 100644 --- a/src/lra/simplex2.ml +++ b/src/lra/simplex2.ml @@ -138,7 +138,7 @@ end (* TODO(optim): page 14, paragraph 2: we could detect which variables occur in no atom after preprocessing; then these variables can be "inlined" (removed - by Gaussian elimination) as a preprocessing step, and this removes one column + by Gaussian elimination) as a preprocessing proof_rule, and this removes one column and maybe one row if it was basic. *) module Make(Q : RATIONAL)(Var: VAR) diff --git a/src/lra/tests/test_simplex2.real.ml b/src/lra/tests/test_simplex2.real.ml index 65d1bf5f..fad21c04 100644 --- a/src/lra/tests/test_simplex2.real.ml +++ b/src/lra/tests/test_simplex2.real.ml @@ -98,7 +98,7 @@ module Step = struct let rec aux n vars acc = if n<=0 then return (List.rev acc) else ( - let* vars, step = + let* vars, proof_rule = frequency @@ List.flatten [ (* add a bound *) (match vars with @@ -138,7 +138,7 @@ module Step = struct ) else []); ] in - aux (n-1) vars (step::acc) + aux (n-1) vars (proof_rule::acc) ) in aux n [] [] @@ -162,7 +162,7 @@ end let on_propagate _ ~reason:_ = () -(* add a single step to the simplexe *) +(* add a single proof_rule to the simplexe *) let add_step simplex (s:Step.t) : unit = begin match s with | Step.S_new_var v -> Spl.add_var simplex v @@ -242,7 +242,7 @@ let prop_sound ?(inv=false) pb = let v_x = get_val x in if Q.(v_x < n) then failwith (spf "val=%s, n=%s"(q_dbg v_x)(q_dbg n)) with e -> - QC.Test.fail_reportf "step failed: %a@.exn:@.%s@." + QC.Test.fail_reportf "proof_rule failed: %a@.exn:@.%s@." Step.pp_ s (Printexc.to_string e) ); if inv then Spl._check_invariants simplex; diff --git a/src/proof/Proof.ml b/src/proof/Proof.ml index e5d47f0a..f95972ce 100644 --- a/src/proof/Proof.ml +++ b/src/proof/Proof.ml @@ -59,7 +59,7 @@ type t = | Composite of { (* some named (atomic) assumptions *) assumptions: (string * lit) list; - steps: composite_step array; (* last step is the proof *) + steps: composite_step array; (* last proof_rule is the proof *) } and bool_c_name = string @@ -75,7 +75,7 @@ and composite_step = (* TODO: be able to name clauses, to be expanded at parsing. note that this is not the same as [S_step_c] which defines an - explicit step with a conclusion and proofs that can be exploited + explicit proof_rule with a conclusion and proofs that can be exploited separately. We could introduce that in Compress.rename… @@ -192,7 +192,7 @@ module Compress = struct type 'a shared_status = | First (* first occurrence of t *) | Shared (* multiple occurrences observed *) - | Pre_named of 'a (* another step names it *) + | Pre_named of 'a (* another proof_rule names it *) | Named of 'a (* already named it *) (* is [t] too small to be shared? *) @@ -301,15 +301,15 @@ module Compress = struct | _ -> ()) in - (* introduce naming in [step], then push it into {!new_steps} *) - let process_step_ step = - traverse_step_ step ~f_t:traverse_t; - (* see if we print the step or skip it *) - begin match step with + (* introduce naming in [proof_rule], then push it into {!new_steps} *) + let process_step_ proof_rule = + traverse_step_ proof_rule ~f_t:traverse_t; + (* see if we print the proof_rule or skip it *) + begin match proof_rule with | S_define_t (t,_) when T.Tbl.mem skip_name_t t -> () | S_define_t_name (s,_) when Hashtbl.mem skip_name_s s -> () | _ -> - Vec.push new_steps step; + Vec.push new_steps proof_rule; end in @@ -426,10 +426,10 @@ module Quip = struct l[a"steps";l(List.map pp_ass assumptions); iter_toplist (pp_composite_step sharing) (Iter.of_array steps)] - and pp_composite_step sharing step : printer = + and pp_composite_step sharing proof_rule : printer = let pp_t = pp_t sharing in let pp_cl = pp_cl ~pp_t in - match step with + match proof_rule with | S_step_c {name;res;proof} -> l[a"stepc";a name;pp_cl res;pp_rec sharing proof] | S_define_t (c,rhs) -> diff --git a/src/sat/Solver.ml b/src/sat/Solver.ml index 174529ef..347a6935 100644 --- a/src/sat/Solver.ml +++ b/src/sat/Solver.ml @@ -19,8 +19,8 @@ module Make(Plugin : PLUGIN) type lit = Plugin.lit type theory = Plugin.t type proof = Plugin.proof - type step_id = Plugin.step_id - type pstep = proof -> step_id + type proof_step = Plugin.proof_step + type proof_rule = proof -> proof_step type clause_pool_id = Clause_pool_id.t module Lit = Plugin.Lit @@ -95,7 +95,7 @@ module Make(Plugin : PLUGIN) c_lits: atom array Vec.t; (* storage for clause content *) c_activity: Vec_float.t; c_recycle_idx: VecI32.t; (* recycle clause numbers that were GC'd *) - c_proof: Step_vec.t; (* clause -> step for its proof *) + c_proof: Step_vec.t; (* clause -> proof_rule for its proof *) c_attached: Bitvec.t; c_marked: Bitvec.t; c_removable: Bitvec.t; @@ -253,9 +253,9 @@ module Make(Plugin : PLUGIN) (** Make a clause with the given atoms *) - val make_a : store -> removable:bool -> atom array -> step_id -> t - val make_l : store -> removable:bool -> atom list -> step_id -> t - val make_vec : store -> removable:bool -> atom Vec.t -> step_id -> t + val make_a : store -> removable:bool -> atom array -> proof_step -> t + val make_l : store -> removable:bool -> atom list -> proof_step -> t + val make_vec : store -> removable:bool -> atom Vec.t -> proof_step -> t val n_atoms : store -> t -> int @@ -271,8 +271,8 @@ module Make(Plugin : PLUGIN) val dealloc : store -> t -> unit (** Delete the clause *) - val set_proof_step : store -> t -> step_id -> unit - val proof_step : store -> t -> step_id + val set_proof_step : store -> t -> proof_step -> unit + val proof_step : store -> t -> proof_step val activity : store -> t -> float val set_activity : store -> t -> float -> unit @@ -296,7 +296,7 @@ module Make(Plugin : PLUGIN) (* TODO: store watch lists inside clauses *) - let make_a (store:store) ~removable (atoms:atom array) step_id : t = + let make_a (store:store) ~removable (atoms:atom array) proof_step : t = let { c_recycle_idx; c_lits; c_activity; c_attached; c_dead; c_removable; c_marked; c_proof; @@ -323,16 +323,16 @@ module Make(Plugin : PLUGIN) end; Vec.set c_lits cid atoms; - Step_vec.set c_proof cid step_id; + Step_vec.set c_proof cid proof_step; let c = of_int_unsafe cid in c - let make_l store ~removable atoms step : t = - make_a store ~removable (Array.of_list atoms) step + let make_l store ~removable atoms proof_rule : t = + make_a store ~removable (Array.of_list atoms) proof_rule - let make_vec store ~removable atoms step : t = - make_a store ~removable (Vec.to_array atoms) step + let make_vec store ~removable atoms proof_rule : t = + make_a store ~removable (Vec.to_array atoms) proof_rule let[@inline] n_atoms (store:store) (c:t) : int = Array.length (Vec.get store.c_store.c_lits (c:t:>int)) @@ -394,14 +394,14 @@ module Make(Plugin : PLUGIN) let[@inline] activity store c = Vec_float.get store.c_store.c_activity (c:t:>int) let[@inline] set_activity store c f = Vec_float.set store.c_store.c_activity (c:t:>int) f - let[@inline] make_removable store l step : t = - make_l store ~removable:true l step + let[@inline] make_removable store l proof_rule : t = + make_l store ~removable:true l proof_rule - let[@inline] make_removable_a store a step = - make_a store ~removable:true a step + let[@inline] make_removable_a store a proof_rule = + make_a store ~removable:true a proof_rule - let[@inline] make_permanent store l step : t = - let c = make_l store ~removable:false l step in + let[@inline] make_permanent store l proof_rule : t = + let c = make_l store ~removable:false l proof_rule in assert (not (removable store c)); (* permanent by default *) c @@ -1377,7 +1377,7 @@ module Make(Plugin : PLUGIN) } (* FIXME - let prove_unsat_ (self:t) (conflict:conflict_res) : step_id = + let prove_unsat_ (self:t) (conflict:conflict_res) : proof_step = if Array.length conflict.atoms = 0 then ( conflict ) else ( @@ -1620,20 +1620,20 @@ module Make(Plugin : PLUGIN) let[@inline] slice_get st i = AVec.get st.trail i - let acts_add_clause self ?(keep=false) (l:lit list) (pstep:pstep): unit = + let acts_add_clause self ?(keep=false) (l:lit list) (proof_rule:proof_rule): unit = let atoms = List.rev_map (make_atom_ self) l in let removable = not keep in let c = - let p = Proof.with_proof self.proof pstep in + let p = Proof.with_proof self.proof proof_rule in Clause.make_l self.store ~removable atoms p in Log.debugf 5 (fun k->k "(@[sat.th.add-clause@ %a@])" (Clause.debug self.store) c); CVec.push self.clauses_to_add_learnt c - let acts_add_clause_in_pool self ~pool (l:lit list) (pstep:pstep): unit = + let acts_add_clause_in_pool self ~pool (l:lit list) (proof_rule:proof_rule): unit = let atoms = List.rev_map (make_atom_ self) l in let removable = true in let c = - let p = Proof.with_proof self.proof pstep in + let p = Proof.with_proof self.proof proof_rule in Clause.make_l self.store ~removable atoms p in let pool = Vec.get self.clause_pools (pool:clause_pool_id:>int) in Log.debugf 5 (fun k->k "(@[sat.th.add-clause-in-pool@ %a@ :pool %s@])" @@ -1650,11 +1650,11 @@ module Make(Plugin : PLUGIN) self.next_decisions <- a :: self.next_decisions ) - let acts_raise self (l:lit list) (pstep:pstep) : 'a = + let acts_raise self (l:lit list) (proof_rule:proof_rule) : 'a = let atoms = List.rev_map (make_atom_ self) l in (* conflicts can be removed *) let c = - let p = Proof.with_proof self.proof pstep in + let p = Proof.with_proof self.proof proof_rule in Clause.make_l self.store ~removable:true atoms p in Log.debugf 5 (fun k->k "(@[@{sat.th.raise-conflict@}@ %a@])" (Clause.debug self.store) c); @@ -1676,17 +1676,17 @@ module Make(Plugin : PLUGIN) let p = make_atom_ self f in if Atom.is_true store p then () else if Atom.is_false store p then ( - let lits, pstep = mk_expl() in + let lits, proof_rule = mk_expl() in let l = List.rev_map (fun f -> Atom.neg @@ make_atom_ self f) lits in check_consequence_lits_false_ self l; let c = - let proof = Proof.with_proof self.proof pstep in + let proof = Proof.with_proof self.proof proof_rule in Clause.make_l store ~removable:true (p :: l) proof in raise_notrace (Th_conflict c) ) else ( insert_var_order self (Atom.var p); let c = lazy ( - let lits, pstep = mk_expl () in + let lits, proof_rule = mk_expl () in let l = List.rev_map (fun f -> Atom.neg @@ make_atom_ self f) lits in (* note: we can check that invariant here in the [lazy] block, as conflict analysis will run in an environment where @@ -1695,7 +1695,7 @@ module Make(Plugin : PLUGIN) (otherwise the propagated lit would have been backtracked and discarded already.) *) check_consequence_lits_false_ self l; - let proof = Proof.with_proof self.proof pstep in + let proof = Proof.with_proof self.proof proof_rule in Clause.make_l store ~removable:true (p :: l) proof ) in let level = decision_level self in @@ -1724,8 +1724,8 @@ module Make(Plugin : PLUGIN) let[@inline] current_slice st : _ Solver_intf.acts = let module M = struct type nonrec proof = proof - type nonrec step_id = step_id - type pstep = proof -> step_id + type nonrec proof_step = proof_step + type proof_rule = proof -> proof_step type nonrec clause_pool_id = clause_pool_id type nonrec lit = lit let iter_assumptions=acts_iter st ~full:false st.th_head @@ -1743,8 +1743,8 @@ module Make(Plugin : PLUGIN) let[@inline] full_slice st : _ Solver_intf.acts = let module M = struct type nonrec proof = proof - type nonrec step_id = step_id - type pstep = proof -> step_id + type nonrec proof_step = proof_step + type proof_rule = proof -> proof_step type nonrec clause_pool_id = clause_pool_id type nonrec lit = lit let iter_assumptions=acts_iter st ~full:true st.th_head @@ -2120,7 +2120,7 @@ module Make(Plugin : PLUGIN) (* Result type *) type res = | Sat of Lit.t Solver_intf.sat_state - | Unsat of (lit,clause,step_id) Solver_intf.unsat_state + | Unsat of (lit,clause,proof_step) Solver_intf.unsat_state let pp_all self lvl status = Log.debugf lvl @@ -2169,7 +2169,7 @@ module Make(Plugin : PLUGIN) in let module M = struct type nonrec lit = lit - type nonrec proof = step_id + type nonrec proof = proof_step type clause = Clause.t let unsat_conflict = unsat_conflict let unsat_assumptions = unsat_assumptions @@ -2179,9 +2179,9 @@ module Make(Plugin : PLUGIN) end in (module M) - let add_clause_atoms_ self ~pool ~removable (c:atom array) step : unit = + let add_clause_atoms_ self ~pool ~removable (c:atom array) proof_rule : unit = try - let proof = Proof.with_proof self.proof step in + let proof = Proof.with_proof self.proof proof_rule in let c = Clause.make_a self.store ~removable c proof in add_clause_ ~pool self c with @@ -2270,7 +2270,7 @@ module Make_pure_sat(Plugin : Solver_intf.PLUGIN_SAT) = Make(struct type lit = Plugin.lit type proof = Plugin.proof - type step_id = Plugin.step_id + type proof_step = Plugin.proof_step module Lit = Plugin.Lit module Proof = Plugin.Proof type t = unit diff --git a/src/sat/Solver_intf.ml b/src/sat/Solver_intf.ml index 6c68445e..eb521412 100644 --- a/src/sat/Solver_intf.ml +++ b/src/sat/Solver_intf.ml @@ -102,9 +102,9 @@ end module type ACTS = sig type lit type proof - type step_id + type proof_step type clause_pool_id = Clause_pool_id.t - type pstep = proof -> step_id + type proof_rule = proof -> proof_step val iter_assumptions: (lit -> unit) -> unit (** Traverse the new assumptions on the boolean trail. *) @@ -116,7 +116,7 @@ module type ACTS = sig (** Map the given lit to an internal atom, which will be decided by the SAT solver. *) - val add_clause: ?keep:bool -> lit list -> pstep -> unit + val add_clause: ?keep:bool -> lit list -> proof_rule -> 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 @@ -124,16 +124,16 @@ module type ACTS = sig - [C_use_allocator alloc] puts the clause in the given allocator. *) - val add_clause_in_pool : pool:clause_pool_id -> lit list -> pstep -> unit + val add_clause_in_pool : pool:clause_pool_id -> lit list -> proof_rule -> unit (** Like {!add_clause} but uses a custom clause pool for the clause, with its own lifetime. *) - val raise_conflict: lit list -> pstep -> 'b + val raise_conflict: lit list -> proof_rule -> '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: lit -> (lit, pstep) reason -> unit + val propagate: lit -> (lit, proof_rule) reason -> unit (** Propagate a lit, i.e. the theory can evaluate the lit to be true (see the definition of {!type:eval_res} *) @@ -189,13 +189,13 @@ module type PLUGIN_CDCL_T = sig type proof (** Proof storage/recording *) - type step_id + type proof_step (** Identifier for a clause precendently added/proved *) module Proof : PROOF with type t = proof and type lit = lit - and type step_id = step_id + and type proof_step = proof_step val push_level : t -> unit (** Create a new backtrack level *) @@ -221,11 +221,11 @@ module type PLUGIN_SAT = sig module Lit : LIT with type t = lit type proof - type step_id + type proof_step module Proof : PROOF with type t = proof and type lit = lit - and type step_id = step_id + and type proof_step = proof_step end (** The external interface implemented by safe solvers, such as the one @@ -249,9 +249,9 @@ module type S = sig type proof (** A representation of a full proof *) - type step_id + type proof_step - type pstep = proof -> step_id + type proof_rule = proof -> proof_step type solver (** The main solver type. *) @@ -345,7 +345,7 @@ module type S = sig (** Result type for the solver *) type res = | Sat of lit sat_state (** Returned when the solver reaches SAT, with a model *) - | Unsat of (lit,clause,step_id) unsat_state (** Returned when the solver reaches UNSAT, with a proof *) + | Unsat of (lit,clause,proof_step) unsat_state (** Returned when the solver reaches UNSAT, with a proof *) exception UndecidedLit (** Exception raised by the evaluating functions when a literal @@ -357,10 +357,10 @@ module type S = sig (** Add the list of clauses to the current set of assumptions. Modifies the sat solver state in place. *) - val add_clause : t -> lit list -> pstep -> unit + val add_clause : t -> lit list -> proof_rule -> unit (** Lower level addition of clauses *) - val add_clause_a : t -> lit array -> pstep -> unit + val add_clause_a : t -> lit array -> proof_rule -> unit (** Lower level addition of clauses *) val add_input_clause : t -> lit list -> unit @@ -369,10 +369,10 @@ module type S = sig val add_input_clause_a : t -> lit array -> unit (** Like {!add_clause_a} but with justification of being an input clause *) - val add_clause_in_pool : t -> pool:clause_pool_id -> lit list -> pstep -> unit + val add_clause_in_pool : t -> pool:clause_pool_id -> lit list -> proof_rule -> unit (** Like {!add_clause} but using a specific clause pool *) - val add_clause_a_in_pool : t -> pool:clause_pool_id -> lit array -> pstep -> unit + val add_clause_a_in_pool : t -> pool:clause_pool_id -> lit array -> proof_rule -> unit (** Like {!add_clause_a} but using a specific clause pool *) (* TODO: API to push/pop/clear assumptions from an inner vector *) diff --git a/src/smt-solver/Sidekick_smt_solver.ml b/src/smt-solver/Sidekick_smt_solver.ml index 621a0229..442eac14 100644 --- a/src/smt-solver/Sidekick_smt_solver.ml +++ b/src/smt-solver/Sidekick_smt_solver.ml @@ -13,9 +13,11 @@ module type ARG = sig module T : TERM module Lit : LIT with module T = T type proof + type proof_step module P : PROOF with type term = T.Term.t and type t = proof + and type proof_step = proof_step and type lit = Lit.t val cc_view : T.Term.t -> (T.Fun.t, T.Term.t, T.Term.t Iter.t) CC_view.t @@ -32,6 +34,7 @@ module Make(A : ARG) : S with module T = A.T and type proof = A.proof + and type proof_step = A.proof_step and module Lit = A.Lit and module P = A.P = struct @@ -43,7 +46,8 @@ module Make(A : ARG) type term = Term.t type ty = Ty.t type proof = A.proof - type dproof = proof -> unit + type proof_step = A.proof_step + type proof_rule = proof -> proof_step type lit = Lit.t (* actions from the sat solver *) @@ -85,7 +89,8 @@ module Make(A : ARG) module CC = CC module N = CC.N type nonrec proof = proof - type dproof = proof -> unit + type nonrec proof_step = proof_step + type proof_rule = proof -> proof_step type term = Term.t type ty = Ty.t type lit = Lit.t @@ -160,7 +165,7 @@ module Make(A : ARG) module type PREPROCESS_ACTS = sig val mk_lit : ?sign:bool -> term -> lit - val add_clause : lit list -> dproof -> unit + val add_clause : lit list -> proof_rule -> unit val add_lit : ?default_pol:bool -> lit -> unit end type preprocess_actions = (module PREPROCESS_ACTS) @@ -236,12 +241,12 @@ module Make(A : ARG) let[@inline] propagate_l self acts p cs proof : unit = propagate self acts p ~reason:(fun()->cs,proof) - let add_sat_clause_ self (acts:theory_actions) ~keep lits (proof:dproof) : unit = + let add_sat_clause_ self (acts:theory_actions) ~keep lits (proof:proof_rule) : unit = let (module A) = acts in Stat.incr self.count_axiom; A.add_clause ~keep lits proof - let add_sat_clause_pool_ self (acts:theory_actions) ~pool lits (proof:dproof) : unit = + let add_sat_clause_pool_ self (acts:theory_actions) ~pool lits (proof:proof_rule) : unit = let (module A) = acts in Stat.incr self.count_axiom; A.add_clause_in_pool ~pool lits proof @@ -371,7 +376,7 @@ module Make(A : ARG) Lit.atom self.tst ~sign u (* add a clause using [acts] *) - let add_clause_ self acts lits (proof:dproof) : unit = + let add_clause_ self acts lits (proof:proof_rule) : unit = add_sat_clause_ self acts ~keep:true lits proof let[@inline] add_lit _self (acts:theory_actions) ?default_pol lit : unit = @@ -398,11 +403,11 @@ module Make(A : ARG) let[@inline] preprocess_term self (pacts:preprocess_actions) (t:term) : term = preprocess_term_ self pacts t - let[@inline] add_clause_temp self acts c (proof:dproof) : unit = + let[@inline] add_clause_temp self acts c (proof:proof_rule) : unit = let c = preprocess_clause_ self acts c in add_sat_clause_ self acts ~keep:false c proof - let[@inline] add_clause_permanent self acts c (proof:dproof) : unit = + let[@inline] add_clause_permanent self acts c (proof:proof_rule) : unit = let c = preprocess_clause_ self acts c in add_sat_clause_ self acts ~keep:true c proof @@ -687,7 +692,7 @@ module Make(A : ARG) let pp_stats out (self:t) : unit = Stat.pp_all out (Stat.all @@ stats self) - let add_clause (self:t) (c:lit IArray.t) (proof:dproof) : unit = + let add_clause (self:t) (c:lit IArray.t) (proof:proof_rule) : unit = Stat.incr self.count_clause; Log.debugf 50 (fun k-> k "(@[solver.add-clause@ %a@])" diff --git a/src/th-bool-static/Sidekick_th_bool_static.ml b/src/th-bool-static/Sidekick_th_bool_static.ml index 703fd9f7..cd469f07 100644 --- a/src/th-bool-static/Sidekick_th_bool_static.ml +++ b/src/th-bool-static/Sidekick_th_bool_static.ml @@ -36,20 +36,20 @@ module type ARG = sig Only enable if some theories are susceptible to create boolean formulas during the proof search. *) - val lemma_bool_tauto : S.Lit.t Iter.t -> S.P.t -> unit + val lemma_bool_tauto : S.Lit.t Iter.t -> S.P.proof_rule (** Boolean tautology lemma (clause) *) - val lemma_bool_c : string -> term list -> S.P.t -> unit + val lemma_bool_c : string -> term list -> S.P.proof_rule (** Basic boolean logic lemma for a clause [|- c]. [proof_bool_c b name cs] is the rule designated by [name]. *) - val lemma_bool_equiv : term -> term -> S.P.t -> unit + val lemma_bool_equiv : term -> term -> S.P.proof_rule (** Boolean tautology lemma (equivalence) *) - val lemma_ite_true : a:term -> ite:term -> S.P.t -> unit + val lemma_ite_true : a:term -> ite:term -> S.P.proof_rule (** lemma [a => ite a b c = b] *) - val lemma_ite_false : a:term -> ite:term -> S.P.t -> unit + val lemma_ite_false : a:term -> ite:term -> S.P.proof_rule (** lemma [¬a => ite a b c = c] *) (** Fresh symbol generator. @@ -116,21 +116,24 @@ module Make(A : ARG) : S with module A = A = struct let is_true t = match T.as_bool t with Some true -> true | _ -> false let is_false t = match T.as_bool t with Some false -> true | _ -> false - let simplify (self:state) (simp:SI.Simplify.t) (t:T.t) : T.t option = + let simplify (self:state) (simp:SI.Simplify.t) (t:T.t) : (T.t * SI.proof_step Iter.t) option = let tst = self.tst in - let ret u = - if not (T.equal t u) then ( - SI.Simplify.with_proof simp (fun p -> - A.lemma_bool_equiv t u p; - A.S.P.lemma_preprocess t u p; - ); - ); - Some u + let steps = ref [] in + let add_step_ s = steps := s :: !steps in + + let[@inline] ret u = + Some (u, Iter.of_list !steps) in + (* proof is [t <=> u] *) + let ret_bequiv t1 u = + add_step_ @@ SI.Simplify.with_proof simp (A.lemma_bool_equiv t1 u); + ret u + in + match A.view_as_bool t with | B_bool _ -> None - | B_not u when is_true u -> ret (T.bool tst false) - | B_not u when is_false u -> ret (T.bool tst true) + | B_not u when is_true u -> ret_bequiv t (T.bool tst false) + | B_not u when is_false u -> ret_bequiv t (T.bool tst true) | B_not _ -> None | B_opaque_bool _ -> None | B_and a -> @@ -148,28 +151,29 @@ module Make(A : ARG) : S with module A = A = struct | B_ite (a,b,c) -> (* directly simplify [a] so that maybe we never will simplify one of the branches *) - let a = SI.Simplify.normalize_t simp a in + let a, prf_a = SI.Simplify.normalize_t simp a in + Iter.iter add_step_ prf_a; begin match A.view_as_bool a with | B_bool true -> - SI.Simplify.with_proof simp (A.lemma_ite_true ~a ~ite:t); - Some b + add_step_ @@ SI.Simplify.with_proof simp (A.lemma_ite_true ~a ~ite:t); + ret b | B_bool false -> - SI.Simplify.with_proof simp (A.lemma_ite_false ~a ~ite:t); - Some c + add_step_ @@ SI.Simplify.with_proof simp (A.lemma_ite_false ~a ~ite:t); + ret c | _ -> None end - | B_equiv (a,b) when is_true a -> ret b - | B_equiv (a,b) when is_false a -> ret (not_ tst b) - | B_equiv (a,b) when is_true b -> ret a - | B_equiv (a,b) when is_false b -> ret (not_ tst a) - | B_xor (a,b) when is_false a -> ret b - | B_xor (a,b) when is_true a -> ret (not_ tst b) - | B_xor (a,b) when is_false b -> ret a - | B_xor (a,b) when is_true b -> ret (not_ tst a) + | B_equiv (a,b) when is_true a -> ret_bequiv t b + | B_equiv (a,b) when is_false a -> ret_bequiv t (not_ tst b) + | B_equiv (a,b) when is_true b -> ret_bequiv t a + | B_equiv (a,b) when is_false b -> ret_bequiv t (not_ tst a) + | B_xor (a,b) when is_false a -> ret_bequiv t b + | B_xor (a,b) when is_true a -> ret_bequiv t (not_ tst b) + | B_xor (a,b) when is_false b -> ret_bequiv t a + | B_xor (a,b) when is_true b -> ret_bequiv t (not_ tst a) | B_equiv _ | B_xor _ -> None - | B_eq (a,b) when T.equal a b -> ret (T.bool tst true) - | B_neq (a,b) when T.equal a b -> ret (T.bool tst true) + | B_eq (a,b) when T.equal a b -> ret_bequiv t (T.bool tst true) + | B_neq (a,b) when T.equal a b -> ret_bequiv t (T.bool tst true) | B_eq _ | B_neq _ -> None | B_atom _ -> None @@ -186,28 +190,35 @@ module Make(A : ARG) : S with module A = A = struct proxy, mk_lit proxy (* preprocess "ite" away *) - let preproc_ite self si (module PA:SI.PREPROCESS_ACTS) (t:T.t) : T.t option = + let preproc_ite self si (module PA:SI.PREPROCESS_ACTS) (t:T.t) : (T.t * SI.proof_step Iter.t) option = + let steps = ref [] in + let add_step_ s = steps := s :: !steps in + + let ret t = Some (t, Iter.of_list !steps) in + match A.view_as_bool t with | B_ite (a,b,c) -> - let a = SI.simp_t si a in - begin match A.view_as_bool a with + let a', pr_a = SI.simp_t si a in + CCOpt.iter add_step_ pr_a; + begin match A.view_as_bool a' with | B_bool true -> (* [a=true |- ite a b c=b], [|- a=true] ==> [|- t=b] *) - SI.with_proof si (A.lemma_ite_true ~a ~ite:t); - Some b + add_step_ @@ SI.with_proof si (A.lemma_ite_true ~a:a' ~ite:t); + ret b | B_bool false -> (* [a=false |- ite a b c=c], [|- a=false] ==> [|- t=c] *) - SI.with_proof si (A.lemma_ite_false ~a ~ite:t); - Some c + add_step_ @@ SI.with_proof si (A.lemma_ite_false ~a:a' ~ite:t); + ret c | _ -> let t_ite = fresh_term self ~for_t:t ~pre:"ite" (T.ty b) in SI.define_const si ~const:t_ite ~rhs:t; - SI.with_proof si (SI.P.define_term t_ite t); - let lit_a = PA.mk_lit a in + let pr = SI.with_proof si (SI.P.define_term t_ite t) in + let lit_a = PA.mk_lit a' in + (* TODO: use unit paramod on each clause with side t=t_ite and on a=a' *) PA.add_clause [Lit.neg lit_a; PA.mk_lit (eq self.tst t_ite b)] - (fun p -> A.lemma_ite_true ~a ~ite:t p); + (fun p -> SI.P.proof_p1 pr_a (A.lemma_ite_true ~a:a' ~ite:t p) p); PA.add_clause [lit_a; PA.mk_lit (eq self.tst t_ite c)] - (fun p -> A.lemma_ite_false p ~a ~ite:t); + (fun p -> A.lemma_ite_false p ~a:a' ~ite:t); Some t_ite end | _ -> None