SuggestCADOptions - Maple Help
For the best experience, we recommend viewing online help using Google Chrome or Microsoft Edge.

QuantifierElimination[QuantifierTools]

 optimize calling sequence for (Partial)CylindricalAlgebraicDecompose

Parameters

 expr -

Returns

 • Expression sequence with the following three elements:
 – exprout : Rational Tarski Formula, resulting from converting expr to prenex form and removing any constraints recognized as lifting constraints
 – liftingconstraints = cons, where cons is the set of the real lifting constraints removed from expr,
 – opencad = truefalse, value determining whether open CAD is suggested to use

Description

 • Suggests arguments to pass to QuantifierElimination's CylindricalAlgebraicDecompose or PartialCylindricalAlgebraicDecompose command for expr, with the purpose of optimizing the computational efficiency of such a call. This will lead to a (partial) CAD with a smaller number of cells.
 • Usage of lifting constraints and/or open CAD for either command can speed up lifting considerably, so this function can separate out the real lifting constraints (see QuantifierElimination options for definition) from an existentially quantified $\mathrm{And}$, and possibly suggest to use open CAD for formulae that contain no equations or non-strict inequalities.
 • This generates a sequence of arguments amenable to pass to either routine, where that call will then be faster to process.
 • SuggestCADOptions preprocesses expr for a subsequent (partial) CAD. In particular, the input formula is converted to prenex form, and all denominators are removed (see ConvertRationalConstraintsToTarski).

Examples

 > $\mathrm{with}\left(\mathrm{QuantifierElimination}\right):$$\mathrm{with}\left(\mathrm{QuantifierTools}\right)$
 $\left[{\mathrm{AlphaConvert}}{,}{\mathrm{ConvertRationalConstraintsToTarski}}{,}{\mathrm{ConvertToPrenexForm}}{,}{\mathrm{GetAllPolynomials}}{,}{\mathrm{GetEquationalConstraints}}{,}{\mathrm{GetUnquantifiedFormula}}{,}{\mathrm{NegateFormula}}{,}{\mathrm{SuggestCADOptions}}\right]$ (1)
 > $\mathrm{f1}≔\mathrm{exists}\left(\left[y,x\right],\mathrm{And}\left({x}^{2}+{y}^{2}-1=0,{b}^{2}{\left(x-c\right)}^{2}+{a}^{2}{y}^{2}-{a}^{2}{b}^{2}=0,0
 ${\mathrm{f1}}{≔}{\exists }{}\left(\left[{y}{,}{x}\right]{,}{{x}}^{{2}}{+}{{y}}^{{2}}{-}{1}{=}{0}{\wedge }{{b}}^{{2}}{}{\left({x}{-}{c}\right)}^{{2}}{+}{{a}}^{{2}}{}{{y}}^{{2}}{-}{{a}}^{{2}}{}{{b}}^{{2}}{=}{0}{\wedge }{0}{<}{a}{\wedge }{a}{<}{1}{\wedge }{0}{<}{b}{\wedge }{b}{<}{1}{\wedge }{0}{\le }{c}{\wedge }{c}{<}{1}\right)$ (2)
 > $\mathrm{SuggestCADOptions}\left(\mathrm{f1}\right)$
 ${\exists }{}\left(\left[{y}{,}{x}\right]{,}{{x}}^{{2}}{+}{{y}}^{{2}}{-}{1}{=}{0}{\wedge }{{a}}^{{2}}{}{{b}}^{{2}}{-}{{a}}^{{2}}{}{{y}}^{{2}}{-}{{b}}^{{2}}{}{{c}}^{{2}}{+}{2}{}{{b}}^{{2}}{}{c}{}{x}{-}{{b}}^{{2}}{}{{x}}^{{2}}{=}{0}\right){,}{\mathrm{liftingconstraints}}{=}\left\{{-}{c}{\le }{0}{,}{a}{<}{1}{,}{b}{<}{1}{,}{c}{<}{1}{,}{-}{a}{<}{0}{,}{-}{b}{<}{0}\right\}{,}{\mathrm{opencad}}{=}{\mathrm{false}}$ (3)
 > $\mathrm{f2}≔\mathrm{forall}\left(x,0<4{x}^{8}-4\left(L-3\right){x}^{6}-2\left(3L-6\right){x}^{4}-2\left(L-3\right){x}^{2}+1\right)$
 ${\mathrm{f2}}{≔}{\forall }{}\left({x}{,}{0}{<}{4}{}{{x}}^{{8}}{-}{4}{}\left({L}{-}{3}\right){}{{x}}^{{6}}{-}{2}{}\left({3}{}{L}{-}{6}\right){}{{x}}^{{4}}{-}{2}{}\left({L}{-}{3}\right){}{{x}}^{{2}}{+}{1}\right)$ (4)
 > $\mathrm{SuggestCADOptions}\left(\mathrm{f2}\right)$
 ${\forall }{}\left({x}{,}{-}{4}{}{{x}}^{{8}}{+}{4}{}{{x}}^{{6}}{}{L}{-}{12}{}{{x}}^{{6}}{+}{6}{}{{x}}^{{4}}{}{L}{-}{12}{}{{x}}^{{4}}{+}{2}{}{{x}}^{{2}}{}{L}{-}{6}{}{{x}}^{{2}}{<}{1}\right){,}{\mathrm{liftingconstraints}}{=}{\varnothing }{,}{\mathrm{opencad}}{=}{\mathrm{true}}$ (5)

Compatibility

 • The QuantifierElimination:-QuantifierTools:-SuggestCADOptions command was introduced in Maple 2023.
 • For more information on Maple 2023 changes, see Updates in Maple 2023.