Represent a cell's open-interval boundary object along one single axis by two irreducible, multivariate polynomials of level k. More...

#include <OpenCAD.h>

Public Member Functions
bool	isLowBoundNegInfty () const

bool	isHighBoundInfty () const

Data Fields
std::optional< Section >	lowBound

std::optional< Section >	highBound

Detailed Description

Represent a cell's open-interval boundary object along one single axis by two irreducible, multivariate polynomials of level k.

A sector is an algebraic/"moving" boundary, because it's basically a function f: algReal^{k-1} -> (algReal,algReal); from a multi-dimensional input point of level k-1 (whose components are algebraic reals) to a pair of algebraic reals (the lower and upper bound for an open interval along k-th axis that changes depending on the input point). Note that if 'lowBound' or 'highBound' is not defined, then this represents negative and positive infinity, respectively.

Definition at line 76 of file OpenCAD.h.

Member Function Documentation

◆ isHighBoundInfty()

bool smtrat::onecellcad::recursive::Sector::isHighBoundInfty ( ) const

inline

Definition at line 85 of file OpenCAD.h.

Here is the caller graph for this function:

◆ isLowBoundNegInfty()

bool smtrat::onecellcad::recursive::Sector::isLowBoundNegInfty ( ) const

inline

Definition at line 81 of file OpenCAD.h.

Here is the caller graph for this function:

Field Documentation

◆ highBound

std::optional<Section> smtrat::onecellcad::recursive::Sector::highBound

Definition at line 79 of file OpenCAD.h.

◆ lowBound

std::optional<Section> smtrat::onecellcad::recursive::Sector::lowBound

Definition at line 77 of file OpenCAD.h.

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

smtrat-mcsat/explanations/onecellcad/recursive/OpenCAD.h

Public Member Functions