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

Semantics: The space is divided into a number of intervals: (-oo,a)[a,a](a,b)[b,b](b,oo) A bit is set if the constraints refutes the corresponding interval. More...

#include <Covering.h>

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

Public Member Functions

 Covering (std::size_t intervals)
 
void add (const FormulaT &c, const carl::Bitset &b)
 
bool conflicts () const
 
std::size_t satisfyingInterval () const
 
const auto & satisfyingSamples () const
 
void buildConflictingCore (std::vector< FormulaT > &core) const
 

Private Attributes

std::map< FormulaT, carl::Bitset > mData
 
carl::Bitset mOkay
 

Friends

std::ostream & operator<< (std::ostream &os, const Covering &ri)
 

Detailed Description

Semantics: The space is divided into a number of intervals: (-oo,a)[a,a](a,b)[b,b](b,oo) A bit is set if the constraints refutes the corresponding interval.

Definition at line 19 of file Covering.h.

Constructor & Destructor Documentation

◆ Covering()

smtrat::mcsat::arithmetic::Covering::Covering ( std::size_t  intervals)
inline

Definition at line 25 of file Covering.h.

Member Function Documentation

◆ add()

void smtrat::mcsat::arithmetic::Covering::add ( const FormulaT &  c,
const carl::Bitset &  b 
)
inline

Definition at line 28 of file Covering.h.

Here is the caller graph for this function:

◆ buildConflictingCore()

void smtrat::mcsat::arithmetic::Covering::buildConflictingCore ( std::vector< FormulaT > &  core) const
inline

Definition at line 41 of file Covering.h.

Here is the caller graph for this function:

◆ conflicts()

bool smtrat::mcsat::arithmetic::Covering::conflicts ( ) const
inline

Definition at line 32 of file Covering.h.

Here is the caller graph for this function:

◆ satisfyingInterval()

std::size_t smtrat::mcsat::arithmetic::Covering::satisfyingInterval ( ) const
inline

Definition at line 35 of file Covering.h.

Here is the caller graph for this function:

◆ satisfyingSamples()

const auto& smtrat::mcsat::arithmetic::Covering::satisfyingSamples ( ) const
inline

Definition at line 38 of file Covering.h.

Here is the caller graph for this function:

Friends And Related Function Documentation

◆ operator<<

std::ostream& operator<< ( std::ostream &  os,
const Covering &  ri 
)
friend

Definition at line 59 of file Covering.h.

Field Documentation

◆ mData

std::map<FormulaT, carl::Bitset> smtrat::mcsat::arithmetic::Covering::mData
private

Definition at line 22 of file Covering.h.

◆ mOkay

carl::Bitset smtrat::mcsat::arithmetic::Covering::mOkay
private

Definition at line 23 of file Covering.h.

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