Demonstration of the QuantifierElimination and QuantifierTools packages in Maple
>
|
with( QuantifierElimination );
|
| (1) |
>
|
with( QuantifierTools );
|
| (2) |
This worksheet is an in-depth demonstration of ways to use the routines of QuantifierElimination and QuantifierTools.
Throughout, QE and CAD are abbreviations of Quantifier Elimination and Cylindrical Algebraic Decomposition, respectively.
It also offers a wealth of typical examples on how to interact with QEData and CADData objects returned in the course of incrementality or stock CAD.
QE or CAD formulae as examples that originally have an academic source are appended with a reference on formula definition (generally [3] or [9]). Both works are either repositories of data or works that cite a repository of data. Other references appended at the bottom of the worksheet are general major works of interest in terms of implementation of the QuantifierElimination package. An extremely comprehensive source of reference for the package and in particular its implementation is [8].
|
Quantifier Elimination & Tarski formulae
|
|
Below demonstrates some general usage of the package, in particular in terms of what to expect from QuantifierEliminate in terms of input syntax for formulae. By default, when no keyword options are used, the quantifier-free equivalent of a formula is returned.
>
|
expr := exists( [ x, y ], And( 3*x^2 - 2*y > 0, Or( x > 0, y > 0 ) ) );
|
| (1.1) |
>
|
QuantifierEliminate( expr );
|
>
|
expr := exists( x, forall( y, exists( z, And(4*x^2 + x*y^2 - z + 1/4 = 0, 2*x + y^2*z + 1/2 = 0, x^2*z - 1/2*x - y^2 = 0 ) ) ) );
|
| (1.3) |
>
|
QuantifierEliminate( expr );
|
Generic boolean operators such as Implies are supported. Under the hood, QuantifierElimination routines work with 'prenex' formulae only.
>
|
expr := Implies( forall( x, x > 0 ), x^2 > 0 );
|
| (1.5) |
>
|
QuantifierEliminate( expr );
|
The conversion to prenex form can be realized by the QuantifierTools routine ConvertToPrenexForm.
>
|
prenexExpr := ConvertToPrenexForm( expr );
|
| (1.7) |
>
|
QuantifierEliminate( prenexExpr );
|
QuantifierEliminate accepts formulae involving rational functions:
>
|
expr := exists( x, x / y > 0 );
|
| (1.9) |
>
|
QuantifierEliminate( expr );
|
These rational functions are interpreted in terms of equivalent Tarski formulae under the hood. This conversion is realizable by the QuantifierTools routine ConvertRationalConstraintsToTarski:
>
|
ConvertRationalConstraintsToTarski( expr );
|
|
|
Witnesses for QE [5] on fully quantified formulae [3], relation to Satisfiability Modulo Theories (SMT)
|
|
For formulae where every variable is quantified in terms of exactly one quantifier symbol, the quantifier-free equivalent of the formula must be identically 'true' or 'false'.
>
|
expr := exists([v__1, v__2, v__3, v__4, v__5, v__6, v__7, v__8],And(v__7 < 0,0 < v__8,0
< v__4,v__2*v__6+v__3*v__8 = v__4,v__1*v__5+v__3*v__7 = v__4,v__6 = 1,v__5 = 1,
0 < v__1)); # [3], Economics QE example 0001
|
| (2.1) |
>
|
QuantifierEliminate( expr );
|
In the scenario where a formula is equivalent to 'true' in the existentially quantified case, or 'false' in the universally quantified case, there exists a set of assignments of the quantified variables to real algebraic numbers that realizes the equivalence of the quantified formula to its quantifier-free equivalent. This is called a set of 'witnesses'. Witnesses can be requested as an output argument by including the symbol 'witnesses' as part of the list for the keyword option 'output':
>
|
( q, w ) := QuantifierEliminate( expr, 'output = [ qf, witnesses]' ); # provide some witnesses for proof of the example
|
| (2.3) |
| (2.4) |
>
|
map( evalb@eval, GetUnquantifiedFormula( expr ), wit ); # the witnesses work
|
| (2.5) |
>
|
# evalb@eval composition of evalb with eval
|
>
|
( q, w ) := QuantifierEliminate( expr, 'output = [ qf, witnesses ]', 'processwitnesses' = false );
|
| (2.6) |
Satisfy from the SMTLIB package offers similar functionality when judging the unquantified part of the quantified formula to be an SMT formula under the theory of real arithmetic.
>
|
exprUnq := GetUnquantifiedFormula( expr );
|
| (2.7) |
>
|
SMTWitnesses := SMTLIB:-Satisfy( exprUnq );
|
| (2.8) |
>
|
map( evalb@eval, exprUnq, convert( SMTWitnesses, 'list' ) );
|
| (2.9) |
Usage of a low value for the 'eagerness' keyword option can provide a more comprehensive set of witnesses at the cost of more exploration of the solution space by the QE algorithm(s) used.
>
|
( q, w ) := QuantifierEliminate( expr, 'output = [ qf, witnesses ]', 'eagerness' = 1 ): # get a covering of all possible witnesses
q;
map(print, w):
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| (2.10) |
>
|
for wit in w do # all witness results work
map( evalb@eval, GetUnquantifiedFormula( expr ), wit[ 2.. -1 ] );
end do;
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| (2.11) |
Exploring a universally quantified problem equivalent to false provides the same functionality:
>
|
expr := forall([v__1, v__2, v__3, v__4, v__5, v__6, v__7, v__8],Implies(And(v__7 < 0,0
< v__8,0 < v__4,v__2*v__6+v__3*v__8 = v__4,v__1*v__5+v__3*v__7 = v__4,v__6 = 1,
v__5 = 1),0 < v__1)); # [3], Economics QE theorem 0001
|
| (2.12) |
>
|
( q, w ) := QuantifierEliminate( expr, 'output = [ qf, witnesses ]' );
|
| (2.13) |
>
|
map( evalb@eval, ConvertToPrenexForm( GetUnquantifiedFormula( expr ) ), w[][ 2.. -1 ] );
|
| (2.14) |
QE specifically requested by CAD using PartialCylindricalAlgebraicDecompose offers the same functionality as QuantifierEliminate.
>
|
( q, w, data ) := PartialCylindricalAlgebraicDecompose( expr, 'output = [ qf, witnesses, data ]', 'eagerness = 1' ); # CAD provides the same functionality
|
| (2.15) |
>
|
map( evalb@eval, ConvertToPrenexForm( GetUnquantifiedFormula( expr ) ), w[2][ 2.. -1 ] );
|
| (2.16) |
|
|
Full incrementality for QE [1,2,4] & homogeneously quantified problems
|
|
QuantifierElimination offers the opportunity to perform QE in an entirely 'evolutionary' fashion. The word 'evolutionary' is roughly synonymous with the word 'incrementality' usually used in academic literature for QE in this context.
This means that solution of a QE problem can be performed incrementally in terms of intermediate formulae, reusing returned data structures to make successive calls adding extra parts of the formula more performant. In this way, if an intermediate quantified formula is equivalent to a fixed point (such as 'true' or 'false'), one can terminate computation early without needing to perform successive calls with extra parts of the formula.
More generally, incrementality allows for more granular and powerful inspection of quantified formulae.
The term 'evolutionary' is intended to make the definition of 'incrementality' less loose—the InsertFormula and DeleteFormula routines in QuantifierElimination strictly correspond to incrementality (addition of data to a previous formula) and decrementality (removal of data from a previous formula).
>
|
expr := forall( x, Implies( x > 0, x^2 > 0 ) );
|
| (3.1) |
>
|
forall( x, Implies( x >= 0, x^2 > 0 ) );
|
>
|
ConvertToPrenexForm( expr );
|
| (3.3) |
With a formula in prenex form, one can explore manipulation of the formula from a QE perspective. Note that the symbol 'data' must appear in the list requested for output via the keyword option 'output'. The QEData object returned contains the data structures necessary to enable further evolutionary operations via InsertFormula and DeleteFormula.
>
|
( q, w, data ) := QuantifierEliminate( expr, 'output = [ qf, witnesses, data ]' );
|
| (3.4) |
Perform QE with the operand of the quantified formula at atomic position 1 removed. In other words, we consider a change to the originally quantified formula such that 0 <= -x is removed.
Atomic positions simply refer to the position of an operand of a formula in terms of traversal of the formula as a DAG.
>
|
( q, w, data ) := DeleteFormula( data, 1, 'output = [ qf, witnesses, data ]' );
|
| (3.5) |
Having removed the operand 0 <= -x, we now investigate its replacement with the atomic formula x < 0. In terms of the original formula featuring the Implies symbol, the quantified formula below is equivalent to Implies( 0 <= x, 0 < x^2 ), which should be false, because of x = 0.
InsertFormula requires an operand corresponding to 'And' or 'Or', as more generally one can "build" a new disjunction or conjunction at an atomic position in usage of this parameter. Here, we are essentially rebuilding the disjunction which we lost as of the last call.
>
|
( q, w, data ) := InsertFormula( data, 'Or', 1, x < 0, 'output = [ qf, witnesses, data ]' );
|
| (3.6) |
Formulae which are "SMT-like" in the sense they have many variables which are all quantified with the same symbol, and are essentially a large conjunction of formulae (i.e. the formula is in conjunctive normal form) admit usage of this incrementality very well.
>
|
expr := exists([v__1, v__2, v__3, v__4, v__5, v__6, v__7, v__8],And(v__2 = v__1,v__3*
v__5+v__4*v__7 = v__1,v__3*v__6+v__4*v__7 = v__1,v__3*v__6+v__4*v__8 = v__2,0 <
v__3,0 < v__4,v__6 < v__5,v__7 < v__8)); # [3], Economics QE example 0018
|
| (3.7) |
Eliminate the quantifiers without incrementality:
>
|
QuantifierEliminate( expr );
|
To instead perform QE incrementally in terms of the operands of the formula, start with the quantified formula corresponding to quantification of just the first operand:
>
|
exprIn := op( 0, expr )( op( 1, expr ), op( [ 2, 1 ], expr ) );
|
| (3.9) |
>
|
( q, w, data ) := QuantifierEliminate( exprIn, 'output = [ qf, witnesses, data ]' );
|
| (3.10) |
One can then do a loop to successively add in the further operands from the formula. If the quantified formula we are building is ever equivalent 'false', no addition of further operands will make the formula 'true' due to the conjunctive nature of the formula.
>
|
for i from 2 to nops( op( 2, expr ) ) do
print( op( [ 2, i ], expr ) );
( q, w, data ) := InsertFormula( data, ':-And', i, op( [ 2, i ], expr ), 'output = [ qf, witnesses, data ]' );
if q then
print( map( is, eval( ':-And'( op( [ 2, 1 .. i ], expr ) ), w[ 1 ][ 2 .. -1 ] ) ) );
end if;
until not q;
|
| |
| |
| |
| |
| |
| |
| (3.11) |
In this case, the formula is actually equivalent to false without usage of all the operands. The unsatisfiable core of the formula is smaller than the set of all the operands.
>
|
i, op( [ 2, i ], expr ), op( [ 2, -1 ], expr ); # the clause where we obtained 'false', and the last clause
|
| (3.13) |
Using DeleteFormula, we can "go backwards" to remove operands (remove them from the opposite side we were appending to):
>
|
do
print( op( [ 2, j ], expr ) );
( q, w, data ) := DeleteFormula( data, 1, 'output = [ qf, witnesses, data ]' );
j++;
if q then
print( map( is, eval( ':-And'( op( [ 2, j .. i ], expr ) ), w[ 1 ][ 2 .. -1 ] ) ) );
end if;
until j = nops( op( 2, expr ) ) - 1; # note these deletions happen in reverse order, ie. we're deleting the clause we started with first
|
| |
| |
| |
| |
| |
| |
Investigate a similar occurrence but using a universally quantified formula. Note that witnesses are always being requested, and are kept up to date with the current state of the quantifier-free equivalent for the formula.
>
|
expr := exists([v__1, v__2, v__3, v__4, v__5, v__6, v__7, v__8],And(v__2 = v__1,v__3*
v__5+v__4*v__7 = v__1,v__3*v__6+v__4*v__7 = v__1,v__3*v__6+v__4*v__8 = v__2,0 <
v__3,0 < v__4,v__6 < v__5,v__7 < v__8)); # [3], Economics QE theorem 0001
|
| (3.16) |
>
|
( q, w, data ) := QuantifierEliminate( expr, 'output = [ qf, witnesses, data ]' );
|
| (3.17) |
>
|
( q, w, data ) := DeleteFormula( data, 1, 'output = [ qf, witnesses, data ]' ); # delete -v__7 <= 0
|
| (3.18) |
>
|
( q, w, data ) := InsertFormula( data, 'Or', 1, -v__7 < 0, 'output = [ qf, witnesses, data ]' ); # insert v__7 < 0
|
| (3.19) |
>
|
( q, w, data ) := DeleteFormula( data, 1, 'output = [ qf, witnesses, data ]' ); # delete v__7 < 0
|
| (3.20) |
>
|
( q, w, data ) := DeleteFormula( data, 1, 'output = [ qf, witnesses, data ]' ); # delete v__8 <= 0
|
| (3.21) |
>
|
( q, w, data ) := DeleteFormula( data, 1, 'output = [ qf, witnesses, data ]' ); # delete v__4 <= 0
|
| (3.22) |
>
|
( q, w, data ) := DeleteFormula( data, 3, 'output = [ qf, witnesses, data ]' ); # delete -1 + v__5 <> 0
|
| (3.23) |
>
|
( q, w, data ) := DeleteFormula( data, 3, 'output = [ qf, witnesses, data ]' ); # delete -v__1 < 0
|
| (3.24) |
>
|
expr := exists([v__1, v__2, v__3, v__4, v__5, v__6, v__7, v__8],And(v__2 = v__1,v__3*
v__5+v__4*v__7 = v__1,v__3*v__6+v__4*v__7 = v__1,v__3*v__6+v__4*v__8 = v__2,0 <
v__3,0 < v__4,v__6 < v__5,v__7 < v__8)); # [3], Economics QE example 0018
|
| (3.25) |
>
|
( q, w, data ) := QuantifierEliminate( expr, 'output = [ qf, witnesses, data ]' );
|
| (3.26) |
>
|
( q, w, data ) := DeleteFormula( data, 6, 'output = [ qf, witnesses, data ]' ); # delete -v__4 < 0
|
| (3.27) |
>
|
( q, w, data ) := DeleteFormula( data, 5, 'output = [ qf, witnesses, data ]' ); # delete -v__3 < 0
|
| (3.28) |
>
|
( q, w, data ) := InsertFormula( data, 'And', 5, -v__3 <= 0, 'output = [ qf, witnesses, data ]' ); # insert -v__3 <= 0
|
| (3.29) |
>
|
( q, w, data ) := InsertFormula( data, 'And', 6, -v__4 <= 0, 'output = [ qf, witnesses, data ]' ); # insert -v__4 <= 0
|
| (3.30) |
Get the current corresponding quantified formula for the QEData in terms of the evolutionary operations performed:
>
|
expr := GetInputFormula( data );
|
| (3.31) |
Check the current witnesses are correct:
>
|
map( is@eval, ConvertToPrenexForm( GetUnquantifiedFormula( expr ) ), w[1][2..-1] );
|
| (3.32) |
>
|
map( eval, ConvertToPrenexForm( GetUnquantifiedFormula( expr ) ), w[1][2..-1] );
|
| (3.33) |
Due to the default poly-algorithm used by QuantifierEliminate, InsertFormula and DeleteFormula, evolutionary operations are only supported for QEData when the problem is homogeneously quantified as the examples above. For evolutionary methods in any context, QE by CAD must be used in isolation. The following demonstrates examples of this, by acquiring a CADData object from PartialCylindricalAlgebraicDecompose. PartialCylindricalAlgebraicDecompose performs QE purely by CAD. A CADData object is amenable to usage of InsertFormula and DeleteFormula with the same syntax as QEData otherwise.
>
|
expr := exists(z,forall(y,exists(x,And(4*x^2+x*y^2-z+1/4 = 0,2*x+y^2*z+1/2 = 0,x^2*z-1/
2*x-y^2 = 0)))); # [9], "Random A", QEExamples
|
| (3.34) |
>
|
op( [ 2, 2, 2 ], expr ); # the unquantified conjunction from the formula
|
| (3.35) |
>
|
exprIn := exists( z, forall( y, exists( x, 4*x^2 + x*y^2 - z + 1/4 = 0 ) ) );
|
| (3.36) |
>
|
( q, w, data ) := PartialCylindricalAlgebraicDecompose( exprIn, 'output = [ qf, witnesses, data ]' );
|
| (3.37) |
>
|
for i from 2 to nops( op( [ 2, 2, 2 ], expr ) ) do # demonstrating incrementality with loop
printf( "Adding clause %a\n", op( [ 2, 2, 2, i ], expr ) );
( q, data ) := InsertFormula( data, ':-And', i, op( [ 2, 2, 2, i ], expr ), 'output = [ qf, data ]' );
printf( "Number of leaf cells in CAD: %d\n", NumberOfLeafCells( data ) );
until not q: # because of the innermost quantifier which is universal
|
Adding clause 2*x+y^2*z+1/2 = 0
Number of leaf cells in CAD: 61
| |
>
|
i, nops( op( [ 2, 2, 2 ], expr ) );
|
| (3.39) |
>
|
q, data, NumberOfLeafCells( data );
|
| (3.40) |
>
|
infolevel[ PartialCylindricalAlgebraicDecompose ] := 4:
|
>
|
( q, data ) := PartialCylindricalAlgebraicDecompose( expr, 'output = [ qf, data ]' ):
|
projectAllOrders: Exact triangular system deduced for equational constraints
| |
projectAllOrders: 3 elements in Groebner basis for equational constraints
| |
PartialCylindricalAlgebraicDecompose: Prenex conversion of input formula: exists(z,forall(y,exists(x,And(4*x*y^2+16*x^2-4*z+1 = 0,2*y^2*z+4*x+1 = 0,2*x^2*z-2*y^2-x = 0))))
| |
PartialCylindricalAlgebraicDecompose: 2 polynomials used in restricted projection operations due to equational constraints
| |
PartialCylindricalAlgebraicDecompose: 4 polynomials in projection basis for z
| |
PartialCylindricalAlgebraicDecompose: 1 polynomials in projection basis for y
| |
PartialCylindricalAlgebraicDecompose: 1 polynomials in projection basis for x
| |
PartialCylindricalAlgebraicDecompose: 6 total polynomials in projection
| |
PartialCylindricalAlgebraicDecompose: 111 total cells created in CAD
| |
PartialCylindricalAlgebraicDecompose: 45 leaf cells on termination
| |
>
|
q, data, NumberOfLeafCells( data );
|
| (3.41) |
>
|
infolevel[ PartialCylindricalAlgebraicDecompose ] := 0:
|
|
|
Poly-algorithmic QE [5,6]
|
|
The implementation of the default routine offered for QE in QuantifierElimination, QuantifierEliminate, is a poly-algorithm between two main algorithms for QE: VTS (Virtual Term Substitution) and CAD (Cylindrical Algebraic Decomposition).
Briefly, because VTS is currently only applicable up to certain polynomial degrees, CAD can be used as a failover when VTS is no longer applicable in intermediate processing of the formula. However, the usage of CAD within the poly-algorithm is highly incremental at such stages by default.
>
|
expr := exists([a, b, c, d],And(a^2+b^2 = r^2,0 <= a,b < 0,1 <= c,d < -1,c-(1+b)*(c-a)
= 0,d-(1-a)*(d-b) = 0)); # [9], "Piano Movers Problem (Wang)", QEExamples
|
| (4.1) |
Most QuantifierElimination routines offer printing of verbose information via infolevel.
>
|
infolevel[ QuantifierEliminate ] := 3;
|
| (4.2) |
Usage of the poly-algorithm is controllable via keyword options. The 'hybridmode' option controls how the algorithm should traverse nodes of the VTS tree when switching to CAD:
>
|
QuantifierEliminate( expr, 'hybridmode = depth' ); # actually default option in QuantifierEliminate
|
QuantifierEliminate: Prenex conversion of input formula: exists([a, b, c, d],And(a^2+b^2-r^2 = 0,-a <= 0,b < 0,-c <= -1,d < -1,a*b-b*c+a = 0,a*b-a*d-b = 0))
| |
QuantifierEliminate: All quantifiers are the same: exists, so problem is amenable to poly-algorithmic QE
| |
QuantifierEliminate: Eliminating last block of quantifiers in a formula exists([a, b, c, d],And(a^2+b^2-r^2 = 0,-a <= 0,b < 0,-c <= -1,d < -1,a*b-b*c+a = 0,a*b-a*d-b = 0)) via poly-algorithmic QE
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(b,0 < b) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(b,0 < -b) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < -a) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(b,0 < b) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(b,0 < -b) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
QuantifierEliminate: 0 unused calculated VTS test points
| |
QuantifierEliminate: 2 leaf formulae on termination of VTS
| |
QuantifierEliminate: Entering CAD for the first time to solve QE problem(s) of excessive degree for VTS
| |
QuantifierEliminate: Producing new CAD on QE problem of excessive degree: exists(a,And(a^2-r^2 <= 0,a <> 0,-a <= 0,a^2-r^2 < 0,Or(And(a^2 < 0,-a^6+a^4*r^2+2*a^5-2*a^3*r^2-2*a^4+a^2*r^2 < 0),And(-a^2+a <= 0,Or(a^2 < 0,a^6-a^4*r^2-2*a^5+2*a^3*r^2+2*a^4-a^2*r^2 < 0))),a^2-r^2 = 0,-a^2 <= 0,a^4-a^2*r^2+a^2 = 0))
| |
QuantifierEliminate: 1 polynomials used in restricted projection operations due to equational constraints
| |
QuantifierEliminate: 1 polynomials in projection basis for a
| |
QuantifierEliminate: 5 polynomials in projection basis for a
| |
QuantifierEliminate: 6 total polynomials in projection
| |
QuantifierEliminate: 30 total cells created in CAD
| |
QuantifierEliminate: 27 leaf cells on termination
| |
QuantifierEliminate: Modifying existing CAD to solve QE problem of excessive degree: exists(a,And(a^2-r^2 <= 0,a^2-r^2 <> 0,a <> 0,-a <= 0,a^2-r^2 < 0,Or(And(a^3-a*r^2-a^2+r^2 <= 0,-a^6+2*a^4*r^2-a^2*r^4+2*a^5-4*a^3*r^2+2*a*r^4-2*a^4+3*a^2*r^2-r^4 <= 0),And(a <= 0,a^6-2*a^4*r^2+a^2*r^4-2*a^5+4*a^3*r^2-2*a*r^4+2*a^4-3*a^2*r^2+r^4 <= 0)),Or(And(a^2 < 0,-a^6+a^4*r^2+2*a^5-2*a^3*r^2-2*a^4+a^2*r^2 < 0),And(-a^2+a <= 0,Or(a^2 < 0,a^6-a^4*r^2-2*a^5+2*a^3*r^2+2*a^4-a^2*r^2 < 0)))))
| |
modifyCADResult: 0 new quantified variables involved in CAD in VTS to CAD incrementality
| |
modifyCADResult: 1 polynomials are used in restricted projection operations due to equational constraints
| |
modifyCADResult: 4 new polynomials in r from incremental projection
| |
modifyCADResult: 0 new polynomials in a from incremental projection
| |
modifyCADResult: 168 total cells created in CAD
| |
modifyCADResult: 135 leaf cells on termination
| |
QuantifierEliminate: Modifying existing CAD to solve QE problem of excessive degree: exists(a,And(a^2-r^2 <= 0,a^2-r^2 <> 0,-a <= 0,a^2-r^2 < 0,Or(And(a^3-a*r^2-a^2+r^2 <= 0,-a^6+2*a^4*r^2-a^2*r^4+2*a^5-4*a^3*r^2+2*a*r^4-2*a^4+3*a^2*r^2-r^4 <= 0),And(a <= 0,a^6-2*a^4*r^2+a^2*r^4-2*a^5+4*a^3*r^2-2*a*r^4+2*a^4-3*a^2*r^2+r^4 <= 0)),a = 0,a^4-a^2*r^2-2*a^3+2*a*r^2+a^2-r^2 = 0))
| |
modifyCADResult: 0 new quantified variables involved in CAD in VTS to CAD incrementality
| |
modifyCADResult: 1 polynomials are used in restricted projection operations due to equational constraints
| |
modifyCADResult: 0 new polynomials in r from incremental projection
| |
modifyCADResult: 0 new polynomials in a from incremental projection
| |
modifyCADResult: 168 total cells created in CAD
| |
modifyCADResult: 143 leaf cells on termination
| |
QuantifierEliminate: Modifying existing CAD to solve QE problem of excessive degree: exists(a,And(a^2-r^2 <= 0,a <> 0,-a <= 0,a^2-r^2 < 0,Or(And(a^2 < 0,-a^6+a^4*r^2+2*a^5-2*a^3*r^2-2*a^4+a^2*r^2 < 0),And(-a^2+a <= 0,Or(a^2 < 0,a^6-a^4*r^2-2*a^5+2*a^3*r^2+2*a^4-a^2*r^2 < 0))),-a^2+a <= 0,a^4-a^2*r^2-2*a^3+2*a*r^2+2*a^2-r^2 = 0))
| |
modifyCADResult: 0 new quantified variables involved in CAD in VTS to CAD incrementality
| |
modifyCADResult: 1 polynomials are used in restricted projection operations due to equational constraints
| |
modifyCADResult: 0 new polynomials in r from incremental projection
| |
modifyCADResult: 0 new polynomials in a from incremental projection
| |
modifyCADResult: 168 total cells created in CAD
| |
modifyCADResult: 143 leaf cells on termination
| |
QuantifierEliminate: Modifying existing CAD to solve QE problem of excessive degree: exists(a,And(a^2-r^2 <= 0,-a <= 0,a^2-r^2 < 0,-a^2+a <= 0,a^4-a^2*r^2-2*a^3+2*a*r^2+2*a^2-r^2 = 0,a = 0,a^4-a^2*r^2-2*a^3+2*a*r^2+a^2-r^2 = 0))
| |
modifyCADResult: 0 new quantified variables involved in CAD in VTS to CAD incrementality
| |
modifyCADResult: 1 polynomials are used in restricted projection operations due to equational constraints
| |
modifyCADResult: 0 new polynomials in r from incremental projection
| |
modifyCADResult: 0 new polynomials in a from incremental projection
| |
modifyCADResult: 168 total cells created in CAD
| |
modifyCADResult: 143 leaf cells on termination
| |
QuantifierEliminate: Modifying existing CAD to solve QE problem of excessive degree: exists(a,And(a < 1,a^2-a <> 0,a^4-a^2*r^2-2*a^3+2*a*r^2+2*a^2-r^2 = 0,-a <= 0,-a^2+a < 0,a = 0))
| |
modifyCADResult: 0 new quantified variables involved in CAD in VTS to CAD incrementality
| |
modifyCADResult: 1 polynomials are used in restricted projection operations due to equational constraints
| |
modifyCADResult: 0 new polynomials in r from incremental projection
| |
modifyCADResult: 0 new polynomials in a from incremental projection
| |
modifyCADResult: 168 total cells created in CAD
| |
modifyCADResult: 143 leaf cells on termination
| |
QuantifierEliminate: Modifying existing CAD to solve QE problem of excessive degree: exists(a,And(-a < -1,a^2-a <> 0,a^4-a^2*r^2-2*a^3+2*a*r^2+2*a^2-r^2 = 0,-a <= 0,-a^2+a < 0,a = 0))
| |
modifyCADResult: 0 new quantified variables involved in CAD in VTS to CAD incrementality
| |
modifyCADResult: 1 polynomials are used in restricted projection operations due to equational constraints
| |
modifyCADResult: 0 new polynomials in r from incremental projection
| |
modifyCADResult: 0 new polynomials in a from incremental projection
| |
modifyCADResult: 168 total cells created in CAD
| |
modifyCADResult: 143 leaf cells on termination
| |
QuantifierEliminate: Modifying existing CAD to solve QE problem of excessive degree: exists(a,And(a-1 <> 0,a^4-a^2*r^2-2*a^3+2*a*r^2+2*a^2-r^2 = 0,-a <= 0,-a^2+a < 0,a = 0))
| |
modifyCADResult: 0 new quantified variables involved in CAD in VTS to CAD incrementality
| |
modifyCADResult: 1 polynomials are used in restricted projection operations due to equational constraints
| |
modifyCADResult: 0 new polynomials in r from incremental projection
| |
modifyCADResult: 0 new polynomials in a from incremental projection
| |
modifyCADResult: 168 total cells created in CAD
| |
modifyCADResult: 143 leaf cells on termination
| |
| (4.3) |
>
|
QuantifierEliminate( expr, 'hybridmode = whole' );
|
QuantifierEliminate: Prenex conversion of input formula: exists([a, b, c, d],And(a^2+b^2-r^2 = 0,-a <= 0,b < 0,-c <= -1,d < -1,a*b-b*c+a = 0,a*b-a*d-b = 0))
| |
QuantifierEliminate: All quantifiers are the same: exists, so problem is amenable to poly-algorithmic QE
| |
QuantifierEliminate: Eliminating last block of quantifiers in a formula exists([a, b, c, d],And(a^2+b^2-r^2 = 0,-a <= 0,b < 0,-c <= -1,d < -1,a*b-b*c+a = 0,a*b-a*d-b = 0)) via poly-algorithmic QE
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(b,0 < b) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(b,0 < -b) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < -a) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(b,0 < b) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(b,0 < -b) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < a-1) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
ModuleCopy: Eliminating last block of quantifiers in a formula exists(a,0 < 1-a) via poly-algorithmic QE
| |
ModuleCopy: 0 unused calculated VTS test points
| |
ModuleCopy: 1 leaf formulae on termination of VTS
| |
QuantifierEliminate: 0 unused calculated VTS test points
| |
QuantifierEliminate: 2 leaf formulae on termination of VTS
| |
QuantifierEliminate: Entering CAD for the first time to solve QE problem(s) of excessive degree for VTS
| |
QuantifierEliminate: Entered CAD to solve (whole) QE problem of excessive degree for VTS: exists(a,Or(And(a-1 <> 0,a^4-a^2*r^2-2*a^3+2*a*r^2+2*a^2-r^2 = 0,-a <= 0,-a^2+a < 0,a = 0),And(a^2-r^2 <= 0,-a <= 0,a^2-r^2 < 0,-a^2+a <= 0,a^4-a^2*r^2-2*a^3+2*a*r^2+2*a^2-r^2 = 0,a = 0,a^4-a^2*r^2-2*a^3+2*a*r^2+a^2-r^2 = 0),And(-a < -1,a^2-a <> 0,a^4-a^2*r^2-2*a^3+2*a*r^2+2*a^2-r^2 = 0,-a <= 0,-a^2+a < 0,a = 0),And(a < 1,a^2-a <> 0,a^4-a^2*r^2-2*a^3+2*a*r^2+2*a^2-r^2 = 0,-a <= 0,-a^2+a < 0,a = 0),And(a^2-r^2 <= 0,a^2-r^2 <> 0,-a <= 0,a^2-r^2 < 0,Or(And(a^3-a*r^2-a^2+r^2 <= 0,-a^6+2*a^4*r^2-a^2*r^4+2*a^5-4*a^3*r^2+2*a*r^4-2*a^4+3*a^2*r^2-r^4 <= 0),And(a <= 0,a^6-2*a^4*r^2+a^2*r^4-2*a^5+4*a^3*r^2-2*a*r^4+2*a^4-3*a^2*r^2+r^4 <= 0)),a = 0,a^4-a^2*r^2-2*a^3+2*a*r^2+a^2-r^2 = 0),And(-r^2 <= 0,-r^2 < 0,r^2 = 0),And(a^2-r^2 <= 0,a <> 0,-a <= 0,a^2-r^2 < 0,Or(And(a^2 < 0,-a^6+a^4*r^2+2*a^5-2*a^3*r^2-2*a^4+a^2*r^2 < 0),And(-a^2+a <= 0,Or(a^2 < 0,a^6-a^4*r^2-2*a^5+2*a^3*r^2+2*a^4-a^2*r^2 < 0))),-a^2+a <= 0,a^4-a^2*r^2-2*a^3+2*a*r^2+2*a^2-r^2 = 0),And(a^2-r^2 <= 0,a^2-r^2 <> 0,a <> 0,-a <= 0,a^2-r^2 < 0,Or(And(a^3-a*r^2-a^2+r^2 <= 0,-a^6+2*a^4*r^2-a^2*r^4+2*a^5-4*a^3*r^2+2*a*r^4-2*a^4+3*a^2*r^2-r^4 <= 0),And(a <= 0,a^6-2*a^4*r^2+a^2*r^4-2*a^5+4*a^3*r^2-2*a*r^4+2*a^4-3*a^2*r^2+r^4 <= 0)),Or(And(a^2 < 0,-a^6+a^4*r^2+2*a^5-2*a^3*r^2-2*a^4+a^2*r^2 < 0),And(-a^2+a <= 0,Or(a^2 < 0,a^6-a^4*r^2-2*a^5+2*a^3*r^2+2*a^4-a^2*r^2 < 0)))),And(a^2-r^2 <= 0,a <> 0,-a <= 0,a^2-r^2 < 0,Or(And(a^2 < 0,-a^6+a^4*r^2+2*a^5-2*a^3*r^2-2*a^4+a^2*r^2 < 0),And(-a^2+a <= 0,Or(a^2 < 0,a^6-a^4*r^2-2*a^5+2*a^3*r^2+2*a^4-a^2*r^2 < 0))),a^2-r^2 = 0,-a^2 <= 0,a^4-a^2*r^2+a^2 = 0)))
| |
QuantifierEliminate: 0 polynomials used in restricted projection operations due to equational constraints
| |
QuantifierEliminate: 7 polynomials in projection basis for r
| |
QuantifierEliminate: 6 polynomials in projection basis for a
| |
QuantifierEliminate: 13 total polynomials in projection
| |
QuantifierEliminate: 314 total cells created in CAD
| |
QuantifierEliminate: 283 leaf cells on termination
| |
| (4.4) |
>
|
infolevel[ QuantifierEliminate ] := 0:
|
The 'maxvsdegree' keyword option controls the maximum applicable degree QuantifierEliminate will consider for usage of VTS. As such, 'maxvsdegree = 0' is completely equivalent to usage of PartialCylindricalAlgebraicDecompose, which offers QE completely by CAD under all circumstances.
|
|
Working with Cylindrical Algebraic Decompositions [1]
|
|
PartialCylindricalAlgebraicDecompose is the routine offered by QuantifierElimination to perform QE purely by CAD:
>
|
expr := exists(c,forall([b, a],Implies(Or(And(a-d = 0,b-c = 0),And(a-c = 0,b-1 = 0)),a^2-b = 0))); # [9], "Davenport-Heintz", QEExamples
|
| (5.1) |
>
|
PartialCylindricalAlgebraicDecompose( expr );
|
However CADs can be used to achieve more generic things in real algebraic geometry. CylindricalAlgebraicDecompose is the routine which allows you to retrieve a full "stock" CAD for a formula, via a CADData object.
>
|
C := CylindricalAlgebraicDecompose( GetUnquantifiedFormula( expr ), 'variablestrategy' = [ d, c, b, a ] ); # variable strategy as it would have to be for QE
|
| (5.3) |
Various methods are available on a CADData object. One can examine the underlying projection bases for the CAD in terms of the projection and lifting methodology of QuantifierElimination's CAD:
>
|
PrintProjection( C, 'verbose = true' );
|
| |
| |
| |
| |
| |
| |
| (5.4) |
>
|
NumberOfLeafCells( C );
|
>
|
leaves := GetCells( C )[ 1 .. 5 ]: # a few of the leaf cells
map(print, leaves):
|
| |
| |
| |
| |
| (5.6) |
GetCells is a method on a CADData object allowing for access to all cells of the CAD.
| (5.7) |
A CADCell is an object representing a CAD cell. The following demonstrates usage of two methods to query properties of a CADCell:
>
|
GetFullDescription( cell );
|
>
|
GetSamplePoints( cell );
|
| (5.9) |
SignOfPolynomialOnCell allows for querying the sign of a polynomial on a single CAD cell. It uses data from the overall CAD data structure, so is principally a method on CADData:
>
|
SignOfPolynomialOnCell( C, c - a, cell );
|
>
|
SignOfPolynomialOnCell( C, d - 1, cell );
|
>
|
SignOfPolynomialOnCell( C, ( c - a )*( d - 1 ), cell );
|
SignOfPolynomialOnCell will produce warnings when the query is ill defined in terms of the sign invariance of the CAD.
>
|
SignOfPolynomialOnCell( C, b + c, cell );
|
GetCellContainingPoint is a more specific method to retrieve a cell from a CAD containing a specific point in real space. This is a CADData method.
>
|
GetCellContainingPoint( C, [ d = 10, c = 0, a = -1, b = 2 ] );
|
| (5.14) |
>
|
GetCellDescriptionContainingPoint( C, [ d = 10, c = 0, a = -1, b = 2 ] );
|
| (5.15) |
The method produces warnings when the request is non-specific or otherwise not well defined in terms of the CAD.
>
|
GetCellContainingPoint( C, [ a = 4 ] );
|
| (5.16) |
>
|
cells := GetCells( CylindricalAlgebraicDecompose( x^2 + y^2 - 2 ) ):
|
>
|
for c in cells do
GetFullDescription( c );
end do;
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| (5.17) |
The 'data' output of the QuantifierEliminate routine of QuantifierElimination will be a QEData or CADData object. However, it is guaranteed to be a CADData object when the methodology of the routine is in some way forced to be pure CAD, such as the existence of radicals (where the radical is equivalent to a real algebraic number):
>
|
expr := exists( x, sqrt( 2 ) * x - 2 > 0 );
|
| (5.18) |
>
|
( q, w, data ) := QuantifierEliminate( expr, 'output = [ qf, witnesses, data ]' );
|
| (5.19) |
>
|
expr := [x^2+y^2-9 = 0, x^2+y^2-1 = 0]; # [9], "Concentric Circles", CADExamples
|
| (5.20) |
"Stock" CAD accepts sets or lists of polynomials, and will deduce equational constraints:
>
|
CylindricalAlgebraicDecompose( expr, 'variablestrategy = greedy' );
|
| (5.21) |
Under the various overloads offered by CylindricalAlgebraicDecompose, equational constraints can be specifically designated by the user via the second passed collection of polynomials:
>
|
A, E := [ randpoly( [ x, y ] ) ], { randpoly( [ x, y ] ) };
|
| (5.22) |
>
|
C := CylindricalAlgebraicDecompose( A, E, 'variablestrategy = sotd' );
NumberOfLeafCells( C );
|
| |
CylindricalAlgebraicDecompose allows for various keyword options at no constraint to produce a specific CAD requested by the user.
>
|
C := CylindricalAlgebraicDecompose( A, E, 'variablestrategy = sotd', 'liftingconstraints' = { x > -1, y > 0 } );
NumberOfLeafCells( C );
|
| |
>
|
C := CylindricalAlgebraicDecompose( A, E, 'variablestrategy = sotd', 'liftingconstraints = positive' );
NumberOfLeafCells( C );
|
| |
>
|
select( i -> length( i ) < 150, map( GetSamplePoints, GetCells( C ) ) ); # get some of the simpler CADCells to inspect
|
| (5.26) |
>
|
C := CylindricalAlgebraicDecompose( { randpoly([x]) }, 'opencad = true' )
|
| (5.27) |
>
|
NumberOfLeafCells( C );
|
>
|
C := CylindricalAlgebraicDecompose( x^2 + y^2 - 2 )
|
| (5.29) |
>
|
map(print, GetCells( C, output=['descriptions'] )):
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| (5.30) |
|
|
Equational Constraints with the Lazard Projection in CAD
|
|
Equational constraints are usually of high importance to implementations of CAD using the "projection and lifting" methodology for construction of CAD, as QuantifierElimination's is. CAD in QuantifierElimination is the first implementation of CAD for Maple using the Lazard projection. Furthermore, it is the first implementation using equational constraints in the Lazard projection.
Usage of equational constraints is more performant for CAD, but can threaten the integrity of the output via various observable mathematical occurrences which may force construction of CAD to fail in usage of the equational constraints. The QuantifierElimination package offers support for usage of up to multiple equational constraints from input, and in implementation of various algorithms from recent research [6,7], can guarantee resolution of a correct CAD for usage of a single equational constraint ('useequations = single'). Usage of multiple equational constraints 'useequations = multiple' may produce an error in circumstances where the mathematical impediments from usage of multiple equational constraints cannot be resolved.
>
|
expr := exists([b,a], And(a+b+c = 0,a*b+a*c+b*c = 0,a*b*c-1 = 0)); # [9], "Cyclic-3", QEExamples
|
| (6.1) |
The GetEquationalConstraints routine from QuantifierTools allows for examination of the equational constraints for a formula. These are the same equational constraints QuantifierElimination routines will use under the hood.
>
|
GetEquationalConstraints( expr );
|
| (6.2) |
Equational constraints can be implicit:
>
|
GetEquationalConstraints( And( x = 0, Or( y = a, b = c ) ) );
|
>
|
( q, data ) := PartialCylindricalAlgebraicDecompose( expr, 'output = [ qf, data ]' ):
|
| (6.5) |
We examine the properties of a CAD under varying usage of equational constraints. 'usegroebner' is a keyword option controlling preprocessing of equational constraints using Gröbner bases, while 'propagateecs' is relevant to usage of equational constraints in projection.
>
|
NumberOfLeafCells( data );
|
>
|
PrintProjection( data );
|
| |
| |
| (6.7) |
>
|
( q, data ) := PartialCylindricalAlgebraicDecompose( expr, 'output = [ qf, data ]', 'usegroebner' = false ):
|
>
|
PrintProjection( data );
|
| |
| |
| (6.8) |
>
|
NumberOfLeafCells( data );
|
>
|
( q, data ) := PartialCylindricalAlgebraicDecompose( expr, 'output = [ qf, data ]', 'usegroebner = false', 'propagateecs = false' ):
|
>
|
PrintProjection( data );
|
| |
| |
| (6.10) |
>
|
NumberOfLeafCells( data );
|
>
|
expr := exists([v__1, v__10, v__2, v__3, v__4, v__5, v__6, v__7, v__8, v__9],And(-v__3*
v__5*v__8+v__1*v__4 = 0,v__3*v__8 <> 0,-v__3*v__6*v__8+v__2*v__7 = 0,v__3*v__8
<> 0,v__7*v__9 = v__3,v__10*v__8 = v__1,-v__10*v__4*v__8+v__7*v__8*v__9-v__2*
v__7 = 0,v__7 <> 0,v__6 = 1-v__5)); # [3], Economics QE example 0063
|
| (6.12) |
>
|
eqns := GetEquationalConstraints( expr ); nops( eqns );
nops( op( 2, expr ) );
|
| |
>
|
infolevel[ PartialCylindricalAlgebraicDecompose ] := 4:
|
>
|
( q, data ) := PartialCylindricalAlgebraicDecompose( expr, 'output = [ qf, data ]', 'usegroebner' = true );
|
projectAllOrders: 6 elements in Groebner basis for equational constraints
| |
PartialCylindricalAlgebraicDecompose: Prenex conversion of input formula: exists([v__8, v__7, v__3, v__9, v__6, v__5, v__4, v__2, v__10, v__1],And(-v__3*v__5*v__8+v__1*v__4 = 0,v__3*v__8 <> 0,-v__3*v__6*v__8+v__2*v__7 = 0,-v__7*v__9+v__3 = 0,-v__10*v__8+v__1 = 0,v__10*v__4*v__8-v__7*v__8*v__9+v__2*v__7 = 0,v__7 <> 0,v__6-1+v__5 = 0))
| |
PartialCylindricalAlgebraicDecompose: 6 polynomials used in restricted projection operations due to equational constraints
| |
PartialCylindricalAlgebraicDecompose: 1 polynomials in projection basis for v__8
| |
PartialCylindricalAlgebraicDecompose: 1 polynomials in projection basis for v__7
| |
PartialCylindricalAlgebraicDecompose: 1 polynomials in projection basis for v__3
| |
PartialCylindricalAlgebraicDecompose: 1 polynomials in projection basis for v__9
| |
PartialCylindricalAlgebraicDecompose: 2 polynomials in projection basis for v__6
| |
PartialCylindricalAlgebraicDecompose: 1 polynomials in projection basis for v__5
| |
PartialCylindricalAlgebraicDecompose: 1 polynomials in projection basis for v__4
| |
PartialCylindricalAlgebraicDecompose: 2 polynomials in projection basis for v__2
| |
PartialCylindricalAlgebraicDecompose: 2 polynomials in projection basis for v__10
| |
PartialCylindricalAlgebraicDecompose: 1 polynomials in projection basis for v__1
| |
PartialCylindricalAlgebraicDecompose: 13 total polynomials in projection
| |
PartialCylindricalAlgebraicDecompose: 34 total cells created in CAD
| |
PartialCylindricalAlgebraicDecompose: 16 leaf cells on termination
| |
| (6.14) |
>
|
( q, data ) := PartialCylindricalAlgebraicDecompose( expr, 'output = [ qf, data ]', 'usegroebner = false' );
|
PartialCylindricalAlgebraicDecompose: Prenex conversion of input formula: exists([v__8, v__7, v__3, v__9, v__6, v__5, v__4, v__2, v__10, v__1],And(-v__3*v__5*v__8+v__1*v__4 = 0,v__3*v__8 <> 0,-v__3*v__6*v__8+v__2*v__7 = 0,-v__7*v__9+v__3 = 0,-v__10*v__8+v__1 = 0,v__10*v__4*v__8-v__7*v__8*v__9+v__2*v__7 = 0,v__7 <> 0,v__6-1+v__5 = 0))
| |
PartialCylindricalAlgebraicDecompose: 6 polynomials used in restricted projection operations due to equational constraints
| |
PartialCylindricalAlgebraicDecompose: 1 polynomials in projection basis for v__8
| |
PartialCylindricalAlgebraicDecompose: 1 polynomials in projection basis for v__7
| |
PartialCylindricalAlgebraicDecompose: 1 polynomials in projection basis for v__3
| |
PartialCylindricalAlgebraicDecompose: 2 polynomials in projection basis for v__9
| |
PartialCylindricalAlgebraicDecompose: 3 polynomials in projection basis for v__6
| |
PartialCylindricalAlgebraicDecompose: 2 polynomials in projection basis for v__5
| |
PartialCylindricalAlgebraicDecompose: 1 polynomials in projection basis for v__4
| |
PartialCylindricalAlgebraicDecompose: 3 polynomials in projection basis for v__2
| |
PartialCylindricalAlgebraicDecompose: 3 polynomials in projection basis for v__10
| |
PartialCylindricalAlgebraicDecompose: 2 polynomials in projection basis for v__1
| |
PartialCylindricalAlgebraicDecompose: 19 total polynomials in projection
| |
PartialCylindricalAlgebraicDecompose: 38 total cells created in CAD
| |
PartialCylindricalAlgebraicDecompose: 20 leaf cells on termination
| |
| (6.15) |
>
|
infolevel[ PartialCylindricalAlgebraicDecompose ] := 0:
|
>
|
expr := exists([a, b, c, d],And(a^2+b^2 = r^2,0 <= a,b < 0,1 <= c,d < -1,c-(1+b)*(c-a)
= 0,d-(1-a)*(d-b) = 0)); # [9], "Piano Movers Problem (Wang)", QEExamples
|
| (6.16) |
As stated before, usage of multiple equational constraints ('useequations = multiple') can fail with an expectable error.
>
|
CylindricalAlgebraicDecompose( expr, 'useequations = multiple' );
|
Error, (in QuantifierElimination:-CylindricalAlgebraicDecompose) Lazard curtain detected: a level 4 equational constraint a*b-a*d-b has non zero valuation on cell with index [4, 2, 3], and sample point [b = 0, a = 0, r = 1] and so a Lazard projection CAD using equational constraint optimizations cannot be produced for the input polynomials or formula with this variable ordering [b, a, r, d, c] and multiple equational constraints (useequations = multiple) |lib/QuantifierElimination/CAD/CADCell_Methods/src/CCHILD.mm:110|
| |
>
|
infolevel[ CylindricalAlgebraicDecompose ] := 4;
|
| (6.17) |
Usage of at most a single equational constraint is always a viable failover in such a case.
>
|
CylindricalAlgebraicDecompose( expr, 'useequations = single' );
|
projectAllOrders: 3 elements in Groebner basis for equational constraints
| |
CylindricalAlgebraicDecompose: 1 polynomials used in restricted projection operations due to equational constraints
| |
CylindricalAlgebraicDecompose: 4 polynomials in projection basis for b
| |
CylindricalAlgebraicDecompose: 4 polynomials in projection basis for a
| |
CylindricalAlgebraicDecompose: 1 polynomials in projection basis for r
| |
CylindricalAlgebraicDecompose: 2 polynomials in projection basis for d
| |
CylindricalAlgebraicDecompose: 2 polynomials in projection basis for c
| |
CylindricalAlgebraicDecompose: 13 total polynomials in projection
| |
decomposeCurtainCellsCAD: Performing extra decomposition to fix 15 cells with non-point curtains from lifting, via 1 polynomials from original inequalities
| |
CylindricalAlgebraicDecompose: 4039 total cells created in CAD
| |
CylindricalAlgebraicDecompose: 3155 leaf cells on termination
| |
| (6.18) |
>
|
infolevel[ CylindricalAlgebraicDecompose ] := 0:
|
|
|
QuantifierTools
|
|
QuantifierTools is a subpackage of QuantifierElimination offering routines for manipulation of formulae in the same format as the input syntax for QuantifierElimination as a whole.
>
|
expr := Implies( x > 0, forall( x, Not( x^2 <= 0 ) ) );
|
| (7.1) |
>
|
prenexExpr := ConvertToPrenexForm( expr );
|
| (7.2) |
>
|
NegateFormula( prenexExpr );
|
| (7.3) |
>
|
expr := And( exists( x, x > 0 ), exists( x, x = 0 ) );
|
| (7.4) |
AlphaConvert removes conflicts between variables using the same symbol for formulae which are principally non-prenex:
| (7.5) |
>
|
ConvertToPrenexForm( expr );
|
| (7.6) |
>
|
expr := And( x/y <> 0, z/d > 0 );
|
ConvertRationalConstraintsToTarski converts formulae using rational functions to an equivalent Tarski formula:
>
|
ConvertRationalConstraintsToTarski( expr );
|
>
|
expr := exists([y, x],And(x^2+y^2-1 = 0,b^2*(x-c)^2+a^2*y^2-a^2*b^2 = 0,0 < a,a < 1,0 < b,b < 1,0 <= c,c < 1)); # [9], "Ellipse A", QEExamples
|
| (7.9) |
SuggestCADOptions suggests a set of parameters including keyword options applicable to the CylindricalAlgebraicDecompose and PartialCylindricalAlgebraicDecompose routines of QuantifierElimination. These keyword options are suggested in terms of improvement of performance while preserving the integrity of the output.
The 'liftingconstraints' option allows for construction of a CAD in a hyperrectangle in real space for performance. In the above example, the formula principally includes the definition of such a hyperrectangle which can be extracted.
>
|
paramsSuggest := SuggestCADOptions( expr );
|
| (7.10) |
>
|
PartialCylindricalAlgebraicDecompose( paramsSuggest, 'useequations = single' );
|
| (7.11) |
The 'opencad' option allows for construction only of cells of full dimension. This is applicable when the input formula principally features no strong bounds:
>
|
expr := forall(x,0 < 4*x^8-4*(L-3)*x^6-2*(3*L-6)*x^4-2*(L-3)*x^2+1); # [9], "Piano Movers Problem (Yang, Zheng)", QEExamples
|
| (7.12) |
>
|
paramsSuggest := SuggestCADOptions( expr );
|
| (7.13) |
>
|
PartialCylindricalAlgebraicDecompose( paramsSuggest );
|
| (7.14) |
|
|
References
|
|
[1] G.E. Collins. "Quantifier Elimination for Real Closed Fields by Cylindrical Algebraic Decomposition". In Proceedings 2nd. GI Conference Automata Theory & Formal Languages, pages 134–183, 1975.
[2] V. Weispfenning. "The complexity of linear problems in fields". Journal of Symbolic Computation, 5(1):3–27, 1988.
[3] C.B. Mulligan, R. Bradford, J.H. Davenport, M. England, and Z. Tonks. "Non-linear Real Arithmetic Benchmarks derived from Automated Reasoning in Economics". In Proceedings SC2 Workshop FLoC 2018. CEUR Workshop Proceedings, 2018.
[4] Z. Tonks. "Evolutionary Virtual Term Substitution in a Quantifier Elimination System". In Proceedings SC2 Workshop 2019. CEUR Workshop Proceedings, 10 2019.
[5] Z. Tonks. "A Poly-algorithmic Quantifier Elimination Package in Maple". In Jürgen Gerhard and Ilias Kotsireas, editors, Maple in Mathematics Education and Research, pages 171–186, Cham, 2020. Springer International Publishing. https://www.youtube.com/watch?v=DzrBaUkXLAo
[6] A. Nair, J.H. Davenport, and G. Sankaran, "Curtains in CAD: Why Are They a Problem and How Do We Fix Them?". In Mathematical Software - ICMS 2020, volume 12097 of Lecture Notes in Computer Science, pages 17-26, Cham, 2020. Springer.
[7] A. Nair, "Curtains in Cylindrical Algebraic Decomposition". PhD thesis, University of Bath, 2021.
[8] Z. Tonks. "Poly-algorithmic Techniques in Real Quantifier Elimination". PhD thesis, University of Bath, 2021.
[9] Z. Tonks. "Repository of data supporting the thesis "Poly-algorithmic Techniques in Real Quantifier Elimination"". https://zenodo.org/record/4382083, 2021.
|
Return to Index for Example Worksheets
|