Skip to content

Setups Overview

solverpy_learn.setups

Evalset

Bases: TypedDict

Per-dataset configuration: problems, strategies, and ML training state.

Source code in packages/solverpy/src/solverpy/setups/evalset.py 
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
class Evalset(TypedDict, total=False):
   """Per-dataset configuration: problems, strategies, and ML training state."""
   label: str
   benchmarks: list[str]
   strategies: list[str]
   bidfile: str
   sidfile: str
   refs: list[str]
   ref: bool | int | str | None
   limit: str
   cores: int
   binary: str
   static: list[str]
   complete: bool
   force: bool
   shuffle: bool
   solvedby: str
   max_proofs: int
   pool_context: str
   plugin: Any  # SvmTrains
   plugins: list["Plugin"]
   solver: "SolverPy"
   dataname: str
   basedataname: str
   previous_trains: str | tuple[str]
   proofs: dict[str, int] | None
   start_dataname: str

Setup

Bases: TypedDict

A (typed) dictionary summarizing the configuration of the experiment. An ordinary dictionary can be used in its place but type annotations provide additional safety.

Some parameters should be set by the user, others are automatically filled in by functions in the setups module.

Evaluation parameters

The following are the most important parameters to be set by the user for an evaluation run:

Attributes:

Name Type Description
limit str

Resource limit for solvers.
cores int

Number of CPU cores for parallel evaluation.
benchmarks int

List of benchmark ids.

strategies int

List of strategy ids.
complete bool

Complete use of the solver (sat/Satisfiable are successes).

The following parameters additional parameters for an evaluation run:

Attributes:

Name Type Description
ref

Reference strategy id.
binary str

Custom solver binary. Must be in PATH.
static list[str]

Fixed solver options.
ntfy str

Address for user push notifications via ntfy.
options list[str]

Experiment boolean options. An option is identified by its string name, and represents a boolean yes/no value. Use no-option, like no-compress, to set the option to no. Currently supported options are:

option description default
outputs Keep raw solver output files from all runs. no
compress Compress output files (outputs, trains, results). yes
flatten Put all output files in a single directory (replace / with _._). yes
compress-trains Compress trains. yes
debug-trains Dump training data for each file separately. no
proofs Store proof objects in the database. no
premises Store premise selections in the database. no
headless Suppress progress bars and interactive UI (for non-terminal use). no
plugins list[Plugin]

List of additional solver plugins.
delfix int | str | None

Prefix to remove from problem names.

  • If the value is of type str, then this prefix is removed from the beginning of every problem name.
  • If the value is of type int, then the problem name is expected to be a /-separated path, and the first delfix components are removed.
  • If the value None, nothing is removed.

The typical use is to remove the prefix problems/ from problem names when the problems are stored inside problems/ subdirectory. In that case, set delfix=1.

This applies to DB providers that support delfix (e.g. Solved and Status). The default value is None.

ML parameters

The following are user options for ML experiments.

Attributes:

Name Type Description
loops int

Number of iterations of the eval/ML loop.
force bool

Recompute everything.
shuffle bool

Shuffle problem order.
e_training_examples str

Output format of training samples for eprover.
gen_features str

ENIGMA features for generation filtering.
sel_features str

ENIGMA features for clause selection.
posneg_ratio float

Maximum ratio of negative to positive examples.
templates list[str]

Templates for strategy generation.
evals Evalset

Primary evaluation dataset configuration (Evalset with benchmarks, strategies, plugin, etc.).
devels Evalset

Development dataset configuration (Evalset).

Internal parameters

The following parameters are used internally and should not be set directly by the user.

Attributes:

Name Type Description
it int

Current iteration number.
news list[str]

New ML strategies.
db DB

Database object.
builder Any

Builder object.
Source code in packages/solverpy/src/solverpy/setups/setup.py 
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
class Setup(TypedDict, total=False):
   """
   A (typed) dictionary summarizing the configuration of the experiment.
   An ordinary dictionary can be used in its place but type annotations
   provide additional safety.

   Some parameters should be set by the user, others are automatically
   filled in by functions in the [`setups`][solverpy.setups] module.

   # Evaluation parameters

   The following are the most important parameters to be set by the user for an evaluation run:

   Attributes: 
       limit: Resource limit for solvers.
       cores: Number of CPU cores for parallel evaluation.
       benchmarks: List of benchmark ids. 
       strategies: List of strategy ids.
       complete: Complete use of the solver (sat/Satisfiable are successes).

   The following parameters additional parameters for an evaluation run:

   Attributes:
       ref: Reference strategy id.
       binary: Custom solver binary.  Must be in `PATH`.
       static: Fixed solver options.
       ntfy: Address for user push notifications via [ntfy](https://ntfy.sh).
       options: Experiment boolean options.
           An *option* is identified by its string name, and represents a boolean yes/no value.
           Use `no-`option, like `no-compress`, to set the option to `no`.
           Currently supported options are:

           |option|description|default|
           |------|-----------|-------|
           |`outputs`|Keep raw solver output files from all runs.|no|
           |`compress`|Compress output files (outputs, trains, results).|yes|
           |`flatten`|Put all output files in a single directory (replace `/` with `_._`).|yes|
           |`compress-trains`|Compress trains.|yes|
           |`debug-trains`|Dump training data for each file separately.|no|
           |`proofs`|Store proof objects in the database.|no|
           |`premises`|Store premise selections in the database.|no|
           |`headless`|Suppress progress bars and interactive UI (for non-terminal use).|no|

       plugins: List of additional solver plugins.
       delfix: 
           Prefix to remove from problem names.

           + If the value is of type `str`, then this prefix is removed from the
           beginning of every problem name.
           + If the value is of type `int`, then the problem name is expected to
           be a `/`-separated path, and the first `delfix` components are
           removed.
           + If the value `None`, nothing is removed.

           The typical use is to remove the prefix `problems/` from problem
           names when the problems are stored inside `problems/` subdirectory.
           In that case, set `delfix=1`.

           This applies to DB providers that support `delfix` (e.g.
           [`Solved`][solverpy.benchmark.db.providers.solved] and
           [`Status`][solverpy.benchmark.db.providers.status]).
           The default value is `None`.





   # ML parameters

   The following are user options for ML experiments.

   Attributes:
       loops: Number of iterations of the eval/ML loop.
       force: Recompute everything.
       shuffle: Shuffle problem order.
       e_training_examples: Output format of training samples for `eprover`.
       gen_features: ENIGMA features for generation filtering.
       sel_features: ENIGMA features for clause selection.
       posneg_ratio: Maximum ratio of negative to positive examples.
       templates: Templates for strategy generation.
       evals: Primary evaluation dataset configuration (Evalset with benchmarks, strategies, plugin, etc.).
       devels: Development dataset configuration (Evalset).

   # Internal parameters

   The following parameters are used internally and should not be set
   directly by the user.

   Attributes:
       it: Current iteration number.
       news: New ML strategies.
       db: Database object.
       builder: Builder object.
   """
   limit: str
   cores: int
   binary: str
   static: list[str]
   ntfy: str
   it: int
   loops: int
   news: list[str]
   options: list[str]
   common: dict[str, Any]
   delfix: (int | str | None)
   complete: bool

   force: bool
   shuffle: bool

   db: "DB"
   builder: Any  # set by solverpy_learn
   talker: "Talker"
   reloader: bool
   evals: "Evalset"  # primary evaluation dataset (set by solverpy_learn or evaluation())
   devels: "Evalset"  # development dataset (set by solverpy_learn)
   plugins: list["Plugin"]
   e_training_examples: str
   gen_features: str
   sel_features: str
   posneg_ratio: float
   posneg_weight: float
   templates: list[str]
   chunk_size: int  # rows per NPZ chunk when compressing SVM-Light trains (default 1_000_000)
   pool_context: str  # multiprocessing start method for the evaluation pool (default "forkserver")

bitwuzla(setup: Setup) -> Setup

Configure setup to use the Bitwuzla solver.

Source code in packages/solverpy/src/solverpy/setups/solver.py 
95
96
97
98
def bitwuzla(setup: Setup) -> Setup:
   """Configure `setup` to use the [`Bitwuzla`][solverpy.solver.smt.bitwuzla.Bitwuzla] solver."""
   init(setup)
   return _evalset_solvers(setup, Bitwuzla, BWZ_STATIC.split())

cvc5ml(setup: Setup, tuneargs: dict[str, Any] | None = None) -> Setup

Configure setup with a Cvc5ML builder.

Source code in packages/solverpy-learn/src/solverpy_learn/setups/tuner.py 
46
47
48
49
50
51
52
def cvc5ml(
   setup: Setup,
   tuneargs: (dict[str, Any] | None) = None,
) -> Setup:
   """Configure `setup` with a [`Cvc5ML`][solverpy_learn.builder.cvc5ml.Cvc5ML] builder."""
   defaultweight(setup, tuneargs)
   return autotuner(Cvc5ML, setup, tuneargs)

enigma(setup: Setup, tunesel: dict[str, Any] | None = None, tunegen: dict[str, Any] | None = None) -> Setup

Configure setup with an Enigma builder.

Source code in packages/solverpy-learn/src/solverpy_learn/setups/tuner.py 
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
def enigma(
   setup: Setup,
   tunesel: (dict[str, Any] | None) = None,
   tunegen: (dict[str, Any] | None) = None,
) -> Setup:
   """Configure `setup` with an [`Enigma`][solverpy_learn.builder.enigma.Enigma] builder."""
   default(setup, "templates", None)
   defaultweight(setup, tunesel)
   defaultweight(setup, tunegen)
   assert "templates" in setup
   return autotuner(
      Enigma,
      setup,
      tunesel,
      tunegen,
      templates=setup["templates"],
   )

evaluation(setup: Setup) -> Setup

Configure setup for benchmark evaluation: DB, cores, strategies, and benchmarks.

Source code in packages/solverpy/src/solverpy/setups/loop.py 
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
def evaluation(setup: Setup) -> Setup:
   """Configure `setup` for benchmark evaluation: DB, cores, strategies, and benchmarks."""
   def configure_evalset(evalset: Evalset) -> None:
      default(evalset, "ref", True)
      if "strategies" not in evalset:
         default(evalset, "sidfile", "sids")
         with open(evalset["sidfile"]) as f:
            evalset["strategies"] = f.read().strip().split("\n")
      if "benchmarks" not in evalset:
         default(evalset, "bidfile", "bids")
         with open(evalset["bidfile"]) as f:
            evalset["benchmarks"] = f.read().strip().split("\n")

   def check_list(evalset: Evalset, key: str, fun: Callable) -> None:
      if key not in evalset:
         return
      for id in evalset[key]:
         try:
            fun(id)
         except Exception as e:
            logger.error(f"Wrong id in {key}: {id}")
            logger.error(f"Exception: {e}")
            sys.exit(0)

   default(setup, "cores", 4)
   default(setup, "delfix", None)
   assert "delfix" in setup
   default(setup, "db", db.default(delfix=setup["delfix"]))
   default(setup, "ntfy", None)

   for key in ("evals", "devels"):
      if key not in setup:
         continue
      evalset = setup[key]
      configure_evalset(evalset)
      check_list(evalset, "strategies", sids.load)
      check_list(evalset, "refs", sids.load)
      check_list(evalset, "benchmarks", bids.problems)
   return setup

experiment(setup: Setup) -> Setup

Normalize a user-facing setup before evaluation or looping starts.

Source code in packages/solverpy/src/solverpy/setups/loop.py 
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
def experiment(setup: Setup) -> Setup:
   """Normalize a user-facing setup before evaluation or looping starts."""
   common = setup.pop("common", {})
   if "evals" in setup and "trains" in setup:
      if setup["evals"] != setup["trains"]:
         raise ValueError("Use either 'evals' or 'trains', not both.")
      setup.pop("trains")
   elif "trains" in setup:
      setup["evals"] = setup.pop("trains")

   for key in ("evals", "devels"):
      if key not in setup:
         continue
      evalset = setup[key]
      setup[key] = Evalset(common, **evalset)
   return setup

initialize(setup: Setup) -> Runtime

Initialize all Managed plugins in the setup with a shared Manager.

Source code in packages/solverpy/src/solverpy/setups/runtime.py 
35
36
37
38
39
40
41
42
def initialize(setup: Setup) -> Runtime:
   """Initialize all Managed plugins in the setup with a shared Manager."""
   configured = list(setup.get("plugins", []))
   for key in ("evals", "devels"):
      if key in setup:
         configured.extend(setup[key].get("plugins", []))
   plugins = [p for p in configured if isinstance(p, Managed)]
   return Runtime(plugins)

prover9(setup: Setup) -> Setup

Configure setup to use the Prover9 solver.

Source code in packages/solverpy/src/solverpy/setups/solver.py 
89
90
91
92
def prover9(setup: Setup) -> Setup:
   """Configure `setup` to use the [`Prover9`][solverpy.solver.atp.prover9.Prover9] solver."""
   init(setup)
   return _evalset_solvers(setup, Prover9)

vampire(setup: Setup) -> Setup

Configure setup to use the Vampire solver.

Source code in packages/solverpy/src/solverpy/setups/solver.py 
83
84
85
86
def vampire(setup: Setup) -> Setup:
   """Configure `setup` to use the [`Vampire`][solverpy.solver.atp.vampire.Vampire] solver."""
   init(setup)
   return _evalset_solvers(setup, Vampire, V_STATIC.split())

z3(setup: Setup) -> Setup

Configure setup to use the Z3 solver.

Source code in packages/solverpy/src/solverpy/setups/solver.py 
101
102
103
104
105
106
107
108
109
def z3(setup: Setup) -> Setup:
   """Configure `setup` to use the [`Z3`][solverpy.solver.smt.z3.Z3] solver."""
   init(setup)
   # No static: `Z3` is a `StdinSolver`, where `static` is the prefix of the
   # stdin payload and not the command line.  `Z3_STATIC` is already baked
   # into the command by `Z3.__init__`, and passing it here as well sent
   # `-smt2 -st` down the SMT-LIB2 stream, so every z3 run answered with a
   # leading `(error "line 1 column 1: invalid command, '(' expected")`.
   return _evalset_solvers(setup, Z3)