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 as well as the CPLEX mixed-integer programming solver. 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, 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 Yices

To use this solver, download and install Yices (version 2.6.0 or later), and either add the yices-smt2 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 'ALL.

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

4.9.2.5 CPLEX

To use this solver, download and install CPLEX, and locate the CPLEX interactive executable, which is likely to be at CPLEX_Studio*/cplex/bin/x86-64*/cplex. Either add this directory to your PATH, or pass the path to the executable as the path argument.

The options argument provides additional options for configuring CPLEX. Setting the key 'timeout in options to an integer controls the solving timeout in seconds. Setting the key 'verbose in options to #t displays detailed output from the CPLEX solver.

The assertions given to solver-assert must be linear in order to use the CPLEX solver. Otherwise, an exn:fail exception is raised.

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: