3.2 Solver-Aided Forms
The Essentials chapter introduced the key concepts of solver-aided programming. This section describes the corresponding syntactic constructs in detail.
3.2.1 Symbolic Constants
syntax
(define-symbolic id ...+ type)
(define-symbolic id type #:length k)
type : (and/c solvable? type?)
k : natural?
> (define (always-same) (define-symbolic x integer?) x) > (always-same) x
> (always-same) x
> (equal? (always-same) (always-same)) #t
The second form creates a list of k distinct
constants and binds it to id. The same constants
are bound to id every time the form is evaluated.
The form requires k to evaluate to a natural number
statically—
> (define (always-same-3) (define-symbolic y integer? #:length (+ 1 2)) y) > (always-same-3) (list y$0 y$1 y$2)
> (always-same-3) (list y$0 y$1 y$2)
> (equal? (always-same-3) (always-same-3)) #t
> (define (always-same-n n) (define-symbolic y integer? #:length n) y) eval:9.0: define-symbolic: expected a natural? for #:length
at: (define-symbolic y integer? #:length n)
in: (define-symbolic y integer? #:length n)
syntax
(define-symbolic* id ...+ type)
(define-symbolic* id type #:length k)
type : (and/c solvable? type?)
k : natural?
> (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)
The second form binds id to a list of the next k elements from its stream every time the form is evaluated. The expression k may produce different natural numbers depending on the calling context.
> (define (always-different-n n) (define-symbolic* y integer? #:length n) y) > (always-different-n 2) (list y$4 y$5)
> (always-different-n 3) (list y$6 y$7 y$8)
> (equal? (always-different-n 4) (always-different-n 4)) (&& (= y$9 y$13) (= y$10 y$14) (= y$11 y$15) (= y$12 y$16))
3.2.2 Assertions and Assumptions
> (assert #t) ; No effect. > (assert 1) ; No effect. > (vc) ; The VC tracks assumptions and assertions. (vc #t #t)
> (define-symbolic x boolean?) > (assert x) > (vc) ; x is added to the VC's asserts. (vc #t x)
> (assert #f "bad value") [assert] bad value
> (vc) (vc #t #f)
> (clear-vc!) ; Clear the VC. > (vc) (vc #t #t)
> (vc) (vc #t #t)
> (assume #t) ; No effect. > (assume 1) ; No effect. > (vc) ; The VC tracks assumptions and assertions. (vc #t #t)
> (define-symbolic x boolean?) > (assume x) > (vc) ; x is added to the VC's assumes. (vc x #t)
> (assume #f "bad value") [assume] bad value
> (vc) (vc #f #t)
> (clear-vc!) ; Clear the VC. > (vc) (vc #t #t)
3.2.3 Verification
syntax
(verify expr)
Formally, (verify expr) searches for a model of the formula (vc-assumes P) ∧ (vc-asserts P) ∧ (vc-assumes Q) ∧ ¬ (vc-asserts Q), where P is the verification condition before the call to verify and Q is the verification condition generated by evaluating expr.
The verify query does not retain the assumptions and assertions generated by expr, leaving the current verification condition (vc) unchanged after the query returns.
> (define-symbolic a b c d boolean?) > (vc) (vc #t #t)
; This query forces a to be false: > (verify (assert a))
(model
[a #f])
> (vc) ; VC is unchanged. (vc #t #t)
> (assume a) > (assert b) > (vc) (vc a (|| b (! a)))
; This query forces a, b, c to be true, and d to be false:
> (verify (begin (assume c) (assert d)))
(model
[a #t]
[b #t]
[c #t]
[d #f])
> (vc) (vc a (|| b (! a)))
; This query has no solution because we assumed a above: > (verify (assert a)) (unsat)
; Clearing the VC gives the expected solution: > (clear-vc!) > (vc) (vc #t #t)
> (verify (assert a))
(model
[a #f])
3.2.4 Synthesis
syntax
(synthesize input expr)
(synthesize #:forall input #:guarantee expr)
Formally, (synthesize input expr) searches for a model of the formula ∃ H. (∃ I. pre(H, I)) ∧ (∀ I. pre(H, I) ⇒ post(H, I)), where pre(H, I) is (vc-assumes P) ∧ (vc-asserts P) ∧ (vc-assumes Q), post(H, I) is (vc-asserts Q), P is the verification condition accumulated before the evaluation of expr, and Q is the verification condition generated by evaluating expr. This formula is stronger than the classic synthesis formula ∃ H. ∀ I. pre(H, I) ⇒ post(H, I). The additional constraint, ∃ I. pre(H, I), rules out trivial solutions that allow pre(H, I) to be false on all inputs I. The formulas pre(H, I) and post(H, I) are required to be free of quantifiers, so no quantified formulas can be part of the assumptions or assertions that make up a synthesis query.
The synthesize query does not retain the assumptions and assertions generated by expr, but it does retain the updates to (vc), if any, produced by evaluating input. In other words, (synthesize input expr) is equivalent to (let ([v input]) (synthesize v expr)), where v is a fresh variable.
> (define-symbolic x c integer?) > (vc) (vc #t #t)
; This query finds a binding for c that works for all even x:
> (synthesize #:forall (list x) #:guarantee (begin (assume (even? x)) (assert (odd? (+ x c)))))
(model
[c 1])
> (vc) ; VC is unchanged. (vc #t #t)
> (assume (odd? x)) > (vc) (vc (! (= 0 (remainder x 2))) #t)
; This query finds a binding for c that works for all odd x:
> (synthesize #:forall (list x) #:guarantee (assert (odd? (+ x c))))
(model
[c 0])
> (vc) (vc (! (= 0 (remainder x 2))) #t)
; This query has no solution because we assumed (odd? x) above:
> (synthesize #:forall (list x) #:guarantee (begin (assume (even? x)) (assert (odd? (+ x c))))) (unsat)
; Clearing the VC gives the expected solution: > (clear-vc!) > (vc) (vc #t #t)
> (synthesize #:forall (list x) #:guarantee (begin (assume (even? x)) (assert (odd? (+ x c)))))
(model
[c 1])
3.2.5 Angelic Execution
syntax
(solve expr)
Formally, (solve expr) searches for a model of the formula (vc-assumes P) ∧ (vc-asserts P) ∧ (vc-assumes Q) ∧ (vc-asserts Q), where P is the verification condition before the call to solve and Q is the verification condition generated by evaluating expr.
The solve query does not retain the assumptions and assertions generated by expr, leaving the current verification condition (vc) unchanged after the query returns.
> (define-symbolic x y boolean?) > (assume x) > (vc) ; x is added to the VC's assumes. (vc x #t)
; This query forces both x and y to be true. > (solve (assert y))
(model
[x #t]
[y #t])
> (vc) ; VC is unchanged. (vc x #t)
; This query has solution because we assumed (not x) above: > (solve (assert (not x))) (unsat)
; Clearing the VC gives the expected solution: > (clear-vc!) > (vc) (vc #t #t)
> (solve (assert (not x)))
(model
[x #f])
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 after shutdown. solver-push: contract violation:
expected: solver?
given: #f
argument position: 1st
3.2.6 Optimization
syntax
(optimize maybe-minimize maybe-maximize #:guarantee expr)
maybe-minimize =
| #:minimize min-expr maybe-maximize =
| #:maximize max-expr
min-expr : (listof (or/c integer? real? bv?))
max-expr : (listof (or/c integer? real? bv?))
Formally, (solve expr) searches for an optimal model of the formula (vc-assumes P) ∧ (vc-asserts P) ∧ (vc-assumes Q) ∧ (vc-asserts Q), where P is the verification condition before the evaluation of expr, Q is the verification condition generated by evaluating expr, the cost terms min-expr are minimized, and the cost terms max-expr are maximized.
The optimize query does not retain the assumptions and assertions generated by expr, but it does retain the updates to (vc), if any, produced by evaluating min-expr and max-expr. In other words, (optimize #:minimize min-expr #:maximize max-expr #:guarantee expr) is equivalent to (let ([v min-expr] [w max-expr]) (optimize #:minimize v #:maximize w #:guarantee expr)), where v and w are fresh variables.
> (define-symbolic x y integer?) ; This query maximizes x + y while ensuring that y - x < 1 whenever x < 2:
> (optimize #:maximize (list (+ x y)) #:guarantee (begin (assume (< x 2)) (assert (< (- y x) 1))))
(model
[x 1]
[y 1])
3.2.7 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) ; Use 5 bits for integers and reals. > (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 ; Quantifiers are not supported, (assert (forall (list x) (= x (+ x y))))) finitize: cannot use (current-bitwidth 5) with a quantified
formula (forall (x) (= x (+ x y))); use (current-bitwidth
#f) instead
> (solve ; and neither are uninterpreted functions. (assert (= x (f x)))) finitize: cannot use (current-bitwidth 5) with an
uninterpreted function f; use (current-bitwidth #f) instead
> (current-bitwidth #f) ; Use infinite-precision semantics ... > (solve (assert (= x 3.5))) ; to obtain the expected results.
(model
[x 7/2])
> (solve (assert (= x 64)))
(model
[x 64])
> (solve (assert (and (= x 64) (= x 0)))) (unsat)
> (solve ; Quantifiers work, and (assert (forall (list x) (= x (+ x y)))))
(model
[y 0])
> (solve (assert (= x (f x)))) ; so do uninterpreted functions.
(model
[x 0]
[f (fv real?~>real?)])
> (define-symbolic i j integer?)
> (solve ; But nonlinear integer arithmetic (begin ; is undecidable. (assert (> i 0)) (assert (> j 0)) (assert (or (= (/ i j) 2) (= (/ j i) 2))))) (unknown)