►The Rosette Guide
▼7 Symbolic Reflection
On this page:
pc
asserts
clear-asserts!
with-asserts
with-asserts-only
term-cache
clear-terms!
7.7
  top  ← prev  up  next → 

7.2 Reflecting on Symbolic State

Like standard program execution, Rosette’s symbolic evaluation  [3] can be understood as a sequence of transitions from one program state to the next. In addition to the memory and register values, the state of a Rosette program also includes the current path condition and the current assertion store. The path condition is a boolean value encoding the branch decisions taken to reach the present state, and the assertion store is the set of boolean values (i.e., constraints) that have been asserted so far. This section describes the built-in facilities for accessing and modifying various aspects of the symbolic state from within a Rosette program. In general, these facilities should only be used by expert Rosette programmers to implement low-level solver-aided tools.

procedure

(pc) → boolean?

Returns the current path condition.

Examples:
> (define-symbolic a b boolean?)
> (if a
      (if b
          #f
          (pc))
      #f)

(&& a (! b))

procedure

(asserts) → (listof boolean?)

Returns the contents of the assertion store as a list of symbolic boolean values (or #f) that have been asserted so far.

Examples:
> (define-symbolic a b boolean?)
> (assert a)
> (asserts)

'(a)

> (assert b)
> (asserts)

'(b a)

procedure

(clear-asserts!) → void?

Clears the assertion store from all symbolic boolean values (or #f) that have been asserted so far. Rosette programs should not clear the assertion store unless they are implementing low-level tools.

Examples:
> (define-symbolic a b boolean?)
> (assert a)
> (assert b)
> (asserts)

'(b a)

> (clear-asserts!)
> (asserts)

'()

syntax

(with-asserts expr)

Returns two values: the result of evaluating expr and the assertions generated during the evaluation of expr. These assertions will not appear in the assertion store after with-asserts returns.

Examples:
> (define-symbolic a b boolean?)
> (define-values (result asserted)
    (with-asserts
     (begin (assert a)
            (assert b)
            4)))
> (printf "result = ~a\n" result)

result = 4

> (printf "asserted = ~a\n" asserted)

asserted = (b a)

> (asserts)

'()

syntax

(with-asserts-only expr)

Like with-asserts, but returns only the assertions generated during the evaluation of expr.

Examples:
> (define-symbolic a b boolean?)
> (with-asserts-only
     (begin (assert a)
            (assert b)
            4))

'(b a)

parameter

(term-cache) → hash?

(term-cache h) → void?
  h : hash?
A parameter that holds the cache of all symbolic terms constructed during symbolic evaluation. This cache stores terms for the purposes of partial cannonicalization. In particular, Rosette uses the term cache to ensure that no syntactically identical terms are created. Rosette programs should not modify the term cache unless they are implementing low-level tools.

Examples:
> (pretty-print (term-cache))

'#hash()

> (define-symbolic a b c d integer?)
> (pretty-print (term-cache))

(hash

 #<syntax:eval:25:0 a>

 a

 #<syntax:eval:25:0 d>

 d

 #<syntax:eval:25:0 c>

 c

 #<syntax:eval:25:0 b>

 b)

> (* d (- (+ a b) c))

(* d (+ (+ a b) (- c)))

> (pretty-print (term-cache))

(hash

 #<syntax:eval:25:0 a>

 a

 (list + (+ a b) (- c))

 (+ (+ a b) (- c))

 (list - c)

 (- c)

 (list * d (+ (+ a b) (- c)))

 (* d (+ (+ a b) (- c)))

 (list + a b)

 (+ a b)

 #<syntax:eval:25:0 d>

 d

 #<syntax:eval:25:0 c>

 c

 #<syntax:eval:25:0 b>

 b)

procedure

(clear-terms! [terms]) → void?

  terms : (or/c #f (listof term?)) = #f
Clears the entire term-cache if invoked with #f (default), or it evicts all of the given terms as well as any expressions that transitively contain them. Rosette programs should not clear the term cache unless they are implementing low-level tools.

Examples:
> (term-cache)

#hash()

> (define-symbolic a b c d integer?)
> (pretty-print (term-cache))

(hash

 #<syntax:eval:31:0 a>

 a

 #<syntax:eval:31:0 d>

 d

 #<syntax:eval:31:0 c>

 c

 #<syntax:eval:31:0 b>

 b)

> (* d (- (+ a b) c))

(* d (+ (+ a b) (- c)))

> (pretty-print (term-cache))

(hash

 #<syntax:eval:31:0 a>

 a

 (list * d (+ (+ a b) (- c)))

 (* d (+ (+ a b) (- c)))

 (list + a b)

 (+ a b)

 (list + (+ a b) (- c))

 (+ (+ a b) (- c))

 (list - c)

 (- c)

 #<syntax:eval:31:0 d>

 d

 #<syntax:eval:31:0 c>

 c

 #<syntax:eval:31:0 b>

 b)

> (clear-terms! (list c d))
> (pretty-print (term-cache))

(hash #<syntax:eval:31:0 a> a (list + a b) (+ a b) #<syntax:eval:31:0 b> b)

> (clear-terms!)
> (pretty-print (term-cache))

'#hash()

  top  ← prev  up  next →