From 28ad2d20f8dc45f32462eb5f7a3151bf34cc44a2 Mon Sep 17 00:00:00 2001 From: AD1024 Date: Tue, 28 Feb 2023 01:02:01 -0500 Subject: [PATCH 01/18] fix some big --- flexmatch/src/main.rs | 100 ++----- flexmatch/src/maxsat_extract.rs | 493 ++++++++++++++++++++++++++++++++ flexmatch/src/mod.rs | 3 +- flexmatch/test.sh | 1 + tests/validate_compilation.py | 8 +- 5 files changed, 530 insertions(+), 75 deletions(-) create mode 100644 flexmatch/src/maxsat_extract.rs create mode 100644 flexmatch/test.sh diff --git a/flexmatch/src/main.rs b/flexmatch/src/main.rs index 9e0cb3b..76c6c17 100644 --- a/flexmatch/src/main.rs +++ b/flexmatch/src/main.rs @@ -1,3 +1,4 @@ +mod maxsat_extract; mod rewrites; use egg::{EGraph, Extractor, Language, Runner}; @@ -5,6 +6,7 @@ use glenside::{ extraction::AcceleratorCostFunction, language::{serialize_analysis_data, MyAnalysis, MyAnalysisData, RelayOperator}, }; +use maxsat_extract::*; use rewrites::{get_rewrite_from_string, im2col_rewrites, linear_rewrites}; use serde::Deserialize; use serde_json; @@ -220,72 +222,30 @@ fn main() { &best, ); } else { - // The following extraction strategy is borrowed from Glenside ISCA demo - /* - #[cfg(feature = "cplex")] - { - use rplex::*; - info!("Extraction with ILP solver"); - let mut cplex_env = Env::new().unwrap(); - cplex_env.set_param(EnvParam::ScreenOutput(true)).unwrap(); - cplex_env - .set_param(EnvParam::MIPLimitsSolutions(1)) - .unwrap(); - // Deterministic time limit in "ticks" - cplex_env - .set_param(EnvParam::DetTimeLimit(6000000.0)) - .unwrap(); - let mut model = glenside::extraction::ilp::create_generic_egraph_lp_model( - &cplex_env, - &runner.egraph, - |node, id, egraph| true && filter_nodes(node, id, egraph), - &[root_expr], - "ilp-extraction", - ); - let mut costs = Constraint::new( - ConstraintType::Eq, /*ignored*/ - 0.0, /*ignored*/ - "costs", - ); - for (_, var) in model.bq_vars.iter() { - costs.add_wvar(WeightedVariable::new_idx(*var, 1.0)); + struct Costfn; + impl MaxsatCostFunction for Costfn { + fn node_cost( + &mut self, + egraph: &EGraph, + eclass: egg::Id, + enode: &glenside::language::Language, + ) -> f64 { + return get_node_weights(enode, egraph.total_size() as f64); } - for (_, var) in model.topo_sort_vars.iter() { - costs.add_wvar(WeightedVariable::new_idx(*var, 0.0)); - } - for (&node, var) in model.bn_vars.iter() { - let weight = get_node_weights(node, runner.egraph.total_size() as f64); - costs.add_wvar(WeightedVariable::new_idx(*var, weight)); - } - model - .problem - .set_objective(ObjectiveType::Minimize, costs) - .unwrap(); - info!("objective set"); - - info!("ilp problem created, beginning solving..."); - let result = model.problem.solve().unwrap(); - info!("ilp problem solved"); - - let (expr, _old_id_to_new_id_map) = - glenside::extraction::ilp::extract_single_expression( - &model, - &result.variables, - EGraph::new(MyAnalysis { - name_to_shape: env.clone(), - name_to_dtype: dtype_info.iter().cloned().collect(), - }), - ); - let mut rec_expr = egg::RecExpr::default(); - save_egraph_as_recexpr(&expr, &mut rec_expr); - save_expr_and_analysis( - output_file, - analysis_data_file, - &env, - &dtype_info.iter().cloned().collect(), - &rec_expr, - ); - } */ + } + let mut maxsat_ext = MaxsatExtractor::new(&runner.egraph, "problem.wcnf".into()); + let mut problem = maxsat_ext.create_problem(root_expr, "problem", true, Costfn); + let (solve_time, cost, best) = problem.solve_with_refinement(); + // println!("{}", best); + println!("Solve time: {}", solve_time); + println!("Cost: {}", cost.unwrap()); + save_expr_and_analysis( + output_file, + analysis_data_file, + &env, + &dtype_info.into_iter().collect(), + &best, + ); } } } @@ -305,7 +265,7 @@ fn get_node_weights(node: &glenside::language::Language, total_size: f64) -> f64 debug!("Accelerator-call encountered"); } match node { - glenside::language::Language::AcceleratorCall(_) => -total_size * 10.0, + glenside::language::Language::AcceleratorCall(_) => 1.0, glenside::language::Language::List(_) | glenside::language::Language::Shape(_) | glenside::language::Language::RelayKernelLayout(_) @@ -322,7 +282,7 @@ fn get_node_weights(node: &glenside::language::Language, total_size: f64) -> f64 | glenside::language::Language::Literal(_) | glenside::language::Language::AccessLiteral(_) | glenside::language::Language::AccessTensor(_) => 1.0, - glenside::language::Language::RelayOperatorCall(_) => total_size / 100.0, + glenside::language::Language::RelayOperatorCall(_) => 1.0, glenside::language::Language::RelayOperator(_) => 1.0, glenside::language::Language::AccessTranspose(_) | glenside::language::Language::AccessPad(_) @@ -332,13 +292,13 @@ fn get_node_weights(node: &glenside::language::Language, total_size: f64) -> f64 | glenside::language::Language::AccessBroadcast(_) | glenside::language::Language::AccessInsertAxis(_) | glenside::language::Language::AccessSlice(_) - | glenside::language::Language::AccessSqueeze(_) => total_size / 10.0, + | glenside::language::Language::AccessSqueeze(_) => 1.0, glenside::language::Language::Compute(_) | glenside::language::Language::AccessReshape(_) | glenside::language::Language::ComputeType(_) - | glenside::language::Language::AccessPair(_) => total_size, - _ => total_size / 20.0, + | glenside::language::Language::AccessPair(_) => 1.0, + _ => total_size, } } diff --git a/flexmatch/src/maxsat_extract.rs b/flexmatch/src/maxsat_extract.rs new file mode 100644 index 0000000..f842100 --- /dev/null +++ b/flexmatch/src/maxsat_extract.rs @@ -0,0 +1,493 @@ +use std::process::Command; + +use egg::{Analysis, EGraph, Id, Language, RecExpr}; +use std::collections::{HashMap, HashSet}; +use std::time::Instant; + +/// Get all cycles in the given E-Graph +pub fn get_cycles( + egraph: &EGraph, + root: &Id, + path: &mut Vec<(Id, L)>, + vis: &mut HashSet, + cycles: &mut Vec>, + node_vars: &HashMap, +) where + L: Language, + N: Analysis, +{ + assert!( + !vis.contains(root), + "cannot be visited again, should be handled in cycle detection" + ); + assert!(*root == egraph.find(*root)); + vis.insert(*root); + for node in egraph[*root].nodes.iter() { + for ch in node.children() { + if vis.contains(ch) { + // cycle detected + if let Some((idx, _)) = path.iter().enumerate().find(|(_, (id, _))| id == ch) { + let mut subpath = path[idx..].to_vec(); + subpath.push((*root, node.clone())); + cycles.push(subpath.clone()); + } else if ch == root { + // self loop + cycles.push(vec![(*root, node.clone())]) + } + } else { + let mut to_here = path.clone(); + to_here.push((*root, node.clone())); + get_cycles(egraph, ch, &mut to_here, vis, cycles, node_vars); + } + } + } +} + +pub fn get_all_cycles( + egraph: &EGraph, + root: &Id, + parent: Option, + color: &mut HashMap, + path: &Vec<(Id, L)>, + cycles: &mut Vec>, + node_vars: &HashMap, +) where + L: Language, + N: Analysis, +{ + if color.contains_key(root) && color[root] == 2 { + return; + } + if color.contains_key(root) && color[root] == 1 { + let mut new_cycle = Vec::new(); + if let Some((idx, _)) = path.iter().enumerate().find(|(_, (id, _))| id == root) { + let subpath = path[idx..].to_vec(); + for (_, n) in subpath { + new_cycle.push(node_vars[&n]); + } + new_cycle.push(parent.unwrap()); + cycles.push(new_cycle); + return; + } + panic!("Should have a cycle here: {}; path: {:?}", root, path); + } + color.insert(*root, 1); + for node in egraph[*root].nodes.iter() { + for ch in node.children() { + let mut to_here = path.clone(); + to_here.push((*root, node.clone())); + get_all_cycles( + egraph, + ch, + Some(node_vars[node]), + color, + &to_here, + cycles, + node_vars, + ); + } + } + color.insert(*root, 2); +} + +fn cycle_2( + egraph: &EGraph, + root: Id, + length_2_cycle: &mut Vec>, + node_vars: &HashMap, + vis: &mut HashSet, +) where + L: Language, + N: Analysis, +{ + if vis.contains(&root) { + return; + } + vis.insert(root); + for level_1_node in egraph[root].nodes.iter() { + for level_1_node_child in level_1_node.children() { + for level_2_node in egraph[*level_1_node_child].nodes.iter() { + for level_2_node_child in level_2_node.children() { + if *level_2_node_child == root { + println!( + "found a cycle of length 2: {:?} {:?}", + level_1_node, level_2_node + ); + length_2_cycle + .push(vec![node_vars[&level_1_node], node_vars[&level_2_node]]); + } + } + } + cycle_2(egraph, *level_1_node_child, length_2_cycle, node_vars, vis); + } + } +} + +#[derive(Clone)] +struct ProblemWriter { + pub path: String, + problem: String, + parameters: String, + clause_counter: usize, +} + +impl ProblemWriter { + pub fn new(path: String) -> Self { + Self { + path, + problem: String::new(), + parameters: String::new(), + clause_counter: 0, + } + } + + pub fn comment(&mut self, comment: &str) { + self.problem.push_str(&format!("c {}\n", comment)); + } + + pub fn parameters(&mut self, num_vars: usize, top: f64) { + self.parameters = format!( + "p wcnf {} {} {}\n", + num_vars, self.clause_counter, top as i64 + ); + } + + pub fn hard_clause(&mut self, clause: &str, top: f64) { + self.clause_counter += 1; + self.problem + .push_str(&format!("{} {} 0\n", top as i64, clause)); + } + + pub fn soft_clause(&mut self, clause: &str, weight: f64) { + self.clause_counter += 1; + self.problem + .push_str(&format!("{} {} 0\n", weight as i64, clause)); + } + + pub fn dump(&mut self) { + println!("written to {}", self.path); + std::fs::write( + self.path.clone(), + format!("{}{}", self.parameters.clone(), self.problem.clone()), + ) + .unwrap(); + } +} + +/// the Extractor that constructs the constraint problem +pub struct MaxsatExtractor<'a, L: Language, N: Analysis> { + /// EGraph to extract + pub egraph: &'a EGraph, + writer: ProblemWriter, +} + +/// A weighted partial maxsat problem +pub struct WeightedPartialMaxsatProblem<'a, L: Language, N: Analysis> { + // pub class_vars: HashMap, + /// a map from enodes to maxsat variables (starting from 1) + pub node_vars: HashMap, + /// root eclass Id + pub root: Id, + /// EGraph to extract + pub egraph: &'a EGraph, + top: f64, + problem_writer: ProblemWriter, +} + +impl<'a, L, N> WeightedPartialMaxsatProblem<'a, L, N> +where + L: Language, + N: Analysis, +{ + /// Given a weighted partial maxsat problem, solve the problem + /// and parse the output + pub fn solve(&self) -> Result<(u128, Option, RecExpr), Vec> { + // assume maxhs installed + let start = Instant::now(); + let result = Command::new("maxhs") + .arg("-printSoln") + .arg(self.problem_writer.path.clone()) + .output(); + let elapsed = start.elapsed().as_millis(); + if let Ok(output) = result { + let stdout = String::from_utf8_lossy(&output.stdout); + let lines = stdout.lines(); + let (mut comments, mut opt_line, mut sol_line, mut solution) = + (vec![], vec![], vec![], vec![]); + for l in lines { + let mut line = l.split(" "); + if let Some(indicator) = line.next() { + match indicator { + "c" => comments.push(line.collect::>().join(" ")), + "o" => opt_line.push(line.collect::>().join(" ")), + "s" => sol_line.push(line.collect::>().join(" ")), + "v" => solution.push(line.collect::>().join(" ")), + _ => (), + } + } + } + assert!(sol_line.len() > 0, "Solution cannot be empty"); + let sol = sol_line.iter().next().unwrap(); + if sol.contains("UNSATISFIABLE") { + panic!("Problem UNSAT") + } else { + assert!( + solution.len() > 0, + "No solution line (try add -printSoln option to maxhs)" + ); + let sol = solution.iter().next().unwrap(); + // println!("Sol: {}", sol); + let sat_map = sol + .chars() + .enumerate() + .filter(|(_, res)| *res == '1') + .map(|(car, _)| car + 1) + .collect::>(); + let mut worklist = Vec::new(); + let mut expr = RecExpr::default(); + let mut id_map = HashMap::new(); + worklist.push(self.root); + let mut path: Vec<(Id, L)> = Vec::new(); + while let Some(&id) = worklist.last() { + if id_map.contains_key(&id) { + worklist.pop(); + path = path + .iter() + .cloned() + .filter(|(i, _)| *i != id) + .collect::>(); + continue; + } + // println!("Current node ids: {:?}", &self.egraph[id].nodes.iter().map(|x| self.node_vars[x]).collect::>()); + let mut not_found = true; + for n in &self.egraph[id].nodes { + if sat_map.contains(&self.node_vars[&n]) { + path.push((id, n.clone())); + not_found = false; + if n.all(|ch| id_map.contains_key(&ch)) { + let new_id = expr.add( + n.clone().map_children(|ch| id_map[&self.egraph.find(ch)]), + ); + id_map.insert(id.clone(), new_id); + path = path + .iter() + .cloned() + .filter(|(i, _)| *i != id) + .collect::>(); + worklist.pop(); + } else { + let pending_work = n + .children() + .iter() + .filter(|&x| !id_map.contains_key(x)) + .collect::>(); + for each in pending_work { + if let Some((idx, _)) = + path.iter().enumerate().find(|(_, (id, _))| id == each) + { + let subpath = path[idx..] + .iter() + .map(|(_, l)| l.clone()) + .collect::>(); + return Err(subpath + .iter() + .map(|x| self.node_vars[x]) + .collect::>()); + } + } + worklist.extend_from_slice(n.children()); + } + break; + } + } + if not_found { + panic!("No active node for eclass: {}", id.clone()); + } + } + // parse opt + if opt_line.len() > 0 { + let opt = opt_line.iter().next().unwrap(); + return Ok((elapsed, Some(opt.parse::().unwrap()), expr)); + } + return Ok((elapsed, None, expr)); + } + } else { + panic!( + "Unable to solve {}, err: {}", + self.problem_writer.path, + result.err().unwrap() + ); + } + } + + pub fn solve_with_refinement(&mut self) -> (u128, Option, RecExpr) { + loop { + let x = self.solve(); + if x.is_err() { + let cycle = x.err().unwrap(); + println!("Elim Cycle: {:?}", cycle); + let cycle_elim_clause = cycle + .iter() + .map(|x| format!("-{}", x)) + .collect::>() + .join(" "); + self.problem_writer + .hard_clause(&cycle_elim_clause, self.top); + self.problem_writer + .parameters(self.node_vars.len(), self.top); + self.problem_writer.dump(); + } else { + return x.unwrap(); + } + } + } +} + +/// Cost function; same interface as `LpCostFunction`. +pub trait MaxsatCostFunction> { + /// Returns the cost of the given e-node. + /// + /// This function may look at other parts of the e-graph to compute the cost + /// of the given e-node. + fn node_cost(&mut self, egraph: &EGraph, eclass: Id, enode: &L) -> f64; +} + +impl<'a, L, N> MaxsatExtractor<'a, L, N> +where + L: Language, + N: Analysis, +{ + /// create a new maxsat extractor + pub fn new(egraph: &'a EGraph, path: String) -> Self { + Self { + egraph, + writer: ProblemWriter::new(path.clone()), + } + } + + /// create a maxsat problem + pub fn create_problem( + &mut self, + root: Id, + name: &str, + no_cycle: bool, + mut cost_fn: CF, + ) -> WeightedPartialMaxsatProblem<'a, L, N> + where + CF: MaxsatCostFunction, + { + // Hard Constraints + // === root constraint (pick at least one in root) + // \forall n \in R, \bigvee v_n + // === children constraint + // \forall n, \forall C\in children(n), v_n -> \bigvee_cN v_cN \forall cN \in C + self.writer.comment(&format!("Problem: {}", name)); + // create variables + let mut num_vars = 0; + let mut top = 0 as f64; + let mut node_vars = HashMap::default(); + let mut node_weight_map = HashMap::new(); + for c in self.egraph.classes() { + for n in c.nodes.iter() { + node_vars.insert(n.clone(), num_vars + 1); + num_vars += 1; + + node_weight_map.insert(n.clone(), cost_fn.node_cost(self.egraph, c.id, n)); + top += cost_fn.node_cost(self.egraph, c.id, n); + } + } + + let top = top + 1 as f64; + + // Hard clauses + let mut hard_clauses = Vec::new(); + // root constraint + let root_clause = self.egraph[root] + .nodes + .iter() + .map(|n| node_vars[n]) + .map(|v| v.to_string()) + .collect::>() + .join(" "); + hard_clauses.push(root_clause); + + // children constraint + for c in self.egraph.classes() { + for n in c.nodes.iter() { + // v_n -> \bigvee_cN v_cN forall C + for ch in n.children() { + let mut clause = String::new(); + clause.push_str(&format!("-{}", node_vars[n])); + for ch_node in self.egraph[*ch].nodes.iter() { + clause.push_str(&format!(" {}", node_vars[ch_node])); + } + hard_clauses.push(clause); + } + } + } + + // cycle constraint + if no_cycle { + let mut cycles = Vec::new(); + // let mut vis = HashSet::default(); + let path = Vec::new(); + get_all_cycles( + self.egraph, + &root, + None, + &mut HashMap::new(), + &path, + &mut cycles, + &node_vars, + ); + cycle_2( + self.egraph, + root, + &mut cycles, + &node_vars, + &mut HashSet::new(), + ); + for cycle in cycles { + // println!("cycle: {:?}", cycle); + let clause = cycle + .iter() + .map(|v| format!("-{}", v)) + .collect::>() + .join(" "); + hard_clauses.push(clause); + } + } + + // soft clauses (i.e. not all nodes need to be picked) + let mut soft_clauses = HashMap::new(); + for c in self.egraph.classes() { + for n in c.nodes.iter() { + soft_clauses.insert(n.clone(), format!("-{}", node_vars[n])); + } + } + + let nbvars = num_vars; + + self.writer.comment("Hard clauses:"); + for clause in hard_clauses { + self.writer.hard_clause(&clause, top); + } + + self.writer.comment("Soft clauses:"); + for (n, clause) in soft_clauses { + self.writer.soft_clause(&clause, node_weight_map[&n]); + } + + self.writer.parameters(nbvars, top); + + self.writer.dump(); + + WeightedPartialMaxsatProblem { + top, + node_vars, + root, + egraph: self.egraph, + problem_writer: self.writer.clone(), + } + } +} diff --git a/flexmatch/src/mod.rs b/flexmatch/src/mod.rs index ca5c465..9b55f11 100644 --- a/flexmatch/src/mod.rs +++ b/flexmatch/src/mod.rs @@ -1 +1,2 @@ -pub(crate) mod rewrites; \ No newline at end of file +pub(crate) mod rewrites; +pub mod maxsat_extract; \ No newline at end of file diff --git a/flexmatch/test.sh b/flexmatch/test.sh new file mode 100644 index 0000000..268ca89 --- /dev/null +++ b/flexmatch/test.sh @@ -0,0 +1 @@ +cargo run ../tests/models/mobilenetv2.relay rewrite.json data.json vta-dense.json im2col.json --ilp diff --git a/tests/validate_compilation.py b/tests/validate_compilation.py index 545ae49..7c2ee5b 100644 --- a/tests/validate_compilation.py +++ b/tests/validate_compilation.py @@ -4,7 +4,7 @@ import numpy import tvm import test_model_on_vta as utils -from tvm.relay.testing import op_summary +# from tvm.relay.testing import op_summary DEFAULT_CONFIGS = { 'max_pool2d': ['flexasr-maxpool'], @@ -69,9 +69,9 @@ def get_offload_stats(model, quantize): mod = tvm.parser.fromtext(src) if quantize: mod = quantize_model(mod) - print(f'ALL overloads: {op_summary.count_all_overloads(mod)}') - print(f'ALL Ops: {op_summary.count_all_ops(mod)}') - print(f'ALL Ops in overloads = {op_summary.count_all_ops_in_overloads(mod)} * #ops per pattern') + # print(f'ALL overloads: {op_summary.count_all_overloads(mod)}') + # print(f'ALL Ops: {op_summary.count_all_ops(mod)}') + # print(f'ALL Ops in overloads = {op_summary.count_all_ops_in_overloads(mod)} * #ops per pattern') def run_model(model, configs, use_ilp, debug, get_stats, quantize): print(f'Step 1: Run EqSat with {" ".join(configs)}') From cb432244be125e858ed7008780bdc4b123660b9b Mon Sep 17 00:00:00 2001 From: AD1024 Date: Tue, 28 Feb 2023 01:12:18 -0500 Subject: [PATCH 02/18] tweak --- flexmatch/src/maxsat_extract.rs | 52 +++++---------------------------- 1 file changed, 8 insertions(+), 44 deletions(-) diff --git a/flexmatch/src/maxsat_extract.rs b/flexmatch/src/maxsat_extract.rs index f842100..b8988ee 100644 --- a/flexmatch/src/maxsat_extract.rs +++ b/flexmatch/src/maxsat_extract.rs @@ -4,45 +4,6 @@ use egg::{Analysis, EGraph, Id, Language, RecExpr}; use std::collections::{HashMap, HashSet}; use std::time::Instant; -/// Get all cycles in the given E-Graph -pub fn get_cycles( - egraph: &EGraph, - root: &Id, - path: &mut Vec<(Id, L)>, - vis: &mut HashSet, - cycles: &mut Vec>, - node_vars: &HashMap, -) where - L: Language, - N: Analysis, -{ - assert!( - !vis.contains(root), - "cannot be visited again, should be handled in cycle detection" - ); - assert!(*root == egraph.find(*root)); - vis.insert(*root); - for node in egraph[*root].nodes.iter() { - for ch in node.children() { - if vis.contains(ch) { - // cycle detected - if let Some((idx, _)) = path.iter().enumerate().find(|(_, (id, _))| id == ch) { - let mut subpath = path[idx..].to_vec(); - subpath.push((*root, node.clone())); - cycles.push(subpath.clone()); - } else if ch == root { - // self loop - cycles.push(vec![(*root, node.clone())]) - } - } else { - let mut to_here = path.clone(); - to_here.push((*root, node.clone())); - get_cycles(egraph, ch, &mut to_here, vis, cycles, node_vars); - } - } - } -} - pub fn get_all_cycles( egraph: &EGraph, root: &Id, @@ -201,7 +162,7 @@ where { /// Given a weighted partial maxsat problem, solve the problem /// and parse the output - pub fn solve(&self) -> Result<(u128, Option, RecExpr), Vec> { + pub fn solve(&self) -> Result<(u128, Option, RecExpr), (u128, Vec)> { // assume maxhs installed let start = Instant::now(); let result = Command::new("maxhs") @@ -289,10 +250,10 @@ where .iter() .map(|(_, l)| l.clone()) .collect::>(); - return Err(subpath + return Err((elapsed, subpath .iter() .map(|x| self.node_vars[x]) - .collect::>()); + .collect::>())); } } worklist.extend_from_slice(n.children()); @@ -321,10 +282,12 @@ where } pub fn solve_with_refinement(&mut self) -> (u128, Option, RecExpr) { + let mut total_time = 0; loop { let x = self.solve(); if x.is_err() { - let cycle = x.err().unwrap(); + let (t, cycle) = x.err().unwrap(); + total_time += t; println!("Elim Cycle: {:?}", cycle); let cycle_elim_clause = cycle .iter() @@ -337,7 +300,8 @@ where .parameters(self.node_vars.len(), self.top); self.problem_writer.dump(); } else { - return x.unwrap(); + let (t1, x, y) = x.unwrap(); + return (t1 + total_time, x, y); } } } From fafe03ef3b12f6c6a88ab2ad5b41d7b219894549 Mon Sep 17 00:00:00 2001 From: AD1024 Date: Tue, 28 Feb 2023 01:48:58 -0500 Subject: [PATCH 03/18] fix cycle detection --- flexmatch/src/maxsat_extract.rs | 42 +++++++++++++++++++++++---------- 1 file changed, 30 insertions(+), 12 deletions(-) diff --git a/flexmatch/src/maxsat_extract.rs b/flexmatch/src/maxsat_extract.rs index b8988ee..f47e090 100644 --- a/flexmatch/src/maxsat_extract.rs +++ b/flexmatch/src/maxsat_extract.rs @@ -10,6 +10,7 @@ pub fn get_all_cycles( parent: Option, color: &mut HashMap, path: &Vec<(Id, L)>, + cycle_map: &mut HashMap>>, cycles: &mut Vec>, node_vars: &HashMap, ) where @@ -27,13 +28,22 @@ pub fn get_all_cycles( new_cycle.push(node_vars[&n]); } new_cycle.push(parent.unwrap()); + let fst = new_cycle[0]; + if cycle_map.contains_key(&fst) { + let cycle_entry = cycle_map.get_mut(&fst).unwrap(); + cycle_entry.push(new_cycle.clone()); + } else { + let mut cycle_entry = Vec::new(); + cycle_entry.push(new_cycle.clone()); + cycle_map.insert(fst, cycle_entry); + } cycles.push(new_cycle); return; } panic!("Should have a cycle here: {}; path: {:?}", root, path); } color.insert(*root, 1); - for node in egraph[*root].nodes.iter() { + for (idx, node) in egraph[*root].nodes.iter().enumerate() { for ch in node.children() { let mut to_here = path.clone(); to_here.push((*root, node.clone())); @@ -43,10 +53,21 @@ pub fn get_all_cycles( Some(node_vars[node]), color, &to_here, + cycle_map, cycles, node_vars, ); } + for i in 0..idx { + if let Some(prev_cycle) = cycle_map.get(&node_vars[&egraph[*root].nodes[i]]) { + for cycle in prev_cycle { + let mut new_cycle = cycle.iter().cloned().skip(1).collect::>(); + new_cycle.push(node_vars[node]); + new_cycle.push(node_vars[&egraph[*root].nodes[idx]]); + cycles.push(new_cycle); + } + } + } } color.insert(*root, 2); } @@ -70,10 +91,6 @@ fn cycle_2( for level_2_node in egraph[*level_1_node_child].nodes.iter() { for level_2_node_child in level_2_node.children() { if *level_2_node_child == root { - println!( - "found a cycle of length 2: {:?} {:?}", - level_1_node, level_2_node - ); length_2_cycle .push(vec![node_vars[&level_1_node], node_vars[&level_2_node]]); } @@ -401,16 +418,17 @@ where None, &mut HashMap::new(), &path, + &mut HashMap::new(), &mut cycles, &node_vars, ); - cycle_2( - self.egraph, - root, - &mut cycles, - &node_vars, - &mut HashSet::new(), - ); + // cycle_2( + // self.egraph, + // root, + // &mut cycles, + // &node_vars, + // &mut HashSet::new(), + // ); for cycle in cycles { // println!("cycle: {:?}", cycle); let clause = cycle From e73bbd741d0648a80a8367501c63c26b5cd34990 Mon Sep 17 00:00:00 2001 From: AD1024 Date: Tue, 28 Feb 2023 01:51:46 -0500 Subject: [PATCH 04/18] add comment; important note! --- flexmatch/src/maxsat_extract.rs | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/flexmatch/src/maxsat_extract.rs b/flexmatch/src/maxsat_extract.rs index f47e090..4c5ce4f 100644 --- a/flexmatch/src/maxsat_extract.rs +++ b/flexmatch/src/maxsat_extract.rs @@ -58,6 +58,15 @@ pub fn get_all_cycles( node_vars, ); } + // This is the fundamental flaw that was not captured + // in Tensat's cycle detection algorithm: + // Even with coloring, nodes in the same eclass could share the same cycle by + // sharing some common children. + // However these children e-class will not be visited after we finish + // cycle detection for the first node in the e-class, so we need to maintain + // a map from the starting node to the cycles it is in, which will be used by + // other nodes that are in the same e-class to construct the cycles that + // they are not able to detect. for i in 0..idx { if let Some(prev_cycle) = cycle_map.get(&node_vars[&egraph[*root].nodes[i]]) { for cycle in prev_cycle { From e0f7505ccbc7c5e876bbda70d9c7670c7ce79e43 Mon Sep 17 00:00:00 2001 From: AD1024 Date: Tue, 28 Feb 2023 02:15:53 -0500 Subject: [PATCH 05/18] timeout comparisons --- flexmatch/Cargo.toml | 2 +- flexmatch/src/main.rs | 65 +++++++++++++++++++++++++-------- flexmatch/src/maxsat_extract.rs | 11 ++++-- 3 files changed, 57 insertions(+), 21 deletions(-) diff --git a/flexmatch/Cargo.toml b/flexmatch/Cargo.toml index 8ddd91b..7c40014 100644 --- a/flexmatch/Cargo.toml +++ b/flexmatch/Cargo.toml @@ -19,7 +19,7 @@ env_logger = "0.9.0" git = "https://github.com/gussmith23/glenside" rev = "611a6bc4b9990849f26daaa4d808a8497124fedc" default-features = false -features = ["tvm"] +features = ["tvm", "rplex"] [dependencies.egg] git = "https://github.com/AD1024/egg" diff --git a/flexmatch/src/main.rs b/flexmatch/src/main.rs index 76c6c17..cf2ff22 100644 --- a/flexmatch/src/main.rs +++ b/flexmatch/src/main.rs @@ -97,7 +97,8 @@ fn main() { let output_file = PathBuf::from(&args[2]); let analysis_data_file = PathBuf::from(&args[3]); let use_ilp = &args[args.len() - 1] == "--ilp"; - let config_files = if use_ilp { + let use_maxsat = &args[args.len() - 1] == "--maxsat"; + let config_files = if use_ilp || use_maxsat { &args[4..args.len() - 1] } else { &args[4..] @@ -207,7 +208,7 @@ fn main() { } info!("Root eclass analysis: {:?}", runner.egraph[root_expr].data); info!("Root eclass nodes: {:?}", runner.egraph[root_expr].nodes); - if !use_ilp { + if !use_ilp && !use_maxsat { info!("Extraction without ILP"); let extractor = Extractor::new( &runner.egraph, @@ -227,25 +228,57 @@ fn main() { fn node_cost( &mut self, egraph: &EGraph, - eclass: egg::Id, + _: egg::Id, enode: &glenside::language::Language, ) -> f64 { return get_node_weights(enode, egraph.total_size() as f64); } } - let mut maxsat_ext = MaxsatExtractor::new(&runner.egraph, "problem.wcnf".into()); - let mut problem = maxsat_ext.create_problem(root_expr, "problem", true, Costfn); - let (solve_time, cost, best) = problem.solve_with_refinement(); - // println!("{}", best); - println!("Solve time: {}", solve_time); - println!("Cost: {}", cost.unwrap()); - save_expr_and_analysis( - output_file, - analysis_data_file, - &env, - &dtype_info.into_iter().collect(), - &best, - ); + if use_maxsat { + let mut maxsat_ext = MaxsatExtractor::new(&runner.egraph, "problem.wcnf".into()); + let mut problem = maxsat_ext.create_problem(root_expr, "problem", true, Costfn); + let (solve_time, cost, best) = problem.solve_with_refinement(); + // println!("{}", best); + println!("Solve time: {}", solve_time); + println!("Cost: {}", cost.unwrap()); + save_expr_and_analysis( + output_file, + analysis_data_file, + &env, + &dtype_info.into_iter().collect(), + &best, + ); + } else { + #[cfg(feature = "cplex")] + { + println!("Extract using ILP"); + let cplex_env = rplex::Env::new().unwrap(); + let mut model = glenside::extraction::ilp::create_generic_egraph_lp_model( + &cplex_env, + &runner.egraph, + |_, _, _| true, + &[root_expr], + "ilp_ext", + ); + let result = model.problem.solve().unwrap(); + let (out_expr, _old_id_to_new_id_map) = + glenside::extraction::ilp::extract_single_expression( + &model, + &result.variables, + EGraph::new(MyAnalysis { + name_to_shape: env.clone(), + name_to_dtype: dtype_info.iter().cloned().collect(), + }), + ); + let mut maxsat_ext = + MaxsatExtractor::new(&out_expr, "compare-original.wcnf".into()); + let mut problem = maxsat_ext.create_problem(root_expr, "problem", true, Costfn); + let (solve_time, cost, _) = problem.solve_with_refinement(); + // println!("{}", best); + println!("Solve time: {}", solve_time); + println!("Cost: {}", cost.unwrap()); + } + } } } } diff --git a/flexmatch/src/maxsat_extract.rs b/flexmatch/src/maxsat_extract.rs index 4c5ce4f..0935ee3 100644 --- a/flexmatch/src/maxsat_extract.rs +++ b/flexmatch/src/maxsat_extract.rs @@ -276,10 +276,13 @@ where .iter() .map(|(_, l)| l.clone()) .collect::>(); - return Err((elapsed, subpath - .iter() - .map(|x| self.node_vars[x]) - .collect::>())); + return Err(( + elapsed, + subpath + .iter() + .map(|x| self.node_vars[x]) + .collect::>(), + )); } } worklist.extend_from_slice(n.children()); From f83600e6937d604eb61da41ad26795ed696e3b7f Mon Sep 17 00:00:00 2001 From: AD1024 Date: Wed, 1 Mar 2023 14:35:45 -0500 Subject: [PATCH 06/18] optimize --- flexmatch/src/main.rs | 54 ++++++++---- flexmatch/src/maxsat_extract.rs | 145 ++++++++++++-------------------- 2 files changed, 94 insertions(+), 105 deletions(-) diff --git a/flexmatch/src/main.rs b/flexmatch/src/main.rs index cf2ff22..9e84ced 100644 --- a/flexmatch/src/main.rs +++ b/flexmatch/src/main.rs @@ -15,6 +15,7 @@ use std::{ env, fs, path::{Path, PathBuf}, process::exit, + time::Instant, }; use tvm; @@ -46,6 +47,7 @@ fn read_configs(flexmatch_home: &PathBuf, config_files: &[String]) -> Vec, rec_expr: &mut egg::RecExpr, @@ -58,7 +60,7 @@ fn save_egraph_as_recexpr( for (_id, expr) in expr_map.into_iter() { rec_expr.add(expr); } -} +} */ fn save_expr_and_analysis( rec_expr_file: PathBuf, @@ -208,13 +210,40 @@ fn main() { } info!("Root eclass analysis: {:?}", runner.egraph[root_expr].data); info!("Root eclass nodes: {:?}", runner.egraph[root_expr].nodes); + struct Costfn; + impl MaxsatCostFunction for Costfn { + fn node_cost( + &mut self, + egraph: &EGraph, + _: egg::Id, + enode: &glenside::language::Language, + ) -> f64 { + return get_node_weights(enode, egraph.total_size() as f64); + } + } if !use_ilp && !use_maxsat { info!("Extraction without ILP"); let extractor = Extractor::new( &runner.egraph, AcceleratorCostFunction(runner.egraph.total_size() as f64), ); + let start = Instant::now(); let (_cost, best) = extractor.find_best(root_expr); + let elapsed = start.elapsed().as_millis(); + // Convert cost to CostFn + let mut tmp_egraph: EGraph<_, MyAnalysis> = EGraph::new(MyAnalysis { + name_to_shape: env.clone(), + name_to_dtype: dtype_info.iter().cloned().collect(), + }); + tmp_egraph.add_expr(&best); + let mut cost = 0.0; + for c in tmp_egraph.classes() { + for n in c.nodes.iter() { + cost += get_node_weights(n, runner.egraph.total_size() as f64); + } + } + println!("Extraction time: {} ms", elapsed); + println!("Cost: {}", cost); save_expr_and_analysis( output_file, analysis_data_file, @@ -223,23 +252,14 @@ fn main() { &best, ); } else { - struct Costfn; - impl MaxsatCostFunction for Costfn { - fn node_cost( - &mut self, - egraph: &EGraph, - _: egg::Id, - enode: &glenside::language::Language, - ) -> f64 { - return get_node_weights(enode, egraph.total_size() as f64); - } - } if use_maxsat { let mut maxsat_ext = MaxsatExtractor::new(&runner.egraph, "problem.wcnf".into()); + let start = Instant::now(); let mut problem = maxsat_ext.create_problem(root_expr, "problem", true, Costfn); let (solve_time, cost, best) = problem.solve_with_refinement(); - // println!("{}", best); - println!("Solve time: {}", solve_time); + let elapsed = start.elapsed().as_millis(); + println!("Extraction time: {} ms", elapsed); + println!("Solver time: {} ms", solve_time); println!("Cost: {}", cost.unwrap()); save_expr_and_analysis( output_file, @@ -283,6 +303,7 @@ fn main() { } } +/* fn check_accelerator_call_by_eid( ch_id: &egg::Id, egraph: &EGraph, @@ -291,7 +312,7 @@ fn check_accelerator_call_by_eid( MyAnalysisData::AccessPattern(access) => access.contains_accelerator_calls, _ => false, } -} +} */ fn get_node_weights(node: &glenside::language::Language, total_size: f64) -> f64 { if let glenside::language::Language::AcceleratorCall(_) = node { @@ -335,6 +356,7 @@ fn get_node_weights(node: &glenside::language::Language, total_size: f64) -> f64 } } +/* fn filter_nodes( node: &glenside::language::Language, id: egg::Id, @@ -372,4 +394,4 @@ fn filter_nodes( } } return true; -} +} */ diff --git a/flexmatch/src/maxsat_extract.rs b/flexmatch/src/maxsat_extract.rs index 0935ee3..3c53a6d 100644 --- a/flexmatch/src/maxsat_extract.rs +++ b/flexmatch/src/maxsat_extract.rs @@ -4,15 +4,24 @@ use egg::{Analysis, EGraph, Id, Language, RecExpr}; use std::collections::{HashMap, HashSet}; use std::time::Instant; -pub fn get_all_cycles( +fn disjuct_negative(nodes: &Vec, problem_writer: &mut ProblemWriter, top: f64) { + let clause = nodes + .iter() + .map(|x| format!("-{}", x)) + .collect::>() + .join(" "); + problem_writer.hard_clause(&clause, top); +} + +fn get_all_cycles( egraph: &EGraph, root: &Id, parent: Option, color: &mut HashMap, - path: &Vec<(Id, L)>, - cycle_map: &mut HashMap>>, - cycles: &mut Vec>, + path: &mut Vec<(Id, L)>, + problem_writer: &mut ProblemWriter, node_vars: &HashMap, + top: f64, ) where L: Language, N: Analysis, @@ -21,23 +30,21 @@ pub fn get_all_cycles( return; } if color.contains_key(root) && color[root] == 1 { - let mut new_cycle = Vec::new(); if let Some((idx, _)) = path.iter().enumerate().find(|(_, (id, _))| id == root) { + // let mut subpath: Vec = path[idx..].iter().cloned().map(|(_, n)| node_vars[&n]).collect(); + // subpath.push(parent.unwrap()); + // cycles.entry(*root).or_insert_with(Vec::new).push(subpath); + // + let mut new_cycle = Vec::new(); let subpath = path[idx..].to_vec(); for (_, n) in subpath { new_cycle.push(node_vars[&n]); } new_cycle.push(parent.unwrap()); - let fst = new_cycle[0]; - if cycle_map.contains_key(&fst) { - let cycle_entry = cycle_map.get_mut(&fst).unwrap(); - cycle_entry.push(new_cycle.clone()); - } else { - let mut cycle_entry = Vec::new(); - cycle_entry.push(new_cycle.clone()); - cycle_map.insert(fst, cycle_entry); + for node_idx in egraph[*root].nodes.iter().map(|x| node_vars[x]) { + new_cycle[0] = node_idx; + disjuct_negative(&new_cycle, problem_writer, top); } - cycles.push(new_cycle); return; } panic!("Should have a cycle here: {}; path: {:?}", root, path); @@ -45,71 +52,25 @@ pub fn get_all_cycles( color.insert(*root, 1); for (idx, node) in egraph[*root].nodes.iter().enumerate() { for ch in node.children() { - let mut to_here = path.clone(); - to_here.push((*root, node.clone())); + // let mut to_here = path.clone(); + // to_here.push((*root, node.clone())); + path.push((*root, node.clone())); get_all_cycles( egraph, ch, Some(node_vars[node]), color, - &to_here, - cycle_map, - cycles, + path, + problem_writer, node_vars, + top, ); - } - // This is the fundamental flaw that was not captured - // in Tensat's cycle detection algorithm: - // Even with coloring, nodes in the same eclass could share the same cycle by - // sharing some common children. - // However these children e-class will not be visited after we finish - // cycle detection for the first node in the e-class, so we need to maintain - // a map from the starting node to the cycles it is in, which will be used by - // other nodes that are in the same e-class to construct the cycles that - // they are not able to detect. - for i in 0..idx { - if let Some(prev_cycle) = cycle_map.get(&node_vars[&egraph[*root].nodes[i]]) { - for cycle in prev_cycle { - let mut new_cycle = cycle.iter().cloned().skip(1).collect::>(); - new_cycle.push(node_vars[node]); - new_cycle.push(node_vars[&egraph[*root].nodes[idx]]); - cycles.push(new_cycle); - } - } + path.pop(); } } color.insert(*root, 2); } -fn cycle_2( - egraph: &EGraph, - root: Id, - length_2_cycle: &mut Vec>, - node_vars: &HashMap, - vis: &mut HashSet, -) where - L: Language, - N: Analysis, -{ - if vis.contains(&root) { - return; - } - vis.insert(root); - for level_1_node in egraph[root].nodes.iter() { - for level_1_node_child in level_1_node.children() { - for level_2_node in egraph[*level_1_node_child].nodes.iter() { - for level_2_node_child in level_2_node.children() { - if *level_2_node_child == root { - length_2_cycle - .push(vec![node_vars[&level_1_node], node_vars[&level_2_node]]); - } - } - } - cycle_2(egraph, *level_1_node_child, length_2_cycle, node_vars, vis); - } - } -} - #[derive(Clone)] struct ProblemWriter { pub path: String, @@ -421,35 +382,41 @@ where // cycle constraint if no_cycle { - let mut cycles = Vec::new(); - // let mut vis = HashSet::default(); - let path = Vec::new(); + // let mut cycles = HashMap::new(); + let mut path = Vec::new(); get_all_cycles( self.egraph, &root, None, &mut HashMap::new(), - &path, - &mut HashMap::new(), - &mut cycles, + &mut path, + &mut self.writer, &node_vars, + top, ); - // cycle_2( - // self.egraph, - // root, - // &mut cycles, - // &node_vars, - // &mut HashSet::new(), - // ); - for cycle in cycles { - // println!("cycle: {:?}", cycle); - let clause = cycle - .iter() - .map(|v| format!("-{}", v)) - .collect::>() - .join(" "); - hard_clauses.push(clause); - } + // for (eid, cycles) in cycles { + // for enode_id in self.egraph[eid].nodes.iter().map(|x| node_vars[x]) { + // for cycle_tail in cycles.iter() { + // let mut cycle = vec![enode_id]; + // cycle.extend(cycle_tail.iter()); + // let clause = cycle + // .iter() + // .map(|v| format!("-{}", v)) + // .collect::>() + // .join(" "); + // hard_clauses.push(clause); + // } + // } + // } + // for cycle in cycles { + // // println!("cycle: {:?}", cycle); + // let clause = cycle + // .iter() + // .map(|v| format!("-{}", v)) + // .collect::>() + // .join(" "); + // hard_clauses.push(clause); + // } } // soft clauses (i.e. not all nodes need to be picked) From f0c2bec753186bf705431c281e663995cee89517 Mon Sep 17 00:00:00 2001 From: AD1024 Date: Fri, 3 Mar 2023 11:39:00 -0500 Subject: [PATCH 07/18] save --- flexmatch/src/main.rs | 29 +++++++++++++++++++++++++++-- 1 file changed, 27 insertions(+), 2 deletions(-) diff --git a/flexmatch/src/main.rs b/flexmatch/src/main.rs index 9e84ced..690637c 100644 --- a/flexmatch/src/main.rs +++ b/flexmatch/src/main.rs @@ -9,10 +9,12 @@ use glenside::{ use maxsat_extract::*; use rewrites::{get_rewrite_from_string, im2col_rewrites, linear_rewrites}; use serde::Deserialize; -use serde_json; +use serde_json::{self, json}; +use std::io::prelude::*; use std::{ collections::{BTreeMap, HashMap, HashSet}, - env, fs, + env, + fs::{self, OpenOptions}, path::{Path, PathBuf}, process::exit, time::Instant, @@ -87,6 +89,29 @@ fn save_expr_and_analysis( let _ = std::fs::write(data_output, data_json_dump.to_string()).unwrap(); } +fn save_extraction_stats( + algo: &'static str, + stat_file: &String, + best_cost: f64, + solver_time: u128, + extract_time: u128, +) { + let output_file = PathBuf::from(env::current_dir().unwrap()).join(stat_file); + let stat = json!({ + "algo": algo, + "best_cost": best_cost, + "solver_time": solver_time, + "extract_time": extract_time, + }); + let mut file = OpenOptions::new() + .write(true) + .append(true) + .create(true) + .open(output_file) + .unwrap(); + writeln!(file, "{}", stat).unwrap(); +} + fn main() { env_logger::init(); let args = env::args().collect::>(); From 0093f8d9487477c10cb047c7a6364048ecb31cca Mon Sep 17 00:00:00 2001 From: AD1024 Date: Sat, 4 Mar 2023 23:47:23 -0500 Subject: [PATCH 08/18] new ilp extract --- flexmatch/Cargo.toml | 1 + flexmatch/src/ilp_extract.rs | 239 ++++++++++++++++++++++++++++++++ flexmatch/src/main.rs | 78 ++++++++--- flexmatch/src/maxsat_extract.rs | 53 ++----- 4 files changed, 304 insertions(+), 67 deletions(-) create mode 100644 flexmatch/src/ilp_extract.rs diff --git a/flexmatch/Cargo.toml b/flexmatch/Cargo.toml index 7c40014..ddf5fa5 100644 --- a/flexmatch/Cargo.toml +++ b/flexmatch/Cargo.toml @@ -14,6 +14,7 @@ serde_json = "1.0" serde = "1.0.130" log = "0.4.14" env_logger = "0.9.0" +rand = "0.8.5" [dependencies.glenside] git = "https://github.com/gussmith23/glenside" diff --git a/flexmatch/src/ilp_extract.rs b/flexmatch/src/ilp_extract.rs new file mode 100644 index 0000000..f7ef50f --- /dev/null +++ b/flexmatch/src/ilp_extract.rs @@ -0,0 +1,239 @@ +use std::{collections::HashMap, time::Instant}; + +use egg::{Analysis, EGraph, Id, Language, RecExpr}; +use rand::Rng; +use rplex::{self, var, Problem, VariableValue, WeightedVariable}; + +fn get_all_cycles<'a, L, N>( + egraph: &EGraph, + root: &Id, + color: &mut HashMap, + path: &mut Vec<(Id, L)>, + problem: &mut Problem<'a>, + node_vars: &HashMap, +) where + L: Language, + N: Analysis, +{ + if color.contains_key(root) && color[root] == 2 { + return; + } + if color.contains_key(root) && color[root] == 1 { + if let Some((idx, _)) = path.iter().enumerate().find(|(_, (id, _))| id == root) { + let mut new_cycle = Vec::new(); + let subpath = path[idx..].to_vec(); + for (_, n) in subpath { + new_cycle.push(node_vars[&n]); + } + let mut rng = rand::thread_rng(); + if new_cycle.len() == 1 { + let mut constraint = rplex::Constraint::new( + rplex::ConstraintType::Eq, + 0.0, + format!("cycle_{}_{}", root, rng.gen::()), + ); + constraint.add_wvar(WeightedVariable::new_idx(new_cycle[0], 1.0)); + problem.add_constraint(constraint).unwrap(); + } else { + for node_idx in egraph[*root].nodes.iter().map(|x| node_vars[x]) { + new_cycle[0] = node_idx; + // sum up <= len(new_cycle) - 1 + let mut constraint = rplex::Constraint::new( + rplex::ConstraintType::LessThanEq, + new_cycle.len() as f64 - 1.0, + format!("cycle_{}_{}", root, rng.gen::()), + ); + for node_idx in new_cycle.iter() { + constraint.add_wvar(WeightedVariable::new_idx(*node_idx, 1.0)); + } + problem.add_constraint(constraint).unwrap(); + } + } + return; + } + panic!("Should have a cycle here: {}; path: {:?}", root, path); + } + color.insert(*root, 1); + for node in egraph[*root].nodes.iter() { + for ch in node.children() { + path.push((*root, node.clone())); + get_all_cycles(egraph, ch, color, path, problem, node_vars); + path.pop(); + } + } + color.insert(*root, 2); +} + +pub struct ILPProblem<'a, L, N> +where + L: Language, + N: Analysis, +{ + pub node_vars: HashMap, + pub problem: Problem<'a>, + pub root: Id, + pub egraph: &'a EGraph, +} + +impl<'a, L, N> ILPProblem<'a, L, N> +where + L: Language, + N: Analysis, +{ + pub fn new( + problem: Problem<'a>, + egraph: &'a EGraph, + root: Id, + node_vars: HashMap, + ) -> Self { + ILPProblem { + problem, + root, + node_vars, + egraph, + } + } + + pub fn solve(&mut self) -> (u128, f64, RecExpr) { + self.problem + .set_objective_type(rplex::ObjectiveType::Minimize) + .unwrap(); + let start = Instant::now(); + let solution = self.problem.solve().unwrap(); + let solve_time = start.elapsed().as_millis(); + let cost = solution.objective; + + let mut expr = RecExpr::default(); + let mut new_id_map = HashMap::new(); + let mut worklist = vec![self.root]; + let mut path: Vec<(Id, L)> = Vec::new(); + + while let Some(&id) = worklist.last() { + if new_id_map.contains_key(&id) { + worklist.pop(); + path = path + .iter() + .cloned() + .filter(|(i, _)| *i != id) + .collect::>(); + continue; + } + let mut not_found = true; + for node in &self.egraph[id].nodes { + let node_idx = self.node_vars[node]; + match solution.variables[node_idx] { + VariableValue::Binary(true) => { + path.push((id, node.clone())); + not_found = false; + if node.all(|c| new_id_map.contains_key(&c)) { + let new_id = expr.add(node.clone().map_children(|c| new_id_map[&c])); + new_id_map.insert(id, new_id); + path = path + .iter() + .cloned() + .filter(|(i, _)| *i != id) + .collect::>(); + worklist.pop(); + } else { + let pending_work = node + .children() + .iter() + .filter(|&x| !new_id_map.contains_key(x)) + .collect::>(); + for each in pending_work { + if let Some((idx, _)) = + path.iter().enumerate().find(|(_, (id, _))| id == each) + { + let subpath = path[idx..] + .iter() + .map(|(_, l)| l.clone()) + .collect::>(); + panic!("Cycle detected at {}: {:?}", id, subpath); + } + } + worklist.extend(node.children()); + } + break; + } + _ => continue, + } + } + if not_found { + panic!("No enode chosen for eclass {}", id); + } + } + + return (solve_time, cost, expr); + } +} + +fn node_name(idx: usize) -> String { + format!("node_idx_{}", idx) +} + +pub fn create_problem<'a, L, N, CF>( + env: &'a rplex::Env, + root: Id, + egraph: &'a EGraph, + no_cycle: bool, + mut cost_fn: CF, +) -> ILPProblem<'a, L, N> +where + L: Language, + N: Analysis, + CF: FnMut(&EGraph, egg::Id, &L) -> f64, +{ + let mut problem = Problem::new(&env, "egraph_ext").unwrap(); + let mut node_vars = HashMap::new(); + + // create node_vars + for eclass in egraph.classes() { + for (idx, node) in eclass.nodes.iter().enumerate() { + let name = node_name(idx); + let cost = cost_fn(egraph, eclass.id, node); + let var = var!(0.0 <= name <= 1.0 -> cost as Binary); + node_vars.insert(node.clone(), problem.add_variable(var).unwrap()); + } + } + + // root constraint + let mut constraint = rplex::Constraint::new(rplex::ConstraintType::Eq, 1.0, "root constraint"); + for node_idx in egraph[root].nodes.iter().map(|x| node_vars[x]) { + constraint.add_wvar(WeightedVariable::new_idx(node_idx, 1.0)); + } + problem.add_constraint(constraint).unwrap(); + + // children constraint + for eclass in egraph.classes() { + for node in egraph[eclass.id].nodes.iter() { + let node_idx = node_vars[node]; + for (ch_idx, ch) in node.children().iter().enumerate() { + let mut constraint = rplex::Constraint::new( + rplex::ConstraintType::GreaterThanEq, + 0.0, + format!("{}_child_{}", node_idx, ch_idx), + ); + constraint.add_wvar(WeightedVariable::new_idx(node_idx, -1.0)); + for ch_node_idx in egraph[*ch].nodes.iter().map(|x| node_vars[x]) { + constraint.add_wvar(WeightedVariable::new_idx(ch_node_idx, 1.0)); + } + problem.add_constraint(constraint).unwrap(); + } + } + } + + if no_cycle { + let mut color = HashMap::new(); + let mut path = Vec::new(); + get_all_cycles( + egraph, + &root, + &mut color, + &mut path, + &mut problem, + &node_vars, + ); + } + + return ILPProblem::new(problem, egraph, root, node_vars); +} diff --git a/flexmatch/src/main.rs b/flexmatch/src/main.rs index 690637c..f828b7a 100644 --- a/flexmatch/src/main.rs +++ b/flexmatch/src/main.rs @@ -1,3 +1,4 @@ +mod ilp_extract; mod maxsat_extract; mod rewrites; @@ -123,7 +124,8 @@ fn main() { let source_file = &args[1]; let output_file = PathBuf::from(&args[2]); let analysis_data_file = PathBuf::from(&args[3]); - let use_ilp = &args[args.len() - 1] == "--ilp"; + let use_custom_ilp = &args[args.len() - 1] == "--new-ilp"; + let use_ilp = &args[args.len() - 1] == "--ilp" || use_custom_ilp; let use_maxsat = &args[args.len() - 1] == "--maxsat"; let config_files = if use_ilp || use_maxsat { &args[4..args.len() - 1] @@ -294,34 +296,64 @@ fn main() { &best, ); } else { - #[cfg(feature = "cplex")] - { - println!("Extract using ILP"); + if use_custom_ilp { + println!("Extract using custom ILP cycle breaking"); let cplex_env = rplex::Env::new().unwrap(); - let mut model = glenside::extraction::ilp::create_generic_egraph_lp_model( + let mut cost_fn = Costfn {}; + let start = Instant::now(); + let mut problem = ilp_extract::create_problem( &cplex_env, + root_expr, &runner.egraph, - |_, _, _| true, - &[root_expr], - "ilp_ext", + true, + move |x, y, z| cost_fn.node_cost(x, y, z), ); - let result = model.problem.solve().unwrap(); - let (out_expr, _old_id_to_new_id_map) = - glenside::extraction::ilp::extract_single_expression( - &model, - &result.variables, - EGraph::new(MyAnalysis { - name_to_shape: env.clone(), - name_to_dtype: dtype_info.iter().cloned().collect(), - }), - ); + let (solve_time, _, best) = problem.solve(); + let elapsed = start.elapsed().as_millis(); + let mut tmp_egraph = EGraph::new(MyAnalysis { + name_to_shape: env.clone(), + name_to_dtype: dtype_info.iter().cloned().collect(), + }); + let root = tmp_egraph.add_expr(&best); let mut maxsat_ext = - MaxsatExtractor::new(&out_expr, "compare-original.wcnf".into()); - let mut problem = maxsat_ext.create_problem(root_expr, "problem", true, Costfn); - let (solve_time, cost, _) = problem.solve_with_refinement(); - // println!("{}", best); - println!("Solve time: {}", solve_time); + MaxsatExtractor::new(&tmp_egraph, "compare-original.wcnf".into()); + let mut problem = maxsat_ext.create_problem(root, "problem", true, Costfn); + let (_, cost, _) = problem.solve_with_refinement(); + + println!("Extraction time: {} ms", elapsed); + println!("Solver time: {} ms", solve_time); println!("Cost: {}", cost.unwrap()); + } else { + #[cfg(feature = "cplex")] + { + println!("Extract using ILP"); + let cplex_env = rplex::Env::new().unwrap(); + let mut model = glenside::extraction::ilp::create_generic_egraph_lp_model( + &cplex_env, + &runner.egraph, + |_, _, _| true, + &[root_expr], + "ilp_ext", + ); + let result = model.problem.solve().unwrap(); + let (out_expr, _old_id_to_new_id_map) = + glenside::extraction::ilp::extract_single_expression( + &model, + &result.variables, + EGraph::new(MyAnalysis { + name_to_shape: env.clone(), + name_to_dtype: dtype_info.iter().cloned().collect(), + }), + ); + let mut maxsat_ext = + MaxsatExtractor::new(&out_expr, "compare-original.wcnf".into()); + let mut problem = + maxsat_ext.create_problem(root_expr, "problem", true, Costfn); + let (solve_time, cost, _) = problem.solve_with_refinement(); + // println!("{}", best); + println!("Solve time: {}", solve_time); + println!("Cost: {}", cost.unwrap()); + } } } } diff --git a/flexmatch/src/maxsat_extract.rs b/flexmatch/src/maxsat_extract.rs index 3c53a6d..dccc0dc 100644 --- a/flexmatch/src/maxsat_extract.rs +++ b/flexmatch/src/maxsat_extract.rs @@ -16,7 +16,6 @@ fn disjuct_negative(nodes: &Vec, problem_writer: &mut ProblemWriter, top: fn get_all_cycles( egraph: &EGraph, root: &Id, - parent: Option, color: &mut HashMap, path: &mut Vec<(Id, L)>, problem_writer: &mut ProblemWriter, @@ -31,40 +30,30 @@ fn get_all_cycles( } if color.contains_key(root) && color[root] == 1 { if let Some((idx, _)) = path.iter().enumerate().find(|(_, (id, _))| id == root) { - // let mut subpath: Vec = path[idx..].iter().cloned().map(|(_, n)| node_vars[&n]).collect(); - // subpath.push(parent.unwrap()); - // cycles.entry(*root).or_insert_with(Vec::new).push(subpath); - // let mut new_cycle = Vec::new(); let subpath = path[idx..].to_vec(); for (_, n) in subpath { new_cycle.push(node_vars[&n]); } - new_cycle.push(parent.unwrap()); - for node_idx in egraph[*root].nodes.iter().map(|x| node_vars[x]) { - new_cycle[0] = node_idx; - disjuct_negative(&new_cycle, problem_writer, top); + if new_cycle.len() == 1 { + problem_writer.hard_clause(&format!("-{}", new_cycle[0]), top); + } else { + for node_idx in egraph[*root].nodes.iter().map(|x| node_vars[x]) { + new_cycle[0] = node_idx; + disjuct_negative(&new_cycle, problem_writer, top); + } } return; } panic!("Should have a cycle here: {}; path: {:?}", root, path); } color.insert(*root, 1); - for (idx, node) in egraph[*root].nodes.iter().enumerate() { + for node in egraph[*root].nodes.iter() { for ch in node.children() { // let mut to_here = path.clone(); // to_here.push((*root, node.clone())); path.push((*root, node.clone())); - get_all_cycles( - egraph, - ch, - Some(node_vars[node]), - color, - path, - problem_writer, - node_vars, - top, - ); + get_all_cycles(egraph, ch, color, path, problem_writer, node_vars, top); path.pop(); } } @@ -387,36 +376,12 @@ where get_all_cycles( self.egraph, &root, - None, &mut HashMap::new(), &mut path, &mut self.writer, &node_vars, top, ); - // for (eid, cycles) in cycles { - // for enode_id in self.egraph[eid].nodes.iter().map(|x| node_vars[x]) { - // for cycle_tail in cycles.iter() { - // let mut cycle = vec![enode_id]; - // cycle.extend(cycle_tail.iter()); - // let clause = cycle - // .iter() - // .map(|v| format!("-{}", v)) - // .collect::>() - // .join(" "); - // hard_clauses.push(clause); - // } - // } - // } - // for cycle in cycles { - // // println!("cycle: {:?}", cycle); - // let clause = cycle - // .iter() - // .map(|v| format!("-{}", v)) - // .collect::>() - // .join(" "); - // hard_clauses.push(clause); - // } } // soft clauses (i.e. not all nodes need to be picked) From b9e125fadd4e96c3db32648b3f2a0c5f11a0d9b0 Mon Sep 17 00:00:00 2001 From: AD1024 Date: Sun, 5 Mar 2023 14:31:46 -0500 Subject: [PATCH 09/18] add topo sort comparison --- flexmatch/src/ilp_extract.rs | 50 ++++++++++++++++++++++++++++-------- flexmatch/src/main.rs | 6 +++-- 2 files changed, 44 insertions(+), 12 deletions(-) diff --git a/flexmatch/src/ilp_extract.rs b/flexmatch/src/ilp_extract.rs index f7ef50f..844bc0e 100644 --- a/flexmatch/src/ilp_extract.rs +++ b/flexmatch/src/ilp_extract.rs @@ -176,6 +176,7 @@ pub fn create_problem<'a, L, N, CF>( root: Id, egraph: &'a EGraph, no_cycle: bool, + topo_sort: bool, mut cost_fn: CF, ) -> ILPProblem<'a, L, N> where @@ -223,16 +224,45 @@ where } if no_cycle { - let mut color = HashMap::new(); - let mut path = Vec::new(); - get_all_cycles( - egraph, - &root, - &mut color, - &mut path, - &mut problem, - &node_vars, - ); + if topo_sort { + // add topo variables for each enode + let mut topo_vars = HashMap::new(); + let top = egraph.total_size() as f64; + for eclass in egraph.classes() { + let name = format!("topo_{}", eclass.id); + let var = var!(0.0 <= name <= (top - 1.0) -> 0.0 as Integer); + topo_vars.insert(eclass.id, problem.add_variable(var).unwrap()); + } + // topolotical ordering + // let mut memo = HashSet::new(); + for eclass in egraph.classes() { + for enode in eclass.nodes.iter() { + for child in enode.children().iter() { + let mut topo_constraint = rplex::Constraint::new( + rplex::ConstraintType::GreaterThanEq, + 1.0 - top, + format!("topo_sort_{}_{}", eclass.id, child), + ); + topo_constraint + .add_wvar(WeightedVariable::new_idx(topo_vars[&eclass.id], 1.0)); + topo_constraint.add_wvar(WeightedVariable::new_idx(node_vars[enode], -top)); + topo_constraint.add_wvar(WeightedVariable::new_idx(topo_vars[child], -1.0)); + problem.add_constraint(topo_constraint).unwrap(); + } + } + } + } else { + let mut color = HashMap::new(); + let mut path = Vec::new(); + get_all_cycles( + egraph, + &root, + &mut color, + &mut path, + &mut problem, + &node_vars, + ); + } } return ILPProblem::new(problem, egraph, root, node_vars); diff --git a/flexmatch/src/main.rs b/flexmatch/src/main.rs index f828b7a..cb4cabb 100644 --- a/flexmatch/src/main.rs +++ b/flexmatch/src/main.rs @@ -125,7 +125,8 @@ fn main() { let output_file = PathBuf::from(&args[2]); let analysis_data_file = PathBuf::from(&args[3]); let use_custom_ilp = &args[args.len() - 1] == "--new-ilp"; - let use_ilp = &args[args.len() - 1] == "--ilp" || use_custom_ilp; + let use_topo_sort_ilp = &args[args.len() - 1] == "--topo-sort-ilp"; + let use_ilp = &args[args.len() - 1] == "--ilp" || use_custom_ilp || use_topo_sort_ilp; let use_maxsat = &args[args.len() - 1] == "--maxsat"; let config_files = if use_ilp || use_maxsat { &args[4..args.len() - 1] @@ -296,7 +297,7 @@ fn main() { &best, ); } else { - if use_custom_ilp { + if use_custom_ilp || use_topo_sort_ilp { println!("Extract using custom ILP cycle breaking"); let cplex_env = rplex::Env::new().unwrap(); let mut cost_fn = Costfn {}; @@ -306,6 +307,7 @@ fn main() { root_expr, &runner.egraph, true, + use_topo_sort_ilp, move |x, y, z| cost_fn.node_cost(x, y, z), ); let (solve_time, _, best) = problem.solve(); From f6a63e94b49bd308f3aab6008662fc869b85d23f Mon Sep 17 00:00:00 2001 From: AD1024 Date: Sun, 5 Mar 2023 14:34:03 -0500 Subject: [PATCH 10/18] simplify --- flexmatch/src/ilp_extract.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/flexmatch/src/ilp_extract.rs b/flexmatch/src/ilp_extract.rs index 844bc0e..0e4ec18 100644 --- a/flexmatch/src/ilp_extract.rs +++ b/flexmatch/src/ilp_extract.rs @@ -234,7 +234,6 @@ where topo_vars.insert(eclass.id, problem.add_variable(var).unwrap()); } // topolotical ordering - // let mut memo = HashSet::new(); for eclass in egraph.classes() { for enode in eclass.nodes.iter() { for child in enode.children().iter() { From cb8c9b5aae4294c30d748ced1f95e290bbec0ebd Mon Sep 17 00:00:00 2001 From: AD1024 Date: Sun, 5 Mar 2023 15:27:34 -0500 Subject: [PATCH 11/18] add eval script and eval mode --- flexmatch/src/main.rs | 184 ++++++++++++++++++++---------------------- flexmatch/test.sh | 7 +- 2 files changed, 93 insertions(+), 98 deletions(-) mode change 100644 => 100755 flexmatch/test.sh diff --git a/flexmatch/src/main.rs b/flexmatch/src/main.rs index cb4cabb..82d9f90 100644 --- a/flexmatch/src/main.rs +++ b/flexmatch/src/main.rs @@ -91,18 +91,24 @@ fn save_expr_and_analysis( } fn save_extraction_stats( - algo: &'static str, - stat_file: &String, + algo: &str, + model_name: &String, best_cost: f64, solver_time: u128, extract_time: u128, + egraph: &EGraph, ) { - let output_file = PathBuf::from(env::current_dir().unwrap()).join(stat_file); + let output_file = PathBuf::from(env::current_dir().unwrap()).join("extraction_stats.txt"); let stat = json!({ "algo": algo, "best_cost": best_cost, + "model": model_name, "solver_time": solver_time, "extract_time": extract_time, + "num_enodes:": egraph.total_number_of_nodes(), + "num_eclass": egraph.number_of_classes(), + "eclass_size": egraph.total_size(), + "avg_enode_per_class": egraph.total_number_of_nodes() as f64 / egraph.number_of_classes() as f64, }); let mut file = OpenOptions::new() .write(true) @@ -124,10 +130,12 @@ fn main() { let source_file = &args[1]; let output_file = PathBuf::from(&args[2]); let analysis_data_file = PathBuf::from(&args[3]); - let use_custom_ilp = &args[args.len() - 1] == "--new-ilp"; - let use_topo_sort_ilp = &args[args.len() - 1] == "--topo-sort-ilp"; - let use_ilp = &args[args.len() - 1] == "--ilp" || use_custom_ilp || use_topo_sort_ilp; - let use_maxsat = &args[args.len() - 1] == "--maxsat"; + let run_eval = &args[args.len() - 1] == "--eval"; + let use_custom_ilp = &args[args.len() - 1] == "--new-ilp" || run_eval; + let use_topo_sort_ilp = &args[args.len() - 1] == "--topo-sort-ilp" || run_eval; + let use_ilp = + &args[args.len() - 1] == "--ilp" || use_custom_ilp || use_topo_sort_ilp || run_eval; + let use_maxsat = &args[args.len() - 1] == "--maxsat" || run_eval; let config_files = if use_ilp || use_maxsat { &args[4..args.len() - 1] } else { @@ -249,7 +257,7 @@ fn main() { return get_node_weights(enode, egraph.total_size() as f64); } } - if !use_ilp && !use_maxsat { + if (!use_ilp && !use_maxsat) || run_eval { info!("Extraction without ILP"); let extractor = Extractor::new( &runner.egraph, @@ -272,107 +280,89 @@ fn main() { } println!("Extraction time: {} ms", elapsed); println!("Cost: {}", cost); - save_expr_and_analysis( - output_file, - analysis_data_file, - &env, - &dtype_info.into_iter().collect(), - &best, + // save_expr_and_analysis( + // output_file, + // analysis_data_file, + // &env, + // &dtype_info.into_iter().collect(), + // &best, + // ); + save_extraction_stats( + "Greedy", + source_file, + cost, + elapsed, + elapsed, + &runner.egraph, ); - } else { - if use_maxsat { - let mut maxsat_ext = MaxsatExtractor::new(&runner.egraph, "problem.wcnf".into()); + } + if use_maxsat { + let mut maxsat_ext = MaxsatExtractor::new(&runner.egraph, "problem.wcnf".into()); + let start = Instant::now(); + let mut problem = maxsat_ext.create_problem(root_expr, "problem", true, Costfn); + let (solve_time, cost, best) = problem.solve_with_refinement(); + let elapsed = start.elapsed().as_millis(); + println!("Extraction time: {} ms", elapsed); + println!("Solver time: {} ms", solve_time); + println!("Cost: {}", cost.unwrap()); + save_extraction_stats( + "WPMAXSAT", + source_file, + cost.unwrap(), + solve_time, + elapsed, + &runner.egraph, + ); + } + if use_custom_ilp || use_topo_sort_ilp { + let mut options = Vec::new(); + if use_custom_ilp { + options.push(("ACyc", false)); + } + if use_topo_sort_ilp { + options.push(("Topo", true)); + } + for (algo, topo_sort) in options { + println!("Extract using ILP-{}", algo); + let cplex_env = rplex::Env::new().unwrap(); + let mut cost_fn = Costfn {}; let start = Instant::now(); - let mut problem = maxsat_ext.create_problem(root_expr, "problem", true, Costfn); - let (solve_time, cost, best) = problem.solve_with_refinement(); + let mut problem = ilp_extract::create_problem( + &cplex_env, + root_expr, + &runner.egraph, + true, + topo_sort, + move |x, y, z| cost_fn.node_cost(x, y, z), + ); + let (solve_time, _, best) = problem.solve(); let elapsed = start.elapsed().as_millis(); + let mut tmp_egraph = EGraph::new(MyAnalysis { + name_to_shape: env.clone(), + name_to_dtype: dtype_info.iter().cloned().collect(), + }); + let root = tmp_egraph.add_expr(&best); + let mut maxsat_ext = + MaxsatExtractor::new(&tmp_egraph, "compare-original.wcnf".into()); + let mut problem = maxsat_ext.create_problem(root, "problem", true, Costfn); + let (_, cost, _) = problem.solve_with_refinement(); + println!("Extraction time: {} ms", elapsed); println!("Solver time: {} ms", solve_time); println!("Cost: {}", cost.unwrap()); - save_expr_and_analysis( - output_file, - analysis_data_file, - &env, - &dtype_info.into_iter().collect(), - &best, + save_extraction_stats( + format!("ILP-{}", algo).as_str(), + source_file, + cost.unwrap(), + solve_time, + elapsed, + &runner.egraph, ); - } else { - if use_custom_ilp || use_topo_sort_ilp { - println!("Extract using custom ILP cycle breaking"); - let cplex_env = rplex::Env::new().unwrap(); - let mut cost_fn = Costfn {}; - let start = Instant::now(); - let mut problem = ilp_extract::create_problem( - &cplex_env, - root_expr, - &runner.egraph, - true, - use_topo_sort_ilp, - move |x, y, z| cost_fn.node_cost(x, y, z), - ); - let (solve_time, _, best) = problem.solve(); - let elapsed = start.elapsed().as_millis(); - let mut tmp_egraph = EGraph::new(MyAnalysis { - name_to_shape: env.clone(), - name_to_dtype: dtype_info.iter().cloned().collect(), - }); - let root = tmp_egraph.add_expr(&best); - let mut maxsat_ext = - MaxsatExtractor::new(&tmp_egraph, "compare-original.wcnf".into()); - let mut problem = maxsat_ext.create_problem(root, "problem", true, Costfn); - let (_, cost, _) = problem.solve_with_refinement(); - - println!("Extraction time: {} ms", elapsed); - println!("Solver time: {} ms", solve_time); - println!("Cost: {}", cost.unwrap()); - } else { - #[cfg(feature = "cplex")] - { - println!("Extract using ILP"); - let cplex_env = rplex::Env::new().unwrap(); - let mut model = glenside::extraction::ilp::create_generic_egraph_lp_model( - &cplex_env, - &runner.egraph, - |_, _, _| true, - &[root_expr], - "ilp_ext", - ); - let result = model.problem.solve().unwrap(); - let (out_expr, _old_id_to_new_id_map) = - glenside::extraction::ilp::extract_single_expression( - &model, - &result.variables, - EGraph::new(MyAnalysis { - name_to_shape: env.clone(), - name_to_dtype: dtype_info.iter().cloned().collect(), - }), - ); - let mut maxsat_ext = - MaxsatExtractor::new(&out_expr, "compare-original.wcnf".into()); - let mut problem = - maxsat_ext.create_problem(root_expr, "problem", true, Costfn); - let (solve_time, cost, _) = problem.solve_with_refinement(); - // println!("{}", best); - println!("Solve time: {}", solve_time); - println!("Cost: {}", cost.unwrap()); - } - } } } } } -/* -fn check_accelerator_call_by_eid( - ch_id: &egg::Id, - egraph: &EGraph, -) -> bool { - match &egraph[*ch_id].data { - MyAnalysisData::AccessPattern(access) => access.contains_accelerator_calls, - _ => false, - } -} */ - fn get_node_weights(node: &glenside::language::Language, total_size: f64) -> f64 { if let glenside::language::Language::AcceleratorCall(_) = node { debug!("Accelerator-call encountered"); diff --git a/flexmatch/test.sh b/flexmatch/test.sh old mode 100644 new mode 100755 index 268ca89..1843910 --- a/flexmatch/test.sh +++ b/flexmatch/test.sh @@ -1 +1,6 @@ -cargo run ../tests/models/mobilenetv2.relay rewrite.json data.json vta-dense.json im2col.json --ilp +#!/bin/bash +models=(mobilenetv2.relay resmlp.relay resnet18.relay bert.relay efficientnet.relay resnet50_simplifyinference_from_pytorch.relay) + +for relay_file in ${models[@]}; do + cargo run --features cplex ../tests/models/$relay_file rewrite.json data.json vta-dense.json im2col.json --eval +done \ No newline at end of file From ac2b9d13f839aeb17eab291c8e4f06777b209729 Mon Sep 17 00:00:00 2001 From: AD1024 Date: Mon, 6 Mar 2023 12:21:51 -0500 Subject: [PATCH 12/18] add graphing script --- flexmatch/draw_graph.py | 85 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 85 insertions(+) create mode 100644 flexmatch/draw_graph.py diff --git a/flexmatch/draw_graph.py b/flexmatch/draw_graph.py new file mode 100644 index 0000000..e99ee6e --- /dev/null +++ b/flexmatch/draw_graph.py @@ -0,0 +1,85 @@ +import matplotlib +matplotlib.use('agg') +import matplotlib.pyplot as plt +import numpy as np +import json + +def parse_data(filename: str) -> dict: + with open(filename) as fp: + data = fp.read().splitlines() + parsed_data = list(map(json.loads, data)) + + # aggregate w.r.t. model + data = dict() + for x in parsed_data: + key = x['model'].split('/')[-1].split('.')[0] + datum = data.get(key, []) + datum.append(x) + data[key] = datum + return data + +def draw_extraction_times(data: dict): + # plt.clf() + plt.title('End-to-end Term Extraction Time') + plt.xlabel('Model') + fig, ax = plt.subplots() + ax.set_ylabel('Extraction Time (ms)') + ax.set_xlabel('Model', fontsize=14) + ax.set_title('End-to-end Term Extraction Time') + # ax.set_yscale('log') + x = np.arange(len(data)) + # x *= 1.5 + + solver_times = dict() + overhead_times = dict() + x_ticks = [] + for (model, model_data) in data.items(): + x_ticks.append(model) + for datum in model_data: + if datum['algo'] not in solver_times: + solver_times[datum['algo']] = [] + overhead_times[datum['algo']] = [] + solver_times[datum['algo']].append(datum['solver_time']) + overhead_times[datum['algo']].append(datum['extract_time'] - datum['solver_time']) + + bar_width = 0.25 + ax.bar(x - bar_width, solver_times['ILP-ACyc'], bar_width, label='ILP-ACyc', color='lightgreen', edgecolor='grey') + overhead = ax.bar(x - bar_width, overhead_times['ILP-ACyc'], bar_width, bottom=solver_times['ILP-ACyc'], color='slateblue', label='Overhead', hatch='//', edgecolor='grey') + + ax.bar(x, solver_times['WPMAXSAT'], bar_width, label='WPMAXSAT', color='lightpink', edgecolor='grey') + overhead = ax.bar(x, overhead_times['WPMAXSAT'], bar_width, bottom=solver_times['WPMAXSAT'], color='slateblue', hatch='//', edgecolor='grey') + + ax.bar(x + bar_width, solver_times['ILP-Topo'], bar_width, label='ILP-Topo', color='lightblue', edgecolor='grey') + overhead= ax.bar(x + bar_width, overhead_times['ILP-Topo'], bar_width, bottom=solver_times['ILP-Topo'], color='slateblue', hatch='//', edgecolor='grey') + + ax.set_xticks(x, data.keys()) + ax.set_xticklabels(x_ticks) + ax.legend(loc='upper left') + plt.savefig('extraction_time.png') + +def draw_egraph_sizes(data: dict): + plt.clf() + plt.title('EGraph Stats After Equality Saturation') + fig, (ax1, ax2) = plt.subplots(1, 2) + num_eclasses = [] + num_enodes = [] + xticks = [] + for (model, model_data) in data.items(): + xticks.append(model) + num_eclasses.append(model_data[0]['num_eclass']) + num_enodes.append(model_data[0]['num_enodes']) + tick_loc = np.arange(len(xticks)) + tick_loc *= 2 + ax1.bar(tick_loc, num_eclasses, width=1) + ax1.set_xticks(tick_loc, xticks, rotation=90) + ax1.set_title('Number of EClasses') + ax2.bar(tick_loc, num_enodes, width=1) + ax2.set_xticks(tick_loc, xticks, rotation=90) + ax2.set_title('Number of ENodes') + plt.tight_layout() + plt.savefig('egraph_stats.png') + +if __name__ == '__main__': + data = parse_data('extraction_stats.txt') + draw_extraction_times(data) + draw_egraph_sizes(data) \ No newline at end of file From 5c06eab6f157b2a23c077e3cb3b396819f42072b Mon Sep 17 00:00:00 2001 From: AD1024 Date: Mon, 6 Mar 2023 15:04:07 -0500 Subject: [PATCH 13/18] fix stats gen --- flexmatch/draw_graph.py | 30 ++++++++++++++++++++++++------ flexmatch/src/main.rs | 3 +-- flexmatch/test.sh | 4 ++-- 3 files changed, 27 insertions(+), 10 deletions(-) diff --git a/flexmatch/draw_graph.py b/flexmatch/draw_graph.py index e99ee6e..5a44390 100644 --- a/flexmatch/draw_graph.py +++ b/flexmatch/draw_graph.py @@ -12,7 +12,7 @@ def parse_data(filename: str) -> dict: # aggregate w.r.t. model data = dict() for x in parsed_data: - key = x['model'].split('/')[-1].split('.')[0] + key = x['model'].split('/')[-1].split('.')[0].split('_')[0] datum = data.get(key, []) datum.append(x) data[key] = datum @@ -20,12 +20,12 @@ def parse_data(filename: str) -> dict: def draw_extraction_times(data: dict): # plt.clf() - plt.title('End-to-end Term Extraction Time') + plt.title('Term Extraction Time') plt.xlabel('Model') fig, ax = plt.subplots() ax.set_ylabel('Extraction Time (ms)') ax.set_xlabel('Model', fontsize=14) - ax.set_title('End-to-end Term Extraction Time') + ax.set_title('Term Extraction Time') # ax.set_yscale('log') x = np.arange(len(data)) # x *= 1.5 @@ -35,12 +35,24 @@ def draw_extraction_times(data: dict): x_ticks = [] for (model, model_data) in data.items(): x_ticks.append(model) + counter = dict() for datum in model_data: + solver_time = datum['solver_time'] + overhead_time = datum['extract_time'] - datum['solver_time'] + counter[datum['algo']] = counter.get(datum['algo'], 0) if datum['algo'] not in solver_times: solver_times[datum['algo']] = [] overhead_times[datum['algo']] = [] - solver_times[datum['algo']].append(datum['solver_time']) - overhead_times[datum['algo']].append(datum['extract_time'] - datum['solver_time']) + if counter[datum['algo']] == 0: + solver_times[datum['algo']].append(solver_time) + overhead_times[datum['algo']].append(overhead_time) + else: + solver_times[datum['algo']][-1] += solver_time + overhead_times[datum['algo']][-1] += overhead_time + counter[datum['algo']] += 1 + for (algo, count) in counter.items(): + solver_times[algo][-1] /= count + overhead_times[algo][-1] /= count bar_width = 0.25 ax.bar(x - bar_width, solver_times['ILP-ACyc'], bar_width, label='ILP-ACyc', color='lightgreen', edgecolor='grey') @@ -54,7 +66,13 @@ def draw_extraction_times(data: dict): ax.set_xticks(x, data.keys()) ax.set_xticklabels(x_ticks) - ax.legend(loc='upper left') + + box = ax.get_position() + ax.set_position([box.x0, box.y0 + box.height * 0.1, + box.width, box.height * 0.9]) + + ax.legend(loc='upper center', bbox_to_anchor=(0.5, -0.05), + fancybox=True, shadow=True, ncol=5) plt.savefig('extraction_time.png') def draw_egraph_sizes(data: dict): diff --git a/flexmatch/src/main.rs b/flexmatch/src/main.rs index 82d9f90..de76fa3 100644 --- a/flexmatch/src/main.rs +++ b/flexmatch/src/main.rs @@ -105,9 +105,8 @@ fn save_extraction_stats( "model": model_name, "solver_time": solver_time, "extract_time": extract_time, - "num_enodes:": egraph.total_number_of_nodes(), + "num_enodes": egraph.total_number_of_nodes(), "num_eclass": egraph.number_of_classes(), - "eclass_size": egraph.total_size(), "avg_enode_per_class": egraph.total_number_of_nodes() as f64 / egraph.number_of_classes() as f64, }); let mut file = OpenOptions::new() diff --git a/flexmatch/test.sh b/flexmatch/test.sh index 1843910..26a0a82 100755 --- a/flexmatch/test.sh +++ b/flexmatch/test.sh @@ -1,6 +1,6 @@ #!/bin/bash -models=(mobilenetv2.relay resmlp.relay resnet18.relay bert.relay efficientnet.relay resnet50_simplifyinference_from_pytorch.relay) +models=(mobilenetv2.relay resmlp.relay resnet18.relay efficientnet.relay resnet50_simplifyinference_from_pytorch.relay) for relay_file in ${models[@]}; do cargo run --features cplex ../tests/models/$relay_file rewrite.json data.json vta-dense.json im2col.json --eval -done \ No newline at end of file +done From 6bd17d345c4d7dbc06098763a93beb85faf67356 Mon Sep 17 00:00:00 2001 From: AD1024 Date: Mon, 13 Mar 2023 15:13:06 -0400 Subject: [PATCH 14/18] compare with removing redaundant constraints --- flexmatch/draw_graph.py | 5 +++ flexmatch/src/ilp_extract.rs | 54 ++++++++++++++++++++++----------- flexmatch/src/main.rs | 11 ++++++- flexmatch/src/maxsat_extract.rs | 26 +++++++++++++--- flexmatch/src/rewrites.rs | 1 + 5 files changed, 75 insertions(+), 22 deletions(-) diff --git a/flexmatch/draw_graph.py b/flexmatch/draw_graph.py index 5a44390..3d0b810 100644 --- a/flexmatch/draw_graph.py +++ b/flexmatch/draw_graph.py @@ -64,6 +64,11 @@ def draw_extraction_times(data: dict): ax.bar(x + bar_width, solver_times['ILP-Topo'], bar_width, label='ILP-Topo', color='lightblue', edgecolor='grey') overhead= ax.bar(x + bar_width, overhead_times['ILP-Topo'], bar_width, bottom=solver_times['ILP-Topo'], color='slateblue', hatch='//', edgecolor='grey') + print((np.array(solver_times['ILP-Topo']) + overhead_times['ILP-Topo']) / (np.array(solver_times['ILP-ACyc']) + overhead_times['ILP-ACyc'])) + print((np.array(solver_times['ILP-Topo']) + overhead_times['ILP-Topo']) / (np.array(solver_times['WPMAXSAT']) + overhead_times['WPMAXSAT'])) + # print(solver_times['ILP-ACyc']) + # print(solver_times['WPMAXSAT']) + ax.set_xticks(x, data.keys()) ax.set_xticklabels(x_ticks) diff --git a/flexmatch/src/ilp_extract.rs b/flexmatch/src/ilp_extract.rs index 0e4ec18..9d19983 100644 --- a/flexmatch/src/ilp_extract.rs +++ b/flexmatch/src/ilp_extract.rs @@ -1,4 +1,7 @@ -use std::{collections::HashMap, time::Instant}; +use std::{ + collections::{HashMap, HashSet}, + time::Instant, +}; use egg::{Analysis, EGraph, Id, Language, RecExpr}; use rand::Rng; @@ -11,6 +14,7 @@ fn get_all_cycles<'a, L, N>( path: &mut Vec<(Id, L)>, problem: &mut Problem<'a>, node_vars: &HashMap, + node_to_children: &HashMap>, ) where L: Language, N: Analysis, @@ -22,8 +26,8 @@ fn get_all_cycles<'a, L, N>( if let Some((idx, _)) = path.iter().enumerate().find(|(_, (id, _))| id == root) { let mut new_cycle = Vec::new(); let subpath = path[idx..].to_vec(); - for (_, n) in subpath { - new_cycle.push(node_vars[&n]); + for (_, n) in &subpath { + new_cycle.push(node_vars[n]); } let mut rng = rand::thread_rng(); if new_cycle.len() == 1 { @@ -35,18 +39,21 @@ fn get_all_cycles<'a, L, N>( constraint.add_wvar(WeightedVariable::new_idx(new_cycle[0], 1.0)); problem.add_constraint(constraint).unwrap(); } else { - for node_idx in egraph[*root].nodes.iter().map(|x| node_vars[x]) { - new_cycle[0] = node_idx; - // sum up <= len(new_cycle) - 1 - let mut constraint = rplex::Constraint::new( - rplex::ConstraintType::LessThanEq, - new_cycle.len() as f64 - 1.0, - format!("cycle_{}_{}", root, rng.gen::()), - ); - for node_idx in new_cycle.iter() { - constraint.add_wvar(WeightedVariable::new_idx(*node_idx, 1.0)); + let nxt_hop = subpath[1].0; + for node_idx in egraph[*root].nodes.iter().map(|n| node_vars[n]) { + if node_to_children[&node_idx].contains(&nxt_hop) { + new_cycle[0] = node_idx; + // sum up <= len(new_cycle) - 1 + let mut constraint = rplex::Constraint::new( + rplex::ConstraintType::LessThanEq, + new_cycle.len() as f64 - 1.0, + format!("cycle_{}_{}", root, rng.gen::()), + ); + for node_idx in new_cycle.iter() { + constraint.add_wvar(WeightedVariable::new_idx(*node_idx, 1.0)); + } + problem.add_constraint(constraint).unwrap(); } - problem.add_constraint(constraint).unwrap(); } } return; @@ -55,11 +62,19 @@ fn get_all_cycles<'a, L, N>( } color.insert(*root, 1); for node in egraph[*root].nodes.iter() { + path.push((*root, node.clone())); for ch in node.children() { - path.push((*root, node.clone())); - get_all_cycles(egraph, ch, color, path, problem, node_vars); - path.pop(); + get_all_cycles( + egraph, + ch, + color, + path, + problem, + node_vars, + node_to_children, + ); } + path.pop(); } color.insert(*root, 2); } @@ -203,12 +218,15 @@ where constraint.add_wvar(WeightedVariable::new_idx(node_idx, 1.0)); } problem.add_constraint(constraint).unwrap(); + let mut node_to_children = HashMap::new(); // children constraint for eclass in egraph.classes() { for node in egraph[eclass.id].nodes.iter() { let node_idx = node_vars[node]; + let mut node_children_set = HashSet::new(); for (ch_idx, ch) in node.children().iter().enumerate() { + node_children_set.insert(*ch); let mut constraint = rplex::Constraint::new( rplex::ConstraintType::GreaterThanEq, 0.0, @@ -220,6 +238,7 @@ where } problem.add_constraint(constraint).unwrap(); } + node_to_children.insert(node_idx, node_children_set); } } @@ -260,6 +279,7 @@ where &mut path, &mut problem, &node_vars, + &node_to_children, ); } } diff --git a/flexmatch/src/main.rs b/flexmatch/src/main.rs index de76fa3..8f559eb 100644 --- a/flexmatch/src/main.rs +++ b/flexmatch/src/main.rs @@ -142,7 +142,16 @@ fn main() { }; let aggregated_configs = read_configs(&flexmatch_home, config_files); - let mut rewrites = vec![]; + let mut rewrites = vec![ + // glenside::language::rewrites::collapse_nested_transposes(), + // glenside::language::rewrites::simplify_multiple_transposes(), + // glenside::language::rewrites::simplify_multiple_accesses(), + // glenside::language::rewrites::simplify_reduce_max(), + // glenside::language::rewrites::bubble_access_reshape_through_compute_reduce_max(), + // glenside::language::rewrites::simplify_multiple_access_reshapes(), + // glenside::language::rewrites::collapse_nested_accesses(), + // glenside::language::rewrites::flatten_dot_product_to_dense(), + ]; let mut rewrite_set = HashSet::new(); debug!("{:?}", aggregated_configs); for config in aggregated_configs.iter() { diff --git a/flexmatch/src/maxsat_extract.rs b/flexmatch/src/maxsat_extract.rs index dccc0dc..213e862 100644 --- a/flexmatch/src/maxsat_extract.rs +++ b/flexmatch/src/maxsat_extract.rs @@ -20,6 +20,7 @@ fn get_all_cycles( path: &mut Vec<(Id, L)>, problem_writer: &mut ProblemWriter, node_vars: &HashMap, + node_to_children: &HashMap>, top: f64, ) where L: Language, @@ -32,15 +33,18 @@ fn get_all_cycles( if let Some((idx, _)) = path.iter().enumerate().find(|(_, (id, _))| id == root) { let mut new_cycle = Vec::new(); let subpath = path[idx..].to_vec(); - for (_, n) in subpath { + for (_, n) in &subpath { new_cycle.push(node_vars[&n]); } if new_cycle.len() == 1 { problem_writer.hard_clause(&format!("-{}", new_cycle[0]), top); } else { + let nxt_hop = subpath[1].0; for node_idx in egraph[*root].nodes.iter().map(|x| node_vars[x]) { - new_cycle[0] = node_idx; - disjuct_negative(&new_cycle, problem_writer, top); + // if node_to_children[&node_idx].contains(&nxt_hop) { + new_cycle[0] = node_idx; + disjuct_negative(&new_cycle, problem_writer, top); + // } } } return; @@ -53,7 +57,16 @@ fn get_all_cycles( // let mut to_here = path.clone(); // to_here.push((*root, node.clone())); path.push((*root, node.clone())); - get_all_cycles(egraph, ch, color, path, problem_writer, node_vars, top); + get_all_cycles( + egraph, + ch, + color, + path, + problem_writer, + node_vars, + node_to_children, + top, + ); path.pop(); } } @@ -354,11 +367,14 @@ where .join(" "); hard_clauses.push(root_clause); + let mut node_to_children = HashMap::new(); // children constraint for c in self.egraph.classes() { for n in c.nodes.iter() { // v_n -> \bigvee_cN v_cN forall C + let mut node_children = HashSet::new(); for ch in n.children() { + node_children.insert(*ch); let mut clause = String::new(); clause.push_str(&format!("-{}", node_vars[n])); for ch_node in self.egraph[*ch].nodes.iter() { @@ -366,6 +382,7 @@ where } hard_clauses.push(clause); } + node_to_children.insert(node_vars[n], node_children); } } @@ -380,6 +397,7 @@ where &mut path, &mut self.writer, &node_vars, + &node_to_children, top, ); } diff --git a/flexmatch/src/rewrites.rs b/flexmatch/src/rewrites.rs index 24df658..1cee0fd 100644 --- a/flexmatch/src/rewrites.rs +++ b/flexmatch/src/rewrites.rs @@ -22,6 +22,7 @@ pub fn get_rewrite_from_string(name: &String, args: &Box<[i32]>) -> Rewrite simplify_multiple_access_reshapes(), "bubble-access-through-access-transpose" => bubble_access_through_access_transpose(), "simplify-reduce-max" => simplify_reduce_max(), + "collapse-nested-transposes" => collapse_nested_transposes(), "flex-linear-rewrite" => linear_layer_accelerator_rewrites(), "flex-linear-dense" => dot_product_to_linear(), From d77dd96ecb0e3d5444a74494180ffa30e9700e05 Mon Sep 17 00:00:00 2001 From: AD1024 Date: Tue, 14 Mar 2023 01:20:14 -0400 Subject: [PATCH 15/18] add simplification rewrites --- configs/simpl.json | 14 +++ flexmatch/Cargo.toml | 1 + flexmatch/run_with_im2col.sh | 11 ++ flexmatch/run_with_opt.sh | 16 +++ flexmatch/src/ilp_extract.rs | 45 ++++---- flexmatch/src/main.rs | 183 ++++++++++++++++++++++++-------- flexmatch/src/maxsat_extract.rs | 4 +- 7 files changed, 203 insertions(+), 71 deletions(-) create mode 100644 configs/simpl.json create mode 100755 flexmatch/run_with_im2col.sh create mode 100755 flexmatch/run_with_opt.sh diff --git a/configs/simpl.json b/configs/simpl.json new file mode 100644 index 0000000..b12580b --- /dev/null +++ b/configs/simpl.json @@ -0,0 +1,14 @@ +{ + "rewrites": { + "simplify-multiple-accesses": [], + "simplify-multiple-transposes": [], + "simplify-multiple-access-reshapes": [], + "bubble-access-through-access-transpose": [], + "simplify-reduce-max": [], + "collapse-nested-transposes": [] + }, + "composites": {}, + "compilers": {}, + "debug_functions": {}, + "out_dtypes": {} +} \ No newline at end of file diff --git a/flexmatch/Cargo.toml b/flexmatch/Cargo.toml index ddf5fa5..a5b560a 100644 --- a/flexmatch/Cargo.toml +++ b/flexmatch/Cargo.toml @@ -15,6 +15,7 @@ serde = "1.0.130" log = "0.4.14" env_logger = "0.9.0" rand = "0.8.5" +coin_cbc = "0.1.6" [dependencies.glenside] git = "https://github.com/gussmith23/glenside" diff --git a/flexmatch/run_with_im2col.sh b/flexmatch/run_with_im2col.sh new file mode 100755 index 0000000..20560c1 --- /dev/null +++ b/flexmatch/run_with_im2col.sh @@ -0,0 +1,11 @@ +#!/bin/bash +models=(mobilenetv2.relay resmlp.relay resnet18.relay efficientnet.relay resnet50_simplifyinference_from_pytorch.relay) +cargo build --features cplex +echo "Run EqSat + Extraction with Im2Col alone" +for i in {1..5}; do + for relay_file in ${models[@]}; do + ./target/debug/flexmatch ../tests/models/$relay_file rewrite.json data.json im2col.json --eval + done +done + +mv extraction_stats.txt extraction_stats_im2col.txt \ No newline at end of file diff --git a/flexmatch/run_with_opt.sh b/flexmatch/run_with_opt.sh new file mode 100755 index 0000000..ff70303 --- /dev/null +++ b/flexmatch/run_with_opt.sh @@ -0,0 +1,16 @@ +#!/bin/bash +models=(mobilenetv2.relay resmlp.relay resnet18.relay efficientnet.relay resnet50_simplifyinference_from_pytorch.relay) +cargo build --features cplex +echo "Run EqSat + Extraction with Im2Col + Simplifications" +for i in {1..5}; do + for relay_file in ${models[@]}; do + echo ">>> Extract with WPMAXSAT" + timeout 20 ./target/debug/flexmatch ../tests/models/$relay_file rewrite.json data.json simpl.json im2col.json --maxsat + echo ">>> Extract with ILP-ACyc" + timeout 20 ./target/debug/flexmatch ../tests/models/$relay_file rewrite.json data.json simpl.json im2col.json --new-ilp + echo ">>> Extract with ILP-Topo" + timeout 20 ./target/debug/flexmatch ../tests/models/$relay_file rewrite.json data.json simpl.json im2col.json --topo-sort-ilp + done +done + +mv extraction_stats.txt extraction_stats_im2col_with_simpl.txt \ No newline at end of file diff --git a/flexmatch/src/ilp_extract.rs b/flexmatch/src/ilp_extract.rs index 9d19983..922b925 100644 --- a/flexmatch/src/ilp_extract.rs +++ b/flexmatch/src/ilp_extract.rs @@ -14,7 +14,7 @@ fn get_all_cycles<'a, L, N>( path: &mut Vec<(Id, L)>, problem: &mut Problem<'a>, node_vars: &HashMap, - node_to_children: &HashMap>, + // node_to_children: &HashMap>, ) where L: Language, N: Analysis, @@ -41,19 +41,19 @@ fn get_all_cycles<'a, L, N>( } else { let nxt_hop = subpath[1].0; for node_idx in egraph[*root].nodes.iter().map(|n| node_vars[n]) { - if node_to_children[&node_idx].contains(&nxt_hop) { - new_cycle[0] = node_idx; - // sum up <= len(new_cycle) - 1 - let mut constraint = rplex::Constraint::new( - rplex::ConstraintType::LessThanEq, - new_cycle.len() as f64 - 1.0, - format!("cycle_{}_{}", root, rng.gen::()), - ); - for node_idx in new_cycle.iter() { - constraint.add_wvar(WeightedVariable::new_idx(*node_idx, 1.0)); - } - problem.add_constraint(constraint).unwrap(); + // if node_to_children[&node_idx].contains(&nxt_hop) { + new_cycle[0] = node_idx; + // sum up <= len(new_cycle) - 1 + let mut constraint = rplex::Constraint::new( + rplex::ConstraintType::LessThanEq, + new_cycle.len() as f64 - 1.0, + format!("cycle_{}_{}", root, rng.gen::()), + ); + for node_idx in new_cycle.iter() { + constraint.add_wvar(WeightedVariable::new_idx(*node_idx, 1.0)); } + problem.add_constraint(constraint).unwrap(); + // } } } return; @@ -65,13 +65,8 @@ fn get_all_cycles<'a, L, N>( path.push((*root, node.clone())); for ch in node.children() { get_all_cycles( - egraph, - ch, - color, - path, - problem, - node_vars, - node_to_children, + egraph, ch, color, path, problem, node_vars, + // node_to_children, ); } path.pop(); @@ -218,15 +213,15 @@ where constraint.add_wvar(WeightedVariable::new_idx(node_idx, 1.0)); } problem.add_constraint(constraint).unwrap(); - let mut node_to_children = HashMap::new(); + // let mut node_to_children = HashMap::new(); // children constraint for eclass in egraph.classes() { for node in egraph[eclass.id].nodes.iter() { let node_idx = node_vars[node]; - let mut node_children_set = HashSet::new(); + // let mut node_children_set = HashSet::new(); for (ch_idx, ch) in node.children().iter().enumerate() { - node_children_set.insert(*ch); + // node_children_set.insert(*ch); let mut constraint = rplex::Constraint::new( rplex::ConstraintType::GreaterThanEq, 0.0, @@ -238,7 +233,7 @@ where } problem.add_constraint(constraint).unwrap(); } - node_to_children.insert(node_idx, node_children_set); + // node_to_children.insert(node_idx, node_children_set); } } @@ -279,7 +274,7 @@ where &mut path, &mut problem, &node_vars, - &node_to_children, + // &node_to_children, ); } } diff --git a/flexmatch/src/main.rs b/flexmatch/src/main.rs index 8f559eb..58af922 100644 --- a/flexmatch/src/main.rs +++ b/flexmatch/src/main.rs @@ -1,3 +1,4 @@ +mod egg_lp_extract; mod ilp_extract; mod maxsat_extract; mod rewrites; @@ -36,6 +37,18 @@ struct RewriteConfig { out_dtypes: HashMap, } +struct Costfn; +impl MaxsatCostFunction for Costfn { + fn node_cost( + &mut self, + egraph: &EGraph, + _: egg::Id, + enode: &glenside::language::Language, + ) -> f64 { + return get_node_weights(enode, egraph.total_size() as f64); + } +} + fn read_configs(flexmatch_home: &PathBuf, config_files: &[String]) -> Vec { let mut result: Vec = Vec::default(); for config in config_files { @@ -118,6 +131,59 @@ fn save_extraction_stats( writeln!(file, "{}", stat).unwrap(); } +fn extract_with_ilp_topo( + root: egg::Id, + egraph: &EGraph, +) -> (u128, u128, egg::RecExpr) { + println!("Extract using ILP-Topo"); + let mut cost_fn = Costfn {}; + let cplex_env = rplex::Env::new().unwrap(); + let start = Instant::now(); + let mut problem = + ilp_extract::create_problem(&cplex_env, root, &egraph, true, true, move |x, y, z| { + cost_fn.node_cost(x, y, z) + }); + let (solve_time, _, best) = problem.solve(); + let elapsed = start.elapsed().as_millis(); + return (solve_time, elapsed, best); +} + +fn extract_with_ilp_acyc( + root: egg::Id, + egraph: &EGraph, +) -> (u128, u128, egg::RecExpr) { + println!("Extract using ILP-ACyc"); + let mut cost_fn = Costfn {}; + let cplex_env = rplex::Env::new().unwrap(); + let start = Instant::now(); + let mut problem = + ilp_extract::create_problem(&cplex_env, root, &egraph, true, false, move |x, y, z| { + cost_fn.node_cost(x, y, z) + }); + let (solve_time, _, best) = problem.solve(); + let elapsed = start.elapsed().as_millis(); + return (solve_time, elapsed, best); +} + +fn extract_with_maxsat( + root: egg::Id, + egraph: &EGraph, +) -> ( + u128, + u128, + Option, + egg::RecExpr, +) { + println!("Extract using WPMAXSAT"); + let mut cost_fn = Costfn {}; + let mut maxsat_ext = MaxsatExtractor::new(&egraph, "problem.wcnf".into()); + let start = Instant::now(); + let mut problem = maxsat_ext.create_problem(root, "problem", true, Costfn); + let (solve_time, cost, best) = problem.solve_with_refinement(); + let elapsed = start.elapsed().as_millis(); + return (solve_time, elapsed, cost, best); +} + fn main() { env_logger::init(); let args = env::args().collect::>(); @@ -254,17 +320,6 @@ fn main() { } info!("Root eclass analysis: {:?}", runner.egraph[root_expr].data); info!("Root eclass nodes: {:?}", runner.egraph[root_expr].nodes); - struct Costfn; - impl MaxsatCostFunction for Costfn { - fn node_cost( - &mut self, - egraph: &EGraph, - _: egg::Id, - enode: &glenside::language::Language, - ) -> f64 { - return get_node_weights(enode, egraph.total_size() as f64); - } - } if (!use_ilp && !use_maxsat) || run_eval { info!("Extraction without ILP"); let extractor = Extractor::new( @@ -305,46 +360,49 @@ fn main() { ); } if use_maxsat { - let mut maxsat_ext = MaxsatExtractor::new(&runner.egraph, "problem.wcnf".into()); - let start = Instant::now(); - let mut problem = maxsat_ext.create_problem(root_expr, "problem", true, Costfn); - let (solve_time, cost, best) = problem.solve_with_refinement(); - let elapsed = start.elapsed().as_millis(); - println!("Extraction time: {} ms", elapsed); - println!("Solver time: {} ms", solve_time); + let (solver_time, extract_time, cost, best) = + extract_with_maxsat(root_expr, &runner.egraph); + println!("Solver time: {} ms", solver_time); + println!("Extraction time: {} ms", extract_time); println!("Cost: {}", cost.unwrap()); save_extraction_stats( "WPMAXSAT", source_file, cost.unwrap(), - solve_time, - elapsed, + solver_time, + extract_time, &runner.egraph, ); } if use_custom_ilp || use_topo_sort_ilp { - let mut options = Vec::new(); if use_custom_ilp { - options.push(("ACyc", false)); - } - if use_topo_sort_ilp { - options.push(("Topo", true)); - } - for (algo, topo_sort) in options { - println!("Extract using ILP-{}", algo); - let cplex_env = rplex::Env::new().unwrap(); - let mut cost_fn = Costfn {}; - let start = Instant::now(); - let mut problem = ilp_extract::create_problem( - &cplex_env, - root_expr, + let (solver_time, extract_time, best) = + extract_with_ilp_acyc(root_expr, &runner.egraph); + let mut tmp_egraph = EGraph::new(MyAnalysis { + name_to_shape: env.clone(), + name_to_dtype: dtype_info.iter().cloned().collect(), + }); + let root = tmp_egraph.add_expr(&best); + let mut maxsat_ext = + MaxsatExtractor::new(&tmp_egraph, "compare-original.wcnf".into()); + let mut problem = maxsat_ext.create_problem(root, "problem", true, Costfn); + let (_, cost, _) = problem.solve_with_refinement(); + + println!("Extraction time: {} ms", extract_time); + println!("Solver time: {} ms", solver_time); + println!("Cost: {}", cost.unwrap()); + save_extraction_stats( + "ILP-ACyc", + source_file, + cost.unwrap(), + solver_time, + extract_time, &runner.egraph, - true, - topo_sort, - move |x, y, z| cost_fn.node_cost(x, y, z), ); - let (solve_time, _, best) = problem.solve(); - let elapsed = start.elapsed().as_millis(); + } + if use_topo_sort_ilp { + let (solver_time, extract_time, best) = + extract_with_ilp_topo(root_expr, &runner.egraph); let mut tmp_egraph = EGraph::new(MyAnalysis { name_to_shape: env.clone(), name_to_dtype: dtype_info.iter().cloned().collect(), @@ -355,18 +413,55 @@ fn main() { let mut problem = maxsat_ext.create_problem(root, "problem", true, Costfn); let (_, cost, _) = problem.solve_with_refinement(); - println!("Extraction time: {} ms", elapsed); - println!("Solver time: {} ms", solve_time); + println!("Extraction time: {} ms", extract_time); + println!("Solver time: {} ms", solver_time); println!("Cost: {}", cost.unwrap()); save_extraction_stats( - format!("ILP-{}", algo).as_str(), + "ILP-Topo", source_file, cost.unwrap(), - solve_time, - elapsed, + solver_time, + extract_time, &runner.egraph, ); } + // for (algo, topo_sort) in options { + // println!("Extract using ILP-{}", algo); + // let cplex_env = rplex::Env::new().unwrap(); + // let mut cost_fn = Costfn {}; + // let start = Instant::now(); + // let mut problem = ilp_extract::create_problem( + // &cplex_env, + // root_expr, + // &runner.egraph, + // true, + // topo_sort, + // move |x, y, z| cost_fn.node_cost(x, y, z), + // ); + // let (solve_time, _, best) = problem.solve(); + // let elapsed = start.elapsed().as_millis(); + // let mut tmp_egraph = EGraph::new(MyAnalysis { + // name_to_shape: env.clone(), + // name_to_dtype: dtype_info.iter().cloned().collect(), + // }); + // let root = tmp_egraph.add_expr(&best); + // let mut maxsat_ext = + // MaxsatExtractor::new(&tmp_egraph, "compare-original.wcnf".into()); + // let mut problem = maxsat_ext.create_problem(root, "problem", true, Costfn); + // let (_, cost, _) = problem.solve_with_refinement(); + + // println!("Extraction time: {} ms", elapsed); + // println!("Solver time: {} ms", solve_time); + // println!("Cost: {}", cost.unwrap()); + // save_extraction_stats( + // format!("ILP-{}", algo).as_str(), + // source_file, + // cost.unwrap(), + // solve_time, + // elapsed, + // &runner.egraph, + // ); + // } } } } diff --git a/flexmatch/src/maxsat_extract.rs b/flexmatch/src/maxsat_extract.rs index 213e862..7c399a4 100644 --- a/flexmatch/src/maxsat_extract.rs +++ b/flexmatch/src/maxsat_extract.rs @@ -42,8 +42,8 @@ fn get_all_cycles( let nxt_hop = subpath[1].0; for node_idx in egraph[*root].nodes.iter().map(|x| node_vars[x]) { // if node_to_children[&node_idx].contains(&nxt_hop) { - new_cycle[0] = node_idx; - disjuct_negative(&new_cycle, problem_writer, top); + new_cycle[0] = node_idx; + disjuct_negative(&new_cycle, problem_writer, top); // } } } From e230fc028225ad47f505218589f403a962da219a Mon Sep 17 00:00:00 2001 From: AD1024 Date: Tue, 14 Mar 2023 01:21:04 -0400 Subject: [PATCH 16/18] add data got from runs on the sat-10 server --- flexmatch/extraction_stats_im2col.txt | 148 ++++++++++++++++++ .../extraction_stats_im2col_with_simpl.txt | 79 ++++++++++ 2 files changed, 227 insertions(+) create mode 100644 flexmatch/extraction_stats_im2col.txt create mode 100644 flexmatch/extraction_stats_im2col_with_simpl.txt diff --git a/flexmatch/extraction_stats_im2col.txt b/flexmatch/extraction_stats_im2col.txt new file mode 100644 index 0000000..24088e1 --- /dev/null +++ b/flexmatch/extraction_stats_im2col.txt @@ -0,0 +1,148 @@ +{"algo":"Greedy","avg_enode_per_class":1.8799665680853799,"best_cost":2056.0,"extract_time":4,"model":"../tests/models/mobilenetv2.relay","num_eclass":15554,"num_enodes":29241,"solver_time":4} +{"algo":"WPMAXSAT","avg_enode_per_class":1.8799665680853799,"best_cost":1685.0,"extract_time":5037,"model":"../tests/models/mobilenetv2.relay","num_eclass":15554,"num_enodes":29241,"solver_time":4147} +{"algo":"ILP-ACyc","avg_enode_per_class":1.8799665680853799,"best_cost":1685.0,"extract_time":1149,"model":"../tests/models/mobilenetv2.relay","num_eclass":15554,"num_enodes":29241,"solver_time":323} +{"algo":"ILP-Topo","avg_enode_per_class":1.8799665680853799,"best_cost":1685.0,"extract_time":5817,"model":"../tests/models/mobilenetv2.relay","num_eclass":15554,"num_enodes":29241,"solver_time":5023} +{"algo":"Greedy","avg_enode_per_class":1.8888600868381829,"best_cost":2056.0,"extract_time":4,"model":"../tests/models/mobilenetv2.relay","num_eclass":15431,"num_enodes":29147,"solver_time":4} +{"algo":"WPMAXSAT","avg_enode_per_class":1.8888600868381829,"best_cost":1685.0,"extract_time":4978,"model":"../tests/models/mobilenetv2.relay","num_eclass":15431,"num_enodes":29147,"solver_time":4132} +{"algo":"ILP-ACyc","avg_enode_per_class":1.8888600868381829,"best_cost":1685.0,"extract_time":1132,"model":"../tests/models/mobilenetv2.relay","num_eclass":15431,"num_enodes":29147,"solver_time":313} +{"algo":"ILP-Topo","avg_enode_per_class":1.8888600868381829,"best_cost":1685.0,"extract_time":5181,"model":"../tests/models/mobilenetv2.relay","num_eclass":15431,"num_enodes":29147,"solver_time":4477} +{"algo":"Greedy","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":1,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":1} +{"algo":"WPMAXSAT","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":2500,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":2022} +{"algo":"ILP-ACyc","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":1192,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":688} +{"algo":"ILP-Topo","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":4805,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":4369} +{"algo":"Greedy","avg_enode_per_class":1.9464018791373052,"best_cost":721.0,"extract_time":1,"model":"../tests/models/resnet18.relay","num_eclass":9366,"num_enodes":18230,"solver_time":1} +{"algo":"WPMAXSAT","avg_enode_per_class":1.9464018791373052,"best_cost":602.0,"extract_time":1947,"model":"../tests/models/resnet18.relay","num_eclass":9366,"num_enodes":18230,"solver_time":1524} +{"algo":"ILP-ACyc","avg_enode_per_class":1.9464018791373052,"best_cost":602.0,"extract_time":1573,"model":"../tests/models/resnet18.relay","num_eclass":9366,"num_enodes":18230,"solver_time":1158} +{"algo":"ILP-Topo","avg_enode_per_class":1.9464018791373052,"best_cost":602.0,"extract_time":4564,"model":"../tests/models/resnet18.relay","num_eclass":9366,"num_enodes":18230,"solver_time":4175} +{"algo":"Greedy","avg_enode_per_class":1.8526782843547038,"best_cost":1692.0,"extract_time":3,"model":"../tests/models/efficientnet.relay","num_eclass":15551,"num_enodes":28811,"solver_time":3} +{"algo":"WPMAXSAT","avg_enode_per_class":1.8526782843547038,"best_cost":1583.0,"extract_time":5106,"model":"../tests/models/efficientnet.relay","num_eclass":15551,"num_enodes":28811,"solver_time":4109} +{"algo":"ILP-ACyc","avg_enode_per_class":1.8526782843547038,"best_cost":1583.0,"extract_time":1105,"model":"../tests/models/efficientnet.relay","num_eclass":15551,"num_enodes":28811,"solver_time":278} +{"algo":"ILP-Topo","avg_enode_per_class":1.8526782843547038,"best_cost":1583.0,"extract_time":5497,"model":"../tests/models/efficientnet.relay","num_eclass":15551,"num_enodes":28811,"solver_time":4783} +{"algo":"Greedy","avg_enode_per_class":1.894946170198176,"best_cost":1801.0,"extract_time":4,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14583,"num_enodes":27634,"solver_time":4} +{"algo":"WPMAXSAT","avg_enode_per_class":1.894946170198176,"best_cost":1535.0,"extract_time":4457,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14583,"num_enodes":27634,"solver_time":3654} +{"algo":"ILP-ACyc","avg_enode_per_class":1.894946170198176,"best_cost":1535.0,"extract_time":1112,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14583,"num_enodes":27634,"solver_time":303} +{"algo":"ILP-Topo","avg_enode_per_class":1.894946170198176,"best_cost":1535.0,"extract_time":5173,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14583,"num_enodes":27634,"solver_time":4481} +{"algo":"Greedy","avg_enode_per_class":1.8799665680853799,"best_cost":2056.0,"extract_time":4,"model":"../tests/models/mobilenetv2.relay","num_eclass":15554,"num_enodes":29241,"solver_time":4} +{"algo":"WPMAXSAT","avg_enode_per_class":1.8799665680853799,"best_cost":1685.0,"extract_time":2404,"model":"../tests/models/mobilenetv2.relay","num_eclass":15554,"num_enodes":29241,"solver_time":1523} +{"algo":"ILP-ACyc","avg_enode_per_class":1.8799665680853799,"best_cost":1685.0,"extract_time":1158,"model":"../tests/models/mobilenetv2.relay","num_eclass":15554,"num_enodes":29241,"solver_time":340} +{"algo":"ILP-Topo","avg_enode_per_class":1.8799665680853799,"best_cost":1685.0,"extract_time":5593,"model":"../tests/models/mobilenetv2.relay","num_eclass":15554,"num_enodes":29241,"solver_time":4816} +{"algo":"Greedy","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":1,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":1} +{"algo":"WPMAXSAT","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":1313,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":783} +{"algo":"ILP-ACyc","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":1169,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":698} +{"algo":"ILP-Topo","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":4982,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":4574} +{"algo":"Greedy","avg_enode_per_class":1.9464018791373052,"best_cost":721.0,"extract_time":1,"model":"../tests/models/resnet18.relay","num_eclass":9366,"num_enodes":18230,"solver_time":1} +{"algo":"WPMAXSAT","avg_enode_per_class":1.9464018791373052,"best_cost":602.0,"extract_time":1108,"model":"../tests/models/resnet18.relay","num_eclass":9366,"num_enodes":18230,"solver_time":646} +{"algo":"ILP-ACyc","avg_enode_per_class":1.9464018791373052,"best_cost":602.0,"extract_time":1373,"model":"../tests/models/resnet18.relay","num_eclass":9366,"num_enodes":18230,"solver_time":914} +{"algo":"ILP-Topo","avg_enode_per_class":1.9464018791373052,"best_cost":602.0,"extract_time":4799,"model":"../tests/models/resnet18.relay","num_eclass":9366,"num_enodes":18230,"solver_time":4423} +{"algo":"Greedy","avg_enode_per_class":1.8516768095299754,"best_cost":1692.0,"extract_time":3,"model":"../tests/models/efficientnet.relay","num_eclass":15446,"num_enodes":28601,"solver_time":3} +{"algo":"WPMAXSAT","avg_enode_per_class":1.8516768095299754,"best_cost":1583.0,"extract_time":2301,"model":"../tests/models/efficientnet.relay","num_eclass":15446,"num_enodes":28601,"solver_time":1430} +{"algo":"ILP-ACyc","avg_enode_per_class":1.8516768095299754,"best_cost":1583.0,"extract_time":1132,"model":"../tests/models/efficientnet.relay","num_eclass":15446,"num_enodes":28601,"solver_time":263} +{"algo":"ILP-Topo","avg_enode_per_class":1.8516768095299754,"best_cost":1583.0,"extract_time":5740,"model":"../tests/models/efficientnet.relay","num_eclass":15446,"num_enodes":28601,"solver_time":4955} +{"algo":"Greedy","avg_enode_per_class":1.908307900983384,"best_cost":1801.0,"extract_time":4,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14745,"num_enodes":28138,"solver_time":4} +{"algo":"WPMAXSAT","avg_enode_per_class":1.908307900983384,"best_cost":1535.0,"extract_time":2286,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14745,"num_enodes":28138,"solver_time":1426} +{"algo":"ILP-ACyc","avg_enode_per_class":1.908307900983384,"best_cost":1535.0,"extract_time":1143,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14745,"num_enodes":28138,"solver_time":371} +{"algo":"ILP-Topo","avg_enode_per_class":1.908307900983384,"best_cost":1535.0,"extract_time":5515,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14745,"num_enodes":28138,"solver_time":4885} +{"algo":"Greedy","avg_enode_per_class":1.8917769700294904,"best_cost":1535.0,"extract_time":3,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14581,"num_enodes":27584,"solver_time":3} +{"algo":"WPMAXSAT","avg_enode_per_class":1.8917769700294904,"best_cost":1535.0,"extract_time":2195,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14581,"num_enodes":27584,"solver_time":1400} +{"algo":"ILP-ACyc","avg_enode_per_class":1.8917769700294904,"best_cost":1535.0,"extract_time":1047,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14581,"num_enodes":27584,"solver_time":327} +{"algo":"ILP-Topo","avg_enode_per_class":1.8917769700294904,"best_cost":1535.0,"extract_time":5544,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14581,"num_enodes":27584,"solver_time":4981} +{"algo":"Greedy","avg_enode_per_class":1.8743826358201197,"best_cost":1685.0,"extract_time":3,"model":"../tests/models/mobilenetv2.relay","num_eclass":15388,"num_enodes":28843,"solver_time":3} +{"algo":"WPMAXSAT","avg_enode_per_class":1.8743826358201197,"best_cost":1685.0,"extract_time":2380,"model":"../tests/models/mobilenetv2.relay","num_eclass":15388,"num_enodes":28843,"solver_time":1486} +{"algo":"ILP-ACyc","avg_enode_per_class":1.8743826358201197,"best_cost":1685.0,"extract_time":1115,"model":"../tests/models/mobilenetv2.relay","num_eclass":15388,"num_enodes":28843,"solver_time":318} +{"algo":"ILP-Topo","avg_enode_per_class":1.8743826358201197,"best_cost":1685.0,"extract_time":4558,"model":"../tests/models/mobilenetv2.relay","num_eclass":15388,"num_enodes":28843,"solver_time":3899} +{"algo":"Greedy","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":1,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":1} +{"algo":"WPMAXSAT","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":1271,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":790} +{"algo":"ILP-ACyc","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":1191,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":722} +{"algo":"ILP-Topo","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":4724,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":4305} +{"algo":"Greedy","avg_enode_per_class":1.9434002563007262,"best_cost":602.0,"extract_time":1,"model":"../tests/models/resnet18.relay","num_eclass":9364,"num_enodes":18198,"solver_time":1} +{"algo":"WPMAXSAT","avg_enode_per_class":1.9434002563007262,"best_cost":602.0,"extract_time":1217,"model":"../tests/models/resnet18.relay","num_eclass":9364,"num_enodes":18198,"solver_time":758} +{"algo":"ILP-ACyc","avg_enode_per_class":1.9434002563007262,"best_cost":602.0,"extract_time":1355,"model":"../tests/models/resnet18.relay","num_eclass":9364,"num_enodes":18198,"solver_time":868} +{"algo":"ILP-Topo","avg_enode_per_class":1.9434002563007262,"best_cost":602.0,"extract_time":5048,"model":"../tests/models/resnet18.relay","num_eclass":9364,"num_enodes":18198,"solver_time":4650} +{"algo":"Greedy","avg_enode_per_class":1.86069045174538,"best_cost":1583.0,"extract_time":3,"model":"../tests/models/efficientnet.relay","num_eclass":15584,"num_enodes":28997,"solver_time":3} +{"algo":"WPMAXSAT","avg_enode_per_class":1.86069045174538,"best_cost":1583.0,"extract_time":2438,"model":"../tests/models/efficientnet.relay","num_eclass":15584,"num_enodes":28997,"solver_time":1480} +{"algo":"ILP-ACyc","avg_enode_per_class":1.86069045174538,"best_cost":1583.0,"extract_time":1183,"model":"../tests/models/efficientnet.relay","num_eclass":15584,"num_enodes":28997,"solver_time":373} +{"algo":"ILP-Topo","avg_enode_per_class":1.86069045174538,"best_cost":1583.0,"extract_time":5586,"model":"../tests/models/efficientnet.relay","num_eclass":15584,"num_enodes":28997,"solver_time":4936} +{"algo":"Greedy","avg_enode_per_class":1.904475572258285,"best_cost":1535.0,"extract_time":3,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14635,"num_enodes":27872,"solver_time":3} +{"algo":"WPMAXSAT","avg_enode_per_class":1.904475572258285,"best_cost":1535.0,"extract_time":2227,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14635,"num_enodes":27872,"solver_time":1450} +{"algo":"ILP-ACyc","avg_enode_per_class":1.904475572258285,"best_cost":1535.0,"extract_time":1094,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14635,"num_enodes":27872,"solver_time":331} +{"algo":"ILP-Topo","avg_enode_per_class":1.904475572258285,"best_cost":1535.0,"extract_time":5920,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14635,"num_enodes":27872,"solver_time":5287} +{"algo":"Greedy","avg_enode_per_class":1.8854809670781894,"best_cost":1685.0,"extract_time":3,"model":"../tests/models/mobilenetv2.relay","num_eclass":15552,"num_enodes":29323,"solver_time":3} +{"algo":"WPMAXSAT","avg_enode_per_class":1.8854809670781894,"best_cost":1685.0,"extract_time":2624,"model":"../tests/models/mobilenetv2.relay","num_eclass":15552,"num_enodes":29323,"solver_time":1639} +{"algo":"ILP-ACyc","avg_enode_per_class":1.8854809670781894,"best_cost":1685.0,"extract_time":1144,"model":"../tests/models/mobilenetv2.relay","num_eclass":15552,"num_enodes":29323,"solver_time":367} +{"algo":"ILP-Topo","avg_enode_per_class":1.8854809670781894,"best_cost":1685.0,"extract_time":5169,"model":"../tests/models/mobilenetv2.relay","num_eclass":15552,"num_enodes":29323,"solver_time":4515} +{"algo":"Greedy","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":1,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":1} +{"algo":"WPMAXSAT","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":1300,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":816} +{"algo":"ILP-ACyc","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":1192,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":711} +{"algo":"ILP-Topo","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":5217,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":4839} +{"algo":"Greedy","avg_enode_per_class":1.933058925476603,"best_cost":602.0,"extract_time":1,"model":"../tests/models/resnet18.relay","num_eclass":9232,"num_enodes":17846,"solver_time":1} +{"algo":"WPMAXSAT","avg_enode_per_class":1.933058925476603,"best_cost":602.0,"extract_time":1178,"model":"../tests/models/resnet18.relay","num_eclass":9232,"num_enodes":17846,"solver_time":721} +{"algo":"ILP-ACyc","avg_enode_per_class":1.933058925476603,"best_cost":602.0,"extract_time":1062,"model":"../tests/models/resnet18.relay","num_eclass":9232,"num_enodes":17846,"solver_time":677} +{"algo":"ILP-Topo","avg_enode_per_class":1.933058925476603,"best_cost":602.0,"extract_time":3658,"model":"../tests/models/resnet18.relay","num_eclass":9232,"num_enodes":17846,"solver_time":3304} +{"algo":"Greedy","avg_enode_per_class":1.8519635523613962,"best_cost":1583.0,"extract_time":3,"model":"../tests/models/efficientnet.relay","num_eclass":15584,"num_enodes":28861,"solver_time":3} +{"algo":"WPMAXSAT","avg_enode_per_class":1.8519635523613962,"best_cost":1583.0,"extract_time":2442,"model":"../tests/models/efficientnet.relay","num_eclass":15584,"num_enodes":28861,"solver_time":1446} +{"algo":"ILP-ACyc","avg_enode_per_class":1.8519635523613962,"best_cost":1583.0,"extract_time":1107,"model":"../tests/models/efficientnet.relay","num_eclass":15584,"num_enodes":28861,"solver_time":282} +{"algo":"ILP-Topo","avg_enode_per_class":1.8519635523613962,"best_cost":1583.0,"extract_time":6235,"model":"../tests/models/efficientnet.relay","num_eclass":15584,"num_enodes":28861,"solver_time":5533} +{"algo":"Greedy","avg_enode_per_class":1.8921762897164331,"best_cost":1535.0,"extract_time":3,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14635,"num_enodes":27692,"solver_time":3} +{"algo":"WPMAXSAT","avg_enode_per_class":1.8921762897164331,"best_cost":1535.0,"extract_time":2388,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14635,"num_enodes":27692,"solver_time":1580} +{"algo":"ILP-ACyc","avg_enode_per_class":1.8921762897164331,"best_cost":1535.0,"extract_time":1045,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14635,"num_enodes":27692,"solver_time":337} +{"algo":"ILP-Topo","avg_enode_per_class":1.8921762897164331,"best_cost":1535.0,"extract_time":4982,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14635,"num_enodes":27692,"solver_time":4361} +{"algo":"Greedy","avg_enode_per_class":1.8851782605892593,"best_cost":1685.0,"extract_time":3,"model":"../tests/models/mobilenetv2.relay","num_eclass":15511,"num_enodes":29241,"solver_time":3} +{"algo":"WPMAXSAT","avg_enode_per_class":1.8851782605892593,"best_cost":1685.0,"extract_time":2423,"model":"../tests/models/mobilenetv2.relay","num_eclass":15511,"num_enodes":29241,"solver_time":1533} +{"algo":"ILP-ACyc","avg_enode_per_class":1.8851782605892593,"best_cost":1685.0,"extract_time":1141,"model":"../tests/models/mobilenetv2.relay","num_eclass":15511,"num_enodes":29241,"solver_time":315} +{"algo":"ILP-Topo","avg_enode_per_class":1.8851782605892593,"best_cost":1685.0,"extract_time":5396,"model":"../tests/models/mobilenetv2.relay","num_eclass":15511,"num_enodes":29241,"solver_time":4748} +{"algo":"Greedy","avg_enode_per_class":1.9741559953434227,"best_cost":681.0,"extract_time":1,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":16958,"solver_time":1} +{"algo":"WPMAXSAT","avg_enode_per_class":1.9741559953434227,"best_cost":681.0,"extract_time":1244,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":16958,"solver_time":770} +{"algo":"ILP-ACyc","avg_enode_per_class":1.9741559953434227,"best_cost":681.0,"extract_time":979,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":16958,"solver_time":527} +{"algo":"ILP-Topo","avg_enode_per_class":1.9741559953434227,"best_cost":681.0,"extract_time":5139,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":16958,"solver_time":4795} +{"algo":"Greedy","avg_enode_per_class":1.9434002563007262,"best_cost":602.0,"extract_time":1,"model":"../tests/models/resnet18.relay","num_eclass":9364,"num_enodes":18198,"solver_time":1} +{"algo":"WPMAXSAT","avg_enode_per_class":1.9434002563007262,"best_cost":602.0,"extract_time":1187,"model":"../tests/models/resnet18.relay","num_eclass":9364,"num_enodes":18198,"solver_time":744} +{"algo":"ILP-ACyc","avg_enode_per_class":1.9434002563007262,"best_cost":602.0,"extract_time":1572,"model":"../tests/models/resnet18.relay","num_eclass":9364,"num_enodes":18198,"solver_time":1135} +{"algo":"ILP-Topo","avg_enode_per_class":1.9434002563007262,"best_cost":602.0,"extract_time":4649,"model":"../tests/models/resnet18.relay","num_eclass":9364,"num_enodes":18198,"solver_time":4283} +{"algo":"Greedy","avg_enode_per_class":1.8506216006216005,"best_cost":1583.0,"extract_time":3,"model":"../tests/models/efficientnet.relay","num_eclass":15444,"num_enodes":28581,"solver_time":3} +{"algo":"WPMAXSAT","avg_enode_per_class":1.8506216006216005,"best_cost":1583.0,"extract_time":2361,"model":"../tests/models/efficientnet.relay","num_eclass":15444,"num_enodes":28581,"solver_time":1454} +{"algo":"ILP-ACyc","avg_enode_per_class":1.8506216006216005,"best_cost":1583.0,"extract_time":1095,"model":"../tests/models/efficientnet.relay","num_eclass":15444,"num_enodes":28581,"solver_time":265} +{"algo":"ILP-Topo","avg_enode_per_class":1.8506216006216005,"best_cost":1583.0,"extract_time":6115,"model":"../tests/models/efficientnet.relay","num_eclass":15444,"num_enodes":28581,"solver_time":5366} +{"algo":"Greedy","avg_enode_per_class":1.8933567615057105,"best_cost":1535.0,"extract_time":3,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14797,"num_enodes":28016,"solver_time":3} +{"algo":"WPMAXSAT","avg_enode_per_class":1.8933567615057105,"best_cost":1535.0,"extract_time":2244,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14797,"num_enodes":28016,"solver_time":1440} +{"algo":"ILP-ACyc","avg_enode_per_class":1.8933567615057105,"best_cost":1535.0,"extract_time":1085,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14797,"num_enodes":28016,"solver_time":371} +{"algo":"ILP-Topo","avg_enode_per_class":1.8933567615057105,"best_cost":1535.0,"extract_time":5218,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14797,"num_enodes":28016,"solver_time":4634} +{"algo":"Greedy","avg_enode_per_class":1.8851782605892593,"best_cost":1685.0,"extract_time":3,"model":"../tests/models/mobilenetv2.relay","num_eclass":15511,"num_enodes":29241,"solver_time":3} +{"algo":"WPMAXSAT","avg_enode_per_class":1.8851782605892593,"best_cost":1685.0,"extract_time":2468,"model":"../tests/models/mobilenetv2.relay","num_eclass":15511,"num_enodes":29241,"solver_time":1554} +{"algo":"ILP-ACyc","avg_enode_per_class":1.8851782605892593,"best_cost":1685.0,"extract_time":1145,"model":"../tests/models/mobilenetv2.relay","num_eclass":15511,"num_enodes":29241,"solver_time":337} +{"algo":"ILP-Topo","avg_enode_per_class":1.8851782605892593,"best_cost":1685.0,"extract_time":5389,"model":"../tests/models/mobilenetv2.relay","num_eclass":15511,"num_enodes":29241,"solver_time":4675} +{"algo":"Greedy","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":1,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":1} +{"algo":"WPMAXSAT","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":1299,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":818} +{"algo":"ILP-ACyc","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":1135,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":675} +{"algo":"ILP-Topo","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":4751,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":4328} +{"algo":"Greedy","avg_enode_per_class":1.942727469202507,"best_cost":602.0,"extract_time":1,"model":"../tests/models/resnet18.relay","num_eclass":9254,"num_enodes":17978,"solver_time":1} +{"algo":"WPMAXSAT","avg_enode_per_class":1.942727469202507,"best_cost":602.0,"extract_time":1235,"model":"../tests/models/resnet18.relay","num_eclass":9254,"num_enodes":17978,"solver_time":725} +{"algo":"ILP-ACyc","avg_enode_per_class":1.942727469202507,"best_cost":602.0,"extract_time":1444,"model":"../tests/models/resnet18.relay","num_eclass":9254,"num_enodes":17978,"solver_time":922} +{"algo":"ILP-Topo","avg_enode_per_class":1.942727469202507,"best_cost":602.0,"extract_time":4222,"model":"../tests/models/resnet18.relay","num_eclass":9254,"num_enodes":17978,"solver_time":3825} +{"algo":"Greedy","avg_enode_per_class":1.8506216006216005,"best_cost":1583.0,"extract_time":3,"model":"../tests/models/efficientnet.relay","num_eclass":15444,"num_enodes":28581,"solver_time":3} +{"algo":"WPMAXSAT","avg_enode_per_class":1.8506216006216005,"best_cost":1583.0,"extract_time":2309,"model":"../tests/models/efficientnet.relay","num_eclass":15444,"num_enodes":28581,"solver_time":1406} +{"algo":"ILP-ACyc","avg_enode_per_class":1.8506216006216005,"best_cost":1583.0,"extract_time":1050,"model":"../tests/models/efficientnet.relay","num_eclass":15444,"num_enodes":28581,"solver_time":264} +{"algo":"ILP-Topo","avg_enode_per_class":1.8506216006216005,"best_cost":1583.0,"extract_time":6389,"model":"../tests/models/efficientnet.relay","num_eclass":15444,"num_enodes":28581,"solver_time":5783} +{"algo":"Greedy","avg_enode_per_class":1.8917769700294904,"best_cost":1535.0,"extract_time":5,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14581,"num_enodes":27584,"solver_time":5} +{"algo":"WPMAXSAT","avg_enode_per_class":1.8917769700294904,"best_cost":1535.0,"extract_time":4286,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14581,"num_enodes":27584,"solver_time":2111} +{"algo":"ILP-ACyc","avg_enode_per_class":1.8917769700294904,"best_cost":1535.0,"extract_time":3082,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14581,"num_enodes":27584,"solver_time":1127} +{"algo":"ILP-Topo","avg_enode_per_class":1.8917769700294904,"best_cost":1535.0,"extract_time":9451,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14581,"num_enodes":27584,"solver_time":8212} +{"algo":"Greedy","avg_enode_per_class":1.8743826358201197,"best_cost":1685.0,"extract_time":3,"model":"../tests/models/mobilenetv2.relay","num_eclass":15388,"num_enodes":28843,"solver_time":3} +{"algo":"WPMAXSAT","avg_enode_per_class":1.8743826358201197,"best_cost":1685.0,"extract_time":2406,"model":"../tests/models/mobilenetv2.relay","num_eclass":15388,"num_enodes":28843,"solver_time":1505} +{"algo":"ILP-ACyc","avg_enode_per_class":1.8743826358201197,"best_cost":1685.0,"extract_time":1064,"model":"../tests/models/mobilenetv2.relay","num_eclass":15388,"num_enodes":28843,"solver_time":303} +{"algo":"ILP-Topo","avg_enode_per_class":1.8743826358201197,"best_cost":1685.0,"extract_time":5053,"model":"../tests/models/mobilenetv2.relay","num_eclass":15388,"num_enodes":28843,"solver_time":4310} +{"algo":"Greedy","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":1,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":1} +{"algo":"WPMAXSAT","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":1292,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":811} +{"algo":"ILP-ACyc","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":1229,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":769} +{"algo":"ILP-Topo","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":5125,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":4743} +{"algo":"Greedy","avg_enode_per_class":1.9434002563007262,"best_cost":602.0,"extract_time":1,"model":"../tests/models/resnet18.relay","num_eclass":9364,"num_enodes":18198,"solver_time":1} +{"algo":"WPMAXSAT","avg_enode_per_class":1.9434002563007262,"best_cost":602.0,"extract_time":1213,"model":"../tests/models/resnet18.relay","num_eclass":9364,"num_enodes":18198,"solver_time":759} +{"algo":"ILP-ACyc","avg_enode_per_class":1.9434002563007262,"best_cost":602.0,"extract_time":1504,"model":"../tests/models/resnet18.relay","num_eclass":9364,"num_enodes":18198,"solver_time":1059} +{"algo":"ILP-Topo","avg_enode_per_class":1.9434002563007262,"best_cost":602.0,"extract_time":4526,"model":"../tests/models/resnet18.relay","num_eclass":9364,"num_enodes":18198,"solver_time":4152} +{"algo":"Greedy","avg_enode_per_class":1.8509593643000193,"best_cost":1583.0,"extract_time":3,"model":"../tests/models/efficientnet.relay","num_eclass":15479,"num_enodes":28651,"solver_time":3} +{"algo":"WPMAXSAT","avg_enode_per_class":1.8509593643000193,"best_cost":1583.0,"extract_time":2347,"model":"../tests/models/efficientnet.relay","num_eclass":15479,"num_enodes":28651,"solver_time":1471} +{"algo":"ILP-ACyc","avg_enode_per_class":1.8509593643000193,"best_cost":1583.0,"extract_time":1042,"model":"../tests/models/efficientnet.relay","num_eclass":15479,"num_enodes":28651,"solver_time":270} +{"algo":"ILP-Topo","avg_enode_per_class":1.8509593643000193,"best_cost":1583.0,"extract_time":5700,"model":"../tests/models/efficientnet.relay","num_eclass":15479,"num_enodes":28651,"solver_time":5085} +{"algo":"Greedy","avg_enode_per_class":1.9041218023455182,"best_cost":1535.0,"extract_time":3,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14581,"num_enodes":27764,"solver_time":3} +{"algo":"WPMAXSAT","avg_enode_per_class":1.9041218023455182,"best_cost":1535.0,"extract_time":2236,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14581,"num_enodes":27764,"solver_time":1433} +{"algo":"ILP-ACyc","avg_enode_per_class":1.9041218023455182,"best_cost":1535.0,"extract_time":1067,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14581,"num_enodes":27764,"solver_time":322} +{"algo":"ILP-Topo","avg_enode_per_class":1.9041218023455182,"best_cost":1535.0,"extract_time":4768,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14581,"num_enodes":27764,"solver_time":4161} diff --git a/flexmatch/extraction_stats_im2col_with_simpl.txt b/flexmatch/extraction_stats_im2col_with_simpl.txt new file mode 100644 index 0000000..9e1c5bb --- /dev/null +++ b/flexmatch/extraction_stats_im2col_with_simpl.txt @@ -0,0 +1,79 @@ +{"algo":"Greedy","avg_enode_per_class":1.8747164430617669,"best_cost":1685.0,"extract_time":3,"model":"../tests/models/mobilenetv2.relay","num_eclass":15429,"num_enodes":28925,"solver_time":3} +{"algo":"WPMAXSAT","avg_enode_per_class":1.8747164430617669,"best_cost":1685.0,"extract_time":2368,"model":"../tests/models/mobilenetv2.relay","num_eclass":15429,"num_enodes":28925,"solver_time":1506} +{"algo":"ILP-ACyc","avg_enode_per_class":1.8747164430617669,"best_cost":1685.0,"extract_time":1083,"model":"../tests/models/mobilenetv2.relay","num_eclass":15429,"num_enodes":28925,"solver_time":325} +{"algo":"ILP-Topo","avg_enode_per_class":1.8747164430617669,"best_cost":1685.0,"extract_time":5009,"model":"../tests/models/mobilenetv2.relay","num_eclass":15429,"num_enodes":28925,"solver_time":4361} +{"algo":"Greedy","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":1,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":1} +{"algo":"WPMAXSAT","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":1273,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":794} +{"algo":"ILP-ACyc","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":1128,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":702} +{"algo":"ILP-Topo","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":5161,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":4800} +{"algo":"Greedy","avg_enode_per_class":1.9434002563007262,"best_cost":602.0,"extract_time":1,"model":"../tests/models/resnet18.relay","num_eclass":9364,"num_enodes":18198,"solver_time":1} +{"algo":"WPMAXSAT","avg_enode_per_class":1.9434002563007262,"best_cost":602.0,"extract_time":1184,"model":"../tests/models/resnet18.relay","num_eclass":9364,"num_enodes":18198,"solver_time":724} +{"algo":"ILP-ACyc","avg_enode_per_class":1.9434002563007262,"best_cost":602.0,"extract_time":1375,"model":"../tests/models/resnet18.relay","num_eclass":9364,"num_enodes":18198,"solver_time":924} +{"algo":"ILP-Topo","avg_enode_per_class":1.9434002563007262,"best_cost":602.0,"extract_time":4586,"model":"../tests/models/resnet18.relay","num_eclass":9364,"num_enodes":18198,"solver_time":4229} +{"algo":"WPMAXSAT","avg_enode_per_class":2.1604213573496303,"best_cost":1658.0,"extract_time":2089,"model":"../tests/models/mobilenetv2.relay","num_eclass":12436,"num_enodes":26867,"solver_time":1287} +{"algo":"WPMAXSAT","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":585,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":322} +{"algo":"ILP-Topo","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":1258,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":1087} +{"algo":"WPMAXSAT","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":473,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":262} +{"algo":"ILP-Topo","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":1689,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":1534} +{"algo":"WPMAXSAT","avg_enode_per_class":2.1604213573496303,"best_cost":1658.0,"extract_time":2119,"model":"../tests/models/mobilenetv2.relay","num_eclass":12436,"num_enodes":26867,"solver_time":1321} +{"algo":"ILP-ACyc","avg_enode_per_class":2.1063965544743977,"best_cost":1583.0,"extract_time":871,"model":"../tests/models/efficientnet.relay","num_eclass":12538,"num_enodes":26410,"solver_time":231} +{"algo":"ILP-ACyc","avg_enode_per_class":2.109090909090909,"best_cost":1583.0,"extract_time":885,"model":"../tests/models/efficientnet.relay","num_eclass":12540,"num_enodes":26448,"solver_time":232} +{"algo":"WPMAXSAT","avg_enode_per_class":2.1604213573496303,"best_cost":1658.0,"extract_time":2037,"model":"../tests/models/mobilenetv2.relay","num_eclass":12436,"num_enodes":26867,"solver_time":1274} +{"algo":"ILP-ACyc","avg_enode_per_class":2.1604213573496303,"best_cost":1658.0,"extract_time":996,"model":"../tests/models/mobilenetv2.relay","num_eclass":12436,"num_enodes":26867,"solver_time":269} +{"algo":"WPMAXSAT","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":588,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":331} +{"algo":"ILP-ACyc","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":295,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":87} +{"algo":"WPMAXSAT","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":491,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":268} +{"algo":"ILP-ACyc","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":1127,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":969} +{"algo":"ILP-Topo","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":1768,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":1601} +{"algo":"WPMAXSAT","avg_enode_per_class":2.1063965544743977,"best_cost":1583.0,"extract_time":2099,"model":"../tests/models/efficientnet.relay","num_eclass":12538,"num_enodes":26410,"solver_time":1281} +{"algo":"ILP-ACyc","avg_enode_per_class":2.1063965544743977,"best_cost":1583.0,"extract_time":913,"model":"../tests/models/efficientnet.relay","num_eclass":12538,"num_enodes":26410,"solver_time":230} +{"algo":"WPMAXSAT","avg_enode_per_class":2.19946474868278,"best_cost":1529.0,"extract_time":2238,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":11957,"num_enodes":26299,"solver_time":1376} +{"algo":"ILP-ACyc","avg_enode_per_class":2.19946474868278,"best_cost":1529.0,"extract_time":867,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":11957,"num_enodes":26299,"solver_time":237} +{"algo":"WPMAXSAT","avg_enode_per_class":2.1604213573496303,"best_cost":1658.0,"extract_time":2162,"model":"../tests/models/mobilenetv2.relay","num_eclass":12436,"num_enodes":26867,"solver_time":1304} +{"algo":"ILP-ACyc","avg_enode_per_class":2.1604213573496303,"best_cost":1658.0,"extract_time":873,"model":"../tests/models/mobilenetv2.relay","num_eclass":12436,"num_enodes":26867,"solver_time":265} +{"algo":"WPMAXSAT","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":586,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":337} +{"algo":"ILP-ACyc","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":275,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":86} +{"algo":"ILP-Topo","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":1267,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":1114} +{"algo":"WPMAXSAT","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":513,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":272} +{"algo":"ILP-ACyc","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":1205,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":1045} +{"algo":"ILP-Topo","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":1588,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":1426} +{"algo":"WPMAXSAT","avg_enode_per_class":2.1063965544743977,"best_cost":1583.0,"extract_time":2155,"model":"../tests/models/efficientnet.relay","num_eclass":12538,"num_enodes":26410,"solver_time":1300} +{"algo":"ILP-ACyc","avg_enode_per_class":2.1063965544743977,"best_cost":1583.0,"extract_time":870,"model":"../tests/models/efficientnet.relay","num_eclass":12538,"num_enodes":26410,"solver_time":230} +{"algo":"WPMAXSAT","avg_enode_per_class":2.19946474868278,"best_cost":1529.0,"extract_time":2042,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":11957,"num_enodes":26299,"solver_time":1293} +{"algo":"ILP-ACyc","avg_enode_per_class":2.19946474868278,"best_cost":1529.0,"extract_time":851,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":11957,"num_enodes":26299,"solver_time":243} +{"algo":"WPMAXSAT","avg_enode_per_class":2.1604213573496303,"best_cost":1658.0,"extract_time":2124,"model":"../tests/models/mobilenetv2.relay","num_eclass":12436,"num_enodes":26867,"solver_time":1367} +{"algo":"ILP-ACyc","avg_enode_per_class":2.1604213573496303,"best_cost":1658.0,"extract_time":898,"model":"../tests/models/mobilenetv2.relay","num_eclass":12436,"num_enodes":26867,"solver_time":264} +{"algo":"WPMAXSAT","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":481,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":251} +{"algo":"ILP-ACyc","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":289,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":86} +{"algo":"ILP-Topo","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":1638,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":1486} +{"algo":"WPMAXSAT","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":493,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":276} +{"algo":"ILP-ACyc","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":1379,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":1216} +{"algo":"ILP-Topo","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":1538,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":1398} +{"algo":"WPMAXSAT","avg_enode_per_class":2.1063965544743977,"best_cost":1583.0,"extract_time":2083,"model":"../tests/models/efficientnet.relay","num_eclass":12538,"num_enodes":26410,"solver_time":1305} +{"algo":"ILP-ACyc","avg_enode_per_class":2.1063965544743977,"best_cost":1583.0,"extract_time":910,"model":"../tests/models/efficientnet.relay","num_eclass":12538,"num_enodes":26410,"solver_time":234} +{"algo":"WPMAXSAT","avg_enode_per_class":2.19946474868278,"best_cost":1529.0,"extract_time":2217,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":11957,"num_enodes":26299,"solver_time":1417} +{"algo":"ILP-ACyc","avg_enode_per_class":2.19946474868278,"best_cost":1529.0,"extract_time":941,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":11957,"num_enodes":26299,"solver_time":237} +{"algo":"WPMAXSAT","avg_enode_per_class":2.1604213573496303,"best_cost":1658.0,"extract_time":2081,"model":"../tests/models/mobilenetv2.relay","num_eclass":12436,"num_enodes":26867,"solver_time":1289} +{"algo":"ILP-ACyc","avg_enode_per_class":2.1604213573496303,"best_cost":1658.0,"extract_time":906,"model":"../tests/models/mobilenetv2.relay","num_eclass":12436,"num_enodes":26867,"solver_time":257} +{"algo":"WPMAXSAT","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":575,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":343} +{"algo":"ILP-ACyc","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":287,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":86} +{"algo":"ILP-Topo","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":1526,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":1390} +{"algo":"WPMAXSAT","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":501,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":269} +{"algo":"ILP-ACyc","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":1017,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":840} +{"algo":"ILP-Topo","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":1771,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":1617} +{"algo":"WPMAXSAT","avg_enode_per_class":2.1063965544743977,"best_cost":1583.0,"extract_time":2081,"model":"../tests/models/efficientnet.relay","num_eclass":12538,"num_enodes":26410,"solver_time":1273} +{"algo":"ILP-ACyc","avg_enode_per_class":2.1063965544743977,"best_cost":1583.0,"extract_time":906,"model":"../tests/models/efficientnet.relay","num_eclass":12538,"num_enodes":26410,"solver_time":231} +{"algo":"WPMAXSAT","avg_enode_per_class":2.19946474868278,"best_cost":1529.0,"extract_time":2199,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":11957,"num_enodes":26299,"solver_time":1414} +{"algo":"ILP-ACyc","avg_enode_per_class":2.19946474868278,"best_cost":1529.0,"extract_time":838,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":11957,"num_enodes":26299,"solver_time":241} +{"algo":"WPMAXSAT","avg_enode_per_class":2.1604213573496303,"best_cost":1658.0,"extract_time":2102,"model":"../tests/models/mobilenetv2.relay","num_eclass":12436,"num_enodes":26867,"solver_time":1344} +{"algo":"ILP-ACyc","avg_enode_per_class":2.1604213573496303,"best_cost":1658.0,"extract_time":918,"model":"../tests/models/mobilenetv2.relay","num_eclass":12436,"num_enodes":26867,"solver_time":265} +{"algo":"WPMAXSAT","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":579,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":342} +{"algo":"ILP-ACyc","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":305,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":109} +{"algo":"ILP-Topo","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":1259,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":1090} +{"algo":"WPMAXSAT","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":479,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":267} +{"algo":"ILP-ACyc","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":997,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":817} +{"algo":"ILP-Topo","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":1630,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":1497} +{"algo":"WPMAXSAT","avg_enode_per_class":2.1063965544743977,"best_cost":1583.0,"extract_time":2128,"model":"../tests/models/efficientnet.relay","num_eclass":12538,"num_enodes":26410,"solver_time":1279} +{"algo":"ILP-ACyc","avg_enode_per_class":2.1063965544743977,"best_cost":1583.0,"extract_time":944,"model":"../tests/models/efficientnet.relay","num_eclass":12538,"num_enodes":26410,"solver_time":233} +{"algo":"WPMAXSAT","avg_enode_per_class":2.19946474868278,"best_cost":1529.0,"extract_time":2110,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":11957,"num_enodes":26299,"solver_time":1365} +{"algo":"ILP-ACyc","avg_enode_per_class":2.19946474868278,"best_cost":1529.0,"extract_time":862,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":11957,"num_enodes":26299,"solver_time":239} From 1a81265fd1bf470f92b56f50395d45a47081852a Mon Sep 17 00:00:00 2001 From: AD1024 Date: Tue, 14 Mar 2023 02:02:57 -0400 Subject: [PATCH 17/18] save graphing changes --- flexmatch/draw_graph.py | 81 ++++++++++++++++++++++++++++------------- flexmatch/src/main.rs | 40 +------------------- 2 files changed, 56 insertions(+), 65 deletions(-) diff --git a/flexmatch/draw_graph.py b/flexmatch/draw_graph.py index 3d0b810..cb9abc3 100644 --- a/flexmatch/draw_graph.py +++ b/flexmatch/draw_graph.py @@ -1,6 +1,7 @@ import matplotlib matplotlib.use('agg') import matplotlib.pyplot as plt +plt.rcParams['text.usetex'] = True import numpy as np import json @@ -18,14 +19,13 @@ def parse_data(filename: str) -> dict: data[key] = datum return data -def draw_extraction_times(data: dict): +def draw_extraction_times(data: dict, simpl: bool): # plt.clf() - plt.title('Term Extraction Time') plt.xlabel('Model') fig, ax = plt.subplots() ax.set_ylabel('Extraction Time (ms)') ax.set_xlabel('Model', fontsize=14) - ax.set_title('Term Extraction Time') + ax.set_title(r'Term Extraction Time (\textsc{im2col} + \textsc{simpl})' if simpl else r'Term Extraction Time (\textsc{im2col} only)') # ax.set_yscale('log') x = np.arange(len(data)) # x *= 1.5 @@ -34,6 +34,7 @@ def draw_extraction_times(data: dict): overhead_times = dict() x_ticks = [] for (model, model_data) in data.items(): + i = len(x_ticks) x_ticks.append(model) counter = dict() for datum in model_data: @@ -41,31 +42,50 @@ def draw_extraction_times(data: dict): overhead_time = datum['extract_time'] - datum['solver_time'] counter[datum['algo']] = counter.get(datum['algo'], 0) if datum['algo'] not in solver_times: - solver_times[datum['algo']] = [] - overhead_times[datum['algo']] = [] + solver_times[datum['algo']] = {} + overhead_times[datum['algo']] = {} if counter[datum['algo']] == 0: - solver_times[datum['algo']].append(solver_time) - overhead_times[datum['algo']].append(overhead_time) + solver_times[datum['algo']][i] = solver_time + overhead_times[datum['algo']][i] = overhead_time else: - solver_times[datum['algo']][-1] += solver_time - overhead_times[datum['algo']][-1] += overhead_time + solver_times[datum['algo']][i] += solver_time + overhead_times[datum['algo']][i] += overhead_time counter[datum['algo']] += 1 for (algo, count) in counter.items(): - solver_times[algo][-1] /= count - overhead_times[algo][-1] /= count + solver_times[algo][i] /= count + overhead_times[algo][i] /= count bar_width = 0.25 - ax.bar(x - bar_width, solver_times['ILP-ACyc'], bar_width, label='ILP-ACyc', color='lightgreen', edgecolor='grey') - overhead = ax.bar(x - bar_width, overhead_times['ILP-ACyc'], bar_width, bottom=solver_times['ILP-ACyc'], color='slateblue', label='Overhead', hatch='//', edgecolor='grey') + ilp_acyc_xaxis = np.array(sorted(list(solver_times['ILP-ACyc'].keys()))) + ilp_acyc_solver_times = list(map(solver_times['ILP-ACyc'].get, ilp_acyc_xaxis)) + ilp_acyc_overhead_times = list(map(overhead_times['ILP-ACyc'].get, ilp_acyc_xaxis)) + ax.bar(ilp_acyc_xaxis - bar_width, ilp_acyc_solver_times, bar_width, label='ILP-ACyc', color='lightgreen', edgecolor='grey') + overhead = ax.bar(ilp_acyc_xaxis - bar_width, ilp_acyc_overhead_times, bar_width, bottom=ilp_acyc_solver_times, color='slateblue', label='Overhead', hatch='//', edgecolor='grey') - ax.bar(x, solver_times['WPMAXSAT'], bar_width, label='WPMAXSAT', color='lightpink', edgecolor='grey') - overhead = ax.bar(x, overhead_times['WPMAXSAT'], bar_width, bottom=solver_times['WPMAXSAT'], color='slateblue', hatch='//', edgecolor='grey') + maxsat_xaxis = np.array(sorted(list(solver_times['WPMAXSAT'].keys()))) + maxsat_solver_times = list(map(solver_times['WPMAXSAT'].get, maxsat_xaxis)) + maxsat_overhead_times = list(map(overhead_times['WPMAXSAT'].get, maxsat_xaxis)) + ax.bar(maxsat_xaxis, maxsat_solver_times, bar_width, label='WPMAXSAT', color='lightblue', edgecolor='grey') + overhead = ax.bar(maxsat_xaxis, maxsat_overhead_times, bar_width, bottom=maxsat_solver_times, color='slateblue', hatch='//', edgecolor='grey') - ax.bar(x + bar_width, solver_times['ILP-Topo'], bar_width, label='ILP-Topo', color='lightblue', edgecolor='grey') - overhead= ax.bar(x + bar_width, overhead_times['ILP-Topo'], bar_width, bottom=solver_times['ILP-Topo'], color='slateblue', hatch='//', edgecolor='grey') + ilp_topo_xaxis = np.array(sorted(list(solver_times['ILP-Topo'].keys()))) + ilp_topo_solver_times = list(map(solver_times['ILP-Topo'].get, ilp_topo_xaxis)) + ilp_topo_overhead_times = list(map(overhead_times['ILP-Topo'].get, ilp_topo_xaxis)) + ax.bar(ilp_topo_xaxis + bar_width, ilp_topo_solver_times, bar_width, label='ILP-Topo', color='lightpink', edgecolor='grey') + overhead= ax.bar(ilp_topo_xaxis + bar_width, ilp_topo_overhead_times, bar_width, bottom=ilp_topo_solver_times, color='slateblue', hatch='//', edgecolor='grey') - print((np.array(solver_times['ILP-Topo']) + overhead_times['ILP-Topo']) / (np.array(solver_times['ILP-ACyc']) + overhead_times['ILP-ACyc'])) - print((np.array(solver_times['ILP-Topo']) + overhead_times['ILP-Topo']) / (np.array(solver_times['WPMAXSAT']) + overhead_times['WPMAXSAT'])) + labeled = False + for i in ilp_acyc_xaxis: + if i not in ilp_topo_xaxis: + ax.bar([i], [0]) + if not labeled: + ax.axvline(i + 1.25 * bar_width, color='red', linestyle='--', label='ILP-Topo timeouts (20s)') + labeled = True + else: + ax.axvline(i + 1.25 * bar_width, color='red', linestyle='--') + + # print((np.array(solver_times['ILP-Topo']) + overhead_times['ILP-Topo']) / (np.array(solver_times['ILP-ACyc']) + overhead_times['ILP-ACyc'])) + # print((np.array(solver_times['ILP-Topo']) + overhead_times['ILP-Topo']) / (np.array(solver_times['WPMAXSAT']) + overhead_times['WPMAXSAT'])) # print(solver_times['ILP-ACyc']) # print(solver_times['WPMAXSAT']) @@ -77,10 +97,12 @@ def draw_extraction_times(data: dict): box.width, box.height * 0.9]) ax.legend(loc='upper center', bbox_to_anchor=(0.5, -0.05), - fancybox=True, shadow=True, ncol=5) - plt.savefig('extraction_time.png') + fancybox=True, shadow=True, ncol=3) + # ax.legend(loc='upper center', bbox_to_anchor=(0.5, 1.05), + # ncol=3, fancybox=True, shadow=True) + plt.savefig('extraction_time_im2col.png' if not simpl else 'extraction_time_im2col_simpl.png') -def draw_egraph_sizes(data: dict): +def draw_egraph_sizes(data: dict, simpl: bool): plt.clf() plt.title('EGraph Stats After Equality Saturation') fig, (ax1, ax2) = plt.subplots(1, 2) @@ -91,6 +113,8 @@ def draw_egraph_sizes(data: dict): xticks.append(model) num_eclasses.append(model_data[0]['num_eclass']) num_enodes.append(model_data[0]['num_enodes']) + print(num_eclasses) + print(num_enodes) tick_loc = np.arange(len(xticks)) tick_loc *= 2 ax1.bar(tick_loc, num_eclasses, width=1) @@ -100,9 +124,14 @@ def draw_egraph_sizes(data: dict): ax2.set_xticks(tick_loc, xticks, rotation=90) ax2.set_title('Number of ENodes') plt.tight_layout() - plt.savefig('egraph_stats.png') + plt.savefig('egraph_stats_im2col.png' if not simpl else 'egraph_stats_im2col_simpl.png') if __name__ == '__main__': - data = parse_data('extraction_stats.txt') - draw_extraction_times(data) - draw_egraph_sizes(data) \ No newline at end of file + import argparse + parser = argparse.ArgumentParser() + parser.add_argument('extraction_stats', type=str, help='extraction stats file') + parser.add_argument('--render-simpl', action='store_true') + args = parser.parse_args() + data = parse_data(args.extraction_stats) + draw_extraction_times(data, args.render_simpl) + draw_egraph_sizes(data, args.render_simpl) \ No newline at end of file diff --git a/flexmatch/src/main.rs b/flexmatch/src/main.rs index 58af922..38e0daf 100644 --- a/flexmatch/src/main.rs +++ b/flexmatch/src/main.rs @@ -1,4 +1,3 @@ -mod egg_lp_extract; mod ilp_extract; mod maxsat_extract; mod rewrites; @@ -225,7 +224,7 @@ fn main() { if rewrite_set.contains(rws) { continue; } - info!("Adding rewrite: {:?} with args {:?}", rws, rw_args); + println!("Adding rewrite: {:?} with args {:?}", rws, rw_args); rewrite_set.insert(rws.clone()); match rws.as_str() { "im2col" => rewrites.extend(im2col_rewrites()), @@ -425,43 +424,6 @@ fn main() { &runner.egraph, ); } - // for (algo, topo_sort) in options { - // println!("Extract using ILP-{}", algo); - // let cplex_env = rplex::Env::new().unwrap(); - // let mut cost_fn = Costfn {}; - // let start = Instant::now(); - // let mut problem = ilp_extract::create_problem( - // &cplex_env, - // root_expr, - // &runner.egraph, - // true, - // topo_sort, - // move |x, y, z| cost_fn.node_cost(x, y, z), - // ); - // let (solve_time, _, best) = problem.solve(); - // let elapsed = start.elapsed().as_millis(); - // let mut tmp_egraph = EGraph::new(MyAnalysis { - // name_to_shape: env.clone(), - // name_to_dtype: dtype_info.iter().cloned().collect(), - // }); - // let root = tmp_egraph.add_expr(&best); - // let mut maxsat_ext = - // MaxsatExtractor::new(&tmp_egraph, "compare-original.wcnf".into()); - // let mut problem = maxsat_ext.create_problem(root, "problem", true, Costfn); - // let (_, cost, _) = problem.solve_with_refinement(); - - // println!("Extraction time: {} ms", elapsed); - // println!("Solver time: {} ms", solve_time); - // println!("Cost: {}", cost.unwrap()); - // save_extraction_stats( - // format!("ILP-{}", algo).as_str(), - // source_file, - // cost.unwrap(), - // solve_time, - // elapsed, - // &runner.egraph, - // ); - // } } } } From af8b73e4a5cbbfc9ef2c2a469ae59229811fb0fd Mon Sep 17 00:00:00 2001 From: AD1024 Date: Tue, 14 Mar 2023 04:10:52 -0400 Subject: [PATCH 18/18] save graphing script --- flexmatch/draw_graph.py | 63 +++-- flexmatch/extraction_stats_im2col.txt | 248 +++++++----------- .../extraction_stats_im2col_with_simpl.txt | 149 +++++------ 3 files changed, 212 insertions(+), 248 deletions(-) diff --git a/flexmatch/draw_graph.py b/flexmatch/draw_graph.py index cb9abc3..517bc5f 100644 --- a/flexmatch/draw_graph.py +++ b/flexmatch/draw_graph.py @@ -23,9 +23,9 @@ def draw_extraction_times(data: dict, simpl: bool): # plt.clf() plt.xlabel('Model') fig, ax = plt.subplots() - ax.set_ylabel('Extraction Time (ms)') - ax.set_xlabel('Model', fontsize=14) - ax.set_title(r'Term Extraction Time (\textsc{im2col} + \textsc{simpl})' if simpl else r'Term Extraction Time (\textsc{im2col} only)') + ax.set_ylabel('Extraction Time (ms)', fontsize=14) + # ax.set_xlabel('Model', fontsize=14) + ax.set_title(r'\begin{center}(\textsc{im2col} + \textsc{simpl})\end{center}' if simpl else r'\begin{center}Term Extraction Time\\(\textsc{im2col} only)\end{center}', fontsize=14) # ax.set_yscale('log') x = np.arange(len(data)) # x *= 1.5 @@ -84,27 +84,37 @@ def draw_extraction_times(data: dict, simpl: bool): else: ax.axvline(i + 1.25 * bar_width, color='red', linestyle='--') - # print((np.array(solver_times['ILP-Topo']) + overhead_times['ILP-Topo']) / (np.array(solver_times['ILP-ACyc']) + overhead_times['ILP-ACyc'])) - # print((np.array(solver_times['ILP-Topo']) + overhead_times['ILP-Topo']) / (np.array(solver_times['WPMAXSAT']) + overhead_times['WPMAXSAT'])) + try: + for i in ilp_topo_xaxis: + print((np.array(solver_times['ILP-Topo'][i]) + overhead_times['ILP-Topo'][i]) / (np.array(solver_times['ILP-ACyc'][i]) + overhead_times['ILP-ACyc'][i])) + print((np.array(solver_times['ILP-Topo'][i]) + overhead_times['ILP-Topo'][i]) / (np.array(solver_times['WPMAXSAT'][i]) + overhead_times['WPMAXSAT'][i])) + except: + print('oopse') # print(solver_times['ILP-ACyc']) # print(solver_times['WPMAXSAT']) + ax.tick_params(axis='both', which='major', labelsize=15) + ax.tick_params(axis='both', which='minor', labelsize=15) - ax.set_xticks(x, data.keys()) - ax.set_xticklabels(x_ticks) + if simpl: + ax.set_xticks(x, data.keys()) + ax.set_xticklabels(x_ticks) + else: + ax.set_xticks([], []) - box = ax.get_position() - ax.set_position([box.x0, box.y0 + box.height * 0.1, - box.width, box.height * 0.9]) + if simpl: + box = ax.get_position() + ax.set_position([box.x0, box.y0 + box.height * 0.1, + box.width, box.height * 0.9]) - ax.legend(loc='upper center', bbox_to_anchor=(0.5, -0.05), - fancybox=True, shadow=True, ncol=3) + ax.legend(loc='upper center', bbox_to_anchor=(0.5, -0.1), + fancybox=False, shadow=True, ncol=2, fontsize=14) # ax.legend(loc='upper center', bbox_to_anchor=(0.5, 1.05), # ncol=3, fancybox=True, shadow=True) - plt.savefig('extraction_time_im2col.png' if not simpl else 'extraction_time_im2col_simpl.png') + plt.savefig('extraction_time_im2col.pdf' if not simpl else 'extraction_time_im2col_simpl.pdf', bbox_inches='tight') def draw_egraph_sizes(data: dict, simpl: bool): plt.clf() - plt.title('EGraph Stats After Equality Saturation') + plt.title(r'EGraph Stats After Equality Saturation (\textsc{im2col} only)' if not simpl else r'EGraph Stats After Equality Saturation (\textsc{im2col} + \textsc{simpl})') fig, (ax1, ax2) = plt.subplots(1, 2) num_eclasses = [] num_enodes = [] @@ -117,14 +127,25 @@ def draw_egraph_sizes(data: dict, simpl: bool): print(num_enodes) tick_loc = np.arange(len(xticks)) tick_loc *= 2 - ax1.bar(tick_loc, num_eclasses, width=1) - ax1.set_xticks(tick_loc, xticks, rotation=90) - ax1.set_title('Number of EClasses') - ax2.bar(tick_loc, num_enodes, width=1) - ax2.set_xticks(tick_loc, xticks, rotation=90) - ax2.set_title('Number of ENodes') + ax1.bar(tick_loc, num_eclasses, width=1, color='mediumslateblue') + if simpl: + ax1.set_xticks(tick_loc, xticks, rotation=90) + else: + ax1.set_xticks([], []) + ax1.set_title(r'\begin{center}Number of EClasses\\(\textsc{im2col} only)\end{center}' if not simpl else r'\begin{center}(\textsc{im2col} + \textsc{simpl})\end{center}', fontsize=16) + ax1.get_title() + ax2.bar(tick_loc, num_enodes, width=1, color='mediumslateblue') + if simpl: + ax2.set_xticks(tick_loc, xticks, rotation=90) + else: + ax2.set_xticks([], []) + ax2.set_title(r'\begin{center}Number of ENodes\\(\textsc{im2col} only)\end{center}' if not simpl else r'\begin{center}(\textsc{im2col} + \textsc{simpl})\end{center}', fontsize=16) + ax1.tick_params(axis='both', which='major', labelsize=14) + ax1.tick_params(axis='both', which='minor', labelsize=14) + ax2.tick_params(axis='both', which='major', labelsize=14) + ax2.tick_params(axis='both', which='minor', labelsize=14) plt.tight_layout() - plt.savefig('egraph_stats_im2col.png' if not simpl else 'egraph_stats_im2col_simpl.png') + plt.savefig('egraph_stats_im2col.pdf' if not simpl else 'egraph_stats_im2col_simpl.pdf') if __name__ == '__main__': import argparse diff --git a/flexmatch/extraction_stats_im2col.txt b/flexmatch/extraction_stats_im2col.txt index 24088e1..f42c5dd 100644 --- a/flexmatch/extraction_stats_im2col.txt +++ b/flexmatch/extraction_stats_im2col.txt @@ -1,148 +1,100 @@ -{"algo":"Greedy","avg_enode_per_class":1.8799665680853799,"best_cost":2056.0,"extract_time":4,"model":"../tests/models/mobilenetv2.relay","num_eclass":15554,"num_enodes":29241,"solver_time":4} -{"algo":"WPMAXSAT","avg_enode_per_class":1.8799665680853799,"best_cost":1685.0,"extract_time":5037,"model":"../tests/models/mobilenetv2.relay","num_eclass":15554,"num_enodes":29241,"solver_time":4147} -{"algo":"ILP-ACyc","avg_enode_per_class":1.8799665680853799,"best_cost":1685.0,"extract_time":1149,"model":"../tests/models/mobilenetv2.relay","num_eclass":15554,"num_enodes":29241,"solver_time":323} -{"algo":"ILP-Topo","avg_enode_per_class":1.8799665680853799,"best_cost":1685.0,"extract_time":5817,"model":"../tests/models/mobilenetv2.relay","num_eclass":15554,"num_enodes":29241,"solver_time":5023} -{"algo":"Greedy","avg_enode_per_class":1.8888600868381829,"best_cost":2056.0,"extract_time":4,"model":"../tests/models/mobilenetv2.relay","num_eclass":15431,"num_enodes":29147,"solver_time":4} -{"algo":"WPMAXSAT","avg_enode_per_class":1.8888600868381829,"best_cost":1685.0,"extract_time":4978,"model":"../tests/models/mobilenetv2.relay","num_eclass":15431,"num_enodes":29147,"solver_time":4132} -{"algo":"ILP-ACyc","avg_enode_per_class":1.8888600868381829,"best_cost":1685.0,"extract_time":1132,"model":"../tests/models/mobilenetv2.relay","num_eclass":15431,"num_enodes":29147,"solver_time":313} -{"algo":"ILP-Topo","avg_enode_per_class":1.8888600868381829,"best_cost":1685.0,"extract_time":5181,"model":"../tests/models/mobilenetv2.relay","num_eclass":15431,"num_enodes":29147,"solver_time":4477} -{"algo":"Greedy","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":1,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":1} -{"algo":"WPMAXSAT","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":2500,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":2022} -{"algo":"ILP-ACyc","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":1192,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":688} -{"algo":"ILP-Topo","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":4805,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":4369} -{"algo":"Greedy","avg_enode_per_class":1.9464018791373052,"best_cost":721.0,"extract_time":1,"model":"../tests/models/resnet18.relay","num_eclass":9366,"num_enodes":18230,"solver_time":1} -{"algo":"WPMAXSAT","avg_enode_per_class":1.9464018791373052,"best_cost":602.0,"extract_time":1947,"model":"../tests/models/resnet18.relay","num_eclass":9366,"num_enodes":18230,"solver_time":1524} -{"algo":"ILP-ACyc","avg_enode_per_class":1.9464018791373052,"best_cost":602.0,"extract_time":1573,"model":"../tests/models/resnet18.relay","num_eclass":9366,"num_enodes":18230,"solver_time":1158} -{"algo":"ILP-Topo","avg_enode_per_class":1.9464018791373052,"best_cost":602.0,"extract_time":4564,"model":"../tests/models/resnet18.relay","num_eclass":9366,"num_enodes":18230,"solver_time":4175} -{"algo":"Greedy","avg_enode_per_class":1.8526782843547038,"best_cost":1692.0,"extract_time":3,"model":"../tests/models/efficientnet.relay","num_eclass":15551,"num_enodes":28811,"solver_time":3} -{"algo":"WPMAXSAT","avg_enode_per_class":1.8526782843547038,"best_cost":1583.0,"extract_time":5106,"model":"../tests/models/efficientnet.relay","num_eclass":15551,"num_enodes":28811,"solver_time":4109} -{"algo":"ILP-ACyc","avg_enode_per_class":1.8526782843547038,"best_cost":1583.0,"extract_time":1105,"model":"../tests/models/efficientnet.relay","num_eclass":15551,"num_enodes":28811,"solver_time":278} -{"algo":"ILP-Topo","avg_enode_per_class":1.8526782843547038,"best_cost":1583.0,"extract_time":5497,"model":"../tests/models/efficientnet.relay","num_eclass":15551,"num_enodes":28811,"solver_time":4783} -{"algo":"Greedy","avg_enode_per_class":1.894946170198176,"best_cost":1801.0,"extract_time":4,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14583,"num_enodes":27634,"solver_time":4} -{"algo":"WPMAXSAT","avg_enode_per_class":1.894946170198176,"best_cost":1535.0,"extract_time":4457,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14583,"num_enodes":27634,"solver_time":3654} -{"algo":"ILP-ACyc","avg_enode_per_class":1.894946170198176,"best_cost":1535.0,"extract_time":1112,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14583,"num_enodes":27634,"solver_time":303} -{"algo":"ILP-Topo","avg_enode_per_class":1.894946170198176,"best_cost":1535.0,"extract_time":5173,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14583,"num_enodes":27634,"solver_time":4481} -{"algo":"Greedy","avg_enode_per_class":1.8799665680853799,"best_cost":2056.0,"extract_time":4,"model":"../tests/models/mobilenetv2.relay","num_eclass":15554,"num_enodes":29241,"solver_time":4} -{"algo":"WPMAXSAT","avg_enode_per_class":1.8799665680853799,"best_cost":1685.0,"extract_time":2404,"model":"../tests/models/mobilenetv2.relay","num_eclass":15554,"num_enodes":29241,"solver_time":1523} -{"algo":"ILP-ACyc","avg_enode_per_class":1.8799665680853799,"best_cost":1685.0,"extract_time":1158,"model":"../tests/models/mobilenetv2.relay","num_eclass":15554,"num_enodes":29241,"solver_time":340} -{"algo":"ILP-Topo","avg_enode_per_class":1.8799665680853799,"best_cost":1685.0,"extract_time":5593,"model":"../tests/models/mobilenetv2.relay","num_eclass":15554,"num_enodes":29241,"solver_time":4816} -{"algo":"Greedy","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":1,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":1} -{"algo":"WPMAXSAT","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":1313,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":783} -{"algo":"ILP-ACyc","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":1169,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":698} -{"algo":"ILP-Topo","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":4982,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":4574} -{"algo":"Greedy","avg_enode_per_class":1.9464018791373052,"best_cost":721.0,"extract_time":1,"model":"../tests/models/resnet18.relay","num_eclass":9366,"num_enodes":18230,"solver_time":1} -{"algo":"WPMAXSAT","avg_enode_per_class":1.9464018791373052,"best_cost":602.0,"extract_time":1108,"model":"../tests/models/resnet18.relay","num_eclass":9366,"num_enodes":18230,"solver_time":646} -{"algo":"ILP-ACyc","avg_enode_per_class":1.9464018791373052,"best_cost":602.0,"extract_time":1373,"model":"../tests/models/resnet18.relay","num_eclass":9366,"num_enodes":18230,"solver_time":914} -{"algo":"ILP-Topo","avg_enode_per_class":1.9464018791373052,"best_cost":602.0,"extract_time":4799,"model":"../tests/models/resnet18.relay","num_eclass":9366,"num_enodes":18230,"solver_time":4423} -{"algo":"Greedy","avg_enode_per_class":1.8516768095299754,"best_cost":1692.0,"extract_time":3,"model":"../tests/models/efficientnet.relay","num_eclass":15446,"num_enodes":28601,"solver_time":3} -{"algo":"WPMAXSAT","avg_enode_per_class":1.8516768095299754,"best_cost":1583.0,"extract_time":2301,"model":"../tests/models/efficientnet.relay","num_eclass":15446,"num_enodes":28601,"solver_time":1430} -{"algo":"ILP-ACyc","avg_enode_per_class":1.8516768095299754,"best_cost":1583.0,"extract_time":1132,"model":"../tests/models/efficientnet.relay","num_eclass":15446,"num_enodes":28601,"solver_time":263} -{"algo":"ILP-Topo","avg_enode_per_class":1.8516768095299754,"best_cost":1583.0,"extract_time":5740,"model":"../tests/models/efficientnet.relay","num_eclass":15446,"num_enodes":28601,"solver_time":4955} -{"algo":"Greedy","avg_enode_per_class":1.908307900983384,"best_cost":1801.0,"extract_time":4,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14745,"num_enodes":28138,"solver_time":4} -{"algo":"WPMAXSAT","avg_enode_per_class":1.908307900983384,"best_cost":1535.0,"extract_time":2286,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14745,"num_enodes":28138,"solver_time":1426} -{"algo":"ILP-ACyc","avg_enode_per_class":1.908307900983384,"best_cost":1535.0,"extract_time":1143,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14745,"num_enodes":28138,"solver_time":371} -{"algo":"ILP-Topo","avg_enode_per_class":1.908307900983384,"best_cost":1535.0,"extract_time":5515,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14745,"num_enodes":28138,"solver_time":4885} -{"algo":"Greedy","avg_enode_per_class":1.8917769700294904,"best_cost":1535.0,"extract_time":3,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14581,"num_enodes":27584,"solver_time":3} -{"algo":"WPMAXSAT","avg_enode_per_class":1.8917769700294904,"best_cost":1535.0,"extract_time":2195,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14581,"num_enodes":27584,"solver_time":1400} -{"algo":"ILP-ACyc","avg_enode_per_class":1.8917769700294904,"best_cost":1535.0,"extract_time":1047,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14581,"num_enodes":27584,"solver_time":327} -{"algo":"ILP-Topo","avg_enode_per_class":1.8917769700294904,"best_cost":1535.0,"extract_time":5544,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14581,"num_enodes":27584,"solver_time":4981} -{"algo":"Greedy","avg_enode_per_class":1.8743826358201197,"best_cost":1685.0,"extract_time":3,"model":"../tests/models/mobilenetv2.relay","num_eclass":15388,"num_enodes":28843,"solver_time":3} -{"algo":"WPMAXSAT","avg_enode_per_class":1.8743826358201197,"best_cost":1685.0,"extract_time":2380,"model":"../tests/models/mobilenetv2.relay","num_eclass":15388,"num_enodes":28843,"solver_time":1486} -{"algo":"ILP-ACyc","avg_enode_per_class":1.8743826358201197,"best_cost":1685.0,"extract_time":1115,"model":"../tests/models/mobilenetv2.relay","num_eclass":15388,"num_enodes":28843,"solver_time":318} -{"algo":"ILP-Topo","avg_enode_per_class":1.8743826358201197,"best_cost":1685.0,"extract_time":4558,"model":"../tests/models/mobilenetv2.relay","num_eclass":15388,"num_enodes":28843,"solver_time":3899} -{"algo":"Greedy","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":1,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":1} -{"algo":"WPMAXSAT","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":1271,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":790} -{"algo":"ILP-ACyc","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":1191,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":722} -{"algo":"ILP-Topo","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":4724,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":4305} -{"algo":"Greedy","avg_enode_per_class":1.9434002563007262,"best_cost":602.0,"extract_time":1,"model":"../tests/models/resnet18.relay","num_eclass":9364,"num_enodes":18198,"solver_time":1} -{"algo":"WPMAXSAT","avg_enode_per_class":1.9434002563007262,"best_cost":602.0,"extract_time":1217,"model":"../tests/models/resnet18.relay","num_eclass":9364,"num_enodes":18198,"solver_time":758} -{"algo":"ILP-ACyc","avg_enode_per_class":1.9434002563007262,"best_cost":602.0,"extract_time":1355,"model":"../tests/models/resnet18.relay","num_eclass":9364,"num_enodes":18198,"solver_time":868} -{"algo":"ILP-Topo","avg_enode_per_class":1.9434002563007262,"best_cost":602.0,"extract_time":5048,"model":"../tests/models/resnet18.relay","num_eclass":9364,"num_enodes":18198,"solver_time":4650} -{"algo":"Greedy","avg_enode_per_class":1.86069045174538,"best_cost":1583.0,"extract_time":3,"model":"../tests/models/efficientnet.relay","num_eclass":15584,"num_enodes":28997,"solver_time":3} -{"algo":"WPMAXSAT","avg_enode_per_class":1.86069045174538,"best_cost":1583.0,"extract_time":2438,"model":"../tests/models/efficientnet.relay","num_eclass":15584,"num_enodes":28997,"solver_time":1480} -{"algo":"ILP-ACyc","avg_enode_per_class":1.86069045174538,"best_cost":1583.0,"extract_time":1183,"model":"../tests/models/efficientnet.relay","num_eclass":15584,"num_enodes":28997,"solver_time":373} -{"algo":"ILP-Topo","avg_enode_per_class":1.86069045174538,"best_cost":1583.0,"extract_time":5586,"model":"../tests/models/efficientnet.relay","num_eclass":15584,"num_enodes":28997,"solver_time":4936} -{"algo":"Greedy","avg_enode_per_class":1.904475572258285,"best_cost":1535.0,"extract_time":3,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14635,"num_enodes":27872,"solver_time":3} -{"algo":"WPMAXSAT","avg_enode_per_class":1.904475572258285,"best_cost":1535.0,"extract_time":2227,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14635,"num_enodes":27872,"solver_time":1450} -{"algo":"ILP-ACyc","avg_enode_per_class":1.904475572258285,"best_cost":1535.0,"extract_time":1094,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14635,"num_enodes":27872,"solver_time":331} -{"algo":"ILP-Topo","avg_enode_per_class":1.904475572258285,"best_cost":1535.0,"extract_time":5920,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14635,"num_enodes":27872,"solver_time":5287} -{"algo":"Greedy","avg_enode_per_class":1.8854809670781894,"best_cost":1685.0,"extract_time":3,"model":"../tests/models/mobilenetv2.relay","num_eclass":15552,"num_enodes":29323,"solver_time":3} -{"algo":"WPMAXSAT","avg_enode_per_class":1.8854809670781894,"best_cost":1685.0,"extract_time":2624,"model":"../tests/models/mobilenetv2.relay","num_eclass":15552,"num_enodes":29323,"solver_time":1639} -{"algo":"ILP-ACyc","avg_enode_per_class":1.8854809670781894,"best_cost":1685.0,"extract_time":1144,"model":"../tests/models/mobilenetv2.relay","num_eclass":15552,"num_enodes":29323,"solver_time":367} -{"algo":"ILP-Topo","avg_enode_per_class":1.8854809670781894,"best_cost":1685.0,"extract_time":5169,"model":"../tests/models/mobilenetv2.relay","num_eclass":15552,"num_enodes":29323,"solver_time":4515} -{"algo":"Greedy","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":1,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":1} -{"algo":"WPMAXSAT","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":1300,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":816} -{"algo":"ILP-ACyc","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":1192,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":711} -{"algo":"ILP-Topo","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":5217,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":4839} -{"algo":"Greedy","avg_enode_per_class":1.933058925476603,"best_cost":602.0,"extract_time":1,"model":"../tests/models/resnet18.relay","num_eclass":9232,"num_enodes":17846,"solver_time":1} -{"algo":"WPMAXSAT","avg_enode_per_class":1.933058925476603,"best_cost":602.0,"extract_time":1178,"model":"../tests/models/resnet18.relay","num_eclass":9232,"num_enodes":17846,"solver_time":721} -{"algo":"ILP-ACyc","avg_enode_per_class":1.933058925476603,"best_cost":602.0,"extract_time":1062,"model":"../tests/models/resnet18.relay","num_eclass":9232,"num_enodes":17846,"solver_time":677} -{"algo":"ILP-Topo","avg_enode_per_class":1.933058925476603,"best_cost":602.0,"extract_time":3658,"model":"../tests/models/resnet18.relay","num_eclass":9232,"num_enodes":17846,"solver_time":3304} -{"algo":"Greedy","avg_enode_per_class":1.8519635523613962,"best_cost":1583.0,"extract_time":3,"model":"../tests/models/efficientnet.relay","num_eclass":15584,"num_enodes":28861,"solver_time":3} -{"algo":"WPMAXSAT","avg_enode_per_class":1.8519635523613962,"best_cost":1583.0,"extract_time":2442,"model":"../tests/models/efficientnet.relay","num_eclass":15584,"num_enodes":28861,"solver_time":1446} -{"algo":"ILP-ACyc","avg_enode_per_class":1.8519635523613962,"best_cost":1583.0,"extract_time":1107,"model":"../tests/models/efficientnet.relay","num_eclass":15584,"num_enodes":28861,"solver_time":282} -{"algo":"ILP-Topo","avg_enode_per_class":1.8519635523613962,"best_cost":1583.0,"extract_time":6235,"model":"../tests/models/efficientnet.relay","num_eclass":15584,"num_enodes":28861,"solver_time":5533} -{"algo":"Greedy","avg_enode_per_class":1.8921762897164331,"best_cost":1535.0,"extract_time":3,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14635,"num_enodes":27692,"solver_time":3} -{"algo":"WPMAXSAT","avg_enode_per_class":1.8921762897164331,"best_cost":1535.0,"extract_time":2388,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14635,"num_enodes":27692,"solver_time":1580} -{"algo":"ILP-ACyc","avg_enode_per_class":1.8921762897164331,"best_cost":1535.0,"extract_time":1045,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14635,"num_enodes":27692,"solver_time":337} -{"algo":"ILP-Topo","avg_enode_per_class":1.8921762897164331,"best_cost":1535.0,"extract_time":4982,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14635,"num_enodes":27692,"solver_time":4361} -{"algo":"Greedy","avg_enode_per_class":1.8851782605892593,"best_cost":1685.0,"extract_time":3,"model":"../tests/models/mobilenetv2.relay","num_eclass":15511,"num_enodes":29241,"solver_time":3} -{"algo":"WPMAXSAT","avg_enode_per_class":1.8851782605892593,"best_cost":1685.0,"extract_time":2423,"model":"../tests/models/mobilenetv2.relay","num_eclass":15511,"num_enodes":29241,"solver_time":1533} -{"algo":"ILP-ACyc","avg_enode_per_class":1.8851782605892593,"best_cost":1685.0,"extract_time":1141,"model":"../tests/models/mobilenetv2.relay","num_eclass":15511,"num_enodes":29241,"solver_time":315} -{"algo":"ILP-Topo","avg_enode_per_class":1.8851782605892593,"best_cost":1685.0,"extract_time":5396,"model":"../tests/models/mobilenetv2.relay","num_eclass":15511,"num_enodes":29241,"solver_time":4748} -{"algo":"Greedy","avg_enode_per_class":1.9741559953434227,"best_cost":681.0,"extract_time":1,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":16958,"solver_time":1} -{"algo":"WPMAXSAT","avg_enode_per_class":1.9741559953434227,"best_cost":681.0,"extract_time":1244,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":16958,"solver_time":770} -{"algo":"ILP-ACyc","avg_enode_per_class":1.9741559953434227,"best_cost":681.0,"extract_time":979,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":16958,"solver_time":527} -{"algo":"ILP-Topo","avg_enode_per_class":1.9741559953434227,"best_cost":681.0,"extract_time":5139,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":16958,"solver_time":4795} -{"algo":"Greedy","avg_enode_per_class":1.9434002563007262,"best_cost":602.0,"extract_time":1,"model":"../tests/models/resnet18.relay","num_eclass":9364,"num_enodes":18198,"solver_time":1} -{"algo":"WPMAXSAT","avg_enode_per_class":1.9434002563007262,"best_cost":602.0,"extract_time":1187,"model":"../tests/models/resnet18.relay","num_eclass":9364,"num_enodes":18198,"solver_time":744} -{"algo":"ILP-ACyc","avg_enode_per_class":1.9434002563007262,"best_cost":602.0,"extract_time":1572,"model":"../tests/models/resnet18.relay","num_eclass":9364,"num_enodes":18198,"solver_time":1135} -{"algo":"ILP-Topo","avg_enode_per_class":1.9434002563007262,"best_cost":602.0,"extract_time":4649,"model":"../tests/models/resnet18.relay","num_eclass":9364,"num_enodes":18198,"solver_time":4283} -{"algo":"Greedy","avg_enode_per_class":1.8506216006216005,"best_cost":1583.0,"extract_time":3,"model":"../tests/models/efficientnet.relay","num_eclass":15444,"num_enodes":28581,"solver_time":3} -{"algo":"WPMAXSAT","avg_enode_per_class":1.8506216006216005,"best_cost":1583.0,"extract_time":2361,"model":"../tests/models/efficientnet.relay","num_eclass":15444,"num_enodes":28581,"solver_time":1454} -{"algo":"ILP-ACyc","avg_enode_per_class":1.8506216006216005,"best_cost":1583.0,"extract_time":1095,"model":"../tests/models/efficientnet.relay","num_eclass":15444,"num_enodes":28581,"solver_time":265} -{"algo":"ILP-Topo","avg_enode_per_class":1.8506216006216005,"best_cost":1583.0,"extract_time":6115,"model":"../tests/models/efficientnet.relay","num_eclass":15444,"num_enodes":28581,"solver_time":5366} -{"algo":"Greedy","avg_enode_per_class":1.8933567615057105,"best_cost":1535.0,"extract_time":3,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14797,"num_enodes":28016,"solver_time":3} -{"algo":"WPMAXSAT","avg_enode_per_class":1.8933567615057105,"best_cost":1535.0,"extract_time":2244,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14797,"num_enodes":28016,"solver_time":1440} -{"algo":"ILP-ACyc","avg_enode_per_class":1.8933567615057105,"best_cost":1535.0,"extract_time":1085,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14797,"num_enodes":28016,"solver_time":371} -{"algo":"ILP-Topo","avg_enode_per_class":1.8933567615057105,"best_cost":1535.0,"extract_time":5218,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14797,"num_enodes":28016,"solver_time":4634} -{"algo":"Greedy","avg_enode_per_class":1.8851782605892593,"best_cost":1685.0,"extract_time":3,"model":"../tests/models/mobilenetv2.relay","num_eclass":15511,"num_enodes":29241,"solver_time":3} -{"algo":"WPMAXSAT","avg_enode_per_class":1.8851782605892593,"best_cost":1685.0,"extract_time":2468,"model":"../tests/models/mobilenetv2.relay","num_eclass":15511,"num_enodes":29241,"solver_time":1554} -{"algo":"ILP-ACyc","avg_enode_per_class":1.8851782605892593,"best_cost":1685.0,"extract_time":1145,"model":"../tests/models/mobilenetv2.relay","num_eclass":15511,"num_enodes":29241,"solver_time":337} -{"algo":"ILP-Topo","avg_enode_per_class":1.8851782605892593,"best_cost":1685.0,"extract_time":5389,"model":"../tests/models/mobilenetv2.relay","num_eclass":15511,"num_enodes":29241,"solver_time":4675} -{"algo":"Greedy","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":1,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":1} -{"algo":"WPMAXSAT","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":1299,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":818} -{"algo":"ILP-ACyc","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":1135,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":675} -{"algo":"ILP-Topo","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":4751,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":4328} -{"algo":"Greedy","avg_enode_per_class":1.942727469202507,"best_cost":602.0,"extract_time":1,"model":"../tests/models/resnet18.relay","num_eclass":9254,"num_enodes":17978,"solver_time":1} -{"algo":"WPMAXSAT","avg_enode_per_class":1.942727469202507,"best_cost":602.0,"extract_time":1235,"model":"../tests/models/resnet18.relay","num_eclass":9254,"num_enodes":17978,"solver_time":725} -{"algo":"ILP-ACyc","avg_enode_per_class":1.942727469202507,"best_cost":602.0,"extract_time":1444,"model":"../tests/models/resnet18.relay","num_eclass":9254,"num_enodes":17978,"solver_time":922} -{"algo":"ILP-Topo","avg_enode_per_class":1.942727469202507,"best_cost":602.0,"extract_time":4222,"model":"../tests/models/resnet18.relay","num_eclass":9254,"num_enodes":17978,"solver_time":3825} -{"algo":"Greedy","avg_enode_per_class":1.8506216006216005,"best_cost":1583.0,"extract_time":3,"model":"../tests/models/efficientnet.relay","num_eclass":15444,"num_enodes":28581,"solver_time":3} -{"algo":"WPMAXSAT","avg_enode_per_class":1.8506216006216005,"best_cost":1583.0,"extract_time":2309,"model":"../tests/models/efficientnet.relay","num_eclass":15444,"num_enodes":28581,"solver_time":1406} -{"algo":"ILP-ACyc","avg_enode_per_class":1.8506216006216005,"best_cost":1583.0,"extract_time":1050,"model":"../tests/models/efficientnet.relay","num_eclass":15444,"num_enodes":28581,"solver_time":264} -{"algo":"ILP-Topo","avg_enode_per_class":1.8506216006216005,"best_cost":1583.0,"extract_time":6389,"model":"../tests/models/efficientnet.relay","num_eclass":15444,"num_enodes":28581,"solver_time":5783} -{"algo":"Greedy","avg_enode_per_class":1.8917769700294904,"best_cost":1535.0,"extract_time":5,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14581,"num_enodes":27584,"solver_time":5} -{"algo":"WPMAXSAT","avg_enode_per_class":1.8917769700294904,"best_cost":1535.0,"extract_time":4286,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14581,"num_enodes":27584,"solver_time":2111} -{"algo":"ILP-ACyc","avg_enode_per_class":1.8917769700294904,"best_cost":1535.0,"extract_time":3082,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14581,"num_enodes":27584,"solver_time":1127} -{"algo":"ILP-Topo","avg_enode_per_class":1.8917769700294904,"best_cost":1535.0,"extract_time":9451,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14581,"num_enodes":27584,"solver_time":8212} -{"algo":"Greedy","avg_enode_per_class":1.8743826358201197,"best_cost":1685.0,"extract_time":3,"model":"../tests/models/mobilenetv2.relay","num_eclass":15388,"num_enodes":28843,"solver_time":3} -{"algo":"WPMAXSAT","avg_enode_per_class":1.8743826358201197,"best_cost":1685.0,"extract_time":2406,"model":"../tests/models/mobilenetv2.relay","num_eclass":15388,"num_enodes":28843,"solver_time":1505} -{"algo":"ILP-ACyc","avg_enode_per_class":1.8743826358201197,"best_cost":1685.0,"extract_time":1064,"model":"../tests/models/mobilenetv2.relay","num_eclass":15388,"num_enodes":28843,"solver_time":303} -{"algo":"ILP-Topo","avg_enode_per_class":1.8743826358201197,"best_cost":1685.0,"extract_time":5053,"model":"../tests/models/mobilenetv2.relay","num_eclass":15388,"num_enodes":28843,"solver_time":4310} -{"algo":"Greedy","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":1,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":1} -{"algo":"WPMAXSAT","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":1292,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":811} -{"algo":"ILP-ACyc","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":1229,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":769} -{"algo":"ILP-Topo","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":5125,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":4743} -{"algo":"Greedy","avg_enode_per_class":1.9434002563007262,"best_cost":602.0,"extract_time":1,"model":"../tests/models/resnet18.relay","num_eclass":9364,"num_enodes":18198,"solver_time":1} -{"algo":"WPMAXSAT","avg_enode_per_class":1.9434002563007262,"best_cost":602.0,"extract_time":1213,"model":"../tests/models/resnet18.relay","num_eclass":9364,"num_enodes":18198,"solver_time":759} -{"algo":"ILP-ACyc","avg_enode_per_class":1.9434002563007262,"best_cost":602.0,"extract_time":1504,"model":"../tests/models/resnet18.relay","num_eclass":9364,"num_enodes":18198,"solver_time":1059} -{"algo":"ILP-Topo","avg_enode_per_class":1.9434002563007262,"best_cost":602.0,"extract_time":4526,"model":"../tests/models/resnet18.relay","num_eclass":9364,"num_enodes":18198,"solver_time":4152} -{"algo":"Greedy","avg_enode_per_class":1.8509593643000193,"best_cost":1583.0,"extract_time":3,"model":"../tests/models/efficientnet.relay","num_eclass":15479,"num_enodes":28651,"solver_time":3} -{"algo":"WPMAXSAT","avg_enode_per_class":1.8509593643000193,"best_cost":1583.0,"extract_time":2347,"model":"../tests/models/efficientnet.relay","num_eclass":15479,"num_enodes":28651,"solver_time":1471} -{"algo":"ILP-ACyc","avg_enode_per_class":1.8509593643000193,"best_cost":1583.0,"extract_time":1042,"model":"../tests/models/efficientnet.relay","num_eclass":15479,"num_enodes":28651,"solver_time":270} -{"algo":"ILP-Topo","avg_enode_per_class":1.8509593643000193,"best_cost":1583.0,"extract_time":5700,"model":"../tests/models/efficientnet.relay","num_eclass":15479,"num_enodes":28651,"solver_time":5085} -{"algo":"Greedy","avg_enode_per_class":1.9041218023455182,"best_cost":1535.0,"extract_time":3,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14581,"num_enodes":27764,"solver_time":3} -{"algo":"WPMAXSAT","avg_enode_per_class":1.9041218023455182,"best_cost":1535.0,"extract_time":2236,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14581,"num_enodes":27764,"solver_time":1433} -{"algo":"ILP-ACyc","avg_enode_per_class":1.9041218023455182,"best_cost":1535.0,"extract_time":1067,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14581,"num_enodes":27764,"solver_time":322} -{"algo":"ILP-Topo","avg_enode_per_class":1.9041218023455182,"best_cost":1535.0,"extract_time":4768,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":14581,"num_enodes":27764,"solver_time":4161} +{"algo":"Greedy","avg_enode_per_class":1.9738239062786016,"best_cost":1685.0,"extract_time":2,"model":"../tests/models/mobilenetv2.relay","num_eclass":27315,"num_enodes":53915,"solver_time":2} +{"algo":"WPMAXSAT","avg_enode_per_class":1.9738239062786016,"best_cost":1685.0,"extract_time":2429,"model":"../tests/models/mobilenetv2.relay","num_eclass":27315,"num_enodes":53915,"solver_time":1737} +{"algo":"ILP-ACyc","avg_enode_per_class":1.9738239062786016,"best_cost":1685.0,"extract_time":909,"model":"../tests/models/mobilenetv2.relay","num_eclass":27315,"num_enodes":53915,"solver_time":315} +{"algo":"ILP-Topo","avg_enode_per_class":1.9738239062786016,"best_cost":1685.0,"extract_time":8202,"model":"../tests/models/mobilenetv2.relay","num_eclass":27315,"num_enodes":53915,"solver_time":7767} +{"algo":"Greedy","avg_enode_per_class":2.043522727272727,"best_cost":681.0,"extract_time":0,"model":"../tests/models/resmlp.relay","num_eclass":17600,"num_enodes":35966,"solver_time":0} +{"algo":"WPMAXSAT","avg_enode_per_class":2.043522727272727,"best_cost":681.0,"extract_time":1039,"model":"../tests/models/resmlp.relay","num_eclass":17600,"num_enodes":35966,"solver_time":629} +{"algo":"ILP-ACyc","avg_enode_per_class":2.043522727272727,"best_cost":681.0,"extract_time":508,"model":"../tests/models/resmlp.relay","num_eclass":17600,"num_enodes":35966,"solver_time":182} +{"algo":"ILP-Topo","avg_enode_per_class":2.043522727272727,"best_cost":681.0,"extract_time":5096,"model":"../tests/models/resmlp.relay","num_eclass":17600,"num_enodes":35966,"solver_time":4832} +{"algo":"Greedy","avg_enode_per_class":2.032279986408427,"best_cost":602.0,"extract_time":0,"model":"../tests/models/resnet18.relay","num_eclass":17658,"num_enodes":35886,"solver_time":0} +{"algo":"WPMAXSAT","avg_enode_per_class":2.032279986408427,"best_cost":602.0,"extract_time":986,"model":"../tests/models/resnet18.relay","num_eclass":17658,"num_enodes":35886,"solver_time":594} +{"algo":"ILP-ACyc","avg_enode_per_class":2.032279986408427,"best_cost":602.0,"extract_time":535,"model":"../tests/models/resnet18.relay","num_eclass":17658,"num_enodes":35886,"solver_time":225} +{"algo":"ILP-Topo","avg_enode_per_class":2.032279986408427,"best_cost":602.0,"extract_time":4522,"model":"../tests/models/resnet18.relay","num_eclass":17658,"num_enodes":35886,"solver_time":4260} +{"algo":"Greedy","avg_enode_per_class":1.9399955303933254,"best_cost":1583.0,"extract_time":1,"model":"../tests/models/efficientnet.relay","num_eclass":26848,"num_enodes":52085,"solver_time":1} +{"algo":"WPMAXSAT","avg_enode_per_class":1.9399955303933254,"best_cost":1583.0,"extract_time":1787,"model":"../tests/models/efficientnet.relay","num_eclass":26848,"num_enodes":52085,"solver_time":1140} +{"algo":"ILP-ACyc","avg_enode_per_class":1.9399955303933254,"best_cost":1583.0,"extract_time":885,"model":"../tests/models/efficientnet.relay","num_eclass":26848,"num_enodes":52085,"solver_time":340} +{"algo":"ILP-Topo","avg_enode_per_class":1.9399955303933254,"best_cost":1583.0,"extract_time":5669,"model":"../tests/models/efficientnet.relay","num_eclass":26848,"num_enodes":52085,"solver_time":5258} +{"algo":"Greedy","avg_enode_per_class":2.000262065953265,"best_cost":1535.0,"extract_time":1,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":22895,"num_enodes":45796,"solver_time":1} +{"algo":"WPMAXSAT","avg_enode_per_class":2.000262065953265,"best_cost":1535.0,"extract_time":1644,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":22895,"num_enodes":45796,"solver_time":1081} +{"algo":"ILP-ACyc","avg_enode_per_class":2.000262065953265,"best_cost":1535.0,"extract_time":724,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":22895,"num_enodes":45796,"solver_time":260} +{"algo":"ILP-Topo","avg_enode_per_class":2.000262065953265,"best_cost":1535.0,"extract_time":6096,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":22895,"num_enodes":45796,"solver_time":5733} +{"algo":"Greedy","avg_enode_per_class":1.9520787186914295,"best_cost":1685.0,"extract_time":1,"model":"../tests/models/mobilenetv2.relay","num_eclass":23476,"num_enodes":45827,"solver_time":1} +{"algo":"WPMAXSAT","avg_enode_per_class":1.9520787186914295,"best_cost":1685.0,"extract_time":1650,"model":"../tests/models/mobilenetv2.relay","num_eclass":23476,"num_enodes":45827,"solver_time":1100} +{"algo":"ILP-ACyc","avg_enode_per_class":1.9520787186914295,"best_cost":1685.0,"extract_time":710,"model":"../tests/models/mobilenetv2.relay","num_eclass":23476,"num_enodes":45827,"solver_time":249} +{"algo":"ILP-Topo","avg_enode_per_class":1.9520787186914295,"best_cost":1685.0,"extract_time":5953,"model":"../tests/models/mobilenetv2.relay","num_eclass":23476,"num_enodes":45827,"solver_time":5584} +{"algo":"Greedy","avg_enode_per_class":2.0443852126550004,"best_cost":681.0,"extract_time":0,"model":"../tests/models/resmlp.relay","num_eclass":17258,"num_enodes":35282,"solver_time":0} +{"algo":"WPMAXSAT","avg_enode_per_class":2.0443852126550004,"best_cost":681.0,"extract_time":1130,"model":"../tests/models/resmlp.relay","num_eclass":17258,"num_enodes":35282,"solver_time":722} +{"algo":"ILP-ACyc","avg_enode_per_class":2.0443852126550004,"best_cost":681.0,"extract_time":500,"model":"../tests/models/resmlp.relay","num_eclass":17258,"num_enodes":35282,"solver_time":174} +{"algo":"ILP-Topo","avg_enode_per_class":2.0443852126550004,"best_cost":681.0,"extract_time":7337,"model":"../tests/models/resmlp.relay","num_eclass":17258,"num_enodes":35282,"solver_time":7075} +{"algo":"Greedy","avg_enode_per_class":2.0322398190045248,"best_cost":602.0,"extract_time":0,"model":"../tests/models/resnet18.relay","num_eclass":17680,"num_enodes":35930,"solver_time":0} +{"algo":"WPMAXSAT","avg_enode_per_class":2.0322398190045248,"best_cost":602.0,"extract_time":976,"model":"../tests/models/resnet18.relay","num_eclass":17680,"num_enodes":35930,"solver_time":589} +{"algo":"ILP-ACyc","avg_enode_per_class":2.0322398190045248,"best_cost":602.0,"extract_time":551,"model":"../tests/models/resnet18.relay","num_eclass":17680,"num_enodes":35930,"solver_time":236} +{"algo":"ILP-Topo","avg_enode_per_class":2.0322398190045248,"best_cost":602.0,"extract_time":4518,"model":"../tests/models/resnet18.relay","num_eclass":17680,"num_enodes":35930,"solver_time":4245} +{"algo":"Greedy","avg_enode_per_class":1.9399955303933254,"best_cost":1583.0,"extract_time":1,"model":"../tests/models/efficientnet.relay","num_eclass":26848,"num_enodes":52085,"solver_time":1} +{"algo":"WPMAXSAT","avg_enode_per_class":1.9399955303933254,"best_cost":1583.0,"extract_time":1824,"model":"../tests/models/efficientnet.relay","num_eclass":26848,"num_enodes":52085,"solver_time":1151} +{"algo":"ILP-ACyc","avg_enode_per_class":1.9399955303933254,"best_cost":1583.0,"extract_time":864,"model":"../tests/models/efficientnet.relay","num_eclass":26848,"num_enodes":52085,"solver_time":318} +{"algo":"ILP-Topo","avg_enode_per_class":1.9399955303933254,"best_cost":1583.0,"extract_time":6180,"model":"../tests/models/efficientnet.relay","num_eclass":26848,"num_enodes":52085,"solver_time":5772} +{"algo":"Greedy","avg_enode_per_class":1.9798170685614938,"best_cost":1535.0,"extract_time":1,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":26458,"num_enodes":52382,"solver_time":1} +{"algo":"WPMAXSAT","avg_enode_per_class":1.9798170685614938,"best_cost":1535.0,"extract_time":1729,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":26458,"num_enodes":52382,"solver_time":1096} +{"algo":"ILP-ACyc","avg_enode_per_class":1.9798170685614938,"best_cost":1535.0,"extract_time":826,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":26458,"num_enodes":52382,"solver_time":296} +{"algo":"ILP-Topo","avg_enode_per_class":1.9798170685614938,"best_cost":1535.0,"extract_time":6309,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":26458,"num_enodes":52382,"solver_time":5914} +{"algo":"Greedy","avg_enode_per_class":1.9515712440809299,"best_cost":1685.0,"extract_time":1,"model":"../tests/models/mobilenetv2.relay","num_eclass":23230,"num_enodes":45335,"solver_time":1} +{"algo":"WPMAXSAT","avg_enode_per_class":1.9515712440809299,"best_cost":1685.0,"extract_time":1684,"model":"../tests/models/mobilenetv2.relay","num_eclass":23230,"num_enodes":45335,"solver_time":1142} +{"algo":"ILP-ACyc","avg_enode_per_class":1.9515712440809299,"best_cost":1685.0,"extract_time":699,"model":"../tests/models/mobilenetv2.relay","num_eclass":23230,"num_enodes":45335,"solver_time":250} +{"algo":"ILP-Topo","avg_enode_per_class":1.9515712440809299,"best_cost":1685.0,"extract_time":5095,"model":"../tests/models/mobilenetv2.relay","num_eclass":23230,"num_enodes":45335,"solver_time":4725} +{"algo":"Greedy","avg_enode_per_class":2.0451810782116313,"best_cost":681.0,"extract_time":0,"model":"../tests/models/resmlp.relay","num_eclass":16954,"num_enodes":34674,"solver_time":0} +{"algo":"WPMAXSAT","avg_enode_per_class":2.0451810782116313,"best_cost":681.0,"extract_time":1079,"model":"../tests/models/resmlp.relay","num_eclass":16954,"num_enodes":34674,"solver_time":669} +{"algo":"ILP-ACyc","avg_enode_per_class":2.0451810782116313,"best_cost":681.0,"extract_time":496,"model":"../tests/models/resmlp.relay","num_eclass":16954,"num_enodes":34674,"solver_time":174} +{"algo":"ILP-Topo","avg_enode_per_class":2.0451810782116313,"best_cost":681.0,"extract_time":5683,"model":"../tests/models/resmlp.relay","num_eclass":16954,"num_enodes":34674,"solver_time":5421} +{"algo":"Greedy","avg_enode_per_class":2.0322398190045248,"best_cost":602.0,"extract_time":0,"model":"../tests/models/resnet18.relay","num_eclass":17680,"num_enodes":35930,"solver_time":0} +{"algo":"WPMAXSAT","avg_enode_per_class":2.0322398190045248,"best_cost":602.0,"extract_time":1046,"model":"../tests/models/resnet18.relay","num_eclass":17680,"num_enodes":35930,"solver_time":646} +{"algo":"ILP-ACyc","avg_enode_per_class":2.0322398190045248,"best_cost":602.0,"extract_time":536,"model":"../tests/models/resnet18.relay","num_eclass":17680,"num_enodes":35930,"solver_time":224} +{"algo":"ILP-Topo","avg_enode_per_class":2.0322398190045248,"best_cost":602.0,"extract_time":4517,"model":"../tests/models/resnet18.relay","num_eclass":17680,"num_enodes":35930,"solver_time":4249} +{"algo":"Greedy","avg_enode_per_class":1.9399955303933254,"best_cost":1583.0,"extract_time":1,"model":"../tests/models/efficientnet.relay","num_eclass":26848,"num_enodes":52085,"solver_time":1} +{"algo":"WPMAXSAT","avg_enode_per_class":1.9399955303933254,"best_cost":1583.0,"extract_time":1879,"model":"../tests/models/efficientnet.relay","num_eclass":26848,"num_enodes":52085,"solver_time":1222} +{"algo":"ILP-ACyc","avg_enode_per_class":1.9399955303933254,"best_cost":1583.0,"extract_time":865,"model":"../tests/models/efficientnet.relay","num_eclass":26848,"num_enodes":52085,"solver_time":314} +{"algo":"ILP-Topo","avg_enode_per_class":1.9399955303933254,"best_cost":1583.0,"extract_time":5970,"model":"../tests/models/efficientnet.relay","num_eclass":26848,"num_enodes":52085,"solver_time":5561} +{"algo":"Greedy","avg_enode_per_class":1.9798170685614938,"best_cost":1535.0,"extract_time":1,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":26458,"num_enodes":52382,"solver_time":1} +{"algo":"WPMAXSAT","avg_enode_per_class":1.9798170685614938,"best_cost":1535.0,"extract_time":1749,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":26458,"num_enodes":52382,"solver_time":1116} +{"algo":"ILP-ACyc","avg_enode_per_class":1.9798170685614938,"best_cost":1535.0,"extract_time":815,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":26458,"num_enodes":52382,"solver_time":283} +{"algo":"ILP-Topo","avg_enode_per_class":1.9798170685614938,"best_cost":1535.0,"extract_time":7355,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":26458,"num_enodes":52382,"solver_time":6959} +{"algo":"Greedy","avg_enode_per_class":1.9735860209095275,"best_cost":1685.0,"extract_time":1,"model":"../tests/models/mobilenetv2.relay","num_eclass":27069,"num_enodes":53423,"solver_time":1} +{"algo":"WPMAXSAT","avg_enode_per_class":1.9735860209095275,"best_cost":1685.0,"extract_time":2216,"model":"../tests/models/mobilenetv2.relay","num_eclass":27069,"num_enodes":53423,"solver_time":1498} +{"algo":"ILP-ACyc","avg_enode_per_class":1.9735860209095275,"best_cost":1685.0,"extract_time":904,"model":"../tests/models/mobilenetv2.relay","num_eclass":27069,"num_enodes":53423,"solver_time":318} +{"algo":"ILP-Topo","avg_enode_per_class":1.9735860209095275,"best_cost":1685.0,"extract_time":6644,"model":"../tests/models/mobilenetv2.relay","num_eclass":27069,"num_enodes":53423,"solver_time":6211} +{"algo":"Greedy","avg_enode_per_class":2.043522727272727,"best_cost":681.0,"extract_time":0,"model":"../tests/models/resmlp.relay","num_eclass":17600,"num_enodes":35966,"solver_time":0} +{"algo":"WPMAXSAT","avg_enode_per_class":2.043522727272727,"best_cost":681.0,"extract_time":1236,"model":"../tests/models/resmlp.relay","num_eclass":17600,"num_enodes":35966,"solver_time":752} +{"algo":"ILP-ACyc","avg_enode_per_class":2.043522727272727,"best_cost":681.0,"extract_time":521,"model":"../tests/models/resmlp.relay","num_eclass":17600,"num_enodes":35966,"solver_time":170} +{"algo":"ILP-Topo","avg_enode_per_class":2.043522727272727,"best_cost":681.0,"extract_time":5719,"model":"../tests/models/resmlp.relay","num_eclass":17600,"num_enodes":35966,"solver_time":5427} +{"algo":"Greedy","avg_enode_per_class":2.032279986408427,"best_cost":602.0,"extract_time":0,"model":"../tests/models/resnet18.relay","num_eclass":17658,"num_enodes":35886,"solver_time":0} +{"algo":"WPMAXSAT","avg_enode_per_class":2.032279986408427,"best_cost":602.0,"extract_time":1110,"model":"../tests/models/resnet18.relay","num_eclass":17658,"num_enodes":35886,"solver_time":669} +{"algo":"ILP-ACyc","avg_enode_per_class":2.032279986408427,"best_cost":602.0,"extract_time":569,"model":"../tests/models/resnet18.relay","num_eclass":17658,"num_enodes":35886,"solver_time":219} +{"algo":"ILP-Topo","avg_enode_per_class":2.032279986408427,"best_cost":602.0,"extract_time":5135,"model":"../tests/models/resnet18.relay","num_eclass":17658,"num_enodes":35886,"solver_time":4850} +{"algo":"Greedy","avg_enode_per_class":1.9399172043411779,"best_cost":1583.0,"extract_time":1,"model":"../tests/models/efficientnet.relay","num_eclass":26813,"num_enodes":52015,"solver_time":1} +{"algo":"WPMAXSAT","avg_enode_per_class":1.9399172043411779,"best_cost":1583.0,"extract_time":1877,"model":"../tests/models/efficientnet.relay","num_eclass":26813,"num_enodes":52015,"solver_time":1229} +{"algo":"ILP-ACyc","avg_enode_per_class":1.9399172043411779,"best_cost":1583.0,"extract_time":926,"model":"../tests/models/efficientnet.relay","num_eclass":26813,"num_enodes":52015,"solver_time":374} +{"algo":"ILP-Topo","avg_enode_per_class":1.9399172043411779,"best_cost":1583.0,"extract_time":7541,"model":"../tests/models/efficientnet.relay","num_eclass":26813,"num_enodes":52015,"solver_time":7132} +{"algo":"Greedy","avg_enode_per_class":1.9763413229365114,"best_cost":1535.0,"extract_time":1,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":22571,"num_enodes":44608,"solver_time":1} +{"algo":"WPMAXSAT","avg_enode_per_class":1.9763413229365114,"best_cost":1535.0,"extract_time":1770,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":22571,"num_enodes":44608,"solver_time":1164} +{"algo":"ILP-ACyc","avg_enode_per_class":1.9763413229365114,"best_cost":1535.0,"extract_time":742,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":22571,"num_enodes":44608,"solver_time":268} +{"algo":"ILP-Topo","avg_enode_per_class":1.9763413229365114,"best_cost":1535.0,"extract_time":5699,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":22571,"num_enodes":44608,"solver_time":5335} +{"algo":"Greedy","avg_enode_per_class":1.9521622655951014,"best_cost":1685.0,"extract_time":1,"model":"../tests/models/mobilenetv2.relay","num_eclass":23517,"num_enodes":45909,"solver_time":1} +{"algo":"WPMAXSAT","avg_enode_per_class":1.9521622655951014,"best_cost":1685.0,"extract_time":1708,"model":"../tests/models/mobilenetv2.relay","num_eclass":23517,"num_enodes":45909,"solver_time":1147} +{"algo":"ILP-ACyc","avg_enode_per_class":1.9521622655951014,"best_cost":1685.0,"extract_time":728,"model":"../tests/models/mobilenetv2.relay","num_eclass":23517,"num_enodes":45909,"solver_time":256} +{"algo":"ILP-Topo","avg_enode_per_class":1.9521622655951014,"best_cost":1685.0,"extract_time":6615,"model":"../tests/models/mobilenetv2.relay","num_eclass":23517,"num_enodes":45909,"solver_time":6229} +{"algo":"Greedy","avg_enode_per_class":2.0443852126550004,"best_cost":681.0,"extract_time":0,"model":"../tests/models/resmlp.relay","num_eclass":17258,"num_enodes":35282,"solver_time":0} +{"algo":"WPMAXSAT","avg_enode_per_class":2.0443852126550004,"best_cost":681.0,"extract_time":1209,"model":"../tests/models/resmlp.relay","num_eclass":17258,"num_enodes":35282,"solver_time":744} +{"algo":"ILP-ACyc","avg_enode_per_class":2.0443852126550004,"best_cost":681.0,"extract_time":526,"model":"../tests/models/resmlp.relay","num_eclass":17258,"num_enodes":35282,"solver_time":170} +{"algo":"ILP-Topo","avg_enode_per_class":2.0443852126550004,"best_cost":681.0,"extract_time":6608,"model":"../tests/models/resmlp.relay","num_eclass":17258,"num_enodes":35282,"solver_time":6317} +{"algo":"Greedy","avg_enode_per_class":2.0136085280108866,"best_cost":602.0,"extract_time":0,"model":"../tests/models/resnet18.relay","num_eclass":17636,"num_enodes":35512,"solver_time":0} +{"algo":"WPMAXSAT","avg_enode_per_class":2.0136085280108866,"best_cost":602.0,"extract_time":1111,"model":"../tests/models/resnet18.relay","num_eclass":17636,"num_enodes":35512,"solver_time":680} +{"algo":"ILP-ACyc","avg_enode_per_class":2.0136085280108866,"best_cost":602.0,"extract_time":571,"model":"../tests/models/resnet18.relay","num_eclass":17636,"num_enodes":35512,"solver_time":224} +{"algo":"ILP-Topo","avg_enode_per_class":2.0136085280108866,"best_cost":602.0,"extract_time":5503,"model":"../tests/models/resnet18.relay","num_eclass":17636,"num_enodes":35512,"solver_time":5202} +{"algo":"Greedy","avg_enode_per_class":1.9301690507152145,"best_cost":1583.0,"extract_time":1,"model":"../tests/models/efficientnet.relay","num_eclass":23070,"num_enodes":44529,"solver_time":1} +{"algo":"WPMAXSAT","avg_enode_per_class":1.9301690507152145,"best_cost":1583.0,"extract_time":1786,"model":"../tests/models/efficientnet.relay","num_eclass":23070,"num_enodes":44529,"solver_time":1168} +{"algo":"ILP-ACyc","avg_enode_per_class":1.9301690507152145,"best_cost":1583.0,"extract_time":803,"model":"../tests/models/efficientnet.relay","num_eclass":23070,"num_enodes":44529,"solver_time":289} +{"algo":"ILP-Topo","avg_enode_per_class":1.9301690507152145,"best_cost":1583.0,"extract_time":5799,"model":"../tests/models/efficientnet.relay","num_eclass":23070,"num_enodes":44529,"solver_time":5388} +{"algo":"Greedy","avg_enode_per_class":1.9763413229365114,"best_cost":1535.0,"extract_time":1,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":22571,"num_enodes":44608,"solver_time":1} +{"algo":"WPMAXSAT","avg_enode_per_class":1.9763413229365114,"best_cost":1535.0,"extract_time":1682,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":22571,"num_enodes":44608,"solver_time":1095} +{"algo":"ILP-ACyc","avg_enode_per_class":1.9763413229365114,"best_cost":1535.0,"extract_time":735,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":22571,"num_enodes":44608,"solver_time":244} +{"algo":"ILP-Topo","avg_enode_per_class":1.9763413229365114,"best_cost":1535.0,"extract_time":6778,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":22571,"num_enodes":44608,"solver_time":6381} diff --git a/flexmatch/extraction_stats_im2col_with_simpl.txt b/flexmatch/extraction_stats_im2col_with_simpl.txt index 9e1c5bb..92c6125 100644 --- a/flexmatch/extraction_stats_im2col_with_simpl.txt +++ b/flexmatch/extraction_stats_im2col_with_simpl.txt @@ -1,79 +1,70 @@ -{"algo":"Greedy","avg_enode_per_class":1.8747164430617669,"best_cost":1685.0,"extract_time":3,"model":"../tests/models/mobilenetv2.relay","num_eclass":15429,"num_enodes":28925,"solver_time":3} -{"algo":"WPMAXSAT","avg_enode_per_class":1.8747164430617669,"best_cost":1685.0,"extract_time":2368,"model":"../tests/models/mobilenetv2.relay","num_eclass":15429,"num_enodes":28925,"solver_time":1506} -{"algo":"ILP-ACyc","avg_enode_per_class":1.8747164430617669,"best_cost":1685.0,"extract_time":1083,"model":"../tests/models/mobilenetv2.relay","num_eclass":15429,"num_enodes":28925,"solver_time":325} -{"algo":"ILP-Topo","avg_enode_per_class":1.8747164430617669,"best_cost":1685.0,"extract_time":5009,"model":"../tests/models/mobilenetv2.relay","num_eclass":15429,"num_enodes":28925,"solver_time":4361} -{"algo":"Greedy","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":1,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":1} -{"algo":"WPMAXSAT","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":1273,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":794} -{"algo":"ILP-ACyc","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":1128,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":702} -{"algo":"ILP-Topo","avg_enode_per_class":2.0449359720605353,"best_cost":681.0,"extract_time":5161,"model":"../tests/models/resmlp.relay","num_eclass":8590,"num_enodes":17566,"solver_time":4800} -{"algo":"Greedy","avg_enode_per_class":1.9434002563007262,"best_cost":602.0,"extract_time":1,"model":"../tests/models/resnet18.relay","num_eclass":9364,"num_enodes":18198,"solver_time":1} -{"algo":"WPMAXSAT","avg_enode_per_class":1.9434002563007262,"best_cost":602.0,"extract_time":1184,"model":"../tests/models/resnet18.relay","num_eclass":9364,"num_enodes":18198,"solver_time":724} -{"algo":"ILP-ACyc","avg_enode_per_class":1.9434002563007262,"best_cost":602.0,"extract_time":1375,"model":"../tests/models/resnet18.relay","num_eclass":9364,"num_enodes":18198,"solver_time":924} -{"algo":"ILP-Topo","avg_enode_per_class":1.9434002563007262,"best_cost":602.0,"extract_time":4586,"model":"../tests/models/resnet18.relay","num_eclass":9364,"num_enodes":18198,"solver_time":4229} -{"algo":"WPMAXSAT","avg_enode_per_class":2.1604213573496303,"best_cost":1658.0,"extract_time":2089,"model":"../tests/models/mobilenetv2.relay","num_eclass":12436,"num_enodes":26867,"solver_time":1287} -{"algo":"WPMAXSAT","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":585,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":322} -{"algo":"ILP-Topo","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":1258,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":1087} -{"algo":"WPMAXSAT","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":473,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":262} -{"algo":"ILP-Topo","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":1689,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":1534} -{"algo":"WPMAXSAT","avg_enode_per_class":2.1604213573496303,"best_cost":1658.0,"extract_time":2119,"model":"../tests/models/mobilenetv2.relay","num_eclass":12436,"num_enodes":26867,"solver_time":1321} -{"algo":"ILP-ACyc","avg_enode_per_class":2.1063965544743977,"best_cost":1583.0,"extract_time":871,"model":"../tests/models/efficientnet.relay","num_eclass":12538,"num_enodes":26410,"solver_time":231} -{"algo":"ILP-ACyc","avg_enode_per_class":2.109090909090909,"best_cost":1583.0,"extract_time":885,"model":"../tests/models/efficientnet.relay","num_eclass":12540,"num_enodes":26448,"solver_time":232} -{"algo":"WPMAXSAT","avg_enode_per_class":2.1604213573496303,"best_cost":1658.0,"extract_time":2037,"model":"../tests/models/mobilenetv2.relay","num_eclass":12436,"num_enodes":26867,"solver_time":1274} -{"algo":"ILP-ACyc","avg_enode_per_class":2.1604213573496303,"best_cost":1658.0,"extract_time":996,"model":"../tests/models/mobilenetv2.relay","num_eclass":12436,"num_enodes":26867,"solver_time":269} -{"algo":"WPMAXSAT","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":588,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":331} -{"algo":"ILP-ACyc","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":295,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":87} -{"algo":"WPMAXSAT","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":491,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":268} -{"algo":"ILP-ACyc","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":1127,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":969} -{"algo":"ILP-Topo","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":1768,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":1601} -{"algo":"WPMAXSAT","avg_enode_per_class":2.1063965544743977,"best_cost":1583.0,"extract_time":2099,"model":"../tests/models/efficientnet.relay","num_eclass":12538,"num_enodes":26410,"solver_time":1281} -{"algo":"ILP-ACyc","avg_enode_per_class":2.1063965544743977,"best_cost":1583.0,"extract_time":913,"model":"../tests/models/efficientnet.relay","num_eclass":12538,"num_enodes":26410,"solver_time":230} -{"algo":"WPMAXSAT","avg_enode_per_class":2.19946474868278,"best_cost":1529.0,"extract_time":2238,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":11957,"num_enodes":26299,"solver_time":1376} -{"algo":"ILP-ACyc","avg_enode_per_class":2.19946474868278,"best_cost":1529.0,"extract_time":867,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":11957,"num_enodes":26299,"solver_time":237} -{"algo":"WPMAXSAT","avg_enode_per_class":2.1604213573496303,"best_cost":1658.0,"extract_time":2162,"model":"../tests/models/mobilenetv2.relay","num_eclass":12436,"num_enodes":26867,"solver_time":1304} -{"algo":"ILP-ACyc","avg_enode_per_class":2.1604213573496303,"best_cost":1658.0,"extract_time":873,"model":"../tests/models/mobilenetv2.relay","num_eclass":12436,"num_enodes":26867,"solver_time":265} -{"algo":"WPMAXSAT","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":586,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":337} -{"algo":"ILP-ACyc","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":275,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":86} -{"algo":"ILP-Topo","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":1267,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":1114} -{"algo":"WPMAXSAT","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":513,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":272} -{"algo":"ILP-ACyc","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":1205,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":1045} -{"algo":"ILP-Topo","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":1588,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":1426} -{"algo":"WPMAXSAT","avg_enode_per_class":2.1063965544743977,"best_cost":1583.0,"extract_time":2155,"model":"../tests/models/efficientnet.relay","num_eclass":12538,"num_enodes":26410,"solver_time":1300} -{"algo":"ILP-ACyc","avg_enode_per_class":2.1063965544743977,"best_cost":1583.0,"extract_time":870,"model":"../tests/models/efficientnet.relay","num_eclass":12538,"num_enodes":26410,"solver_time":230} -{"algo":"WPMAXSAT","avg_enode_per_class":2.19946474868278,"best_cost":1529.0,"extract_time":2042,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":11957,"num_enodes":26299,"solver_time":1293} -{"algo":"ILP-ACyc","avg_enode_per_class":2.19946474868278,"best_cost":1529.0,"extract_time":851,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":11957,"num_enodes":26299,"solver_time":243} -{"algo":"WPMAXSAT","avg_enode_per_class":2.1604213573496303,"best_cost":1658.0,"extract_time":2124,"model":"../tests/models/mobilenetv2.relay","num_eclass":12436,"num_enodes":26867,"solver_time":1367} -{"algo":"ILP-ACyc","avg_enode_per_class":2.1604213573496303,"best_cost":1658.0,"extract_time":898,"model":"../tests/models/mobilenetv2.relay","num_eclass":12436,"num_enodes":26867,"solver_time":264} -{"algo":"WPMAXSAT","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":481,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":251} -{"algo":"ILP-ACyc","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":289,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":86} -{"algo":"ILP-Topo","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":1638,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":1486} -{"algo":"WPMAXSAT","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":493,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":276} -{"algo":"ILP-ACyc","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":1379,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":1216} -{"algo":"ILP-Topo","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":1538,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":1398} -{"algo":"WPMAXSAT","avg_enode_per_class":2.1063965544743977,"best_cost":1583.0,"extract_time":2083,"model":"../tests/models/efficientnet.relay","num_eclass":12538,"num_enodes":26410,"solver_time":1305} -{"algo":"ILP-ACyc","avg_enode_per_class":2.1063965544743977,"best_cost":1583.0,"extract_time":910,"model":"../tests/models/efficientnet.relay","num_eclass":12538,"num_enodes":26410,"solver_time":234} -{"algo":"WPMAXSAT","avg_enode_per_class":2.19946474868278,"best_cost":1529.0,"extract_time":2217,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":11957,"num_enodes":26299,"solver_time":1417} -{"algo":"ILP-ACyc","avg_enode_per_class":2.19946474868278,"best_cost":1529.0,"extract_time":941,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":11957,"num_enodes":26299,"solver_time":237} -{"algo":"WPMAXSAT","avg_enode_per_class":2.1604213573496303,"best_cost":1658.0,"extract_time":2081,"model":"../tests/models/mobilenetv2.relay","num_eclass":12436,"num_enodes":26867,"solver_time":1289} -{"algo":"ILP-ACyc","avg_enode_per_class":2.1604213573496303,"best_cost":1658.0,"extract_time":906,"model":"../tests/models/mobilenetv2.relay","num_eclass":12436,"num_enodes":26867,"solver_time":257} -{"algo":"WPMAXSAT","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":575,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":343} -{"algo":"ILP-ACyc","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":287,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":86} -{"algo":"ILP-Topo","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":1526,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":1390} -{"algo":"WPMAXSAT","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":501,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":269} -{"algo":"ILP-ACyc","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":1017,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":840} -{"algo":"ILP-Topo","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":1771,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":1617} -{"algo":"WPMAXSAT","avg_enode_per_class":2.1063965544743977,"best_cost":1583.0,"extract_time":2081,"model":"../tests/models/efficientnet.relay","num_eclass":12538,"num_enodes":26410,"solver_time":1273} -{"algo":"ILP-ACyc","avg_enode_per_class":2.1063965544743977,"best_cost":1583.0,"extract_time":906,"model":"../tests/models/efficientnet.relay","num_eclass":12538,"num_enodes":26410,"solver_time":231} -{"algo":"WPMAXSAT","avg_enode_per_class":2.19946474868278,"best_cost":1529.0,"extract_time":2199,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":11957,"num_enodes":26299,"solver_time":1414} -{"algo":"ILP-ACyc","avg_enode_per_class":2.19946474868278,"best_cost":1529.0,"extract_time":838,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":11957,"num_enodes":26299,"solver_time":241} -{"algo":"WPMAXSAT","avg_enode_per_class":2.1604213573496303,"best_cost":1658.0,"extract_time":2102,"model":"../tests/models/mobilenetv2.relay","num_eclass":12436,"num_enodes":26867,"solver_time":1344} -{"algo":"ILP-ACyc","avg_enode_per_class":2.1604213573496303,"best_cost":1658.0,"extract_time":918,"model":"../tests/models/mobilenetv2.relay","num_eclass":12436,"num_enodes":26867,"solver_time":265} -{"algo":"WPMAXSAT","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":579,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":342} -{"algo":"ILP-ACyc","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":305,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":109} -{"algo":"ILP-Topo","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":1259,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":1090} -{"algo":"WPMAXSAT","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":479,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":267} -{"algo":"ILP-ACyc","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":997,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":817} -{"algo":"ILP-Topo","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":1630,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":1497} -{"algo":"WPMAXSAT","avg_enode_per_class":2.1063965544743977,"best_cost":1583.0,"extract_time":2128,"model":"../tests/models/efficientnet.relay","num_eclass":12538,"num_enodes":26410,"solver_time":1279} -{"algo":"ILP-ACyc","avg_enode_per_class":2.1063965544743977,"best_cost":1583.0,"extract_time":944,"model":"../tests/models/efficientnet.relay","num_eclass":12538,"num_enodes":26410,"solver_time":233} -{"algo":"WPMAXSAT","avg_enode_per_class":2.19946474868278,"best_cost":1529.0,"extract_time":2110,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":11957,"num_enodes":26299,"solver_time":1365} -{"algo":"ILP-ACyc","avg_enode_per_class":2.19946474868278,"best_cost":1529.0,"extract_time":862,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":11957,"num_enodes":26299,"solver_time":239} +{"algo":"WPMAXSAT","avg_enode_per_class":2.7400606980273143,"best_cost":1658.0,"extract_time":566,"model":"../tests/models/mobilenetv2.relay","num_eclass":6590,"num_enodes":18057,"solver_time":319} +{"algo":"ILP-ACyc","avg_enode_per_class":2.7400606980273143,"best_cost":1658.0,"extract_time":281,"model":"../tests/models/mobilenetv2.relay","num_eclass":6590,"num_enodes":18057,"solver_time":76} +{"algo":"ILP-Topo","avg_enode_per_class":2.7400606980273143,"best_cost":1658.0,"extract_time":1025,"model":"../tests/models/mobilenetv2.relay","num_eclass":6590,"num_enodes":18057,"solver_time":859} +{"algo":"WPMAXSAT","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":213,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":118} +{"algo":"ILP-ACyc","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":137,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":60} +{"algo":"ILP-Topo","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":721,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":656} +{"algo":"WPMAXSAT","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":171,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":83} +{"algo":"ILP-ACyc","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":172,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":102} +{"algo":"ILP-Topo","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":694,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":633} +{"algo":"WPMAXSAT","avg_enode_per_class":2.666716328963051,"best_cost":1583.0,"extract_time":574,"model":"../tests/models/efficientnet.relay","num_eclass":6712,"num_enodes":17899,"solver_time":311} +{"algo":"ILP-ACyc","avg_enode_per_class":2.666716328963051,"best_cost":1583.0,"extract_time":304,"model":"../tests/models/efficientnet.relay","num_eclass":6712,"num_enodes":17899,"solver_time":79} +{"algo":"ILP-Topo","avg_enode_per_class":2.666716328963051,"best_cost":1583.0,"extract_time":1594,"model":"../tests/models/efficientnet.relay","num_eclass":6712,"num_enodes":17899,"solver_time":1399} +{"algo":"WPMAXSAT","avg_enode_per_class":2.1747891058086286,"best_cost":1529.0,"extract_time":1531,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":20745,"num_enodes":45116,"solver_time":1003} +{"algo":"ILP-ACyc","avg_enode_per_class":2.21060496505182,"best_cost":1529.0,"extract_time":688,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":20745,"num_enodes":45859,"solver_time":244} +{"algo":"WPMAXSAT","avg_enode_per_class":2.7400606980273143,"best_cost":1658.0,"extract_time":581,"model":"../tests/models/mobilenetv2.relay","num_eclass":6590,"num_enodes":18057,"solver_time":332} +{"algo":"ILP-ACyc","avg_enode_per_class":2.7400606980273143,"best_cost":1658.0,"extract_time":289,"model":"../tests/models/mobilenetv2.relay","num_eclass":6590,"num_enodes":18057,"solver_time":77} +{"algo":"ILP-Topo","avg_enode_per_class":2.7400606980273143,"best_cost":1658.0,"extract_time":1538,"model":"../tests/models/mobilenetv2.relay","num_eclass":6590,"num_enodes":18057,"solver_time":1365} +{"algo":"WPMAXSAT","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":210,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":116} +{"algo":"ILP-ACyc","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":149,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":60} +{"algo":"ILP-Topo","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":785,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":714} +{"algo":"WPMAXSAT","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":168,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":80} +{"algo":"ILP-ACyc","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":202,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":132} +{"algo":"ILP-Topo","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":695,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":626} +{"algo":"WPMAXSAT","avg_enode_per_class":2.666716328963051,"best_cost":1583.0,"extract_time":561,"model":"../tests/models/efficientnet.relay","num_eclass":6712,"num_enodes":17899,"solver_time":293} +{"algo":"ILP-ACyc","avg_enode_per_class":2.666716328963051,"best_cost":1583.0,"extract_time":314,"model":"../tests/models/efficientnet.relay","num_eclass":6712,"num_enodes":17899,"solver_time":79} +{"algo":"ILP-Topo","avg_enode_per_class":2.666716328963051,"best_cost":1583.0,"extract_time":1584,"model":"../tests/models/efficientnet.relay","num_eclass":6712,"num_enodes":17899,"solver_time":1405} +{"algo":"WPMAXSAT","avg_enode_per_class":2.1747891058086286,"best_cost":1529.0,"extract_time":1717,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":20745,"num_enodes":45116,"solver_time":1178} +{"algo":"ILP-ACyc","avg_enode_per_class":2.1747891058086286,"best_cost":1529.0,"extract_time":737,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":20745,"num_enodes":45116,"solver_time":262} +{"algo":"WPMAXSAT","avg_enode_per_class":2.7400606980273143,"best_cost":1658.0,"extract_time":549,"model":"../tests/models/mobilenetv2.relay","num_eclass":6590,"num_enodes":18057,"solver_time":299} +{"algo":"ILP-ACyc","avg_enode_per_class":2.7400606980273143,"best_cost":1658.0,"extract_time":304,"model":"../tests/models/mobilenetv2.relay","num_eclass":6590,"num_enodes":18057,"solver_time":90} +{"algo":"ILP-Topo","avg_enode_per_class":2.7400606980273143,"best_cost":1658.0,"extract_time":1440,"model":"../tests/models/mobilenetv2.relay","num_eclass":6590,"num_enodes":18057,"solver_time":1270} +{"algo":"WPMAXSAT","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":219,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":120} +{"algo":"ILP-ACyc","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":154,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":74} +{"algo":"ILP-Topo","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":629,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":560} +{"algo":"WPMAXSAT","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":179,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":86} +{"algo":"ILP-ACyc","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":183,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":108} +{"algo":"ILP-Topo","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":727,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":661} +{"algo":"WPMAXSAT","avg_enode_per_class":2.666716328963051,"best_cost":1583.0,"extract_time":624,"model":"../tests/models/efficientnet.relay","num_eclass":6712,"num_enodes":17899,"solver_time":334} +{"algo":"ILP-ACyc","avg_enode_per_class":2.666716328963051,"best_cost":1583.0,"extract_time":323,"model":"../tests/models/efficientnet.relay","num_eclass":6712,"num_enodes":17899,"solver_time":79} +{"algo":"ILP-Topo","avg_enode_per_class":2.666716328963051,"best_cost":1583.0,"extract_time":1785,"model":"../tests/models/efficientnet.relay","num_eclass":6712,"num_enodes":17899,"solver_time":1587} +{"algo":"WPMAXSAT","avg_enode_per_class":2.1747891058086286,"best_cost":1529.0,"extract_time":1744,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":20745,"num_enodes":45116,"solver_time":1167} +{"algo":"ILP-ACyc","avg_enode_per_class":2.1747891058086286,"best_cost":1529.0,"extract_time":707,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":20745,"num_enodes":45116,"solver_time":251} +{"algo":"WPMAXSAT","avg_enode_per_class":2.7400606980273143,"best_cost":1658.0,"extract_time":578,"model":"../tests/models/mobilenetv2.relay","num_eclass":6590,"num_enodes":18057,"solver_time":323} +{"algo":"ILP-ACyc","avg_enode_per_class":2.7400606980273143,"best_cost":1658.0,"extract_time":297,"model":"../tests/models/mobilenetv2.relay","num_eclass":6590,"num_enodes":18057,"solver_time":90} +{"algo":"ILP-Topo","avg_enode_per_class":2.7400606980273143,"best_cost":1658.0,"extract_time":988,"model":"../tests/models/mobilenetv2.relay","num_eclass":6590,"num_enodes":18057,"solver_time":822} +{"algo":"WPMAXSAT","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":226,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":123} +{"algo":"ILP-ACyc","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":128,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":52} +{"algo":"ILP-Topo","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":727,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":663} +{"algo":"WPMAXSAT","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":188,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":80} +{"algo":"ILP-ACyc","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":182,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":108} +{"algo":"ILP-Topo","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":717,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":655} +{"algo":"WPMAXSAT","avg_enode_per_class":2.666716328963051,"best_cost":1583.0,"extract_time":575,"model":"../tests/models/efficientnet.relay","num_eclass":6712,"num_enodes":17899,"solver_time":305} +{"algo":"ILP-ACyc","avg_enode_per_class":2.666716328963051,"best_cost":1583.0,"extract_time":311,"model":"../tests/models/efficientnet.relay","num_eclass":6712,"num_enodes":17899,"solver_time":78} +{"algo":"ILP-Topo","avg_enode_per_class":2.666716328963051,"best_cost":1583.0,"extract_time":1728,"model":"../tests/models/efficientnet.relay","num_eclass":6712,"num_enodes":17899,"solver_time":1521} +{"algo":"WPMAXSAT","avg_enode_per_class":2.1747891058086286,"best_cost":1529.0,"extract_time":1775,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":20745,"num_enodes":45116,"solver_time":1164} +{"algo":"ILP-ACyc","avg_enode_per_class":2.1747891058086286,"best_cost":1529.0,"extract_time":703,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":20745,"num_enodes":45116,"solver_time":232} +{"algo":"WPMAXSAT","avg_enode_per_class":2.7400606980273143,"best_cost":1658.0,"extract_time":636,"model":"../tests/models/mobilenetv2.relay","num_eclass":6590,"num_enodes":18057,"solver_time":349} +{"algo":"ILP-ACyc","avg_enode_per_class":2.7400606980273143,"best_cost":1658.0,"extract_time":310,"model":"../tests/models/mobilenetv2.relay","num_eclass":6590,"num_enodes":18057,"solver_time":87} +{"algo":"ILP-Topo","avg_enode_per_class":2.7400606980273143,"best_cost":1658.0,"extract_time":1129,"model":"../tests/models/mobilenetv2.relay","num_eclass":6590,"num_enodes":18057,"solver_time":959} +{"algo":"WPMAXSAT","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":211,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":112} +{"algo":"ILP-ACyc","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":132,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":54} +{"algo":"ILP-Topo","avg_enode_per_class":3.021074380165289,"best_cost":625.0,"extract_time":822,"model":"../tests/models/resmlp.relay","num_eclass":2420,"num_enodes":7311,"solver_time":758} +{"algo":"WPMAXSAT","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":185,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":87} +{"algo":"ILP-ACyc","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":163,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":86} +{"algo":"ILP-Topo","avg_enode_per_class":2.7346938775510203,"best_cost":602.0,"extract_time":710,"model":"../tests/models/resnet18.relay","num_eclass":2695,"num_enodes":7370,"solver_time":646} +{"algo":"WPMAXSAT","avg_enode_per_class":2.666716328963051,"best_cost":1583.0,"extract_time":602,"model":"../tests/models/efficientnet.relay","num_eclass":6712,"num_enodes":17899,"solver_time":319} +{"algo":"ILP-ACyc","avg_enode_per_class":2.666716328963051,"best_cost":1583.0,"extract_time":340,"model":"../tests/models/efficientnet.relay","num_eclass":6712,"num_enodes":17899,"solver_time":85} +{"algo":"ILP-Topo","avg_enode_per_class":2.666716328963051,"best_cost":1583.0,"extract_time":1764,"model":"../tests/models/efficientnet.relay","num_eclass":6712,"num_enodes":17899,"solver_time":1560} +{"algo":"WPMAXSAT","avg_enode_per_class":2.1747891058086286,"best_cost":1529.0,"extract_time":1638,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":20745,"num_enodes":45116,"solver_time":1100} +{"algo":"ILP-ACyc","avg_enode_per_class":2.21060496505182,"best_cost":1529.0,"extract_time":688,"model":"../tests/models/resnet50_simplifyinference_from_pytorch.relay","num_eclass":20745,"num_enodes":45859,"solver_time":235}