smtrat::mcsat::onecellcad::Section Struct Reference

Represent a cell's (closed-interval-boundary) component along th k-th axis. More...

#include <utils.h>

Collaboration diagram for smtrat::mcsat::onecellcad::Section:

Data Fields
MultivariateRootT	boundFunction
RAN	isolatedRoot
	For performance we cache the isolated root from ‘boundFunction’ that lies closest along this section's level to the main point. More...

Detailed Description

Represent a cell's (closed-interval-boundary) component along th k-th axis.

A section is a function f: algReal^{k-1} -> algReal; from a multi-dimensional input point of level k-1 (whose components are algebraic reals) to an algebraic real. We use a root-expression with an irreducible, multivariate polynomial of level k.

Definition at line 231 of file utils.h.

Field Documentation

boundFunction

MultivariateRootT smtrat::mcsat::onecellcad::Section::boundFunction

Definition at line 233 of file utils.h.

isolatedRoot

RAN smtrat::mcsat::onecellcad::Section::isolatedRoot

For performance we cache the isolated root from ‘boundFunction’ that lies closest along this section's level to the main point.

Definition at line 239 of file utils.h.

---

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

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