#include <FMplexQE.h>

Collaboration diagram for smtrat::qe::fmplex::FMplexQE:

[legend]

Data Structures
struct	cmp_row

Public Types
using	Matrix = qe::util::Matrix

using	RowIndex = Matrix::RowIndex

using	ColIndex = Matrix::ColIndex

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

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

FormulaT	eliminate_quantifiers ()

Private Member Functions
std::vector< carl::Variable >	gather_elimination_variables () const

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)

FormulaT	constraint_from_row (const Row &row) const

void	collect_constraint (const Row &row)
	truncates the given row to not contain any "origin" information and inserts the result into the set of final projected constraints- This assumes that the row does contain origins and does not contain elimination variables. More...

std::vector< Node >	split_into_independent_nodes (const Node &n) const
	Splits the given node into multiple nodes that are independent in the following sense: More...

void	build_initial_systems ()
	Constructs the starting nodes from m_query and m_formula as follows: More...

Matrix	build_initial_matrix (const FormulasT &constraints)
	Constructs a matrix from the given constraints. More...

Node	unbounded_elimination (Node &parent)
	Eliminates the chosen column in parent by dropping all rows with non-zero entry in that column. More...

Node	bounded_elimination (Node &parent)
	Eliminates the chosen column in parent using the next eliminator in parent. More...

bool	fm_elimination (Node &parent)
	Eliminates the chosen column in parent using Fourier-Motzkin, but discards rows with 0 coeff. More...

void	write_matrix_to_ine (const Matrix &m, const std::string &filename) const
	writes the given qe problem as a .ine file as used in CDD lib. More...

void	write_matrix_to_redlog (const Matrix &m, const std::string &filename) const

Private Attributes
QEQuery	m_query

FormulaT	m_formula

std::vector< Node >	m_nodes

FormulaSetT	m_found_conjuncts

qe::util::VariableIndex	m_var_idx

ColIndex	m_first_parameter_col

std::set< Row, cmp_row >	m_found_rows

Detailed Description

Definition at line 13 of file FMplexQE.h.

Member Typedef Documentation

◆ ColIndex

using smtrat::qe::fmplex::FMplexQE::ColIndex = Matrix::ColIndex

Definition at line 18 of file FMplexQE.h.

◆ Matrix

using smtrat::qe::fmplex::FMplexQE::Matrix = qe::util::Matrix

Definition at line 16 of file FMplexQE.h.

◆ Row

using smtrat::qe::fmplex::FMplexQE::Row = std::vector<Matrix::RowEntry>

Definition at line 19 of file FMplexQE.h.

◆ RowIndex

using smtrat::qe::fmplex::FMplexQE::RowIndex = Matrix::RowIndex

Definition at line 17 of file FMplexQE.h.

Constructor & Destructor Documentation

◆ FMplexQE()

smtrat::qe::fmplex::FMplexQE::FMplexQE	(	const FormulaT &	qfree,
		const QEQuery &	quantifiers
	)

inline

Definition at line 49 of file FMplexQE.h.

Member Function Documentation

◆ bounded_elimination()

Node smtrat::qe::fmplex::FMplexQE::bounded_elimination ( Node & parent )

private

Eliminates the chosen column in parent using the next eliminator in parent.

This eliminator is then erased and added to the ignored rows. Should only be applied if the type of parent is LBS or UBS.

Definition at line 300 of file FMplexQE.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ build_initial_matrix()

FMplexQE::Matrix smtrat::qe::fmplex::FMplexQE::build_initial_matrix ( const FormulasT & constraints )

private

Constructs a matrix from the given constraints.

Each row of the matrix has the form [a_1 ... a_n | a'_1 ... a'_k| b | d | 0 ... 1 ... 0] where

The corresponding constraint is equivalent to (a_1 x_1 + ... + a_n x_n) + (a'_1 y_1 + ... a'_k y_k) + (b + delta*d) <= 0,
x_1,...x_n are the quantified variables, y_1,...,y_k are the parameter variables,
d is 0 if the constraint is weak and 1 if it is strict,
the 0 ... 1 ... 0 part has one entry for each constraint, where the 1 indidicates at which index in the input constraints the corresponding constraint is.

Definition at line 100 of file FMplexQE.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ build_initial_systems()

void smtrat::qe::fmplex::FMplexQE::build_initial_systems ( )

private

Constructs the starting nodes from m_query and m_formula as follows:

Collects the variables in m_query and constraints in m_formula
Uses equations in m_formula to eliminate as many variables as possible
Filters finished constraints from the result
Splits the variables and constraints into independent blocks
Builds a matrix for each block using build_initial_matrix
Adds an according Node for each block to the stack of nodes

Definition at line 188 of file FMplexQE.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ collect_constraint()

void smtrat::qe::fmplex::FMplexQE::collect_constraint ( const Row & row )

inlineprivate

truncates the given row to not contain any "origin" information and inserts the result into the set of final projected constraints- This assumes that the row does contain origins and does not contain elimination variables.

Definition at line 86 of file FMplexQE.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ constant_column()

ColIndex smtrat::qe::fmplex::FMplexQE::constant_column ( ) const

inlineprivate

Definition at line 63 of file FMplexQE.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ constraint_from_row()

FormulaT smtrat::qe::fmplex::FMplexQE::constraint_from_row ( const Row & row ) const

private

Definition at line 80 of file FMplexQE.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ delta_column()

ColIndex smtrat::qe::fmplex::FMplexQE::delta_column ( ) const

inlineprivate

Definition at line 64 of file FMplexQE.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ eliminate_quantifiers()

FormulaT smtrat::qe::fmplex::FMplexQE::eliminate_quantifiers ( )

Definition at line 17 of file FMplexQE.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ fm_elimination()

bool smtrat::qe::fmplex::FMplexQE::fm_elimination ( Node & parent )

private

Eliminates the chosen column in parent using Fourier-Motzkin, but discards rows with 0 coeff.

Should only be called if type of parent is FM, i.e. if only one variable is left to eliminate.

Returns: false if a global conflict is found and true otherwise.

Definition at line 391 of file FMplexQE.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ gather_elimination_variables()

std::vector< carl::Variable > smtrat::qe::fmplex::FMplexQE::gather_elimination_variables ( ) const

private

Definition at line 70 of file FMplexQE.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ is_conflict()

bool smtrat::qe::fmplex::FMplexQE::is_conflict ( const Row & row ) const

inlineprivate

Definition at line 72 of file FMplexQE.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ is_positive_combination()

bool smtrat::qe::fmplex::FMplexQE::is_positive_combination ( const Row & row )

private

Definition at line 290 of file FMplexQE.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ is_trivial()

bool smtrat::qe::fmplex::FMplexQE::is_trivial ( const Row & row ) const

inlineprivate

Definition at line 67 of file FMplexQE.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ origin_column()

ColIndex smtrat::qe::fmplex::FMplexQE::origin_column ( RowIndex row ) const

inlineprivate

Definition at line 65 of file FMplexQE.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ split_into_independent_nodes()

std::vector< Node > smtrat::qe::fmplex::FMplexQE::split_into_independent_nodes ( const Node & n ) const

private

Splits the given node into multiple nodes that are independent in the following sense:

they partition the elimination variables and
the constraints of a node to not contain any of the elimination variables of another node. Thus, these eliminations can be carried out independently.

Definition at line 139 of file FMplexQE.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ unbounded_elimination()

Node smtrat::qe::fmplex::FMplexQE::unbounded_elimination ( Node & parent )

private

Eliminates the chosen column in parent by dropping all rows with non-zero entry in that column.

Should only be applied if the type of parent is NBS, i.e. if the chosen column is unbounded.

Definition at line 255 of file FMplexQE.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ write_matrix_to_ine()

void smtrat::qe::fmplex::FMplexQE::write_matrix_to_ine	(	const Matrix &	m,
		const std::string &	filename
	)		const

private

writes the given qe problem as a .ine file as used in CDD lib.

Definition at line 420 of file FMplexQE.cpp.

Here is the call graph for this function:

◆ write_matrix_to_redlog()

void smtrat::qe::fmplex::FMplexQE::write_matrix_to_redlog	(	const Matrix &	m,
		const std::string &	filename
	)		const

private

Definition at line 455 of file FMplexQE.cpp.

Here is the call graph for this function:

Field Documentation

◆ m_first_parameter_col

ColIndex smtrat::qe::fmplex::FMplexQE::m_first_parameter_col

private

Definition at line 43 of file FMplexQE.h.

◆ m_formula

FormulaT smtrat::qe::fmplex::FMplexQE::m_formula

private

Definition at line 39 of file FMplexQE.h.

◆ m_found_conjuncts

FormulaSetT smtrat::qe::fmplex::FMplexQE::m_found_conjuncts

private

Definition at line 41 of file FMplexQE.h.

◆ m_found_rows

std::set<Row, cmp_row> smtrat::qe::fmplex::FMplexQE::m_found_rows

private

Definition at line 44 of file FMplexQE.h.

◆ m_nodes

std::vector<Node> smtrat::qe::fmplex::FMplexQE::m_nodes

private

Definition at line 40 of file FMplexQE.h.

◆ m_query

QEQuery smtrat::qe::fmplex::FMplexQE::m_query

private

Definition at line 38 of file FMplexQE.h.

◆ m_var_idx

qe::util::VariableIndex smtrat::qe::fmplex::FMplexQE::m_var_idx

private

Definition at line 42 of file FMplexQE.h.

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

smtrat-qe/fmplex/FMplexQE.h
smtrat-qe/fmplex/FMplexQE.cpp

Data Structures

Public Types

Public Member Functions

Private Member Functions

Private Attributes

Detailed Description

Member Typedef Documentation

◆ ColIndex

◆ Matrix

◆ Row

◆ RowIndex

Constructor & Destructor Documentation

◆ FMplexQE()

Member Function Documentation

◆ bounded_elimination()

◆ build_initial_matrix()

◆ build_initial_systems()

◆ collect_constraint()

◆ constant_column()

◆ constraint_from_row()

◆ delta_column()

◆ eliminate_quantifiers()

◆ fm_elimination()

◆ gather_elimination_variables()

◆ is_conflict()

◆ is_positive_combination()

◆ is_trivial()

◆ origin_column()

◆ split_into_independent_nodes()

◆ unbounded_elimination()

◆ write_matrix_to_ine()

◆ write_matrix_to_redlog()

Field Documentation

◆ m_first_parameter_col

◆ m_formula

◆ m_found_conjuncts

◆ m_found_rows

◆ m_nodes

◆ m_query

◆ m_var_idx