Struct biodivine_lib_bdd::Bdd

pub struct Bdd(/* private fields */);

An array-based encoding of the binary decision diagram implementing basic logical operations.

To create Bdds for atomic formulas, use a BddVariableSet.

Implementations

impl Bdd

Basic boolean logical operations for Bdds: $\neg, \land, \lor, \Rightarrow, \Leftrightarrow, \oplus$.

pub fn not(&self) -> Bdd

Create a Bdd corresponding to the $\neg \phi$ formula, where $\phi$ is this Bdd.

pub fn and(&self, right: &Bdd) -> Bdd

Create a Bdd corresponding to the $\phi \land \psi$ formula, where $\phi$ and $\psi$ are the two given Bdds.

pub fn or(&self, right: &Bdd) -> Bdd

Create a Bdd corresponding to the $\phi \lor \psi$ formula, where $\phi$ and $\psi$ are the two given Bdds.

pub fn imp(&self, right: &Bdd) -> Bdd

Create a Bdd corresponding to the $\phi \Rightarrow \psi$ formula, where $\phi$ and $\psi$ are the two given Bdds.

pub fn iff(&self, right: &Bdd) -> Bdd

Create a Bdd corresponding to the $\phi \Leftrightarrow \psi$ formula, where $\phi$ and $\psi$ are the two given Bdds.

pub fn xor(&self, right: &Bdd) -> Bdd

Create a Bdd corresponding to the $\phi \oplus \psi$ formula, where $\phi$ and $\psi$ are the two given Bdds.

pub fn and_not(&self, right: &Bdd) -> Bdd

Create a Bdd corresponding to the $\phi \land \neg \psi$ formula, where $\phi$ and $\psi$ are the two given Bdds.

pub fn if_then_else(a: &Bdd, b: &Bdd, c: &Bdd) -> Bdd

A standard “if-then-else” ternary operation. It is equivalent to $(a \land b) \lor (\neg a \land c)$.

Additional non-standard ternary operators are available through Bdd::ternary_op.

pub fn binary_op<T>(left: &Bdd, right: &Bdd, op_function: T) -> Bdd

where T: Fn(Option<bool>, Option<bool>) -> Option<bool>,

Apply a general binary operation to two given Bdd objects.

The op_function specifies the actual logical operation that will be performed. See crate::op_function module for examples.

In general, this function can be used to slightly speed up less common Boolean operations or to fuse together several operations (like negation and binary operation).

pub fn binary_op_with_limit<T>( limit: usize, left: &Bdd, right: &Bdd, op_function: T ) -> Option<Bdd>

where T: Fn(Option<bool>, Option<bool>) -> Option<bool>,

Same as binary_op, but the result of the operation is None if the size of the Bdd exceeds the given limit.

pub fn fused_binary_flip_op<T>( left: (&Bdd, Option<BddVariable>), right: (&Bdd, Option<BddVariable>), flip_output: Option<BddVariable>, op_function: T ) -> Bdd

where T: Fn(Option<bool>, Option<bool>) -> Option<bool>,

Apply a general binary operation together with up-to three Bdd variable flips. See also binary_op.

A flip exchanges the edges of all decision nodes with the specified variable x. As a result, the set of bitvectors represented by this Bdd has the value of x negated.

With this operation, you can apply such flip to both input operands and the output Bdd. This can greatly simplify implementation of state space generators for asynchronous systems.

pub fn fused_binary_flip_op_with_limit<T>( limit: usize, left: (&Bdd, Option<BddVariable>), right: (&Bdd, Option<BddVariable>), flip_output: Option<BddVariable>, op_function: T ) -> Option<Bdd>

where T: Fn(Option<bool>, Option<bool>) -> Option<bool>,

Same as Self::fused_binary_flip_op, but the result of the operation is None if the size of the Bdd exceeds the given limit.

pub fn check_binary_op<T>( limit: usize, left: &Bdd, right: &Bdd, op_function: T ) -> Option<(bool, usize)>

where T: Fn(Option<bool>, Option<bool>) -> Option<bool>,

Performs a “dry run” of the supplied operation. This computes two useful results:

1. A true value indicating that the resulting BDD will not be “empty” (i.e. not a contradiction).

2. A number of low-level BDD tasks that need to be completed to resolve the operation.

You can also limit the enumeration up to a specific number of tasks using the limit parameter. If this limit is exceeded, the result is None. Note that this limit parameter does not correspond to the number of nodes in the (hypothetical) resulting Bdd, but rather the number of steps needed to create it.

Generally, the method requires much less space and time than binary_op, but does not produce the actual BDD. As such, it is useful for operations where the result would be likely discarded anyway, like subset checks or size comparisons.

Nevertheless, note that the number of low-level task is not the size of the resulting BDD (it is an upper bound on its size though).

pub fn check_fused_binary_flip_op<T>( limit: usize, left: (&Bdd, Option<BddVariable>), right: (&Bdd, Option<BddVariable>), flip_output: Option<BddVariable>, op_function: T ) -> Option<(bool, usize)>

where T: Fn(Option<bool>, Option<bool>) -> Option<bool>,

The same as Bdd::check_binary_op, but it takes into account variable flips.

impl Bdd

pub fn ternary_op<T>(a: &Bdd, b: &Bdd, c: &Bdd, op_function: T) -> Bdd

where T: Fn(Option<bool>, Option<bool>, Option<bool>) -> Option<bool>,

A ternary logical operation on three Bdd objects. Works the same as Bdd::binary_op, but with three arguments.

Note that this may not necessarily be faster than performing two (or more) binary operations. However, in some cases it can significantly reduce overhead incurred by creating large intermediate decision diagrams.

pub fn fused_ternary_flip_op<T>( a: (&Bdd, Option<BddVariable>), b: (&Bdd, Option<BddVariable>), c: (&Bdd, Option<BddVariable>), flip_output: Option<BddVariable>, op_function: T ) -> Bdd

where T: Fn(Option<bool>, Option<bool>, Option<bool>) -> Option<bool>,

A ternary version of Bdd::fused_binary_flip_op that makes it possible to flip the meaning of a single variable the input and output diagrams.

Note that this may not necessarily be faster than performing two (or more) binary operations. However, in some cases it can significantly reduce overhead incurred by creating large intermediate decision diagrams.

impl Bdd

pub fn binary_op_with_for_all<F>( left: &Bdd, right: &Bdd, op: F, variables: &[BddVariable] ) -> Bdd

where F: Fn(Option<bool>, Option<bool>) -> Option<bool>,

Performs a logical operation (op) on two BDDs while performing a universal projection on the given variables in the result BDD.

pub fn binary_op_with_exists<F>( left: &Bdd, right: &Bdd, op: F, variables: &[BddVariable] ) -> Bdd

where F: Fn(Option<bool>, Option<bool>) -> Option<bool>,

Performs a logical operation (op) on two BDDs while performing an existential projection on the given variables in the result BDD.

pub fn binary_op_nested<F1, F2, Trigger>( left: &Bdd, right: &Bdd, trigger: Trigger, outer_op: F1, inner_op: F2 ) -> Bdd

where F1: Fn(Option<bool>, Option<bool>) -> Option<bool>, F2: Fn(Option<bool>, Option<bool>) -> Option<bool>, Trigger: Fn(BddVariable) -> bool,

A “nested” apply function performs two “nested” passes of the apply algorithm:

• First, the outer_op is applied to combine the left and right BDDs.
• Then, for each node of the newly created BDD, the trigger function is executed and if it returns true, the inner_op is applied to the two children of this node and the result replaces the original node in the final BDD.

This operation can be used to implement various combinations of logic + projection. Specifically, using inner_op = or implements existential projection and inner_op = and implements universal projection on the result of the “outer” operation. However, much “wilder” combinations are possible if you need them.

impl Bdd

Advanced relation-like operations for Bdds.

pub fn var_project(&self, variable: BddVariable) -> Bdd

👎Deprecated

This operation is deprecated in favour of Bdd::var_exists which provides the same functionality but better naming.

pub fn var_exists(&self, variable: BddVariable) -> Bdd

Eliminates one given variable from the Bdd using existential projection.

If we see the Bdd as a set of bitvectors, this is essentially existential quantification: $\exists x_i : (x_1, …, x_i, …, x_n) \in BDD$.

pub fn var_for_all(&self, variable: BddVariable) -> Bdd

Eliminates one given variable from the Bdd using universal projection.

If we see the Bdd as a set of bitvectors, this is essentially universal quantification: $\forall x_i : (x_1, …, x_i, …, x_n) \in BDD$.

pub fn project(&self, variables: &[BddVariable]) -> Bdd

👎Deprecated

This method is deprecated in favour of Bdd::exists which provides the same functionality but better naming.

pub fn exists(&self, variables: &[BddVariable]) -> Bdd

Eliminate all given variables from the Bdd using existential projection.

This can be used to implement operations like domain and range for a specific relation.

Note that this method should be faster than repeated calls to var_exists once the size of variables is non-trivial, but it has a higher overhead. So for very small instances the performance advantage may not be very high.

pub fn for_all(&self, variables: &[BddVariable]) -> Bdd

Eliminate all given variables from the Bdd using universal projection.

Same performance characteristics as Bdd::exists.

pub fn var_pick(&self, variable: BddVariable) -> Bdd

Picks one valuation for the given BddVariable.

Essentially, what this means is that $(x_1, …, x_i, …, x_n) \in B \Leftrightarrow (x_1, …, \neg x_i, …, x_n) \not\in B$. That is, each valuation (without $x_i$) can be present only with either $x_i = 1$ or $x_i = 0$, but not both.

WARNING! var_pick is a bit troublesome in terms of composition: B.var_pick(x).var_pick(y) is probably not what you think. So make sure to prove and test thoroughly.

pub fn var_pick_random<R: Rng>(&self, variable: BddVariable, rng: &mut R) -> Bdd

Same as bdd.var_pick, but the preferred value is picked randomly using the provided generator, instead of defaulting to false.

Note that this is not the same as having a random value picked on each path in the Bdd. Instead, there is one “global” value that is preferred on every path.

pub fn pick(&self, variables: &[BddVariable]) -> Bdd

Picks one “witness” valuation for the given variables. This is a generalized variant of var_pick.

After this operation, if we view Bdd as a set of bitvectors, every partial valuation in the original Bdd, disregarding the given variables, has exactly one witness valuation in the result, which was also in the original Bdd.

This can be used to implement non-trivial element picking on relations (for example, for $A \times B$, picking one $b \in B$ for every $a \in A$).

pub fn pick_random<R: Rng>(&self, variables: &[BddVariable], rng: &mut R) -> Bdd

Same as bdd.pick, but the preferred value for each variable is picked randomly using the provided generator.

pub fn var_select(&self, variable: BddVariable, value: bool) -> Bdd

Fix the value of a specific BddVariable to the given value. This is just a shorthand for $B \land (x \Leftrightarrow \texttt{value})$.

pub fn select(&self, variables: &[(BddVariable, bool)]) -> Bdd

Generalized operation to var_select, allows effectively fixing multiple variables to the given values. Similar to BddValuation.into::<Bdd>(), but here you don’t have to specify all variables.

pub fn var_restrict(&self, variable: BddVariable, value: bool) -> Bdd

Fixes a variable to the given value, and then eliminates said variable using existential projection.

A valuation v satisfies the resulting formula B_2 if and only if v[variable = value] satisfied the original formula B_1.

pub fn restrict(&self, variables: &[(BddVariable, bool)]) -> Bdd

Generalized operation to var_restrict. Allows fixing multiple Bdd variables and eliminating them at the same time.

Examples found in repository

examples/bench_restrict.rs (line 28)

fn main() {
    let args = std::env::args().collect::<Vec<_>>();
    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()
            );
        }
    }
}

impl Bdd

.dot export procedure for Bdds.

pub fn write_as_dot_string( &self, output: &mut dyn Write, variables: &BddVariableSet, zero_pruned: bool ) -> Result<(), Error>

Output this Bdd as a .dot string into the given output writer.

Variable names in the graph are resolved from the given BddVariableSet.

If zero_pruned is true, edges leading to zero are not shown. This can greatly simplify the graph without losing information.

pub fn to_dot_string( &self, variables: &BddVariableSet, zero_pruned: bool ) -> String

Convert this Bdd to a .dot string.

Variable names in the graph are resolved from the given BddVariableSet.

If zero_pruned is true, edges leading to zero are not shown. This can greatly simplify the graph without losing information.

impl Bdd

Serialisation and deserialization methods for Bdds.

pub fn write_as_string(&self, output: &mut dyn Write) -> Result<(), Error>

Write this Bdd into the given output writer using a simple string format.

pub fn read_as_string(input: &mut dyn Read) -> Result<Bdd, String>

Read a Bdd from the given input reader, assuming a simple string format.

pub fn write_as_bytes(&self, output: &mut dyn Write) -> Result<(), Error>

Write this Bdd into the given output writer using a simple little-endian binary encoding.

pub fn read_as_bytes(input: &mut dyn Read) -> Result<Bdd, Error>

Read a Bdd from a given input reader using a simple little-endian binary encoding.

Examples found in repository

examples/bench_restrict.rs (line 9)

fn main() {
    let args = std::env::args().collect::<Vec<_>>();
    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()
            );
        }
    }
}

pub fn from_string(bdd: &str) -> Bdd

Read a Bdd from a serialized string.

pub fn to_bytes(&self) -> Vec<u8>

Convert this Bdd to a byte vector.

pub fn from_bytes(data: &mut &[u8]) -> Bdd

Read a Bdd from a byte vector.

impl Bdd

Several useful (mostly internal) low-level utility methods for Bdds.

pub fn size(&self) -> usize

The number of nodes in this Bdd. (Do not confuse with cardinality)

Examples found in repository

examples/bench_restrict.rs (line 10)

fn main() {
    let args = std::env::args().collect::<Vec<_>>();
    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()
            );
        }
    }
}

pub fn num_vars(&self) -> u16

Number of variables in the corresponding BddVariableSet.

pub unsafe fn set_num_vars(&mut self, new_value: u16)

Change the number of variables tracked by this BDD.

Safety

This operation is “unsafe”, as it makes the BDD incompatible with the original BddVariableSet and overall can break compatibility of BDD operations. However, the operation will not allow you to create an invalid BDD. We still check that the new_value covers at least the highest used variable in the BDD, and if the property is broken, the operation panics.

pub unsafe fn rename_variables( &mut self, permutation: &HashMap<BddVariable, BddVariable> )

The same as Bdd::rename_variable, but applies the renaming across several variables. Each node is renamed at most one (i.e. if v1 renames to v2 and v2 renames to v3, a decision node based on v1 only renames to v2).

Safety

This operation is “unsafe” because it can change the BDD in a “non-semantic” way. However, as long as the operation does not panic, the result will be a valid BDD.

pub unsafe fn rename_variable( &mut self, old_id: BddVariable, new_id: BddVariable )

Change the provided variable ID to the new one. This change does not perform any structural changes to the BDD itself. As such, it is only valid when the BDD does not depend on any variables that are between old_id and new_id. Furthermore, old_id and new_id must be admissible in this BDD. The method panics otherwise.

Safety

This operation is “unsafe” because it can change the BDD in a “non-semantic” way. However, as long as the operation does not panic, the result will be a valid BDD.

pub fn is_true(&self) -> bool

True if this Bdd is exactly the true formula.

pub fn is_false(&self) -> bool

True if this Bdd is exactly the false formula.

pub fn exact_cardinality(&self) -> BigInt

pub fn cardinality(&self) -> f64

Approximately computes the number of valuations satisfying the formula given by this Bdd.

pub fn exact_clause_cardinality(&self) -> BigInt

Computes the number of satisfying clauses that are represented within this BDD.

The result should correspond to the number of items returned by the Bdd::sat_clauses iterator.

pub fn sat_witness(&self) -> Option<BddValuation>

If the Bdd is satisfiable, return some BddValuation that satisfies the Bdd.

pub fn to_boolean_expression( &self, variables: &BddVariableSet ) -> BooleanExpression

Convert this Bdd to a BooleanExpression (using the variable names from the given BddVariableSet).

pub fn root_pointer(&self) -> BddPointer

Pointer to the root of the decision diagram.

pub fn low_link_of(&self, node: BddPointer) -> BddPointer

Get the low link of the node at a specified location.

pub fn high_link_of(&self, node: BddPointer) -> BddPointer

Get the high link of the node at a specified location.

pub fn var_of(&self, node: BddPointer) -> BddVariable

Get the conditioning variable of the node at a specified location.

Note that this also technically works for terminals, but the returned BddVariable is not valid in this Bdd.

pub fn is_valuation(&self) -> bool

Check if this Bdd represents a single valuation with all variables fixed to a specific value.

This can be used for example to verify that a set represented by a Bdd is a singleton.

pub fn is_clause(&self) -> bool

Check if this Bdd represents a single conjunctive clause, i.e. that the formula represented by this Bdd is for example x & !y & z & ... (here x, !y, z are some positive/negative literals).

pub fn size_per_variable(&self) -> HashMap<BddVariable, usize>

Compute the number of BDD nodes that condition on individual variables. If the variable does not appear in the BDD, it will not be contained in the result (i.e. keys of the returned map are the support set of the BDD).

pub fn support_set(&self) -> HashSet<BddVariable>

Return the set of all variables that actually appear as decision variables in this BDD.

Examples found in repository

examples/bench_restrict.rs (line 12)

fn main() {
    let args = std::env::args().collect::<Vec<_>>();
    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()
            );
        }
    }
}

pub fn substitute(&self, var: BddVariable, function: &Bdd) -> Bdd

Return the BDD which represents a function where variable var was substituted for function (represented as a BDD).

This should be equivalent to the expression exists var. (function <=> var) and self (assuming var does not appear in function).

If var does appear in function, it is as if var in function and var in the rest of the expression are different variables (which intuitively corresponds to how syntactic substitution on expressions typically operates).

Note that if you want to substitute multiple variables at the same time, there is currently no method that can do that with the “syntactic substitution” semantics when the variable names clash. However, if you need it, it should be possible to implement it later on (please create an issue for this).

Also note that because a proxy variable is necessary when var appears in function, this operation will panic if the number of variables is u16::MAX, as no the proxy variable cannot be created.

pub fn to_nodes(self) -> Vec<BddNode>

Consume this Bdd and return a vector of BDD nodes that it represents.

pub fn from_nodes(data: &[BddNode]) -> Result<Bdd, String>

Create a Bdd from a “raw” list of nodes.

The function does not require the input to be minimal/canonical, but the graph must be a BDD: I.e. the terminal nodes must be correct, each non-terminal node must reference existing nodes in the vector, and the edges must follow the variable ordering.

impl Bdd

Utilities for extracting interesting valuations and paths from a Bdd.

pub fn first_valuation(&self) -> Option<BddValuation>

Return the lexicographically first satisfying valuation of this Bdd.

(In this context, lexicographically means 0 < 1, with the greatest variable id being the most significant).

pub fn last_valuation(&self) -> Option<BddValuation>

Return the lexicographically last satisfying valuation of this Bdd.

(In this context, lexicographically means 0 < 1, with the greatest variable id being the most significant).

pub fn first_clause(&self) -> Option<BddPartialValuation>

Return the lexicographically fist path in this Bdd, represented as a conjunctive clause.

pub fn last_clause(&self) -> Option<BddPartialValuation>

Return the lexicographically last path in this Bdd, represented as a conjunctive clause.

pub fn most_positive_valuation(&self) -> Option<BddValuation>

Return a valuation in this Bdd that contains the greatest amount of positive literals.

If such valuation is not unique, the method should return the one that is first lexicographically.

pub fn most_negative_valuation(&self) -> Option<BddValuation>

Return a valuation in this Bdd that contains the greatest amount of negative literals.

If such valuation is not unique, the method should return the one that is first lexicographically.

pub fn most_fixed_clause(&self) -> Option<BddPartialValuation>

Compute the path in this Bdd that has the highest amount of fixed variables.

If there are multiple such paths, try to order them lexicographically.

pub fn most_free_clause(&self) -> Option<BddPartialValuation>

Compute the path in this Bdd that has the highest amount of free variables.

If there are multiple such paths, try to order them lexicographically.

pub fn random_valuation<R: Rng>(&self, rng: &mut R) -> Option<BddValuation>

Pick a random valuation that satisfies this Bdd, using a provided random number generator.

Note that the random distribution with which the valuations are picked depends on the structure of the Bdd and is not necessarily uniform.

pub fn random_clause<R: Rng>(&self, rng: &mut R) -> Option<BddPartialValuation>

Pick a random path that appears in this Bdd, using a provided random number generator.

Note that the distribution with which the path is picked depends on the structure of the Bdd and is not necessarily uniform.

pub fn necessary_clause(&self) -> Option<BddPartialValuation>

Compute the most restrictive conjunctive clause that covers all satisfying values in this BDD. In other words, if you compute the BDD corresponding to the resulting partial valuation, the new BDD will be a superset of this BDD, and it will be the smallest superset that can be described using a single clause.

impl Bdd

pub fn to_dnf(&self) -> Vec<BddPartialValuation>

Construct a DNF representation of this BDD. This is equivalent to collecting all results of the Bdd::sat_clauses iterator. However, it uses a different algorithm that should be slightly faster for enumerating all results at the same time (the sat_clauses iterator is optimized for visiting the results one-by-one).

pub fn to_optimized_dnf(&self) -> Vec<BddPartialValuation>

Similar to Bdd::to_dnf, but uses a quadratic optimization algorithm to greedily minimize the number of clauses in the final normal form.

For very large BDDs, this can require a lot of computation time. However, in such cases, Bdd::to_dnf is likely not going to yield good results either.

Currently, there is no “iterator” variant of this algorithm that would generate the DNF on-the-fly. But it should be relatively straightforward, so if you need it, please get in touch.

pub fn _to_optimized_dnf<E, I: Fn() -> Result<(), E>>( &self, interrupt: &I ) -> Result<Vec<BddPartialValuation>, E>

A cancellable variant of Bdd::to_optimized_dnf.

impl Bdd

pub fn to_cnf(&self) -> Vec<BddPartialValuation>

Construct a CNF representation of this BDD.

impl Bdd

Methods for working with Bdd valuations.

pub fn eval_in(&self, valuation: &BddValuation) -> bool

Evaluate this Bdd in a specified BddValuation.

impl Bdd

pub fn sat_valuations(&self) -> BddSatisfyingValuations<'_>

Create an iterator that goes through all the satisfying valuations of this Bdd.

Note that the number of such valuations can be substantial and can be approximated using Bdd.cardinality.

pub fn into_sat_valuations(self) -> OwnedBddSatisfyingValuations

Same as Bdd::sat_valuations, but the iterator takes ownership of the Bdd.

You can convert the iterator back into the underlying Bdd at any time using Bdd::from.

pub fn sat_clauses(&self) -> BddPathIterator<'_>

Create an iterator that goes through all paths of this Bdd. Each path is represented as a conjunctive clause in the form of BddPartialValuation.

The whole formula represented by a Bdd can be then seen as a disjunction of these clauses/paths.

pub fn into_sat_clauses(self) -> OwnedBddPathIterator

Same as Bdd::sat_clauses, but the iterator takes ownership of the Bdd.

You can convert the iterator back into the underlying Bdd at any time using Bdd::from.

Trait Implementations

impl Clone for Bdd

fn clone(&self) -> Bdd

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Bdd

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Display for Bdd

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl From<Bdd> for OwnedBddPathIterator

fn from(value: Bdd) -> Self

Converts to this type from the input type.

impl From<Bdd> for OwnedBddSatisfyingValuations

fn from(value: Bdd) -> Self

Converts to this type from the input type.

impl From<BddValuation> for Bdd

Convert a BddValuation to a Bdd with, well, exactly that one valuation.

fn from(valuation: BddValuation) -> Self

Converts to this type from the input type.

impl From<OwnedBddPathIterator> for Bdd

fn from(value: OwnedBddPathIterator) -> Self

Converts to this type from the input type.

impl From<OwnedBddSatisfyingValuations> for Bdd

fn from(value: OwnedBddSatisfyingValuations) -> Self

Converts to this type from the input type.

impl Hash for Bdd

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl IntoBdd for &Bdd

fn into_bdd(self, _variables: &BddVariableSet) -> Bdd

impl IntoBdd for Bdd

fn into_bdd(self, _variables: &BddVariableSet) -> Bdd

impl PartialEq for Bdd

fn eq(&self, other: &Bdd) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

This method tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for Bdd

impl StructuralPartialEq for Bdd