Given an SCC P over a TRS R this techniques tries to find a polynomial order > with
s ≥ t for all DPs s → t ∈ P
s > t for at least one DP s → t ∈ P
l ≥ r for all rules l → r ∈ U(P,π)
Here U(P,π) are the usable rules of P regarding the argument filtering π that
is implicit in the polynomial order.
If such an order is found, all strictly decreasing DPs are removed from P.
After the removal the Dependency Graph for the remaining DPs is computed again.
The set of SCCs of this new graph is the final result of this technique.
See [TGSK '04, GTSKF '03b] for references.
Application and Configuration
The user has two configuration possibilities for this technique. First, he can configure the
polynomial order in more detail by pressing the Configure POLO-button. Second, he can select
the method of how to search for the strict constraint. AProVE offers three different search modes:
Auto Strict uses the constraint ∑si - ti > 0
to enforce that there will be at least one strict decrease. In this way there only
has to be one call to the polynomial constraint solver. The drawback to the
equally powerful Search Strict mode is that
there will be one large constraint that may slow down
the constraint solver.
All Strict generates strict constraints for all DPs. This restricts power but if the
constraints are satisfiable then all DPs of the SCC can be removed resulting in no new
SCCs. Like in the Auto Strict mode, only one call to the polynomial solver is
required.
Search Strict iterates over the different possibilities of the strict constraint.
As soon as it finds a satisfiable set of constraints it stops the search and uses
the corresponding polynomial order as result. In the worst case there will be
n calls to the polynomial constraint solver where n is the number of DPs in the SCC.
Processing SCCs by solving polynomial constraints is quite fast if one uses
linear polynomial interpretations. These already turn out to
be sufficient for many examples resulting in a very good tradeoff between efficiency and power.