3.2 Solver-Aided Forms

7.7

3.2 Solver-Aided Forms

The Essentials chapter introduced the key concepts of solver-aided programming. This section defines the corresponding syntactic constructs more precisely.

3.2.1 Symbolic Constants

syntax
(define-symbolic id ...+ type)

type : (and/c solvable? type?)

Binds each provided identifier to a distinct symbolic constant of the given solvable type. The identifiers are bound to the same constants every time the form is evaluated.

Examples:

> (define (always-same)
(define-symbolic x integer?)
x)
> (always-same)
x
> (always-same)
x
> (eq? (always-same) (always-same))
#t

syntax
(define-symbolic* id ...+ type)

type : (and/c solvable? type?)

Creates a stream of distinct symbolic constants of the given solvable type for each identifier, binding the identifier to the next element from its stream every time the form is evaluated.

Examples:

> (define (always-different)
(define-symbolic* x integer?)
x)
> (always-different)
x$0
> (always-different)
x$1
> (eq? (always-different) (always-different))
(= x$2 x$3)

3.2.2 Assertions

syntax
(assert expr maybe-message)

maybe-message =
| msg

msg : (or/c string? procedure?)

Provides a mechanism for communicating desired program properties to the underlying solver. Rosette keeps track of all assertions evaluated during an execution in an assertion store. If expr evaluates to #f, an error is thrown using the optional failure message, and #f is added to the assertion store. The error message can be either a string or a no-argument procedure that throws an error when called. If expr evaluates to a symbolic boolean value, that value is added to the assertion store. If expr evaluates to any other value, assert has no effect. The contents of the assertion store can be examined using the asserts procedure, and they can be cleared using the clear-asserts! procedure.

Examples:

> (assert #t) ; no effect
> (assert 1)  ; no effect
> (asserts)   ; retrieve the assertion store
'()
> (define-symbolic x boolean?)
> (assert x)
> (asserts)   ; x added to the assertion store
'(x)
> (assert #f "bad value")
assert: bad value
> (asserts)
'(#f x)
> (clear-asserts!)   ; clear the assertion store
> (asserts)
'()

3.2.3 Angelic Execution

syntax
(solve expr)

Searches for a binding of symbolic constants to concrete values that satisfies all assertions encountered before the invocation of solve and during the evaluation of expr. If such a binding exists, it is returned in the form of a satisfiable solution?; otherwise, the result is an unsatisfiable solution. The assertions encountered while evaluating expr are removed from the global assertion store once solve returns. As a result, solve has no observable effect on the assertion store. The solver’s ability to find solutions depends on the current reasoning precision, as determined by the current-bitwidth parameter.

Examples:

> (define-symbolic x y boolean?)
> (assert x)
> (asserts) ; x added to the assertion store
'(x)
> (define sol (solve (assert y)))
> (asserts) ; assertion store same as before
'(x)
> (evaluate x sol) ; x must be true
#t
> (evaluate y sol) ; y must be true
#t
> (solve (assert (not x)))
(unsat)

procedure
(solve+) → procedure?

Returns a stateful procedure that uses a fresh solver? instance to incrementally solve a sequence of constraints (with respect to current-bitwidth).

The returned procedure consumes a constraint (i.e., a boolean value or symbolic term), a positive integer, or the symbol 'shutdown.

If the argument is a constraint, it is pushed onto the solver’s constraint stack and a solution for all constraints on the stack is returned.

If the argument is a positive integer k, then the top k constraints are popped from the solver’s constraint stack and the result is the solution to the remaining constraints.

If the argument is 'shutdown, all resources used by the procedure are released, and any subsequent calls to the procedure throw an exception.

Examples:

> (define-symbolic x y integer?)
> (define inc (solve+))
> (inc (< x y))   ; push (< x y) and solve
(model
[x 0]
[y 1])
> (inc (> x 5))   ; push (> x 5) and solve
(model
[x 6]
[y 7])
> (inc (< y 4))   ; push (< y 4) and solve
(unsat)
> (inc 1)         ; pop (< y 4) and solve
(model
[x 6]
[y 7])
> (inc (< y 9))   ; push (< y 9) and solve
(model
[x 6]
[y 7])
> (inc 'shutdown) ; release resources
> (inc (> y 4))   ; unusable
solver-push: contract violation:
expected: solver?
given: #f
argument position: 1st

3.2.4 Verification

syntax
(verify guarantee-expr)
(verify #:assume assume-expr #:guarantee guarantee-expr)

Searches for a binding of symbolic constants to concrete values that violates at least one of the assertions encountered during the evaluation of guarantee-expr, but that satisfies all assertions encountered before the invocation of verify and during the evaluation of assume-expr. If such a binding exists, it is returned in the form of a satisfiable solution?; otherwise, the result is an unsatisfiable solution. The assertions encountered while evaluating assume-expr and guarantee-expr are removed from the global assertion store once verify returns. The solver’s ability to find solutions depends on the current reasoning precision, as determined by the current-bitwidth parameter.

Examples:

> (define-symbolic x y boolean?)
> (assert x)
> (asserts) ; x added to the assertion store
'(x)
> (define sol (verify (assert y)))
> (asserts) ; assertion store same as before
'(x)
> (evaluate x sol) ; x must be true
#t
> (evaluate y sol) ; y must be false
#f
> (verify #:assume (assert y) #:guarantee (assert (and x y)))
(unsat)

3.2.5 Synthesis

syntax
(synthesize input-expr expr)
(synthesize
#:forall input-expr
maybe-assume
#:guarantee guarantee-expr)

maybe-assume =
| #:assume assume-expr

Searches for a binding of symbolic constants to concrete values that has the following properties:

it does not map the constants in (symbolics input-expr); and,
it satisfies all assertions encountered during the evaluation of guarantee-expr, for every binding of input-expr constants to values that satisfies the assertions encountered before the invocation of synthesize and during the evaluation of assume-expr.

If no such binding exists, the result is an unsatisfiable solution?. The assertions encountered while evaluating assume-expr and guarantee-expr are removed from the global assertion store once synthesize returns. These assertions may not include quantified formulas. The solver’s ability to find solutions depends on the current reasoning precision, as determined by the current-bitwidth parameter.

Examples:

> (define-symbolic x c integer?)
> (assert (even? x))
> (asserts)   ; assertion pushed on the store
'((= 0 (remainder x 2)))
> (define sol
    (synthesize #:forall x
                #:guarantee (assert (odd? (+ x c)))))
> (asserts)   ; assertion store same as before
'((= 0 (remainder x 2)))
> (evaluate x sol) ; x is unbound
x
> (evaluate c sol) ; c must an odd integer
77

3.2.6 Optimization

syntax
(optimize
   maybe-minimize
   maybe-maximize
   #:guarantee guarantee-expr)

maybe-minimize =
| #:minimize minimize-expr

maybe-maximize =
| #:maximize maximize-expr

   minimize-expr : (listof (or/c integer? real? bv?))
   maximize-expr : (listof (or/c integer? real? bv?))

Searches for a binding of symbolic constants to concrete values that satisfies all assertions encountered before the invocation of optimize and during the evaluation of minimize-expr, maximize-expr, and guarantee-expr. If such a binding exists, it is returned in the form of a satisfiable solution?; otherwise, the result is an unsatisfiable solution. Any satisfiable solution returned by optimize is optimal with respect to the cost terms provided in the minimize-expr and maximize-expr lists. Specifically, these terms take on the minimum or maximum values when evaluated with respect to a satisfiable solution. For more details on solving optimization problems, see the Z3 optimization tutorial.

As is the case for other solver-aided queries, the assertions encountered while evaluating minimize-expr, maximize-expr, and guarantee-expr are removed from the global assertion store once the query returns. As a result, optimize has no observable effect on the assertion store. The solver’s ability to find solutions (as well as their optimality) depends on the current reasoning precision, as determined by the current-bitwidth parameter.

Examples:

> (current-bitwidth #f) ; use infinite-precision arithmetic
> (define-symbolic x y integer?)
> (assert (< x 2))
> (asserts)   ; assertion added to the store
'((< x 2))
> (define sol
    (optimize #:maximize (list (+ x y))
              #:guarantee (assert (< (- y x) 1))))
> (asserts)   ; assertion store same as before
'((< x 2))
> (evaluate x sol) ; x + y is maximal at x = 1
1
> (evaluate y sol) ; and y = 1
1

3.2.7 Debugging

(require rosette/query/debug)

package: rosette

syntax
(define/debug head body ...)

head = id
| (id ...)

Defines a procedure or an expression, and marks it as a candidate for debugging. When a debug query is applied to a failing execution, forms that are not marked in this way are considered correct. The solver will apply the debugging algorithm only to expressions and procedures marked as potentially faulty using define/debug.

syntax
(debug [type ...+] expr)

type : (and/c solvable? type? (not/c function?))

Searches for a minimal set of define/debug expressions of the given solvable type(s) that are collectively responsible for the observed failure of expr. If no expressions of the specified types are relevent to the failure, an error is thrown. The returned expressions, if any, are called a minimal unsatisfiable core. The core expressions are relevant to the observed failure in that preventing the failure requries modifying at least one core expression. In particular, if all of the non-core expressions were replaced with fresh constants created using define-symbolic*, (solve expr) would still fail. It can only execute successfully if at least one of the core expressions is also replaced with a fresh constant. See the Essentials chapter for example uses of the debug form.

3.2.8 Reasoning Precision

parameter
(current-bitwidth) → (or/c #f positive-integer?)
(current-bitwidth k) → void?
k : (or/c #f positive-integer?)
= #f

A parameter that defines the current reasoning precision for solver-aided queries over integer? and real? constants. Setting current-bitwidth to a positive integer k instructs Rosette to approximate both reals and integers with signed k-bit words. Setting it to #f instructs Rosette to use infinite precision for real and integer operations. As a general rule, current-bitwidth should be set once, before any solver-aided queries are issued.

When current-bitwidth is #f, Rosette translates queries over reals and integers into constraints in the theories of reals and integers. These theories are effectively decidable only for linear constraints, so setting current-bitwidth to a positive integer will lead to better performance for programs that perform nonlinear arithmetic.

When current-bitwidth is set to a positive integer k, Rosette translates queries over reals and integers into constraints in the theory of bitvectors (of size k), which can be decided efficiently in practice. When this form of translation is used, however, solver-aided queries can produce counterintuitive results due to arithmetic over- and under-flow, as demonstrated below.

Rosette sets current-bitwidth to #f by default for two reasons. First, this setting is consistent with Racket’s infinite-precision semantics for integers and reals, avoiding counterintuitive query behavior. Second, the current-bitwidth parameter must be set to #f when executing queries over assertions that contain quantified formulas or uninterpreted functions. Otherwise, such a query will throw an exception.

Examples:

> (define-symbolic x y real?)
> (define-symbolic f (~> real? real?))
> (current-bitwidth 5)
> (solve (assert (= x 3.5)))              ; 3.5 = 3 under 5-bit semantics
(model
[x 3])
> (solve (assert (= x 64)))               ; 0 = 64 under 5-bit semantics
(model
[x 0])
> (solve (assert (and (= x 64) (= x 0)))) ; leading to counterintuitive results.
(model
[x 0])
> (solve (assert (forall (list x) (= x (+ x y)))))  ; Quantifiers are not supported,
finitize: cannot use (current-bitwidth 5) with a quantified
formula (forall (x) (= x (+ x y))); use (current-bitwidth
#f) instead
> (solve (assert (= x (f x))))  ; and neither are uninterpreted functions.
finitize: cannot use (current-bitwidth 5) with an
uninterpreted function f; use (current-bitwidth #f) instead
> (current-bitwidth #f)
> (solve (assert (= x 3.5))) ; Infinite-precision semantics produces expected results.
(model
[x 7/2])
> (solve (assert (= x 64)))
(model
[x 64])
> (solve (assert (and (= x 64) (= x 0))))
(unsat)
> (solve (assert (forall (list x) (= x (+ x y)))))  ; Quantifiers work, and
(model
[y 0])
> (solve (assert (= x (f x)))) ; so do uninterpreted functions.
(model
[x 0]
[f (fv real?~>real?)])
> (define-symbolic i j integer?) ; But nonlinear integer arithmetic is undecidable.
> (solve
   (begin
     (assert (> i 0))
     (assert (> j 0))
     (assert (or (= (/ i j) 2) (= (/ j i) 2)))))
(unknown)

top ← prev up next →

1	Getting Started
2	Rosette Essentials
3	Syntactic Forms
4	Built-In Datatypes
5	Structures
6	Libraries
7	Symbolic Reflection
8	Unsafe Operations
9	Performance
10	References
	Index

3.2.1	Symbolic Constants
3.2.2	Assertions
3.2.3	Angelic Execution
3.2.4	Verification
3.2.5	Synthesis
3.2.6	Optimization
3.2.7	Debugging
3.2.8	Reasoning Precision