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, =, <, <=, >, >=, expt, 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.
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.
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).
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.
> (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
> (define g (forall (list a) (= a (+ a b)))) ; b is free in g > (solve (assert g)) ; so the model has a binding for b
> (define h (exists (list a) (forall (list a) (= a (+ a a))))) ; body refers to the innermost a > (solve (assert h)) ; so h is unsatisfiable.