From 85ba423e8ccbfba296924f35f9d8f88c08e08bb1 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 12 Oct 2022 12:22:19 -0400 Subject: [PATCH] wip: refactor(smt): use sidekick.proof for proof tracing --- src/smt/dune | 4 ++-- src/smt/preprocess.ml | 9 +++++---- src/smt/preprocess.mli | 4 ++-- src/smt/sigs.ml | 4 ++-- src/smt/solver.ml | 2 -- src/smt/solver.mli | 8 +++----- src/smt/solver_internal.ml | 25 +++++++++++++------------ src/smt/solver_internal.mli | 20 ++++++++------------ src/smt/tracer.ml | 36 ++++++++++++++++++++---------------- src/smt/tracer.mli | 16 +++++++++++++--- 10 files changed, 68 insertions(+), 60 deletions(-) diff --git a/src/smt/dune b/src/smt/dune index e72db5d8..3474e024 100644 --- a/src/smt/dune +++ b/src/smt/dune @@ -3,6 +3,6 @@ (public_name sidekick.smt-solver) (synopsis "main SMT solver") (libraries containers iter sidekick.core sidekick.util sidekick.cc - sidekick.sat sidekick.abstract-solver sidekick.simplify - sidekick.model sidekick.trace) + sidekick.sat sidekick.abstract-solver sidekick.simplify sidekick.model + sidekick.proof sidekick.trace) (flags :standard -w +32 -open Sidekick_util)) diff --git a/src/smt/preprocess.ml b/src/smt/preprocess.ml index d259097f..561574a6 100644 --- a/src/smt/preprocess.ml +++ b/src/smt/preprocess.ml @@ -1,7 +1,7 @@ open Sigs module type PREPROCESS_ACTS = sig - val proof : proof_trace + val proof_tracer : Proof.Tracer.t val mk_lit : ?sign:bool -> term -> lit val add_clause : lit list -> step_id -> unit val add_lit : ?default_pol:bool -> lit -> unit @@ -13,7 +13,7 @@ type t = { tst: Term.store; (** state for managing terms *) cc: CC.t; simplify: Simplify.t; - proof: proof_trace; + proof: Proof.Tracer.t; mutable preprocess: preprocess_hook list; preprocessed: Term.t Term.Tbl.t; n_preprocess_clause: int Stat.counter; @@ -28,6 +28,7 @@ and preprocess_hook = term option let create ?(stat = Stat.global) ~proof ~cc ~simplify tst : t = + let proof = (proof : #Proof.Tracer.t :> Proof.Tracer.t) in { tst; proof; @@ -130,8 +131,8 @@ module Preprocess_clause (A : ARR) = struct pr_c else ( Stat.incr self.n_preprocess_clause; - Proof_trace.add_step self.proof @@ fun () -> - Proof_core.lemma_rw_clause pr_c ~res:(A.to_list c') ~using:!steps + Proof.Tracer.add_step self.proof @@ fun () -> + Proof.Core_rules.lemma_rw_clause pr_c ~res:(A.to_list c') ~using:!steps ) in c', pr_c' diff --git a/src/smt/preprocess.mli b/src/smt/preprocess.mli index 40fda4f3..1ccb5c76 100644 --- a/src/smt/preprocess.mli +++ b/src/smt/preprocess.mli @@ -14,7 +14,7 @@ type t val create : ?stat:Stat.t -> - proof:proof_trace -> + proof:#Proof.Tracer.t -> cc:CC.t -> simplify:Simplify.t -> Term.store -> @@ -22,7 +22,7 @@ val create : (** Actions given to preprocessor hooks *) module type PREPROCESS_ACTS = sig - val proof : proof_trace + val proof_tracer : Proof.Tracer.t val mk_lit : ?sign:bool -> term -> lit (** [mk_lit t] creates a new literal for a boolean term [t]. *) diff --git a/src/smt/sigs.ml b/src/smt/sigs.ml index cdd56bea..cc4732d3 100644 --- a/src/smt/sigs.ml +++ b/src/smt/sigs.ml @@ -18,14 +18,14 @@ module Simplify = Sidekick_simplify module CC = Sidekick_cc.CC module E_node = Sidekick_cc.E_node module CC_expl = Sidekick_cc.Expl +module Proof = Sidekick_proof type term = Term.t type ty = term type value = Term.t type lit = Lit.t type term_store = Term.store -type proof_trace = Proof_trace.t -type step_id = Proof_step.id +type step_id = Sidekick_proof.Step.id (* actions from the sat solver *) type sat_acts = Sidekick_sat.acts diff --git a/src/smt/solver.ml b/src/smt/solver.ml index 4a0abab5..e424cbd1 100644 --- a/src/smt/solver.ml +++ b/src/smt/solver.ml @@ -11,8 +11,6 @@ module Check_res = Sidekick_abstract_solver.Check_res module Sat_solver = Sidekick_sat (** the parametrized SAT Solver *) -(** {2 Result} *) - module Unknown = Sidekick_abstract_solver.Unknown [@@ocaml.warning "-37"] type res = Check_res.t = diff --git a/src/smt/solver.mli b/src/smt/solver.mli index 766c98d6..766447b7 100644 --- a/src/smt/solver.mli +++ b/src/smt/solver.mli @@ -31,15 +31,14 @@ val mk_theory : val stats : t -> Stat.t val tst : t -> Term.store -val proof : t -> proof_trace +val tracer : t -> #Tracer.t val create : (module ARG) -> ?stat:Stat.t -> ?size:[ `Big | `Tiny | `Small ] -> (* TODO? ?config:Config.t -> *) - ?tracer:Tracer.t -> - proof:proof_trace -> + tracer:Tracer.t -> theories:Theory.t list -> Term.store -> unit -> @@ -61,8 +60,7 @@ val create_default : ?stat:Stat.t -> ?size:[ `Big | `Tiny | `Small ] -> (* TODO? ?config:Config.t -> *) - ?tracer:Tracer.t -> - proof:proof_trace -> + tracer:Tracer.t -> theories:Theory.t list -> Term.store -> unit -> diff --git a/src/smt/solver_internal.ml b/src/smt/solver_internal.ml index 998ca25e..c79ebdb5 100644 --- a/src/smt/solver_internal.ml +++ b/src/smt/solver_internal.ml @@ -39,7 +39,7 @@ type preprocess_hook = type t = { tst: Term.store; (** state for managing terms *) cc: CC.t; (** congruence closure *) - proof: proof_trace; (** proof logger *) + tracer: Tracer.t; registry: Registry.t; seen_types: Term.Weak_set.t; (** types we've seen so far *) on_progress: (unit, unit) Event.Emitter.t; @@ -58,7 +58,6 @@ type t = { mutable level: int; mutable complete: bool; stat: Stat.t; - tracer: Tracer.t; [@ocaml.warning "-69"] count_axiom: int Stat.counter; count_conflict: int Stat.counter; count_propagate: int Stat.counter; @@ -73,7 +72,7 @@ type solver = t let[@inline] cc (self : t) = self.cc let[@inline] tst self = self.tst -let[@inline] proof self = self.proof +let[@inline] tracer self = self.tracer let stats self = self.stat let registry self = self.registry let simplifier self = self.simp @@ -111,7 +110,7 @@ let add_sat_clause_ self (acts : theory_actions) ~keep lits (proof : step_id) : unit = let (module A) = acts in Stat.incr self.count_axiom; - A.add_clause ~keep lits proof + A.add_clause ~keep lits (fun () -> Proof.Pterm.ref proof) let add_sat_lit_ _self ?default_pol (acts : theory_actions) (lit : Lit.t) : unit = @@ -129,7 +128,7 @@ let delayed_add_clause (self : t) ~keep (c : Lit.t list) (pr : step_id) : unit = let preprocess_acts (self : t) : Preprocess.preprocess_actions = (module struct - let proof = self.proof + let proof_tracer = (self.tracer :> Proof.Tracer.t) let mk_lit ?sign t : Lit.t = Lit.atom ?sign self.tst t let add_clause c pr = delayed_add_clause self ~keep:true c pr let add_lit ?default_pol lit = delayed_add_lit self ?default_pol lit @@ -307,7 +306,7 @@ let cc_are_equal self t1 t2 = let cc_resolve_expl self e : lit list * _ = let r = CC.explain_expl (cc self) e in - r.lits, r.pr self.proof + r.lits, r.pr (** {2 Interface with the SAT solver} *) @@ -411,7 +410,7 @@ let check_cc_with_acts_ (self : t) (acts : theory_actions) = acts | Error (CC.Result_action.Conflict (lits, pr)) -> Stat.incr self.count_conflict; - A.raise_conflict lits pr + A.raise_conflict lits (fun () -> Proof.Pterm.ref pr) (* handle a literal assumed by the SAT solver *) let assert_lits_ ~final (self : t) (acts : theory_actions) (lits : Lit.t Iter.t) @@ -521,16 +520,18 @@ let add_theory_state ~st ~push_level ~pop_levels (self : t) = self.th_states <- Ths_cons { st; push_level; pop_levels; next = self.th_states } -let create (module A : ARG) ~stat ~tracer ~proof (tst : Term.store) () : t = - let simp = Simplify.create tst ~proof in - let cc = CC.create (module A : CC.ARG) ~size:`Big tst proof in - let preprocess = Preprocess.create ~stat ~proof ~cc ~simplify:simp tst in +let create (module A : ARG) ~stat ~tracer (tst : Term.store) () : t = + let tracer = (tracer : #Tracer.t :> Tracer.t) in + let simp = Simplify.create tst ~proof:tracer in + let cc = CC.create (module A : CC.ARG) ~size:`Big tst tracer in + let preprocess = + Preprocess.create ~stat ~proof:tracer ~cc ~simplify:simp tst + in let find_foreign = Find_foreign.create () in let self = { tst; cc; - proof; tracer; th_states = Ths_nil; stat; diff --git a/src/smt/solver_internal.mli b/src/smt/solver_internal.mli index a6226aa7..80c238b4 100644 --- a/src/smt/solver_internal.mli +++ b/src/smt/solver_internal.mli @@ -13,8 +13,8 @@ type solver = t val tst : t -> term_store val stats : t -> Stat.t -val proof : t -> proof_trace -(** Access the proof object *) +val tracer : t -> Tracer.t +(** Access the tracer object *) val registry : t -> Registry.t (** A solver contains a registry so that theories can share data *) @@ -121,11 +121,13 @@ val propagate_l : t -> theory_actions -> lit -> lit list -> step_id -> 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 -> step_id -> unit +val add_clause_temp : + t -> theory_actions -> lit list -> Proof.Pterm.delayed -> 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 -> step_id -> unit +val add_clause_permanent : + t -> theory_actions -> lit list -> Proof.Pterm.delayed -> unit (** Add toplevel clause to the SAT solver. This clause will not be backtracked. *) @@ -150,7 +152,7 @@ val cc_find : t -> E_node.t -> E_node.t val cc_are_equal : t -> term -> term -> bool (** Are these two terms equal in the congruence closure? *) -val cc_resolve_expl : t -> CC_expl.t -> lit list * step_id +val cc_resolve_expl : t -> CC_expl.t -> lit list * Proof.Pterm.delayed (* val cc_raise_conflict_expl : t -> theory_actions -> CC_expl.t -> 'a @@ -284,10 +286,4 @@ val add_theory_state : unit val create : - (module ARG) -> - stat:Stat.t -> - tracer:Tracer.t -> - proof:Proof_trace.t -> - Term.store -> - unit -> - t + (module ARG) -> stat:Stat.t -> tracer:#Tracer.t -> Term.store -> unit -> t diff --git a/src/smt/tracer.ml b/src/smt/tracer.ml index 92967187..8405d422 100644 --- a/src/smt/tracer.ml +++ b/src/smt/tracer.ml @@ -1,18 +1,20 @@ open Sidekick_core module Tr = Sidekick_trace +module Proof = Sidekick_proof module V = Ser_value class type t = object inherit Term.Tracer.t - method emit_assert_term : Term.t -> Tr.Entry_id.t - inherit Clause_tracer.t + inherit Sidekick_proof.Tracer.t + inherit Sidekick_sat.Tracer.t method emit_assert_term : Term.t -> Tr.Entry_id.t end class concrete (sink : Tr.Sink.t) : t = object (self) inherit Term.Tracer.concrete ~sink as emit_t + inherit Sidekick_proof.Tracer.concrete ~sink method emit_assert_term t = let id_t = emit_t#emit_term t in @@ -20,23 +22,23 @@ class concrete (sink : Tr.Sink.t) : t = let id = Tr.Sink.emit sink ~tag:"AssT" v in id - method encode_lit (lit : Lit.t) : V.t = + method sat_encode_lit (lit : Lit.t) : V.t = let sign = Lit.sign lit in let id_t = emit_t#emit_term @@ Lit.term lit in V.(list [ bool sign; int id_t ]) - method assert_clause ~id (c : Lit.t Iter.t) = + method sat_assert_clause ~id (c : Lit.t Iter.t) (pr : Proof.Step.id) = (* get a list of pairs *) - let l = Iter.map self#encode_lit c |> Iter.to_rev_list |> V.list in - let v = V.(dict_of_list [ "id", int id; "c", l ]) in + let l = Iter.map self#sat_encode_lit c |> Iter.to_rev_list |> V.list in + let v = V.(dict_of_list [ "id", int id; "c", l; "p", int pr ]) in let id = Tr.Sink.emit sink ~tag:"AssC" v in id - method unsat_clause ~id = + method sat_unsat_clause ~id = let v = Ser_value.(dict_of_list [ "id", int id ]) in Tr.Sink.emit sink ~tag:"UnsatC" v - method delete_clause ~id _lits : unit = + method sat_delete_clause ~id _lits : unit = let v = Ser_value.(dict_of_list [ "id", int id ]) in ignore (Tr.Sink.emit sink ~tag:"DelCSat" v : Tr.Entry_id.t) end @@ -44,23 +46,25 @@ class concrete (sink : Tr.Sink.t) : t = class dummy : t = object inherit Term.Tracer.dummy - inherit Clause_tracer.dummy + inherit Sidekick_sat.Tracer.dummy method emit_assert_term _ = Tr.Entry_id.dummy end let dummy : #t = new dummy let make ~sink () = new concrete sink -let assert_clause (self : #t) ~id c : Tr.Entry_id.t = self#assert_clause ~id c -let assert_clause' (self : #t) ~id c : unit = - ignore (self#assert_clause ~id c : Tr.Entry_id.t) +let assert_clause (self : #t) ~id c pr : Tr.Entry_id.t = + self#sat_assert_clause ~id c pr -let unsat_clause (self : #t) ~id : Tr.Entry_id.t = self#unsat_clause ~id +let assert_clause' (self : #t) ~id c pr : unit = + ignore (self#sat_assert_clause ~id c pr : Tr.Entry_id.t) + +let unsat_clause (self : #t) ~id : Tr.Entry_id.t = self#sat_unsat_clause ~id let unsat_clause' (self : #t) ~id : unit = - ignore (self#unsat_clause ~id : Tr.Entry_id.t) + ignore (self#sat_unsat_clause ~id : Tr.Entry_id.t) -let delete_clause (self : #t) ~id c = self#delete_clause ~id c -let encode_lit (self : #t) lit = self#encode_lit lit +let delete_clause (self : #t) ~id c = self#sat_delete_clause ~id c +let encode_lit (self : #t) lit = self#sat_encode_lit lit let assert_term (self : #t) t = self#emit_assert_term t let assert_term' (self : #t) t = ignore (assert_term self t : Tr.Entry_id.t) diff --git a/src/smt/tracer.mli b/src/smt/tracer.mli index 1cd55a64..f0f4b6cd 100644 --- a/src/smt/tracer.mli +++ b/src/smt/tracer.mli @@ -1,10 +1,17 @@ +(** Tracer for SMT solvers. + + The tracer is used to track clauses and terms used or deduced during proof + search. *) + open Sidekick_core module Tr = Sidekick_trace +module Proof = Sidekick_proof class type t = object inherit Term.Tracer.t - inherit Clause_tracer.t + inherit Sidekick_sat.Tracer.t + inherit Sidekick_proof.Tracer.t method emit_assert_term : Term.t -> Tr.Entry_id.t (** Emit an assertion *) @@ -20,8 +27,11 @@ val dummy : t val make : sink:Tr.Sink.t -> unit -> t val assert_term : #t -> Term.t -> Tr.Entry_id.t val assert_term' : #t -> Term.t -> unit -val assert_clause : #t -> id:int -> Lit.t Iter.t -> Tr.Entry_id.t -val assert_clause' : #t -> id:int -> Lit.t Iter.t -> unit + +val assert_clause : + #t -> id:int -> Lit.t Iter.t -> Proof.Step.id -> Tr.Entry_id.t + +val assert_clause' : #t -> id:int -> Lit.t Iter.t -> Proof.Step.id -> unit val delete_clause : #t -> id:int -> Lit.t Iter.t -> unit val unsat_clause : #t -> id:int -> Tr.Entry_id.t val unsat_clause' : #t -> id:int -> unit