On this page:
4.2.1 Additional Logical Operators
!
&&
||
=>
<=>
4.2.2 Quantifiers
forall
exists
7.9

4.2 Booleans, Integers, and Reals

Rosette lifts the following operations on booleans, integers, and reals:

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.

Examples:
> (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.

procedure

(! v)  boolean?

  v : boolean?
Returns the negation of the given boolean value.

Examples:
> (! #f)

#t

> (! #t)

#f

> (define-symbolic b boolean?)
> (! (if b #f 3)) ; this typechecks only when b is true

#t

> (asserts)       ; so Rosette emits a corresponding assertion

'(b)

procedure

(&& v ...)  boolean?

  v : boolean?
(|| v ...)  boolean?
  v : boolean?
Returns the logical conjunction or disjunction of zero or more boolean values.

Examples:
> (&&)

#t

> (||)

#f

> (&& #f (begin (displayln "hello") #t)) ; no shortcircuiting

#f

> (define-symbolic a b boolean?)
> (&& a (if b #t 1)) ; this typechecks only when b is true

a

> (asserts)          ; so Rosette emits a corresponding assertion

'(b)

procedure

(=> x y)  boolean?

  x : boolean?
  y : boolean?
(<=> x y)  boolean?
  x : boolean?
  y : boolean?
Returns the logical implication or bi-implication of two boolean values.

Examples:
> (=> #f (begin (displayln "hello") #f)) ; no shortcircuiting

#t

> (define-symbolic a b boolean?)
> (<=> a (if b #t 1)) ; this typechecks only when b is true

a

> (asserts)           ; so Rosette emits a corresponding assertion

'(b)

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

(forall vs body)  boolean?

  vs : (listof constant?)
  body : boolean?
(exists vs body)  boolean?
  vs : (listof constant?)
  body : boolean?
Returns a universally or existentially quantified formula, where the symbolic constants vs are treated as quantified variables. Each constant in vs must have a non-function? solvable? type. The body argument is a boolean value, which is usually a symbolic boolean expression over the quantified variables vs and, optionally, over free symbolic (Skolem) constants. Any assertions emitted during the evaluation of body are added to the assertion store. This may be the desired behavior in some circumstances but not in others, so to avoid surprises, it is best to handle these assertions separately and call quantifiers with pure bodies, as shown below.

Examples:
> (current-bitwidth #f)
> (define-symbolic x y integer?)
> (exists (list x y) (= x y)) ; pure body expression

(exists (x y) (= x y))

> (define-symbolic t boolean?)
> (forall (list t x y) (= (+ (if t x 'x) 1) y)) ; body emits a type assertion

(forall (t x y) (= y (+ 1 x)))

> (asserts)

'(t)

> (clear-asserts!)
; To avoid surprises, capture assertions using with-asserts,
; and handle as desired, e.g.:
> (define-values (q-body q-asserts) (with-asserts (= (+ (if t x 'x) 1) y)))
> q-body

(= y (+ 1 x))

> q-asserts

'(t)

> (forall (list t x y) (=> (apply && q-asserts) q-body))

(forall (t x y) (|| (! t) (= y (+ 1 x))))

> (asserts)

'()

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.

Examples:
> (define-symbolic a b integer?)
> (define f (forall (list a) (exists (list b) (= a (+ a b))))) ; a and b are not free in f,
> (solve (assert f))                                           ; so not bound in the model.

(model)

> (define g (forall (list a) (= a (+ a b))))                   ; b is free in g,
> (solve (assert g))                                           ; so it is bound in the model.

(model

 [b 0])

> (define h (exists (list a) (forall (list a) (= a (+ a a))))) ; body refers to the innermost a,
> (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 that is passed to a synthesize query, either via an (implicit or explicit) assumption or a guarantee expression.