SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Public Types | Public Member Functions | Protected Types | Protected Attributes
smtrat::InequalitiesTable< Settings > Class Template Reference

Datastructure for the GBModule. More...

#include <InequalitiesTable.h>

Collaboration diagram for smtrat::InequalitiesTable< Settings >:
Collaboration graph
[legend]

Public Types

typedef std::pair< unsigned, Polynomial > CellEntry
 
typedef std::tuple< ModuleInput::iterator, carl::Relation, std::list< CellEntry > > RowEntry
 
typedef std::map< ModuleInput::const_iterator, RowEntry, ModuleInput::IteratorCompare > Rows
 
typedef std::pair< ModuleInput::const_iterator, RowEntry > Row
 
typedef std::map< carl::Variable, std::pair< TermT, carl::BitVector > > RewriteRules
 

Public Member Functions

 InequalitiesTable (GBModule< Settings > *module)
 
Rows::iterator InsertReceivedFormula (ModuleInput::const_iterator received)
 
void pushBacktrackPoint ()
 
void popBacktrackPoint (unsigned nrBacktracks)
 
Answer reduceWRTGroebnerBasis (const Ideal &gb, const RewriteRules &rules)
 
bool reduceWRTGroebnerBasis (typename Rows::iterator, const Ideal &gb, const RewriteRules &rules)
 
Answer reduceWRTGroebnerBasis (const std::list< typename Rows::iterator > &ineqToBeReduced, const Ideal &gb, const RewriteRules &rules)
 
Answer reduceWRTVariableRewriteRules (const RewriteRules &rules)
 
bool reduceWRTVariableRewriteRules (typename Rows::iterator it, const RewriteRules &rules)
 
Answer reduceWRTVariableRewriteRules (const std::list< typename Rows::iterator > &ineqToBeReduced, const RewriteRules &rules)
 
void removeInequality (ModuleInput::const_iterator _formula)
 
void print (std::ostream &os=std::cout) const
 

Protected Types

typedef Settings::PolynomialWithReasons Polynomial
 
typedef Settings::MultivariateIdeal Ideal
 

Protected Attributes

Rows mReducedInequalities
 A map of pointers from received iterators to rows. More...
 
unsigned mBtnumber
 The actual number of backtrackpoints. More...
 
GBModule< Settings > * mModule
 A pointer to the GBModule which uses this table. More...
 
Rows::iterator mNewConstraints
 
unsigned mLastRestart
 

Detailed Description

template<class Settings>
class smtrat::InequalitiesTable< Settings >

Datastructure for the GBModule.

A table of all inequalities and how they are reduced.

Author
Sebastian Junges

Definition at line 24 of file InequalitiesTable.h.

Member Typedef Documentation

◆ CellEntry

template<class Settings >
typedef std::pair<unsigned, Polynomial> smtrat::InequalitiesTable< Settings >::CellEntry

Definition at line 30 of file InequalitiesTable.h.

◆ Ideal

template<class Settings >
typedef Settings::MultivariateIdeal smtrat::InequalitiesTable< Settings >::Ideal
protected

Definition at line 28 of file InequalitiesTable.h.

◆ Polynomial

template<class Settings >
typedef Settings::PolynomialWithReasons smtrat::InequalitiesTable< Settings >::Polynomial
protected

Definition at line 27 of file InequalitiesTable.h.

◆ RewriteRules

template<class Settings >
typedef std::map<carl::Variable, std::pair<TermT, carl::BitVector> > smtrat::InequalitiesTable< Settings >::RewriteRules

Definition at line 34 of file InequalitiesTable.h.

◆ Row

template<class Settings >
typedef std::pair<ModuleInput::const_iterator, RowEntry> smtrat::InequalitiesTable< Settings >::Row

Definition at line 33 of file InequalitiesTable.h.

◆ RowEntry

template<class Settings >
typedef std::tuple<ModuleInput::iterator, carl::Relation, std::list<CellEntry> > smtrat::InequalitiesTable< Settings >::RowEntry

Definition at line 31 of file InequalitiesTable.h.

◆ Rows

template<class Settings >
typedef std::map<ModuleInput::const_iterator, RowEntry, ModuleInput::IteratorCompare> smtrat::InequalitiesTable< Settings >::Rows

Definition at line 32 of file InequalitiesTable.h.

Constructor & Destructor Documentation

◆ InequalitiesTable()

template<class Settings >
smtrat::InequalitiesTable< Settings >::InequalitiesTable ( GBModule< Settings > *  module)

Member Function Documentation

◆ InsertReceivedFormula()

template<class Settings >
Rows::iterator smtrat::InequalitiesTable< Settings >::InsertReceivedFormula ( ModuleInput::const_iterator  received)

◆ popBacktrackPoint()

template<class Settings >
void smtrat::InequalitiesTable< Settings >::popBacktrackPoint ( unsigned  nrBacktracks)

◆ print()

template<class Settings >
void smtrat::InequalitiesTable< Settings >::print ( std::ostream &  os = std::cout) const

◆ pushBacktrackPoint()

template<class Settings >
void smtrat::InequalitiesTable< Settings >::pushBacktrackPoint ( )

◆ reduceWRTGroebnerBasis() [1/3]

template<class Settings >
Answer smtrat::InequalitiesTable< Settings >::reduceWRTGroebnerBasis ( const Ideal &  gb,
const RewriteRules &  rules 
)

◆ reduceWRTGroebnerBasis() [2/3]

template<class Settings >
Answer smtrat::InequalitiesTable< Settings >::reduceWRTGroebnerBasis ( const std::list< typename Rows::iterator > &  ineqToBeReduced,
const Ideal &  gb,
const RewriteRules &  rules 
)

◆ reduceWRTGroebnerBasis() [3/3]

template<class Settings >
bool smtrat::InequalitiesTable< Settings >::reduceWRTGroebnerBasis ( typename Rows::iterator  ,
const Ideal &  gb,
const RewriteRules &  rules 
)

◆ reduceWRTVariableRewriteRules() [1/3]

template<class Settings >
Answer smtrat::InequalitiesTable< Settings >::reduceWRTVariableRewriteRules ( const RewriteRules &  rules)

◆ reduceWRTVariableRewriteRules() [2/3]

template<class Settings >
Answer smtrat::InequalitiesTable< Settings >::reduceWRTVariableRewriteRules ( const std::list< typename Rows::iterator > &  ineqToBeReduced,
const RewriteRules &  rules 
)

◆ reduceWRTVariableRewriteRules() [3/3]

template<class Settings >
bool smtrat::InequalitiesTable< Settings >::reduceWRTVariableRewriteRules ( typename Rows::iterator  it,
const RewriteRules &  rules 
)

◆ removeInequality()

template<class Settings >
void smtrat::InequalitiesTable< Settings >::removeInequality ( ModuleInput::const_iterator  _formula)

Field Documentation

◆ mBtnumber

template<class Settings >
unsigned smtrat::InequalitiesTable< Settings >::mBtnumber
protected

The actual number of backtrackpoints.

Definition at line 41 of file InequalitiesTable.h.

◆ mLastRestart

template<class Settings >
unsigned smtrat::InequalitiesTable< Settings >::mLastRestart
protected

Definition at line 48 of file InequalitiesTable.h.

◆ mModule

template<class Settings >
GBModule<Settings>* smtrat::InequalitiesTable< Settings >::mModule
protected

A pointer to the GBModule which uses this table.

Definition at line 43 of file InequalitiesTable.h.

◆ mNewConstraints

template<class Settings >
Rows::iterator smtrat::InequalitiesTable< Settings >::mNewConstraints
protected

Definition at line 45 of file InequalitiesTable.h.

◆ mReducedInequalities

template<class Settings >
Rows smtrat::InequalitiesTable< Settings >::mReducedInequalities
protected

A map of pointers from received iterators to rows.

Definition at line 39 of file InequalitiesTable.h.

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