simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-28 12:24:50 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

feat(dyn-trans): provide config record when instantiating theory

Browse source
This commit is contained in:
Simon Cruanes 2021-09-24 22:44:52 -04:00
parent 5f51863cd3
commit 697678d6d2
No known key found for this signature in database
GPG key ID: 4AC01D0849AA62B6
2 changed files with 33 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/base-solver/sidekick_base_solver.ml
View file

@ -120,6 +120,7 @@ end)
module Th_dyn_trans = Sidekick_th_dyn_trans.Make(struct module Th_dyn_trans = Sidekick_th_dyn_trans.Make(struct
module Solver = Solver module Solver = Solver
type term = Solver.T.Term.t type term = Solver.T.Term.t
let config = Sidekick_th_dyn_trans.default_config
let term_as_eqn _tst t = let term_as_eqn _tst t =
match Term.view t with match Term.view t with
| Term.Eq(a,b) -> Some (a,b) | Term.Eq(a,b) -> Some (a,b)

42
src/th-dyn-trans/Sidekick_th_dyn_trans.ml
View file

@ -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 type ARG = sig
module Solver : Sidekick_core.SOLVER module Solver : Sidekick_core.SOLVER
type term = Solver.T.Term.t type term = Solver.T.Term.t
val config : config
val term_as_eqn : Solver.T.Term.store -> term -> (term*term) option val term_as_eqn : Solver.T.Term.store -> term -> (term*term) option
val mk_eqn : Solver.T.Term.store -> term -> term -> term val mk_eqn : Solver.T.Term.store -> term -> term -> term
@ -68,16 +95,11 @@ module Make(A: ARG)
(* CONFIG *) (* CONFIG *)
let cpool_size = (try int_of_string (Sys.getenv "CPOOL_SIZE") with _ -> 400) let cpool_size = A.config.cpool_size
let min_confl_len = A.config.min_confl_len
(* only do dyn-trans if conflict has more than this many lits *) let max_batch_size = A.config.max_batch_size
let min_confl_len = (try int_of_string (Sys.getenv "MIN_CONFL_LEN") with _ -> 4) let activity_bump = A.config.activity_bump
let min_activity = A.config.min_activity
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 max_activity = min_activity *. (activity_bump ** 15.) let max_activity = min_activity *. (activity_bump ** 15.)
let activity_decay = activity_bump ** (-13.) let activity_decay = activity_bump ** (-13.)