smtrat::fmplex Namespace Reference

Data Structures
struct	VariableIndex
class	FMplexElimination
class	Matrix
struct	Node

Typedefs
using	Poly = carl::MultivariatePolynomial< Rational >
using	Formula = carl::Formula< carl::MultivariatePolynomial< Rational > >
using	EigenMat = Eigen::Matrix< Rational, Eigen::Dynamic, Eigen::Dynamic >
using	EigenVec = Eigen::Matrix< Rational, Eigen::Dynamic, 1 >
using	Rational = mpq_class

Functions
Formula	eliminate_variables (const Formula &f, const std::vector< carl::Variable > &vars)
std::pair< EigenMat, EigenVec >	eliminate_cols (const EigenMat &constraints, const EigenVec &constants, const std::vector< std::size_t > &cols)
void	write_matrix_to_ine (const EigenMat &constraints, const EigenVec &constants, const std::vector< std::size_t > &cols, const std::string &filename)
void	gcd_normalize (std::vector< typename Matrix::RowEntry > &row)

Typedef Documentation

EigenMat

using smtrat::fmplex::EigenMat = typedef Eigen::Matrix<Rational, Eigen::Dynamic, Eigen::Dynamic>

Definition at line 17 of file eliminate.h.

EigenVec

using smtrat::fmplex::EigenVec = typedef Eigen::Matrix<Rational, Eigen::Dynamic, 1>

Definition at line 18 of file eliminate.h.

Formula

using smtrat::fmplex::Formula = typedef carl::Formula<carl::MultivariatePolynomial<Rational> >

Definition at line 16 of file eliminate.h.

Poly

using smtrat::fmplex::Poly = typedef carl::MultivariatePolynomial<Rational>

Definition at line 38 of file eliminate.cpp.

Rational

using smtrat::fmplex::Rational = typedef mpq_class

Definition at line 7 of file Matrix.h.

Function Documentation

eliminate_cols()

std::pair< EigenMat, EigenVec > smtrat::fmplex::eliminate_cols	(	const EigenMat &	constraints,
		const EigenVec &	constants,
		const std::vector< std::size_t > &	cols
	)

Definition at line 125 of file eliminate.cpp.

Here is the call graph for this function:

eliminate_variables()

Formula smtrat::fmplex::eliminate_variables	(	const Formula &	f,
		const std::vector< carl::Variable > &	vars
	)

Definition at line 41 of file eliminate.cpp.

Here is the call graph for this function:

gcd_normalize()

void smtrat::fmplex::gcd_normalize ( std::vector< typename Matrix::RowEntry > &  row )

inline

Definition at line 212 of file Matrix.h.

Here is the call graph for this function:

Here is the caller graph for this function:

write_matrix_to_ine()

void smtrat::fmplex::write_matrix_to_ine	(	const EigenMat &	constraints,
		const EigenVec &	constants,
		const std::vector< std::size_t > &	cols,
		const std::string &	filename
	)

Definition at line 169 of file eliminate.cpp.

Here is the call graph for this function: