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 implementationThis 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-indexandmanager-pointerare 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)
Modules§
- bcdd
- Binary decision diagrams with complemented edges (BCDDs)
- bdd
- Binary decision diagrams (BDDs)
- 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§
- Boolean
Operator - Binary operators on Boolean functions
Traits§
- Boolean
Function - Boolean functions 𝔹ⁿ → 𝔹
- Boolean
Function Quant - Quantification extension for
BooleanFunction - Boolean
VecSet - Set of Boolean vectors
- Edge
- Edge in a decision diagram
- Function
- Function in a decision diagram
- Function
Subst - Substitution extension for
Function - HasWorkers
- Helper trait to be implemented by
ManagerandManagerRefif they feature aWorkerPool. - Inner
Node - Node in a decision diagram
- Manager
- Manager for nodes in a decision diagram
- Manager
Ref - Manager reference
- Number
Base - Basic trait for numbers
- Pseudo
Boolean Function - Pseudo-Boolean function 𝔹ⁿ → ℝ
- Substitution
- Substitution mapping variables to replacement functions
- TVLFunction
- Function of three valued logic
- Worker
Pool - Worker thread pool associated with a
Manager
Type Aliases§
- LevelNo
- Level number type
- NodeID
- Node identifier returned by
Edge::node_id()