Struct BooleanDecisionDiagram 

pub struct BooleanDecisionDiagram { /* private fields */ }

Reduced ordered Boolean decision diagram with bounded construction work.

Implementations

impl BooleanDecisionDiagram

pub fn with_limits(limits: BooleanLimits) -> Self

Creates an empty diagram with explicit resource limits.

pub fn limits(&self) -> BooleanLimits

Returns the configured resource limits.

pub fn steps(&self) -> usize

Returns cumulative charged work.

pub fn charge(&mut self, steps: usize) -> Result<(), BooleanResourceError>

Charge before traversal or allocation. Collection and cloning preserve consumed work; an error never stands in for a Boolean result. Cheap constant/cache returns do not consume steps. Callers must charge their own loops, including loops over constant Boolean expressions.

Errors

Returns BooleanResourceError if charging steps exceeds the work limit.

pub fn collect_garbage<'a>( &mut self, roots: impl IntoIterator<Item = &'a mut DecisionId>, ) -> usize

Rebuild the diagram from all live roots, removing dead intermediate functions and operation caches. Variable indices do not change.

Every surviving DecisionId must be passed here: ids are renumbered, and any unlisted external ids become invalid. Collect only at a boundary where the caller owns the complete root set.

pub fn evaluate( &self, root: DecisionId, variable: impl FnMut(usize) -> bool, ) -> bool

Evaluate one Boolean function without traversing unrelated choices.

pub fn witness(&self, root: DecisionId) -> Option<BTreeMap<usize, bool>>

One satisfying variable assignment; omitted variables are don’t-cares.

pub fn conjunction_witness( &mut self, roots: &[DecisionId], ) -> Result<Option<BTreeMap<usize, bool>>, BooleanResourceError>

Finds one assignment satisfying every supplied decision.

Errors

Returns BooleanResourceError if the search exceeds the work limit.

pub fn variables(&self, root: DecisionId) -> BTreeSet<usize>

Returns every variable reachable from root.

pub fn constrain( &mut self, root: DecisionId, care: DecisionId, ) -> Result<DecisionId, BooleanResourceError>

Simplify a function outside its care set. The returned function equals root wherever care holds; impossible selector combinations are free.

Errors

Returns BooleanResourceError if construction exceeds configured limits.

Panics

Panics if either decision does not belong to this diagram.

pub fn nodes(&self) -> &[DecisionNode]

Returns the nonterminal nodes in decision-id order.

pub fn make_node( &mut self, variable: usize, low: DecisionId, high: DecisionId, ) -> Result<DecisionId, BooleanResourceError>

Returns the reduced node for variable, low, and high.

Errors

Returns BooleanResourceError if allocation exceeds configured limits.

pub fn node(&self, id: DecisionId) -> Option<DecisionNode>

Returns the nonterminal node named by id, or None for a terminal.

Panics

Panics if id names a nonterminal outside this diagram.

pub fn cached_complement(&self, root: DecisionId) -> Option<DecisionId>

Returns an already known exact complement without constructing nodes. Constants always have known complements.

Panics

Panics if root does not belong to this diagram.

pub fn negate( &mut self, root: DecisionId, ) -> Result<DecisionId, BooleanResourceError>

Returns the logical negation of root.

Errors

Returns BooleanResourceError if construction exceeds configured limits.

Panics

Panics if root does not belong to this diagram.

pub fn apply( &mut self, operator: BooleanOp, left: DecisionId, right: DecisionId, ) -> Result<DecisionId, BooleanResourceError>

Fold constants before visiting decision pairs. All operators commute.

Errors

Returns BooleanResourceError if construction exceeds configured limits.

pub fn values_up_to( &mut self, roots: &[DecisionId], limit: usize, ) -> Result<Vec<Vec<bool>>, BooleanResourceError>

Enumerate at most limit distinct output tuples, charging residual states and their coordinates before allocating them.

Errors

Returns BooleanResourceError if enumeration exceeds the work limit.

impl BooleanDecisionDiagram

pub fn start_witness_tape( &mut self, explicit_columns: impl IntoIterator<Item = usize>, max_operations: usize, ) -> Result<(), BooleanResourceError>

Start an owned tape for passive row coefficients. Every deferred row shares this explicit-column partition; keep every row-space constraint column explicit until all rows are expanded. Passive coordinates can be read with BooleanRow::probe_coefficients. Operation bounds include dead history, and construction/reconstruction spend the same work meter.

Errors

Returns BooleanResourceError if indexing columns exceeds configured limits.

Panics

Panics if a witness tape is already active.

pub fn extend_witness_front( &mut self, columns: &[usize], rows: &mut [BooleanRow], ) -> Result<(), BooleanResourceError>

Promote coordinates into the shared explicit row front without expanding other coefficients. The caller must supply every surviving deferred row owned by this tape, including rows retained for later queries or replay. No deferred clone outside rows may be used after this boundary. Explicit rows may also be supplied and remain unchanged.

Raw coefficients, including off-activation values, are queried under the old partition. Row fronts and the partition change only after all work succeeds; a failure retains the tape and rows without refunding spent work. Activation and witness handles never change, and columns are never demoted. Fixed roots share one topological evaluation per new column; intermediate values for different columns are never stored together.

Errors

Returns BooleanResourceError if querying or staging exceeds resource limits.

Panics

Panics if no witness tape is active.

pub fn witness_collection_work(&self) -> usize

Additional owned tape nodes and decision handles walked by collection. Charge this together with the arena and external roots before collecting.

pub fn finish_witness_tape(&mut self)

Release the tape after every retained deferred row has been expanded.

Trait Implementations

impl Clone for BooleanDecisionDiagram

fn clone(&self) -> BooleanDecisionDiagram

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for BooleanDecisionDiagram

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

Formats the value using the given formatter.

impl Default for BooleanDecisionDiagram

fn default() -> BooleanDecisionDiagram

Returns the “default value” for a type.