diff --git a/data/dummy_examples/Makefile b/data/dummy_examples/Makefile new file mode 100644 index 0000000..9355a77 --- /dev/null +++ b/data/dummy_examples/Makefile @@ -0,0 +1,15 @@ +# make the .json data from the .egg files in this directory +# run make from this directory +# FIXME this doesn't quite work yet, egglog +# doesn't export roots properly + +egg_files = $(wildcard *.egg) +json_files = $(egg_files:.egg=.json) + +all: $(json_files) + +egglog_manifest = ../../../egglog/Cargo.toml + +%.json: %.egg + cargo run --manifest-path $(egglog_manifest) -- $< --to-json + \ No newline at end of file diff --git a/data/dummy_examples/ab_add.egg b/data/dummy_examples/ab_add.egg index e42ede0..1b42c72 100644 --- a/data/dummy_examples/ab_add.egg +++ b/data/dummy_examples/ab_add.egg @@ -7,10 +7,10 @@ ; DAG extraction notices that balanced trees are much cheaper ; Optimal tree is (let t1 (a + b) in let t2 = (t1 + t1) in (t2 + t2) ; Which is cost 5 and proportional to the logarithm of the number of nodes -(define A2 (Add (A) (A))) -(define A4 (Add A2 A2)) -(define B2 (Add (B) (B))) -(define B4 (Add B2 B2)) -(define t (Add A4 B4)) +(let A2 (Add (A) (A))) +(let A4 (Add A2 A2)) +(let B2 (Add (B) (B))) +(let B4 (Add B2 B2)) +(let t (Add A4 B4)) (run 10) diff --git a/data/dummy_examples/ab_add.json b/data/dummy_examples/ab_add.json index d1f1f4e..6f9a03c 100644 --- a/data/dummy_examples/ab_add.json +++ b/data/dummy_examples/ab_add.json @@ -1,513 +1,445 @@ { - "nodes": { - "B2-0": { - "op": "B2", - "children": [], - "eclass": "4", - "cost": 9.223372036854776e18 - }, - "Add-0": { - "op": "Add", - "children": [ - "A-0", - "v10___-0" - ], - "eclass": "1", - "cost": 1.0 - }, - "Add-6828067974578293639": { - "op": "Add", - "children": [ - "A2-0", - "Add-0" - ], - "eclass": "2", - "cost": 1.0 - }, - "Add-15443823971188422721": { - "op": "Add", - "children": [ - "v13___-0", - "B-0" - ], - "eclass": "4", - "cost": 1.0 - }, - "Add-5435976351651060604": { - "op": "Add", - "children": [ - "B2-0", - "Add-15443823971188422721" - ], - "eclass": "5", - "cost": 1.0 - }, - "Add-2743974990046126629": { - "op": "Add", - "children": [ - "Add-11413373673517832166", - "Add-4024615130029849749" - ], - "eclass": "6", - "cost": 1.0 - }, - "Add-15318938057191675792": { - "op": "Add", - "children": [ - "v11___-0", - "v12___-0" - ], - "eclass": "11", - "cost": 1.0 - }, - "Add-5871781006564002453": { - "op": "Add", - "children": [ - "A-0", - "v9___-0" - ], - "eclass": "14", - "cost": 1.0 - }, - "Add-16275225025205966978": { - "op": "Add", - "children": [ - "v13___-0", - "B2-0" - ], - "eclass": "16", - "cost": 1.0 - }, - "Add-11868447927124751835": { - "op": "Add", - "children": [ - "A2-0", - "B4-0" - ], - "eclass": "18", - "cost": 1.0 - }, - "Add-17014444194973979140": { - "op": "Add", - "children": [ - "Add-12139158412232607314", - "Add-15443823971188422721" - ], - "eclass": "6", - "cost": 1.0 - }, - "Add-8055065427700440304": { - "op": "Add", - "children": [ - "v14___-0", - "A4-0" - ], - "eclass": "6", - "cost": 1.0 - }, - "Add-8417957797057827878": { - "op": "Add", - "children": [ - "v10___-0", - "Add-5871781006564002453" - ], - "eclass": "2", - "cost": 1.0 - }, - "Add-1154085167566592390": { - "op": "Add", - "children": [ - "B-0", - "Add-16275225025205966978" - ], - "eclass": "5", - "cost": 1.0 - }, - "Add-9374244765072119064": { - "op": "Add", - "children": [ - "Add-0", - "Add-13089610212606157694" - ], - "eclass": "6", - "cost": 1.0 - }, - "Add-5996666920560749382": { - "op": "Add", - "children": [ - "v9___-0", - "v12___-0" - ], - "eclass": "30", - "cost": 1.0 - }, - "Add-13531250035159840349": { - "op": "Add", - "children": [ - "A2-0", - "v13___-0" - ], - "eclass": "34", - "cost": 1.0 - }, - "Add-10912160959110460649": { - "op": "Add", - "children": [ - "A-0", - "Add-1154085167566592390" - ], - "eclass": "46", - "cost": 1.0 - }, - "Add-5040379952546458196": { - "op": "Add", - "children": [ - "v10___-0", - "B2-0" - ], - "eclass": "51", - "cost": 1.0 - }, - "Add-6372993720971373970": { - "op": "Add", - "children": [ - "Add-956286968014291186", - "Add-15443823971188422721" - ], - "eclass": "53", - "cost": 1.0 - }, - "Add-13458337749604286074": { - "op": "Add", - "children": [ - "A-0", - "Add-13287408412158458898" - ], - "eclass": "56", - "cost": 1.0 - }, - "Add-9572042964624420268": { - "op": "Add", - "children": [ - "B-0", - "Add-8417957797057827878" - ], - "eclass": "59", - "cost": 1.0 - }, - "Add-4024615130029849749": { - "op": "Add", - "children": [ - "Add-18010939418796609767", - "v13___-0" - ], - "eclass": "5", - "cost": 1.0 - }, - "Add-802958170842058029": { - "op": "Add", - "children": [ - "Add-16275225025205966978", - "Add-9572042964624420268" - ], - "eclass": "6", - "cost": 1.0 - }, - "Add-11413373673517832166": { - "op": "Add", - "children": [ - "Add-5871781006564002453", - "v10___-0" - ], - "eclass": "2", - "cost": 1.0 - }, - "Add-6424967349412566624": { - "op": "Add", - "children": [ - "Add-956286968014291186", - "Add-10912160959110460649" - ], - "eclass": "6", - "cost": 1.0 - }, - "Add-10685919876382673217": { - "op": "Add", - "children": [ - "Add-5871781006564002453", - "Add-5040379952546458196" - ], - "eclass": "11", - "cost": 1.0 - }, - "Add-11808970072622434574": { - "op": "Add", - "children": [ - "Add-7223664373682896047", - "Add-0" - ], - "eclass": "6", - "cost": 1.0 - }, - "Add-2671062704490572354": { - "op": "Add", - "children": [ - "v9___-0", - "Add-18010939418796609767" - ], - "eclass": "32", - "cost": 1.0 - }, - "Add-197798199552301204": { - "op": "Add", - "children": [ - "v11___-0", - "Add-16275225025205966978" - ], - "eclass": "36", - "cost": 1.0 - }, - "Add-7930179513703693375": { - "op": "Add", - "children": [ - "v12___-0", - "Add-16056488168539304153" - ], - "eclass": "6", - "cost": 1.0 - }, - "Add-18010939418796609767": { - "op": "Add", - "children": [ - "B2-0", - "B-0" - ], - "eclass": "16", - "cost": 1.0 - }, - "Add-956286968014291186": { - "op": "Add", - "children": [ - "A2-0", - "A-0" - ], - "eclass": "14", - "cost": 1.0 - }, - "Add-13775186695512593401": { - "op": "Add", - "children": [ - "Add-5996666920560749382", - "Add-15443823971188422721" - ], - "eclass": "18", - "cost": 1.0 - }, - "Add-13089610212606157694": { - "op": "Add", - "children": [ - "Add-2671062704490572354", - "v13___-0" - ], - "eclass": "18", - "cost": 1.0 - }, - "Add-13287408412158458898": { - "op": "Add", - "children": [ - "Add-13531250035159840349", - "Add-16275225025205966978" - ], - "eclass": "18", - "cost": 1.0 - }, - "Add-7613425605146757649": { - "op": "Add", - "children": [ - "Add-197798199552301204", - "B-0" - ], - "eclass": "6", - "cost": 1.0 - }, - "Add-7223664373682896047": { - "op": "Add", - "children": [ - "B4-0", - "Add-0" - ], - "eclass": "18", - "cost": 1.0 - }, - "Add-12139158412232607314": { - "op": "Add", - "children": [ - "v12___-0", - "A4-0" - ], - "eclass": "11", - "cost": 1.0 - }, - "Add-4333864812525660868": { - "op": "Add", - "children": [ - "v9___-0", - "Add-5996666920560749382" - ], - "eclass": "11", - "cost": 1.0 - }, - "Add-16056488168539304153": { - "op": "Add", - "children": [ - "v10___-0", - "Add-6372993720971373970" - ], - "eclass": "11", - "cost": 1.0 - }, - "v10___-0": { - "op": "v10___", - "children": [], - "eclass": "0", - "cost": 9.223372036854776e18 - }, - "B-0": { - "op": "B", - "children": [], - "eclass": "3", - "cost": 1.0 - }, - "A-0": { - "op": "A", - "children": [], - "eclass": "0", - "cost": 1.0 - }, - "v12___-0": { - "op": "v12___", - "children": [], - "eclass": "4", - "cost": 9.223372036854776e18 - }, - "v13___-0": { - "op": "v13___", - "children": [], - "eclass": "3", - "cost": 9.223372036854776e18 - }, - "v9___-0": { - "op": "v9___", - "children": [], - "eclass": "1", - "cost": 9.223372036854776e18 - }, - "A2-0": { - "op": "A2", - "children": [], - "eclass": "1", - "cost": 9.223372036854776e18 - }, - "B4-0": { - "op": "B4", - "children": [], - "eclass": "5", - "cost": 9.223372036854776e18 - }, - "v15___-0": { - "op": "v15___", - "children": [], - "eclass": "6", - "cost": 9.223372036854776e18 - }, - "t-0": { - "op": "t", - "children": [], - "eclass": "6", - "cost": 9.223372036854776e18 - }, - "v14___-0": { - "op": "v14___", - "children": [], - "eclass": "5", - "cost": 9.223372036854776e18 - }, - "v11___-0": { - "op": "v11___", - "children": [], - "eclass": "2", - "cost": 9.223372036854776e18 - }, - "A4-0": { - "op": "A4", - "children": [], - "eclass": "2", - "cost": 9.223372036854776e18 - } - }, - "root_eclasses": [ - "6" - ], - "class_data": { - "4": { - "type": "Math" - }, - "1": { - "type": "Math" - }, - "0": { - "type": "Math" - }, - "2": { - "type": "Math" - }, - "3": { - "type": "Math" - }, - "5": { - "type": "Math" - }, - "6": { - "type": "Math" - }, - "11": { - "type": "Math" - }, - "14": { - "type": "Math" - }, - "16": { - "type": "Math" - }, - "18": { - "type": "Math" - }, - "30": { - "type": "Math" - }, - "34": { - "type": "Math" - }, - "46": { - "type": "Math" - }, - "51": { - "type": "Math" - }, - "53": { - "type": "Math" - }, - "56": { - "type": "Math" - }, - "59": { - "type": "Math" - }, - "32": { - "type": "Math" - }, - "36": { - "type": "Math" - } + "nodes": { + "A-0": { + "op": "A", + "children": [], + "eclass": "0", + "cost": 1.0 + }, + "Add-0": { + "op": "Add", + "children": [ + "A-0", + "A-0" + ], + "eclass": "1", + "cost": 1.0 + }, + "Add-6828067974578293639": { + "op": "Add", + "children": [ + "Add-0", + "Add-0" + ], + "eclass": "2", + "cost": 1.0 + }, + "Add-15443823971188422721": { + "op": "Add", + "children": [ + "B-0", + "B-0" + ], + "eclass": "4", + "cost": 1.0 + }, + "Add-5435976351651060604": { + "op": "Add", + "children": [ + "Add-15443823971188422721", + "Add-15443823971188422721" + ], + "eclass": "5", + "cost": 1.0 + }, + "Add-2743974990046126629": { + "op": "Add", + "children": [ + "Add-17680751079186437027", + "Add-4024615130029849749" + ], + "eclass": "6", + "cost": 1.0 + }, + "Add-15318938057191675792": { + "op": "Add", + "children": [ + "Add-6828067974578293639", + "Add-15443823971188422721" + ], + "eclass": "8", + "cost": 1.0 + }, + "Add-11868447927124751835": { + "op": "Add", + "children": [ + "Add-0", + "Add-5435976351651060604" + ], + "eclass": "14", + "cost": 1.0 + }, + "Add-16275225025205966978": { + "op": "Add", + "children": [ + "B-0", + "Add-15443823971188422721" + ], + "eclass": "16", + "cost": 1.0 + }, + "Add-5871781006564002453": { + "op": "Add", + "children": [ + "A-0", + "Add-0" + ], + "eclass": "18", + "cost": 1.0 + }, + "Add-8055065427700440304": { + "op": "Add", + "children": [ + "Add-1154085167566592390", + "Add-13458337749604286074" + ], + "eclass": "6", + "cost": 1.0 + }, + "Add-11703353757319665465": { + "op": "Add", + "children": [ + "Add-12139158412232607314", + "Add-15443823971188422721" + ], + "eclass": "6", + "cost": 1.0 + }, + "Add-2619089076049379700": { + "op": "Add", + "children": [ + "Add-0", + "Add-8537008543413834001" + ], + "eclass": "6", + "cost": 1.0 + }, + "Add-1154085167566592390": { + "op": "Add", + "children": [ + "B-0", + "Add-16275225025205966978" + ], + "eclass": "5", + "cost": 1.0 + }, + "Add-13458337749604286074": { + "op": "Add", + "children": [ + "A-0", + "Add-5871781006564002453" + ], + "eclass": "2", + "cost": 1.0 + }, + "Add-13531250035159840349": { + "op": "Add", + "children": [ + "Add-0", + "B-0" + ], + "eclass": "28", + "cost": 1.0 + }, + "Add-1081172882011038115": { + "op": "Add", + "children": [ + "Add-6828067974578293639", + "B-0" + ], + "eclass": "30", + "cost": 1.0 + }, + "Add-1351883367118893594": { + "op": "Add", + "children": [ + "Add-5435976351651060604", + "A-0" + ], + "eclass": "38", + "cost": 1.0 + }, + "Add-5996666920560749382": { + "op": "Add", + "children": [ + "Add-0", + "Add-15443823971188422721" + ], + "eclass": "40", + "cost": 1.0 + }, + "Add-5040379952546458196": { + "op": "Add", + "children": [ + "A-0", + "Add-15443823971188422721" + ], + "eclass": "50", + "cost": 1.0 + }, + "Add-12640371126639978831": { + "op": "Add", + "children": [ + "Add-956286968014291186", + "Add-15443823971188422721" + ], + "eclass": "54", + "cost": 1.0 + }, + "Add-4024615130029849749": { + "op": "Add", + "children": [ + "Add-18010939418796609767", + "B-0" + ], + "eclass": "5", + "cost": 1.0 + }, + "Add-17680751079186437027": { + "op": "Add", + "children": [ + "Add-5871781006564002453", + "A-0" + ], + "eclass": "2", + "cost": 1.0 + }, + "Add-7651964802534713289": { + "op": "Add", + "children": [ + "Add-956286968014291186", + "Add-5040379952546458196" + ], + "eclass": "8", + "cost": 1.0 + }, + "Add-17285154680081834619": { + "op": "Add", + "children": [ + "Add-13089610212606157694", + "Add-0" + ], + "eclass": "6", + "cost": 1.0 + }, + "Add-8761580567721237632": { + "op": "Add", + "children": [ + "Add-15443823971188422721", + "Add-15318938057191675792" + ], + "eclass": "6", + "cost": 1.0 + }, + "Add-2671062704490572354": { + "op": "Add", + "children": [ + "Add-0", + "Add-16275225025205966978" + ], + "eclass": "32", + "cost": 1.0 + }, + "Add-197798199552301204": { + "op": "Add", + "children": [ + "Add-17680751079186437027", + "Add-18010939418796609767" + ], + "eclass": "34", + "cost": 1.0 + }, + "Add-6340289691224159136": { + "op": "Add", + "children": [ + "Add-4024615130029849749", + "Add-5871781006564002453" + ], + "eclass": "36", + "cost": 1.0 + }, + "Add-12139158412232607314": { + "op": "Add", + "children": [ + "Add-15443823971188422721", + "Add-6828067974578293639" + ], + "eclass": "8", + "cost": 1.0 + }, + "Add-18010939418796609767": { + "op": "Add", + "children": [ + "Add-15443823971188422721", + "B-0" + ], + "eclass": "16", + "cost": 1.0 + }, + "Add-956286968014291186": { + "op": "Add", + "children": [ + "Add-0", + "A-0" + ], + "eclass": "18", + "cost": 1.0 + }, + "Add-7223664373682896047": { + "op": "Add", + "children": [ + "Add-5435976351651060604", + "Add-0" + ], + "eclass": "14", + "cost": 1.0 + }, + "Add-8537008543413834001": { + "op": "Add", + "children": [ + "Add-13531250035159840349", + "Add-18010939418796609767" + ], + "eclass": "14", + "cost": 1.0 + }, + "Add-7020031006489854037": { + "op": "Add", + "children": [ + "Add-1081172882011038115", + "Add-16275225025205966978" + ], + "eclass": "6", + "cost": 1.0 + }, + "Add-13089610212606157694": { + "op": "Add", + "children": [ + "Add-2671062704490572354", + "B-0" + ], + "eclass": "14", + "cost": 1.0 + }, + "Add-9130403142070737613": { + "op": "Add", + "children": [ + "Add-197798199552301204", + "B-0" + ], + "eclass": "6", + "cost": 1.0 + }, + "Add-13485206611710760102": { + "op": "Add", + "children": [ + "Add-6340289691224159136", + "A-0" + ], + "eclass": "6", + "cost": 1.0 + }, + "Add-7811223804699058853": { + "op": "Add", + "children": [ + "Add-1351883367118893594", + "Add-5871781006564002453" + ], + "eclass": "6", + "cost": 1.0 + }, + "Add-14712204064832906767": { + "op": "Add", + "children": [ + "Add-5996666920560749382", + "Add-15443823971188422721" + ], + "eclass": "14", + "cost": 1.0 + }, + "Add-14606587749530137658": { + "op": "Add", + "children": [ + "Add-1081172882011038115", + "B-0" + ], + "eclass": "8", + "cost": 1.0 + }, + "B-0": { + "op": "B", + "children": [], + "eclass": "3", + "cost": 1.0 + } + }, + "root_eclasses": [ + "1", + "2", + "4", + "5", + "6" + ], + "class_data": { + "0": { + "type": "Math" + }, + "1": { + "type": "Math" + }, + "2": { + "type": "Math" + }, + "4": { + "type": "Math" + }, + "3": { + "type": "Math" + }, + "5": { + "type": "Math" + }, + "6": { + "type": "Math" + }, + "8": { + "type": "Math" + }, + "14": { + "type": "Math" + }, + "16": { + "type": "Math" + }, + "18": { + "type": "Math" + }, + "28": { + "type": "Math" + }, + "30": { + "type": "Math" + }, + "38": { + "type": "Math" + }, + "40": { + "type": "Math" + }, + "50": { + "type": "Math" + }, + "54": { + "type": "Math" + }, + "32": { + "type": "Math" + }, + "34": { + "type": "Math" + }, + "36": { + "type": "Math" } + } } \ No newline at end of file diff --git a/data/dummy_examples/choice.egg b/data/dummy_examples/choice.egg index 73b1336..ea48c77 100644 --- a/data/dummy_examples/choice.egg +++ b/data/dummy_examples/choice.egg @@ -6,7 +6,7 @@ ; Tree extraction would pick (g (x n)) ; Dag extraction notices the shared subterm A B across choices and makes the opposite choice. ; A and B are amoritized across uses, so cost (f n A B) ~ 1 -(define t +(let t (Cons (g (x 0)) (Cons (g (x 1)) (Cons (g (x 2)) diff --git a/data/dummy_examples/choice.json b/data/dummy_examples/choice.json new file mode 100644 index 0000000..9dfa5c6 --- /dev/null +++ b/data/dummy_examples/choice.json @@ -0,0 +1,937 @@ +{ + "nodes": { + "B-0": { + "op": "B", + "children": [], + "eclass": "53", + "cost": 1.0 + }, + "i64-0": { + "op": "0", + "children": [], + "eclass": "i64-0", + "cost": 0.0 + }, + "x-0": { + "op": "x", + "children": [ + "i64-0" + ], + "eclass": "0", + "cost": 1.0 + }, + "i64-5871781006564002453": { + "op": "1", + "children": [], + "eclass": "i64-5871781006564002453", + "cost": 0.0 + }, + "x-5871781006564002453": { + "op": "x", + "children": [ + "i64-5871781006564002453" + ], + "eclass": "2", + "cost": 1.0 + }, + "i64-11743562013128004906": { + "op": "2", + "children": [], + "eclass": "i64-11743562013128004906", + "cost": 0.0 + }, + "x-11743562013128004906": { + "op": "x", + "children": [ + "i64-11743562013128004906" + ], + "eclass": "4", + "cost": 1.0 + }, + "i64-17615343019692007359": { + "op": "3", + "children": [], + "eclass": "i64-17615343019692007359", + "cost": 0.0 + }, + "x-17615343019692007359": { + "op": "x", + "children": [ + "i64-17615343019692007359" + ], + "eclass": "6", + "cost": 1.0 + }, + "i64-5040379952546458196": { + "op": "4", + "children": [], + "eclass": "i64-5040379952546458196", + "cost": 0.0 + }, + "x-5040379952546458196": { + "op": "x", + "children": [ + "i64-5040379952546458196" + ], + "eclass": "8", + "cost": 1.0 + }, + "i64-10912160959110460649": { + "op": "5", + "children": [], + "eclass": "i64-10912160959110460649", + "cost": 0.0 + }, + "x-10912160959110460649": { + "op": "x", + "children": [ + "i64-10912160959110460649" + ], + "eclass": "10", + "cost": 1.0 + }, + "i64-16783941965674463102": { + "op": "6", + "children": [], + "eclass": "i64-16783941965674463102", + "cost": 0.0 + }, + "x-16783941965674463102": { + "op": "x", + "children": [ + "i64-16783941965674463102" + ], + "eclass": "12", + "cost": 1.0 + }, + "i64-4208978898528913939": { + "op": "7", + "children": [], + "eclass": "i64-4208978898528913939", + "cost": 0.0 + }, + "x-4208978898528913939": { + "op": "x", + "children": [ + "i64-4208978898528913939" + ], + "eclass": "14", + "cost": 1.0 + }, + "i64-10080759905092916392": { + "op": "8", + "children": [], + "eclass": "i64-10080759905092916392", + "cost": 0.0 + }, + "x-10080759905092916392": { + "op": "x", + "children": [ + "i64-10080759905092916392" + ], + "eclass": "16", + "cost": 1.0 + }, + "i64-15952540911656918845": { + "op": "9", + "children": [], + "eclass": "i64-15952540911656918845", + "cost": 0.0 + }, + "x-15952540911656918845": { + "op": "x", + "children": [ + "i64-15952540911656918845" + ], + "eclass": "18", + "cost": 1.0 + }, + "i64-3377577844511369682": { + "op": "10", + "children": [], + "eclass": "i64-3377577844511369682", + "cost": 0.0 + }, + "x-3377577844511369682": { + "op": "x", + "children": [ + "i64-3377577844511369682" + ], + "eclass": "20", + "cost": 1.0 + }, + "i64-9249358851075372135": { + "op": "11", + "children": [], + "eclass": "i64-9249358851075372135", + "cost": 0.0 + }, + "x-9249358851075372135": { + "op": "x", + "children": [ + "i64-9249358851075372135" + ], + "eclass": "22", + "cost": 1.0 + }, + "i64-15121139857639374588": { + "op": "12", + "children": [], + "eclass": "i64-15121139857639374588", + "cost": 0.0 + }, + "x-15121139857639374588": { + "op": "x", + "children": [ + "i64-15121139857639374588" + ], + "eclass": "24", + "cost": 1.0 + }, + "i64-2546176790493825425": { + "op": "13", + "children": [], + "eclass": "i64-2546176790493825425", + "cost": 0.0 + }, + "x-2546176790493825425": { + "op": "x", + "children": [ + "i64-2546176790493825425" + ], + "eclass": "26", + "cost": 1.0 + }, + "i64-8417957797057827878": { + "op": "14", + "children": [], + "eclass": "i64-8417957797057827878", + "cost": 0.0 + }, + "x-8417957797057827878": { + "op": "x", + "children": [ + "i64-8417957797057827878" + ], + "eclass": "28", + "cost": 1.0 + }, + "i64-14289738803621830331": { + "op": "15", + "children": [], + "eclass": "i64-14289738803621830331", + "cost": 0.0 + }, + "x-14289738803621830331": { + "op": "x", + "children": [ + "i64-14289738803621830331" + ], + "eclass": "30", + "cost": 1.0 + }, + "i64-1714775736476281168": { + "op": "16", + "children": [], + "eclass": "i64-1714775736476281168", + "cost": 0.0 + }, + "x-1714775736476281168": { + "op": "x", + "children": [ + "i64-1714775736476281168" + ], + "eclass": "32", + "cost": 1.0 + }, + "Cons-3913163647086339834": { + "op": "Cons", + "children": [ + "f-14404162188104689347", + "Nil-0" + ], + "eclass": "35", + "cost": 1.0 + }, + "Cons-7092943292045408312": { + "op": "Cons", + "children": [ + "f-10841857528096821280", + "Cons-3913163647086339834" + ], + "eclass": "36", + "cost": 1.0 + }, + "Cons-17755332423162375103": { + "op": "Cons", + "children": [ + "f-12439173641694160734", + "Cons-7092943292045408312" + ], + "eclass": "37", + "cost": 1.0 + }, + "Cons-5034544784905717390": { + "op": "Cons", + "children": [ + "f-17346800407185313199", + "Cons-17755332423162375103" + ], + "eclass": "38", + "cost": 1.0 + }, + "Cons-3173944477318327672": { + "op": "Cons", + "children": [ + "f-9047720384188800451", + "Cons-5034544784905717390" + ], + "eclass": "39", + "cost": 1.0 + }, + "Cons-17213911452946664145": { + "op": "Cons", + "children": [ + "f-11357196730744934837", + "Cons-3173944477318327672" + ], + "eclass": "40", + "cost": 1.0 + }, + "Cons-5324524868707550689": { + "op": "Cons", + "children": [ + "f-2696893396811418316", + "Cons-17213911452946664145" + ], + "eclass": "41", + "cost": 1.0 + }, + "Cons-15986913999824517480": { + "op": "Cons", + "children": [ + "f-17541124554704762424", + "Cons-5324524868707550689" + ], + "eclass": "42", + "cost": 1.0 + }, + "Cons-14957714746254672019": { + "op": "Cons", + "children": [ + "f-5073273888987675178", + "Cons-15986913999824517480" + ], + "eclass": "43", + "cost": 1.0 + }, + "Cons-16474692283178651983": { + "op": "Cons", + "children": [ + "f-2169771887131140391", + "Cons-14957714746254672019" + ], + "eclass": "44", + "cost": 1.0 + }, + "Cons-12067915185097436840": { + "op": "Cons", + "children": [ + "f-3212232599459531873", + "Cons-16474692283178651983" + ], + "eclass": "45", + "cost": 1.0 + }, + "Cons-11090689559968784033": { + "op": "Cons", + "children": [ + "f-15593295566627074243", + "Cons-12067915185097436840" + ], + "eclass": "46", + "cost": 1.0 + }, + "Cons-5852511407870024633": { + "op": "Cons", + "children": [ + "f-16215055113516144691", + "Cons-11090689559968784033" + ], + "eclass": "47", + "cost": 1.0 + }, + "Cons-8148916370370356200": { + "op": "Cons", + "children": [ + "f-13628307020216545630", + "Cons-5852511407870024633" + ], + "eclass": "48", + "cost": 1.0 + }, + "Cons-14654300231399601706": { + "op": "Cons", + "children": [ + "f-12955991996068655944", + "Cons-8148916370370356200" + ], + "eclass": "49", + "cost": 1.0 + }, + "Cons-3596314701178032507": { + "op": "Cons", + "children": [ + "f-14077105124241970906", + "Cons-14654300231399601706" + ], + "eclass": "50", + "cost": 1.0 + }, + "Cons-5944693292119556728": { + "op": "Cons", + "children": [ + "f-11690014363617800052", + "Cons-3596314701178032507" + ], + "eclass": "51", + "cost": 1.0 + }, + "g-0": { + "op": "g", + "children": [ + "x-0" + ], + "eclass": "1", + "cost": 1.0 + }, + "g-11743562013128004906": { + "op": "g", + "children": [ + "x-5871781006564002453" + ], + "eclass": "3", + "cost": 1.0 + }, + "g-5040379952546458196": { + "op": "g", + "children": [ + "x-11743562013128004906" + ], + "eclass": "5", + "cost": 1.0 + }, + "g-16783941965674463102": { + "op": "g", + "children": [ + "x-17615343019692007359" + ], + "eclass": "7", + "cost": 1.0 + }, + "g-10080759905092916392": { + "op": "g", + "children": [ + "x-5040379952546458196" + ], + "eclass": "9", + "cost": 1.0 + }, + "g-3377577844511369682": { + "op": "g", + "children": [ + "x-10912160959110460649" + ], + "eclass": "11", + "cost": 1.0 + }, + "g-15121139857639374588": { + "op": "g", + "children": [ + "x-16783941965674463102" + ], + "eclass": "13", + "cost": 1.0 + }, + "g-8417957797057827878": { + "op": "g", + "children": [ + "x-4208978898528913939" + ], + "eclass": "15", + "cost": 1.0 + }, + "g-1714775736476281168": { + "op": "g", + "children": [ + "x-10080759905092916392" + ], + "eclass": "17", + "cost": 1.0 + }, + "g-13458337749604286074": { + "op": "g", + "children": [ + "x-15952540911656918845" + ], + "eclass": "19", + "cost": 1.0 + }, + "g-6755155689022739364": { + "op": "g", + "children": [ + "x-3377577844511369682" + ], + "eclass": "21", + "cost": 1.0 + }, + "g-51973628441192654": { + "op": "g", + "children": [ + "x-9249358851075372135" + ], + "eclass": "23", + "cost": 1.0 + }, + "g-11795535641569197560": { + "op": "g", + "children": [ + "x-15121139857639374588" + ], + "eclass": "25", + "cost": 1.0 + }, + "g-5092353580987650850": { + "op": "g", + "children": [ + "x-2546176790493825425" + ], + "eclass": "27", + "cost": 1.0 + }, + "g-16835915594115655756": { + "op": "g", + "children": [ + "x-8417957797057827878" + ], + "eclass": "29", + "cost": 1.0 + }, + "g-10132733533534109046": { + "op": "g", + "children": [ + "x-14289738803621830331" + ], + "eclass": "31", + "cost": 1.0 + }, + "g-3429551472952562336": { + "op": "g", + "children": [ + "x-1714775736476281168" + ], + "eclass": "33", + "cost": 1.0 + }, + "A-0": { + "op": "A", + "children": [], + "eclass": "52", + "cost": 1.0 + }, + "f-14404162188104689347": { + "op": "f", + "children": [ + "i64-1714775736476281168", + "A-0", + "B-0" + ], + "eclass": "33", + "cost": 1.0 + }, + "f-10841857528096821280": { + "op": "f", + "children": [ + "i64-14289738803621830331", + "A-0", + "B-0" + ], + "eclass": "31", + "cost": 1.0 + }, + "f-2696893396811418316": { + "op": "f", + "children": [ + "i64-3377577844511369682", + "A-0", + "B-0" + ], + "eclass": "21", + "cost": 1.0 + }, + "f-17541124554704762424": { + "op": "f", + "children": [ + "i64-15952540911656918845", + "A-0", + "B-0" + ], + "eclass": "19", + "cost": 1.0 + }, + "f-16215055113516144691": { + "op": "f", + "children": [ + "i64-5040379952546458196", + "A-0", + "B-0" + ], + "eclass": "9", + "cost": 1.0 + }, + "f-13628307020216545630": { + "op": "f", + "children": [ + "i64-17615343019692007359", + "A-0", + "B-0" + ], + "eclass": "7", + "cost": 1.0 + }, + "f-12439173641694160734": { + "op": "f", + "children": [ + "i64-8417957797057827878", + "A-0", + "B-0" + ], + "eclass": "29", + "cost": 1.0 + }, + "f-17346800407185313199": { + "op": "f", + "children": [ + "i64-2546176790493825425", + "A-0", + "B-0" + ], + "eclass": "27", + "cost": 1.0 + }, + "f-5073273888987675178": { + "op": "f", + "children": [ + "i64-10080759905092916392", + "A-0", + "B-0" + ], + "eclass": "17", + "cost": 1.0 + }, + "f-2169771887131140391": { + "op": "f", + "children": [ + "i64-4208978898528913939", + "A-0", + "B-0" + ], + "eclass": "15", + "cost": 1.0 + }, + "f-12955991996068655944": { + "op": "f", + "children": [ + "i64-11743562013128004906", + "A-0", + "B-0" + ], + "eclass": "5", + "cost": 1.0 + }, + "f-14077105124241970906": { + "op": "f", + "children": [ + "i64-5871781006564002453", + "A-0", + "B-0" + ], + "eclass": "3", + "cost": 1.0 + }, + "f-9047720384188800451": { + "op": "f", + "children": [ + "i64-15121139857639374588", + "A-0", + "B-0" + ], + "eclass": "25", + "cost": 1.0 + }, + "f-11357196730744934837": { + "op": "f", + "children": [ + "i64-9249358851075372135", + "A-0", + "B-0" + ], + "eclass": "23", + "cost": 1.0 + }, + "f-3212232599459531873": { + "op": "f", + "children": [ + "i64-16783941965674463102", + "A-0", + "B-0" + ], + "eclass": "13", + "cost": 1.0 + }, + "f-15593295566627074243": { + "op": "f", + "children": [ + "i64-10912160959110460649", + "A-0", + "B-0" + ], + "eclass": "11", + "cost": 1.0 + }, + "f-11690014363617800052": { + "op": "f", + "children": [ + "i64-0", + "A-0", + "B-0" + ], + "eclass": "1", + "cost": 1.0 + }, + "Nil-0": { + "op": "Nil", + "children": [], + "eclass": "34", + "cost": 1.0 + } + }, + "root_eclasses": [ + "51" + ], + "class_data": { + "53": { + "type": "Term" + }, + "0": { + "type": "Term" + }, + "i64-0": { + "type": "i64" + }, + "2": { + "type": "Term" + }, + "i64-5871781006564002453": { + "type": "i64" + }, + "4": { + "type": "Term" + }, + "i64-11743562013128004906": { + "type": "i64" + }, + "6": { + "type": "Term" + }, + "i64-17615343019692007359": { + "type": "i64" + }, + "8": { + "type": "Term" + }, + "i64-5040379952546458196": { + "type": "i64" + }, + "10": { + "type": "Term" + }, + "i64-10912160959110460649": { + "type": "i64" + }, + "12": { + "type": "Term" + }, + "i64-16783941965674463102": { + "type": "i64" + }, + "14": { + "type": "Term" + }, + "i64-4208978898528913939": { + "type": "i64" + }, + "16": { + "type": "Term" + }, + "i64-10080759905092916392": { + "type": "i64" + }, + "18": { + "type": "Term" + }, + "i64-15952540911656918845": { + "type": "i64" + }, + "20": { + "type": "Term" + }, + "i64-3377577844511369682": { + "type": "i64" + }, + "22": { + "type": "Term" + }, + "i64-9249358851075372135": { + "type": "i64" + }, + "24": { + "type": "Term" + }, + "i64-15121139857639374588": { + "type": "i64" + }, + "26": { + "type": "Term" + }, + "i64-2546176790493825425": { + "type": "i64" + }, + "28": { + "type": "Term" + }, + "i64-8417957797057827878": { + "type": "i64" + }, + "30": { + "type": "Term" + }, + "i64-14289738803621830331": { + "type": "i64" + }, + "32": { + "type": "Term" + }, + "i64-1714775736476281168": { + "type": "i64" + }, + "35": { + "type": "Term" + }, + "33": { + "type": "Term" + }, + "34": { + "type": "Term" + }, + "36": { + "type": "Term" + }, + "31": { + "type": "Term" + }, + "37": { + "type": "Term" + }, + "29": { + "type": "Term" + }, + "38": { + "type": "Term" + }, + "27": { + "type": "Term" + }, + "39": { + "type": "Term" + }, + "25": { + "type": "Term" + }, + "40": { + "type": "Term" + }, + "23": { + "type": "Term" + }, + "41": { + "type": "Term" + }, + "21": { + "type": "Term" + }, + "42": { + "type": "Term" + }, + "19": { + "type": "Term" + }, + "43": { + "type": "Term" + }, + "17": { + "type": "Term" + }, + "44": { + "type": "Term" + }, + "15": { + "type": "Term" + }, + "45": { + "type": "Term" + }, + "13": { + "type": "Term" + }, + "46": { + "type": "Term" + }, + "11": { + "type": "Term" + }, + "47": { + "type": "Term" + }, + "9": { + "type": "Term" + }, + "48": { + "type": "Term" + }, + "7": { + "type": "Term" + }, + "49": { + "type": "Term" + }, + "5": { + "type": "Term" + }, + "50": { + "type": "Term" + }, + "3": { + "type": "Term" + }, + "51": { + "type": "Term" + }, + "1": { + "type": "Term" + }, + "52": { + "type": "Term" + } + } +} \ No newline at end of file diff --git a/data/dummy_examples/loop.egg b/data/dummy_examples/loop.egg index 0c1e8b4..709ba50 100644 --- a/data/dummy_examples/loop.egg +++ b/data/dummy_examples/loop.egg @@ -7,7 +7,7 @@ ; We pick enode e = (Mul (One) e) -(define t +(let t (Mul (One) (foo (foo (foo (foo (One)))) ))) (run 1) diff --git a/data/dummy_examples/loop.json b/data/dummy_examples/loop.json index 92e4fc7..bfcf051 100644 --- a/data/dummy_examples/loop.json +++ b/data/dummy_examples/loop.json @@ -1,113 +1,71 @@ { - "nodes": { - "v2___-0": { - "op": "v2___", - "children": [], - "eclass": "5", - "cost": 9.223372036854776e18 - }, - "t-0": { - "op": "t", - "children": [], - "eclass": "5", - "cost": 9.223372036854776e18 - }, - "v1___-0": { - "op": "v1___", - "children": [], - "eclass": "0", - "cost": 9.223372036854776e18 - }, - "v3___-0": { - "op": "v3___", - "children": [], - "eclass": "3", - "cost": 9.223372036854776e18 - }, - "One-0": { - "op": "One", - "children": [], - "eclass": "0", - "cost": 1.0 - }, - "v4___-0": { - "op": "v4___", - "children": [], - "eclass": "2", - "cost": 9.223372036854776e18 - }, - "foo-0": { - "op": "foo", - "children": [ - "One-0" - ], - "eclass": "1", - "cost": 1.0 - }, - "foo-5871781006564002453": { - "op": "foo", - "children": [ - "foo-0" - ], - "eclass": "2", - "cost": 1.0 - }, - "foo-11743562013128004906": { - "op": "foo", - "children": [ - "foo-5871781006564002453" - ], - "eclass": "3", - "cost": 1.0 - }, - "foo-17615343019692007359": { - "op": "foo", - "children": [ - "foo-11743562013128004906" - ], - "eclass": "5", - "cost": 1.0 - }, - "v0___-0": { - "op": "v0___", - "children": [], - "eclass": "5", - "cost": 9.223372036854776e18 - }, - "v5___-0": { - "op": "v5___", - "children": [], - "eclass": "1", - "cost": 9.223372036854776e18 - }, - "Mul-10912160959110460649": { - "op": "Mul", - "children": [ - "v1___-0", - "t-0" - ], - "eclass": "5", - "cost": 1.0 - } + "nodes": { + "Mul-5040379952546458196": { + "op": "Mul", + "children": [ + "One-0", + "Mul-5040379952546458196" + ], + "eclass": "5", + "cost": 1.0 }, - "root_eclasses": [ - "5" - ], - "class_data": { - "5": { - "type": "Math" - }, - "0": { - "type": "Math" - }, - "3": { - "type": "Math" - }, - "2": { - "type": "Math" - }, - "1": { - "type": "Math" - } + "One-0": { + "op": "One", + "children": [], + "eclass": "0", + "cost": 1.0 + }, + "foo-0": { + "op": "foo", + "children": [ + "One-0" + ], + "eclass": "1", + "cost": 1.0 + }, + "foo-5871781006564002453": { + "op": "foo", + "children": [ + "foo-0" + ], + "eclass": "2", + "cost": 1.0 + }, + "foo-11743562013128004906": { + "op": "foo", + "children": [ + "foo-5871781006564002453" + ], + "eclass": "3", + "cost": 1.0 + }, + "foo-17615343019692007359": { + "op": "foo", + "children": [ + "foo-11743562013128004906" + ], + "eclass": "5", + "cost": 1.0 + } + }, + "root_eclasses": [ + "5" + ], + "class_data": { + "5": { + "type": "Math" + }, + "0": { + "type": "Math" + }, + "1": { + "type": "Math" + }, + "2": { + "type": "Math" + }, + "3": { + "type": "Math" } + } } \ No newline at end of file