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

#include <CADPreprocessor.h>

Collaboration diagram for smtrat::cad::preprocessor::ResultantRule:
Collaboration graph
[legend]

Public Member Functions

 ResultantRule (Origins &origins, const std::vector< carl::Variable > &vars)
 
std::optional< std::vector< FormulaT > > compute (const std::map< ConstraintT, ConstraintT > &constraints)
 
const auto & getNewECs () const
 

Private Member Functions

bool addPoly (const Poly &poly)
 
bool addPoly (const UPoly &poly, std::size_t level, const std::vector< FormulaT > &origin)
 
std::optional< std::vector< FormulaT > > computeResultants (std::size_t level)
 

Private Attributes

const std::vector< carl::Variable > & mVars
 
std::vector< ConstraintT > mConstraints
 
std::vector< std::vector< UPoly > > mData
 
std::vector< ConstraintT > mNewECs
 
Origins & mOrigins
 

Detailed Description

Definition at line 89 of file CADPreprocessor.h.

Constructor & Destructor Documentation

◆ ResultantRule()

smtrat::cad::preprocessor::ResultantRule::ResultantRule ( Origins &  origins,
const std::vector< carl::Variable > &  vars 
)
inline

Definition at line 102 of file CADPreprocessor.h.

Member Function Documentation

◆ addPoly() [1/2]

bool smtrat::cad::preprocessor::ResultantRule::addPoly ( const Poly &  poly)
private

Definition at line 162 of file CADPreprocessor.cpp.

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

◆ addPoly() [2/2]

bool smtrat::cad::preprocessor::ResultantRule::addPoly ( const UPoly &  poly,
std::size_t  level,
const std::vector< FormulaT > &  origin 
)
private

Definition at line 177 of file CADPreprocessor.cpp.

Here is the call graph for this function:

◆ compute()

std::optional< std::vector< FormulaT > > smtrat::cad::preprocessor::ResultantRule::compute ( const std::map< ConstraintT, ConstraintT > &  constraints)

Definition at line 220 of file CADPreprocessor.cpp.

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

◆ computeResultants()

std::optional< std::vector< FormulaT > > smtrat::cad::preprocessor::ResultantRule::computeResultants ( std::size_t  level)
private

Definition at line 201 of file CADPreprocessor.cpp.

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

◆ getNewECs()

const auto& smtrat::cad::preprocessor::ResultantRule::getNewECs ( ) const
inline

Definition at line 109 of file CADPreprocessor.h.

Here is the caller graph for this function:

Field Documentation

◆ mConstraints

std::vector<ConstraintT> smtrat::cad::preprocessor::ResultantRule::mConstraints
private

Definition at line 92 of file CADPreprocessor.h.

◆ mData

std::vector<std::vector<UPoly> > smtrat::cad::preprocessor::ResultantRule::mData
private

Definition at line 93 of file CADPreprocessor.h.

◆ mNewECs

std::vector<ConstraintT> smtrat::cad::preprocessor::ResultantRule::mNewECs
private

Definition at line 94 of file CADPreprocessor.h.

◆ mOrigins

Origins& smtrat::cad::preprocessor::ResultantRule::mOrigins
private

Definition at line 95 of file CADPreprocessor.h.

◆ mVars

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

Definition at line 91 of file CADPreprocessor.h.

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