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

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, current-bitwidth is, by default, set 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 also supports the following logical operations: conjunction (&&), disjunction (||), implication (=>), bi-implication (<=>), negation (!), universal quantification (forall), and existential quantification (exists). 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 disjunciton 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)

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. The body of the formula is a boolean expression over the quantified variables vs and, optionally, over free symbolic (Skolem) constants.

If a set of constraints is satisfiable, their model includes bindings only for free symbolic constants: no bindings are provided for constants that do not appear freely in any formula. All quantified symbolics must be have a non-function? solvable? type. 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.

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.

Examples:
> (current-bitwidth #f)
> (define-symbolic a b integer?)
> (forall (list) (= a b))

(= a b)

> (define f (forall (list a) (exists (list b) (= a (+ a b))))) ; no free constants
> (solve (assert f)) ; so the model has no bindings

(model)

> (define g (forall (list a) (= a (+ a b)))) ; b is free in g
> (solve (assert g)) ; so the model has a binding for b

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