From 84d67bf2a5d361a4529eff932a059cbb58e3017f Mon Sep 17 00:00:00 2001 From: Trevor Hansen Date: Fri, 12 Jan 2024 11:02:10 +1100 Subject: [PATCH 1/2] ILP-based extractor that produces an optimal dag-cost extraction (#30) * better ilp extractor * Separate extractor with timeout and without timeout * fix build. enable ilp-cbc by default * fix to use ilp-cbc with timeout * Move the timeout to the caller * Removing cbc because I don't have permission to install cbc during github workflow * re-enable global-greedy-dag * add description of how cycles are blocked * Following the suggestion of @mwillsey to use floats rather than integers for the levels * fix layout --- Cargo.lock | 7 + src/extract/ilp_cbc.rs | 381 +++++++++++++++++------------------------ src/main.rs | 5 + 3 files changed, 173 insertions(+), 220 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 46f2e35..707fbcd 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -93,6 +93,7 @@ dependencies = [ "ordered-float", "pico-args", "rpds", + "rustc-hash", ] [[package]] @@ -237,6 +238,12 @@ dependencies = [ "archery", ] +[[package]] +name = "rustc-hash" +version = "1.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "08d43f7aa6b08d49f382cde6a7982047c3426db949b1424bc4b7ec9ae12c6ce2" + [[package]] name = "ryu" version = "1.0.14" diff --git a/src/extract/ilp_cbc.rs b/src/extract/ilp_cbc.rs index c48b04b..82522bd 100644 --- a/src/extract/ilp_cbc.rs +++ b/src/extract/ilp_cbc.rs @@ -1,267 +1,208 @@ -use core::panic; +/* An ILP extractor that returns the optimal DAG-extraction. + +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. +*/ use super::*; use coin_cbc::{Col, Model, Sense}; use indexmap::IndexSet; -const INITIALISE_WITH_BOTTOM_UP: bool = false; - struct ClassVars { active: Col, nodes: Vec, } -pub struct CbcExtractor; +pub struct CbcExtractorWithTimeout; -impl Extractor for CbcExtractor { +impl Extractor for CbcExtractorWithTimeout { fn extract(&self, egraph: &EGraph, roots: &[ClassId]) -> ExtractionResult { - let mut model = Model::default(); - - let true_literal = model.add_binary(); - model.set_col_lower(true_literal, 1.0); - - let vars: IndexMap = egraph - .classes() - .values() - .map(|class| { - let cvars = ClassVars { - active: if roots.contains(&class.id) { - // Roots must be active. - true_literal - } else { - 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, TIMEOUT_IN_SECONDS); + } +} - let childrens_classes_var = |nid: NodeId| { - egraph[&nid] - .children - .iter() - .map(|n| egraph[n].eclass.clone()) - .map(|n| vars[&n].active) - .collect::>() - }; +pub struct CbcExtractor; - let mut intersection: IndexSet = - childrens_classes_var(egraph[class_id].nodes[0].clone()); +impl Extractor for CbcExtractor { + fn extract(&self, egraph: &EGraph, roots: &[ClassId]) -> ExtractionResult { + return extract(egraph, roots, std::u32::MAX); + } +} - for node in &egraph[class_id].nodes[1..] { - intersection = intersection - .intersection(&childrens_classes_var(node.clone())) - .cloned() - .collect(); - } +fn extract(egraph: &EGraph, roots: &[ClassId], timeout_seconds: u32) -> ExtractionResult { + let mut model = Model::default(); - // A class being active implies that all in the intersection - // of it's children are too. - for c in &intersection { - let row = model.add_row(); - model.set_row_upper(row, 0.0); - model.set_weight(row, class.active, 1.0); - model.set_weight(row, *c, -1.0); - } + model.set_parameter("seconds", &timeout_seconds.to_string()); - 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 - if !intersection.contains(&child_active) { - 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 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); } - model.set_obj_sense(Sense::Minimize); - for class in egraph.classes().values() { - let min_cost = class - .nodes + let childrens_classes_var = |nid: NodeId| { + egraph[&nid] + .children .iter() - .map(|n_id| egraph[n_id].cost) - .min() - .unwrap_or(Cost::default()) - .into_inner(); - - // Most helpful when the members of the class all have the same cost. - // For example if the members' costs are [1,1,1], three terms get - // replaced by one in the objective function. - if min_cost != 0.0 { - model.set_obj_coeff(vars[&class.id].active, min_cost); - } - - 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() - min_cost; - assert!(node_cost >= 0.0); - - if node_cost != 0.0 { - model.set_obj_coeff(node_active, node_cost); - } + .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); } } + } - // set initial solution based on bottom up extractor - if INITIALISE_WITH_BOTTOM_UP { - let initial_result = super::bottom_up::BottomUpExtractor.extract(egraph, roots); - for (class, class_vars) in egraph.classes().values().zip(vars.values()) { - if let Some(node_id) = initial_result.choices.get(&class.id) { - model.set_col_initial_solution(class_vars.active, 1.0); - for col in &class_vars.nodes { - model.set_col_initial_solution(*col, 0.0); - } - let node_idx = class.nodes.iter().position(|n| n == node_id).unwrap(); - model.set_col_initial_solution(class_vars.nodes[node_idx], 1.0); - } else { - model.set_col_initial_solution(class_vars.active, 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); - let mut banned_cycles: IndexSet<(ClassId, usize)> = Default::default(); - find_cycles(egraph, |id, i| { - banned_cycles.insert((id, i)); - }); - for (class_id, class_vars) in &vars { - for (i, &node_active) in class_vars.nodes.iter().enumerate() { - if banned_cycles.contains(&(class_id.clone(), i)) { - model.set_col_upper(node_active, 0.0); - model.set_col_lower(node_active, 0.0); - } - } - } - log::info!("@blocked {}", banned_cycles.len()); - - let solution = model.solve(); - log::info!( - "CBC status {:?}, {:?}, obj = {}", - solution.raw().status(), - solution.raw().secondary_status(), - solution.raw().obj_value(), - ); - - 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); + if node_cost != 0.0 { + model.set_obj_coeff(node_active, node_cost); } } - - let cycles = result.find_cycles(egraph, roots); - assert!(cycles.is_empty()); - return result; } -} -// from @khaki3 -// fixes bug in egg 0.9.4's version -// https://github.com/egraphs-good/egg/issues/207#issuecomment-1264737441 -fn find_cycles(egraph: &EGraph, mut f: impl FnMut(ClassId, usize)) { - let mut pending: IndexMap> = IndexMap::default(); + for root in roots { + model.set_col_lower(vars[root].active, 1.0); + } - let mut order: IndexMap = IndexMap::default(); + block_cycles(&mut model, &vars, &egraph); - let mut memo: IndexMap<(ClassId, usize), bool> = IndexMap::default(); + let solution = model.solve(); + log::info!( + "CBC status {:?}, {:?}, obj = {}", + solution.raw().status(), + solution.raw().secondary_status(), + solution.raw().obj_value(), + ); - let mut stack: Vec<(ClassId, usize)> = vec![]; + if solution.raw().status() != coin_cbc::raw::Status::Finished { + assert!(timeout_seconds != std::u32::MAX); - let n2c = |nid: &NodeId| egraph.nid_to_cid(nid); + let initial_result = + super::faster_greedy_dag::FasterGreedyDagExtractor.extract(egraph, roots); + log::info!("Unfinished CBC solution"); + return initial_result; + } - for class in egraph.classes().values() { - let id = &class.id; - for (i, node_id) in egraph[id].nodes.iter().enumerate() { - let node = &egraph[node_id]; - for child in &node.children { - let child = n2c(child).clone(); - pending - .entry(child) - .or_insert_with(Vec::new) - .push((id.clone(), i)); - } + let mut result = ExtractionResult::default(); - if node.is_leaf() { - stack.push((id.clone(), i)); - } + 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 mut count = 0; - - while let Some((id, i)) = stack.pop() { - if memo.get(&(id.clone(), i)).is_some() { - continue; - } + return result; +} - let node_id = &egraph[&id].nodes[i]; - let node = &egraph[node_id]; - let mut update = false; - - if node.is_leaf() { - update = true; - } else if node.children.iter().all(|x| order.get(n2c(x)).is_some()) { - if let Some(ord) = order.get(&id) { - update = node.children.iter().all(|x| &order[n2c(x)] < ord); - if !update { - memo.insert((id, i), false); - continue; - } - } else { - update = true; - } - } +/* + + 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() { + 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 update { - if order.get(&id).is_none() { - if egraph[node_id].is_leaf() { - order.insert(id.clone(), 0); - } else { - order.insert(id.clone(), count); - count += 1; - } - } - memo.insert((id.clone(), i), true); - if let Some(mut v) = pending.remove(&id) { - stack.append(&mut v); - stack.sort(); - stack.dedup(); - }; + // If n.variable is true, opposite_col will be false and vice versa. + let mut opposite: IndexMap = Default::default(); + for c in vars.values() { + for n in &c.nodes { + let opposite_col = model.add_binary(); + opposite.insert(*n, opposite_col); + let row = model.add_row(); + model.set_row_equal(row, 1.0); + model.set_weight(row, opposite_col, 1.0); + model.set_weight(row, *n, 1.0); } } - for class in egraph.classes().values() { - let id = &class.id; - for (i, node) in class.nodes.iter().enumerate() { - if let Some(true) = memo.get(&(id.clone(), i)) { + for (class_id, c) in vars { + for i in 0..c.nodes.len() { + let n_id = &egraph[class_id].nodes[i]; + let n = &egraph[n_id]; + let var = c.nodes[i]; + + let children_classes = n + .children + .iter() + .map(|n| egraph[n].eclass.clone()) + .collect::>(); + + if children_classes.contains(class_id) { + // Self loop - disable this node. + // This is clumsier than calling set_col_lower(var,0.0), + // but means it'll be infeasible (rather than producing an + // incorrect solution) if var corresponds to a root node. + let row = model.add_row(); + model.set_weight(row, var, 1.0); + model.set_row_equal(row, 0.0); continue; } - assert!(!egraph[node].is_leaf()); - f(id.clone(), i); + + for cc in children_classes { + assert!(*levels.get(class_id).unwrap() != *levels.get(&cc).unwrap()); + + let row = model.add_row(); + 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); + } } } - assert!(pending.is_empty()); } diff --git a/src/main.rs b/src/main.rs index bddc552..fab1624 100644 --- a/src/main.rs +++ b/src/main.rs @@ -36,6 +36,11 @@ fn main() { "global-greedy-dag", extract::global_greedy_dag::GlobalGreedyDagExtractor.boxed(), ), + #[cfg(feature = "ilp-cbc")] + ( + "ilp-cbc-timeout", + extract::ilp_cbc::CbcExtractorWithTimeout::<10>.boxed(), + ), ] .into_iter() .collect(); From c04b7fcc53aae9b0c00284e40c5af05fa9a11983 Mon Sep 17 00:00:00 2001 From: Philip Zucker Date: Fri, 12 Jan 2024 14:49:57 -0500 Subject: [PATCH 2/2] Add Simple Examples (#6) * handwritten examples~ * fixed root * something is wrong with the dump of choice.egg * Update dummy data from egglog --------- Co-authored-by: Max Willsey --- data/dummy_examples/Makefile | 15 + data/dummy_examples/ab_add.egg | 16 + data/dummy_examples/ab_add.json | 445 +++++++++++++++ data/dummy_examples/choice.egg | 32 ++ data/dummy_examples/choice.json | 937 ++++++++++++++++++++++++++++++++ data/dummy_examples/loop.egg | 14 + data/dummy_examples/loop.json | 71 +++ 7 files changed, 1530 insertions(+) create mode 100644 data/dummy_examples/Makefile create mode 100644 data/dummy_examples/ab_add.egg create mode 100644 data/dummy_examples/ab_add.json create mode 100644 data/dummy_examples/choice.egg create mode 100644 data/dummy_examples/choice.json create mode 100644 data/dummy_examples/loop.egg create mode 100644 data/dummy_examples/loop.json 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