Refactor the synthesize query to use assumption and assertion stacks.

Update all uses of the query to conform to the new syntax.
Change (vcgen e) and (vcgen-eval e) to return only the
assumptions and assertions generated during the evaluation of e,
without prepending the assumptions and assertions that were on
the stack before the form was evaluated.
Change (vcs e) accordingly to maintaing the eval/asserts semantics.

rosette/base/base.rkt

@@ -16,8 +16,11 @@
   (filtered-out drop@ 
     (combine-out   
      ; core/bool.rkt
-     pc with-asserts with-asserts-only asserts clear-asserts!
-     @assert @boolean? @false? @! @&& @=> @<=> @forall @exists
+     pc 
+     @assert with-asserts with-asserts-only asserts clear-asserts!
+     @assume assumes clear-assumes!
+     vcgen vcgen-eval
+     @boolean? @false? @! @&& @=> @<=> @forall @exists
      ; core/real.rkt
      @integer? @real? @= @< @<= @>= @> 
      @+ @* @- @/ @quotient @remainder @modulo @abs

rosette/base/core/bool.rkt

@@ -5,8 +5,10 @@
 (provide @boolean? @false? 
          ! && || => <=> @! @&& @|| @=> @<=> @exists @forall
          and-&& or-|| instance-of?
-         @assert pc with-asserts with-asserts-only 
-         (rename-out [export-asserts asserts]) clear-asserts!
+         pc @assert @assume vcgen vcgen-eval
+         with-asserts with-asserts-only 
+         (rename-out [get-asserts asserts] [get-assumes assumes])
+         clear-asserts! clear-assumes!
          T*->boolean?)
 
 ;; ----------------- Boolean type ----------------- ;; 
@@ -262,17 +264,7 @@
     [(_ _) #f]))
 
   
-;; ----------------- Assertions and path condition ----------------- ;; 
-(define (export-asserts) (remove-duplicates (asserts)))
-
-(define (clear-asserts!)  (asserts '()))
-    
-(define asserts 
-  (make-parameter 
-   '()
-   (match-lambda [(? list? xs) xs]
-                 [x (if (eq? x #t) (asserts) (cons x (asserts)))])))
-
+;; ----------------- Path condition ----------------- ;; 
 (define pc 
   (make-parameter 
    #t
@@ -283,23 +275,65 @@
      (or (&& (pc) new-pc)
          (error 'pc "infeasible path condition")))))
 
-(define-syntax (@assert stx)
+;; ----------------- Assertions and assumptions ----------------- ;;
+
+(define-syntax-rule (define-vcg-form id @id ids get-id clear-id!)
+  (begin
+
+    (define ids 
+      (make-parameter 
+       '()
+       (match-lambda [(? list? xs) xs]
+                     [x (if (eq? x #t) (ids) (cons x (ids)))])))
+    
+    (define (get-id) (remove-duplicates (ids)))
+
+    (define (clear-id!) (ids '()))
+
+    (define-syntax (@id stx)
       (syntax-case stx ()
-    [(_ val) (syntax/loc stx (@assert val #f))]
+        [(_ val) (syntax/loc stx (@id val #f))]
         [(_ val msg) 
          (syntax/loc stx 
            (let ([guard (not-false? val)])
-         (asserts (=> (pc) guard)) 
+             (ids (=> (pc) guard)) 
              (when (false? guard)
-           (raise-assertion-error msg))))]))
+               (raise-vcg-form-error 'id msg))))]))))
 
 (define (not-false? v)
   (or (eq? v #t) (! (@false? v))))
 
-(define (raise-assertion-error msg)
+(define (raise-vcg-form-error kind msg)
   (if (procedure? msg)
       (msg)
-      (error 'assert (if msg (format "~a" msg) "failed"))))
+      (error kind (if msg (format "~a" msg) "failed"))))
+    
+(define-vcg-form assert @assert asserts get-asserts clear-asserts!)
+(define-vcg-form assume @assume assumes get-assumes clear-assumes!)
+
+;; ----------------- VC generation ----------------- ;;
+
+; Evaluates the given expression and returns 3 values:
+; * the result of the evaluation,
+; * the assumptions generated during evaluation, and
+; * the assertions generated during evaluation.
+; The global assumptions and assertions stack has the
+; same state before and after the evaluation of a vcgen-eval form.
+(define-syntax (vcgen-eval stx)
+  (syntax-case stx (begin)
+    [(_ (begin form ...)) #'(vcgen-eval (let () form ...))]
+    [(_ form) #`(parameterize ([asserts '()]
+                               [assumes '()])
+                  (values form (get-assumes) (get-asserts)))]))
+
+; Evaluates the given expression and returns 2 values:
+; * the assumptions generated during evaluation, and
+; * the assertions generated during evaluation.
+; The global assumptions and assertions stack has the
+; same state before and after the evaluation of a vcgen-eval form.
+(define-syntax-rule (vcgen form)
+  (let-values ([(out assumes asserts) (vcgen-eval form)])
+    (values assumes asserts)))
 
 (define-syntax (with-asserts stx)
   (syntax-case stx (begin)
@@ -312,3 +346,6 @@
 (define-syntax-rule (with-asserts-only form)
   (let-values ([(out asserts) (with-asserts form)])
     asserts))
+
+
+

rosette/lib/roseunit.rkt

@@ -4,7 +4,7 @@
 (require rackunit)
 (require (only-in rosette 
                   clear-state!
-                  current-bitwidth term-cache current-oracle oracle with-asserts-only
+                  current-bitwidth term-cache current-oracle oracle vcgen
                   solution? sat? unsat?))
 
 (provide run-all-tests test-groups test-suite+ test-sat test-unsat check-sol check-sat check-unsat)    
@@ -52,11 +52,14 @@
       name
       #:before (thunk (printf "~a\n" name) (before)) 
       #:after after
-      (with-asserts-only
+      (call-with-values
+       (thunk 
+        (vcgen
             (parameterize ([current-bitwidth (current-bitwidth)]
                            [term-cache (hash-copy (term-cache))]
                            [current-oracle (oracle (current-oracle))])
-         test ...)))]
+              test ...)))
+       void))]
     [(_ name #:before before test ...)
      (test-suite+ name #:before before #:after void test ...)]
     [(_ name #:after after test ...)

rosette/query/core.rkt

@@ -4,7 +4,7 @@
   "eval.rkt" "finitize.rkt"
   (only-in "../base/core/term.rkt" constant? term-type get-type term? term-cache clear-terms! term<? solvable-default)
   (only-in "../base/core/equality.rkt" @equal?)
-  (only-in "../base/core/bool.rkt" ! || && => with-asserts-only @boolean?)
+  (only-in "../base/core/bool.rkt" ! || && => with-asserts-only @boolean? vcgen-eval assumes asserts)
   (only-in "../base/core/function.rkt" fv)
   (only-in "../base/core/real.rkt" @integer? @real?)
   (only-in "../base/core/bitvector.rkt" bv bitvector?)
@@ -12,7 +12,7 @@
   (only-in "../solver/solution.rkt" model core sat unsat sat? unsat?)
   (only-in "../solver/smt/z3.rkt" z3))
 
-(provide current-solver ∃-solve ∃-solve+ ∃∀-solve ∃-debug eval/asserts 
+(provide current-solver ∃-solve ∃-solve+ ∃∀-solve ∃-debug eval/asserts vcs
          all-true? some-false? unfinitize)
 
 ; Current solver instance that is used for queries and kept alive for performance.
@@ -43,6 +43,23 @@
   (with-handlers ([exn:fail? return-#f])
     (with-asserts-only (closure))))
 
+(define failed (gensym))
+(define return-failed (lambda (e) failed))
+
+; Returns a list of assumptions and a list of assertions.  The list of
+; assumptions contains all assumptions and assertions generated before the
+; thunk is evaluated, along with all assumptions generated during the evaluation
+; of the thunk.  The list of assertions contains all assertions generated during
+; the evaluation of the thunk.  
+; If the evaluation of the thunk results in an exn:fail? exception,
+; the assertions list will contain the value #f.
+(define (vcs closure)
+  (let-values ([(out out-assumes out-asserts)
+                (vcgen-eval (with-handlers ([exn:fail? return-failed])
+                              (closure)))])
+    (if (eq? out failed)
+        (values (append out-assumes (assumes) (asserts)) (cons #f out-asserts))
+        (values (append out-assumes (assumes) (asserts)) out-asserts))))
 
   
 

rosette/query/form.rkt

@@ -2,10 +2,30 @@
 
 (require "core.rkt" 
          (only-in "../base/core/reflect.rkt" symbolics)
-         (only-in "../base/core/bool.rkt" ! ||))
+         (only-in "../base/core/bool.rkt" ! || vcgen-eval @assume @assert))
 
-(provide solve verify synthesize optimize
-         current-solver (rename-out [∃-solve+ solve+]))
+(provide solve verify synthesize optimize current-solver (rename-out [∃-solve+ solve+])
+         requires ensures)
+
+; Evaluates the given forms and returns the result.
+; All assumptions and assertions generated during the
+; evaluation of these forms are treated as assumptions.
+; In particular, they are all added to the current assumption stack.
+(define-syntax-rule (requires form ...)
+  (let-values ([(result assumes asserts) (vcgen-eval (begin form ...))])
+    (for ([vc (in-sequences (reverse assumes) (reverse asserts))])
+      (@assume vc))
+    result))
+
+; Evaluates the given forms and returns the result.
+; All assumptions and assertions generated during the
+; evaluation of these forms are treated as assertions.
+; In particular, they are all added to the current assertion stack.
+(define-syntax-rule (ensures form ...)
+  (let-values ([(result assumes asserts) (vcgen-eval (begin form ...))])
+    (for ([vc (in-sequences (reverse assumes) (reverse asserts))])
+      (@assert vc))
+    result))
 
 ; The solve query evaluates the given forms, gathers all 
 ; assertions generated during the evaluation, 
@@ -15,7 +35,8 @@
 ; this means that there is no solution under the k-bit semantics that 
 ; corresponds to a solution under the infinite precision semantics.  
 (define-syntax-rule (solve form forms ...)
-  (∃-solve (eval/asserts (thunk form forms ...))))
+  (let-values ([(assumes asserts) (vcs (thunk form forms ...))])
+    (∃-solve (append assumes asserts))))
 
 ; The verify query evaluates the given forms, gathers all 
 ; assumptions and assertions generated during the evaluation, 
@@ -25,27 +46,19 @@
 ; If current-bitwidth is a positive integer k, and the verify form returns unsat, 
 ; this means that there is no solution under the k-bit semantics that 
 ; corresponds to a solution under the infinite precision semantics.  
-(define-syntax verify
-  (syntax-rules ()
-    [(_ #:assume pre #:guarantee post)
-     (∃-solve `(,@(eval/asserts (thunk pre)) 
-                ,(apply || (map ! (eval/asserts (thunk post))))))]
-    [(_ #:guarantee post) (verify #:assume #t #:guarantee post)]
-    [(_ post) (verify #:assume #t #:guarantee post)]))
+(define-syntax-rule (verify form)
+  (let-values ([(assumes asserts) (vcs (thunk form))])
+    (∃-solve `(,@assumes ,(apply || (map ! asserts))))))
+
 
 ; The synthesize query evaluates the given forms, gathers all 
 ; assumptions and assertions generated during the evaluation, 
 ; and searches for a model (a binding from symbolic 
 ; constants to values) of the formula ∃H.∀I. pre => post, 
-; where I are the given input constants and H are all other symoblic constants. 
-(define-syntax synthesize 
-  (syntax-rules (synthesize)
-    [(_ #:forall inputs #:assume pre #:guarantee post)
-     (∃∀-solve (symbolics inputs) 
-               (eval/asserts (thunk pre)) 
-               (eval/asserts (thunk post)))]    
-    [(_ #:forall inputs #:guarantee post)
-     (synthesize #:forall inputs #:assume #t #:guarantee post)]))
+; where I are the given input constants and H are all other symbolic constants. 
+(define-syntax-rule (synthesize #:forall inputs #:guarantee form)
+  (let-values ([(assumes asserts) (vcs (thunk form))])
+     (∃∀-solve (symbolics inputs) assumes asserts)))  
 
 ; The optimize query evaluates the given form, gathers all 
 ; assertions generated during the evaluation, 
@@ -58,9 +71,11 @@
 (define-syntax optimize
   (syntax-rules ()
     [(_ kw opt #:guarantee form)
-     (let ([obj opt]) ; evaluate objective first to push its assertions onto the stack
-       (∃-solve (eval/asserts (thunk form)) kw obj))]
+     (let*-values ([(obj) opt] ; evaluate objective first to push its assertions onto the stack
+                   [(assumes asserts) (vcs (thunk form))])
+       (∃-solve (append assumes asserts) kw obj))]
     [(_ kw1 opt1 kw2 opt2 #:guarantee form)
-     (let ([obj1 opt1]
-           [obj2 opt2]) ; evaluate objectives first to push their assertions onto the stack
-       (∃-solve (eval/asserts (thunk form)) kw1 obj1 kw2 obj2))]))
+     (let*-values ([(obj1) opt1]
+                   [(obj2) opt2] ; evaluate objectives first to push their assertions onto the stack
+                   [(assumes asserts) (vcs (thunk form))])
+       (∃-solve (append assumes asserts) kw1 obj1 kw2 obj2))]))

rosette/safe.rkt

@@ -23,6 +23,7 @@
   (current-bitwidth 5)
   (current-oracle (oracle))
   (clear-asserts!)
+  (clear-assumes!)
   (clear-terms!)
   (current-solver (z3)))
 

sdsl/ifc/verify.rkt

@@ -56,16 +56,16 @@
     (define m1 (start (map instruction (map procedure p)))) ; Use a fresh program (same procedures, fresh args).
     
     (define cex
+      (verify 
        (let ([m0 m0]
              [m1 m1])
-        (verify 
-         #:assume  (begin 
+         (requires
           (assert (≈ m0 m1))     
           (set! m0 (step m0 k))  
           (set! m1 (step m1 k)) 
           (assert (end m0))
           (assert (end m1)))
-         #:guarantee (assert (≈ m0 m1)))))
+         (assert (≈ m0 m1)))))
 
     (if (sat? cex) (EENI-witness (evaluate m0 cex) (evaluate m1 cex) k ≈) #t)))
 

test/base/bitvector.rkt

@@ -16,7 +16,7 @@
 
 (define BV (bitvector 4))
 (define-symbolic x y z BV)
-(define-symbolic a b c d e f g @boolean?)
+(define-symbolic assertions b c d e f g @boolean?)
 
 (define minval (- (expt 2 (sub1 (bitvector-size BV)))))
 (define maxval+1 (expt 2 (sub1 (bitvector-size BV)))) 
@@ -60,7 +60,7 @@
        (define expected 
          ((solve (@bveq (bv i) x)
                  (@bveq (bv j) y)
-                 (@equal? a (op x y))) a))
+                 (@equal? assertions (op x y))) assertions))
        (check-equal? actual expected)))
 
 
@@ -83,12 +83,12 @@
   (check-valid? (@bveq (bv 2) (ite b (bv 2) (bv 0))) b)
   (check-valid? (@bveq (bv 0) (ite b (bv 2) (bv 0))) (! b))
   (check-valid? (@bveq (bv 1) (ite b (bv 2) (bv 0))) #f)
-  (check-valid? (@bveq (ite a (bv 2) (bv 2)) (ite b (bv 2) (bv 2))) #t)
-  (check-valid? (@bveq (ite a (bv 2) (bv 3)) (ite b (bv 4) (bv 5))) #f)
-  (check-valid? (@bveq (ite a (bv 2) (bv 3)) (ite b (bv 2) (bv 5))) (&& a b))
-  (check-valid? (@bveq (ite a (bv 2) (bv 3)) (ite b (bv 5) (bv 2))) (&& a (! b)))
-  (check-valid? (@bveq (ite a (bv 2) (bv 3)) (ite b (bv 3) (bv 5))) (&& (! a) b))
-  (check-valid? (@bveq (ite a (bv 2) (bv 3)) (ite b (bv 5) (bv 3))) (&& (! a) (! b))))
+  (check-valid? (@bveq (ite assertions (bv 2) (bv 2)) (ite b (bv 2) (bv 2))) #t)
+  (check-valid? (@bveq (ite assertions (bv 2) (bv 3)) (ite b (bv 4) (bv 5))) #f)
+  (check-valid? (@bveq (ite assertions (bv 2) (bv 3)) (ite b (bv 2) (bv 5))) (&& assertions b))
+  (check-valid? (@bveq (ite assertions (bv 2) (bv 3)) (ite b (bv 5) (bv 2))) (&& assertions (! b)))
+  (check-valid? (@bveq (ite assertions (bv 2) (bv 3)) (ite b (bv 3) (bv 5))) (&& (! assertions) b))
+  (check-valid? (@bveq (ite assertions (bv 2) (bv 3)) (ite b (bv 5) (bv 3))) (&& (! assertions) (! b))))
                 
 (define (check-bvcmp-simplifications l* g*)
   (check-equal? (g* x y) (l* y x))
@@ -100,12 +100,12 @@
   (check-valid? (l* (bv 1) (ite b (bv 0) (bv 3))) (! b))
   (check-valid? (l* (bv 3) (ite b (bv 2) (bv 1))) #f)
   (check-valid? (l* (bv 0) (ite b (bv 2) (bv 1))) #t)
-  (check-valid? (l* (ite a (bv 2) (bv 1)) (ite b (bv 3) (bv 4))) #t)
-  (check-valid? (l* (ite b (bv 3) (bv 4)) (ite a (bv 2) (bv 1))) #f)
-  (check-valid? (l* (ite a (bv 3) (bv 1)) (ite b (bv 0) (bv 2))) (&& (! a) (! b)))
-  (check-valid? (l* (ite a (bv 1) (bv 3)) (ite b (bv 2) (bv 0))) (&& a b))
-  (check-valid? (l* (ite a (bv 1) (bv 3)) (ite b (bv 0) (bv 2))) (&& a (! b)))
-  (check-valid? (l* (ite a (bv 3) (bv 1)) (ite b (bv 2) (bv 0))) (&& (! a) b)))
+  (check-valid? (l* (ite assertions (bv 2) (bv 1)) (ite b (bv 3) (bv 4))) #t)
+  (check-valid? (l* (ite b (bv 3) (bv 4)) (ite assertions (bv 2) (bv 1))) #f)
+  (check-valid? (l* (ite assertions (bv 3) (bv 1)) (ite b (bv 0) (bv 2))) (&& (! assertions) (! b)))
+  (check-valid? (l* (ite assertions (bv 1) (bv 3)) (ite b (bv 2) (bv 0))) (&& assertions b))
+  (check-valid? (l* (ite assertions (bv 1) (bv 3)) (ite b (bv 0) (bv 2))) (&& assertions (! b)))
+  (check-valid? (l* (ite assertions (bv 3) (bv 1)) (ite b (bv 2) (bv 0))) (&& (! assertions) b)))
 
 (define (check-bvslt-simplifications)
   (check-bvcmp-simplifications @bvslt @bvsgt)
@@ -385,29 +385,29 @@
 (define (phi . xs) (apply merge* xs))
 
 (define-syntax-rule (check-state actual expected-value expected-asserts)
-  (let-values ([(v a) (with-asserts actual)])
+  (let-values ([(v actual-assumes actual-asserts) (vcgen-eval actual)])
     (check-equal? v expected-value)
-    (check-equal? (apply set a) (apply set expected-asserts))))
+    (check-equal? (apply set actual-asserts) (apply set expected-asserts))))
 
 (define-syntax check-bv-exn
   (syntax-rules ()
     [(_ expr)
-     (check-exn #px"expected bitvectors of same length" (thunk (with-asserts-only expr)))]
+     (check-exn #px"expected bitvectors of same length" (thunk (begin (vcgen expr) (void))))]
     [(_ pred expr)
-     (check-exn pred (thunk (with-asserts-only expr)))]))
+     (check-exn pred (thunk (begin (vcgen expr) (void))))]))
          
 (define (check-lifted-unary)
   (define-symbolic* n @integer?)
   (check-not-exn (thunk (@bvnot (bv 1))))
   (check-bv-exn (@bvnot n))
-  (check-bv-exn (@bvnot (phi (cons a 1) (cons b '()))))
-  (check-state (@bvnot (phi (cons a 1) (cons b (bv -1)))) (bv 0) (list b))
-  (check-state (@bvnot (phi (cons a 1) (cons b x) (cons c '()) (cons d (bv -1 2))))
+  (check-bv-exn (@bvnot (phi (cons assertions 1) (cons b '()))))
+  (check-state (@bvnot (phi (cons assertions 1) (cons b (bv -1)))) (bv 0) (list b))
+  (check-state (@bvnot (phi (cons assertions 1) (cons b x) (cons c '()) (cons d (bv -1 2))))
                (phi (cons b (@bvnot x)) (cons d (bv 0 2))) (list (|| b d)))
-  (check-state (@bvnot (phi (cons a 1) (cons b x) (cons c '()) (cons d (bv -1))))
+  (check-state (@bvnot (phi (cons assertions 1) (cons b x) (cons c '()) (cons d (bv -1))))
                (@bvnot (phi (cons b x) (cons d (bv -1 4)))) (list (|| b d)))
-  (check-state (@bvnot (phi (cons a (bv 0 2)) (cons b (bv -1))))
-               (phi (cons a (bv -1 2)) (cons b (bv 0))) (list)))
+  (check-state (@bvnot (phi (cons assertions (bv 0 2)) (cons b (bv -1))))
+               (phi (cons assertions (bv -1 2)) (cons b (bv 0))) (list)))
 
 
 (define (check-lifted-binary)
@@ -415,38 +415,38 @@
   (check-not-exn (thunk (@bvsdiv x y)))
   (check-bv-exn (@bvsdiv x 1))
   (check-bv-exn (@bvsdiv 1 x))
-  (check-state (@bvsdiv x (phi (cons a 1) (cons b y) (cons c (bv 1 2)))) 
+  (check-state (@bvsdiv x (phi (cons assertions 1) (cons b y) (cons c (bv 1 2)))) 
                (@bvsdiv x y) (list b))
-  (check-state (@bvsdiv (phi (cons a 1) (cons b y) (cons c (bv 1 2))) x) 
+  (check-state (@bvsdiv (phi (cons assertions 1) (cons b y) (cons c (bv 1 2))) x) 
                (@bvsdiv y x) (list b))
-  (check-bv-exn (@bvsdiv (phi (cons a 1) (cons b #f)) (phi (cons c '()) (cons d 3))))
-  (check-bv-exn (@bvsdiv (phi (cons a 1) (cons b x)) (phi (cons c '()) (cons d 3))))
-  (check-bv-exn (@bvsdiv (phi (cons a 1) (cons b #f)) (phi (cons c '()) (cons d x))))
-  (check-bv-exn (@bvsdiv (phi (cons a 1) (cons b x)) 
+  (check-bv-exn (@bvsdiv (phi (cons assertions 1) (cons b #f)) (phi (cons c '()) (cons d 3))))
+  (check-bv-exn (@bvsdiv (phi (cons assertions 1) (cons b x)) (phi (cons c '()) (cons d 3))))
+  (check-bv-exn (@bvsdiv (phi (cons assertions 1) (cons b #f)) (phi (cons c '()) (cons d x))))
+  (check-bv-exn (@bvsdiv (phi (cons assertions 1) (cons b x)) 
                          (phi (cons c '()) (cons d (bv 1 2)))))
-  (check-state (@bvsdiv (phi (cons a 1) (cons b x)) (phi (cons c y) (cons d '())))
+  (check-state (@bvsdiv (phi (cons assertions 1) (cons b x)) (phi (cons c y) (cons d '())))
                (@bvsdiv x y) (list (&& b c)))
-  (check-state (@bvsdiv (phi (cons a (bv 1 2)) (cons b x)) 
+  (check-state (@bvsdiv (phi (cons assertions (bv 1 2)) (cons b x)) 
                         (phi (cons c y) (cons d '())))
                (@bvsdiv x y) (list (&& b c)))
-  (check-state (@bvsdiv (phi (cons a (bv 1 2)) (cons b x) (cons e 'e)) 
+  (check-state (@bvsdiv (phi (cons assertions (bv 1 2)) (cons b x) (cons e 'e)) 
                         (phi (cons f "f") (cons c y) (cons d '())))
                (@bvsdiv x y) (list (&& b c)))
-  (check-state (@bvsdiv (phi (cons a (bv 6 8)) (cons b x)) 
+  (check-state (@bvsdiv (phi (cons assertions (bv 6 8)) (cons b x)) 
                         (phi (cons c y) (cons d (bv 2 8))))
                (phi (cons (&& b c) (@bvsdiv x y))
-                    (cons (&& a d) (bv 3 8))) 
+                    (cons (&& assertions d) (bv 3 8))) 
                (list ))
-  (check-state (@bvsdiv (phi (cons a (bv 6 8)) (cons b x)) 
+  (check-state (@bvsdiv (phi (cons assertions (bv 6 8)) (cons b x)) 
                         (phi (cons c y) (cons d (bv 2 8)) (cons e 'e)))
                (phi (cons (&& b c) (@bvsdiv x y))
-                    (cons (&& a d) (bv 3 8))) 
-               (list (|| (&& b c) (&& a d))))
-  (check-state (@bvsdiv (phi (cons a (bv 6 8)) (cons b x) (cons e 'e)) 
+                    (cons (&& assertions d) (bv 3 8))) 
+               (list (|| (&& b c) (&& assertions d))))
+  (check-state (@bvsdiv (phi (cons assertions (bv 6 8)) (cons b x) (cons e 'e)) 
                         (phi (cons c y) (cons d (bv 2 8))))
                (phi (cons (&& b c) (@bvsdiv x y))
-                    (cons (&& a d) (bv 3 8))) 
-               (list (|| (&& b c) (&& a d))))
+                    (cons (&& assertions d) (bv 3 8))) 
+               (list (|| (&& b c) (&& assertions d))))
   )
 
 (define (check-@bvadd-exn bad-arg)
@@ -459,59 +459,59 @@
   (check-not-exn (thunk (@bvadd x y z)))
   (check-@bvadd-exn 1)
   (check-@bvadd-exn n)
-  (check-@bvadd-exn (phi (cons a 1) (cons b (bv 2 2))))
-  (check-state (@bvadd z (phi (cons a 1) (cons b x)) (phi (cons c y) (cons d '())))
+  (check-@bvadd-exn (phi (cons assertions 1) (cons b (bv 2 2))))
+  (check-state (@bvadd z (phi (cons assertions 1) (cons b x)) (phi (cons c y) (cons d '())))
                (@bvadd z x y) (list b c))
-  (check-state (@bvadd z (phi (cons a 1) (cons b x)) y)
+  (check-state (@bvadd z (phi (cons assertions 1) (cons b x)) y)
                (@bvadd z x y) (list b))
-  (check-bv-exn (@bvadd (phi (cons a 1) (cons b x)) 
+  (check-bv-exn (@bvadd (phi (cons assertions 1) (cons b x)) 
                         (phi (cons c 2) (cons d #f))
                         (phi (cons e 'e) (cons f (bv 1 2)))))
-  (check-bv-exn (@bvadd (phi (cons a 1) (cons b x)) 
+  (check-bv-exn (@bvadd (phi (cons assertions 1) (cons b x)) 
                         (phi (cons c 2) (cons d #f))
                         (phi (cons e y) (cons f (bv 1 2)))))
-  (check-bv-exn (@bvadd (phi (cons a 1) (cons b x)) 
+  (check-bv-exn (@bvadd (phi (cons assertions 1) (cons b x)) 
                         (phi (cons c y) (cons d #f))
                         (phi (cons e 'e) (cons f (bv 1 2)))))
-  (check-state (@bvadd (phi (cons a x) (cons b (bv 1 8))) 
+  (check-state (@bvadd (phi (cons assertions x) (cons b (bv 1 8))) 
                        (phi (cons c y) (cons d (bv 2 8)))
                        (phi (cons e z) (cons f (bv 3 8))))
-               (phi (cons (&& a c e) (@bvadd x y z))
+               (phi (cons (&& assertions c e) (@bvadd x y z))
                     (cons (&& b d f) (bv 6 8)))
                (list))
-  (check-state (@bvadd (phi (cons a 1) (cons b (bv 1 8))) 
+  (check-state (@bvadd (phi (cons assertions 1) (cons b (bv 1 8))) 
                        (phi (cons c y) (cons d (bv 2 8)))
                        (phi (cons e z) (cons f (bv 3 8))))
                (bv 6 8)
                (list (&& b d f)))
-  (check-state (@bvadd (phi (cons a x) (cons b (bv 1 8))) 
+  (check-state (@bvadd (phi (cons assertions x) (cons b (bv 1 8))) 
                        (phi (cons c 1) (cons d (bv 2 8)))
                        (phi (cons e z) (cons f (bv 3 8))))
                (bv 6 8)
                (list (&& b d f)))
-  (check-state (@bvadd (phi (cons a x) (cons b (bv 1 8))) 
+  (check-state (@bvadd (phi (cons assertions x) (cons b (bv 1 8))) 
                        (phi (cons c y) (cons d (bv 2 8)))
                        (phi (cons e 1) (cons f (bv 3 8))))
                (bv 6 8)
                (list (&& b d f)))
-  (check-state (@bvadd (phi (cons a x) (cons b (bv 1 8))) 
+  (check-state (@bvadd (phi (cons assertions x) (cons b (bv 1 8))) 
                        (phi (cons c y) (cons d (bv 2 8)) (cons g 'g))
                        (phi (cons e z) (cons f (bv 3 8))))
-               (phi (cons (&& a c e) (@bvadd x y z))
+               (phi (cons (&& assertions c e) (@bvadd x y z))
                     (cons (&& b d f) (bv 6 8)))
-               (list (|| (&& a c e) (&& b d f))))
-  (check-state (@bvadd (phi (cons a x) (cons b (bv 1 8))) 
+               (list (|| (&& assertions c e) (&& b d f))))
+  (check-state (@bvadd (phi (cons assertions x) (cons b (bv 1 8))) 
                        (phi (cons c y) (cons d (bv 2 8)) )
                        (phi (cons e z) (cons f (bv 3 8)) (cons g 'g)))
-               (phi (cons (&& a c e) (@bvadd x y z))
+               (phi (cons (&& assertions c e) (@bvadd x y z))
                     (cons (&& b d f) (bv 6 8)))
-               (list (|| (&& a c e) (&& b d f))))
-  (check-state (@bvadd (phi (cons a x) (cons g 'g) (cons b (bv 1 8))) 
+               (list (|| (&& assertions c e) (&& b d f))))
+  (check-state (@bvadd (phi (cons assertions x) (cons g 'g) (cons b (bv 1 8))) 
                        (phi (cons c y) (cons d (bv 2 8)) )
                        (phi (cons e z) (cons f (bv 3 8))))
-               (phi (cons (&& a c e) (@bvadd x y z))
+               (phi (cons (&& assertions c e) (@bvadd x y z))
                     (cons (&& b d f) (bv 6 8)))
-               (list (|| (&& a c e) (&& b d f)))))
+               (list (|| (&& assertions c e) (&& b d f)))))
 
 (define (check-lifted-concat)
   (define-symbolic* n @integer?)
@@ -521,53 +521,53 @@
   (check-bv-exn exn:fail? (@concat 1))
   (check-bv-exn exn:fail? (@concat 1 x))
   (check-bv-exn exn:fail? (@concat x n))
-  (check-bv-exn exn:fail? (@concat x (phi (cons a 1) (cons b '()))))
-  (check-bv-exn exn:fail? (@concat (phi (cons a 1) (cons b '())) x))
-  (check-state (@concat x (phi (cons a 1) (cons b (bv 2 8))))
+  (check-bv-exn exn:fail? (@concat x (phi (cons assertions 1) (cons b '()))))
+  (check-bv-exn exn:fail? (@concat (phi (cons assertions 1) (cons b '())) x))
+  (check-state (@concat x (phi (cons assertions 1) (cons b (bv 2 8))))
                (@concat x (bv 2 8)) (list b))
-  (check-state (@concat (phi (cons a 1) (cons b (bv 2 8))) x)
+  (check-state (@concat (phi (cons assertions 1) (cons b (bv 2 8))) x)
                (@concat (bv 2 8) x) (list b))
-  (check-state (@concat x (phi (cons a 1) (cons b (bv 2 8)) (cons c y)))
+  (check-state (@concat x (phi (cons assertions 1) (cons b (bv 2 8)) (cons c y)))
                (phi (cons b (@concat x (bv 2 8)))
                     (cons c (@concat x y))) 
                (list (|| b c)))
-  (check-state (@concat x (phi (cons a 1) (cons b (bv 2 8)) (cons c y)) z)
+  (check-state (@concat x (phi (cons assertions 1) (cons b (bv 2 8)) (cons c y)) z)
                (phi (cons b (@concat x (bv 2 8) z))
                     (cons c (@concat x y z))) 
                (list (|| b c)))
-  (check-state (@concat (phi (cons a x) (cons b (bv 2 8))) 
+  (check-state (@concat (phi (cons assertions x) (cons b (bv 2 8))) 
                         (phi (cons c y) (cons d (bv 1 2))))
-               (phi (cons (&& a c) (@concat x y))
-                    (cons (&& a d) (@concat x (bv 1 2)))
+               (phi (cons (&& assertions c) (@concat x y))
+                    (cons (&& assertions d) (@concat x (bv 1 2)))
                     (cons (&& b c) (@concat (bv 2 8) y))
                     (cons (&& b d) (@concat (bv 2 8) (bv 1 2))))
                (list))
-   (check-state (@concat (phi (cons a x) (cons b 1)) 
+   (check-state (@concat (phi (cons assertions x) (cons b 1)) 
                         (phi (cons c y) (cons d (bv 1 2))))
                (phi (cons c (@concat x y))
                     (cons d (@concat x (bv 1 2))))
-               (list a))
-  (check-state (@concat (phi (cons a x) (cons b 1)) 
+               (list assertions))
+  (check-state (@concat (phi (cons assertions x) (cons b 1)) 
                         (phi (cons c y) (cons d 2)))
                (@concat x y)
-               (list a c)) 
-  (check-state (@concat (phi (cons a x) (cons e '3)) 
+               (list assertions c)) 
+  (check-state (@concat (phi (cons assertions x) (cons e '3)) 
                         (phi (cons c y) (cons d (bv 1 2)) (cons f 'f)))
                (phi (cons c (@concat x y))
                     (cons d (@concat x (bv 1 2))))
-               (list a (|| c d)) ))
+               (list assertions (|| c d)) ))
 
 (define (check-lifted-extract)
   (define-symbolic* i j @integer?)
   (check-bv-exn #px"expected integer\\?" (@extract "1" 2 x))
   (check-bv-exn #px"expected integer\\?" (@extract 1 "2" x))
-  (check-bv-exn #px"expected: bitvector\\?" (@extract 2 1 (phi (cons a 3) (cons b '()))))
+  (check-bv-exn #px"expected: bitvector\\?" (@extract 2 1 (phi (cons assertions 3) (cons b '()))))
   (check-bv-exn #px"expected integer\\?" (@extract 2.3 2 x))  
   (check-bv-exn #px"expected integer\\?" (@extract 2 1.9 x))  
   (check-bv-exn #px"expected i >= j" (@extract 2 3 x))  
   (check-bv-exn #px"expected j >= 0" (@extract 2 -1 x))
   (check-bv-exn #px"expected \\(size-of x\\) > i" (@extract 4 1 x))
-  (check-bv-exn exn:fail? (@extract 4 1 (phi (cons a x) (cons b 1))))
+  (check-bv-exn exn:fail? (@extract 4 1 (phi (cons assertions x) (cons b 1))))
   (check-state (@extract 2 1 x) (@extract 2 1 x) (list))
   (check-state (@extract i 3 x) (@extract 3 3 x) (list (@< i 4) (@<= 3 i)))
   (check-state (@extract i 2 x) 
@@ -584,30 +584,30 @@
                     (cons (&& (@= i 1) (@= j 0)) (@extract 1 0 (bv 2 2)))
                     (cons (&& (@= i 0) (@= j 0)) (@extract 0 0 (bv 2 2))))
                (list (@<= 0 j) (@<= j i) (@< i 2)))
-  (check-state (@extract 2 1 (phi (cons a x) (cons b 3))) 
-               (@extract 2 1 x) (list a))
-  (check-state (@extract i 3 (phi (cons a x) (cons b 3) (cons c y) (cons d '()))) 
-               (@extract 3 3 (phi (cons a x)  (cons c y)))
-               (list  (@<= 3 i) (@< i 4) (|| a c)))
-  (check-state (@extract i 2 (phi (cons a x) (cons b 3) (cons c y) (cons d '()))) 
-               (phi (cons (@= i 3) (@extract 3 2 (phi (cons a x)  (cons c y))))
-                    (cons (@= i 2) (@extract 2 2 (phi (cons a x)  (cons c y)))))
-               (list  (@<= 2 i) (@< i 4) (|| a c)))
-  (check-state (@extract 0 j (phi (cons a x) (cons b 3) (cons c y) (cons d '()))) 
-               (@extract 0 0 (phi (cons a x)  (cons c y))) 
-               (list (@<= 0 j) (|| a c) (@<= j 0)))
-  (check-state (@extract 1 j (phi (cons a x) (cons b 3) (cons c y) (cons d '())))  
-               (phi (cons (@= j 0) (@extract 1 0 (phi (cons a x)  (cons c y)))) 
-                    (cons (@= j 1) (@extract 1 1 (phi (cons a x)  (cons c y))))) 
-               (list (@<= j 1) (@<= 0 j) (|| a c)))
-  (check-state (@extract i j (phi (cons a (bv 2 2)) (cons b 3) (cons c (bv 1 1))))
-               (phi (cons (&& a (@= i 1) (@= j 0)) (@extract 1 0 (bv 2 2)))
-                    (cons (|| c (&& a (|| (&& (@= i 1) (@= j 1)) (&& (@= i 0) (@= j 0)))))
-                          (phi (cons (&& a (|| (&& (@= i 1) (@= j 1)) (&& (@= i 0) (@= j 0))))
+  (check-state (@extract 2 1 (phi (cons assertions x) (cons b 3))) 
+               (@extract 2 1 x) (list assertions))
+  (check-state (@extract i 3 (phi (cons assertions x) (cons b 3) (cons c y) (cons d '()))) 
+               (@extract 3 3 (phi (cons assertions x)  (cons c y)))
+               (list  (@<= 3 i) (@< i 4) (|| assertions c)))
+  (check-state (@extract i 2 (phi (cons assertions x) (cons b 3) (cons c y) (cons d '()))) 
+               (phi (cons (@= i 3) (@extract 3 2 (phi (cons assertions x)  (cons c y))))
+                    (cons (@= i 2) (@extract 2 2 (phi (cons assertions x)  (cons c y)))))
+               (list  (@<= 2 i) (@< i 4) (|| assertions c)))
+  (check-state (@extract 0 j (phi (cons assertions x) (cons b 3) (cons c y) (cons d '()))) 
+               (@extract 0 0 (phi (cons assertions x)  (cons c y))) 
+               (list (@<= 0 j) (|| assertions c) (@<= j 0)))
+  (check-state (@extract 1 j (phi (cons assertions x) (cons b 3) (cons c y) (cons d '())))  
+               (phi (cons (@= j 0) (@extract 1 0 (phi (cons assertions x)  (cons c y)))) 
+                    (cons (@= j 1) (@extract 1 1 (phi (cons assertions x)  (cons c y))))) 
+               (list (@<= j 1) (@<= 0 j) (|| assertions c)))
+  (check-state (@extract i j (phi (cons assertions (bv 2 2)) (cons b 3) (cons c (bv 1 1))))
+               (phi (cons (&& assertions (@= i 1) (@= j 0)) (@extract 1 0 (bv 2 2)))
+                    (cons (|| c (&& assertions (|| (&& (@= i 1) (@= j 1)) (&& (@= i 0) (@= j 0)))))
+                          (phi (cons (&& assertions (|| (&& (@= i 1) (@= j 1)) (&& (@= i 0) (@= j 0))))
                                      (phi (cons (&& (@= i 1) (@= j 1)) (@extract 1 1 (bv 2 2)))
                                           (cons (&& (@= i 0) (@= j 0)) (@extract 0 0 (bv 2 2)))))
                                (cons c (@extract 0 0 (bv 1 1))))))
-               (list (|| a c) (|| (@< i 1) (! c)) (|| (@< i 2) (! a)) (@<= 0 j) (@<= j i)))           
+               (list (|| assertions c) (|| (@< i 1) (! c)) (|| (@< i 2) (! assertions)) (@<= 0 j) (@<= j i)))           
   )
     
 (define (check-lifted-extend)
@@ -615,75 +615,75 @@
   (check-bv-exn #px"expected: bitvector\\?" (@sign-extend 1 BV))
   (check-bv-exn err (@sign-extend x 1))
   (check-bv-exn err (@sign-extend x (bitvector 2)))
-  (check-bv-exn err (@sign-extend (phi (cons a x) (cons b (bv 3 3))) (bitvector 2)))
-  (check-bv-exn err (@sign-extend x (phi (cons a (bitvector 2)) (cons b 1))))
-  (check-bv-exn err (@sign-extend (phi (cons a x) (cons b (bv 3 3))) 
+  (check-bv-exn err (@sign-extend (phi (cons assertions x) (cons b (bv 3 3))) (bitvector 2)))
+  (check-bv-exn err (@sign-extend x (phi (cons assertions (bitvector 2)) (cons b 1))))
+  (check-bv-exn err (@sign-extend (phi (cons assertions x) (cons b (bv 3 3))) 
                                   (phi (cons c (bitvector 2)) (cons d (bitvector 1)))))
   (check-state (@sign-extend x (bitvector 5)) (@sign-extend x (bitvector 5)) (list))
-  (check-state (@sign-extend (phi (cons a x) (cons b (bv 3 3))) BV)
-               (phi (cons a x) (cons b (@sign-extend (bv 3 3) BV))) 
+  (check-state (@sign-extend (phi (cons assertions x) (cons b (bv 3 3))) BV)
+               (phi (cons assertions x) (cons b (@sign-extend (bv 3 3) BV))) 
                (list))
-  (check-state (@sign-extend (phi (cons a x) (cons b (bv 3 5))) BV)
+  (check-state (@sign-extend (phi (cons assertions x) (cons b (bv 3 5))) BV)
                x
-               (list a))
-  (check-state (@sign-extend (phi (cons a x) (cons b (bv 3 3)) (cons c 1)) BV)
-               (phi (cons a x) (cons b (@sign-extend (bv 3 3) BV))) 
-               (list (|| a b)))
-  (check-state (@sign-extend x (phi (cons a BV) (cons b (bitvector 5))))
-               (phi (cons a x) (cons b (@sign-extend x (bitvector 5))))
+               (list assertions))
+  (check-state (@sign-extend (phi (cons assertions x) (cons b (bv 3 3)) (cons c 1)) BV)
+               (phi (cons assertions x) (cons b (@sign-extend (bv 3 3) BV))) 
+               (list (|| assertions b)))
+  (check-state (@sign-extend x (phi (cons assertions BV) (cons b (bitvector 5))))
+               (phi (cons assertions x) (cons b (@sign-extend x (bitvector 5))))
                (list))
-  (check-state (@sign-extend x (phi (cons a BV) (cons b (bitvector 3))))
+  (check-state (@sign-extend x (phi (cons assertions BV) (cons b (bitvector 3))))
                x
-               (list a))
-  (check-state (@sign-extend x (phi (cons a BV) (cons b (bitvector 5)) (cons c (bitvector 3)) (cons d 1)))
-               (phi (cons a x) (cons b (@sign-extend x (bitvector 5))))
-               (list (|| a b)))
-  (check-state (@sign-extend (phi (cons a x) (cons b (bv 3 3)))
+               (list assertions))
+  (check-state (@sign-extend x (phi (cons assertions BV) (cons b (bitvector 5)) (cons c (bitvector 3)) (cons d 1)))
+               (phi (cons assertions x) (cons b (@sign-extend x (bitvector 5))))
+               (list (|| assertions b)))
+  (check-state (@sign-extend (phi (cons assertions x) (cons b (bv 3 3)))
                              (phi (cons c BV) (cons d (bitvector 5))))
-               (phi (cons (&& a c) x) 
-                    (cons (&& a d) (@sign-extend x (bitvector 5)))
+               (phi (cons (&& assertions c) x) 
+                    (cons (&& assertions d) (@sign-extend x (bitvector 5)))
                     (cons (&& b c) (@sign-extend (bv 3 3) BV))
                     (cons (&& b d) (@sign-extend (bv 3 3) (bitvector 5))))
                (list))
-  (check-state (@sign-extend (phi (cons a x) (cons b (bv 3 3)) (cons e 'e))
+  (check-state (@sign-extend (phi (cons assertions x) (cons b (bv 3 3)) (cons e 'e))
                              (phi (cons c BV) (cons d (bitvector 5))))
-               (phi (cons (&& a c) x) 
-                    (cons (&& a d) (@sign-extend x (bitvector 5)))
+               (phi (cons (&& assertions c) x) 
+                    (cons (&& assertions d) (@sign-extend x (bitvector 5)))
                     (cons (&& b c) (@sign-extend (bv 3 3) BV))
                     (cons (&& b d) (@sign-extend (bv 3 3) (bitvector 5))))
-               (list (|| a b)))
-  (check-state (@sign-extend (phi (cons a x) (cons b (bv 3 3)))
+               (list (|| assertions b)))
+  (check-state (@sign-extend (phi (cons assertions x) (cons b (bv 3 3)))
                              (phi (cons c BV) (cons d (bitvector 5)) (cons e 'e)))
-               (phi (cons (&& a c) x) 
-                    (cons (&& a d) (@sign-extend x (bitvector 5)))
+               (phi (cons (&& assertions c) x) 
+                    (cons (&& assertions d) (@sign-extend x (bitvector 5)))
                     (cons (&& b c) (@sign-extend (bv 3 3) BV))
                     (cons (&& b d) (@sign-extend (bv 3 3) (bitvector 5))))
-               (list (|| (&& a c) (&& a d) (&& b c) (&& b d))))
-  (check-state (@sign-extend (phi (cons a x) (cons b (bv 8 8)))
+               (list (|| (&& assertions c) (&& assertions d) (&& b c) (&& b d))))
+  (check-state (@sign-extend (phi (cons assertions x) (cons b (bv 8 8)))
                              (phi (cons c BV) (cons d (bitvector 1)) (cons e 'e)))
                x
-               (list (&& a c))))
+               (list (&& assertions c))))
   
 (define (check-lifted-integer->bitvector)
   (check-bv-exn exn:fail? (@integer->bitvector "3" BV))
   (check-bv-exn #px"expected a bitvector type" (@integer->bitvector 3 3))
-  (check-bv-exn #px"expected a bitvector type" (@integer->bitvector 3 (phi (cons a 1) (cons b "3"))))
+  (check-bv-exn #px"expected a bitvector type" (@integer->bitvector 3 (phi (cons assertions 1) (cons b "3"))))
   (check-state (@integer->bitvector 3 BV) (bv 3 4) (list))
-  (check-state (@integer->bitvector (phi (cons a 3) (cons b "3")) BV) (bv 3 4) (list a))
-  (check-state (@integer->bitvector 3 (phi (cons a BV) (cons b (bitvector 3))))
-               (phi (cons a (bv 3 4)) (cons b (bv 3 3))) (list))
-  (check-state (@integer->bitvector 3 (phi (cons a BV) (cons b (bitvector 3)) (cons c '())))
-               (phi (cons a (bv 3 4)) (cons b (bv 3 3))) (list (|| a b))))
+  (check-state (@integer->bitvector (phi (cons assertions 3) (cons b "3")) BV) (bv 3 4) (list assertions))
+  (check-state (@integer->bitvector 3 (phi (cons assertions BV) (cons b (bitvector 3))))
+               (phi (cons assertions (bv 3 4)) (cons b (bv 3 3))) (list))
+  (check-state (@integer->bitvector 3 (phi (cons assertions BV) (cons b (bitvector 3)) (cons c '())))
+               (phi (cons assertions (bv 3 4)) (cons b (bv 3 3))) (list (|| assertions b))))
 
 (define (check-lifted-bv->*)
   (check-bv-exn #px"expected: bitvector\\?" (@bitvector->integer 3))
   (check-state (@bitvector->integer (bv 3 3)) 3 (list))
-  (check-state (@bitvector->integer (phi (cons a (bv 3 4)) (cons b (bv 3 3)))) 
-               (phi (cons a 3) (cons b 3)) (list))
-  (check-state (@bitvector->integer (phi (cons a (bv 3 4)) (cons b 3)))
-               3 (list a))
-  (check-state (@bitvector->integer (phi (cons a (bv 3 4)) (cons b (bv 3 3)) (cons c '()))) 
-               (phi (cons a 3) (cons b 3)) (list (|| a b))))
+  (check-state (@bitvector->integer (phi (cons assertions (bv 3 4)) (cons b (bv 3 3)))) 
+               (phi (cons assertions 3) (cons b 3)) (list))
+  (check-state (@bitvector->integer (phi (cons assertions (bv 3 4)) (cons b 3)))
+               3 (list assertions))
+  (check-state (@bitvector->integer (phi (cons assertions (bv 3 4)) (cons b (bv 3 3)) (cons c '()))) 
+               (phi (cons assertions 3) (cons b 3)) (list (|| assertions b))))
   
 
 (define tests:bv

test/base/finitize.rkt

@@ -34,13 +34,12 @@
                                 (finitized-solution v))))))
 
 (define-syntax-rule (finitize/solve bw constraint ...)
-  (let* ([terms (with-asserts-only 
-                 (begin (@assert constraint) ...))]
-         [fmap (finitize terms bw)]
-         [fsol (apply solve (map (curry hash-ref fmap) terms))])
+  (let*-values ([(assumptions assertions) (vcgen (begin (@assert constraint) ...))]
+                [(fmap) (finitize assertions bw)]
+                [(fsol) (apply solve (map (curry hash-ref fmap) assertions))])
     (lift-solution fsol fmap)))
 
-(define (terms t) ; produces a hashmap from each typed? subterm in t to itself
+(define (assertions t) ; produces a hashmap from each typed? subterm in t to itself
   (define env (make-hash))
   (define (rec v)
     (when (typed? v)
@@ -53,7 +52,7 @@
   (for/hash ([(k v) env]) (values k v)))
 
 (define (check-pure-bitvector-term t)
-  (define expected (terms t))
+  (define expected (assertions t))
   (define actual (for/hash ([(k v) (finitize (list t) bw)] #:when (typed? k))
                    (values k v)))
   ;(printf "expected: ~a\nactual: ~a\n" expected actual)

test/base/merge.rkt

@@ -63,6 +63,11 @@
 
 
 (define (procedure-merge-tests)
+
+  (define-syntax-rule (count-asserts expr)
+    (let-values ([(assumptions assertions) (vcgen expr)])
+      (length assertions)))
+  
   (check-equal? (merge a identity identity) identity)
   (check-equal? (@procedure? (merge a identity 2)) a)
   
@@ -80,18 +85,18 @@
   (define s* (merge a s *))
   (check-equal? (s*) 1)
   (check-true (null? (asserts)))
-  (check-equal? (length (with-asserts-only (check-equal? (s* 3 2) 6))) 1)
+  (check-equal? (count-asserts (check-equal? (s* 3 2) 6)) 1)
   
   (define (kw #:kw y) (- y))
   (define f (merge b + 'f))
   (define g (merge c s* f))
   (check-equal? 
-   (length (with-asserts-only (check-equal? (g) (ite* (cons (&& b (! c)) 0) (cons (|| (&& c (! a)) (&& a c)) 1)))))
+   (count-asserts (check-equal? (g) (ite* (cons (&& b (! c)) 0) (cons (|| (&& c (! a)) (&& a c)) 1))))
    1)
   
   (define h (merge c kw f))
   (check-equal?
-   (length (with-asserts-only (check-equal? (h #:kw 3) -3)))
+   (count-asserts (check-equal? (h #:kw 3) -3))
    2)
   
   )

test/base/quantified.rkt

@@ -4,10 +4,10 @@
          rosette/base/core/term rosette/base/core/bool)
 
 (define-syntax-rule (check-state actual expected-value expected-asserts)
-  (let-values ([(e ignore) (with-asserts expected-value)]
-               [(v a) (with-asserts actual)])
+  (let-values ([(e ignore-assumes ignore-asserts) (vcgen-eval expected-value)]
+               [(v actual-assumes actual-asserts) (vcgen-eval actual)])
     (check-equal? v e)
-    (check-equal? (apply set a) (apply set expected-asserts))))
+    (check-equal? (apply set actual-asserts) (apply set expected-asserts))))
 
 (define (check-pe op)
   (define-symbolic a boolean?)

test/base/real.rkt

@@ -43,9 +43,9 @@
 
 (define-syntax-rule (check-cast (type val) (accepted? result))
   (with-handlers ([exn:fail? (lambda (e) (check-equal? accepted? #f))])  
-    (let-values ([(actual-result asserts) (with-asserts (type-cast type val))])
+    (let-values ([(actual-result actual-assumes actual-asserts) (vcgen-eval (type-cast type val))])
       (check-equal? actual-result result)
-      (match asserts
+      (match actual-asserts
         [(list)   (check-equal? accepted? #t)]
         [(list v) (check-equal? accepted? v)]
         [_ (fail "found more than 1 assertion")]))))
@@ -83,14 +83,14 @@
 (define-syntax check-num-exn
   (syntax-rules ()
     [(_ expr)
-     (check-exn exn:fail? (thunk (with-asserts-only expr)))]
+     (check-exn exn:fail? (thunk (vcgen expr)))]
     [(_ pred expr)
-     (check-exn pred (thunk (with-asserts-only expr)))]))
+     (check-exn pred (thunk (vcgen expr)))]))
 
 (define-syntax-rule (check-state actual expected-value expected-asserts)
-  (let-values ([(v a) (with-asserts actual)])
+  (let-values ([(v actual-assumes actual-asserts) (vcgen-eval actual)])
     (check-equal? v expected-value)
-    (check-equal? (apply set a) (apply set expected-asserts))))
+    (check-equal? (apply set actual-asserts) (apply set expected-asserts))))
 
 (define (check-real?)
   (check-equal? (@real? 1) #t)

test/base/uninterpreted.rkt

@@ -81,10 +81,10 @@
   (check-pred unsat? (solve (assert (= (f #f) .5)))))
 
 (define-syntax-rule (check-state actual expected-value expected-asserts)
-  (let-values ([(e ignore) (with-asserts expected-value)]
-               [(v a) (with-asserts actual)])
+  (let-values ([(e ignore-assumes ignore-asserts) (vcgen-eval expected-value)]
+               [(v actual-assumes actual-asserts) (vcgen-eval actual)])
     (check-equal? v e)
-    (check-equal? (apply set a) (apply set expected-asserts))))
+    (check-equal? (apply set actual-asserts) (apply set expected-asserts))))
 
 (define (check-types)
   (define-symbolic a boolean?)

test/query/synthesize.rkt

@@ -11,29 +11,42 @@
   (test-suite+ "Basic synthesis tests."
     (current-bitwidth #f)
     
-    (check-unsat (synthesize #:forall '() #:guarantee (assert #f)))
-    (check-unsat (synthesize #:forall '() #:assume (assert #f) #:guarantee (assert #f)))
+    (check-unsat (synthesize #:forall '()
+                             #:guarantee (assert #f)))
+    
+    (check-unsat (synthesize #:forall '()
+                             #:guarantee (begin (assume #f)
+                                                (assert #f))))
 
     (check-equal?
-     (model (check-sat (synthesize #:forall a #:assume (assert a) #:guarantee (assert (&& a b)))))
+     (model (check-sat (synthesize #:forall a
+                                   #:guarantee (begin (assume a)
+                                                      (assert (&& a b))))))
      (hash b #t))
     
-    (check-unsat (synthesize #:forall xb #:guarantee (assert (bvslt xb (bvadd xb yb)))))
+    (check-unsat (synthesize #:forall xb
+                             #:guarantee (assert (bvslt xb (bvadd xb yb)))))
     
     (parameterize ([current-bitwidth 4])
-      (check-unsat (synthesize #:forall xi #:guarantee (assert (< xi (+ xi yi))))))
+      (check-unsat (synthesize #:forall xi
+                               #:guarantee (assert (< xi (+ xi yi))))))
     
     (check-true
-     (evaluate (> yi 0) (synthesize #:forall xi #:guarantee (assert (< xi (+ xi yi))))))
+     (evaluate (> yi 0) (synthesize #:forall xi
+                                    #:guarantee (assert (< xi (+ xi yi))))))
     
     (check-true
-     (evaluate (> yr 0) (synthesize #:forall xr #:guarantee (assert (< xr (+ xr yr))))))
+     (evaluate (> yr 0) (synthesize #:forall xr
+                                    #:guarantee (assert (< xr (+ xr yr))))))
     
     (check-true
-     (evaluate (> yr 0) (synthesize #:forall xi #:guarantee (assert (< xi (+ xi yr))))))
+     (evaluate (> yr 0) (synthesize #:forall xi
+                                    #:guarantee (assert (< xi (+ xi yr))))))
     
     (check-true
-     (evaluate (>= yi 0) (synthesize #:forall xi #:assume (assert (> xi 0)) #:guarantee (assert (>= xi yi)))))
+     (evaluate (>= yi 0) (synthesize #:forall xi
+                                     #:guarantee (begin (assume (> xi 0))
+                                                        (assert (>= xi yi))))))
     
     ))
 

test/query/verify.rkt

@@ -15,34 +15,34 @@
     ; basic verify tests
     (check-verify unsat? (verify (assert (or x (not x)))))
     (check-verify sat? (verify (assert (and x (not x)))))
-    (check-verify unsat? (verify #:assume (assert x) #:guarantee (assert (or x (not x)))))
-    (check-verify sat? (verify #:assume (assert x) #:guarantee (assert (not x))))
+    (check-verify unsat? (verify (begin (assume x) (assert (or x (not x))))))
+    (check-verify sat? (verify (begin (assume x) (assert (not x)))))
     
     (check-verify unsat? (verify (assert (or (>= n 0) (< n 0)))))
     (check-verify sat? (verify (assert (= n 0))))
     (check-verify sat? (verify (assert (= (* n 2) 0))))
-    (check-verify unsat? (verify #:assume (= n 0) #:guarantee (= (* n 2) 0)))
+    (check-verify unsat? (verify (begin (assume (= n 0)) (assert (= (* n 2) 0)))))
     ))
 
 (define short-circuit-tests
   (test-suite+ "Verify short-circuit tests"
     ; tests for the verify short-circuit logic
     (check-verify unsat? (verify (assert #t)))
-    (check-verify unsat? (verify #:assume (assert #f) 
-                                 #:guarantee (assert x)))  ; #f => x  is valid
-    (check-verify sat? (verify #:assume (assert #t) 
-                               #:guarantee (assert #f)))   ; #t => #f is invalid
+    (check-verify unsat? (verify (begin (assume #f)
+                                        (assert x))))  ; #f => x  is valid
+    (check-verify sat? (verify (begin (assume #t)
+                                      (assert #f))))   ; #t => #f is invalid
     
     ; unsat assumption that defeats simplification
-    (check-verify unsat? (verify #:assume (assert (and (= (+ (* 2 n) 1) 0) (not (= n 0))))
-                                 #:guarantee (assert #f)))
-    (check-verify unsat? (verify #:assume (assert (and (= (+ (* 2 n) 1) 0) (not (= n 0))))
-                                 #:guarantee (assert #t)))
+    (check-verify unsat? (verify (begin (assume (and (= (+ (* 2 n) 1) 0) (not (= n 0))))
+                                        (assert #f))))
+    (check-verify unsat? (verify (begin (assume (and (= (+ (* 2 n) 1) 0) (not (= n 0))))
+                                        (assert #t))))
     ; invalid guarantee that defeats simplification
-    (check-verify unsat? (verify #:assume (assert #f)
-                                 #:guarantee (assert (and (= (+ (* 2 n) 1) 0) (not (= n 0))))))
-    (check-verify sat? (verify #:assume (assert #t)
-                               #:guarantee (assert (and (= (+ (* 2 n) 1) 0) (not (= n 0))))))
+    (check-verify unsat? (verify (begin (assume #f)
+                                        (assert (and (= (+ (* 2 n) 1) 0) (not (= n 0)))))))
+    (check-verify sat? (verify (begin (assume #t)
+                                      (assert (and (= (+ (* 2 n) 1) 0) (not (= n 0)))))))
     ))
     
 (time (run-tests verify-tests))