QEData is an object storing various QE-relevant data structures obtained in the course of QE computation. Its main purpose is to support the evolutionary methodology of the QuantifierElimination routines InsertFormula and DeleteFormula.

There are also some other methods that allow for querying more verbose data about the computations and data structures for the QE.

QEData may be obtained by usage of QuantifierEliminate, InsertFormula, or DeleteFormula. The latter two routines can take a QEData object as input. A QEData object will be provided when the symbol data appears in the list for the keyword option output (see QuantifierElimination options). If only CAD was used for QE, then a CADData object will be returned instead, which offers similar methods to that of QEData (including the same evolutionary methods).

PrintInfo: prints verbose information about the details of the QE associated with this QEData.

GetInputFormula: gets a prenex quantified formula equivalent to the input formula for QE corresponding to this QEData.

GetOutput: allows for regenerating QE output with the usual syntax for defining QE output via QuantifierElimination options. As such, takes a single parameter options which is a list of allowable symbols for QE output.

TotalVTSNodesCreated: gets a posint of the total number of VTS tree nodes created in the course of the QE represented by this QEData.

InsertFormula: main QuantifierElimination routine offering incrementality for QE - see InsertFormula.

DeleteFormula: main QuantifierElimination routine offering decrementality for QE - see DeleteFormula.