From f2e162b57176fe7e07df9b58135bd181151ba12d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Mon, 9 Dec 2024 14:32:17 -0500 Subject: [PATCH] fix bdd summarize (formula is very very big :( ) --- tools/egraphs-cond-synth/src/summarize.rs | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/tools/egraphs-cond-synth/src/summarize.rs b/tools/egraphs-cond-synth/src/summarize.rs index b85df95..ab8dfe5 100644 --- a/tools/egraphs-cond-synth/src/summarize.rs +++ b/tools/egraphs-cond-synth/src/summarize.rs @@ -11,11 +11,11 @@ use rustc_hash::FxHashMap; pub fn bdd_summarize(rule: &RuleInfo, samples: &Samples) -> String { // generate all labels and the corresponding BDD terminals let labels = get_labels(rule); - let mut bdd = boolean_expression::BDD::::new(); - let vars: Vec<_> = (0..labels.len()).map(|ii| bdd.terminal(ii)).collect(); + let mut bdd = boolean_expression::BDD::::new(); + let vars: Vec<_> = labels.iter().map(|ii| bdd.terminal(ii.clone())).collect(); - // start condition as trivially `true` - let mut cond = boolean_expression::BDD_ONE; + // start condition as trivially `false` + let mut cond = boolean_expression::BDD_ZERO; for (assignment, is_equal) in samples.iter() { let v = FxHashMap::from_iter(assignment); let mut outputs = vec![]; @@ -36,7 +36,7 @@ pub fn bdd_summarize(rule: &RuleInfo, samples: &Samples) -> String { let term = lits.into_iter().reduce(|a, b| bdd.and(a, b)).unwrap(); let term = if is_equal { term } else { bdd.not(term) }; - cond = bdd.and(cond, term); + cond = bdd.or(cond, term); } // extract simplified expression