smtrat::qe::fm::FourierMotzkinQE Class Reference

#include <FourierMotzkinQE.h>

Collaboration diagram for smtrat::qe::fm::FourierMotzkinQE:

Public Member Functions
	FourierMotzkinQE (const FormulaT &qfree, const QEQuery &quantifiers)
FormulaT	eliminateQuantifiers ()

Private Member Functions
std::pair< matrix_t, vector_t >	eliminateCol (const matrix_t &constraints, const vector_t &constants, std::size_t col, bool conservative=true)
std::pair< matrix_t, vector_t >	eliminateCols (const matrix_t &constraints, const vector_t constants, const std::vector< std::size_t > &cols, bool conservative=true)

Private Attributes
QEQuery	m_query
FormulaT	m_formula
	The quantifiers to eliminate. More...
qe::util::VariableIndex	m_var_idx
	The logical representation of the solution space. More...
FormulaSetT	m_finished

Detailed Description

Definition at line 21 of file FourierMotzkinQE.h.

Constructor & Destructor Documentation

FourierMotzkinQE()

smtrat::qe::fm::FourierMotzkinQE::FourierMotzkinQE ( const FormulaT &  qfree, const QEQuery &  quantifiers  )

inline

Definition at line 29 of file FourierMotzkinQE.h.

Member Function Documentation

eliminateCol()

std::pair< matrix_t, vector_t > smtrat::qe::fm::FourierMotzkinQE::eliminateCol ( const matrix_t &  constraints, const vector_t &  constants, std::size_t  col, bool  conservative = true  )

private

Definition at line 103 of file FourierMotzkinQE.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

eliminateCols()

std::pair< matrix_t, vector_t > smtrat::qe::fm::FourierMotzkinQE::eliminateCols ( const matrix_t &  constraints, const vector_t  constants, const std::vector< std::size_t > &  cols, bool  conservative = true  )

private

Definition at line 155 of file FourierMotzkinQE.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

eliminateQuantifiers()

FormulaT smtrat::qe::fm::FourierMotzkinQE::eliminateQuantifiers

(

)

Definition at line 8 of file FourierMotzkinQE.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

Field Documentation

m_finished

FormulaSetT smtrat::qe::fm::FourierMotzkinQE::m_finished

private

Definition at line 26 of file FourierMotzkinQE.h.

m_formula

FormulaT smtrat::qe::fm::FourierMotzkinQE::m_formula

private

The quantifiers to eliminate.

Definition at line 24 of file FourierMotzkinQE.h.

m_query

QEQuery smtrat::qe::fm::FourierMotzkinQE::m_query

private

Definition at line 23 of file FourierMotzkinQE.h.

m_var_idx

qe::util::VariableIndex smtrat::qe::fm::FourierMotzkinQE::m_var_idx

private

The logical representation of the solution space.

Definition at line 25 of file FourierMotzkinQE.h.

---

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

• smtrat-qe/fm/FourierMotzkinQE.h
• smtrat-qe/fm/FourierMotzkinQE.cpp