On this page:
3.2.1 Symbolic Constants
define-symbolic
define-symbolic*
3.2.2 Assertions
assert
3.2.3 Angelic Execution
solve
3.2.4 Verification
verify
3.2.5 Synthesis
synthesize
3.2.6 Optimization
optimize
3.2.7 Debugging
define/  debug
debug
3.2.8 Reasoning Precision
current-bitwidth
6.6

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

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
   #:forall input-expr
   maybe-assume
   #:guarantee guarantee-expr)
 
maybe-assume = 
  | #:assume assume-expr
 
  input-expr : (listof constant?)
Searches for a binding of symbolic constants to concrete values that has the following properties:
  1. it does not map constants in the input-expr list; and,

  2. 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 (list 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

1

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?)
 = 5
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 numeric operations are evaluated.

Technically, when current-bitwidth is a positive integer k, Rosette translates queries over reals and integers into constraints in the theory of bitvectors (of size k), which can be efficiently decided by SMT solvers. When this form of translation is used, a solve or verify query will produce a satisfiable result if and only if there is a solution under k-bit semantics that is also correct under infinite-precision semantics. (Note that this guarantee is limited in the case of unsatisfiability—it says only that no k-bit solution corresponds to an infinite-precision solution.) Rosette does not provide such a soundness guarantee for other queries because it is computationally expensive or impossible to provide. A synthesize query, for example, may produce a solution that is correct under k-bit semantics, but incorrect under infinite-precision semantics.

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 most applications will perform better when current-bitwidth is set to a positive integer.

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))) ; there is no solution under

(unsat)

> (solve (assert (= x 64)))  ; 5-bit signed integer semantics

(unsat)

> (solve (assert (forall (list x) (= x (+ x y)))))  ; and 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))))  ; same for 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))) ; but there is a solution under

(model

 [x 7/2])

> (solve (assert (= x 64)))  ; infinite-precision semantics

(model

 [x 64])

> (solve (assert (forall (list x) (= x (+ x y)))))  ; and quantifiers work

(model

 [y 0])

> (solve (assert (= x (f x)))) ; so do uninterpreted functions

(model

 [x 0]

 [f (fv real?~>real?)])