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

#include <IntervalPropagation.h>

Collaboration diagram for smtrat::mcsat::icp::IntervalPropagation:
Collaboration graph
[legend]

Public Member Functions

 IntervalPropagation (const std::vector< carl::Variable > &vars, const std::vector< FormulaT > &constraints, const Model &model)
 
std::optional< FormulaT > execute ()
 

Private Member Functions

bool has_contractor_above_threshold () const
 
bool has_interval_below_threshold () const
 
Rational sample_small_rational (const Rational &lower, const Rational &upper, int side) const
 Samples a rational with a small representation size. More...
 
std::pair< bool, double > update_model (carl::Variable v, const std::vector< carl::Interval< double >> &intervals)
 
std::optional< FormulaT > find_excluded_interval (carl::Variable v, const std::vector< carl::Interval< double >> &admissible) const
 
auto construct_direct_conflict (carl::Variable v) const
 
auto construct_interval_conflict (carl::Variable v, const FormulaT &excluded) const
 
void validate_box () const
 

Private Attributes

const Model & mModel
 
std::map< carl::Variable, carl::Interval< double > > mBox
 
std::vector< QueueEntry > mContractors
 
Dependencies mDependencies
 

Static Private Attributes

static constexpr double weight_age = 0.5
 
static constexpr double threshold_priority = 0.1
 
static constexpr double threshold_width = 0.1
 

Detailed Description

Definition at line 20 of file IntervalPropagation.h.

Constructor & Destructor Documentation

◆ IntervalPropagation()

smtrat::mcsat::icp::IntervalPropagation::IntervalPropagation ( const std::vector< carl::Variable > &  vars,
const std::vector< FormulaT > &  constraints,
const Model &  model 
)
inline

Definition at line 205 of file IntervalPropagation.h.

Here is the call graph for this function:

Member Function Documentation

◆ construct_direct_conflict()

auto smtrat::mcsat::icp::IntervalPropagation::construct_direct_conflict ( carl::Variable  v) const
inlineprivate

Definition at line 163 of file IntervalPropagation.h.

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

◆ construct_interval_conflict()

auto smtrat::mcsat::icp::IntervalPropagation::construct_interval_conflict ( carl::Variable  v,
const FormulaT &  excluded 
) const
inlineprivate

Definition at line 168 of file IntervalPropagation.h.

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

◆ execute()

std::optional<FormulaT> smtrat::mcsat::icp::IntervalPropagation::execute ( )
inline

Definition at line 217 of file IntervalPropagation.h.

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

◆ find_excluded_interval()

std::optional<FormulaT> smtrat::mcsat::icp::IntervalPropagation::find_excluded_interval ( carl::Variable  v,
const std::vector< carl::Interval< double >> &  admissible 
) const
inlineprivate

Definition at line 116 of file IntervalPropagation.h.

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

◆ has_contractor_above_threshold()

bool smtrat::mcsat::icp::IntervalPropagation::has_contractor_above_threshold ( ) const
inlineprivate

Definition at line 32 of file IntervalPropagation.h.

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

◆ has_interval_below_threshold()

bool smtrat::mcsat::icp::IntervalPropagation::has_interval_below_threshold ( ) const
inlineprivate

Definition at line 37 of file IntervalPropagation.h.

Here is the caller graph for this function:

◆ sample_small_rational()

Rational smtrat::mcsat::icp::IntervalPropagation::sample_small_rational ( const Rational &  lower,
const Rational &  upper,
int  side 
) const
inlineprivate

Samples a rational with a small representation size.

If side < 0: from (|side+1|*lower + upper)/|side| If side > 0: from (lower + |side-1|*upper)/|side|

Definition at line 49 of file IntervalPropagation.h.

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

◆ update_model()

std::pair<bool,double> smtrat::mcsat::icp::IntervalPropagation::update_model ( carl::Variable  v,
const std::vector< carl::Interval< double >> &  intervals 
)
inlineprivate

Definition at line 70 of file IntervalPropagation.h.

Here is the caller graph for this function:

◆ validate_box()

void smtrat::mcsat::icp::IntervalPropagation::validate_box ( ) const
inlineprivate

Definition at line 175 of file IntervalPropagation.h.

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

Field Documentation

◆ mBox

std::map<carl::Variable, carl::Interval<double> > smtrat::mcsat::icp::IntervalPropagation::mBox
private

Definition at line 23 of file IntervalPropagation.h.

◆ mContractors

std::vector<QueueEntry> smtrat::mcsat::icp::IntervalPropagation::mContractors
private

Definition at line 24 of file IntervalPropagation.h.

◆ mDependencies

Dependencies smtrat::mcsat::icp::IntervalPropagation::mDependencies
private

Definition at line 26 of file IntervalPropagation.h.

◆ mModel

const Model& smtrat::mcsat::icp::IntervalPropagation::mModel
private

Definition at line 22 of file IntervalPropagation.h.

◆ threshold_priority

constexpr double smtrat::mcsat::icp::IntervalPropagation::threshold_priority = 0.1
staticconstexprprivate

Definition at line 29 of file IntervalPropagation.h.

◆ threshold_width

constexpr double smtrat::mcsat::icp::IntervalPropagation::threshold_width = 0.1
staticconstexprprivate

Definition at line 30 of file IntervalPropagation.h.

◆ weight_age

constexpr double smtrat::mcsat::icp::IntervalPropagation::weight_age = 0.5
staticconstexprprivate

Definition at line 28 of file IntervalPropagation.h.

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