Fixes and adds extra tests to BDD & Arrays (#187)

* Fixes and adds extra tests to BDD

This: 
(1) fixes some BDD operatons, 
(2) reduces the number of rewrites required by adding commutative operations, 
(3) adds more tests,
(4) moves the tests into a separate frame so that the changes made during testing are cleaned up when testing finishes.

* Refactor. Clean up the diff so it's easier to see the changes vs main.

* Include missing addition rewrite rule

includes this:
 (rewrite (add x (Num 0)) x)

tests/array.egg

@@ -51,7 +51,9 @@
 (rewrite (add x y) (add y x))
 (rewrite (add (add x y) z) (add x (add y z)))
 (rewrite (add (Num x) (Num y)) (Num (+ x y)))
+(rewrite (add x (Num 0)) x)
 
+(push)
 (let r1 (Var "r1"))
 (let r2 (Var "r2"))
 (let r3 (Var "r3"))
@@ -63,13 +65,13 @@
 (let test1 (select (store mem1 r1 (Num 42)) r1))
 (let test2 (select (store mem1 r1 (Num 42)) (add r1 (Num 17))))
 (let test3 (select (store (store mem1 (add r1 r2) (Num 1)) (add r2 r1) (Num 2)) (add r1 r3)))
+(let test4 (add (Num 1) (add (add (Num 1) (add (Num 1) r1)) (Num -3))))
 
-(run 4)
+(run 5)
 (check (= test1 (Num 42)))
 (check (neq r1 r2))
 (check (neq r1 (add r1 (Num 17))))
 (check (= test2 (select mem1 (add r1 (Num 17)))))
 (check (= test3 (select mem1 (add r1 r3))))
-
-
-
+(check (= test4 r1))
+(pop)

tests/bdd.egg

@@ -16,81 +16,90 @@
 (rewrite (ITE n a a) a)
 
 (function and (BDD BDD) BDD)
+(rewrite (and x y) (and y x))
 (rewrite (and False n) False)
-(rewrite (and n False) False)
 (rewrite (and True x) x)
-(rewrite (and x True) x)
+
 ; We use an order where low variables are higher in tree
 ; Could go the other way.
 (rewrite (and (ITE n a1 a2) (ITE m b1 b2))
     (ITE n (and a1 (ITE m b1 b2)) (and a2 (ITE m b1 b2)))
     :when ((< n m))
 )
-(rewrite (and (ITE n a1 a2) (ITE m b1 b2))
-    (ITE m (and (ITE n a1 a2) b1) (and (ITE n a1 a2) b2))
-    :when ((> n m))
-)
 (rewrite (and (ITE n a1 a2) (ITE n b1 b2))
     (ITE n (and a1 b1) (and a2 b2))
 )
 
-(let b0 (ITE 0 True False))
-(let b1 (ITE 1 True False))
-(let b2 (ITE 2 True False))
-
-(let b123 (and b2 (and b0 b1)))
-(let b11 (and b1 b1))
-(let b12 (and b1 b2))
-(run 5)
-(query-extract b11)
-(query-extract b12)
-(query-extract b123)
-(check (= (and (ITE 1 True False) (ITE 2 True False))
-       (ITE 1 (ITE 2 True False) False))
-)
-;(check (= b123 (ITE 3 ()))
-
 (function or (BDD BDD) BDD)
+(rewrite (or x y) (or y x))
 (rewrite (or True n) True)
-(rewrite (or n True) True)
 (rewrite (or False x) x)
-(rewrite (or x False) x)
 (rewrite (or (ITE n a1 a2) (ITE m b1 b2))
     (ITE n (or a1 (ITE m b1 b2)) (or a2 (ITE m b1 b2)))
     :when ((< n m))
 )
-(rewrite (or (ITE n a1 a2) (ITE m b1 b2))
-    (ITE m (or (ITE n a1 a2) b1) (or (ITE n a1 a2) b2))
-    :when ((> n m))
-)
 (rewrite (or (ITE n a1 a2) (ITE n b1 b2))
     (ITE n (or a1 b1) (or a2 b2))
 )
 
-(let or121 (or b1 (or b2 b1)))
-(run 5)
-(query-extract or121)
-
 (function not (BDD) BDD)
 (rewrite (not True) False)
 (rewrite (not False) True)
-(rewrite (not (ITE n a1 a2)) (not (ITE n (not a1) (not a2))))
+(rewrite (not (ITE n a1 a2)) (ITE n (not a1) (not a2)))
+
 
 (function xor (BDD BDD) BDD)
+(rewrite (xor x y) (xor y x))
 (rewrite (xor True n) (not n))
-(rewrite (xor n True) (not n))
 (rewrite (xor False x) x)
-(rewrite (xor x False) x)
+
 (rewrite (xor (ITE n a1 a2) (ITE m b1 b2))
-    (ITE n (xor a1 (ITE m b1 b2)) (or a2 (ITE m b1 b2)))
+    (ITE n (xor a1 (ITE m b1 b2)) (xor a2 (ITE m b1 b2)))
     :when ((< n m))
 )
-(rewrite (xor (ITE n a1 a2) (ITE m b1 b2))
-    (ITE m (xor (ITE n a1 a2) b1) (or (ITE n a1 a2) b2))
-    :when ((> n m))
-)
 (rewrite (xor (ITE n a1 a2) (ITE n b1 b2))
     (ITE n (xor a1 b1) (xor a2 b2))
 )
 
+(push)
+;;; Tests
+
+(let v0 (ITE 0 True False))
+(let v1 (ITE 1 True False))
+(let v2 (ITE 2 True False))
+
+(let t0 (not (not v0)))
+(let t1 (or v0 (not v0)))
+(let t2 (and v0 (not v0)))
+(let t3 (and v0 v0))
+(let t4 (or v0 v0))
+(let t5 (xor (not v0) v0))
+(let t6 (and (or v1 v2) v2))
+
+(let t7a (xor (not v0) v1))
+(let t7b (xor v0 (not v1)))
+(let t7c (not (xor v0 v1)))
+
+(let t8 (and v1 v2))
+
+(let t9 (and (not v1) (and (not v0) (xor v0 v1))))
+(let t10 (or (not v1) (or (not v0) (xor  v0 (not v1)))))
+
+(run 30)
+
+(check (= t0 v0)) ; not cancels
+(check (= t1 True))
+(check (= t2 False))
+(check (= t3 v0))
+(check (= t4 v0))
+(check (= t5 True))
+(check (= t6 v2))
+
+(check (= t7a t7b))
+(check (= t7a t7c))
+
+(check (= t8 (ITE 1 (ITE 2 True False) False)))
 
+(check (= t9 False))
+(check (= t10 True))
+(pop)