Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fixes and adds extra tests to BDD & Arrays #187

Merged
merged 3 commits into from
Aug 14, 2023
Merged

Fixes and adds extra tests to BDD & Arrays #187

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
77ab12d
Fixes and adds extra tests to BDD
TrevorHansen Aug 12, 2023
f97c4ad
Refactor. Clean up the diff so it's easier to see the changes vs main.
TrevorHansen Aug 14, 2023
f4bed9a
Include missing addition rewrite rule
TrevorHansen Aug 13, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 6 additions & 4 deletions tests/array.egg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"))
Expand All @@ -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)
89 changes: 49 additions & 40 deletions tests/bdd.egg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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))
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Note that this uses "b1" & "b2" which have been defined above in the test code. So these aren't free variables.

(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)