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

#include <CADElimination.h>

Collaboration diagram for smtrat::qe::cad::CADElimination:
Collaboration graph
[legend]

Public Member Functions

 CADElimination (const FormulaT &quantifierFreePart, const QEQuery &quantifiers)
 
FormulaT eliminateQuantifiers ()
 

Private Types

using TreeIT = CAD< CADSettings >::TreeIterator
 

Private Member Functions

auto & tree ()
 
const auto & tree () const
 
std::vector< TreeIT > collectChildren (const TreeIT &it) const
 
void constructCAD ()
 
void updateCAD (std::vector< Poly > &polynomials)
 
void simplifyCAD ()
 
bool truthBoundaryTest (TreeIT &b, TreeIT &c, TreeIT &d)
 
void computeTruthValues ()
 
void computeSignatures ()
 
bool isProjectionDefinable ()
 
void makeProjectionDefinable ()
 
FormulaT constructImplicant (const TreeIT &sample)
 
FormulaT constructSolutionFormula ()
 
template<typename T >
std::vector< T > computeHittingSet (const std::vector< std::vector< T >> &setOfSets)
 

Private Attributes

FormulaT mQuantifierFreePart
 
std::vector< carl::Variable > mVariables
 
std::vector< ConstraintT > mConstraints
 
std::vector< std::pair< QuantifierType, carl::Variable > > mQuantifiers
 
std::size_t n
 
std::size_t k
 
CAD< CADSettings > mCAD
 
std::map< TreeIT, bool > mTruth
 
std::map< TreeIT, std::vector< carl::Sign > > mSignature
 
std::vector< std::pair< TreeIT, TreeIT > > mCauseConflict
 
std::vector< TreeIT > mTrueSamples
 
std::vector< TreeIT > mFalseSamples
 
FormulasT mAtomicFormulas
 

Detailed Description

Definition at line 35 of file CADElimination.h.

Member Typedef Documentation

◆ TreeIT

using smtrat::qe::cad::CADElimination::TreeIT = CAD<CADSettings>::TreeIterator
private

Definition at line 47 of file CADElimination.h.

Constructor & Destructor Documentation

◆ CADElimination()

smtrat::qe::cad::CADElimination::CADElimination ( const FormulaT &  quantifierFreePart,
const QEQuery &  quantifiers 
)

Definition at line 12 of file CADElimination.cpp.

Here is the call graph for this function:

Member Function Documentation

◆ collectChildren()

std::vector<TreeIT> smtrat::qe::cad::CADElimination::collectChildren ( const TreeIT &  it) const
inlineprivate

Definition at line 65 of file CADElimination.h.

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

◆ computeHittingSet()

template<typename T >
std::vector< T > smtrat::qe::cad::CADElimination::computeHittingSet ( const std::vector< std::vector< T >> &  setOfSets)
private

Definition at line 517 of file CADElimination.cpp.

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

◆ computeSignatures()

void smtrat::qe::cad::CADElimination::computeSignatures ( )
private

Definition at line 252 of file CADElimination.cpp.

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

◆ computeTruthValues()

void smtrat::qe::cad::CADElimination::computeTruthValues ( )
private

Definition at line 215 of file CADElimination.cpp.

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

◆ constructCAD()

void smtrat::qe::cad::CADElimination::constructCAD ( )
private

Definition at line 51 of file CADElimination.cpp.

Here is the caller graph for this function:

◆ constructImplicant()

FormulaT smtrat::qe::cad::CADElimination::constructImplicant ( const TreeIT &  sample)
private

Definition at line 409 of file CADElimination.cpp.

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

◆ constructSolutionFormula()

FormulaT smtrat::qe::cad::CADElimination::constructSolutionFormula ( )
private

Definition at line 450 of file CADElimination.cpp.

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

◆ eliminateQuantifiers()

FormulaT smtrat::qe::cad::CADElimination::eliminateQuantifiers ( )

Definition at line 34 of file CADElimination.cpp.

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

◆ isProjectionDefinable()

bool smtrat::qe::cad::CADElimination::isProjectionDefinable ( )
private

Definition at line 288 of file CADElimination.cpp.

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

◆ makeProjectionDefinable()

void smtrat::qe::cad::CADElimination::makeProjectionDefinable ( )
private

Definition at line 320 of file CADElimination.cpp.

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

◆ simplifyCAD()

void smtrat::qe::cad::CADElimination::simplifyCAD ( )
private

Definition at line 80 of file CADElimination.cpp.

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

◆ tree() [1/2]

auto& smtrat::qe::cad::CADElimination::tree ( )
inlineprivate

Definition at line 58 of file CADElimination.h.

Here is the caller graph for this function:

◆ tree() [2/2]

const auto& smtrat::qe::cad::CADElimination::tree ( ) const
inlineprivate

Definition at line 61 of file CADElimination.h.

◆ truthBoundaryTest()

bool smtrat::qe::cad::CADElimination::truthBoundaryTest ( TreeIT &  b,
TreeIT &  c,
TreeIT &  d 
)
private

Definition at line 190 of file CADElimination.cpp.

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

◆ updateCAD()

void smtrat::qe::cad::CADElimination::updateCAD ( std::vector< Poly > &  polynomials)
private

Definition at line 62 of file CADElimination.cpp.

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

Field Documentation

◆ k

std::size_t smtrat::qe::cad::CADElimination::k
private

Definition at line 43 of file CADElimination.h.

◆ mAtomicFormulas

FormulasT smtrat::qe::cad::CADElimination::mAtomicFormulas
private

Definition at line 56 of file CADElimination.h.

◆ mCAD

CAD<CADSettings> smtrat::qe::cad::CADElimination::mCAD
private

Definition at line 45 of file CADElimination.h.

◆ mCauseConflict

std::vector<std::pair<TreeIT, TreeIT> > smtrat::qe::cad::CADElimination::mCauseConflict
private

Definition at line 52 of file CADElimination.h.

◆ mConstraints

std::vector<ConstraintT> smtrat::qe::cad::CADElimination::mConstraints
private

Definition at line 39 of file CADElimination.h.

◆ mFalseSamples

std::vector<TreeIT> smtrat::qe::cad::CADElimination::mFalseSamples
private

Definition at line 55 of file CADElimination.h.

◆ mQuantifierFreePart

FormulaT smtrat::qe::cad::CADElimination::mQuantifierFreePart
private

Definition at line 37 of file CADElimination.h.

◆ mQuantifiers

std::vector<std::pair<QuantifierType, carl::Variable> > smtrat::qe::cad::CADElimination::mQuantifiers
private

Definition at line 40 of file CADElimination.h.

◆ mSignature

std::map<TreeIT, std::vector<carl::Sign> > smtrat::qe::cad::CADElimination::mSignature
private

Definition at line 50 of file CADElimination.h.

◆ mTrueSamples

std::vector<TreeIT> smtrat::qe::cad::CADElimination::mTrueSamples
private

Definition at line 54 of file CADElimination.h.

◆ mTruth

std::map<TreeIT, bool> smtrat::qe::cad::CADElimination::mTruth
private

Definition at line 49 of file CADElimination.h.

◆ mVariables

std::vector<carl::Variable> smtrat::qe::cad::CADElimination::mVariables
private

Definition at line 38 of file CADElimination.h.

◆ n

std::size_t smtrat::qe::cad::CADElimination::n
private

Definition at line 42 of file CADElimination.h.

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