CADData is an object representing a Cylindrical Algebraic Decomposition (CAD).

CADData may be obtained from the context of Quantifier Elimination (QE) by usage of PartialCylindricalAlgebraicDecompose, InsertFormula or DeleteFormula. The latter two routines can take a CADData object as input. A CADData object will be provided when the symbol data appears in the list for the keyword option output (see QuantifierElimination options). CADData will only be returned over QEData when the methodology for QE was purely CAD based (as will be the case when PartialCylindricalAlgebraicDecompose was used). QEData offers similar methods to that of CADData (including the same evolutionary methods).

CADData may be obtained outside of the context of QE by usage of CylindricalAlgebraicDecompose. CADData objects obtained outside of the context of QE do not support QE related methods, as the output would not be well defined.

CADData objects support various methods for querying information about a CAD.

The methodology for CAD in QuantifierElimination is that of a projection and lifting CAD using the Lazard projection. Optimizations owing to equational constraints are of relevance. The PrintProjection method prints information relating to equational constraints where they were used in generation of the CAD.

Various methods for querying properties of CADCells are owned by CADData as it is necessary to query properties of the CADData to ensure the output is well defined for the query.

PrintProjection: prints information about the projection bases for the CAD. Has keyword option verbose which is a truefalse flag determining whether more verbose information should be printed.

GetCells: gets a list of the leaf CADCells for the CAD - see GetCells.

NumberOfLeafCells: gets a nonnegint describing the number of leaf CADCells for the CAD.

TotalCellsCreated: gets a posint of the total number of CADCells created in the course of construction of this CAD.

GetInputFormula: gets a prenex quantified formula equivalent to the input formula for QE when the CADData object was obtained from a QE context.

GetQuantifierFreeEquivalent: gets a formula representing the quantifier free equivalent of the input formula for QE when the CADData object was obtained from a QE context.

PrintInfo: prints verbose information about the CAD represented by the CADData.

InsertFormula: main QuantifierElimination routine offering incrementality for QE - see InsertFormula. The CADData object must be obtained from a QE context.

DeleteFormula: main QuantifierElimination routine offering decrementality for QE - see DeleteFormula. The CADData object must be obtained from a QE context.

SignOfPolynomialOnCell: takes a polynomial over realalgnums and a CADCell, and returns the sign of the polynomial on the cell. The method will warn if the query is not well defined (e.g. the polynomial is not sign invariant on the cell, as its factors are not contained in the projection bases of the CAD).

GetCellContainingPoint: takes a point which is a list(name=realalgnum). The names must be variables of the CAD. Returns a single CADCell which contains the requested point, if it exists. The cell may not exist if the CAD was created with smaller bounds than the whole of real space (lifting constraints - see QuantifierElimination options). The cell may not be unique if the point is underdefined, i.e. contains fewer variables than the number of variables for the CAD.

GetCellDescriptionContainingPoint: takes a point which is a list(name=realalgnum). The names must be variables of the CAD. Returns an extended Tarski formula representing the description of a CADCell containing the requested point. The cell may not exist if the CAD was created with smaller bounds than the whole of real space (lifting constraints - see QuantifierElimination options). The cell description may not be unique if the point is underdefined, i.e. contains fewer variables than the number of variables for the CAD.

The GetCells method was added in Maple 2023 and updated in Maple 2024; see Performance Improvements in Maple 2024.