Struct BDDFunction 

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

Boolean function represented as BDD

Trait Implementations

impl BooleanFunction for BDDFunction

fn f<'__id>(manager: &<Self as Function>::Manager<'__id>) -> Self

Get the always false function ⊥

fn f_edge<'__id>( manager: &<Self as Function>::Manager<'__id>, ) -> <<Self as Function>::Manager<'__id> as Manager>::Edge

Get the always false function ⊥ as edge

fn t<'__id>(manager: &<Self as Function>::Manager<'__id>) -> Self

Get the always true function ⊤

fn t_edge<'__id>( manager: &<Self as Function>::Manager<'__id>, ) -> <<Self as Function>::Manager<'__id> as Manager>::Edge

Get the always true function ⊤ as edge

fn var<'__id>( manager: &<Self as Function>::Manager<'__id>, var: VarNo, ) -> AllocResult<Self>

Get the Boolean function that is true if and only if var is true

fn var_edge<'__id>( manager: &<Self as Function>::Manager<'__id>, var: VarNo, ) -> AllocResult<<<Self as Function>::Manager<'__id> as Manager>::Edge>

Get the Boolean function (as edge) that is true if and only if var is true

fn not_var<'__id>( manager: &<Self as Function>::Manager<'__id>, var: VarNo, ) -> AllocResult<Self>

Get the Boolean function that is true if and only if var is false

fn not_var_edge<'__id>( manager: &<Self as Function>::Manager<'__id>, var: VarNo, ) -> AllocResult<<<Self as Function>::Manager<'__id> as Manager>::Edge>

Get the Boolean function (as edge) that is true if and only if var is false

fn not(&self) -> AllocResult<Self>

Compute the negation ¬self

fn not_edge<'__id>( manager: &<Self as Function>::Manager<'__id>, edge: &<<Self as Function>::Manager<'__id> as Manager>::Edge, ) -> AllocResult<<<Self as Function>::Manager<'__id> as Manager>::Edge>

Compute the negation ¬edge, edge version

fn not_owned(self) -> AllocResult<Self>

Compute the negation ¬self, owned version

fn not_edge_owned<'__id>( manager: &<Self as Function>::Manager<'__id>, edge: <<Self as Function>::Manager<'__id> as Manager>::Edge, ) -> AllocResult<<<Self as Function>::Manager<'__id> as Manager>::Edge>

Compute the negation ¬edge, owned edge version

fn and(&self, rhs: &Self) -> AllocResult<Self>

Compute the conjunction self ∧ rhs

fn and_edge<'__id>( manager: &<Self as Function>::Manager<'__id>, lhs: &<<Self as Function>::Manager<'__id> as Manager>::Edge, rhs: &<<Self as Function>::Manager<'__id> as Manager>::Edge, ) -> AllocResult<<<Self as Function>::Manager<'__id> as Manager>::Edge>

Compute the conjunction lhs ∧ rhs, edge version

fn or(&self, rhs: &Self) -> AllocResult<Self>

Compute the disjunction self ∨ rhs

fn or_edge<'__id>( manager: &<Self as Function>::Manager<'__id>, lhs: &<<Self as Function>::Manager<'__id> as Manager>::Edge, rhs: &<<Self as Function>::Manager<'__id> as Manager>::Edge, ) -> AllocResult<<<Self as Function>::Manager<'__id> as Manager>::Edge>

Compute the disjunction lhs ∨ rhs, edge version

fn nand(&self, rhs: &Self) -> AllocResult<Self>

Compute the negated conjunction self ⊼ rhs

fn nand_edge<'__id>( manager: &<Self as Function>::Manager<'__id>, lhs: &<<Self as Function>::Manager<'__id> as Manager>::Edge, rhs: &<<Self as Function>::Manager<'__id> as Manager>::Edge, ) -> AllocResult<<<Self as Function>::Manager<'__id> as Manager>::Edge>

Compute the negated conjunction lhs ⊼ rhs, edge version

fn nor(&self, rhs: &Self) -> AllocResult<Self>

Compute the negated disjunction self ⊽ rhs

fn nor_edge<'__id>( manager: &<Self as Function>::Manager<'__id>, lhs: &<<Self as Function>::Manager<'__id> as Manager>::Edge, rhs: &<<Self as Function>::Manager<'__id> as Manager>::Edge, ) -> AllocResult<<<Self as Function>::Manager<'__id> as Manager>::Edge>

Compute the negated disjunction lhs ⊽ rhs, edge version

fn xor(&self, rhs: &Self) -> AllocResult<Self>

Compute the exclusive disjunction self ⊕ rhs

fn xor_edge<'__id>( manager: &<Self as Function>::Manager<'__id>, lhs: &<<Self as Function>::Manager<'__id> as Manager>::Edge, rhs: &<<Self as Function>::Manager<'__id> as Manager>::Edge, ) -> AllocResult<<<Self as Function>::Manager<'__id> as Manager>::Edge>

Compute the exclusive disjunction lhs ⊕ rhs, edge version

fn equiv(&self, rhs: &Self) -> AllocResult<Self>

Compute the equivalence self ↔ rhs

fn equiv_edge<'__id>( manager: &<Self as Function>::Manager<'__id>, lhs: &<<Self as Function>::Manager<'__id> as Manager>::Edge, rhs: &<<Self as Function>::Manager<'__id> as Manager>::Edge, ) -> AllocResult<<<Self as Function>::Manager<'__id> as Manager>::Edge>

Compute the equivalence lhs ↔ rhs, edge version

fn imp(&self, rhs: &Self) -> AllocResult<Self>

Compute the implication self → rhs (or self ≤ rhs)

fn imp_edge<'__id>( manager: &<Self as Function>::Manager<'__id>, lhs: &<<Self as Function>::Manager<'__id> as Manager>::Edge, rhs: &<<Self as Function>::Manager<'__id> as Manager>::Edge, ) -> AllocResult<<<Self as Function>::Manager<'__id> as Manager>::Edge>

Compute the implication lhs → rhs, edge version

fn imp_strict(&self, rhs: &Self) -> AllocResult<Self>

Compute the strict implication self < rhs

fn imp_strict_edge<'__id>( manager: &<Self as Function>::Manager<'__id>, lhs: &<<Self as Function>::Manager<'__id> as Manager>::Edge, rhs: &<<Self as Function>::Manager<'__id> as Manager>::Edge, ) -> AllocResult<<<Self as Function>::Manager<'__id> as Manager>::Edge>

Compute the strict implication lhs < rhs, edge version

fn ite(&self, f1: &Self, f2: &Self) -> AllocResult<Self>

Compute if self { then_case } else { else_case }

fn ite_edge<'__id>( manager: &<Self as Function>::Manager<'__id>, e0: &<<Self as Function>::Manager<'__id> as Manager>::Edge, e1: &<<Self as Function>::Manager<'__id> as Manager>::Edge, e2: &<<Self as Function>::Manager<'__id> as Manager>::Edge, ) -> AllocResult<<<Self as Function>::Manager<'__id> as Manager>::Edge>

Compute if if_edge { then_edge } else { else_edge } (edge version)

fn pick_cube_dd_set(&self, rhs: &Self) -> AllocResult<Self>

Pick a symbolic cube of this function, i.e., as decision diagram, using the literals in literal_set if there is a choice

fn pick_cube_dd_set_edge<'__id>( manager: &<Self as Function>::Manager<'__id>, lhs: &<<Self as Function>::Manager<'__id> as Manager>::Edge, rhs: &<<Self as Function>::Manager<'__id> as Manager>::Edge, ) -> AllocResult<<<Self as Function>::Manager<'__id> as Manager>::Edge>

Edge version of Self::pick_cube_dd_set()

fn cofactors(&self) -> Option<(Self, Self)>

Get the cofactors (f_true, f_false) of self

fn cofactor_true(&self) -> Option<Self>

Get the cofactor f_true of self

fn cofactor_false(&self) -> Option<Self>

Get the cofactor f_false of self

fn cofactors_edge<'__a, '__id>( manager: &'__a <Self as Function>::Manager<'__id>, f: &'__a <<Self as Function>::Manager<'__id> as Manager>::Edge, ) -> Option<(Borrowed<'__a, <<Self as Function>::Manager<'__id> as Manager>::Edge>, Borrowed<'__a, <<Self as Function>::Manager<'__id> as Manager>::Edge>)>

Get the cofactors (f_true, f_false) of f, edge version

fn cofactors_node<'__a, '__id>( tag: ETagOfFunc<'__id, Self>, node: &'__a INodeOfFunc<'__id, Self>, ) -> (Borrowed<'__a, <<Self as Function>::Manager<'__id> as Manager>::Edge>, Borrowed<'__a, <<Self as Function>::Manager<'__id> as Manager>::Edge>)

Get the cofactors (f_true, f_false) of node, assuming an incoming edge with EdgeTag

fn satisfiable(&self) -> bool

Returns true iff self is satisfiable, i.e. is not ⊥

fn valid(&self) -> bool

Returns true iff self is valid, i.e. is ⊤

fn sat_count<__N, __S>( &self, vars: LevelNo, cache: &mut SatCountCache<__N, __S>, ) -> __N

where __N: SatCountNumber, __S: BuildHasher,

Count the number of satisfying assignments, assuming vars input variables

fn sat_count_edge<'__id, __N, __S>( manager: &<Self as Function>::Manager<'__id>, edge: &<<Self as Function>::Manager<'__id> as Manager>::Edge, vars: LevelNo, cache: &mut SatCountCache<__N, __S>, ) -> __N

where __N: SatCountNumber, __S: BuildHasher,

Edge version of Self::sat_count()

fn pick_cube( &self, choice: impl for<'__id> FnMut(&<Self as Function>::Manager<'__id>, &<<Self as Function>::Manager<'__id> as Manager>::Edge, LevelNo) -> bool, ) -> Option<Vec<OptBool>>

Pick a cube of this function

fn pick_cube_edge<'__id>( manager: &<Self as Function>::Manager<'__id>, edge: &<<Self as Function>::Manager<'__id> as Manager>::Edge, choice: impl FnMut(&<Self as Function>::Manager<'__id>, &<<Self as Function>::Manager<'__id> as Manager>::Edge, LevelNo) -> bool, ) -> Option<Vec<OptBool>>

Edge version of Self::pick_cube()

fn pick_cube_dd( &self, choice: impl for<'__id> FnMut(&<Self as Function>::Manager<'__id>, &<<Self as Function>::Manager<'__id> as Manager>::Edge, LevelNo) -> bool, ) -> AllocResult<Self>

Pick a symbolic cube of this function, i.e., as decision diagram

fn pick_cube_dd_edge<'__id>( manager: &<Self as Function>::Manager<'__id>, edge: &<<Self as Function>::Manager<'__id> as Manager>::Edge, choice: impl FnMut(&<Self as Function>::Manager<'__id>, &<<Self as Function>::Manager<'__id> as Manager>::Edge, LevelNo) -> bool, ) -> AllocResult<<<Self as Function>::Manager<'__id> as Manager>::Edge>

Edge version of Self::pick_cube_dd()

fn pick_cube_uniform<__S: BuildHasher>( &self, cache: &mut SatCountCache<F64, __S>, rng: &mut Rng, ) -> Option<Vec<OptBool>>

Pick a random cube of this function, where each cube has the same probability of being chosen

fn pick_cube_uniform_edge<'__id, __S: BuildHasher>( manager: &<Self as Function>::Manager<'__id>, edge: &<<Self as Function>::Manager<'__id> as Manager>::Edge, cache: &mut SatCountCache<F64, __S>, rng: &mut Rng, ) -> Option<Vec<OptBool>>

Edge version of Self::pick_cube_uniform()

fn eval(&self, args: impl IntoIterator<Item = (VarNo, bool)>) -> bool

Evaluate this Boolean function

fn eval_edge<'__id>( manager: &<Self as Function>::Manager<'__id>, edge: &<<Self as Function>::Manager<'__id> as Manager>::Edge, args: impl IntoIterator<Item = (VarNo, bool)>, ) -> bool

Edge version of Self::eval()

impl BooleanFunctionQuant for BDDFunction

fn restrict(&self, rhs: &Self) -> AllocResult<Self>

Restrict a set of vars to constant values

fn restrict_edge<'__id>( manager: &<Self as Function>::Manager<'__id>, lhs: &<<Self as Function>::Manager<'__id> as Manager>::Edge, rhs: &<<Self as Function>::Manager<'__id> as Manager>::Edge, ) -> AllocResult<<<Self as Function>::Manager<'__id> as Manager>::Edge>

Restrict a set of vars to constant values, edge version

fn forall(&self, rhs: &Self) -> AllocResult<Self>

Compute the universal quantification over vars

fn forall_edge<'__id>( manager: &<Self as Function>::Manager<'__id>, lhs: &<<Self as Function>::Manager<'__id> as Manager>::Edge, rhs: &<<Self as Function>::Manager<'__id> as Manager>::Edge, ) -> AllocResult<<<Self as Function>::Manager<'__id> as Manager>::Edge>

Compute the universal quantification of root over vars, edge version

fn exists(&self, rhs: &Self) -> AllocResult<Self>

Compute the existential quantification over vars

fn exists_edge<'__id>( manager: &<Self as Function>::Manager<'__id>, lhs: &<<Self as Function>::Manager<'__id> as Manager>::Edge, rhs: &<<Self as Function>::Manager<'__id> as Manager>::Edge, ) -> AllocResult<<<Self as Function>::Manager<'__id> as Manager>::Edge>

Compute the existential quantification of root over vars, edge version

fn unique(&self, rhs: &Self) -> AllocResult<Self>

Compute the unique quantification over vars

fn unique_edge<'__id>( manager: &<Self as Function>::Manager<'__id>, lhs: &<<Self as Function>::Manager<'__id> as Manager>::Edge, rhs: &<<Self as Function>::Manager<'__id> as Manager>::Edge, ) -> AllocResult<<<Self as Function>::Manager<'__id> as Manager>::Edge>

Compute the unique quantification of root over vars, edge version

fn apply_forall( &self, op: BooleanOperator, rhs: &Self, vars: &Self, ) -> AllocResult<Self>

Combined application of op and quantification ∀x. self <op> rhs, where <op> is any of the operations from BooleanOperator

fn apply_forall_edge<'__id>( manager: &<Self as Function>::Manager<'__id>, op: BooleanOperator, lhs: &<<Self as Function>::Manager<'__id> as Manager>::Edge, rhs: &<<Self as Function>::Manager<'__id> as Manager>::Edge, vars: &<<Self as Function>::Manager<'__id> as Manager>::Edge, ) -> AllocResult<<<Self as Function>::Manager<'__id> as Manager>::Edge>

Combined application of op and forall quantification, edge version

fn apply_exists( &self, op: BooleanOperator, rhs: &Self, vars: &Self, ) -> AllocResult<Self>

Combined application of op and quantification ∃x. self <op> rhs, where <op> is any of the operations from BooleanOperator

fn apply_exists_edge<'__id>( manager: &<Self as Function>::Manager<'__id>, op: BooleanOperator, lhs: &<<Self as Function>::Manager<'__id> as Manager>::Edge, rhs: &<<Self as Function>::Manager<'__id> as Manager>::Edge, vars: &<<Self as Function>::Manager<'__id> as Manager>::Edge, ) -> AllocResult<<<Self as Function>::Manager<'__id> as Manager>::Edge>

Combined application of op and existential quantification, edge version

fn apply_unique( &self, op: BooleanOperator, rhs: &Self, vars: &Self, ) -> AllocResult<Self>

Combined application of op and quantification ∃!x. self <op> rhs, where <op> is any of the operations from BooleanOperator

fn apply_unique_edge<'__id>( manager: &<Self as Function>::Manager<'__id>, op: BooleanOperator, lhs: &<<Self as Function>::Manager<'__id> as Manager>::Edge, rhs: &<<Self as Function>::Manager<'__id> as Manager>::Edge, vars: &<<Self as Function>::Manager<'__id> as Manager>::Edge, ) -> AllocResult<<<Self as Function>::Manager<'__id> as Manager>::Edge>

Combined application of op and unique quantification, edge version

fn exist(&self, vars: &Self) -> Result<Self, OutOfMemory>

👎Deprecated

Deprecated alias for Self::exists()

fn apply_exist( &self, op: BooleanOperator, rhs: &Self, vars: &Self, ) -> Result<Self, OutOfMemory>

👎Deprecated

Deprecated alias for Self::apply_exists()

fn exist_edge<'id>( manager: &Self::Manager<'id>, root: &<Self::Manager<'id> as Manager>::Edge, vars: &<Self::Manager<'id> as Manager>::Edge, ) -> Result<<Self::Manager<'id> as Manager>::Edge, OutOfMemory>

👎Deprecated

Deprecated alias for Self::exists_edge()

fn apply_exist_edge<'id>( manager: &Self::Manager<'id>, op: BooleanOperator, lhs: &<Self::Manager<'id> as Manager>::Edge, rhs: &<Self::Manager<'id> as Manager>::Edge, vars: &<Self::Manager<'id> as Manager>::Edge, ) -> Result<<Self::Manager<'id> as Manager>::Edge, OutOfMemory>

👎Deprecated

Deprecated alias for Self::apply_exists_edge()

impl Clone for BDDFunction

fn clone(&self) -> BDDFunction

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl DotStyle<()> for BDDFunction

fn edge_style(no: usize, tag: T) -> (EdgeStyle, bool, Color)

Get the style for the n-th outgoing edge, tagged with tag

impl Function for BDDFunction

const REPR_ID: &'static str = <FunctionInner as ::oxidd_core::function::Function>::REPR_ID

Representation identifier such as “BDD” or “MTBDD”

type Manager<'__id> = <BDDFunctionMT<<IndexDD<NodeWithLevelCons<2>, (), StaticTerminalManagerCons<BDDTerminal>, BDDRulesCons, BDDManagerDataCons, 2> as DD>::Function> as Function>::Manager<'__id>

Type of the associated manager

type ManagerRef = BDDManagerRef

Manager references for Self::Manager

fn from_edge<'__id>( manager: &Self::Manager<'__id>, edge: <Self::Manager<'__id> as Manager>::Edge, ) -> Self

Create a new function from a manager reference and an edge

fn as_edge<'__id>( &self, manager: &Self::Manager<'__id>, ) -> &<Self::Manager<'__id> as Manager>::Edge

Converts this function into the underlying edge (as reference), checking that it belongs to the given manager

fn into_edge<'__id>( self, manager: &Self::Manager<'__id>, ) -> <Self::Manager<'__id> as Manager>::Edge

Converts this function into the underlying edge, checking that it belongs to the given manager

fn manager_ref(&self) -> BDDManagerRef

Clone the ManagerRef part

fn with_manager_shared<__F, __T>(&self, f: __F) -> __T

where __F: for<'__id> FnOnce(&Self::Manager<'__id>, &<Self::Manager<'__id> as Manager>::Edge) -> __T,

Obtain a shared manager reference as well as the underlying edge

fn with_manager_exclusive<__F, __T>(&self, f: __F) -> __T

where __F: for<'__id> FnOnce(&mut Self::Manager<'__id>, &<Self::Manager<'__id> as Manager>::Edge) -> __T,

Obtain an exclusive manager reference as well as the underlying edge

fn from_edge_ref<'id>( manager: &Self::Manager<'id>, edge: &<Self::Manager<'id> as Manager>::Edge, ) -> Self

Create a new function from a manager reference and an edge reference

fn node_count(&self) -> usize

Count the number of nodes in this function, including terminal nodes

impl FunctionSubst for BDDFunction

fn substitute<'__a>( &'__a self, substitution: impl Substitution<Replacement = &'__a Self>, ) -> AllocResult<Self>

Substitute variables in self according to substitution

fn substitute_edge<'__id, '__a>( manager: &'__a <Self as Function>::Manager<'__id>, edge: &'__a <<Self as Function>::Manager<'__id> as Manager>::Edge, substitution: impl Substitution<Replacement = Borrowed<'__a, <<Self as Function>::Manager<'__id> as Manager>::Edge>>, ) -> AllocResult<<<Self as Function>::Manager<'__id> as Manager>::Edge>

Edge version of Self::substitute()

impl Hash for BDDFunction

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 Ord for BDDFunction

fn cmp(&self, other: &BDDFunction) -> Ordering

This method returns an Ordering between self and other.

fn max(self, other: Self) -> Self

where Self: Sized,

Compares and returns the maximum of two values.

fn min(self, other: Self) -> Self

where Self: Sized,

Compares and returns the minimum of two values.

fn clamp(self, min: Self, max: Self) -> Self

where Self: Sized,

Restrict a value to a certain interval.

impl PartialEq for BDDFunction

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

Tests for self and other values to be equal, and is used by ==.

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

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

impl PartialOrd for BDDFunction

fn partial_cmp(&self, other: &BDDFunction) -> Option<Ordering>

This method returns an ordering between self and other values if one exists.

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

Tests less than (for self and other) and is used by the < operator.

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

Tests less than or equal to (for self and other) and is used by the <= operator.

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

Tests greater than (for self and other) and is used by the > operator.

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

Tests greater than or equal to (for self and other) and is used by the >= operator.

impl Eq for BDDFunction

impl StructuralPartialEq for BDDFunction