#### 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) → void? solver : solver?

> (current-solver) #<z3>

value

procedure

(solver-assert solver constraints) → void?

solver : solver? constraints : (listof boolean?)

procedure

(solver-push solver) → void?

solver : solver?

procedure

(solver-pop solver levels) → void?

solver : solver? levels : integer?

procedure

(solver-clear solver) → void?

solver : solver?

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?))

procedure

(solver-check solver) → solution?

solver : solver?

procedure

(solver-debug solver) → solution?

solver : solver?

procedure

(solver-shutdown solver) → void?

solver : solver?

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

##### 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:

> (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