SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Data Structures | Public Member Functions | Private Types | Private Member Functions | Private Attributes
smtrat::fmplex::FMplexElimination Class Reference

#include <fmplex.h>

Collaboration diagram for smtrat::fmplex::FMplexElimination:
Collaboration graph
[legend]

Data Structures

struct  cmp_row
 

Public Member Functions

 FMplexElimination (const Matrix &m, std::size_t n_quantified, std::size_t n_parameters)
 
Matrix apply ()
 

Private Types

using RowIndex = Matrix::RowIndex
 
using ColIndex = Matrix::ColIndex
 
using RowEntry = Matrix::RowEntry
 
using Row = std::vector< RowEntry >
 

Private Member Functions

ColIndex constant_column () const
 
ColIndex delta_column () const
 
ColIndex origin_column (RowIndex row) const
 
bool is_trivial (const Row &row) const
 
bool is_conflict (const Row &row) const
 
bool is_positive_combination (const Row &row) const
 
bool is_global_conflict (const Row &row) const
 
void collect_constraint (const Row &row)
 
std::vector< Node > split_into_independent_nodes (const Node &n) const
 
Node unbounded_elimination (Node &parent)
 
Node bounded_elimination (Node &parent)
 
bool fm_elimination (Node &parent)
 
Matrix trivial_unsat_matrix () const
 

Private Attributes

std::vector< Node > m_nodes
 
ColIndex m_first_parameter_col
 
ColIndex m_constant_col
 
ColIndex m_total_cols
 
std::set< Row, cmp_row > m_found_rows
 

Detailed Description

Definition at line 12 of file fmplex.h.

Member Typedef Documentation

◆ ColIndex

using smtrat::fmplex::FMplexElimination::ColIndex = Matrix::ColIndex
private

Definition at line 15 of file fmplex.h.

◆ Row

using smtrat::fmplex::FMplexElimination::Row = std::vector<RowEntry>
private

Definition at line 17 of file fmplex.h.

◆ RowEntry

using smtrat::fmplex::FMplexElimination::RowEntry = Matrix::RowEntry
private

Definition at line 16 of file fmplex.h.

◆ RowIndex

using smtrat::fmplex::FMplexElimination::RowIndex = Matrix::RowIndex
private

Definition at line 14 of file fmplex.h.

Constructor & Destructor Documentation

◆ FMplexElimination()

smtrat::fmplex::FMplexElimination::FMplexElimination ( const Matrix &  m,
std::size_t  n_quantified,
std::size_t  n_parameters 
)
inline

Definition at line 44 of file fmplex.h.

Here is the call graph for this function:

Member Function Documentation

◆ apply()

Matrix smtrat::fmplex::FMplexElimination::apply ( )
inline

Definition at line 72 of file fmplex.h.

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

◆ bounded_elimination()

Node smtrat::fmplex::FMplexElimination::bounded_elimination ( Node &  parent)
private

Definition at line 38 of file fmplex.cpp.

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

◆ collect_constraint()

void smtrat::fmplex::FMplexElimination::collect_constraint ( const Row &  row)
inlineprivate

Definition at line 140 of file fmplex.h.

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

◆ constant_column()

ColIndex smtrat::fmplex::FMplexElimination::constant_column ( ) const
inlineprivate

Definition at line 111 of file fmplex.h.

Here is the caller graph for this function:

◆ delta_column()

ColIndex smtrat::fmplex::FMplexElimination::delta_column ( ) const
inlineprivate

Definition at line 112 of file fmplex.h.

Here is the caller graph for this function:

◆ fm_elimination()

bool smtrat::fmplex::FMplexElimination::fm_elimination ( Node &  parent)
private

Definition at line 128 of file fmplex.cpp.

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

◆ is_conflict()

bool smtrat::fmplex::FMplexElimination::is_conflict ( const Row &  row) const
inlineprivate

Definition at line 120 of file fmplex.h.

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

◆ is_global_conflict()

bool smtrat::fmplex::FMplexElimination::is_global_conflict ( const Row &  row) const
inlineprivate

Definition at line 136 of file fmplex.h.

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

◆ is_positive_combination()

bool smtrat::fmplex::FMplexElimination::is_positive_combination ( const Row &  row) const
inlineprivate

Definition at line 127 of file fmplex.h.

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

◆ is_trivial()

bool smtrat::fmplex::FMplexElimination::is_trivial ( const Row &  row) const
inlineprivate

Definition at line 115 of file fmplex.h.

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

◆ origin_column()

ColIndex smtrat::fmplex::FMplexElimination::origin_column ( RowIndex  row) const
inlineprivate

Definition at line 113 of file fmplex.h.

Here is the call graph for this function:

◆ split_into_independent_nodes()

std::vector< Node > smtrat::fmplex::FMplexElimination::split_into_independent_nodes ( const Node &  n) const
private

Definition at line 156 of file fmplex.cpp.

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

◆ trivial_unsat_matrix()

Matrix smtrat::fmplex::FMplexElimination::trivial_unsat_matrix ( ) const
inlineprivate

Definition at line 157 of file fmplex.h.

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

◆ unbounded_elimination()

Node smtrat::fmplex::FMplexElimination::unbounded_elimination ( Node &  parent)
private

Definition at line 5 of file fmplex.cpp.

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

Field Documentation

◆ m_constant_col

ColIndex smtrat::fmplex::FMplexElimination::m_constant_col
private

Definition at line 39 of file fmplex.h.

◆ m_first_parameter_col

ColIndex smtrat::fmplex::FMplexElimination::m_first_parameter_col
private

Definition at line 38 of file fmplex.h.

◆ m_found_rows

std::set<Row, cmp_row> smtrat::fmplex::FMplexElimination::m_found_rows
private

Definition at line 41 of file fmplex.h.

◆ m_nodes

std::vector<Node> smtrat::fmplex::FMplexElimination::m_nodes
private

Definition at line 37 of file fmplex.h.

◆ m_total_cols

ColIndex smtrat::fmplex::FMplexElimination::m_total_cols
private

Definition at line 40 of file fmplex.h.

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