scram::core::zbdd::CutSetContainer

Storage for generated cut sets in MOCUS. More...

#include <zbdd.h>

Inherits from scram::core::Zbdd, boost::noncopyable

Public Functions

	Name
	CutSetContainer(const Settings & settings, int module_index, int gate_index_bound, const Pdag * pdag)<br>Default constructor to initialize member variables.
VertexPtr	ConvertGate(const Gate & gate)<br>Converts a PDAG gate into intermediate cut sets.
int	GetNextGate()<br>Finds a gate in intermediate cut sets.
VertexPtr	ExtractIntermediateCutSets(int index)<br>Extracts (removes!) intermediate cut sets containing a node with a given index.
VertexPtr	ExpandGate(const VertexPtr & gate_zbdd, const VertexPtr & cut_sets)<br>Expands the intermediate ZBDD representation of a gate in intermediate cut sets containing the gate.
void	Merge(const VertexPtr & vertex)<br>Merges a set of cut sets into the main container.
void	EliminateComplements()<br>Eliminates all complements from cut sets.
void	EliminateConstantModules()<br>Removes constant modules from cut sets.
void	Minimize()<br>Minimizes cut sets in the container.
std::map< int, std::pair< bool, int > >	GatherModules()<br>Gathers all module indices in the cut sets.
void	JoinModule(int index, std::unique_ptr< Zbdd > container)<br>Joins a ZBDD representing a module gate.
void	Log()<br>< Joins fully processed modules.

Additional inherited members

Public Classes inherited from scram::core::Zbdd

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

Public Types inherited from scram::core::Zbdd

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

Public Functions inherited from scram::core::Zbdd

	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.
void	SetProbabilityContext(const Pdag * pdag)<br>Installs PDAG context for probability-aware traversal.
const Zbdd &	products() const
std::size_t	size() const
bool	empty() const
bool	base() const

Protected Functions inherited from scram::core::Zbdd

	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, const Pdag * pdag =nullptr)<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
bool	HasProbabilityContext() const
double	LiteralProbability(int literal) const<br>Computes literal probability for the current PDAG context.
const std::map< int, std::unique_ptr< Zbdd > > &	modules() const
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.
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.
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 inherited from scram::core::Zbdd

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

Friends inherited from scram::core::Zbdd

	Name
class	const_iterator

Detailed Description

cpp

class scram::core::zbdd::CutSetContainer;

Storage for generated cut sets in MOCUS.

The semantics is similar to a set of cut sets. The container assumes special variable ordering. Gates to be processed must be ordered to the top.

Public Functions Documentation

function CutSetContainer

cpp

CutSetContainer(
    const Settings & settings,
    int module_index,
    int gate_index_bound,
    const Pdag * pdag
)

Default constructor to initialize member variables.

Parameters:

settings Settings that control analysis complexity.
module_index The of a module if known.
gate_index_bound The exclusive lower bound for gate indices.

Precondition:

No complements of gates.
Gates are indexed sequentially starting from a number larger than the lower bound.
Basic events are indexed sequentially up to a number less than or equal to the given lower bound.

function ConvertGate

cpp

VertexPtr ConvertGate(
    const Gate & gate
)

Converts a PDAG gate into intermediate cut sets.

Parameters:

gate The target AND/OR gate with arguments.

Return: The root vertex of the ZBDD representing the gate cut sets.

function GetNextGate

cpp

inline int GetNextGate()

Finds a gate in intermediate cut sets.

Return:

The index of the gate in intermediate cut sets.
0 if no gates are found.

Precondition: Variable ordering puts the gate to the top (root).

function ExtractIntermediateCutSets

cpp

VertexPtr ExtractIntermediateCutSets(
    int index
)

Extracts (removes!) intermediate cut sets containing a node with a given index.

Parameters:

index The index of the gate.

Return: The root of the ZBDD containing the intermediate cut sets.

Precondition: Variable ordering puts the gate to the top (root).

Postcondition: The extracted cut sets are pre-processed by removing the vertex with the index of the gate.

function ExpandGate

cpp

VertexPtr ExpandGate(
    const VertexPtr & gate_zbdd,
    const VertexPtr & cut_sets
)

Expands the intermediate ZBDD representation of a gate in intermediate cut sets containing the gate.

Parameters:

gate_zbdd The intermediate ZBDD of the gate.
cut_sets A collection of cut sets.

Return: The root vertex of the resulting ZBDD.

Precondition: The intermediate cut sets are pre-processed by removing the vertex with the index of the gate.

function Merge

cpp

void Merge(
    const VertexPtr & vertex
)

Merges a set of cut sets into the main container.

Parameters:

vertex The root ZBDD vertex representing the cut sets.

Precondition: The argument ZBDD cut sets are managed by this container.

function EliminateComplements

cpp

inline void EliminateComplements()

Eliminates all complements from cut sets.

Precondition: The cut sets have negative literals, i.e., non-coherent.

Postcondition: Sub-modules are not processed.

This can only be done if the cut set generation is certain not to have conflicts.

function EliminateConstantModules

cpp

inline void EliminateConstantModules()

Removes constant modules from cut sets.

Precondition: All modules have been processed.

Constant modules are likely to happen after complement elimination.

function Minimize

cpp

inline void Minimize()

Minimizes cut sets in the container.

Postcondition: Sub-modules are not processed.

function GatherModules

cpp

inline std::map< int, std::pair< bool, int > > GatherModules()

Gathers all module indices in the cut sets.

Return: An unordered map module of indices, coherence, and cut-offs.

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 Log

cpp

void Log()

< Joins fully processed modules.

Updated on 2026-01-09 at 21:59:12 +0000

scram::core::zbdd::CutSetContainer ​

Public Functions ​

Additional inherited members ​

Detailed Description ​

Public Functions Documentation ​

function CutSetContainer ​

function ConvertGate ​

function GetNextGate ​

function ExtractIntermediateCutSets ​

function ExpandGate ​

function Merge ​

function EliminateComplements ​

function EliminateConstantModules ​

function Minimize ​

function GatherModules ​

function JoinModule ​

function Log ​

scram::core::zbdd::CutSetContainer

Public Functions

Additional inherited members

Detailed Description

Public Functions Documentation

function CutSetContainer

function ConvertGate

function GetNextGate

function ExtractIntermediateCutSets

function ExpandGate

function Merge

function EliminateComplements

function EliminateConstantModules

function Minimize

function GatherModules

function JoinModule

function Log