From 8eb50afecb449ab41caadca377735d3a3b6105c0 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 2 Sep 2021 22:24:59 -0400 Subject: [PATCH] feat(smt): provide SAT solver to theories upon initialization --- src/core/Sidekick_core.ml | 16 ++++++++++++++-- src/lra/sidekick_arith_lra.ml | 2 +- src/sat/Solver_intf.ml | 2 +- src/smt-solver/Sidekick_smt_solver.ml | 4 ++-- src/smtlib/Process.ml | 2 +- src/th-bool-static/Sidekick_th_bool_static.ml | 2 +- src/th-cstor/Sidekick_th_cstor.ml | 2 +- src/th-data/Sidekick_th_data.ml | 2 +- 8 files changed, 22 insertions(+), 10 deletions(-) diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index c104f93c..f0fdc4f9 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -954,6 +954,18 @@ module type SOLVER = sig type dproof = proof -> unit (** Delayed proof. This is used to build a proof step on demand. *) + (** The internal SAT solver *) + module Sat_solver : sig + type clause_pool_id = Clause_pool_id.t + type t + + val new_clause_pool_gc_fixed_size : + descr:string -> + size:int -> + t -> + clause_pool_id + end + (** {3 A theory} Theories are abstracted over the concrete implementation of the solver, @@ -976,7 +988,7 @@ module type SOLVER = sig val name : string (** Name of the theory (ideally, unique and short) *) - val create_and_setup : Solver_internal.t -> t + val create_and_setup : Solver_internal.t -> Sat_solver.t -> t (** Instantiate the theory's state for the given (internal) solver, register callbacks, create keys, etc. @@ -1004,7 +1016,7 @@ module type SOLVER = sig val mk_theory : name:string -> - create_and_setup:(Solver_internal.t -> 'th) -> + create_and_setup:(Solver_internal.t -> Sat_solver.t -> 'th) -> ?push_level:('th -> unit) -> ?pop_levels:('th -> int -> unit) -> unit -> diff --git a/src/lra/sidekick_arith_lra.ml b/src/lra/sidekick_arith_lra.ml index 844f0be6..65cc411f 100644 --- a/src/lra/sidekick_arith_lra.ml +++ b/src/lra/sidekick_arith_lra.ml @@ -601,7 +601,7 @@ module Make(A : ARG) : S with module A = A = struct T.Tbl.add self.needs_th_combination t () ) - let create_and_setup si = + let create_and_setup si _ = Log.debug 2 "(th-lra.setup)"; let stat = SI.stats si in let st = create ~stat (SI.tst si) (SI.ty_st si) in diff --git a/src/sat/Solver_intf.ml b/src/sat/Solver_intf.ml index 851241c6..5ca14f17 100644 --- a/src/sat/Solver_intf.ml +++ b/src/sat/Solver_intf.ml @@ -222,7 +222,7 @@ module type S = sig type clause - type clause_pool_id + type clause_pool_id = Clause_pool_id.t (** Pool of clauses, with its own lifetime management *) type theory diff --git a/src/smt-solver/Sidekick_smt_solver.ml b/src/smt-solver/Sidekick_smt_solver.ml index db6c7854..a6fb0690 100644 --- a/src/smt-solver/Sidekick_smt_solver.ml +++ b/src/smt-solver/Sidekick_smt_solver.ml @@ -567,7 +567,7 @@ module Make(A : ARG) module type THEORY = sig type t val name : string - val create_and_setup : Solver_internal.t -> t + val create_and_setup : Solver_internal.t -> Sat_solver.t -> t val push_level : t -> unit val pop_levels : t -> int -> unit end @@ -581,7 +581,7 @@ module Make(A : ARG) let (module Th) = th in Log.debugf 2 (fun k-> k "(@[smt-solver.add-theory@ :name %S@])" Th.name); - let st = Th.create_and_setup self.si in + let st = Th.create_and_setup self.si self.solver in (* add push/pop to the internal solver *) begin let open Solver_internal in diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index ea534db3..b9e2b435 100644 --- a/src/smtlib/Process.ml +++ b/src/smtlib/Process.ml @@ -57,7 +57,7 @@ module Check_cc = struct let theory = Solver.mk_theory ~name:"cc-check" - ~create_and_setup:(fun si -> + ~create_and_setup:(fun si _sat -> let n_calls = Stat.mk_int (Solver.Solver_internal.stats si) "check-cc.call" in Solver.Solver_internal.on_cc_conflict si (fun cc ~th c -> diff --git a/src/th-bool-static/Sidekick_th_bool_static.ml b/src/th-bool-static/Sidekick_th_bool_static.ml index 703fd9f7..71bb0399 100644 --- a/src/th-bool-static/Sidekick_th_bool_static.ml +++ b/src/th-bool-static/Sidekick_th_bool_static.ml @@ -355,7 +355,7 @@ module Make(A : ARG) : S with module A = A = struct end; () - let create_and_setup si = + let create_and_setup si _sat = Log.debug 2 "(th-bool.setup)"; let st = create (SI.tst si) (SI.ty_st si) in SI.add_simplifier si (simplify st); diff --git a/src/th-cstor/Sidekick_th_cstor.ml b/src/th-cstor/Sidekick_th_cstor.ml index 993ce743..fccc6821 100644 --- a/src/th-cstor/Sidekick_th_cstor.ml +++ b/src/th-cstor/Sidekick_th_cstor.ml @@ -83,7 +83,7 @@ module Make(A : ARG) : S with module A = A = struct let push_level = ST.push_level let pop_levels = ST.pop_levels - let create_and_setup (solver:SI.t) : t = + let create_and_setup (solver:SI.t) _ : t = Log.debug 1 "(setup :th-cstor)"; let self = ST.create_and_setup ~size:32 solver in self diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml index 26392232..3f02df77 100644 --- a/src/th-data/Sidekick_th_data.ml +++ b/src/th-data/Sidekick_th_data.ml @@ -662,7 +662,7 @@ module Make(A : ARG) : S with module A = A = struct let t = A.mk_cstor self.tst c.c_cstor args in Some t - let create_and_setup (solver:SI.t) : t = + let create_and_setup (solver:SI.t) _ : t = let self = { tst=SI.tst solver; cstors=ST_cstors.create_and_setup ~size:32 solver;