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
z3
4.9.2 Solutions
solution?
sat?
unsat?
unknown?
sat
unsat
unknown
model
core
evaluate
6.6

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 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, and solver-shutdown. 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.

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

procedure

(z3)  solver?

Returns a solver? wrapper for the Z3 solver from Microsoft Research.

4.9.2 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