4.9 Solvers and Solutions🔗ℹ

A solver is an automatic reasoning engine, used to answer queries about Rosette programs. The result of a solver invocation is a solution, containing either a binding of symbolic constants to concrete values, or an unsatisfiable core. Solvers and solutions may not be symbolic. Two solvers (resp. solutions) are eq?/equal? if they refer to the same object.

4.9.1 The Solver Interface🔗ℹ

A solver contains a stack of assertions (boolean terms) to satisfy and a set of objectives (numeric terms) to optimize. The assertion stack is partitioned into levels, with each level containing a set of assertions. The bottom (0) assertion level cannot be removed, but more levels can be created and removed using the solver-push and solver-pop procedures. The solver-assert procedure adds assertions to the top level of the assertion stack, while the solver-minimize and solver-maximize procedures add new terms to the current set of optimization objectives. The solver-check procedure checks the satisfiability of all assertions in the assertion stack, optimizing the resulting solution (if any) with respect to the provided objectives.

• 'qf_bv (quantifier-free fixed-width bitvectors)

• 'qf_uf (quantifier-free uninterpreted functions and equality)

• 'qf_lia (quantifier-free linear integer arithmetic)

• 'qf_nia (quantifier-free non-linear integer arithmetic)

• 'qf_lra (quantifier-free linear real arithmetic)

• 'qf_nra (quantifier-free non-linear real arithmetic)

• 'quantifiers (quantified versions of the supported quantifier-free logics)

• 'optimize (support for objective function optimization)

• 'unsat-cores (unsatisfiable core generation)

When the output-smt parameter is #t or a path-string?, Rosette will log the SMT encoding of all solver queries to temporary files. A new temporary file is created for each solver process Rosette spawns. Note that a single solver-aided query may spawn multiple solver processes, and Rosette may reuse a solver process across several solver-aided queries. When output-smt is #t, the temporary files are created in the system’s temporary directory; otherwise, the temporary files are created in the given path (which must be a directory). The path to each temporary file is printed to current-error-port when it is first created.

When the output-smt parameter is an output-port?, Rosette will log the SMT encoding to that output port. For example, setting output-smt to (current-output-port) will print the SMT encoding to standard output. All solvers will log to the same output port, so several separate encodings may be interleaved when multiple solvers are in use.

Default value is #f.

4.9.2 Supported Solvers🔗ℹ

Rosette supports several SMT solvers. The current-solver parameter controls the solver used for answering solver-aided queries. Each supported solver is contained in a separate module (e.g., rosette/solver/smt/z3), which exports a constructor (e.g., z3) to create a new solver instance.

4.9.2.1 Z3🔗ℹ

The optional logic argument specifies an SMT logic for the solver to use (e.g., 'QF_BV). Specifying a logic can improve solving performance, but Rosette makes no effort to check that emitted constraints fall within the chosen logic. The default is #f, which uses Z3’s default logic.

The options argument provides additional options that are sent to Z3 via the set-option SMT command. For example, setting options to (hash ':smt.relevancy 0) will send the command (set-option :smt.relevancy 0) to Z3 prior to solving.

4.9.2.2 CVC4🔗ℹ

To use this solver, download and install CVC4 (version 1.8 or later), and either add the cvc4 executable to your PATH or pass the path to the executable as the optional path argument.

The optional logic argument specifies an SMT logic for the solver to use (e.g., 'QF_BV). Specifying a logic can improve solving performance, but Rosette makes no effort to check that emitted constraints fall within the chosen logic. The default is #f, which uses CVC4’s default logic.

The options argument provides additional options that are sent to CVC4 via the set-option SMT command. For example, setting options to (hash ':bv-propagate 'true) will send the command (set-option :bv-propagate true) to CVC4 prior to solving.

4.9.2.3 Boolector🔗ℹ

To use this solver, download and install Boolector (version 2.4.1 or later), and either add the boolector executable to your PATH or pass the path to the executable as the optional path argument.

The optional logic argument specifies an SMT logic for the solver to use (e.g., 'QF_BV). Specifying a logic can improve solving performance, but Rosette makes no effort to check that emitted constraints fall within the chosen logic. The default is #f, which uses Boolector’s default logic.

The options argument provides additional options that are sent to Boolector via the set-option SMT command. For example, setting options to (hash ':seed 5) will send the command (set-option :seed 5) to Boolector prior to solving.

4.9.2.4 Bitwuzla🔗ℹ

To use this solver, download prebuilt Bitwuzla or build it yourself, and ensure the executable is on your PATH or pass the path to the executable as the optional path argument. Rosette currently tests Bitwuzla at commit 93a3d930f622b4cef0063215e63b7c3bd10bd663.

The optional logic argument specifies an SMT logic for the solver to use (e.g., 'QF_BV). Specifying a logic can improve solving performance, but Rosette makes no effort to check that emitted constraints fall within the chosen logic. The default is #f, which uses Bitwuzla’s default logic.

The options argument provides additional options that are sent to Bitwuzla via the set-option SMT command. For example, setting options to (hash ':seed 5) will send the command (set-option :seed 5) to Bitwuzla prior to solving.

4.9.2.5 CVC5🔗ℹ

To use this solver, download prebuilt CVC5 or build it yourself, and ensure the executable is on your PATH or pass the path to the executable as the optional path argument. Rosette currently tests CVC5 at version 1.0.7.

The optional logic argument specifies an SMT logic for the solver to use (e.g., 'QF_BV). Specifying a logic can improve solving performance, but Rosette makes no effort to check that emitted constraints fall within the chosen logic. The default is #f, which uses CVC5’s default logic.

The options argument provides additional options that are sent to CVC5 via the set-option SMT command. For example, setting options to (hash ':seed 5) will send the command (set-option :seed 5) to CVC5 prior to solving.

4.9.2.6 STP🔗ℹ

To use this solver, download prebuilt STP or build it yourself, and ensure the executable is on your PATH or pass the path to the executable as the optional path argument. Rosette currently tests STP at commit 0510509a85b6823278211891cbb274022340fa5c. Note that as of December 2023, the STP version on Mac Homebrew is too old to be supported by Rosette.

The optional logic argument specifies an SMT logic for the solver to use (e.g., 'QF_BV). Specifying a logic can improve solving performance, but Rosette makes no effort to check that emitted constraints fall within the chosen logic. The default is #f, which uses STP’s default logic.

The options argument provides additional options that are sent to STP via the set-option SMT command. For example, setting options to (hash ':seed 5) will send the command (set-option :seed 5) to STP prior to solving.

4.9.2.7 Yices2🔗ℹ

To use this solver, download prebuilt Yices2 or build it yourself, and ensure the executable is on your PATH or pass the path to the executable as the optional path argument. Rosette specifically uses the yices-smt2 executable, which is the Yices2 solver with its SMTLIB2 frontend enabled. Note that just building (without installing) Yices2 will produce an executable named yices_smt2. Running the installation step produces an executable with the correct name. However, it is safe to skip the installation step and simply rename or symlink the yices_smt2 executable to yices-smt2. Rosette currently tests Yices2 at commit e27cf308cffb0ecc6cc7165c10e81ca65bc303b3.

The optional logic argument specifies an SMT logic for the solver to use (e.g., 'QF_BV). Specifying a logic can improve solving performance, but Rosette makes no effort to check that emitted constraints fall within the chosen logic. Yices2 expects a logic to be set; Rosette defaults to 'QF_BV.

The options argument provides additional options that are sent to Yices2 via the set-option SMT command. For example, setting options to (hash ':seed 5) will send the command (set-option :seed 5) to Yices2 prior to solving.

4.9.3 Solutions🔗ℹ

A solution to a set of formulas may be satisfiable (sat?), unsatisfiable (unsat?), or unknown (unknown?). A satisfiable solution can be used as a procedure: when applied to a bound symbolic constant, it returns a concrete value for that constant; when applied to any other value, it returns the value itself. The solver returns an unknown? solution if it cannot determine whether the given constraints are satisfiable or not.

A solution supports the following operations: