This repository was 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
/
Copy pathconverted.txt
41 lines (41 loc) · 3.58 KB
/
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
(AddOp ?x (AddOp ?y ?z))=>(AddOp (AddOp ?x ?y) ?z)
(MulOp (AddOp ?x ?y) ?z)=>(AddOp (MulOp ?x ?z) (MulOp ?y ?z))
(AddOp (MulOp ?x ?z) (MulOp ?y ?z))=>(MulOp (AddOp ?x ?y) ?z)
(MulOp ?x (DivOp ?y ?z))=>(DivOp (MulOp ?x ?y) ?z)
(DivOp (MulOp ?x ?y) ?z)=>(MulOp ?x (DivOp ?y ?z))
(DivOp (AddOp ?x ?y) ?z)=>(AddOp (DivOp ?x ?z) (DivOp ?y ?z))
(AddOp (DivOp ?x ?z) (DivOp ?y ?z))=>(DivOp (AddOp ?x ?y) ?z)
(DivOp (SubtractOp ?x ?y) ?z)=>(SubtractOp (DivOp ?x ?z) (DivOp ?y ?z))
(SubtractOp (DivOp ?x ?z) (DivOp ?y ?z))=>(DivOp (SubtractOp ?x ?y) ?z)
(MinOp ?x ?x)=>?x
(MaxOp ?x ?x)=>?x
(SubtractOp ?x ?y)=>(AddOp ?x (NegOp ?y))
(AddOp ?x (NegOp ?y))=>(SubtractOp ?x ?y)
(NegOp (AddOp ?x ?y))=>(AddOp (NegOp ?x) (NegOp ?y))
(AddOp (NegOp ?x) (NegOp ?y))=>(NegOp (AddOp ?x ?y))
(NegOp (MulOp ?x ?y))=>(MulOp (NegOp ?x) ?y)
(MulOp (NegOp ?x) ?y)=>(NegOp (MulOp ?x ?y))
(NegOp (DivOp ?x ?y))=>(DivOp (NegOp ?x) ?y)
(DivOp (NegOp ?x) ?y)=>(NegOp (DivOp ?x ?y))
(NegOp (DivOp ?x ?y))=>(DivOp ?x (NegOp ?y))
(DivOp ?x (NegOp ?y))=>(NegOp (DivOp ?x ?y))
(ConcatenateOp (Vec (AddOp ?x ?y) (AddOp ?z ?w)) ?i)=>(AddOp (ConcatenateOp (Vec ?x ?z) ?i) (ConcatenateOp (Vec ?y ?w) ?i))
(AddOp (ConcatenateOp (Vec ?x ?z) ?i) (ConcatenateOp (Vec ?y ?w) ?i))=>(ConcatenateOp (Vec (AddOp ?x ?y) (AddOp ?z ?w)) ?i)
(ConcatenateOp (Vec (SubtractOp ?x ?y) (SubtractOp ?z ?w)) ?i)=>(SubtractOp (ConcatenateOp (Vec ?x ?z) ?i) (ConcatenateOp (Vec ?y ?w) ?i))
(SubtractOp (ConcatenateOp (Vec ?x ?z) ?i) (ConcatenateOp (Vec ?y ?w) ?i))=>(ConcatenateOp (Vec (SubtractOp ?x ?y) (SubtractOp ?z ?w)) ?i)
(ConcatenateOp (Vec (MulOp ?x ?y) (MulOp ?z ?w)) ?i)=>(MulOp (ConcatenateOp (Vec ?x ?z) ?i) (ConcatenateOp (Vec ?y ?w) ?i))
(MulOp (ConcatenateOp (Vec ?x ?z) ?i) (ConcatenateOp (Vec ?y ?w) ?i))=>(ConcatenateOp (Vec (MulOp ?x ?y) (MulOp ?z ?w)) ?i)
(ConcatenateOp (Vec (DivOp ?x ?y) (DivOp ?z ?w)) ?i)=>(DivOp (ConcatenateOp (Vec ?x ?z) ?i) (ConcatenateOp (Vec ?y ?w) ?i))
(DivOp (ConcatenateOp (Vec ?x ?z) ?i) (ConcatenateOp (Vec ?y ?w) ?i))=>(ConcatenateOp (Vec (DivOp ?x ?y) (DivOp ?z ?w)) ?i)
(DivOp (DivOp ?x ?y) (DivOp ?z ?w))=>(DivOp (MulOp ?x ?w) (MulOp ?y ?z))
(DivOp (MulOp ?x ?w) (MulOp ?y ?z))=>(DivOp (DivOp ?x ?y) (DivOp ?z ?w))
(DotGeneralOp (DotGeneralOp ?x ?y ?lb ?rb ?lc ?rc ?p) ?z ?lb ?rb ?lc ?rc ?p)=>(DotGeneralOp ?x (DotGeneralOp ?y ?z ?lb ?rb ?lc ?rc ?p) ?lb ?rb ?lc ?rc ?p)
(DotGeneralOp ?x (DotGeneralOp ?y ?z ?lb ?rb ?lc ?rc ?p) ?lb ?rb ?lc ?rc ?p)=>(DotGeneralOp (DotGeneralOp ?x ?y ?lb ?rb ?lc ?rc ?p) ?z ?lb ?rb ?lc ?rc ?p)
(AddOp (DotGeneralOp ?x ?z ?lb ?rb ?lc ?rc ?p) (DotGeneralOp ?y ?z ?lb ?rb ?lc ?rc ?p))=>(DotGeneralOp (AddOp ?x ?y) ?z ?lb ?rb ?lc ?rc ?p)
(SubtractOp (DotGeneralOp ?x ?z ?lb ?rb ?lc ?rc ?p) (DotGeneralOp ?y ?z ?lb ?rb ?lc ?rc ?p))=>(DotGeneralOp (SubtractOp ?x ?y) ?z ?lb ?rb ?lc ?rc ?p)
(MulOp (DotGeneralOp ?x ?z ?lb ?rb ?lc ?rc ?p) (DotGeneralOp ?y ?z ?lb ?rb ?lc ?rc ?p))=>(DotGeneralOp (MulOp ?x ?y) ?z ?lb ?rb ?lc ?rc ?p)
(DivOp (DotGeneralOp ?x ?z ?lb ?rb ?lc ?rc ?p) (DotGeneralOp ?y ?z ?lb ?rb ?lc ?rc ?p))=>(DotGeneralOp (DivOp ?x ?y) ?z ?lb ?rb ?lc ?rc ?p)
(AddOp (DotGeneralOp ?x ?y ?lb ?rb ?lc ?rc ?p) (DotGeneralOp ?x ?z ?lb ?rb ?lc ?rc ?p))=>(DotGeneralOp ?x (AddOp ?y ?z) ?lb ?rb ?lc ?rc ?p)
(SubtractOp (DotGeneralOp ?x ?y ?lb ?rb ?lc ?rc ?p) (DotGeneralOp ?x ?z ?lb ?rb ?lc ?rc ?p))=>(DotGeneralOp ?x (SubtractOp ?y ?z) ?lb ?rb ?lc ?rc ?p)
(MulOp (DotGeneralOp ?x ?y ?lb ?rb ?lc ?rc ?p) (DotGeneralOp ?x ?z ?lb ?rb ?lc ?rc ?p))=>(DotGeneralOp ?x (MulOp ?y ?z) ?lb ?rb ?lc ?rc ?p)
(DivOp (DotGeneralOp ?x ?y ?lb ?rb ?lc ?rc ?p) (DotGeneralOp ?x ?z ?lb ?rb ?lc ?rc ?p))=>(DotGeneralOp ?x (DivOp ?y ?z) ?lb ?rb ?lc ?rc ?p)