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

(function add (Math Math) Math)
(function select (Array Math) Math)
(function 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)