From 697678d6d24da7380bdc7d3a11e0ad16c0543db6 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 24 Sep 2021 22:44:52 -0400 Subject: [PATCH] feat(dyn-trans): provide config record when instantiating theory --- src/base-solver/sidekick_base_solver.ml | 1 + src/th-dyn-trans/Sidekick_th_dyn_trans.ml | 42 +++++++++++++++++------ 2 files changed, 33 insertions(+), 10 deletions(-) diff --git a/src/base-solver/sidekick_base_solver.ml b/src/base-solver/sidekick_base_solver.ml index c0e567bf..0759d12e 100644 --- a/src/base-solver/sidekick_base_solver.ml +++ b/src/base-solver/sidekick_base_solver.ml @@ -120,6 +120,7 @@ end) module Th_dyn_trans = Sidekick_th_dyn_trans.Make(struct module Solver = Solver type term = Solver.T.Term.t + let config = Sidekick_th_dyn_trans.default_config let term_as_eqn _tst t = match Term.view t with | Term.Eq(a,b) -> Some (a,b) diff --git a/src/th-dyn-trans/Sidekick_th_dyn_trans.ml b/src/th-dyn-trans/Sidekick_th_dyn_trans.ml index 14f62732..392e3044 100644 --- a/src/th-dyn-trans/Sidekick_th_dyn_trans.ml +++ b/src/th-dyn-trans/Sidekick_th_dyn_trans.ml @@ -1,9 +1,36 @@ +type config = { + (** Size of pool of clauses *) + cpool_size: int; + + (** only do dyn-trans if conflict has more than this many lits *) + min_confl_len : int; + + (** Max number of conflicts produced at once *) + max_batch_size : int; + + (** Bump activity of terms involved in transitivity steps in CC conflicts *) + activity_bump : float; + + (** Min activity of one side of an equation so it can participate in + a dyn-trans inference *) + min_activity : float; +} + +let default_config : config = { + cpool_size = (try int_of_string (Sys.getenv "CPOOL_SIZE") with _ -> 400); + min_confl_len = (try int_of_string (Sys.getenv "MIN_CONFL_LEN") with _ -> 4); + max_batch_size = (try int_of_string (Sys.getenv "MAX_BATCH_SIZE") with _ -> 2); + activity_bump = (try float_of_string (Sys.getenv "ACTIVITY_BUMP") with _ -> 1.1); + min_activity = (try float_of_string (Sys.getenv "MIN_ACTIVITY") with _ -> 1e12); +} module type ARG = sig module Solver : Sidekick_core.SOLVER type term = Solver.T.Term.t + val config : config + val term_as_eqn : Solver.T.Term.store -> term -> (term*term) option val mk_eqn : Solver.T.Term.store -> term -> term -> term @@ -68,16 +95,11 @@ module Make(A: ARG) (* CONFIG *) - let cpool_size = (try int_of_string (Sys.getenv "CPOOL_SIZE") with _ -> 400) - - (* only do dyn-trans if conflict has more than this many lits *) - let min_confl_len = (try int_of_string (Sys.getenv "MIN_CONFL_LEN") with _ -> 4) - - let max_batch_size = (try int_of_string (Sys.getenv "MAX_BATCH_SIZE") with _ -> 2) - - let activity_bump = (try float_of_string (Sys.getenv "ACTIVITY_BUMP") with _ -> 1.1) - - let min_activity = (try float_of_string (Sys.getenv "MIN_ACTIVITY") with _ -> 1e12) + let cpool_size = A.config.cpool_size + let min_confl_len = A.config.min_confl_len + let max_batch_size = A.config.max_batch_size + let activity_bump = A.config.activity_bump + let min_activity = A.config.min_activity let max_activity = min_activity *. (activity_bump ** 15.) let activity_decay = activity_bump ** (-13.)