smtrat::mcsat::onecellcad::Sector Struct Reference

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

#include <utils.h>

Data Fields
std::optional< Section >	lowBound
	A std::nullopt lowBound represents negative infinity. More...
std::optional< Section >	highBound
	A std:nullopt highBound represents infinity. More...

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 258 of file utils.h.

Field Documentation

highBound

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

A std:nullopt highBound represents infinity.

Definition at line 263 of file utils.h.

lowBound

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

A std::nullopt lowBound represents negative infinity.

Definition at line 260 of file utils.h.

---

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

• smtrat-mcsat/explanations/onecellcad/utils.h