diff --git a/examples/bench_restrict.rs b/examples/bench_restrict.rs new file mode 100644 index 0000000..518edba --- /dev/null +++ b/examples/bench_restrict.rs @@ -0,0 +1,36 @@ +use biodivine_lib_bdd::{Bdd, BddPartialValuation}; +use rand::prelude::{SliceRandom, StdRng}; +use rand::{Rng, SeedableRng}; +use std::time::Instant; + +fn main() { + let args = std::env::args().collect::>(); + let mut file = std::fs::File::open(args[1].as_str()).unwrap(); + let bdd = Bdd::read_as_bytes(&mut file).unwrap(); + println!("Loaded: {} as Bdd({})", args[1].as_str(), bdd.size()); + + let mut support = Vec::from_iter(bdd.support_set()); + + for k in 1..5 { + // Fix variables randomly. + let mut reduction = BddPartialValuation::empty(); + let mut rng = StdRng::seed_from_u64(0); + support.sort(); // Don't leak previous shuffled state. + support.shuffle(&mut rng); + + for var in &support[0..k] { + reduction[*var] = Some(rng.gen_bool(0.5)); + } + + // Run restriction. + for _ in 0..5 { + let start = Instant::now(); + let result = bdd.restrict(&reduction.to_values()); + println!( + "Result: Bdd({}) in {}ms", + result.size(), + (Instant::now() - start).as_millis() + ); + } + } +} diff --git a/src/_impl_bdd/_impl_relation_ops.rs b/src/_impl_bdd/_impl_relation_ops.rs index d7443ad..052a4fa 100644 --- a/src/_impl_bdd/_impl_relation_ops.rs +++ b/src/_impl_bdd/_impl_relation_ops.rs @@ -1,5 +1,7 @@ -use crate::{Bdd, BddPartialValuation, BddVariable}; +use crate::{Bdd, BddNode, BddPartialValuation, BddPointer, BddVariable}; +use fxhash::FxBuildHasher; use rand::Rng; +use std::collections::HashMap; /// Advanced relation-like operations for `Bdd`s. impl Bdd { @@ -155,19 +157,14 @@ impl Bdd { /// A valuation `v` satisfies the resulting formula `B_2` if and only if `v[variable = value]` /// satisfied the original formula `B_1`. pub fn var_restrict(&self, variable: BddVariable, value: bool) -> Bdd { - let value_literal = Bdd::mk_literal(self.num_vars(), variable, value); - // TODO: - // We should test if this is actually faster than running self.var_select().exists(). - Bdd::binary_op_with_exists(self, &value_literal, crate::op_function::and, &[variable]) + self.restrict(&[(variable, value)]) } /// Generalized operation to `var_restrict`. Allows fixing multiple Bdd variables and /// eliminating them at the same time. pub fn restrict(&self, variables: &[(BddVariable, bool)]) -> Bdd { let valuation = BddPartialValuation::from_values(variables); - let valuation_bdd = Bdd::mk_partial_valuation(self.num_vars(), &valuation); - let variables: Vec = Vec::from_iter(variables.iter().map(|(x, _)| *x)); - Bdd::binary_op_with_exists(self, &valuation_bdd, crate::op_function::and, &variables) + restriction(self, &valuation) } } @@ -177,3 +174,92 @@ fn sorted(variables: &[BddVariable]) -> Vec { variables.sort(); variables } + +// An internal function to perform a fast restriction operation. This relies on the fact +// that subtrees of the eliminated variables do not have to be merged (like in a normal +// existential projection), but a single subtree is kept instead. +fn restriction(bdd: &Bdd, values: &BddPartialValuation) -> Bdd { + if bdd.is_true() || bdd.is_false() { + return bdd.clone(); + } + + let mut new_id: Vec> = vec![None; bdd.size()]; + new_id[0] = Some(BddPointer::zero()); + new_id[1] = Some(BddPointer::one()); + + let mut output = Bdd::mk_true(bdd.num_vars()); + + let mut node_cache: HashMap = + HashMap::with_capacity_and_hasher(bdd.size(), FxBuildHasher::default()); + node_cache.insert(BddNode::mk_zero(bdd.num_vars()), BddPointer::zero()); + node_cache.insert(BddNode::mk_one(bdd.num_vars()), BddPointer::one()); + + let mut stack = vec![bdd.root_pointer()]; + while let Some(top) = stack.pop() { + if new_id[top.to_index()].is_some() { + // Skip if already computed. + continue; + } + + let top_var = bdd.var_of(top); + if let Some(value) = values[top_var] { + // The variable is restricted, hence only the relevant child is considered. + let link = if value { + bdd.high_link_of(top) + } else { + bdd.low_link_of(top) + }; + + let Some(new_link) = new_id[link.to_index()] else { + stack.push(top); + stack.push(link); + continue; + }; + + // Here, we do not have to create a node, because the variable is erased immediately. + new_id[top.to_index()] = Some(new_link); + } else { + // This variable is unrestricted. We just compute results for both children + // if they are unknown. Otherwise, we copy the node into the new BDD. + let low_link = bdd.low_link_of(top); + let high_link = bdd.high_link_of(top); + + let Some(new_low_link) = new_id[low_link.to_index()] else { + stack.push(top); + stack.push(low_link); + continue; + }; + + let Some(new_high_link) = new_id[high_link.to_index()] else { + stack.push(top); + stack.push(high_link); + continue; + }; + + if new_high_link == new_low_link { + // If a redundant node is created, it is ignored. + new_id[top.to_index()] = Some(new_high_link); + continue; + } + + let new_node = BddNode::mk_node(top_var, new_low_link, new_high_link); + + if let Some(&node) = node_cache.get(&new_node) { + new_id[top.to_index()] = Some(node); + } else { + let node = BddPointer::from_index(output.size()); + output.push_node(new_node); + node_cache.insert(new_node, node); + new_id[top.to_index()] = Some(node); + } + } + } + + let new_root = new_id[bdd.root_pointer().to_index()].unwrap(); + if new_root.is_zero() { + // This could happen if we do, for example, restrict(var, True) in a function `!var`. + return Bdd::mk_false(bdd.num_vars()); + } + + output +}