Skip to content

Commit 3fc2efc

Browse files
ajpalajpal
committed
minimize trig and exp rules
1 parent c27f3a8 commit 3fc2efc

27 files changed

Lines changed: 888 additions & 840 deletions

‎jfp/exp/Enumo-LLM-1-derive.json‎

Lines changed: 16 additions & 35 deletions
Original file line numberDiff line numberDiff line change
@@ -1,53 +1,34 @@
11
{
22
"duration": {
33
"secs": 0,
4-
"nanos": 347611083
4+
"nanos": 336331208
55
},
66
"num_rules": 181,
7-
"num_against": 41,
7+
"num_against": 22,
88
"can": [
9-
"(exp (+ ?x ?y)) ==> (* (exp ?x) (exp ?y))",
10-
"(* (exp ?x) (exp ?y)) ==> (exp (+ ?x ?y))",
11-
"(exp (* -1 ?x)) ==> (/ 1 (exp ?x))",
12-
"(/ 1 (exp ?x)) ==> (exp (* -1 ?x))",
13-
"(exp 0) ==> 1",
14-
"1 ==> (exp 0)",
15-
"(exp 1) ==> (* (exp 0) (exp 1))",
16-
"(* (exp 0) (exp 1)) ==> (exp 1)",
9+
"(pow ?a 0) ==> 1",
10+
"(pow 1 ?b) ==> 1",
11+
"(pow ?a 2) ==> (* ?a ?a)",
12+
"(* ?a ?a) ==> (pow ?a 2)",
1713
"(log (exp ?x)) ==> ?x",
1814
"?x ==> (log (exp ?x))",
1915
"(exp (log ?x)) ==> ?x",
2016
"?x ==> (exp (log ?x))",
21-
"(log (pow ?x ?y)) ==> (* ?y (log ?x))",
22-
"(* ?y (log ?x)) ==> (log (pow ?x ?y))",
23-
"(log 1) ==> 0",
24-
"0 ==> (log 1)",
25-
"(pow ?x 0) ==> 1",
26-
"(pow ?x 1) ==> ?x",
27-
"?x ==> (pow ?x 1)",
28-
"(pow ?x (+ ?y ?z)) ==> (* (pow ?x ?y) (pow ?x ?z))",
29-
"(* (pow ?x ?y) (pow ?x ?z)) ==> (pow ?x (+ ?y ?z))",
30-
"(pow ?x (* ?y ?z)) ==> (pow (pow ?x ?y) ?z)",
31-
"(pow (pow ?x ?y) ?z) ==> (pow ?x (* ?y ?z))",
17+
"(exp (+ ?a ?b)) ==> (* (exp ?a) (exp ?b))",
18+
"(* (exp ?a) (exp ?b)) ==> (exp (+ ?a ?b))",
3219
"(pow ?x ?y) ==> (exp (* ?y (log ?x)))",
3320
"(exp (* ?y (log ?x))) ==> (pow ?x ?y)",
34-
"(exp 1) ==> (exp 1)",
35-
"(pow 1 ?x) ==> 1",
36-
"(exp (log (abs ?x))) ==> (abs ?x)",
37-
"(abs ?x) ==> (exp (log (abs ?x)))",
38-
"(exp (- ?x)) ==> (/ 1 (exp ?x))",
39-
"(/ 1 (exp ?x)) ==> (exp (- ?x))",
40-
"(exp (* ?x (log ?y))) ==> (pow ?y ?x)",
41-
"(pow ?y ?x) ==> (exp (* ?x (log ?y)))",
42-
"(exp (* 2 (log ?x))) ==> (pow ?x 2)",
43-
"(pow ?x 2) ==> (exp (* 2 (log ?x)))",
44-
"(exp (* 3 (log ?x))) ==> (pow ?x 3)",
45-
"(pow ?x 3) ==> (exp (* 3 (log ?x)))"
21+
"(exp (* ?a ?b)) ==> (pow (exp ?a) ?b)",
22+
"(pow (exp ?a) ?b) ==> (exp (* ?a ?b))",
23+
"(log (pow ?a ?b)) ==> (* ?b (log ?a))",
24+
"(* ?b (log ?a)) ==> (log (pow ?a ?b))",
25+
"(pow ?x (* ?y ?z)) ==> (pow (pow ?x ?y) ?z)",
26+
"(pow (pow ?x ?y) ?z) ==> (pow ?x (* ?y ?z))"
4627
],
4728
"cannot": [
4829
"(pow ?x -1) ==> (/ 1 ?x)",
4930
"(/ 1 ?x) ==> (pow ?x -1)",
50-
"(log (/ 1 ?x)) ==> (- (log ?x))",
51-
"(- (log ?x)) ==> (log (/ 1 ?x))"
31+
"(pow ?x (- ?y)) ==> (/ 1 (pow ?x ?y))",
32+
"(/ 1 (pow ?x ?y)) ==> (pow ?x (- ?y))"
5233
]
5334
}

‎jfp/exp/Enumo-LLM-2-derive.json‎

Lines changed: 33 additions & 76 deletions
Original file line numberDiff line numberDiff line change
@@ -1,93 +1,50 @@
11
{
22
"duration": {
3-
"secs": 1,
4-
"nanos": 92233833
3+
"secs": 0,
4+
"nanos": 674082791
55
},
66
"num_rules": 181,
7-
"num_against": 81,
7+
"num_against": 38,
88
"can": [
9-
"(exp (+ ?x ?y)) ==> (* (exp ?x) (exp ?y))",
10-
"(* (exp ?x) (exp ?y)) ==> (exp (+ ?x ?y))",
11-
"(exp (* -1 ?x)) ==> (/ 1 (exp ?x))",
12-
"(/ 1 (exp ?x)) ==> (exp (* -1 ?x))",
13-
"(exp 0) ==> 1",
14-
"1 ==> (exp 0)",
15-
"(exp 1) ==> (* (exp 0) (exp 1))",
16-
"(* (exp 0) (exp 1)) ==> (exp 1)",
9+
"(exp (- ?a ?b)) ==> (/ (exp ?a) (exp ?b))",
10+
"(/ (exp ?a) (exp ?b)) ==> (exp (- ?a ?b))",
11+
"(pow ?x (+ ?a ?b)) ==> (* (pow ?x ?a) (pow ?x ?b))",
12+
"(* (pow ?x ?a) (pow ?x ?b)) ==> (pow ?x (+ ?a ?b))",
13+
"(pow ?a (* ?b ?c)) ==> (pow (pow ?a ?b) ?c)",
14+
"(pow (pow ?a ?b) ?c) ==> (pow ?a (* ?b ?c))",
15+
"(pow ?a 0) ==> 1",
16+
"(pow 1 ?b) ==> 1",
17+
"(pow ?a 2) ==> (* ?a ?a)",
18+
"(* ?a ?a) ==> (pow ?a 2)",
1719
"(log (exp ?x)) ==> ?x",
1820
"?x ==> (log (exp ?x))",
1921
"(exp (log ?x)) ==> ?x",
2022
"?x ==> (exp (log ?x))",
21-
"(log (pow ?x ?y)) ==> (* ?y (log ?x))",
22-
"(* ?y (log ?x)) ==> (log (pow ?x ?y))",
23-
"(log 1) ==> 0",
24-
"0 ==> (log 1)",
25-
"(pow ?x 0) ==> 1",
26-
"(pow ?x 1) ==> ?x",
27-
"?x ==> (pow ?x 1)",
28-
"(pow ?x (+ ?y ?z)) ==> (* (pow ?x ?y) (pow ?x ?z))",
29-
"(* (pow ?x ?y) (pow ?x ?z)) ==> (pow ?x (+ ?y ?z))",
30-
"(pow ?x (* ?y ?z)) ==> (pow (pow ?x ?y) ?z)",
31-
"(pow (pow ?x ?y) ?z) ==> (pow ?x (* ?y ?z))",
23+
"(exp (+ ?a ?b)) ==> (* (exp ?a) (exp ?b))",
24+
"(* (exp ?a) (exp ?b)) ==> (exp (+ ?a ?b))",
3225
"(pow ?x ?y) ==> (exp (* ?y (log ?x)))",
3326
"(exp (* ?y (log ?x))) ==> (pow ?x ?y)",
34-
"(exp 1) ==> (exp 1)",
35-
"(pow 1 ?x) ==> 1",
36-
"(exp (log (abs ?x))) ==> (abs ?x)",
37-
"(abs ?x) ==> (exp (log (abs ?x)))",
38-
"(exp (- ?x)) ==> (/ 1 (exp ?x))",
39-
"(/ 1 (exp ?x)) ==> (exp (- ?x))",
40-
"(exp (* ?x (log ?y))) ==> (pow ?y ?x)",
41-
"(pow ?y ?x) ==> (exp (* ?x (log ?y)))",
42-
"(exp (* 2 (log ?x))) ==> (pow ?x 2)",
43-
"(pow ?x 2) ==> (exp (* 2 (log ?x)))",
44-
"(exp (* 3 (log ?x))) ==> (pow ?x 3)",
45-
"(pow ?x 3) ==> (exp (* 3 (log ?x)))",
46-
"(exp (+ 1 1)) ==> (pow (exp 1) 2)",
47-
"(pow (exp 1) 2) ==> (exp (+ 1 1))",
48-
"(log (exp 0)) ==> 0",
49-
"0 ==> (log (exp 0))",
50-
"(exp (log 1)) ==> 1",
51-
"1 ==> (exp (log 1))",
52-
"(log (pow 1 ?x)) ==> 0",
53-
"(pow (abs ?x) ?y) ==> (exp (* ?y (log (abs ?x))))",
54-
"(exp (* ?y (log (abs ?x)))) ==> (pow (abs ?x) ?y)",
55-
"(log (exp (- ?x))) ==> (- ?x)",
56-
"(- ?x) ==> (log (exp (- ?x)))",
57-
"(log (pow ?x -1)) ==> (- (log ?x))",
58-
"(- (log ?x)) ==> (log (pow ?x -1))",
59-
"(exp (* -1 ?x)) ==> (exp (- ?x))",
60-
"(exp (- ?x)) ==> (exp (* -1 ?x))",
61-
"(pow ?x -2) ==> (/ 1 (pow ?x 2))",
62-
"(/ 1 (pow ?x 2)) ==> (pow ?x -2)",
63-
"(pow (* ?x ?y) ?z) ==> (* (pow ?x ?z) (pow ?y ?z))",
64-
"(* (pow ?x ?z) (pow ?y ?z)) ==> (pow (* ?x ?y) ?z)"
27+
"(exp (* ?a ?b)) ==> (pow (exp ?a) ?b)",
28+
"(pow (exp ?a) ?b) ==> (exp (* ?a ?b))",
29+
"(log (pow ?a ?b)) ==> (* ?b (log ?a))",
30+
"(* ?b (log ?a)) ==> (log (pow ?a ?b))",
31+
"(pow ?x (* ?y ?z)) ==> (pow (pow ?x ?y) ?z)",
32+
"(pow (pow ?x ?y) ?z) ==> (pow ?x (* ?y ?z))"
6533
],
6634
"cannot": [
67-
"(log (* ?x ?y)) ==> (+ (log ?x) (log ?y))",
68-
"(+ (log ?x) (log ?y)) ==> (log (* ?x ?y))",
69-
"(log (/ ?x ?y)) ==> (- (log ?x) (log ?y))",
70-
"(- (log ?x) (log ?y)) ==> (log (/ ?x ?y))",
71-
"(exp (log ?x)) ==> (exp (log (abs ?x)))",
72-
"(exp (log (abs ?x))) ==> (exp (log ?x))",
35+
"(pow 0 ?y) ==> 0",
36+
"(pow ?x 3) ==> (* ?x (* ?x ?x))",
37+
"(* ?x (* ?x ?x)) ==> (pow ?x 3)",
38+
"(pow e ?x) ==> (exp ?x)",
39+
"(exp ?x) ==> (pow e ?x)",
40+
"(pow ?x (/ ?a ?b)) ==> (pow (pow ?x ?a) (/ 1 ?b))",
41+
"(pow (pow ?x ?a) (/ 1 ?b)) ==> (pow ?x (/ ?a ?b))",
42+
"(/ (pow ?a ?b) (pow ?a ?c)) ==> (pow ?a (- ?b ?c))",
43+
"(pow ?a (- ?b ?c)) ==> (/ (pow ?a ?b) (pow ?a ?c))",
44+
"(* (pow ?x ?a) (pow ?x ?b)) ==> (pow ?x (+ ?b ?b))",
7345
"(pow ?x -1) ==> (/ 1 ?x)",
7446
"(/ 1 ?x) ==> (pow ?x -1)",
75-
"(log (/ 1 ?x)) ==> (- (log ?x))",
76-
"(- (log ?x)) ==> (log (/ 1 ?x))",
77-
"(log (* ?a ?b)) ==> (+ (log ?a) (log ?b))",
78-
"(+ (log ?a) (log ?b)) ==> (log (* ?a ?b))",
79-
"(log 0) ==> undefined",
80-
"undefined ==> (log 0)",
81-
"(exp undefined) ==> undefined",
82-
"undefined ==> (exp undefined)",
83-
"(log (abs ?x)) ==> (abs (log ?x))",
84-
"(abs (log ?x)) ==> (log (abs ?x))",
85-
"(pow 0 ?x) ==> 0",
86-
"(pow 0 0) ==> undefined",
87-
"undefined ==> (pow 0 0)",
88-
"(pow ?x -3) ==> (/ 1 (pow ?x 3))",
89-
"(/ 1 (pow ?x 3)) ==> (pow ?x -3)",
90-
"(pow (/ ?x ?y) ?z) ==> (/ (pow ?x ?z) (pow ?y ?z))",
91-
"(/ (pow ?x ?z) (pow ?y ?z)) ==> (pow (/ ?x ?y) ?z)"
47+
"(pow ?x (- ?y)) ==> (/ 1 (pow ?x ?y))",
48+
"(/ 1 (pow ?x ?y)) ==> (pow ?x (- ?y))"
9249
]
9350
}

‎jfp/exp/LLM-1-RAT-Enumo-derive.json‎

Lines changed: 13 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
{
22
"duration": {
33
"secs": 0,
4-
"nanos": 545289583
4+
"nanos": 433656791
55
},
6-
"num_rules": 182,
6+
"num_rules": 163,
77
"num_against": 40,
88
"can": [
99
"(exp (+ ?a ?b)) ==> (* (exp ?a) (exp ?b))",
@@ -13,19 +13,9 @@
1313
"(exp 0) ==> 1",
1414
"(log (exp ?a)) ==> ?a",
1515
"(exp (log ?a)) ==> ?a",
16-
"(pow 1 ?a) ==> (cbrt 1)",
17-
"(pow 1 ?a) ==> (sqrt 1)",
1816
"(pow 1 ?a) ==> 1",
1917
"?a ==> (pow ?a 1)",
2018
"(pow ?a 1) ==> ?a",
21-
"(sqrt (cbrt ?a)) ==> (cbrt (sqrt ?a))",
22-
"(cbrt (sqrt ?a)) ==> (sqrt (cbrt ?a))",
23-
"(cbrt (* ?a ?b)) ==> (* (cbrt ?b) (cbrt ?a))",
24-
"(sqrt (* ?b ?a)) ==> (* (sqrt ?b) (sqrt ?a))",
25-
"(pow (sqrt ?b) ?a) ==> (sqrt (pow ?b ?a))",
26-
"(sqrt (pow ?b ?a)) ==> (pow (sqrt ?b) ?a)",
27-
"(cbrt (pow ?b ?a)) ==> (pow (cbrt ?b) ?a)",
28-
"(pow (cbrt ?b) ?a) ==> (cbrt (pow ?b ?a))",
2919
"(* (pow ?b ?c) (pow ?b ?a)) ==> (pow ?b (+ ?a ?c))",
3020
"(pow ?b (+ ?a ?c)) ==> (* (pow ?b ?c) (pow ?b ?a))",
3121
"(pow (* ?c ?b) ?a) ==> (* (pow ?b ?a) (pow ?c ?a))",
@@ -42,11 +32,21 @@
4232
"(pow (pow ?c ?a) ?b) ==> (pow (pow ?c ?b) ?a)"
4333
],
4434
"cannot": [
35+
"(pow 1 ?a) ==> (cbrt 1)",
36+
"(pow 1 ?a) ==> (sqrt 1)",
4537
"(* 1/2 (log ?a)) ==> (log (sqrt ?a))",
4638
"(log (sqrt ?a)) ==> (* 1/2 (log ?a))",
4739
"(* 1/3 (log ?a)) ==> (log (cbrt ?a))",
4840
"(log (cbrt ?a)) ==> (* 1/3 (log ?a))",
41+
"(sqrt (cbrt ?a)) ==> (cbrt (sqrt ?a))",
42+
"(cbrt (sqrt ?a)) ==> (sqrt (cbrt ?a))",
4943
"(* (cbrt ?b) (cbrt ?a)) ==> (cbrt (* ?a ?b))",
50-
"(* (sqrt ?b) (sqrt ?a)) ==> (sqrt (* ?b ?a))"
44+
"(cbrt (* ?a ?b)) ==> (* (cbrt ?b) (cbrt ?a))",
45+
"(* (sqrt ?b) (sqrt ?a)) ==> (sqrt (* ?b ?a))",
46+
"(sqrt (* ?b ?a)) ==> (* (sqrt ?b) (sqrt ?a))",
47+
"(pow (sqrt ?b) ?a) ==> (sqrt (pow ?b ?a))",
48+
"(sqrt (pow ?b ?a)) ==> (pow (sqrt ?b) ?a)",
49+
"(cbrt (pow ?b ?a)) ==> (pow (cbrt ?b) ?a)",
50+
"(pow (cbrt ?b) ?a) ==> (cbrt (pow ?b ?a))"
5151
]
5252
}

‎jfp/exp/LLM-1-RAT-Herbie-derive.json‎

Lines changed: 20 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,13 @@
11
{
22
"duration": {
33
"secs": 1,
4-
"nanos": 545608958
4+
"nanos": 286280083
55
},
6-
"num_rules": 182,
6+
"num_rules": 163,
77
"num_against": 75,
88
"can": [
99
"(+ (log ?a) (log ?b)) ==> (log (* ?a ?b))",
1010
"(log (* ?a ?b)) ==> (+ (log ?a) (log ?b))",
11-
"(log (/ ?a ?b)) ==> (- (log ?a) (log ?b))",
1211
"(log (pow ?a ?b)) ==> (* ?b (log ?a))",
1312
"(/ 1 ?a) ==> (pow ?a -1)",
1413
"(pow 0 ?a) ==> 0",
@@ -20,23 +19,17 @@
2019
"(pow ?a (* ?b ?c)) ==> (pow (pow ?a ?b) ?c)",
2120
"(pow ?a (+ ?b ?c)) ==> (* (pow ?a ?b) (pow ?a ?c))",
2221
"(pow (* ?a ?b) ?c) ==> (* (pow ?a ?c) (pow ?b ?c))",
23-
"(sqrt ?a) ==> (pow ?a 1/2)",
2422
"(* ?a ?a) ==> (pow ?a 2)",
25-
"(cbrt ?a) ==> (pow ?a 1/3)",
2623
"(exp (* (log ?a) ?b)) ==> (pow ?a ?b)",
2724
"(* (pow ?a ?b) ?a) ==> (pow ?a (+ ?b 1))",
28-
"(pow ?a 1/2) ==> (sqrt ?a)",
2925
"(pow ?a 2) ==> (* ?a ?a)",
30-
"(pow ?a 1/3) ==> (cbrt ?a)",
3126
"?a ==> (pow ?a 1)",
3227
"(pow ?a 0) ==> 1",
3328
"(pow 1 ?a) ==> 1",
3429
"(pow ?a 1) ==> ?a",
3530
"(pow ?a -1) ==> (/ 1 ?a)",
3631
"(* (exp ?a) (exp ?b)) ==> (exp (+ ?a ?b))",
3732
"(exp (* ?a ?b)) ==> (pow (exp ?a) ?b)",
38-
"(exp (/ ?a 2)) ==> (sqrt (exp ?a))",
39-
"(exp (/ ?a 3)) ==> (cbrt (exp ?a))",
4033
"(exp (* ?a 2)) ==> (* (exp ?a) (exp ?a))",
4134
"(exp (* ?a 3)) ==> (pow (exp ?a) 3)",
4235
"(exp (+ ?a ?b)) ==> (* (exp ?a) (exp ?b))",
@@ -46,39 +39,46 @@
4639
"(log (exp ?a)) ==> ?a",
4740
"?a ==> (exp (log ?a))",
4841
"?a ==> (log (exp ?a))",
49-
"(cbrt (* ?a ?b)) ==> (* (cbrt ?a) (cbrt ?b))",
50-
"?a ==> (* (* (cbrt ?a) (cbrt ?a)) (cbrt ?a))",
5142
"(pow (* ?a ?b) 3) ==> (* (pow ?a 3) (pow ?b 3))",
52-
"(pow (cbrt ?a) 3) ==> ?a",
53-
"(cbrt (pow ?a 3)) ==> ?a",
54-
"(* (* (cbrt ?a) (cbrt ?a)) (cbrt ?a)) ==> ?a",
55-
"(* (cbrt ?a) (* (cbrt ?a) (cbrt ?a))) ==> ?a",
56-
"(sqrt (* ?a ?b)) ==> (* (sqrt ?a) (sqrt ?b))",
57-
"(sqrt (pow ?a ?b)) ==> (pow ?a (/ ?b 2))",
58-
"(pow (sqrt ?a) ?b) ==> (pow ?a (/ ?b 2))",
59-
"?a ==> (* (sqrt ?a) (sqrt ?a))",
60-
"(* (sqrt ?a) (sqrt ?a)) ==> ?a",
6143
"(pow ?a ?b) ==> (* (pow ?a (/ ?b 2)) (pow ?a (/ ?b 2)))",
6244
"(* (pow ?a ?b) (pow ?a ?b)) ==> (pow ?a (* 2 ?b))"
6345
],
6446
"cannot": [
6547
"(- (log ?a) (log ?b)) ==> (log (/ ?a ?b))",
48+
"(log (/ ?a ?b)) ==> (- (log ?a) (log ?b))",
6649
"(/ (pow ?a ?b) (pow ?a ?c)) ==> (pow ?a (- ?b ?c))",
6750
"(pow ?a (- ?b ?c)) ==> (/ (pow ?a ?b) (pow ?a ?c))",
51+
"(sqrt ?a) ==> (pow ?a 1/2)",
52+
"(cbrt ?a) ==> (pow ?a 1/3)",
6853
"(* (* ?a ?a) ?a) ==> (pow ?a 3)",
54+
"(pow ?a 1/2) ==> (sqrt ?a)",
6955
"(pow ?a 3) ==> (* (* ?a ?a) ?a)",
56+
"(pow ?a 1/3) ==> (cbrt ?a)",
7057
"(/ (exp ?a) (exp ?b)) ==> (exp (- ?a ?b))",
58+
"(exp (/ ?a 2)) ==> (sqrt (exp ?a))",
59+
"(exp (/ ?a 3)) ==> (cbrt (exp ?a))",
7160
"(exp (- ?a ?b)) ==> (/ (exp ?a) (exp ?b))",
7261
"(* ?a (* ?a ?a)) ==> (pow ?a 3)",
62+
"(cbrt (* ?a ?b)) ==> (* (cbrt ?a) (cbrt ?b))",
7363
"(cbrt (/ ?a ?b)) ==> (/ (cbrt ?a) (cbrt ?b))",
7464
"(* (cbrt ?a) (cbrt ?b)) ==> (cbrt (* ?a ?b))",
7565
"(/ (cbrt ?a) (cbrt ?b)) ==> (cbrt (/ ?a ?b))",
66+
"?a ==> (* (* (cbrt ?a) (cbrt ?a)) (cbrt ?a))",
7667
"?a ==> (cbrt (* (* ?a ?a) ?a))",
7768
"(pow (/ ?a ?b) 3) ==> (/ (pow ?a 3) (pow ?b 3))",
7869
"(pow ?a 3) ==> (* ?a (* ?a ?a))",
70+
"(pow (cbrt ?a) 3) ==> ?a",
71+
"(cbrt (pow ?a 3)) ==> ?a",
72+
"(* (* (cbrt ?a) (cbrt ?a)) (cbrt ?a)) ==> ?a",
73+
"(* (cbrt ?a) (* (cbrt ?a) (cbrt ?a))) ==> ?a",
74+
"(sqrt (* ?a ?b)) ==> (* (sqrt ?a) (sqrt ?b))",
7975
"(sqrt (/ ?a ?b)) ==> (/ (sqrt ?a) (sqrt ?b))",
76+
"(sqrt (pow ?a ?b)) ==> (pow ?a (/ ?b 2))",
77+
"(pow (sqrt ?a) ?b) ==> (pow ?a (/ ?b 2))",
8078
"(* (sqrt ?a) (sqrt ?b)) ==> (sqrt (* ?a ?b))",
8179
"(/ (sqrt ?a) (sqrt ?b)) ==> (sqrt (/ ?a ?b))",
80+
"?a ==> (* (sqrt ?a) (sqrt ?a))",
81+
"(* (sqrt ?a) (sqrt ?a)) ==> ?a",
8282
"(+ (pow ?a 3) (pow ?b 3)) ==> (* (+ (* ?a ?a) (- (* ?b ?b) (* ?a ?b))) (+ ?a ?b))",
8383
"(- (pow ?a 3) (pow ?b 3)) ==> (* (+ (* ?a ?a) (+ (* ?b ?b) (* ?a ?b))) (- ?a ?b))",
8484
"(+ ?a ?b) ==> (/ (+ (pow ?a 3) (pow ?b 3)) (+ (* ?a ?a) (- (* ?b ?b) (* ?a ?b))))",

‎jfp/exp/LLM-1.rules‎

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
(pow ?x -1) ==> (/ 1 ?x)
2+
(/ 1 ?x) ==> (pow ?x -1)
3+
(pow ?a 0) ==> 1
4+
(pow 1 ?b) ==> 1
5+
(pow ?a 2) ==> (* ?a ?a)
6+
(* ?a ?a) ==> (pow ?a 2)
7+
(log (exp ?x)) ==> ?x
8+
?x ==> (log (exp ?x))
9+
(exp (log ?x)) ==> ?x
10+
?x ==> (exp (log ?x))
11+
(pow ?x (- ?y)) ==> (/ 1 (pow ?x ?y))
12+
(/ 1 (pow ?x ?y)) ==> (pow ?x (- ?y))
13+
(exp (+ ?a ?b)) ==> (* (exp ?a) (exp ?b))
14+
(* (exp ?a) (exp ?b)) ==> (exp (+ ?a ?b))
15+
(pow ?x ?y) ==> (exp (* ?y (log ?x)))
16+
(exp (* ?y (log ?x))) ==> (pow ?x ?y)
17+
(exp (* ?a ?b)) ==> (pow (exp ?a) ?b)
18+
(pow (exp ?a) ?b) ==> (exp (* ?a ?b))
19+
(log (pow ?a ?b)) ==> (* ?b (log ?a))
20+
(* ?b (log ?a)) ==> (log (pow ?a ?b))
21+
(pow ?x (* ?y ?z)) ==> (pow (pow ?x ?y) ?z)
22+
(pow (pow ?x ?y) ?z) ==> (pow ?x (* ?y ?z))

‎jfp/exp/LLM-2-RAT-Enumo-derive.json‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
{
22
"duration": {
33
"secs": 0,
4-
"nanos": 105314166
4+
"nanos": 105263000
55
},
6-
"num_rules": 222,
6+
"num_rules": 179,
77
"num_against": 40,
88
"can": [
99
"(exp (+ ?a ?b)) ==> (* (exp ?a) (exp ?b))",

‎jfp/exp/LLM-2-RAT-Herbie-derive.json‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
{
22
"duration": {
33
"secs": 0,
4-
"nanos": 222751917
4+
"nanos": 119834208
55
},
6-
"num_rules": 222,
6+
"num_rules": 179,
77
"num_against": 75,
88
"can": [
99
"(+ (log ?a) (log ?b)) ==> (log (* ?a ?b))",

0 commit comments

Comments
 (0)