Fixed bug that caused repeated visiting of the same expression
@@ -120,6 +120,8 @@ fn subsumption_filter(
ids.push(eg.add_expr(&instantiate(&eq.rhs)));
}
+ // println!("NUM NODES: {} {}", eg.number_of_classes(), eg.total_size());
+
// For each expression, what does it subsume?
let mut subsume : HashMap<Id, Vec<Id>> = HashMap::default();
let id_pairs : Vec<(Id, Id)> = ids.chunks(2).map(|chunk|
@@ -130,15 +132,39 @@ fn subsumption_filter(
}
).collect();
+ println!("ID_PAIRS: {:?}", id_pairs);
+
+ // println!("PRINTING EXPRESSIONS:");
+ // let mut extract = Extractor::new(&eg, AstSize);
+ // for ec in eg.classes() {
+ // let (_, expr) = extract.find_best(ec.id);
+ // println!("{}", expr);
+ // }
+
let ids_and_eqs = equalities.iter().zip(id_pairs.clone());
+ let mut visited_ids : HashSet<Id> = HashSet::default();
for (eq, (lhs_id, rhs_id)) in ids_and_eqs {
+ if !visited_ids.contains(&lhs_id) {
+ println!("SUB ITER: {} {}", lhs_id, eq.lhs);
+ println!("SUB SEARCH LEN: {}", eq.lhs.search(&eg).len());
for mat in eq.lhs.search(&eg) {
+ // println!("hello {} {}", lhs_id, mat.eclass);
subsume.entry(lhs_id).or_default().push(mat.eclass);
}
+ visited_ids.insert(lhs_id);
+ }
+ if !visited_ids.contains(&rhs_id) {
+ println!("SUB ITER: {} {}", rhs_id, eq.rhs);
+ println!("SUB SEARCH LEN: {}", eq.rhs.search(&eg).len());
for mat in eq.rhs.search(&eg) {
+ // println!("hello {} {}", rhs_id, mat.eclass);
subsume.entry(rhs_id).or_default().push(mat.eclass);
}
+ visited_ids.insert(rhs_id);
+ }
}
+ println!("EQS LEN: {}", id_pairs.len());
+ println!("SUB LEN: {}", subsume.len());
let mut lhs_to_rhs : HashMap<Id, Id> = HashMap::default();
for eq_ids in ids.chunks(2) {
@@ -155,6 +181,10 @@ fn subsumption_filter(
continue;
}
+ // TODO: This is a contravariant check
+ // lhs = rhs
+ // -> sub1 = sub_rhs
+ // <- rhs
let subvec = subsume.get(&lhs_id);
if subvec.is_some() {
for sub_id in subvec.unwrap() {
@@ -179,6 +209,7 @@ fn subsumption_filter(
}
}
+ println!("NUM REMOVED: {}", removed_eqs.len());
removed_eqs
}
