scram::core::Zbdd

Zero-Suppressed Binary Decision Diagrams for set manipulations.

#include <zbdd.h>

Inherits from boost::noncopyable

Public Classes

	Name
class	const_iterator <br>Iterator over products in a ZBDD container.

Public Types

	Name
using IntrusivePtr< Vertex< SetNode > >	VertexPtr <br>ZBDD vertex base.
using IntrusivePtr< Terminal< SetNode > >	TerminalPtr <br>Terminal vertex.

Public Functions

	Name
auto	begin() const
auto	end() const
	Zbdd(Bdd * bdd, const Settings & settings)<br>Converts Reduced Ordered BDD into Zero-Suppressed BDD.
	Zbdd(const Pdag * graph, const Settings & settings)<br>Constructor with the analysis target.
virtual	~Zbdd() =default
void	Analyze(const Pdag * graph =nullptr)<br>Runs the analysis with the representation of a PDAG as ZBDD.
const Zbdd &	products() const
std::size_t	size() const
bool	empty() const
bool	base() const

Protected Functions

	Name
Zbdd::VertexPtr	Apply(const VertexPtr & arg_one, const VertexPtr & arg_two, int limit_order)<br>Forward declarations of interdependent Apply operation specializations.
Zbdd::VertexPtr	Apply(const VertexPtr & arg_one, const VertexPtr & arg_two, int limit_order)
	Zbdd(const Settings & settings, bool coherent =false, int module_index =0)<br>The common constructor to initialize member variables.
const VertexPtr &	root() const
void	root(const VertexPtr & vertex)<br>Sets a new root vertex for ZBDD.
const Settings &	settings() const
const std::map< int, std::unique_ptr< Zbdd > > &	modules() const
void	Log()<br>Logs properties of the Zbdd.
SetNodePtr	FindOrAddVertex(int index, const VertexPtr & high, const VertexPtr & low, int order, bool module =false, bool coherent =false)<br>Finds or adds a unique SetNode in the ZBDD.
SetNodePtr	FindOrAddVertex(const Gate & gate, const VertexPtr & high, const VertexPtr & low)<br>Find or adds a ZBDD SetNode vertex using information from gates.
template <Connective Type> <br>VertexPtr	Apply(const VertexPtr & arg_one, const VertexPtr & arg_two, int limit_order)<br>Applies Boolean operation to two vertices representing sets.
VertexPtr	Apply(Connective type, const VertexPtr & arg_one, const VertexPtr & arg_two, int limit_order)<br>Applies Boolean operation to two vertices representing sets.
template <Connective Type> <br>VertexPtr	Apply(const SetNodePtr & arg_one, const SetNodePtr & arg_two, int limit_order)<br>Applies Boolean operation to ZBDD graph non-terminal vertices.
VertexPtr	EliminateComplements(const VertexPtr & vertex, std::unordered_map< int, VertexPtr > * wide_results)<br>Removes complements of variables from products.
void	EliminateConstantModules()<br>Removes constant modules from products.
VertexPtr	Minimize(const VertexPtr & vertex)<br>Removes subsets in ZBDD.
int	GatherModules(const VertexPtr & vertex, int current_order, std::map< int, std::pair< bool, int > > * modules)<br>Traverses ZBDD to find modules and adjusted cut-offs.
void	ApplySubstitutions(const std::vector< Pdag::Substitution > & substitutions)<br>Applies non-declarative substitutions at the end of analysis.
void	ClearTables()<br>Clears all memoization tables.
void	Freeze()<br>Freezes the graph.
void	JoinModule(int index, std::unique_ptr< Zbdd > container)<br>Joins a ZBDD representing a module gate.
Zbdd::VertexPtr	Apply(const SetNodePtr & arg_one, const SetNodePtr & arg_two, int limit_order)<br>Specialization of Apply for AND connective for non-terminal ZBDD vertices.
Zbdd::VertexPtr	Apply(const VertexPtr & arg_one, const VertexPtr & arg_two, int limit_order)<br>Specialization of Apply for AND connective for any ZBDD vertices.
Zbdd::VertexPtr	Apply(const SetNodePtr & arg_one, const SetNodePtr & arg_two, int limit_order)<br>Specialization of Apply for OR connective for non-terminal ZBDD vertices.
Zbdd::VertexPtr	Apply(const VertexPtr & arg_one, const VertexPtr & arg_two, int limit_order)<br>Specialization of Apply for OR connective for any ZBDD vertices.

Protected Attributes

	Name
const TerminalPtr	kBase_ <br>Terminal Base (Unity/1) set.
const TerminalPtr	kEmpty_ <br>Terminal Empty (Null/0) set.

Public Types Documentation

using VertexPtr

cpp

using scram::core::Zbdd::VertexPtr =  IntrusivePtr<Vertex<SetNode> >;

ZBDD vertex base.

using TerminalPtr

cpp

using scram::core::Zbdd::TerminalPtr =  IntrusivePtr<Terminal<SetNode> >;

Terminal vertex.

Public Functions Documentation

function begin

cpp

inline auto begin() const

Return: Iterators over sets in the ZBDD.

function end

cpp

inline auto end() const

function Zbdd

cpp

Zbdd(
    Bdd * bdd,
    const Settings & settings
)

Converts Reduced Ordered BDD into Zero-Suppressed BDD.

Parameters:

bdd ROBDD with the ITE vertices.
settings Settings for analysis.

Note: The input BDD is not passed as a constant because ZBDD needs BDD facilities to calculate prime implicants. However, ZBDD guarantees to preserve the original BDD structure.

Precondition: BDD has attributed edges with only one terminal (1/True).

Postcondition: The input BDD structure is not changed.

function Zbdd

cpp

Zbdd(
    const Pdag * graph,
    const Settings & settings
)

Constructor with the analysis target.

Parameters:

graph Preprocessed and fully normalized PDAG.
settings The analysis settings.

Note: The construction may take considerable time.

Precondition: The passed PDAG already has variable ordering.

ZBDD is directly produced from a PDAG.

function ~Zbdd

cpp

virtual ~Zbdd() =default

function Analyze

cpp

void Analyze(
    const Pdag * graph =nullptr
)

Runs the analysis with the representation of a PDAG as ZBDD.

Parameters:

graph The optional PDAG with non-declarative substitutions.

Postcondition: Substitutions destroy all the modules.

function products

cpp

inline const Zbdd & products() const

Return: Products generated by the analysis.

function size

cpp

inline std::size_t size() const

Return: The number of products in the ZBDD.

Note: This is not cheap. The complexity is O(N) on the number of sets in ZBDD.

function empty

cpp

inline bool empty() const

Return: true for ZBDD with no products.

function base

cpp

inline bool base() const

Return: true if the ZBDD represents a base/unity set.

Protected Functions Documentation

function Apply

cpp

Zbdd::VertexPtr Apply(
    const VertexPtr & arg_one,
    const VertexPtr & arg_two,
    int limit_order
)

Forward declarations of interdependent Apply operation specializations.

function Apply

cpp

Zbdd::VertexPtr Apply(
    const VertexPtr & arg_one,
    const VertexPtr & arg_two,
    int limit_order
)

function Zbdd

cpp

explicit Zbdd(
    const Settings & settings,
    bool coherent =false,
    int module_index =0
)

The common constructor to initialize member variables.

Parameters:

settings Settings that control analysis complexity.
coherent A flag for coherent modular functions.
module_index The index of a module if known.

function root

cpp

inline const VertexPtr & root() const

Return: Current root vertex of the ZBDD.

function root

cpp

inline void root(
    const VertexPtr & vertex
)

Sets a new root vertex for ZBDD.

Parameters:

vertex A vertex already registered in this ZBDD.

function settings

cpp

inline const Settings & settings() const

Return: Analysis setting with this ZBDD.

function modules

cpp

inline const std::map< int, std::unique_ptr< Zbdd > > & modules() const

Return: A set of registered and fully processed modules;

function Log

cpp

void Log()

Logs properties of the Zbdd.

function FindOrAddVertex

cpp

SetNodePtr FindOrAddVertex(
    int index,
    const VertexPtr & high,
    const VertexPtr & low,
    int order,
    bool module =false,
    bool coherent =false
)

Finds or adds a unique SetNode in the ZBDD.

Parameters:

index Positive or negative index of the node.
high The high vertex.
low The low vertex.
order The order for the vertex variable.
module The indication of a proxy for a modular ZBDD.
coherent The indication of a coherent proxy.

Return: Set node with the given parameters.

Warning: This function is not aware of reduction rules.

All vertices in the ZBDD must be created with this function. Otherwise, the ZBDD may not be reduced, and vertices will miss crucial meta-information about the ZBDD.

function FindOrAddVertex

cpp

SetNodePtr FindOrAddVertex(
    const Gate & gate,
    const VertexPtr & high,
    const VertexPtr & low
)

Find or adds a ZBDD SetNode vertex using information from gates.

Parameters:

gate Gate with index, order, and other information.
high The new high vertex.
low The new low vertex.

Return: SetNode for a replacement.

Warning: This function is not aware of reduction rules.

function Apply

cpp

template <Connective Type>
VertexPtr Apply(
    const VertexPtr & arg_one,
    const VertexPtr & arg_two,
    int limit_order
)

Applies Boolean operation to two vertices representing sets.

Parameters:

arg_one First argument ZBDD set.
arg_two Second argument ZBDD set.
limit_order The limit on the order for the computations.

Template Parameters:

Type The connective enum.

Return: The resulting ZBDD vertex.

Postcondition: The limit on the set order is guaranteed.

This is the main function for the operation.

function Apply

cpp

VertexPtr Apply(
    Connective type,
    const VertexPtr & arg_one,
    const VertexPtr & arg_two,
    int limit_order
)

Applies Boolean operation to two vertices representing sets.

Parameters:

type The connective or type of the gate.
arg_one First argument ZBDD set.
arg_two Second argument ZBDD set.
limit_order The limit on the order for the computations.

Return: The resulting ZBDD vertex.

Precondition: The connective is either AND or OR.

Postcondition: The limit on the set order is guaranteed.

This is a convenience function if the connective type cannot be determined at compile time.

function Apply

cpp

template <Connective Type>
VertexPtr Apply(
    const SetNodePtr & arg_one,
    const SetNodePtr & arg_two,
    int limit_order
)

Applies Boolean operation to ZBDD graph non-terminal vertices.

Parameters:

arg_one First argument set vertex.
arg_two Second argument set vertex.
limit_order The limit on the order for the computations.

Template Parameters:

Type The connective enum.

Return: The resulting ZBDD vertex.

Precondition: Argument vertices are ordered.

function EliminateComplements

cpp

VertexPtr EliminateComplements(
    const VertexPtr & vertex,
    std::unordered_map< int, VertexPtr > * wide_results
)

Removes complements of variables from products.

Parameters:

vertex The variable vertex in the ZBDD.
wide_results Memoisation of the processed vertices.

Return: Processed vertex.

Postcondition:

Sub-modules are not processed.
Complements of modules are not eliminated.

This procedure only needs to be performed for non-coherent graphs with minimal cut sets as output.

function EliminateConstantModules

cpp

void EliminateConstantModules()

Removes constant modules from products.

Precondition: All modules have been processed.

Constant modules are likely to happen after complement elimination. This procedure is inherently bottom-up, so the caller must make sure that the modules have already been pre-processed.

function Minimize

cpp

VertexPtr Minimize(
    const VertexPtr & vertex
)

Removes subsets in ZBDD.

Parameters:

vertex The variable node in the set.

Return: Processed vertex.

function GatherModules

cpp

int GatherModules(
    const VertexPtr & vertex,
    int current_order,
    std::map< int, std::pair< bool, int > > * modules
)

Traverses ZBDD to find modules and adjusted cut-offs.

Parameters:

vertex The root vertex to start with.
current_order The product order from the top to the module.
modules A map of module indices, coherence, and cut-offs.

Return:

The minimum product order from the bottom.
-1 if the vertex is terminal Empty on low branch only.

Precondition: The ZBDD is minimal.

Modules within modules are not gathered.

function ApplySubstitutions

cpp

void ApplySubstitutions(
    const std::vector< Pdag::Substitution > & substitutions
)

Applies non-declarative substitutions at the end of analysis.

Parameters:

substitutions The substitutions defined in PDAG.

function ClearTables

cpp

inline void ClearTables()

Clears all memoization tables.

function Freeze

cpp

inline void Freeze()

Freezes the graph.

Precondition: No more graph modifications after the freeze.

Releases all possible memory from memoization and unique tables.

function JoinModule

cpp

inline void JoinModule(
    int index,
    std::unique_ptr< Zbdd > container
)

Joins a ZBDD representing a module gate.

Parameters:

index The index of the module.
container The container of the module graph.

Precondition: The module products are final, and no more processing or sanitizing is needed.

function Apply

cpp

Zbdd::VertexPtr Apply(
    const SetNodePtr & arg_one,
    const SetNodePtr & arg_two,
    int limit_order
)

Specialization of Apply for AND connective for non-terminal ZBDD vertices.

function Apply

cpp

Zbdd::VertexPtr Apply(
    const VertexPtr & arg_one,
    const VertexPtr & arg_two,
    int limit_order
)

Specialization of Apply for AND connective for any ZBDD vertices.

function Apply

cpp

Zbdd::VertexPtr Apply(
    const SetNodePtr & arg_one,
    const SetNodePtr & arg_two,
    int limit_order
)

Specialization of Apply for OR connective for non-terminal ZBDD vertices.

function Apply

cpp

Zbdd::VertexPtr Apply(
    const VertexPtr & arg_one,
    const VertexPtr & arg_two,
    int limit_order
)

Specialization of Apply for OR connective for any ZBDD vertices.

Protected Attributes Documentation

variable kBase_

cpp

const TerminalPtr kBase_;

Terminal Base (Unity/1) set.

variable kEmpty_

cpp

const TerminalPtr kEmpty_;

Terminal Empty (Null/0) set.

Updated on 2025-11-11 at 16:51:08 +0000

scram::core::Zbdd ​

Public Classes ​

Public Types ​

Public Functions ​

Protected Functions ​

Protected Attributes ​

Public Types Documentation ​

using VertexPtr ​

using TerminalPtr ​

Public Functions Documentation ​

function begin ​

function end ​

function Zbdd ​

function Zbdd ​

function ~Zbdd ​

function Analyze ​

function products ​

function size ​

function empty ​

function base ​

Protected Functions Documentation ​

function Apply ​

function Apply ​

function Zbdd ​

function root ​

function root ​

function settings ​

function modules ​

function Log ​

function FindOrAddVertex ​

function FindOrAddVertex ​

function Apply ​

function Apply ​

function Apply ​

function EliminateComplements ​

function EliminateConstantModules ​

function Minimize ​

function GatherModules ​

function ApplySubstitutions ​

function ClearTables ​

function Freeze ​

function JoinModule ​

function Apply ​

function Apply ​

function Apply ​

function Apply ​

Protected Attributes Documentation ​

variable kBase_ ​

variable kEmpty_ ​

scram::core::Zbdd

Public Classes

Public Types

Public Functions

Protected Functions

Protected Attributes

Public Types Documentation

using VertexPtr

using TerminalPtr

Public Functions Documentation

function begin

function end

function Zbdd

function Zbdd

function ~Zbdd

function Analyze

function products

function size

function empty

function base

Protected Functions Documentation

function Apply

function Apply

function Zbdd

function root

function root

function settings

function modules

function Log

function FindOrAddVertex

function FindOrAddVertex

function Apply

function Apply

function Apply

function EliminateComplements

function EliminateConstantModules

function Minimize

function GatherModules

function ApplySubstitutions

function ClearTables

function Freeze

function JoinModule

function Apply

function Apply

function Apply

function Apply

Protected Attributes Documentation

variable kBase_

variable kEmpty_