SMT-RAT
24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
|
Construct a single open CAD Cell IN A LEVEL-WISE MANNER around a given point that is sign-invariant on a given set of polynomials. More...
Go to the source code of this file.
Data Structures | |
class | smtrat::mcsat::onecellcad::levelwise::LevelwiseCAD |
Namespaces | |
smtrat | |
Class to create the formulas for axioms. | |
smtrat::mcsat | |
smtrat::mcsat::onecellcad | |
smtrat::mcsat::onecellcad::levelwise | |
Construct a single open CAD Cell IN A LEVEL-WISE MANNER around a given point that is sign-invariant on a given set of polynomials.
This is an adaptation of the already existing onecellcad in this project.
References: [brown15] Brown, Christopher W., and Marek Košta. "Constructing a single cell in cylindrical algebraic decomposition." Journal of Symbolic Computation 70 (2015): 14-48. [mccallum84] Scott McCallum. "An Improved Projection Operation for Cylindrical Algebraic Decomposition" Ph.D. Dissertation. 1984. The University of Wisconsin - Madison
Definition in file OneCellCAD.h.