This repository has been archived by the owner on Sep 24, 2024. It is now read-only.
forked from uwplse/tensat
-
Notifications
You must be signed in to change notification settings - Fork 1
/
axioms_converted.txt
51 lines (51 loc) · 3.74 KB
/
axioms_converted.txt
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
(ewadd ?x (ewadd ?y ?z))=>(ewadd (ewadd ?x ?y) ?z)
(ewadd ?x ?y)=>(ewadd ?y ?x)
(ewmul ?x (ewmul ?y ?z))=>(ewmul (ewmul ?x ?y) ?z)
(ewmul ?x ?y)=>(ewmul ?y ?x)
(ewmul (ewadd ?x ?y) ?z)=>(ewadd (ewmul ?x ?z) (ewmul ?y ?z))
(smul (smul ?x ?y) ?w)=>(smul ?x (smul ?y ?w))
(smul (ewadd ?x ?y) ?w)=>(ewadd (smul ?x ?w) (smul ?y ?w))
(smul (ewmul ?x ?y) ?w)=>(ewmul ?x (smul ?y ?w))
(matmul 0 ?x (matmul 0 ?y ?z))=>(matmul 0 (matmul 0 ?x ?y) ?z)
(smul (matmul 0 ?x ?y) ?w)=>(matmul 0 ?x (smul ?y ?w))
(matmul 0 ?x (ewadd ?y ?z))=>(ewadd (matmul 0 ?x ?y) (matmul 0 ?x ?z))
(conv2d ?sx ?sy ?p ?c (smul ?x ?w) ?y)=>(conv2d ?sx ?sy ?p ?c ?x (smul ?y ?w))
(smul (conv2d ?sx ?sy ?p 0 ?x ?y) ?w)=>(conv2d ?sx ?sy ?p 0 (smul ?x ?w) ?y)
(conv2d ?sx ?sy ?p 0 ?x (ewadd ?y ?z))=>(ewadd (conv2d ?sx ?sy ?p 0 ?x ?y) (conv2d ?sx ?sy ?p 0 ?x ?z))
(conv2d ?sx ?sy ?p 0 (ewadd ?x ?y) ?z)=>(ewadd (conv2d ?sx ?sy ?p 0 ?x ?z) (conv2d ?sx ?sy ?p 0 ?y ?z))
(conv2d ?sx ?sy ?p 2 ?x ?y)=>(relu (conv2d ?sx ?sy ?p 0 ?x ?y))
(conv2d 1 1 0 0 ?x (Iconv ?kx ?ky))=>?x
(split_0 (split ?a (concat ?a ?n ?x ?y)))=>?x
(split_1 (split ?a (concat ?a ?n ?x ?y)))=>?y
(concat 0 ?n (concat 1 ?n ?x ?y) (concat 1 ?n ?z ?w))=>(concat 1 ?n (concat 0 ?n ?x ?z) (concat 0 ?n ?y ?w))
(concat ?a ?n (smul ?x ?w) (smul ?y ?w))=>(smul (concat ?a ?n ?x ?y) ?w)
(concat ?a ?n (ewadd ?x ?y) (ewadd ?z ?w))=>(ewadd (concat ?a ?n ?x ?z) (concat ?a ?n ?y ?w))
(concat ?a ?n (ewmul ?x ?y) (ewmul ?z ?w))=>(ewmul (concat ?a ?n ?x ?z) (concat ?a ?n ?y ?w))
(concat ?a ?n (relu ?x) (relu ?y))=>(relu (concat ?a ?n ?x ?y))
(concat 1 ?n (matmul 0 ?x ?y) (matmul 0 ?x ?z))=>(matmul 0 ?x (concat 1 ?n ?y ?z))
(matmul 0 (concat 1 ?n ?x ?z) (concat 0 ?n ?y ?w))=>(ewadd (matmul 0 ?x ?y) (matmul 0 ?z ?w))
(concat 0 ?n (conv2d ?sx ?sy ?p ?c ?x ?z) (conv2d ?sx ?sy ?p ?c ?y ?z))=>(conv2d ?sx ?sy ?p ?c (concat 0 ?n ?x ?y) ?z)
(concat 1 ?n (conv2d ?sx ?sy ?p ?c ?x ?y) (conv2d ?sx ?sy ?p ?c ?x ?z))=>(conv2d ?sx ?sy ?p ?c ?x (concat 0 ?n ?y ?z))
(conv2d ?sx ?sy ?p 0 (concat 1 ?n ?x ?z) (concat 1 ?n ?y ?w))=>(ewadd (conv2d ?sx ?sy ?p 0 ?x ?y) (conv2d ?sx ?sy ?p 0 ?z ?w))
(ewadd (ewadd ?x ?y) ?z)=>(ewadd ?x (ewadd ?y ?z))
(ewadd ?y ?x)=>(ewadd ?x ?y)
(ewmul (ewmul ?x ?y) ?z)=>(ewmul ?x (ewmul ?y ?z))
(ewmul ?y ?x)=>(ewmul ?x ?y)
(ewadd (ewmul ?x ?z) (ewmul ?y ?z))=>(ewmul (ewadd ?x ?y) ?z)
(smul ?x (smul ?y ?w))=>(smul (smul ?x ?y) ?w)
(ewadd (smul ?x ?w)(smul ?y ?w))=>(smul (ewadd ?x ?y) ?w)
(ewmul ?x (smul ?y ?w))=>(smul (ewmul ?x ?y) ?w)
(matmul 0 (matmul 0 ?x ?y) ?z)=>(matmul 0 ?x (matmul 0 ?y ?z))
(matmul 0 ?x (smul ?y ?w))=>(smul (matmul 0 ?x ?y) ?w)
(ewadd (matmul 0 ?x ?y) (matmul 0 ?x ?z))=>(matmul 0 ?x (ewadd ?y ?z))
(conv2d ?sx ?sy ?p ?c ?x (smul ?y ?w))=>(conv2d ?sx ?sy ?p ?c (smul ?x ?w) ?y)
(conv2d ?sx ?sy ?p 0 (smul ?x ?w) ?y)=>(smul (conv2d ?sx ?sy ?p 0 ?x ?y) ?w)
(ewadd (conv2d ?sx ?sy ?p 0 ?x ?y) (conv2d ?sx ?sy ?p 0 ?x ?z))=>(conv2d ?sx ?sy ?p 0 ?x (ewadd ?y ?z))
(ewadd (conv2d ?sx ?sy ?p 0 ?x ?z) (conv2d ?sx ?sy ?p 0 ?y ?z))=>(conv2d ?sx ?sy ?p 0 (ewadd ?x ?y) ?z)
(relu (conv2d ?sx ?sy ?p 0 ?x ?y))=>(conv2d ?sx ?sy ?p 2 ?x ?y)
(concat 1 ?n (concat 0 ?n ?x ?z) (concat 0 ?n ?y ?w))=>(concat 0 ?n (concat 1 ?n ?x ?y) (concat 1 ?n ?z ?w))
(smul (concat ?a ?n ?x ?y) ?w)=>(concat ?a ?n (smul ?x ?w) (smul ?y ?w))
(ewadd (concat ?a ?n ?x ?z) (concat ?a ?n ?y ?w))=>(concat ?a ?n (ewadd ?x ?y) (ewadd ?z ?w))
(ewmul (concat ?a ?n ?x ?z) (concat ?a ?n ?y ?w))=>(concat ?a ?n (ewmul ?x ?y) (ewmul ?z ?w))
(relu (concat ?a ?n ?x ?y))=>(concat ?a ?n (relu ?x) (relu ?y))
(matmul 0 ?x (concat 1 ?n ?y ?z))=>(concat 1 ?n (matmul 0 ?x ?y) (matmul 0 ?x ?z))