OpenCAD.h File Reference

Construct a single open CAD Cell around a given point that is sign-invariant on a given set of polynomials. More...

#include <algorithm>
#include <optional>
#include <set>
#include <unordered_map>
#include <vector>
#include <carl-arith/poly/umvpoly/CoCoAAdaptor.h>
#include <carl-arith/poly/umvpoly/MultivariatePolynomial.h>
#include <carl-arith/poly/umvpoly/functions/Resultant.h>
#include <carl-arith/poly/umvpoly/UnivariatePolynomial.h>
#include <carl-arith/core/Variable.h>
#include <carl-arith/core/VariablePool.h>
#include <carl-arith/ran/ran.h>
#include <carl-arith/ran/RealAlgebraicPoint.h>
#include <smtrat-common/smtrat-common.h>

Include dependency graph for OpenCAD.h:

Go to the source code of this file.

Data Structures
struct	smtrat::onecellcad::recursive::Section
	Represent a cell's closed-interval-boundary object along one single axis by an irreducible, multivariate polynomial of level k. More...
struct	smtrat::onecellcad::recursive::Sector
	Represent a cell's open-interval boundary object along one single axis by two irreducible, multivariate polynomials of level k. More...

Namespaces
	smtrat
	Class to create the formulas for axioms.
	smtrat::onecellcad
	smtrat::onecellcad::recursive

Typedefs
using	smtrat::onecellcad::recursive::UniPoly = carl::UnivariatePolynomial< smtrat::Rational >
using	smtrat::onecellcad::recursive::MultiPoly = carl::MultivariatePolynomial< smtrat::Rational >
using	smtrat::onecellcad::recursive::MultiCoeffUniPoly = carl::UnivariatePolynomial< MultiPoly >
using	smtrat::onecellcad::recursive::RANPoint = RealAlgebraicPoint< smtrat::Rational >
using	smtrat::onecellcad::recursive::RANMap = std::map< carl::Variable, RAN >
using	smtrat::onecellcad::recursive::OpenCADCell = std::vector< Sector >
	Represent a single open cell [1]. More...

Functions
std::ostream &	smtrat::onecellcad::recursive::operator<< (std::ostream &o, const Section &s)
std::ostream &	smtrat::onecellcad::recursive::operator<< (std::ostream &o, const Sector &s)
std::ostream &	smtrat::onecellcad::recursive::operator<< (std::ostream &o, const OpenCADCell &c)
OpenCADCell	smtrat::onecellcad::recursive::createFullspaceCoveringCell (size_t level)
size_t	smtrat::onecellcad::recursive::levelOf (const MultiPoly &poly, const std::vector< carl::Variable > &variableOrder)
	Find the index of the highest variable (wrt. More...
std::map< carl::Variable, RAN >	smtrat::onecellcad::recursive::toStdMap (const RANPoint &point, size_t count, const std::vector< carl::Variable > &variableOrder)
	Create a mapping from the first 'count'-many variables in the given 'variableOrder' to the first 'count'-many components of the given 'point'. More...
std::optional< OpenCADCell >	smtrat::onecellcad::recursive::mergeCellWithPoly (OpenCADCell &cell, const RANPoint &point, const std::vector< carl::Variable > &variableOrder, const MultiPoly poly)
	Merge the given open OpenCADCell 'cell' that contains the given 'point' (called "alpha" in [1]) with a polynomial 'poly'. More...
std::optional< OpenCADCell >	smtrat::onecellcad::recursive::createOpenCADCell (const std::vector< MultiPoly > polySet, const RANPoint &point, const std::vector< carl::Variable > &variableOrder)
	Construct a OpenCADCell for the given set of polynomials 'polySet' that contains the given 'point'. More...

Detailed Description

Construct a single open CAD Cell around a given point that is sign-invariant on a given set of polynomials.

References: [1] Christopher W. Brown. 2013. Constructing a single open cell in a cylindrical algebraic decomposition. In Proceedings of the 38th International Symposium on Symbolic and Algebraic Computation (ISSAC '13). ACM

Definition in file OpenCAD.h.