smtrat::cad::Preprocessor Class Reference

#include <Preprocessor.h>

Collaboration diagram for smtrat::cad::Preprocessor:

Public Member Functions
	Preprocessor (const std::vector< carl::Variable > &vars)
void	clear ()
void	addConstraint (const ConstraintT &c)
void	removeConstraint (const ConstraintT &c)
bool	preprocess ()
void	postprocessConflict (std::set< FormulaT > &mis) const
const Model &	model () const
const auto &	getConflict () const
FormulaT	simplify (const FormulaT &f) const
template<typename Map >
preprocessor::ConstraintUpdate	result (const Map &oldC) const

Private Types
using	Origins = std::vector< ConstraintT >
using	Trail = std::vector< std::pair< ConstraintT, Origins > >

Private Member Functions
void	apply_assignments (const ConstraintT &c)
void	resolve_conflict ()
carl::Variable	main_variable_of (const ConstraintT &c) const
bool	try_variable_elimination (const ConstraintT &cur)
void	compute_resultants (const ConstraintT &cur)

Private Attributes
const std::vector< carl::Variable > &	mVars
	Variable ordering. More...
std::map< ConstraintT, carl::Variable >	mAssignments
	Origins for the assignments. More...
Model	mModel
	The model used for variable elimination. More...
Trail	mTrail
	The trail. More...
std::size_t	mTrailID = 0
	Next element to be processed. More...
std::set< ConstraintT >	mCurrent
	Current set of equalities. More...
std::optional< std::set< FormulaT > >	mConflict
	A possibly found conflict. More...

Friends
std::ostream &	operator<< (std::ostream &os, const Preprocessor &cadpp)

Detailed Description

Definition at line 43 of file Preprocessor.h.

Member Typedef Documentation

Origins

using smtrat::cad::Preprocessor::Origins = std::vector<ConstraintT>

private

Definition at line 47 of file Preprocessor.h.

Trail

using smtrat::cad::Preprocessor::Trail = std::vector<std::pair<ConstraintT,Origins> >

private

Definition at line 48 of file Preprocessor.h.

Constructor & Destructor Documentation

Preprocessor()

smtrat::cad::Preprocessor::Preprocessor ( const std::vector< carl::Variable > &  vars )

inline

Definition at line 72 of file Preprocessor.h.

Member Function Documentation

addConstraint()

void smtrat::cad::Preprocessor::addConstraint

(

const ConstraintT &

c

)

Definition at line 134 of file Preprocessor.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

apply_assignments()

void smtrat::cad::Preprocessor::apply_assignments ( const ConstraintT &  c )

private

Definition at line 11 of file Preprocessor.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

clear()

void smtrat::cad::Preprocessor::clear ( )

inline

Definition at line 75 of file Preprocessor.h.

Here is the caller graph for this function:

compute_resultants()

void smtrat::cad::Preprocessor::compute_resultants ( const ConstraintT &  cur )

private

Definition at line 110 of file Preprocessor.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

getConflict()

const auto& smtrat::cad::Preprocessor::getConflict ( ) const

inline

Definition at line 91 of file Preprocessor.h.

main_variable_of()

carl::Variable smtrat::cad::Preprocessor::main_variable_of ( const ConstraintT &  c ) const

private

Definition at line 44 of file Preprocessor.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

model()

const Model& smtrat::cad::Preprocessor::model ( ) const

inline

Definition at line 88 of file Preprocessor.h.

postprocessConflict()

void smtrat::cad::Preprocessor::postprocessConflict

(

std::set< FormulaT > &

mis

)

const

Definition at line 199 of file Preprocessor.cpp.

Here is the caller graph for this function:

preprocess()

bool smtrat::cad::Preprocessor::preprocess

(

)

Definition at line 218 of file Preprocessor.cpp.

Here is the call graph for this function:

removeConstraint()

void smtrat::cad::Preprocessor::removeConstraint

(

const ConstraintT &

c

)

Definition at line 141 of file Preprocessor.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

resolve_conflict()

void smtrat::cad::Preprocessor::resolve_conflict ( )

private

Definition at line 37 of file Preprocessor.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

result()

template<typename Map >

preprocessor::ConstraintUpdate smtrat::cad::Preprocessor::result ( const Map &  oldC ) const

inline

Definition at line 100 of file Preprocessor.h.

simplify()

FormulaT smtrat::cad::Preprocessor::simplify ( const FormulaT &  f ) const

inline

Definition at line 95 of file Preprocessor.h.

Here is the call graph for this function:

try_variable_elimination()

bool smtrat::cad::Preprocessor::try_variable_elimination ( const ConstraintT &  cur )

private

Definition at line 53 of file Preprocessor.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

Friends And Related Function Documentation

operator<<

std::ostream& operator<< ( std::ostream &  os, const Preprocessor &  cadpp  )

friend

Definition at line 123 of file Preprocessor.h.

Field Documentation

mAssignments

std::map<ConstraintT,carl::Variable> smtrat::cad::Preprocessor::mAssignments

private

Origins for the assignments.

Definition at line 53 of file Preprocessor.h.

mConflict

std::optional<std::set<FormulaT> > smtrat::cad::Preprocessor::mConflict

private

A possibly found conflict.

Definition at line 63 of file Preprocessor.h.

mCurrent

std::set<ConstraintT> smtrat::cad::Preprocessor::mCurrent

private

Current set of equalities.

Definition at line 61 of file Preprocessor.h.

mModel

Model smtrat::cad::Preprocessor::mModel

private

The model used for variable elimination.

Definition at line 55 of file Preprocessor.h.

mTrail

Trail smtrat::cad::Preprocessor::mTrail

private

The trail.

Definition at line 57 of file Preprocessor.h.

mTrailID

std::size_t smtrat::cad::Preprocessor::mTrailID = 0

private

Next element to be processed.

Definition at line 59 of file Preprocessor.h.

mVars

const std::vector<carl::Variable>& smtrat::cad::Preprocessor::mVars

private

Variable ordering.

Definition at line 51 of file Preprocessor.h.

---

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

• smtrat-cad/utils/Preprocessor.h
• smtrat-cad/utils/Preprocessor.cpp