Struct obddimal::bdd_manager::DDManager

pub struct DDManager {
    pub nodes: HashMap<NodeID, DDNode>,
    order: Vec<u32>,
    var2nodes: Vec<HashSet<DDNode>>,
    c_table: HashMap<(NodeID, NodeID, NodeID), NodeID>,
}

Container combining the nodes list, unique tables, information about current variable ordering and computed table.

Fields

nodes: HashMap<NodeID, DDNode>

Node List

order: Vec<u32>

Variable ordering: order[v.0] is the depth of variable v in the tree

var2nodes: Vec<HashSet<DDNode>>

Unique Table for each variable. Note that the order (depth) in the BDD may be different than the order of this vec, and is only determined by order!

c_table: HashMap<(NodeID, NodeID, NodeID), NodeID>

Computed Table: maps (f,g,h) to ite(f,g,h)

Implementations

impl DDManager

fn var_at_level(&self, level: u32) -> Option<VarID>

Find the variable at specified level

fn sift_single_var(
    &mut self,
    var: VarID,
    max_increase: Option<u32>,
    f: NodeID
) -> NodeID

Swap layer containing specified variable first to the bottom of the BDD, then to the top, and then to the position which resulted in smallest BDD size. Optional parameter max_increase stops swapping in either direction once the difference between BDD size and current optimum exceeds threshold.

pub fn sift_all_vars(
    &mut self,
    f: NodeID,
    progressbar: bool,
    max_increase: Option<u32>
) -> NodeID

Perform sifting for every layer containing at least one variable. If progressbar is true, display a progress bar in the terminal which shows the number of layers already processed. See Self::sift_single_var() for max_increase parameter.

impl DDManager

pub fn from_instance(
    instance: &mut Instance,
    order: Option<Vec<u32>>,
    options: Options
) -> Result<(DDManager, NodeID), String>

Builds a BDD from a CNF read from DIMACS.

• instance - Input CNF
• order - Optional initial variable ordering, see crate::static_ordering for implementations
• options - DVO and progress bar settings

let mut instance = dimacs::parse_dimacs("examples/trivial.dimacs");
let order = Some(static_ordering::force(&instance));
let dvo = dvo_schedules::SiftingAtThreshold::new(5);
let (man, bdd) = DDManager::from_instance(
    &mut instance,
    order,
    Options::default().with_progressbars().with_dvo(dvo.into()),
).unwrap();

impl DDManager

fn collect_nodes(&self, f: NodeID) -> HashSet<NodeID>

Collect all nodes that are part of the specified function

pub fn graphviz(&self, f: NodeID) -> String

Generate graphviz for the provided function, not including any graph nodes not part of the function. TODO: Graphviz of all functions in DDManager

impl DDManager

pub(crate) fn reduce(&mut self, v: NodeID) -> NodeID

Reduces the BDD. This changes Node IDs, the new Node ID of the function passed to the function is returned. All other known Node IDs are invalid after reduce. Note: Reduction does not imply removing nodes not part of the specified function. Other functions may be present in the tree (multiple root nodes, or root above function).

See also “Graph-Based Algorithms for Boolean Function Manipulation” by Bryant (10.1109/TC.1986.1676819)

impl DDManager

fn is_sat(&self, node: u32) -> bool

pub fn sat_count(&self, f: NodeID) -> BigUint

fn sat_count_rec(
    &self,
    f: NodeID,
    cache: &mut HashMap<NodeID, BigUint>
) -> BigUint

pub fn count_active(&self, f: NodeID) -> u32

impl DDManager

pub fn swap(&mut self, a: VarID, b: VarID, f: NodeID) -> NodeID

Swaps graph layers of variables a and b. Requires a to be directly above b. Performs reduction which may change NodeIDs. Returns new NodeID of f.

impl DDManager

fn bootstrap(&mut self)

Initialize the BDD with zero and one constant nodes

fn ensure_order(&mut self, target: VarID)

Ensure order vec is valid up to specified variable

fn add_node(&mut self, node: DDNode) -> NodeID

Insert Node. ID is assigned for nonterminal nodes (var != 0). This does not check the unique table, you should do so before using!

fn node_get_or_create(&mut self, node: &DDNode) -> NodeID

Search for Node, create if it doesnt exist

fn zero(&self) -> NodeID

fn one(&self) -> NodeID

pub fn ith_var(&mut self, var: VarID) -> NodeID

pub fn nith_var(&mut self, var: VarID) -> NodeID

fn not(&mut self, f: NodeID) -> NodeID

pub fn and(&mut self, f: NodeID, g: NodeID) -> NodeID

pub fn or(&mut self, f: NodeID, g: NodeID) -> NodeID

fn xor(&mut self, f: NodeID, g: NodeID) -> NodeID

fn min_by_order(&self, fvar: VarID, gvar: VarID, hvar: VarID) -> VarID

Find top variable: Highest in tree according to order

fn ite(&mut self, f: NodeID, g: NodeID, h: NodeID) -> NodeID

fn xor_prim(&mut self, _vars: Vec<u32>) -> u32

Creates an XOR “ladder”

fn verify(&self, f: NodeID, trues: &[u32]) -> bool

pub fn purge_retain(&mut self, f: NodeID)

Trait Implementations

impl Clone for DDManager

fn clone(&self) -> DDManager

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for DDManager

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

Formats the value using the given formatter.

impl Default for DDManager

fn default() -> Self

Returns the “default value” for a type.