4.2 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 bboolean? )
> (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.1Additional Logical Operators🔗 i

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 bboolean? )
> (! (if b#f3));This typechecks only when b is true,

#t
> (vc );so Rosette emits a corresponding assertion.

(vc #t 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.

hello

#f
> (define-symbolic abboolean? )
> (&& a(if b#t1));This typechecks only when b is true,

a
> (vc );so Rosette emits a corresponding assertion.

(vc #t b)

procedure
( => xy)→boolean?
x:boolean?
y:boolean?
( <=> xy)→boolean?
x:boolean?
y:boolean?

Returns the logical implication or bi-implication of two boolean values.

Examples:

> (=> #f(begin (displayln "hello")#f));No shortcircuiting.

hello

#t
> (define-symbolic abboolean? )
> (<=> a(if b#t1));This typechecks only when b is true,

a
> (vc );so Rosette emits a corresponding assertion.

(vc #t b)

4.2.2Quantifiers🔗 i

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 vsbody)→boolean?
vs:(listof constant? )
body:boolean?
( exists vsbody)→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 and assumptions emitted during the evaluation of body are added to the current verification condition (vc ). This may be the desired behavior in some circumstances but not in others, so to avoid surprises, it is best to handle side effects separately and call quantifiers with pure bodies, as shown below.

Examples:

> (current-bitwidth #f)
> (define-symbolic xyinteger? )
> (exists (list xy)(= xy));Pure body expression.

(exists (x y) (= x y))
> (define-symbolic bboolean? )

> (forall (list bxy)
(= (+ (if bx'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 bx'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 bxy)
(=> (&& (vc-assumesout-vc)(vc-assertsout-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.

Examples:

> (define-symbolic xyinteger? )

> (define f
(forall (list x)
(exists (list y)
(= x(+ xy)))));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(+ xy))));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(+ xx)))));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.

top ← prev up next →