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

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

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

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

procedure

(solve+) → procedure?

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.

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

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

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.

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

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.

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

##### 3.2.8` `Reasoning Precision

parameter

(current-bitwidth) → (or/c #f positive-integer?)

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

= #f

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.

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