SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Public Types | Public Member Functions | Data Fields
smtrat::ICEModule< Settings >::CycleCollector Struct Reference
Collaboration diagram for smtrat::ICEModule< Settings >::CycleCollector:
Collaboration graph
[legend]

Public Types

using Vertex = typename FHG::Vertex
 
using Edge = typename FHG::Edge
 

Public Member Functions

FormulaT buildFormula (const std::vector< Edge > &edges) const
 
std::vector< Vertex > collectAdjacent (const std::vector< Vertex > &vertices, const std::vector< Edge > &edges)
 
bool operator() (const FHG &graph, const std::vector< Vertex > &vertices, const std::vector< Edge > &edges)
 Is called whenever a cycle is found. More...
 

Data Fields

FormulaSetT mInfeasibleSubset
 
std::vector< std::pair< FormulaT, FormulaT > > mLemmas
 

Detailed Description

template<typename Settings>
struct smtrat::ICEModule< Settings >::CycleCollector

Definition at line 56 of file ICEModule.h.

Member Typedef Documentation

◆ Edge

template<typename Settings >
using smtrat::ICEModule< Settings >::CycleCollector::Edge = typename FHG::Edge

Definition at line 58 of file ICEModule.h.

◆ Vertex

template<typename Settings >
using smtrat::ICEModule< Settings >::CycleCollector::Vertex = typename FHG::Vertex

Definition at line 57 of file ICEModule.h.

Member Function Documentation

◆ buildFormula()

template<typename Settings >
FormulaT smtrat::ICEModule< Settings >::CycleCollector::buildFormula ( const std::vector< Edge > &  edges) const
inline

Definition at line 63 of file ICEModule.h.

Here is the caller graph for this function:

◆ collectAdjacent()

template<typename Settings >
std::vector<Vertex> smtrat::ICEModule< Settings >::CycleCollector::collectAdjacent ( const std::vector< Vertex > &  vertices,
const std::vector< Edge > &  edges 
)
inline

Definition at line 68 of file ICEModule.h.

Here is the caller graph for this function:

◆ operator()()

template<typename Settings >
bool smtrat::ICEModule< Settings >::CycleCollector::operator() ( const FHG &  graph,
const std::vector< Vertex > &  vertices,
const std::vector< Edge > &  edges 
)
inline

Is called whenever a cycle is found.

If true is returned, the search for further cycles is aborted.

Definition at line 86 of file ICEModule.h.

Here is the call graph for this function:

Field Documentation

◆ mInfeasibleSubset

template<typename Settings >
FormulaSetT smtrat::ICEModule< Settings >::CycleCollector::mInfeasibleSubset

Definition at line 60 of file ICEModule.h.

◆ mLemmas

template<typename Settings >
std::vector<std::pair<FormulaT,FormulaT> > smtrat::ICEModule< Settings >::CycleCollector::mLemmas

Definition at line 61 of file ICEModule.h.

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