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

#include <AssignmentFinder_ctx.h>

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

Public Member Functions

 AssignmentFinder_ctx (const std::vector< carl::Variable > &var_order, carl::Variable var, const Model &model)
 
bool addConstraint (const FormulaT &f1)
 
bool addMVBound (const FormulaT &f1)
 
Covering computeCover ()
 
AssignmentOrConflict findAssignment ()
 

Private Types

using Polynomial = carl::ContextPolynomial< Rational >
 

Private Member Functions

bool satisfies (const std::variant< carl::BasicConstraint< Polynomial >, carl::VariableComparison< Polynomial >> &f, const typename Polynomial::RootType &r) const
 
bool compare_assignments (std::size_t lhs, std::size_t rhs) const
 
auto select_assignment (const Covering &cover) const
 
bool fits_context (const FormulaT &f)
 

Private Attributes

Polynomial::ContextType m_context
 
carl::Variable m_var
 
carl::Assignment< typename Polynomial::RootType > m_assignment
 
RootIndexer< typename Polynomial::RootType > m_ri
 
std::map< FormulaT, std::pair< std::vector< typename Polynomial::RootType >, std::variant< carl::BasicConstraint< Polynomial >, carl::VariableComparison< Polynomial > > > > m_root_map
 Maps the input formula to the list of real roots and the simplified formula where m_assignment was substituted. More...
 

Detailed Description

Definition at line 24 of file AssignmentFinder_ctx.h.

Member Typedef Documentation

◆ Polynomial

using smtrat::mcsat::arithmetic::AssignmentFinder_ctx::Polynomial = carl::ContextPolynomial<Rational>
private

Definition at line 28 of file AssignmentFinder_ctx.h.

Constructor & Destructor Documentation

◆ AssignmentFinder_ctx()

smtrat::mcsat::arithmetic::AssignmentFinder_ctx::AssignmentFinder_ctx ( const std::vector< carl::Variable > &  var_order,
carl::Variable  var,
const Model &  model 
)
inline

Definition at line 88 of file AssignmentFinder_ctx.h.

Member Function Documentation

◆ addConstraint()

bool smtrat::mcsat::arithmetic::AssignmentFinder_ctx::addConstraint ( const FormulaT &  f1)
inline

Definition at line 94 of file AssignmentFinder_ctx.h.

Here is the call graph for this function:

◆ addMVBound()

bool smtrat::mcsat::arithmetic::AssignmentFinder_ctx::addMVBound ( const FormulaT &  f1)
inline

Definition at line 144 of file AssignmentFinder_ctx.h.

Here is the call graph for this function:

◆ compare_assignments()

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

Definition at line 51 of file AssignmentFinder_ctx.h.

Here is the call graph for this function:

◆ computeCover()

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

Definition at line 187 of file AssignmentFinder_ctx.h.

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

◆ findAssignment()

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

Definition at line 227 of file AssignmentFinder_ctx.h.

Here is the call graph for this function:

◆ fits_context()

bool smtrat::mcsat::arithmetic::AssignmentFinder_ctx::fits_context ( const FormulaT &  f)
inlineprivate

Definition at line 78 of file AssignmentFinder_ctx.h.

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

◆ satisfies()

bool smtrat::mcsat::arithmetic::AssignmentFinder_ctx::satisfies ( const std::variant< carl::BasicConstraint< Polynomial >, carl::VariableComparison< Polynomial >> &  f,
const typename Polynomial::RootType &  r 
) const
inlineprivate

Definition at line 41 of file AssignmentFinder_ctx.h.

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

◆ select_assignment()

auto smtrat::mcsat::arithmetic::AssignmentFinder_ctx::select_assignment ( const Covering &  cover) const
inlineprivate

Definition at line 67 of file AssignmentFinder_ctx.h.

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

Field Documentation

◆ m_assignment

carl::Assignment<typename Polynomial::RootType> smtrat::mcsat::arithmetic::AssignmentFinder_ctx::m_assignment
private

Definition at line 34 of file AssignmentFinder_ctx.h.

◆ m_context

Polynomial::ContextType smtrat::mcsat::arithmetic::AssignmentFinder_ctx::m_context
private

Definition at line 32 of file AssignmentFinder_ctx.h.

◆ m_ri

RootIndexer<typename Polynomial::RootType> smtrat::mcsat::arithmetic::AssignmentFinder_ctx::m_ri
private

Definition at line 35 of file AssignmentFinder_ctx.h.

◆ m_root_map

std::map<FormulaT, std::pair<std::vector<typename Polynomial::RootType>, std::variant<carl::BasicConstraint<Polynomial>, carl::VariableComparison<Polynomial> > > > smtrat::mcsat::arithmetic::AssignmentFinder_ctx::m_root_map
private

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

Definition at line 39 of file AssignmentFinder_ctx.h.

◆ m_var

carl::Variable smtrat::mcsat::arithmetic::AssignmentFinder_ctx::m_var
private

Definition at line 33 of file AssignmentFinder_ctx.h.

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