Module rsmt2::conf

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, and SmtConf::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.