Module obddimal::bdd_manager

All BDD building and manipulation functionality

Modules

dvo 🔒

Implementation of dynamic variable ordering techniques

dvo_schedules

Strategies for when and how to run DVO during BDD generation

from_dimacs 🔒

BDD building from CNF

graphviz 🔒

Utilities for saving the current BDD as a graphviz file for visualization

hash_select

Type aliases for HashMap and HashSet to be used throuout the codebase

options

Options for BDD building

order 🔒

Utility functions related to variable order

reduce 🔒

BDD reduction

sat 🔒

Satisfyability count, active nodes count

swap 🔒

Implementation of BDD layer swap

test 🔒

Utilities for BDD testing

util 🔒

Utility functions/macros

Structs

DDManager

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

Constants

ONE

Terminal node “one”

ZERO

Terminal node “zero”

Functions

align_clauses 🔒

Determine order in which clauses should be added to BDD

normalize_ite_args 🔒

Bring ITE calls of the form ite(f,f,h) = ite(f,1,h) = ite(h,1,f) ite(f,g,f) = ite(f,g,0) = ite(g,f,0) into canonical form