1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
; Smtlib theory of arrays
; https://smtlib.cs.uiowa.edu/theories-ArraysEx.shtml
; http://smtlib.cs.uiowa.edu/version1/theories/Arrays.smt
(datatype Math
(Num i64)
(Var String)
)
(datatype Array
(Const i64)
(AVar String)
)
(constructor add (Math Math) Math)
(constructor select (Array Math) Math)
(constructor store (Array Math Math) Array)
(relation neq (Math Math))
(rule ((neq x y))
((neq y x)))
(rule ((neq x x))
((panic "query (neq x x) found something equal to itself")))
; injectivity rules take not equal to not equal.
(rule ((neq x y) (= (add x z) e))
((neq (add x z) (add y z))))
(rule ((= (add x (Num i)) e) (!= i 0))
((neq e x)))
(rule ((= (Num a) n1) (= (Num b) n2) (!= a b))
((neq n1 n2)))
; select gets from store
(rewrite (select (store mem i e) i) e)
; select passes through wrong index
(rule ((= (select (store mem i1 e) i2) e1) (neq i1 i2))
((union (select mem i2) e1)))
; aliasing writes destroy old value
(rewrite (store (store mem i e1) i e2) (store mem i e2))
; non-aliasing writes commutes
(rule ((= (store (store mem i2 e2) i1 e1) mem1) (neq i1 i2))
((union (store (store mem i1 e1) i2 e2) mem1)))
; typical math rules
(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"))
(let $mem1 (AVar "mem1"))
(neq $r1 $r2)
(neq $r2 $r3)
(neq $r1 $r3)
(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 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)