SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Public Member Functions | Private Member Functions | Private Attributes
smtrat::mcsat::arithmetic::AssignmentFinder_detail Class Reference

#include <AssignmentFinder_arithmetic.h>

Collaboration diagram for smtrat::mcsat::arithmetic::AssignmentFinder_detail:
Collaboration graph
[legend]

Public Member Functions

 AssignmentFinder_detail (carl::Variable var, const Model &model)
 
bool addConstraint (const FormulaT &f)
 
bool addMVBound (const FormulaT &f)
 
Covering computeCover ()
 
AssignmentOrConflict findAssignment ()
 

Private Member Functions

bool is_univariate (const FormulaT &f) const
 Checks whether a formula is univariate, meaning it contains mVar and only variables from mModel otherwise. More...
 
bool satisfies (const FormulaT &f, const RAN &r) const
 
bool compare_assignments (std::size_t lhs, std::size_t rhs) const
 
ModelValue selectAssignment (const Covering &cover) const
 

Private Attributes

carl::Variable mVar
 
const Model & mModel
 
RootIndexer< typename Poly::RootType > mRI
 
std::map< FormulaT, std::pair< std::vector< RAN >, FormulaT > > mRootMap
 Maps the input formula to the list of real roots and the simplified formula where mModel was substituted. More...
 
std::vector< FormulaT > mMVBounds
 

Detailed Description

Definition at line 19 of file AssignmentFinder_arithmetic.h.

Constructor & Destructor Documentation

◆ AssignmentFinder_detail()

smtrat::mcsat::arithmetic::AssignmentFinder_detail::AssignmentFinder_detail ( carl::Variable  var,
const Model &  model 
)
inline

Definition at line 81 of file AssignmentFinder_arithmetic.h.

Member Function Documentation

◆ addConstraint()

bool smtrat::mcsat::arithmetic::AssignmentFinder_detail::addConstraint ( const FormulaT &  f)
inline

Definition at line 83 of file AssignmentFinder_arithmetic.h.

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

◆ addMVBound()

bool smtrat::mcsat::arithmetic::AssignmentFinder_detail::addMVBound ( const FormulaT &  f)
inline

Definition at line 151 of file AssignmentFinder_arithmetic.h.

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

◆ compare_assignments()

bool smtrat::mcsat::arithmetic::AssignmentFinder_detail::compare_assignments ( std::size_t  lhs,
std::size_t  rhs 
) const
inlineprivate

Definition at line 53 of file AssignmentFinder_arithmetic.h.

Here is the call graph for this function:

◆ computeCover()

Covering smtrat::mcsat::arithmetic::AssignmentFinder_detail::computeCover ( )
inline

Definition at line 193 of file AssignmentFinder_arithmetic.h.

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

◆ findAssignment()

AssignmentOrConflict smtrat::mcsat::arithmetic::AssignmentFinder_detail::findAssignment ( )
inline

Definition at line 260 of file AssignmentFinder_arithmetic.h.

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

◆ is_univariate()

bool smtrat::mcsat::arithmetic::AssignmentFinder_detail::is_univariate ( const FormulaT &  f) const
inlineprivate

Checks whether a formula is univariate, meaning it contains mVar and only variables from mModel otherwise.

Definition at line 31 of file AssignmentFinder_arithmetic.h.

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

◆ satisfies()

bool smtrat::mcsat::arithmetic::AssignmentFinder_detail::satisfies ( const FormulaT &  f,
const RAN &  r 
) const
inlineprivate

Definition at line 42 of file AssignmentFinder_arithmetic.h.

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

◆ selectAssignment()

ModelValue smtrat::mcsat::arithmetic::AssignmentFinder_detail::selectAssignment ( const Covering &  cover) const
inlineprivate

Definition at line 69 of file AssignmentFinder_arithmetic.h.

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

Field Documentation

◆ mModel

const Model& smtrat::mcsat::arithmetic::AssignmentFinder_detail::mModel
private

Definition at line 22 of file AssignmentFinder_arithmetic.h.

◆ mMVBounds

std::vector<FormulaT> smtrat::mcsat::arithmetic::AssignmentFinder_detail::mMVBounds
private

Definition at line 28 of file AssignmentFinder_arithmetic.h.

◆ mRI

RootIndexer<typename Poly::RootType> smtrat::mcsat::arithmetic::AssignmentFinder_detail::mRI
private

Definition at line 23 of file AssignmentFinder_arithmetic.h.

◆ mRootMap

std::map<FormulaT, std::pair<std::vector<RAN>, FormulaT> > smtrat::mcsat::arithmetic::AssignmentFinder_detail::mRootMap
private

Maps the input formula to the list of real roots and the simplified formula where mModel was substituted.

Definition at line 27 of file AssignmentFinder_arithmetic.h.

◆ mVar

carl::Variable smtrat::mcsat::arithmetic::AssignmentFinder_detail::mVar
private

Definition at line 21 of file AssignmentFinder_arithmetic.h.

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