Struct BCDDFunction

pub struct BCDDFunction<F: Function>(/* private fields */);

Boolean function backed by a complement edge binary decision diagram

Implementations

impl<F: Function> BCDDFunction<F>

pub fn into_inner(self) -> F

Convert self into the underlying Function

Trait Implementations

impl<F: Function> BooleanFunction for BCDDFunction<F>

where for<'id> F::Manager<'id>: Manager<Terminal = BCDDTerminal, EdgeTag = EdgeTag> + HasBCDDOpApplyCache<F::Manager<'id>>, for<'id> <F::Manager<'id> as Manager>::InnerNode: HasLevel,

fn new_var<'id>(manager: &mut Self::Manager<'id>) -> AllocResult<Self>

Get a fresh variable, i.e., a function that is true if and only if the variable is true. This adds a new level to a decision diagram.

fn f_edge<'id>(manager: &Self::Manager<'id>) -> EdgeOfFunc<'id, Self>

Get the always false function ⊥ as edge

fn t_edge<'id>(manager: &Self::Manager<'id>) -> EdgeOfFunc<'id, Self>

Get the always true function ⊤ as edge

fn not_edge<'id>( manager: &Self::Manager<'id>, edge: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Compute the negation ¬edge, edge version

fn not_edge_owned<'id>( _manager: &Self::Manager<'id>, edge: EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Compute the negation ¬edge, owned edge version

fn and_edge<'id>( manager: &Self::Manager<'id>, lhs: &EdgeOfFunc<'id, Self>, rhs: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Compute the conjunction lhs ∧ rhs, edge version

fn or_edge<'id>( manager: &Self::Manager<'id>, lhs: &EdgeOfFunc<'id, Self>, rhs: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Compute the disjunction lhs ∨ rhs, edge version

fn nand_edge<'id>( manager: &Self::Manager<'id>, lhs: &EdgeOfFunc<'id, Self>, rhs: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Compute the negated conjunction lhs ⊼ rhs, edge version

fn nor_edge<'id>( manager: &Self::Manager<'id>, lhs: &EdgeOfFunc<'id, Self>, rhs: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Compute the negated disjunction lhs ⊽ rhs, edge version

fn xor_edge<'id>( manager: &Self::Manager<'id>, lhs: &EdgeOfFunc<'id, Self>, rhs: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Compute the exclusive disjunction lhs ⊕ rhs, edge version

fn equiv_edge<'id>( manager: &Self::Manager<'id>, lhs: &EdgeOfFunc<'id, Self>, rhs: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Compute the equivalence lhs ↔ rhs, edge version

fn imp_edge<'id>( manager: &Self::Manager<'id>, lhs: &EdgeOfFunc<'id, Self>, rhs: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Compute the implication lhs → rhs, edge version

fn imp_strict_edge<'id>( manager: &Self::Manager<'id>, lhs: &EdgeOfFunc<'id, Self>, rhs: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Compute the strict implication lhs < rhs, edge version

fn ite_edge<'id>( manager: &Self::Manager<'id>, if_edge: &EdgeOfFunc<'id, Self>, then_edge: &EdgeOfFunc<'id, Self>, else_edge: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

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

fn sat_count_edge<'id, N: SatCountNumber, S: BuildHasher>( manager: &Self::Manager<'id>, edge: &EdgeOfFunc<'id, Self>, vars: LevelNo, cache: &mut SatCountCache<N, S>, ) -> N

Edge version of Self::sat_count()

fn pick_cube_edge<'id, 'a, I>( manager: &'a Self::Manager<'id>, edge: &'a EdgeOfFunc<'id, Self>, order: impl IntoIterator<IntoIter = I>, choice: impl FnMut(&Self::Manager<'id>, &EdgeOfFunc<'id, Self>, LevelNo) -> bool, ) -> Option<Vec<OptBool>>

where I: ExactSizeIterator<Item = &'a EdgeOfFunc<'id, Self>>,

Edge version of Self::pick_cube()

fn pick_cube_dd_edge<'id>( manager: &Self::Manager<'id>, edge: &EdgeOfFunc<'id, Self>, choice: impl FnMut(&Self::Manager<'id>, &EdgeOfFunc<'id, Self>, LevelNo) -> bool, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Edge version of Self::pick_cube_dd()

fn pick_cube_dd_set_edge<'id>( manager: &Self::Manager<'id>, edge: &EdgeOfFunc<'id, Self>, literal_set: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Edge version of Self::pick_cube_dd_set()

fn eval_edge<'id, 'a>( manager: &'a Self::Manager<'id>, edge: &'a EdgeOfFunc<'id, Self>, args: impl IntoIterator<Item = (Borrowed<'a, EdgeOfFunc<'id, Self>>, bool)>, ) -> bool

Edge version of Self::eval()

fn f<'id>(manager: &Self::Manager<'id>) -> Self

Get the always false function ⊥

fn t<'id>(manager: &Self::Manager<'id>) -> Self

Get the always true function ⊤

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 not(&self) -> Result<Self, OutOfMemory>

Compute the negation ¬self

fn not_owned(self) -> Result<Self, OutOfMemory>

Compute the negation ¬self, owned version

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

Compute the conjunction self ∧ rhs

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

Compute the disjunction self ∨ rhs

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

Compute the negated conjunction self ⊼ rhs

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

Compute the negated disjunction self ⊽ rhs

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

Compute the exclusive disjunction self ⊕ rhs

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

Compute the equivalence self ↔ rhs

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

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

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

Compute the strict implication self < rhs

fn cofactors_edge<'a, 'id>( manager: &'a Self::Manager<'id>, f: &'a <Self::Manager<'id> as Manager>::Edge, ) -> Option<(Borrowed<'a, <Self::Manager<'id> as Manager>::Edge>, Borrowed<'a, <Self::Manager<'id> as Manager>::Edge>)>

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

fn cofactors_node<'a, 'id>( tag: <Self::Manager<'id> as Manager>::EdgeTag, node: &'a <Self::Manager<'id> as Manager>::InnerNode, ) -> (Borrowed<'a, <Self::Manager<'id> as Manager>::Edge>, Borrowed<'a, <Self::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 ite(&self, then_case: &Self, else_case: &Self) -> Result<Self, OutOfMemory>

Compute if self { then_case } else { else_case }

fn sat_count<N, S>(&self, vars: u32, cache: &mut SatCountCache<N, S>) -> N

where N: SatCountNumber, S: BuildHasher,

Count the number of satisfying assignments, assuming vars input variables

fn pick_cube<'a, I>( &'a self, order: impl IntoIterator<IntoIter = I>, choice: impl for<'id> FnMut(&Self::Manager<'id>, &<Self::Manager<'id> as Manager>::Edge, u32) -> bool, ) -> Option<Vec<OptBool>>

where I: ExactSizeIterator<Item = &'a Self>,

Pick a cube of this function

fn pick_cube_dd( &self, choice: impl for<'id> FnMut(&Self::Manager<'id>, &<Self::Manager<'id> as Manager>::Edge, u32) -> bool, ) -> Result<Self, OutOfMemory>

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

fn pick_cube_dd_set(&self, literal_set: &Self) -> Result<Self, OutOfMemory>

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_uniform<'a, I, S>( &'a self, order: impl IntoIterator<IntoIter = I>, cache: &mut SatCountCache<F64, S>, rng: &mut WyRand, ) -> Option<Vec<OptBool>>

where I: ExactSizeIterator<Item = &'a Self>, S: BuildHasher,

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

fn pick_cube_uniform_edge<'id, 'a, I, S>( manager: &'a Self::Manager<'id>, edge: &'a <Self::Manager<'id> as Manager>::Edge, order: impl IntoIterator<IntoIter = I>, cache: &mut SatCountCache<F64, S>, rng: &mut WyRand, ) -> Option<Vec<OptBool>>

where I: ExactSizeIterator<Item = &'a <Self::Manager<'id> as Manager>::Edge>, S: BuildHasher,

Edge version of Self::pick_cube_uniform()

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

Evaluate this Boolean function

impl<F: Function> BooleanFunctionQuant for BCDDFunction<F>

where for<'id> F::Manager<'id>: Manager<Terminal = BCDDTerminal, EdgeTag = EdgeTag> + HasBCDDOpApplyCache<F::Manager<'id>>, for<'id> <F::Manager<'id> as Manager>::InnerNode: HasLevel,

fn restrict_edge<'id>( manager: &Self::Manager<'id>, root: &EdgeOfFunc<'id, Self>, vars: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Restrict a set of vars to constant values, edge version

fn forall_edge<'id>( manager: &Self::Manager<'id>, root: &EdgeOfFunc<'id, Self>, vars: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Compute the universal quantification of root over vars, edge version

fn exist_edge<'id>( manager: &Self::Manager<'id>, root: &EdgeOfFunc<'id, Self>, vars: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Compute the existential quantification of root over vars, edge version

fn unique_edge<'id>( manager: &Self::Manager<'id>, root: &EdgeOfFunc<'id, Self>, vars: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Compute the unique quantification of root over vars, edge version

fn apply_forall_edge<'id>( manager: &Self::Manager<'id>, op: BooleanOperator, lhs: &EdgeOfFunc<'id, Self>, rhs: &EdgeOfFunc<'id, Self>, vars: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Combined application of op and forall quantification, edge version

fn apply_exist_edge<'id>( manager: &Self::Manager<'id>, op: BooleanOperator, lhs: &EdgeOfFunc<'id, Self>, rhs: &EdgeOfFunc<'id, Self>, vars: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Combined application of op and existential quantification, edge version

fn apply_unique_edge<'id>( manager: &Self::Manager<'id>, op: BooleanOperator, lhs: &EdgeOfFunc<'id, Self>, rhs: &EdgeOfFunc<'id, Self>, vars: &EdgeOfFunc<'id, Self>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Combined application of op and unique quantification, edge version

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

Restrict a set of vars to constant values

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

Compute the universal quantification over vars

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

Compute the existential quantification over vars

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

Compute the unique quantification over vars

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

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

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

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

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

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

impl<F: Clone + Function> Clone for BCDDFunction<F>

fn clone(&self) -> BCDDFunction<F>

Returns a copy of the value.

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

Performs copy-assignment from source.

impl<F: Debug + Function> Debug for BCDDFunction<F>

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

Formats the value using the given formatter.

impl<F: Function, T: Tag> DotStyle<T> for BCDDFunction<F>

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

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

impl<F: Function> From<F> for BCDDFunction<F>

fn from(value: F) -> Self

Converts to this type from the input type.

impl<F: Function> Function for BCDDFunction<F>

type Manager<'__id> = <F as Function>::Manager<'__id>

Type of the associated manager

type ManagerRef = <F as Function>::ManagerRef

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) -> <F as Function>::ManagerRef

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<F: Function> FunctionSubst for BCDDFunction<F>

where for<'id> F::Manager<'id>: Manager<Terminal = BCDDTerminal, EdgeTag = EdgeTag> + HasBCDDOpApplyCache<F::Manager<'id>>, for<'id> <F::Manager<'id> as Manager>::InnerNode: HasLevel,

fn substitute_edge<'id, 'a>( manager: &'a Self::Manager<'id>, edge: &'a EdgeOfFunc<'id, Self>, substitution: impl Substitution<Var = Borrowed<'a, EdgeOfFunc<'id, Self>>, Replacement = Borrowed<'a, EdgeOfFunc<'id, Self>>>, ) -> AllocResult<EdgeOfFunc<'id, Self>>

Edge version of Self::substitute()

fn substitute<'a>( &'a self, substitution: impl Substitution<Var = &'a Self, Replacement = &'a Self>, ) -> Result<Self, OutOfMemory>

Substitute variables in self according to substitution

impl<F: Hash + Function> Hash for BCDDFunction<F>

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<F: Ord + Function> Ord for BCDDFunction<F>

fn cmp(&self, other: &BCDDFunction<F>) -> 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<F: PartialEq + Function> PartialEq for BCDDFunction<F>

fn eq(&self, other: &BCDDFunction<F>) -> 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<F: PartialOrd + Function> PartialOrd for BCDDFunction<F>

fn partial_cmp(&self, other: &BCDDFunction<F>) -> 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<F: Eq + Function> Eq for BCDDFunction<F>

impl<F: Function> StructuralPartialEq for BCDDFunction<F>