From b1e9f5a9ec0a295becdbb27653499cab53cda2d9 Mon Sep 17 00:00:00 2001 From: AurumTheEnd <47597303+aurumtheend@users.noreply.github.com> Date: Fri, 10 May 2024 22:00:14 +0200 Subject: [PATCH] feat(bdd): implemented substitute --- src/bdd/traits/boolean_function.rs | 20 ++++++++++++++++++-- 1 file changed, 18 insertions(+), 2 deletions(-) diff --git a/src/bdd/traits/boolean_function.rs b/src/bdd/traits/boolean_function.rs index aab1b41..f1ec8cf 100644 --- a/src/bdd/traits/boolean_function.rs +++ b/src/bdd/traits/boolean_function.rs @@ -74,13 +74,29 @@ impl BooleanFunction for Bdd { self.restrict_and_prune_map(valuation, &new_bdd) } - fn substitute(&self, _mapping: &BTreeMap) -> Self { + fn substitute(&self, mapping: &BTreeMap) -> Self { // Bdd.substitute exists, but assumes all BDDs share input variables (we need to extend) // and does not eliminate the substituted variable from inputs afterward (we need to prune). // Bdd.substitute currently assumes that the substituted functions does not depend on the // substituted variables. This will be solved in lib-bdd, we can just panic for now. - todo!() + if mapping + .iter() + .any(|(key, value_bdd)| value_bdd.inputs.contains(key)) + { + panic!("Currently not allowed to have the substituted variable also appear in the substituting BDD value"); + } + + let mut extended_mapping = mapping.clone(); + let (mut self_lifted, _common_inputs) = self.union_and_extend_n_ary(&mut extended_mapping); + + for (k, v) in extended_mapping.iter() { + self_lifted.bdd = self_lifted + .bdd + .substitute(self_lifted.map_var_outer_to_inner(k).unwrap(), &v.bdd) + } + + self_lifted.restrict_and_prune_map(&extended_mapping, &self_lifted) } fn sat_point(&self) -> Option {