Module rsmt2::conf [−][src]
Solver configuration, contains backend-solver-specific info.
Do NOT use wildcards when matching over SmtStyle
. We want the code to fail to compile
whenever we add a solver. Likewise, do not use if let
with SmtStyle
.
Note that the command for each solver can be passed through environment variables, see
Z3_ENV_VAR
,CVC4_ENV_VAR
,YICES_2_ENV_VAR
, and- the
SmtConf::z3_or_env
,SmtConf::cvc4_or_env
, andSmtConf::yices_2_or_env
constructors.
Structs
SmtConf | Configuration and solver specific info. |
Enums
SmtStyle | Solver styles. |
Constants
CVC4_ENV_VAR | Environment variable providing the command for CVC4. |
YICES_2_ENV_VAR | Environment variable providing the command for Yices 2. |
Z3_ENV_VAR | Environment variable providing the command for z3. |
Type Definitions
ConfItem | A configuration item is either a keyword or unsupported. |