#### 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 13])

> (inc (< y 4)) ; push (< y 4) and solve (unsat)

> (inc 1) ; pop (< y 4) and solve

(model

[x 6]

[y 13])

> (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 #:forall input-expr maybe-assume #:guarantee guarantee-expr)

maybe-assume =

| #:assume assume-expr

input-expr : (listof constant?)

it does not map constants in the input-expr list; 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 (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?))

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

= 5

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—

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.

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