SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Public Member Functions | Static Public Member Functions | Private Member Functions | Private Attributes | Friends
smtrat::StrategyGraph Class Reference

#include <StrategyGraph.h>

Collaboration diagram for smtrat::StrategyGraph:
Collaboration graph
[legend]

Public Member Functions

 StrategyGraph ()
 
template<typename Module >
BackendLink addBackend (const std::initializer_list< BackendLink > &backends)
 
BackendLink & addEdge (std::size_t from, std::size_t to)
 
std::size_t addRoot (const std::initializer_list< BackendLink > &backends)
 
bool hasBranches () const
 
std::size_t numberOfBranches () const
 
std::size_t getRoot () const
 
std::set< std::pair< thread_priority, AbstractModuleFactory * > > getBackends (std::size_t vertex, const carl::Condition &condition) const
 

Static Public Member Functions

static bool TrueCondition (const carl::Condition &c)
 

Private Member Functions

std::size_t newVertex (std::unique_ptr< AbstractModuleFactory > factory, const std::initializer_list< BackendLink > &backends)
 
std::size_t getPriority (std::size_t priority)
 
void printAsTree (std::ostream &os, std::size_t vertex, std::set< std::size_t > &history, const std::string &indent="") const
 

Private Attributes

std::vector< std::unique_ptr< AbstractModuleFactory > > mVertices
 
std::vector< std::vector< BackendLink > > mEdges
 
bool mHasBranches = false
 
std::size_t mNumberOfBranches = 1
 
std::size_t nextPriority = 1
 
std::size_t mRoot = 0
 

Friends

std::ostream & operator<< (std::ostream &os, const StrategyGraph &sg)
 

Detailed Description

Definition at line 77 of file StrategyGraph.h.

Constructor & Destructor Documentation

◆ StrategyGraph()

smtrat::StrategyGraph::StrategyGraph ( )
inline

Definition at line 124 of file StrategyGraph.h.

Member Function Documentation

◆ addBackend()

template<typename Module >
BackendLink smtrat::StrategyGraph::addBackend ( const std::initializer_list< BackendLink > &  backends)
inline

Definition at line 129 of file StrategyGraph.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ addEdge()

BackendLink& smtrat::StrategyGraph::addEdge ( std::size_t  from,
std::size_t  to 
)
inline

Definition at line 138 of file StrategyGraph.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ addRoot()

std::size_t smtrat::StrategyGraph::addRoot ( const std::initializer_list< BackendLink > &  backends)
inline

Definition at line 145 of file StrategyGraph.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ getBackends()

std::set<std::pair<thread_priority,AbstractModuleFactory*> > smtrat::StrategyGraph::getBackends ( std::size_t  vertex,
const carl::Condition &  condition 
) const
inline

Definition at line 161 of file StrategyGraph.h.

Here is the caller graph for this function:

◆ getPriority()

std::size_t smtrat::StrategyGraph::getPriority ( std::size_t  priority)
inlineprivate

Definition at line 103 of file StrategyGraph.h.

Here is the caller graph for this function:

◆ getRoot()

std::size_t smtrat::StrategyGraph::getRoot ( ) const
inline

Definition at line 157 of file StrategyGraph.h.

Here is the caller graph for this function:

◆ hasBranches()

bool smtrat::StrategyGraph::hasBranches ( ) const
inline

Definition at line 149 of file StrategyGraph.h.

◆ newVertex()

std::size_t smtrat::StrategyGraph::newVertex ( std::unique_ptr< AbstractModuleFactory >  factory,
const std::initializer_list< BackendLink > &  backends 
)
inlineprivate

Definition at line 91 of file StrategyGraph.h.

Here is the caller graph for this function:

◆ numberOfBranches()

std::size_t smtrat::StrategyGraph::numberOfBranches ( ) const
inline

Definition at line 153 of file StrategyGraph.h.

Here is the caller graph for this function:

◆ printAsTree()

void smtrat::StrategyGraph::printAsTree ( std::ostream &  os,
std::size_t  vertex,
std::set< std::size_t > &  history,
const std::string &  indent = "" 
) const
inlineprivate

Definition at line 109 of file StrategyGraph.h.

◆ TrueCondition()

static bool smtrat::StrategyGraph::TrueCondition ( const carl::Condition &  c)
inlinestatic

Definition at line 79 of file StrategyGraph.h.

Here is the caller graph for this function:

Friends And Related Function Documentation

◆ operator<<

std::ostream& operator<< ( std::ostream &  os,
const StrategyGraph &  sg 
)
friend

Definition at line 175 of file StrategyGraph.h.

Field Documentation

◆ mEdges

std::vector<std::vector<BackendLink> > smtrat::StrategyGraph::mEdges
private

Definition at line 85 of file StrategyGraph.h.

◆ mHasBranches

bool smtrat::StrategyGraph::mHasBranches = false
private

Definition at line 86 of file StrategyGraph.h.

◆ mNumberOfBranches

std::size_t smtrat::StrategyGraph::mNumberOfBranches = 1
private

Definition at line 87 of file StrategyGraph.h.

◆ mRoot

std::size_t smtrat::StrategyGraph::mRoot = 0
private

Definition at line 89 of file StrategyGraph.h.

◆ mVertices

std::vector<std::unique_ptr<AbstractModuleFactory> > smtrat::StrategyGraph::mVertices
private

Definition at line 84 of file StrategyGraph.h.

◆ nextPriority

std::size_t smtrat::StrategyGraph::nextPriority = 1
private

Definition at line 88 of file StrategyGraph.h.

The documentation for this class was generated from the following file: