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

Represents the delineation of a set of polynomials (at a sample), that is. More...

#include <delineation.h>

Public Member Functions

const auto & roots () const
 Returns the underlying root map, which is a set of real algebraic numbers to indexed root expressions. More...
 
const auto & nullified () const
 The set of nullified polynomials. More...
 
const auto & nonzero () const
 The set of polynomials without roots. More...
 
bool empty () const
 
auto delineate_cell (const RAN &sample) const
 Computes the bounds of the interval around the given sample w.r.t. More...
 
void add_root (RAN root, TaggedIndexedRoot tagged_root)
 
void remove_root (RAN root, TaggedIndexedRoot tagged_root)
 
void remove_roots_with_origin (RAN root, PolyRef origin, bool only_optional=false)
 
void add_poly_nonzero (PolyRef poly)
 
void add_poly_nullified (PolyRef poly)
 
void merge_with (const Delineation &other)
 

Private Attributes

RootMap m_roots
 A map from the actual roots to indexed root expressions. Note that this map is sorted. More...
 
boost::container::flat_set< PolyRef > m_polys_nullified
 The set of all nullified polynomials. More...
 
boost::container::flat_set< PolyRef > m_polys_nonzero
 The set of all polynomials without a root. More...
 

Friends

class DelineationInterval
 

Detailed Description

Represents the delineation of a set of polynomials (at a sample), that is.

  • the ordering of all roots,
  • the set of nullified polynomials,
  • the set of polynomials without a root.

Definition at line 118 of file delineation.h.

Member Function Documentation

◆ add_poly_nonzero()

void smtrat::cadcells::datastructures::Delineation::add_poly_nonzero ( PolyRef  poly)
inline

Definition at line 234 of file delineation.h.

Here is the caller graph for this function:

◆ add_poly_nullified()

void smtrat::cadcells::datastructures::Delineation::add_poly_nullified ( PolyRef  poly)
inline

Definition at line 238 of file delineation.h.

Here is the caller graph for this function:

◆ add_root()

void smtrat::cadcells::datastructures::Delineation::add_root ( RAN  root,
TaggedIndexedRoot  tagged_root 
)
inline

Definition at line 206 of file delineation.h.

Here is the caller graph for this function:

◆ delineate_cell()

auto smtrat::cadcells::datastructures::Delineation::delineate_cell ( const RAN &  sample) const
inline

Computes the bounds of the interval around the given sample w.r.t.

this delineation.

Definition at line 154 of file delineation.h.

Here is the caller graph for this function:

◆ empty()

bool smtrat::cadcells::datastructures::Delineation::empty ( ) const
inline

Definition at line 147 of file delineation.h.

Here is the caller graph for this function:

◆ merge_with()

void smtrat::cadcells::datastructures::Delineation::merge_with ( const Delineation &  other)
inline

Definition at line 242 of file delineation.h.

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

◆ nonzero()

const auto& smtrat::cadcells::datastructures::Delineation::nonzero ( ) const
inline

The set of polynomials without roots.

Definition at line 144 of file delineation.h.

Here is the caller graph for this function:

◆ nullified()

const auto& smtrat::cadcells::datastructures::Delineation::nullified ( ) const
inline

The set of nullified polynomials.

Definition at line 138 of file delineation.h.

Here is the caller graph for this function:

◆ remove_root()

void smtrat::cadcells::datastructures::Delineation::remove_root ( RAN  root,
TaggedIndexedRoot  tagged_root 
)
inline

Definition at line 220 of file delineation.h.

Here is the caller graph for this function:

◆ remove_roots_with_origin()

void smtrat::cadcells::datastructures::Delineation::remove_roots_with_origin ( RAN  root,
PolyRef  origin,
bool  only_optional = false 
)
inline

Definition at line 226 of file delineation.h.

Here is the caller graph for this function:

◆ roots()

const auto& smtrat::cadcells::datastructures::Delineation::roots ( ) const
inline

Returns the underlying root map, which is a set of real algebraic numbers to indexed root expressions.

Definition at line 132 of file delineation.h.

Here is the caller graph for this function:

Friends And Related Function Documentation

◆ DelineationInterval

friend class DelineationInterval
friend

Definition at line 119 of file delineation.h.

Field Documentation

◆ m_polys_nonzero

boost::container::flat_set<PolyRef> smtrat::cadcells::datastructures::Delineation::m_polys_nonzero
private

The set of all polynomials without a root.

Definition at line 126 of file delineation.h.

◆ m_polys_nullified

boost::container::flat_set<PolyRef> smtrat::cadcells::datastructures::Delineation::m_polys_nullified
private

The set of all nullified polynomials.

Definition at line 124 of file delineation.h.

◆ m_roots

RootMap smtrat::cadcells::datastructures::Delineation::m_roots
private

A map from the actual roots to indexed root expressions. Note that this map is sorted.

Definition at line 122 of file delineation.h.

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