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 holds the solver object used for
answering solver-aided queries. Rosette’s default solver is z3
new (SMT) solvers can be added well. Rosette will work with any solver that implements the
Returns true if v
is a concrete value that implements the gen:solver
Takes as input a list of boolean terms or values and
adds them to the current (top) level in the assertion stack.
Pushes a new level onto the solver’s assertion stack. Subsequent calls to
will add assertions to this level.
Pops the given number of levels off the solver’s assertion stack,
removing all the assertions at the popped levels. The number of levels
pop must be a positive integer that is no greater than the number of preceding
calls to solver-push
Clears the assertion stack of all levels and all assertions,
and removes all objectives from the current set of objectives to optimize.
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
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 model
it is returned in the form of a satisfiable (sat?
) solution, which optimizes
the objective terms added to the solver via solver-minimize
Otherwise, an unsatisfiable (unsat?
) solution is returned, but without
computing an unsatisfiable core
(i.e., calling core
resulting solution produces #f
Searches for an unsatisfiable core of all constraints (boolean terms)
added to the solver via solver-assert after
the most recent call to
If the constraints are satisfiable, or the given solver does
not support core extraction, an error is thrown. Otherwise, the result is an
solution with a unsatisfiable core
, expressed as a
list of boolean terms.
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
) after a shutdown call.
Returns a solver?
wrapper for the Z3
solver from Microsoft Research.
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:
Returns true if the given value is a solution.
Returns true if the given value is a satisfiable solution.
Returns true if the given value is an unsatisfiable solution.
Returns true if the given value is an unknown solution.
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.
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
Returns an unknown solution.
Returns the binding stored in the given satisfiable solution. The binding is an immutable
hashmap from symbolic constants to values.
Returns the unsatisfiable core stored in the given satisfiable solution. If the solution is
and a core was computed, the result is a list of boolean values that
are collectively unsatisfiable. Otherwise, the result is #f
Given a Rosette value and a satisfiable solution, evaluate
new value obtained by replacing every symbolic constant c
with (solution c)
and simplifying the result.