diff --git a/Cargo.lock b/Cargo.lock
index 2e59466..00f8f19 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -101,14 +101,15 @@ dependencies = [
"rand",
"rpds",
"rustc-hash",
+ "serde_json",
"walkdir",
]
[[package]]
name = "getrandom"
-version = "0.2.11"
+version = "0.2.12"
source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "fe9006bed769170c11f845cf00c7c1e9092aeb3f268e007c3e760ac68008070f"
+checksum = "190092ea657667030ac6a35e305e62fc4dd69fd98ac98631e5d3a2b1575a12b5"
dependencies = [
"cfg-if",
"libc",
@@ -160,9 +161,9 @@ checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646"
[[package]]
name = "libc"
-version = "0.2.151"
+version = "0.2.152"
source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "302d7ab3130588088d277783b1e2d2e10c9e9e4a16dd9050e6ec93fb3e7048f4"
+checksum = "13e3bf6590cbc649f4d1a3eefc9d5d6eb746f5200ffb04e5e142700b8faa56e7"
[[package]]
name = "log"
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
new file mode 100644
index 0000000..1b42c72
--- /dev/null
+++ b/data/dummy_examples/ab_add.egg
@@ -0,0 +1,16 @@
+(datatype Math (Add Math Math) (A) (B))
+
+(birewrite (Add a (Add b c)) (Add (Add a b) c))
+(rewrite (Add a b) (Add b a))
+
+; Tree extraction does not care about associativity or ordering
+; 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
+(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
new file mode 100644
index 0000000..6f9a03c
--- /dev/null
+++ b/data/dummy_examples/ab_add.json
@@ -0,0 +1,445 @@
+{
+ "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
new file mode 100644
index 0000000..ea48c77
--- /dev/null
+++ b/data/dummy_examples/choice.egg
@@ -0,0 +1,32 @@
+(datatype Term (f i64 Term Term) (g Term) (x i64) (A) (B) (Cons Term Term) (Nil))
+
+(rewrite (g (x n)) (f n (A) (B)))
+
+; At every node, we have a binary choice of (g (x n)) : cost 2 or (f n A B) : cost 3 (integers have cost 0)
+; 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
+(let t
+ (Cons (g (x 0))
+ (Cons (g (x 1))
+ (Cons (g (x 2))
+ (Cons (g (x 3))
+ (Cons (g (x 4))
+ (Cons (g (x 5))
+ (Cons (g (x 6))
+ (Cons (g (x 7))
+ (Cons (g (x 8))
+ (Cons (g (x 9))
+ (Cons (g (x 10))
+ (Cons (g (x 11))
+ (Cons (g (x 12))
+ (Cons (g (x 13))
+ (Cons (g (x 14))
+ (Cons (g (x 15))
+ (Cons (g (x 16))
+ (Nil)
+))))))))))))))))))
+(run 10)
+
+
+
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
new file mode 100644
index 0000000..709ba50
--- /dev/null
+++ b/data/dummy_examples/loop.egg
@@ -0,0 +1,14 @@
+(datatype Math (One) (Mul Math Math) (foo Math))
+
+(rewrite (Mul One x) x)
+
+; An example to demonstrate loop breaking.
+; Without loop constraint, recursive term 1*1*1*1*.... is best.
+; We pick enode e = (Mul (One) e)
+
+
+(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
new file mode 100644
index 0000000..bfcf051
--- /dev/null
+++ b/data/dummy_examples/loop.json
@@ -0,0 +1,71 @@
+{
+ "nodes": {
+ "Mul-5040379952546458196": {
+ "op": "Mul",
+ "children": [
+ "One-0",
+ "Mul-5040379952546458196"
+ ],
+ "eclass": "5",
+ "cost": 1.0
+ },
+ "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
diff --git a/src/extract/ilp_cbc.rs b/src/extract/ilp_cbc.rs
index 90e7462..82522bd 100644
--- a/src/extract/ilp_cbc.rs
+++ b/src/extract/ilp_cbc.rs
@@ -5,9 +5,6 @@ This extractor is simple so that it's easy to see that it's correct.
If the timeout is reached, it will return the result of the faster-greedy-dag extractor.
*/
-// Without a timeout, some will take > 10 hours to finish.
-const SOLVING_TIME_LIMIT_SECONDS: u64 = 10;
-
use super::*;
use coin_cbc::{Col, Model, Sense};
use indexmap::IndexSet;
@@ -17,115 +14,146 @@ struct ClassVars {
nodes: Vec,
}
+pub struct CbcExtractorWithTimeout;
+
+impl Extractor for CbcExtractorWithTimeout {
+ fn extract(&self, egraph: &EGraph, roots: &[ClassId]) -> ExtractionResult {
+ return extract(egraph, roots, TIMEOUT_IN_SECONDS);
+ }
+}
+
pub struct CbcExtractor;
impl Extractor for CbcExtractor {
fn extract(&self, egraph: &EGraph, roots: &[ClassId]) -> ExtractionResult {
- let mut model = Model::default();
-
- model.set_parameter("seconds", &SOLVING_TIME_LIMIT_SECONDS.to_string());
-
- let vars: IndexMap = egraph
- .classes()
- .values()
- .map(|class| {
- let cvars = ClassVars {
- active: model.add_binary(),
- nodes: class.nodes.iter().map(|_| model.add_binary()).collect(),
- };
- (class.id.clone(), cvars)
- })
- .collect();
-
- for (class_id, class) in &vars {
- // class active == some node active
- // sum(for node_active in class) == class_active
- let row = model.add_row();
- model.set_row_equal(row, 0.0);
- model.set_weight(row, class.active, -1.0);
- for &node_active in &class.nodes {
- model.set_weight(row, node_active, 1.0);
- }
+ return extract(egraph, roots, std::u32::MAX);
+ }
+}
+
+fn extract(egraph: &EGraph, roots: &[ClassId], timeout_seconds: u32) -> ExtractionResult {
+ let mut model = Model::default();
+
+ model.set_parameter("seconds", &timeout_seconds.to_string());
- let childrens_classes_var = |nid: NodeId| {
- egraph[&nid]
- .children
- .iter()
- .map(|n| egraph[n].eclass.clone())
- .map(|n| vars[&n].active)
- .collect::>()
+ let vars: IndexMap = egraph
+ .classes()
+ .values()
+ .map(|class| {
+ let cvars = ClassVars {
+ active: model.add_binary(),
+ nodes: class.nodes.iter().map(|_| model.add_binary()).collect(),
};
+ (class.id.clone(), cvars)
+ })
+ .collect();
+
+ for (class_id, class) in &vars {
+ // class active == some node active
+ // sum(for node_active in class) == class_active
+ let row = model.add_row();
+ model.set_row_equal(row, 0.0);
+ model.set_weight(row, class.active, -1.0);
+ for &node_active in &class.nodes {
+ model.set_weight(row, node_active, 1.0);
+ }
- for (node_id, &node_active) in egraph[class_id].nodes.iter().zip(&class.nodes) {
- for child_active in childrens_classes_var(node_id.clone()) {
- // node active implies child active, encoded as:
- // node_active <= child_active
- // node_active - child_active <= 0
- let row = model.add_row();
- model.set_row_upper(row, 0.0);
- model.set_weight(row, node_active, 1.0);
- model.set_weight(row, child_active, -1.0);
- }
+ let childrens_classes_var = |nid: NodeId| {
+ egraph[&nid]
+ .children
+ .iter()
+ .map(|n| egraph[n].eclass.clone())
+ .map(|n| vars[&n].active)
+ .collect::>()
+ };
+
+ for (node_id, &node_active) in egraph[class_id].nodes.iter().zip(&class.nodes) {
+ for child_active in childrens_classes_var(node_id.clone()) {
+ // node active implies child active, encoded as:
+ // node_active <= child_active
+ // node_active - child_active <= 0
+ let row = model.add_row();
+ model.set_row_upper(row, 0.0);
+ model.set_weight(row, node_active, 1.0);
+ model.set_weight(row, child_active, -1.0);
}
}
+ }
- model.set_obj_sense(Sense::Minimize);
- for class in egraph.classes().values() {
- for (node_id, &node_active) in class.nodes.iter().zip(&vars[&class.id].nodes) {
- let node = &egraph[node_id];
- let node_cost = node.cost.into_inner();
- assert!(node_cost >= 0.0);
+ model.set_obj_sense(Sense::Minimize);
+ for class in egraph.classes().values() {
+ for (node_id, &node_active) in class.nodes.iter().zip(&vars[&class.id].nodes) {
+ let node = &egraph[node_id];
+ let node_cost = node.cost.into_inner();
+ assert!(node_cost >= 0.0);
- if node_cost != 0.0 {
- model.set_obj_coeff(node_active, node_cost);
- }
+ if node_cost != 0.0 {
+ model.set_obj_coeff(node_active, node_cost);
}
}
+ }
- for root in roots {
- model.set_col_lower(vars[root].active, 1.0);
- }
+ for root in roots {
+ model.set_col_lower(vars[root].active, 1.0);
+ }
- block_cycles(&mut model, &vars, &egraph);
-
- let solution = model.solve();
- log::info!(
- "CBC status {:?}, {:?}, obj = {}",
- solution.raw().status(),
- solution.raw().secondary_status(),
- solution.raw().obj_value(),
- );
-
- if solution.raw().status() != coin_cbc::raw::Status::Finished {
- let initial_result =
- super::faster_greedy_dag::FasterGreedyDagExtractor.extract(egraph, roots);
- log::info!("Unfinished CBC solution");
- return initial_result;
- }
+ block_cycles(&mut model, &vars, &egraph);
- let mut result = ExtractionResult::default();
-
- for (id, var) in &vars {
- let active = solution.col(var.active) > 0.0;
- if active {
- let node_idx = var
- .nodes
- .iter()
- .position(|&n| solution.col(n) > 0.0)
- .unwrap();
- let node_id = egraph[id].nodes[node_idx].clone();
- result.choose(id.clone(), node_id);
- }
- }
+ let solution = model.solve();
+ log::info!(
+ "CBC status {:?}, {:?}, obj = {}",
+ solution.raw().status(),
+ solution.raw().secondary_status(),
+ solution.raw().obj_value(),
+ );
+
+ if solution.raw().status() != coin_cbc::raw::Status::Finished {
+ assert!(timeout_seconds != std::u32::MAX);
- return result;
+ let initial_result =
+ super::faster_greedy_dag::FasterGreedyDagExtractor.extract(egraph, roots);
+ log::info!("Unfinished CBC solution");
+ return initial_result;
}
+
+ let mut result = ExtractionResult::default();
+
+ for (id, var) in &vars {
+ let active = solution.col(var.active) > 0.0;
+ if active {
+ let node_idx = var
+ .nodes
+ .iter()
+ .position(|&n| solution.col(n) > 0.0)
+ .unwrap();
+ let node_id = egraph[id].nodes[node_idx].clone();
+ result.choose(id.clone(), node_id);
+ }
+ }
+
+ return result;
}
+/*
+
+ To block cycles, we enforce that a topological ordering exists on the extraction.
+ Each class is mapped to a variable (called its level). Then for each node,
+ we add a constraint that if a node is active, then the level of the class the node
+ belongs to must be less than than the level of each of the node's children.
+
+ To create a cycle, the levels would need to decrease, so they're blocked. For example,
+ given a two class cycle: if class A, has level 'l', and class B has level 'm', then
+ 'l' must be less than 'm', but because there is also an active node in class B that
+ has class A as a child, 'm' must be less than 'l', which is a contradiction.
+*/
+
fn block_cycles(model: &mut Model, vars: &IndexMap, egraph: &EGraph) {
let mut levels: IndexMap = Default::default();
for c in vars.keys() {
- levels.insert(c.clone(), model.add_integer());
+ let var = model.add_col();
+ levels.insert(c.clone(), var);
+ //model.set_col_lower(var, 0.0);
+ // It solves the benchmarks about 5% faster without this
+ //model.set_col_upper(var, vars.len() as f64);
}
// If n.variable is true, opposite_col will be false and vice versa.
@@ -142,9 +170,6 @@ fn block_cycles(model: &mut Model, vars: &IndexMap, egraph:
}
for (class_id, c) in vars {
- model.set_col_lower(*levels.get(class_id).unwrap(), 0.0);
- model.set_col_upper(*levels.get(class_id).unwrap(), vars.len() as f64);
-
for i in 0..c.nodes.len() {
let n_id = &egraph[class_id].nodes[i];
let n = &egraph[n_id];
@@ -171,16 +196,12 @@ fn block_cycles(model: &mut Model, vars: &IndexMap, egraph:
assert!(*levels.get(class_id).unwrap() != *levels.get(&cc).unwrap());
let row = model.add_row();
- model.set_row_upper(row, -1.0);
- model.set_weight(row, *levels.get(class_id).unwrap(), 1.0);
- model.set_weight(row, *levels.get(&cc).unwrap(), -1.0);
+ model.set_row_lower(row, 1.0);
+ model.set_weight(row, *levels.get(class_id).unwrap(), -1.0);
+ model.set_weight(row, *levels.get(&cc).unwrap(), 1.0);
// If n.variable is 0, then disable the contraint.
- model.set_weight(
- row,
- *opposite.get(&var).unwrap(),
- -((vars.len() + 1) as f64),
- );
+ model.set_weight(row, *opposite.get(&var).unwrap(), (vars.len() + 1) as f64);
}
}
}
diff --git a/src/main.rs b/src/main.rs
index 58f065b..ae13a52 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -109,6 +109,11 @@ fn extractors() -> IndexMap<&'static str, ExtractorDetail> {
use_for_bench: false, // takes >10 hours sometimes
},
),
+ #[cfg(feature = "ilp-cbc")]
+ (
+ "ilp-cbc-timeout",
+ extract::ilp_cbc::CbcExtractorWithTimeout::<10>.boxed(),
+ ),
]
.into_iter()
.collect();