7.2 Reflecting on Symbolic State🔗ℹ

Like standard program execution, Rosette’s symbolic evaluation can be viewed as a function that operates on program states. The state of a Rosette program includes its Racket state (memory, environment, and so on) and its symbolic state. The key parts of the symbolic state are the current verification condition (VC) and the current symbolic heap. The heap consists of all the symbolic terms created so far. The verification condition tracks all the assumptions and assertions issued on any path between the starting program state and the current state. Unlike concrete execution, which evaluates just one path through a program, Rosette evaluates all possible paths when the decision on which path to take depends on a symbolic value. The symbolic heap and the verification condition reflect the current state of this all-path evaluation.

(define-symbolic a b c d boolean?)

(terms) ; Symbolic heap.

(list a c d b)

(assume a)

(vc)    ; Verification condition.

(vc a #t)

(if b     (begin       (printf "Then branch:\n ~a\n" (vc))       (assert c)       (printf " ~a\n" (vc))       1)     (begin       (printf "Else branch:\n ~a\n" (vc))       (assert d)       (printf " ~a\n" (vc))       2))

Then branch:  #(struct:vc (&& a b) #t)  #(struct:vc (&& a b) (|| c (! (&& a b)))) Else branch:  #(struct:vc (&& a (! b)) #t)  #(struct:vc (&& a (! b)) (|| d (! (&& a (! b)))))

(ite b 1 2)

(vc)

(vc a (&& (|| (! b) (|| c (! (&& a b)))) (|| b (|| d (! (&& a (! b)))))))

(terms)

(list  a  c  d  b  (&& (|| (! b) (|| c (! (&& a b)))) (|| b (|| d (! (&& a (! b))))))  ...)

This section describes the built-in facilities for accessing and modifying various aspects of the symbolic state from within a Rosette program. These facilites are useful for low-level debugging and optimizations of Rosette-based tools. But they also make it possible to violate the state invariants maintained by Rosette, so it is best to use them sparingly.

7.2.1 Verification Conditions🔗ℹ

The current (vc) state can be cleared using clear-vc!. This resets (vc) to its starting value, vc-true.

The result of a with-vc expression is a value of type result?. If expr terminates normally, then the result is normal?, and its result-value contains the value computed by expr. If expr fails, the result is failed?, and its result-value contains an exn:fail? exception that represents the cause of the abnormal termination. In either case, result-state holds the final verification condition generated during the evaluation of expr, starting with vc-expr, or (vc), as the initial verification condition.

In the context of symbolic evaluation, expr terminates normally if it has at least one path of execution that terminates normally. A path terminates normally if it is free of any assumption or assertion violations—i.e., any (assume e) or (assert e) expressions where e evaluates to #f. Failures due to exceptions are treated as assertion violations.

See also with-vc.

7.2.2 Symbolic Heap🔗ℹ

The symbolic heap is not garbage collected, which means that long running applications may experience memory pressure. There are two ways to solve this issue, depending on the application’s behavior.

If the application is performing many independent queries that do not share any symbolic constants, then the application may safely clear the heap between query invocations using clear-terms!. This is the most common scenario.

If the application is solving a series of related queries, using clear-terms! can lead to incorrect behavior. In this scenario, the safe solution is to use a garbage-collected heap by invoking (gc-terms!). This has the effect of changing the internal representation of the heap to use a more expensive data structure that cooperates with Racket’s garbage collector. Because of the added runtime overhead, this setting is best saved for when the default heap consumes too much memory.

The result of a with-terms expression is the output of expr.

Note that none of the terms created during the evaluation of expr are preserved in the heap, and having those terms escape the dynamic extent of expr is usually a sign of a programming error. It can lead to incorrect behavior, similarly to using clear-terms!.