4.2 Booleans, Integers, and Reals
Booleans | |
Integers and Reals | number?, real?, integer?, zero?, positive?, negative?, even?, odd?, inexact->exact, exact->inexact, +, -, *, /, quotient, remainder, modulo, add1, sub1, abs, max, min, floor, ceiling, truncate, =, <, <=, >, >=, pi, sgn |
Lifted boolean operations retain their Racket semantics on both concrete and symbolic values. In particular, Rosette extends the intepretation of these operations to work on symbolic values in (logically) the same way that they work on concrete values.
> (define-symbolic b boolean?) > (boolean? b) #t
> (boolean? #t) #t
> (boolean? #f) #t
> (boolean? 1) #f
> (not b) ; Produces a logical negation of b. (! b)
Lifted numeric operations, in contrast, match their Racket semantics only when applied to concrete values. Their symbolic semantics depends on the current reasoning precision, as determined by the current-bitwidth parameter. In particular, if this parameter is set to #f, operations on symbolic numbers retain their infinite-precision Racket semantics. However, because infinite-precision reasoning is not efficiently (or at all) decidable for arbitrary numeric operations, programs may need to set current-bitwidth to a small positive integer k. With this setting, symbolic numbers are treated as signed k-bit integers. See Reasoning Precision for details and examples.
4.2.1 Additional Logical Operators
In addition to lifting Racket’s operations on booleans, Rosette supports the following logical operations: conjunction (&&), disjunction (||), implication (=>), bi-implication (<=>), and negation (!). These operations have their usual logical meaning; e.g., unlike Racket’s shortcircuiting and operator, the logical && operator evaluates all of its arguments before taking their conjunction.
4.2.2 Quantifiers
Rosette also provides constructs for creating universally (forall) and existentially (exists) quantified formulas. These differ from the usual logical quantifiers in that the evaluation of a quantified formula’s body may have side effects (e.g., generate assertions). When there are no side effects, however, these constructs have their usual logical meaning.
procedure
vs : (listof constant?) body : boolean? (exists vs body) → boolean? vs : (listof constant?) body : boolean?
> (current-bitwidth #f) > (define-symbolic x y integer?) > (exists (list x y) (= x y)) ; Pure body expression. (exists (x y) (= x y))
> (define-symbolic b boolean?)
> (forall (list b x y) (= (+ (if b x 'x) 1) y)) ; Body emits a type assertion. (forall (b x y) (= y (+ 1 x)))
> (vc) (vc #t b)
> (clear-vc!) ; To avoid surprises, capture assertions and assumptions using with-vc, ; and handle as desired, e.g.: > (define out (with-vc (= (+ (if b x 'x) 1) y))) > out (normal (= y (+ 1 x)) (vc #t b))
> (define out-val (result-value out)) > (define out-vc (result-state out))
> (forall (list b x y) (=> (&& (vc-assumes out-vc) (vc-asserts out-vc)) out-val)) (forall (b x y) (|| (! b) (= y (+ 1 x))))
> (vc) (vc #t #t)
The usual lexical scoping rules apply to quantified symbolics; if body is a quantified formula over a variable v in vs, then the innermost quantification of v shadows any enclosing quantifications. Quantified symbolics are not bound in a model, unless they also appear freely in some formulas.
> (define-symbolic x y integer?)
> (define f (forall (list x) (exists (list y) (= x (+ x y))))) ; x and y are not free in f, > (solve (assert f)) ; so they are not bound in the model. (model)
> (define g (forall (list x) (= x (+ x y)))) ; y is free in g, > (solve (assert g)) ; so it is bound in the model.
(model
[y 0])
> (define h (exists (list x) (forall (list x) (= x (+ x x))))) ; The body of h refers to the innermost x, > (solve (assert h)) ; so h is unsatisfiable. (unsat)
When executing queries over assertions that contain quantified formulas, the current-bitwidth parameter must be set to #f. Quantified formulas may not appear in any assertion or assumption that is passed to a synthesize query.