SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Public Member Functions | Private Member Functions | Private Attributes | Friends
smtrat::cad::CADPreprocessor Class Reference

#include <CADPreprocessor.h>

Collaboration diagram for smtrat::cad::CADPreprocessor:
Collaboration graph
[legend]

Public Member Functions

 CADPreprocessor (const std::vector< carl::Variable > &vars)
 
const auto & equalities () const
 
const auto & inequalities () const
 
void addConstraint (const ConstraintT &c)
 
void removeConstraint (const ConstraintT &c)
 
bool preprocess ()
 Performs the preprocessing. More...
 
const Model & model () const
 
template<typename Map >
preprocessor::ConstraintUpdate result (const Map &oldC) const
 
std::set< FormulaT > getConflict () const
 
void postprocessConflict (std::set< FormulaT > &mis) const
 
FormulaT simplify (const FormulaT &f) const
 

Private Member Functions

void resetCached ()
 
void removeEquality (const ConstraintT &c)
 
bool addEqualities (const std::vector< ConstraintT > &constraints)
 
std::vector< ConstraintT > collectDerivedEqualities () const
 
bool collectOriginsOfConflict (std::set< FormulaT > &conflict, const std::map< ConstraintT, ConstraintT > &constraints) const
 Replace constraints that have been modified by its origins in the given conflict. More...
 
bool addModelToConflict (std::set< FormulaT > &conflict, carl::Variables &added) const
 

Private Attributes

Model mModel
 The model used for variable elimination. More...
 
const std::vector< carl::Variable > & mVars
 Variable ordering. More...
 
preprocessor::Origins mOrigins
 Origins of new formulas. More...
 
preprocessor::AssignmentCollector mAssignments
 The assignment collector. More...
 
preprocessor::ResultantRule mResultants
 The resultant rule. More...
 
std::vector< ConstraintT > mEqualities
 Equalities from the input. More...
 
std::map< ConstraintT, ConstraintT > mInequalities
 Inequalities from the input. More...
 
std::map< ConstraintT, ConstraintT > mDerivedEqualities
 Derived set of equalities, essentially mEqualities - mModel. More...
 
std::optional< std::set< FormulaT > > mConflict
 

Friends

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

Detailed Description

Definition at line 121 of file CADPreprocessor.h.

Constructor & Destructor Documentation

◆ CADPreprocessor()

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

Definition at line 158 of file CADPreprocessor.h.

Member Function Documentation

◆ addConstraint()

void smtrat::cad::CADPreprocessor::addConstraint ( const ConstraintT &  c)

Definition at line 315 of file CADPreprocessor.cpp.

Here is the call graph for this function:

◆ addEqualities()

bool smtrat::cad::CADPreprocessor::addEqualities ( const std::vector< ConstraintT > &  constraints)
private

Definition at line 259 of file CADPreprocessor.cpp.

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

◆ addModelToConflict()

bool smtrat::cad::CADPreprocessor::addModelToConflict ( std::set< FormulaT > &  conflict,
carl::Variables &  added 
) const
private

Definition at line 291 of file CADPreprocessor.cpp.

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

◆ collectDerivedEqualities()

std::vector< ConstraintT > smtrat::cad::CADPreprocessor::collectDerivedEqualities ( ) const
private

Definition at line 270 of file CADPreprocessor.cpp.

◆ collectOriginsOfConflict()

bool smtrat::cad::CADPreprocessor::collectOriginsOfConflict ( std::set< FormulaT > &  conflict,
const std::map< ConstraintT, ConstraintT > &  constraints 
) const
private

Replace constraints that have been modified by its origins in the given conflict.

Definition at line 278 of file CADPreprocessor.cpp.

Here is the caller graph for this function:

◆ equalities()

const auto& smtrat::cad::CADPreprocessor::equalities ( ) const
inline

Definition at line 165 of file CADPreprocessor.h.

◆ getConflict()

std::set< FormulaT > smtrat::cad::CADPreprocessor::getConflict ( ) const

Definition at line 396 of file CADPreprocessor.cpp.

Here is the call graph for this function:

◆ inequalities()

const auto& smtrat::cad::CADPreprocessor::inequalities ( ) const
inline

Definition at line 168 of file CADPreprocessor.h.

◆ model()

const Model& smtrat::cad::CADPreprocessor::model ( ) const
inline

Definition at line 181 of file CADPreprocessor.h.

◆ postprocessConflict()

void smtrat::cad::CADPreprocessor::postprocessConflict ( std::set< FormulaT > &  mis) const

Definition at line 404 of file CADPreprocessor.cpp.

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

◆ preprocess()

bool smtrat::cad::CADPreprocessor::preprocess ( )

Performs the preprocessing.

Return false if a direct conflict was found, true otherwise.

Definition at line 339 of file CADPreprocessor.cpp.

Here is the call graph for this function:

◆ removeConstraint()

void smtrat::cad::CADPreprocessor::removeConstraint ( const ConstraintT &  c)

Definition at line 326 of file CADPreprocessor.cpp.

Here is the call graph for this function:

◆ removeEquality()

void smtrat::cad::CADPreprocessor::removeEquality ( const ConstraintT &  c)
private

Definition at line 253 of file CADPreprocessor.cpp.

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

◆ resetCached()

void smtrat::cad::CADPreprocessor::resetCached ( )
private

Definition at line 243 of file CADPreprocessor.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::CADPreprocessor::result ( const Map &  oldC) const
inline

Definition at line 186 of file CADPreprocessor.h.

◆ simplify()

FormulaT smtrat::cad::CADPreprocessor::simplify ( const FormulaT &  f) const
inline

Definition at line 219 of file CADPreprocessor.h.

Here is the call graph for this function:

Friends And Related Function Documentation

◆ operator<<

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

Definition at line 224 of file CADPreprocessor.h.

Field Documentation

◆ mAssignments

preprocessor::AssignmentCollector smtrat::cad::CADPreprocessor::mAssignments
private

The assignment collector.

Definition at line 132 of file CADPreprocessor.h.

◆ mConflict

std::optional<std::set<FormulaT> > smtrat::cad::CADPreprocessor::mConflict
private

Definition at line 144 of file CADPreprocessor.h.

◆ mDerivedEqualities

std::map<ConstraintT, ConstraintT> smtrat::cad::CADPreprocessor::mDerivedEqualities
private

Derived set of equalities, essentially mEqualities - mModel.

Definition at line 141 of file CADPreprocessor.h.

◆ mEqualities

std::vector<ConstraintT> smtrat::cad::CADPreprocessor::mEqualities
private

Equalities from the input.

Definition at line 137 of file CADPreprocessor.h.

◆ mInequalities

std::map<ConstraintT, ConstraintT> smtrat::cad::CADPreprocessor::mInequalities
private

Inequalities from the input.

Definition at line 139 of file CADPreprocessor.h.

◆ mModel

Model smtrat::cad::CADPreprocessor::mModel
private

The model used for variable elimination.

Definition at line 126 of file CADPreprocessor.h.

◆ mOrigins

preprocessor::Origins smtrat::cad::CADPreprocessor::mOrigins
private

Origins of new formulas.

Definition at line 130 of file CADPreprocessor.h.

◆ mResultants

preprocessor::ResultantRule smtrat::cad::CADPreprocessor::mResultants
private

The resultant rule.

Definition at line 134 of file CADPreprocessor.h.

◆ mVars

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

Variable ordering.

Definition at line 128 of file CADPreprocessor.h.

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