On this page:
4.9.1 The Solver Interface
current-solver
gen:  solver
solver?
solver-assert
solver-push
solver-pop
solver-clear
solver-minimize
solver-maximize
solver-check
solver-debug
solver-shutdown
solver-features
solver-options
output-smt
4.9.2 Supported Solvers
4.9.2.1 Z3
z3
z3?
4.9.2.2 CVC4
cvc4
cvc4?
cvc4-available?
4.9.2.3 Boolector
boolector
boolector?
boolector-available?
4.9.2.4 Yices
yices
yices?
yices-available?
4.9.2.5 CPLEX
cplex
cplex?
cplex-available?
solver-check-with-init
4.9.3 Solutions
solution?
sat?
unsat?
unknown?
sat
unsat
unknown
model
core
evaluate
complete-solution
7.1

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.

parameter

(current-solver)  solver?

(current-solver solver)  void?
  solver : solver?
The current-solver parameter holds the solver object used for answering solver-aided queries. Rosette’s default solver is z3, although new (SMT) solvers can be added as well. Rosette will work with any solver that implements the gen:solver generic interface.

Example:

A generic interface that specifies the procedures provided by a solver. These include solver-assert, solver-push, solver-pop, solver-clear, solver-minimize, solver-maximize, solver-check, solver-debug, solver-shutdown, and solver-features. A solver may support a subset of this interface, which loosely follows the SMTLib solver interface.

procedure

(solver? v)  boolean?

  v : any/c
Returns true if v is a concrete value that implements the gen:solver interface.

procedure

(solver-assert solver constraints)  void?

  solver : solver?
  constraints : (listof boolean?)
Takes as input a list of boolean terms or values and adds them to the current (top) level in the assertion stack.

procedure

(solver-push solver)  void?

  solver : solver?
Pushes a new level onto the solver’s assertion stack. Subsequent calls to solver-assert will add assertions to this level.

procedure

(solver-pop solver levels)  void?

  solver : solver?
  levels : integer?
Pops the given number of levels off the solver’s assertion stack, removing all the assertions at the popped levels. The number of levels to pop must be a positive integer that is no greater than the number of preceding calls to solver-push.

procedure

(solver-clear solver)  void?

  solver : solver?
Clears the assertion stack of all levels and all assertions, and removes all objectives from the current set of objectives to optimize.

procedure

(solver-minimize solver objs)  void?

  solver : solver?
  objs : (listof (or/c integer? real? bv?))
(solver-maximize solver objs)  void?
  solver : solver?
  objs : (listof (or/c integer? real? bv?))
Adds the given optimization objectives to the given solver. These objectives take the form of numeric terms whose value is to be minimized or maximized by subsequent calls to solver-check, while satisfying all the boolean terms asserted via solver-assert.

procedure

(solver-check solver)  solution?

  solver : solver?
Searches for a binding from symbolic constants to concrete values that satisfies all constraints (boolean terms) added to the solver via solver-assert. If such a binding—or, a modelexists, it is returned in the form of a satisfiable (sat?) solution, which optimizes the objective terms added to the solver via solver-minimize and solver-maximize. Otherwise, an unsatisfiable (unsat?) solution is returned, but without computing an unsatisfiable core (i.e., calling core on the resulting solution produces #f).

procedure

(solver-debug solver)  solution?

  solver : solver?
Searches for an unsatisfiable core of all constraints (boolean terms) added to the solver via solver-assert after the most recent call to clear or solver-check (if any). If the constraints are satisfiable, or the given solver does not support core extraction, an error is thrown. Otherwise, the result is an unsat? solution with a unsatisfiable core, expressed as a list of boolean terms.

procedure

(solver-shutdown solver)  void?

  solver : solver?
Terminates the current solving process (if any), clears all added constraints, and releases all system resources associated with the given solver instance. The solver must be able to reacquire these resources if needed. That is, the solver should behave as though its state was merely cleared (via solver-clear) after a shutdown call.

procedure

(solver-features solver)  (listof symbol?)

  solver : solver?
Returns the list of features supported by the solver. The possible features, which correspond roughly to SMTLib logics, extended with some additional options, are:

procedure

(solver-options solver)  (hash/c symbol? any/c)

  solver : solver?
Returns the options the given solver is configured with (as specified by the #:options argument to solver constructors).

parameter

(output-smt)  (or/c boolean? path-string? output-port?)

(output-smt on?)  void?
  on? : (or/c boolean? path-string? output-port?)
Enables verbose output of generated SMT constraints.

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

 (require rosette/solver/smt/z3) package: rosette

procedure

(z3 [#:path path    
  #:logic logic    
  #:options options])  solver?
  path : (or/c path-string? #f) = #f
  logic : (or/c symbol? #f) = #f
  options : (hash/c symbol? any/c) = (hash)
(z3? v)  boolean?
  v : any/c
Returns a solver? wrapper for the Z3 solver from Microsoft Research. Rosette automatically installs a version of Z3; the optional path argument overrides this version with a path to a new Z3 binary.

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

 (require rosette/solver/smt/cvc4) package: rosette

procedure

(cvc4 [#:path path    
  #:logic logic    
  #:options options])  solver?
  path : (or/c path-string? #f) = #f
  logic : (or/c symbol? #f) = #f
  options : (hash/c symbol? any/c) = (hash)
(cvc4? v)  boolean?
  v : any/c
Returns a solver? wrapper for the CVC4 solver from NYU and UIowa.

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.

procedure

(cvc4-available?)  boolean?

Returns true if the CVC4 solver is available for use (i.e., Rosette can locate a cvc4 binary). If this returns #f, (cvc4) will not succeed without its optional path argument.

4.9.2.3 Boolector

 (require rosette/solver/smt/boolector) package: rosette

procedure

(boolector [#:path path    
  #:logic logic    
  #:options options])  solver?
  path : (or/c path-string? #f) = #f
  logic : (or/c symbol? #f) = #f
  options : (hash/c symbol? any/c) = (hash)
(boolector? v)  boolean?
  v : any/c
Returns a solver? wrapper for the Boolector solver from JKU.

To use this solver, download and install Boolector, 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.

Returns true if the Boolector solver is available for use (i.e., Rosette can locate a boolector binary). If this returns #f, (boolector) will not succeed without its optional path argument.

4.9.2.4 Yices

 (require rosette/solver/smt/yices) package: rosette

procedure

(yices [#:path path    
  #:logic logic    
  #:options options])  solver?
  path : (or/c path-string? #f) = #f
  logic : symbol? = 'ALL
  options : (hash/c symbol? any/c) = (hash)
(yices? v)  boolean?
  v : any/c
Returns a solver? wrapper for the Yices solver from SRI.

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.

procedure

(yices-available?)  boolean?

Returns true if the yices solver is available for use (i.e., Rosette can locate a yices-smt2 binary). If this returns #f, (yices) will not succeed without its optional path argument.

4.9.2.5 CPLEX

 (require rosette/solver/mip/cplex) package: rosette

procedure

(cplex [#:path path #:options options])  solver?

  path : (or/c path-string? #f) = #f
  options : (hash/c symbol? any/c) = (hash)
(cplex? v)  boolean?
  v : any/c
Returns a solver? wrapper for the CPLEX solver from IBM.

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.

procedure

(cplex-available?)  boolean?

Returns true if the CPLEX solver is available for use (i.e., Rosette can locate a cplex binary). If this returns #f, (cplex) will not succeed without its optional path argument.

procedure

(solver-check-with-init solver 
  [#:mip-sol final-solution-file 
  #:mip-start initial-solution-file]) 
  solution?
  solver : cplex?
  final-solution-file : (or/c path-string? #f) = #f
  initial-solution-file : (or/c path-string? #f) = #f
Like solver-check, but accepts only a CPLEX solver, and takes optional arguments final-solution-file and/or initial-solution-file. When final-solution-file is a path-string?, the solver will save the solution to the given file in MST format if a solution exists. This file can be used as the initial-solution-file in a later call to solver-check-with-init to provide starting values for variables. Note that initial-solution-file does not have to be a satisfiable solution, but it must be in MST format.

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:

procedure

(solution? value)  boolean?

  value : any/c
Returns true if the given value is a solution.

procedure

(sat? value)  boolean?

  value : any/c
Returns true if the given value is a satisfiable solution.

procedure

(unsat? value)  boolean?

  value : any/c
Returns true if the given value is an unsatisfiable solution.

procedure

(unknown? value)  boolean?

  value : any/c
Returns true if the given value is an unknown solution.

procedure

(sat)  sat?

(sat binding)  sat?
  binding : (hash/c constant? any/c #:immutable #t)
Returns a satisfiable solution that holds the given binding from symbolic constants to values, or that holds the empty binding. The provided hash must bind every symbolic constant in its keyset to a concrete value of the same type.

procedure

(unsat)  unsat?

(unsat constraints)  unsat?
  constraints : (listof boolean?)
Returns an unsatisfiable solution. The constraints list, if provided, consist of boolean values that are collectively unsatisfiable. If no constraints are provided, applying core to the resulting solution produces #f, indicating that there is no satisfying solution but core extraction was not performed. (Core extraction is an expensive operation that is not supported by all solvers; those that do support it usually don’t compute a core unless explicitly asked for one via solver-debug.)

procedure

(unknown)  unknown?

Returns an unknown solution.

procedure

(model solution)  (hash/c constant? any/c #:immutable #t)

  solution : sat?
Returns the binding stored in the given satisfiable solution. The binding is an immutable hashmap from symbolic constants to values.

procedure

(core solution)  (or/c (listof (and/c constant? boolean?)) #f)

  solution : unsat?
Returns the unsatisfiable core stored in the given satisfiable solution. If the solution is unsat? and a core was computed, the result is a list of boolean values that are collectively unsatisfiable. Otherwise, the result is #f.

procedure

(evaluate v solution)  any/c

  v : any/c
  solution : sat?
Given a Rosette value and a satisfiable solution, evaluate produces a new value obtained by replacing every symbolic constant c in v with (solution c) and simplifying the result.

Examples:
> (define-symbolic a b boolean?)
> (define-symbolic x y integer?)
> (define sol
    (solve (begin (assert a)
                  (assert (= x 1))
                  (assert (= y 2)))))
> (sat? sol)

#t

> (evaluate (list 4 5 x) sol)

'(4 5 1)

> (define vec (vector a))
> (evaluate vec sol)

'#(#t)

> (eq? vec (evaluate vec sol)) ; evaluation produces a new vector

#f

> (evaluate (+ x y) sol)

3

> (evaluate (and a b) sol)

b

procedure

(complete-solution sol consts)  solution?

  sol : solution?
  consts : (listof constant?)
Given a solution sol and a list of symbolic constants consts, returns a solution that is complete with respect to the given list. In particular, if sol is satisfiable, the returned solution is also satisfiable, and it extends the sol model with default bindings for all constants in consts that are not bound by sol. Otherwise, sol itself is returned.

Examples:
> (define-symbolic a boolean?)
> (define-symbolic x integer?)
> (define sol (solve (assert a)))
> sol ; no binding for x

(model

 [a #t])

> (complete-solution sol (list a x))

(model

 [a #t]

 [x 0])

> (complete-solution (solve (assert #f)) (list a x))

(unsat)