abstract-interp-tagged.scm

(load "mk.scm")
(load "z3-driver.scm")
(load "sign-domain.scm")
(load "test-check.scm")

;;; abstract interpreter, inspired by the interpreter in:
;;;
;;; http://matt.might.net/articles/intro-static-analysis/

;; Tag values produced by the abstract interp, to allow the interp to
;; produce closures, booleans, etc, in addition to bit vectors
;; representing abstract integers.

(define lookupo
  (lambda (x env val)
    (conde
      ((fresh (rest)
         (== `((,x . ,val) . ,rest) env)))
      ((fresh (y v rest)
         (== `((,y . ,v) . ,rest) env)
         (symbolo y)
         (=/= y x)
         (lookupo x rest val))))))

(define evalo
  (lambda (expr env val)
    (conde

      [(== expr #f) (== val #f)]
      [(== expr #t) (== val #t)]
      
      [(numbero expr)
       (fresh (v)
         (s/declareo v)
         (== `(num ,v) val)
         (s/z3-alphao expr v))]
      
      [(symbolo expr) (lookupo expr env val)]      

      [(fresh (x e)
         (== `(lambda (,x) ,e) expr)
         (symbolo x)
         (== `(closure ,x ,e ,env) val))]
      
      [(fresh (e v)
         (== `(zero? ,e) expr)
         (s/declareo v)
         (evalo e env `(num ,v))
         (conde
           [(== #t val)
            (s/chas-zeroo v)]
           [(== #f val)
            (conde
              [(s/chas-poso v)]
              [(s/chasnt-poso v) (s/chas-nego v)])]))]
      
      [(fresh (e1 e2 v1 v2 v)
         (== `(+ ,e1 ,e2) expr)
         (s/declareo v1)
         (s/declareo v2)
         (s/declareo v)
         ;; is this the ideal ordering?
         (== `(num ,v) val)
         (s/z3-plus-tableo v1 v2 v)
         (evalo e1 env `(num ,v1))
         (evalo e2 env `(num ,v2)))]

      [(fresh (e1 e2 v1 v2 v)
         (== `(* ,e1 ,e2) expr)
         (s/declareo v1)
         (s/declareo v2)
         (s/declareo v)
         ;; is this the ideal ordering?
         (== `(num ,v) val)
         (s/z3-times-tableo v1 v2 v)
         (evalo e1 env `(num ,v1))
         (evalo e2 env `(num ,v2)))]

      [(fresh (e1 e2 v1 v2)
         (== `(cons ,e1 ,e2) expr)
         (== `(,v1 . ,v2) val)
         (evalo e1 env v1)
         (evalo e2 env v2))]

      [(fresh (e1 e2 e3 v1)
         (== `(if ,e1 ,e2 ,e3) expr)
         (conde
           [(== #f v1)]
           [(== #t v1)])
         (evalo e1 env v1)
         (conde
           [(== #f v1)
            (evalo e3 env val)]
           [(== #t v1)
            (evalo e2 env val)]))]
      
      [(fresh (x e body v env^)
         (== `(let ((,x ,e)) ,body) expr)
         (symbolo x)
         (== `((,x . ,v) . ,env) env^)
         (evalo e env v)
         (evalo body env^ val))]

      [(fresh (e1 e2 x body env^ arg)
         (== `(,e1 ,e2) expr)
         (evalo e1 env `(closure ,x ,body ,env^))
         (symbolo x)
         (evalo e2 env arg)
         (evalo body `((,x . ,arg) . ,env^) val))]
      
      )))


(test "declaro-1"
  (run* (q)
    (s/declareo q))
  '(_.0))

(test "declaro-2"
  (run* (q)
    (s/declareo q)
    (s/declareo q))
  '(_.0))

(test "declaro-3"
  (run* (q)
    (s/declareo q)
    (s/chas-poso q))
  '(bitvec-100
    bitvec-111
    bitvec-110
    bitvec-101))

;;; Non-declarative behavior
;;; compare with declareo-3 -- just swapped order of goals
(todo "declareo-4"
  (run* (q)
    (s/chas-poso q)
    (s/declareo q))
  '?)
;Exception in call-z3: error in z3 out.smt > out.txt
;Type (debug) to enter the debugger.


(test "declareo-5"
  (run* (q)
    (fresh (x y)
      (== (list x y) q)
      (s/declareo x)
      (s/declareo y)
      (== x y)
      (s/chas-poso x)))
  '((bitvec-100 bitvec-100)
    (bitvec-111 bitvec-111)
    (bitvec-110 bitvec-110)
    (bitvec-101 bitvec-101)))

(test "declareo-7"
  (run* (q)
    (fresh (x y)
      (== (list x y) q)
      (s/declareo x)
      (s/declareo y)
      (s/chas-poso x)))
  '((bitvec-100 _.0)
    (bitvec-111 _.0)
    (bitvec-110 _.0)
    (bitvec-101 _.0)))

(test "declareo-8"
  (run* (q)
    (fresh (x y)
      (== (list x y) q)
      (s/declareo x)
      (s/declareo y)))
  '((_.0 _.1)))

(test "declareo-9"
  (run* (q)
    (fresh (x y)
      (== (list x y) q)
      (s/declareo x)
      (s/declareo y)
      (s/chas-poso y)))
  '((_.0 bitvec-100)
    (_.0 bitvec-111)
    (_.0 bitvec-110)
    (_.0 bitvec-101)))

(test "declareo-10"
  (run* (q)
    (fresh (x y)
      (== (list x y) q)
      (== x y)
      (s/declareo x)
      (s/declareo y)))
  '((_.0 _.0)))

(test "declareo-11"
  (run* (q)
    (fresh (x y)
      (== (list x y) q)
      (== x y)
      (s/declareo x)
      (s/declareo y)
      (s/chas-poso x)
      (s/chas-poso y)))
  '((bitvec-100 bitvec-100)
    (bitvec-111 bitvec-111)
    (bitvec-110 bitvec-110)
    (bitvec-101 bitvec-101)))

(test "declareo-12"
  (run* (q)
    (fresh (x y)
      (== (list x y) q)
      (== x y)
      (s/declareo x)
      (s/declareo y)
      (s/chas-poso x)))
  '((bitvec-100 bitvec-100)
    (bitvec-111 bitvec-111)
    (bitvec-110 bitvec-110)
    (bitvec-101 bitvec-101)))

(test "declareo-13"
  (run* (q)
    (fresh (x y)
      (== (list x y) q)
      (s/declareo x)
      (s/declareo y)
      (s/chas-poso x)))
  '((bitvec-100 _.0)
    (bitvec-111 _.0)
    (bitvec-110 _.0)
    (bitvec-101 _.0)))

(test "declareo-14"
  (run* (q)
    (fresh (x y)
      (== (list x y) q)
      (s/declareo x)
      (s/declareo y)
      (s/chas-poso x)
      (s/chas-poso y)))
  '((bitvec-100 bitvec-100)
    (bitvec-111 bitvec-111)
    (bitvec-111 bitvec-110)
    (bitvec-111 bitvec-100)
    (bitvec-111 bitvec-101)
    (bitvec-110 bitvec-110)
    (bitvec-110 bitvec-111)
    (bitvec-110 bitvec-100)
    (bitvec-110 bitvec-101)
    (bitvec-101 bitvec-111)
    (bitvec-101 bitvec-101)
    (bitvec-100 bitvec-101)
    (bitvec-100 bitvec-111)
    (bitvec-101 bitvec-110)
    (bitvec-100 bitvec-110)
    (bitvec-101 bitvec-100)))


(test "lookupo-1"
  (run 3 (q)
    (fresh (x env val v)
      (s/declareo v)
      (s/chas-poso v)
      (symbolo x)
      (== `(num ,v) val)
      (== (list x env val) q)
      (lookupo x env val)))
  '(((_.0 ((_.0 . (num bitvec-100)) . _.1) (num bitvec-100)) (sym _.0))
    ((_.0 ((_.0 . (num bitvec-111)) . _.1) (num bitvec-111)) (sym _.0))
    ((_.0 ((_.0 . (num bitvec-110)) . _.1) (num bitvec-110)) (sym _.0))))

(test "lookupo-2"
  (run* (q)
    (fresh (x env val v1 v2)
      (s/declareo v1)
      (s/chas-poso v1)
      (s/declareo v2)
      (s/chas-nego v2)
      (== `((x . (num ,v1)) (y . (num ,v2))) env)
      (== (list env val) q)
      (lookupo 'x env val)))
  '((((x . (num bitvec-100)) (y . (num bitvec-001))) (num bitvec-100))
    (((x . (num bitvec-111)) (y . (num bitvec-111))) (num bitvec-111))
    (((x . (num bitvec-111)) (y . (num bitvec-101))) (num bitvec-111))
    (((x . (num bitvec-111)) (y . (num bitvec-001))) (num bitvec-111))
    (((x . (num bitvec-111)) (y . (num bitvec-011))) (num bitvec-111))
    (((x . (num bitvec-110)) (y . (num bitvec-101))) (num bitvec-110))
    (((x . (num bitvec-110)) (y . (num bitvec-111))) (num bitvec-110))
    (((x . (num bitvec-110)) (y . (num bitvec-001))) (num bitvec-110))
    (((x . (num bitvec-110)) (y . (num bitvec-011))) (num bitvec-110))
    (((x . (num bitvec-101)) (y . (num bitvec-111))) (num bitvec-101))
    (((x . (num bitvec-101)) (y . (num bitvec-011))) (num bitvec-101))
    (((x . (num bitvec-100)) (y . (num bitvec-011))) (num bitvec-100))
    (((x . (num bitvec-100)) (y . (num bitvec-111))) (num bitvec-100))
    (((x . (num bitvec-101)) (y . (num bitvec-101))) (num bitvec-101))
    (((x . (num bitvec-100)) (y . (num bitvec-101))) (num bitvec-100))
    (((x . (num bitvec-101)) (y . (num bitvec-001))) (num bitvec-101))))

(test "lookupo-3"
  (run* (q)
    (fresh (x env val v1 v2)
      (s/declareo v1)
      (s/declareo v2)
      (s/chas-poso v1)
      (s/chas-nego v2)      
      (== `((x . (num ,v1)) (y . (num ,v2))) env)
      (== (list env val) q)
      (lookupo 'y env val)))
  '((((x . (num bitvec-100)) (y . (num bitvec-001))) (num bitvec-001))
    (((x . (num bitvec-111)) (y . (num bitvec-111))) (num bitvec-111))
    (((x . (num bitvec-111)) (y . (num bitvec-101))) (num bitvec-101))
    (((x . (num bitvec-111)) (y . (num bitvec-001))) (num bitvec-001))
    (((x . (num bitvec-111)) (y . (num bitvec-011))) (num bitvec-011))
    (((x . (num bitvec-110)) (y . (num bitvec-101))) (num bitvec-101))
    (((x . (num bitvec-110)) (y . (num bitvec-111))) (num bitvec-111))
    (((x . (num bitvec-110)) (y . (num bitvec-001))) (num bitvec-001))
    (((x . (num bitvec-110)) (y . (num bitvec-011))) (num bitvec-011))
    (((x . (num bitvec-101)) (y . (num bitvec-111))) (num bitvec-111))
    (((x . (num bitvec-101)) (y . (num bitvec-011))) (num bitvec-011))
    (((x . (num bitvec-100)) (y . (num bitvec-011))) (num bitvec-011))
    (((x . (num bitvec-100)) (y . (num bitvec-111))) (num bitvec-111))
    (((x . (num bitvec-101)) (y . (num bitvec-101))) (num bitvec-101))
    (((x . (num bitvec-100)) (y . (num bitvec-101))) (num bitvec-101))
    (((x . (num bitvec-101)) (y . (num bitvec-001))) (num bitvec-001))))

(test "evalo-0a"
  (run* (q)
    (fresh (expr val)
      (== '3 expr)
      (== (list expr val) q)
      (evalo expr '() val)))
  '((3 (num bitvec-100))))

(test "evalo-0b"
  (run 10 (q)
    (fresh (expr val)
      (numbero expr)
      (== (list expr val) q)
      (evalo expr '() val)))
  '((0 (num bitvec-010))
    (-1 (num bitvec-001))
    (1 (num bitvec-100))
    (2 (num bitvec-100))
    (-2 (num bitvec-001))
    (3 (num bitvec-100))
    (4 (num bitvec-100))
    (5 (num bitvec-100))
    (-3 (num bitvec-001))
    (6 (num bitvec-100))))

(test "evalo-1"
  (run 10 (q)
    (fresh (expr val)
      (== (list expr val) q)
      (evalo expr '() val)))
  '((#f #f)
    (#t #t)
    (0 (num bitvec-010))
    (-1 (num bitvec-001))
    (1 (num bitvec-100))
    (2 (num bitvec-100))
    (-2 (num bitvec-001))
    (((lambda (_.0) _.1) (closure _.0 _.1 ())) (sym _.0))
    (3 (num bitvec-100))
    (4 (num bitvec-100))))

(test "evalo-2a"
  (run* (q)
    (fresh (expr val)
      (== `(+ 3 4) expr)
      (== (list expr val) q)
      (evalo expr '() val)))
  '(((+ 3 4) (num bitvec-100))))

(test "evalo-2b"
  (run 20 (q)
    (fresh (expr val e1 e2)
      (== `(+ ,e1 ,e2) expr)
      (== (list expr val) q)
      (evalo expr '() val)))
  '(((+ 0 -1) (num bitvec-001))
    ((+ 1 -1) (num bitvec-111))
    ((+ 1 -2) (num bitvec-111))
    ((+ 1 -3) (num bitvec-111))
    ((+ 0 1) (num bitvec-100))
    ((+ 2 -4) (num bitvec-111))
    ((+ 1 1) (num bitvec-100))
    ((+ 1 2) (num bitvec-100))
    ((+ 1 -4) (num bitvec-111))
    ((+ 1 -5) (num bitvec-111))
    ((+ 1 -6) (num bitvec-111))
    ((+ -1 -6) (num bitvec-001))
    ((+ 2 -7) (num bitvec-111))
    ((+ -2 3) (num bitvec-111))
    ((+ -3 -6) (num bitvec-001))
    ((+ -2 -7) (num bitvec-001))
    ((+ -2 -8) (num bitvec-001))
    ((+ 3 -8) (num bitvec-111))
    ((+ -4 -6) (num bitvec-001))
    ((+ -5 4) (num bitvec-111))))

(test "evalo-2"
  (run 50 (q)
    (fresh (expr val op e1 e2)
      (== `(,op ,e1 ,e2) expr)
      (== (list expr val) q)
      (evalo expr '() val)))
  '((((lambda (_.0) _.1) (closure _.0 _.1 ())) (sym _.0))
    ((+ 0 -1) (num bitvec-001))
    ((+ 1 -1) (num bitvec-111))
    ((+ 1 -2) (num bitvec-111))
    ((+ 1 -3) (num bitvec-111))
    ((+ 0 1) (num bitvec-100))
    ((+ 2 -4) (num bitvec-111))
    ((+ 1 1) (num bitvec-100))
    ((+ 1 2) (num bitvec-100))
    ((+ 1 -4) (num bitvec-111))
    ((+ 1 -5) (num bitvec-111))
    ((+ 1 -6) (num bitvec-111))
    ((+ -1 -6) (num bitvec-001))
    ((+ 2 -7) (num bitvec-111))
    ((+ -2 3) (num bitvec-111))
    ((+ -3 -6) (num bitvec-001))
    ((cons #f #f) (#f . #f))
    ((+ -2 -7) (num bitvec-001))
    ((+ -2 -8) (num bitvec-001))
    ((+ 3 -8) (num bitvec-111))
    ((+ -4 -6) (num bitvec-001))
    ((+ -5 4) (num bitvec-111))
    ((+ -6 -7) (num bitvec-001))
    ((* 0 0) (num bitvec-010))
    ((+ 0 0) (num bitvec-010))
    ((+ -7 -9) (num bitvec-001))
    ((* -1 -1) (num bitvec-100))
    ((+ 4 -9) (num bitvec-111))
    ((+ -8 5) (num bitvec-111))
    ((* 1 1) (num bitvec-100))
    ((+ -8 -8) (num bitvec-001))
    ((+ -3 -9) (num bitvec-001))
    ((* 2 -2) (num bitvec-001))
    ((+ -9 -9) (num bitvec-001))
    ((+ 5 -10) (num bitvec-111))
    ((* -2 -2) (num bitvec-100))
    ((+ 6 -11) (num bitvec-111))
    ((+ 1 -12) (num bitvec-111))
    ((* 0 2) (num bitvec-010))
    ((+ 1 -13) (num bitvec-111))
    ((+ 6 0) (num bitvec-100))
    ((* -3 -3) (num bitvec-100))
    ((+ 7 0) (num bitvec-100))
    ((+ -10 -10) (num bitvec-001))
    ((* -4 -4) (num bitvec-100))
    ((+ 1 -14) (num bitvec-111))
    ((+ 1 -15) (num bitvec-111))
    ((* 0 -5) (num bitvec-010))
    ((+ -11 -14) (num bitvec-001))
    ((+ -12 6) (num bitvec-111))))

(test "evalo-3"
  (run 10 (q)
    (fresh (expr env val e)
      (== `(let . ,e) expr)
      (== (list expr env val) q)
      (evalo expr env val)))
  '((((let ([_.0 #f]) #f) _.1 #f) (sym _.0))
    (((let ([_.0 #f]) #t) _.1 #t) (sym _.0))
    (((let ([_.0 #t]) #f) _.1 #f) (sym _.0))
    (((let ([_.0 #t]) #t) _.1 #t) (sym _.0))
    (((let ([_.0 #f]) 0) _.1 (num bitvec-010)) (sym _.0))
    (((let #f) ((let closure _.0 #f _.1) . _.2) #f) (sym _.0))
    (((let ([_.0 #f]) -1) _.1 (num bitvec-001)) (sym _.0))
    (((let ([_.0 #f]) 1) _.1 (num bitvec-100)) (sym _.0))
    (((let ([_.0 #f]) 2) _.1 (num bitvec-100)) (sym _.0))
    (((let ([_.0 #f]) -2) _.1 (num bitvec-001)) (sym _.0))))

(test "evalo-4"
  (run 15 (q)
    (fresh (expr env val id e)      
      (== `(let ([,id ,e]) x) expr)
      (== (list expr env val) q)
      (evalo expr env val)))
  '(((let ([x #f]) x)
     _.0
     #f)
    ((let ([x #t]) x)
     _.0
     #t)
    (((let ([_.0 #f]) x)
      ((x . _.1) . _.2)
      _.1)
     (=/= ((_.0 x)))
     (sym _.0))
    (((let ([_.0 #f]) x)
      ((_.1 . _.2) (x . _.3) . _.4)
      _.3)
     (=/= ((_.0 x)) ((_.1 x)))
     (sym _.0 _.1))
    (((let ([_.0 #f]) x)
      ((_.1 . _.2) (_.3 . _.4) (x . _.5) . _.6)
      _.5)
     (=/= ((_.0 x)) ((_.1 x)) ((_.3 x)))
     (sym _.0 _.1 _.3))
    (((let ([_.0 #f]) x)
      ((_.1 . _.2) (_.3 . _.4) (_.5 . _.6) (x . _.7) . _.8)
      _.7)
     (=/= ((_.0 x)) ((_.1 x)) ((_.3 x)) ((_.5 x)))
     (sym _.0 _.1 _.3 _.5))
    (((let ([_.0 #t]) x)
      ((x . _.1) . _.2)
      _.1)
     (=/= ((_.0 x)))
     (sym _.0))
    (((let ([_.0 #f]) x)
      ((_.1 . _.2) (_.3 . _.4) (_.5 . _.6) (_.7 . _.8) (x . _.9) . _.10)
      _.9)
     (=/= ((_.0 x)) ((_.1 x)) ((_.3 x)) ((_.5 x)) ((_.7 x)))
     (sym _.0 _.1 _.3 _.5 _.7))
    ((let ([x 0]) x)
     _.0
     (num bitvec-010))
    ((let ([x -1]) x)
     _.0
     (num bitvec-001))
    ((let ([x 1]) x)
     _.0
     (num bitvec-100))
    ((let ([x 2]) x)
     _.0
     (num bitvec-100))
    ((let ([x -2]) x)
     _.0
     (num bitvec-001))
    (((let ([_.0 #f]) x)
      ((_.1 . _.2) (_.3 . _.4) (_.5 . _.6) (_.7 . _.8) (_.9 . _.10) (x . _.11) . _.12)
      _.11)
     (=/= ((_.0 x)) ((_.1 x)) ((_.3 x)) ((_.5 x)) ((_.7 x)) ((_.9 x)))
     (sym _.0 _.1 _.3 _.5 _.7 _.9))
    ((let ([x 3]) x)
     _.0
     (num bitvec-100))))

(test "evalo-5"
  (run 10 (q)
    (fresh (expr e val)
      (== `(zero? ,e) expr)
      (== (list expr val) q)
      (evalo expr '() val)))
  '(((zero? 0) #t)
    ((zero? 1) #f)
    ((zero? 2) #f)
    ((zero? 3) #f)
    ((zero? 4) #f)
    ((zero? -1) #f)
    ((zero? 5) #f)
    ((zero? 6) #f)
    ((zero? -2) #f)
    ((zero? 7) #f)))

(test "evalo-6"
  (run* (q)
    (fresh (expr val)
      (== `(zero? (+ -1 1)) expr)
      (== (list expr val) q)
      (evalo expr '() val)))
  '(((zero? (+ -1 1)) #t)
    ((zero? (+ -1 1)) #f)))

(test "evalo-7"
  (run* (q)
    (fresh (expr val)
      (== `(zero? (+ 0 1)) expr)
      (== (list expr val) q)
      (evalo expr '() val)))
  '(((zero? (+ 0 1)) #f)))

(test "evalo-8"
  (run* (q)
    (fresh (expr val)
      (== `(zero? (+ 0 -1)) expr)
      (== (list expr val) q)
      (evalo expr '() val)))
  '(((zero? (+ 0 -1)) #f)))

(test "evalo-9"
  (run 10 (q)
    (fresh (expr e val)
      (== `(zero? (* 0 ,e)) expr)
      (== (list expr val) q)
      (evalo expr '() val)))
  '(((zero? (* 0 0)) #t)
    ((zero? (* 0 1)) #t)
    ((zero? (* 0 -1)) #t)
    ((zero? (* 0 2)) #t)
    ((zero? (* 0 -2)) #t)
    ((zero? (* 0 -3)) #t)
    ((zero? (* 0 -4)) #t)
    ((zero? (* 0 -5)) #t)
    ((zero? (* 0 -6)) #t)
    ((zero? (* 0 -7)) #t)))

(test "evalo-10"
  (run 5 (q)
    (fresh (expr e val)
      (== `(zero? (+ ,e 1)) expr)
      (numbero e)
      (== (list expr val) q)
      (== val #t)
      (evalo expr '() val)))
  '(((zero? (+ -1 1)) #t)
    ((zero? (+ -2 1)) #t)
    ((zero? (+ -3 1)) #t)
    ((zero? (+ -4 1)) #t)
    ((zero? (+ -5 1)) #t)))

(test "evalo-11"
  (run 5 (q)
    (fresh (expr e1 e2 val)
      (== `(zero? (+ ,e1 ,e2)) expr)
      (numbero e1)
      (numbero e2)
      (== (list expr val) q)
      (== val #t)
      (evalo expr '() val)))
  '(((zero? (+ 0 0)) #t)
    ((zero? (+ 1 -1)) #t)
    ((zero? (+ 2 -1)) #t)
    ((zero? (+ 3 -1)) #t)
    ((zero? (+ 4 -1)) #t)))

(test "evalo-12"
  (run 50 (q)
    (fresh (expr e1 e2 val)
      (== `(zero? (+ ,e1 ,e2)) expr)
      (numbero e1)
      (numbero e2)
      (== (list expr val) q)
      (== val #f)
      (evalo expr '() val)))
  '(((zero? (+ 1 0)) #f)
    ((zero? (+ 1 -1)) #f)
    ((zero? (+ -1 0)) #f)
    ((zero? (+ 0 1)) #f)
    ((zero? (+ 2 0)) #f)
    ((zero? (+ 0 -1)) #f)
    ((zero? (+ 2 -1)) #f)
    ((zero? (+ 3 0)) #f)
    ((zero? (+ -2 0)) #f)
    ((zero? (+ 3 -1)) #f)
    ((zero? (+ 3 -2)) #f)
    ((zero? (+ 0 -2)) #f)
    ((zero? (+ -1 1)) #f)
    ((zero? (+ -2 1)) #f)
    ((zero? (+ -2 -2)) #f)
    ((zero? (+ 4 -2)) #f)
    ((zero? (+ 3 -3)) #f)
    ((zero? (+ -3 -3)) #f)
    ((zero? (+ 4 0)) #f)
    ((zero? (+ 5 0)) #f)
    ((zero? (+ -4 -4)) #f)
    ((zero? (+ -3 2)) #f)
    ((zero? (+ 6 0)) #f)
    ((zero? (+ -5 -5)) #f)
    ((zero? (+ 5 -1)) #f)
    ((zero? (+ 6 -3)) #f)
    ((zero? (+ -6 -6)) #f)
    ((zero? (+ 1 -4)) #f)
    ((zero? (+ 0 -7)) #f)
    ((zero? (+ -2 3)) #f)
    ((zero? (+ -4 0)) #f)
    ((zero? (+ 7 0)) #f)
    ((zero? (+ -3 0)) #f)
    ((zero? (+ -3 3)) #f)
    ((zero? (+ -5 0)) #f)
    ((zero? (+ -2 4)) #f)
    ((zero? (+ -6 0)) #f)
    ((zero? (+ 0 3)) #f)
    ((zero? (+ -7 0)) #f)
    ((zero? (+ 0 4)) #f)
    ((zero? (+ -7 -7)) #f)
    ((zero? (+ 0 5)) #f)
    ((zero? (+ -8 -8)) #f)
    ((zero? (+ 1 6)) #f)
    ((zero? (+ -1 -9)) #f)
    ((zero? (+ 1 -5)) #f)
    ((zero? (+ -9 -9)) #f)
    ((zero? (+ 0 6)) #f)
    ((zero? (+ -10 0)) #f)
    ((zero? (+ 0 7)) #f)))

(test "evalo-13"
  (run 30 (q)
    (fresh (expr e1 e2 val)
      (== `(cons ,e1 ,e2) expr)
      (== (list expr val) q)
      (evalo expr '() val)))
  '(((cons #f #f) (#f . #f))
    ((cons #f #t) (#f . #t))
    ((cons #t #f) (#t . #f))
    ((cons #t #t) (#t . #t))
    ((cons #f 0) (#f num bitvec-010))
    ((cons #f -1) (#f num bitvec-001))
    ((cons #f 1) (#f num bitvec-100))
    ((cons #f 2) (#f num bitvec-100))
    ((cons #f -2) (#f num bitvec-001))
    ((cons #f 3) (#f num bitvec-100))
    ((cons #f 4) (#f num bitvec-100))
    ((cons #f 5) (#f num bitvec-100))
    ((cons #f -3) (#f num bitvec-001))
    ((cons 0 #f) ((num bitvec-010) . #f))
    ((cons #f 6) (#f num bitvec-100))
    (((cons #f (lambda (_.0) _.1)) (#f closure _.0 _.1 ()))
     (sym _.0))
    ((cons #f 7) (#f num bitvec-100))
    ((cons -1 #f) ((num bitvec-001) . #f))
    ((cons #f 8) (#f num bitvec-100))
    ((cons #t 0) (#t num bitvec-010))
    ((cons #f 9) (#f num bitvec-100))
    ((cons 1 #f) ((num bitvec-100) . #f))
    ((cons #f -4) (#f num bitvec-001))
    ((cons #f 10) (#f num bitvec-100))
    ((cons 2 #f) ((num bitvec-100) . #f))
    ((cons #f 11) (#f num bitvec-100))
    ((cons #t -1) (#t num bitvec-001))
    ((cons #f 12) (#f num bitvec-100))
    ((cons -2 #f) ((num bitvec-001) . #f))
    ((cons #f 13) (#f num bitvec-100))))

;;; first interesting test!
(test "evalo-14"
  (run 10 (q)
    (fresh (expr e val)
      (== `(cons (zero? ,e) (zero? ,e)) expr)
      (== (list expr val) q)
      (== `(#t . #f) val)
      (evalo expr '() val)))
  '(((cons (zero? (+ 1 -1)) (zero? (+ 1 -1))) (#t . #f))
    ((cons (zero? (+ 2 -1)) (zero? (+ 2 -1))) (#t . #f))
    ((cons (zero? (+ 3 -1)) (zero? (+ 3 -1))) (#t . #f))
    ((cons (zero? (+ -1 1)) (zero? (+ -1 1))) (#t . #f))
    ((cons (zero? (+ 1 -2)) (zero? (+ 1 -2))) (#t . #f))
    ((cons (zero? (+ 1 -3)) (zero? (+ 1 -3))) (#t . #f))
    ((cons (zero? (+ -2 2)) (zero? (+ -2 2))) (#t . #f))
    ((cons (zero? (+ 4 -1)) (zero? (+ 4 -1))) (#t . #f))
    ((cons (zero? (+ 2 -2)) (zero? (+ 2 -2))) (#t . #f))
    ((cons (zero? (+ 5 -2)) (zero? (+ 5 -2))) (#t . #f))))

(test "evalo-15"
  (run 30 (q)
    (fresh (expr e1 e2 e3 val)
      (== `(if ,e1 ,e2 ,e3) expr)
      (== (list expr val) q)
      (evalo expr '() val)))
  '(((if #f _.0 #f) #f)
    ((if #f _.0 #t) #t)
    ((if #t #f _.0) #f)
    ((if #f _.0 0) (num bitvec-010))
    ((if #t #t _.0) #t)
    ((if #f _.0 -1) (num bitvec-001))
    ((if #f _.0 1) (num bitvec-100))
    ((if #f _.0 2) (num bitvec-100))
    ((if #f _.0 -2) (num bitvec-001))
    ((if #f _.0 3) (num bitvec-100))
    ((if #f _.0 4) (num bitvec-100))
    ((if #f _.0 5) (num bitvec-100))
    ((if #f _.0 -3) (num bitvec-001))
    ((if #f _.0 6) (num bitvec-100))
    (((if #f _.0 (lambda (_.1) _.2)) (closure _.1 _.2 ()))
     (sym _.1))
    ((if #f _.0 7) (num bitvec-100))
    ((if #f _.0 8) (num bitvec-100))
    ((if #f _.0 9) (num bitvec-100))
    ((if #t 0 _.0) (num bitvec-010))
    ((if #f _.0 -4) (num bitvec-001))
    ((if #f _.0 10) (num bitvec-100))
    ((if #t -1 _.0) (num bitvec-001))
    ((if #f _.0 11) (num bitvec-100))
    ((if #f _.0 12) (num bitvec-100))
    ((if #t 1 _.0) (num bitvec-100))
    ((if #f _.0 13) (num bitvec-100))
    ((if #f _.0 14) (num bitvec-100))
    ((if #t 2 _.0) (num bitvec-100))
    ((if #f _.0 15) (num bitvec-100))
    ((if #f _.0 -5) (num bitvec-001))))

(test "evalo-16"
  (run 10 (q)
    (fresh (expr e1 val)
      (== `(if ,e1 #t #f) expr)
      (== #t val)
      (== (list expr val) q)
      (evalo expr '() val)))
  '(((if #t #t #f) #t)
    ((if (zero? 0) #t #f) #t)
    ((if (if #f _.0 #t) #t #f) #t)
    (((if (let ((_.0 #f)) #t) #t #f) #t) (sym _.0))
    ((if (if #t #t _.0) #t #f) #t)
    (((if (let ((_.0 #t)) #t) #t #f) #t) (sym _.0))
    ((if (zero? (+ 0 0)) #t #f) #t)
    ((if (zero? (+ 1 -1)) #t #f) #t)
    ((if (zero? (+ 2 -1)) #t #f) #t)
    ((if (zero? (+ 3 -1)) #t #f) #t)))

(test "evalo-17"
  (run* (q)
    (fresh (expr e1 val)
      (== `(lambda (y) (* y y)) expr)
      (== (list expr val) q)
      (evalo expr '() val)))
  '(((lambda (y) (* y y)) (closure y (* y y) ()))))

(test "evalo-18"
  (run* (q)
    (fresh (expr e1 val)
      (== `((lambda (y) (* y y)) 3) expr)
      (== (list expr val) q)
      (evalo expr '() val)))
  '((((lambda (y) (* y y)) 3) (num bitvec-100))))

(test "evalo-19"
  (run* (q)
    (fresh (expr e1 val)
      (== `((lambda (y) (* y y)) 3) expr)
      (== (list expr val) q)
      (evalo expr '() val)))
  '((((lambda (y) (* y y)) 3) (num bitvec-100))))