mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-08 12:15:48 -05:00
fix docstrings
This commit is contained in:
parent
697678d6d2
commit
1f5806244e
1 changed files with 5 additions and 5 deletions
|
|
@ -1,20 +1,20 @@
|
||||||
|
|
||||||
type config = {
|
type config = {
|
||||||
(** Size of pool of clauses *)
|
|
||||||
cpool_size: int;
|
cpool_size: int;
|
||||||
|
(** Size of pool of clauses *)
|
||||||
|
|
||||||
(** only do dyn-trans if conflict has more than this many lits *)
|
|
||||||
min_confl_len : int;
|
min_confl_len : int;
|
||||||
|
(** only do dyn-trans if conflict has more than this many lits *)
|
||||||
|
|
||||||
(** Max number of conflicts produced at once *)
|
|
||||||
max_batch_size : int;
|
max_batch_size : int;
|
||||||
|
(** Max number of conflicts produced at once *)
|
||||||
|
|
||||||
(** Bump activity of terms involved in transitivity steps in CC conflicts *)
|
|
||||||
activity_bump : float;
|
activity_bump : float;
|
||||||
|
(** Bump activity of terms involved in transitivity steps in CC conflicts *)
|
||||||
|
|
||||||
|
min_activity : float;
|
||||||
(** Min activity of one side of an equation so it can participate in
|
(** Min activity of one side of an equation so it can participate in
|
||||||
a dyn-trans inference *)
|
a dyn-trans inference *)
|
||||||
min_activity : float;
|
|
||||||
}
|
}
|
||||||
|
|
||||||
let default_config : config = {
|
let default_config : config = {
|
||||||
|
|
|
||||||
Loading…
Add table
Reference in a new issue