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
(datatype Expr
(Add Expr Expr)
(Neg Expr)
(Num i64)
(Mul Expr Expr)
(Var String)
)
(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)))
(rule ((= (Add x y) z))
((union (Add z (Neg y)) x)))
(rewrite (Neg (Neg x)) x)
(rewrite (Neg (Num n)) (Num (- 0 n)))
(rule ((= x (Var v))) ((union (Mul (Num 1) x) x)))
(rule ((= x (Add x1 x2))) ((union (Mul (Num 1) x) x)))
(rewrite (Add (Mul y x) (Mul z x)) (Mul (Add y z) x))
(rewrite (Mul x y) (Mul y x))
(rule ((= (Mul (Num x) y) (Num z))
(= (% z x) 0))
((union y (Num (/ z x)))))
; system 1: x + 2 = 7
(union (Add (Var "x") (Num 2)) (Num 7))
; system 2: z + y = 6, 2z = y
(union (Add (Var "z") (Var "y")) (Num 6))
(union (Add (Var "z") (Var "z")) (Var "y"))
(run 5)
(extract (Var "x"))
(extract (Var "y"))
(extract (Var "z"))
(check (= (Var "z") (Add (Num 6) (Neg (Var "y")))))
(check (= (Var "y") (Add (Add (Num 6) (Neg (Var "y"))) (Add (Num 6) (Neg (Var "y"))))))
(check (= (Var "y") (Add (Add (Num 12) (Neg (Var "y"))) (Neg (Var "y")))))
(check (= (Add (Var "y") (Var "y"))
(Add (Num 12) (Neg (Var "y")))))
(check (= (Add (Add (Var "y") (Var "y")) (Var "y"))
(Num 12)))
(check (= (Add (Mul (Num 2) (Var "y")) (Var "y"))
(Num 12)))
(check (= (Mul (Num 3) (Var "y"))
(Num 12)))