Crate oxidd

Crate oxidd 

Source
Expand description

Default instantiation of oxidd-rules-* using oxidd-manager-index/pointer and an apply cache implementation from oxidd-cache

§Feature flags

  • bdd (enabled by default) — Enable the simple BDD implementation

  • bcdd (enabled by default) — Enable the complement edge BDD implementation

  • mtbdd (enabled by default) — Enable the MTBDD implementation

  • tdd — Enable the TDD implementation

  • zbdd (enabled by default) — Enable the ZBDD implementation

  • multi-threading (enabled by default) — Use multi-threaded implementations of the apply algorithm

  • manager-index (enabled by default) — Use the index-based manager implementation

    This implementation is generally faster than the pointer-based implementation, but is more restricted: There is no possibility to reserve space for more nodes after the initial allocation and the total number of nodes is limited to 2³² nodes for BDDs/ZBDDs, or 2³¹ nodes for BCDDs.

  • manager-pointer — Use the pointer-based manager implementation (suitable for BDDs/ZBDDs with more than 2³² nodes, or BCDDs with more than 2³¹ nodes)

    If both manager-index and manager-pointer are specified, the pointer-based implementation will be used.

  • apply-cache-direct-mapped (enabled by default) — Enable the direct mapped apply cache

  • statistics — Enable statistics (will harm performance)

  • dddmp (enabled by default) — DDDMP export

  • dot-export (enabled by default) — Visualization using Graphviz DOT

  • visualize (enabled by default) — Visualization using OxiDD-vis

Modules§

bcdd
Binary decision diagrams with complemented edges (BCDDs)
bdd
Binary decision diagrams (BDDs)
error
Error types
mtbdd
Multi-terminal binary decision diagrams (MTBDDs)
util
Various utilities for working with DDs
zbdd
Zero-suppressed binary decision diagrams (ZBDDs)

Structs§

Subst
Substitution mapping variables to replacement functions, created from slices of functions

Enums§

BooleanOperator
Binary operators on Boolean functions
Node
Either an inner or a terminal node

Traits§

BooleanFunction
Boolean functions 𝔹ⁿ → 𝔹
BooleanFunctionQuant
Quantification extension for BooleanFunction
BooleanVecSet
Set of Boolean vectors
Edge
Edge in a decision diagram
Function
Function in a decision diagram
FunctionSubst
Substitution extension for Function
HasLevel
Trait for nodes that have a level
HasWorkers
Helper trait to be implemented by Manager and ManagerRef if they feature a WorkerPool.
InnerNode
Node in a decision diagram
Manager
Manager for nodes in a decision diagram
ManagerRef
Manager reference
NumberBase
Basic trait for numbers
PseudoBooleanFunction
Pseudo-Boolean function 𝔹ⁿ → ℝ
Substitution
Substitution mapping variables to replacement functions
TVLFunction
Function of three valued logic
WorkerPool
Worker thread pool associated with a Manager

Type Aliases§

LevelNo
Level number type
NodeID
Node identifier returned by Edge::node_id()
VarNo
Variable number type