Portability | unportable |
---|---|
Stability | unstable |
Maintainer | Martin Avanzini <martin.avanzini@uibk.ac.at> |
Safe Haskell | Safe-Infered |
This module collects available processors of TcT.
A processor p
is the TcT representation of a complexity techniques
that, given a complexity problem, constructs a complete proof for
the problem.
Processors are parameterised in some arguments that control the behaviour
of the processor, for instance, the matrix processor is parameterised
in the dimension of the constructed matrix interpretation.
Parameterised processors are called processor instances, and
can be obtained using the constructors in Tct.Instances.
A list of processors and their synopsis can also be obtained from
the command line, using the flag --list
.
- builtInProcessors :: AnyProcessor
- isDuplicating :: StdProcessor Predicate
- isConstructor :: StdProcessor Predicate
- isCollapsing :: StdProcessor Predicate
- isGround :: StdProcessor Predicate
- isLeftLinear :: StdProcessor Predicate
- isRightLinear :: StdProcessor Predicate
- isWellFormed :: StdProcessor Predicate
- isOutermost :: StdProcessor Predicate
- isInnermost :: StdProcessor Predicate
- isFull :: StdProcessor Predicate
- isContextSensitive :: StdProcessor Predicate
- isDCProblem :: StdProcessor Predicate
- isRCProblem :: StdProcessor Predicate
- popstar :: StdProcessor PopStar
- ppopstar :: StdProcessor PopStar
- lmpo :: StdProcessor PopStar
- bounds :: StdProcessor Bounds
- fail :: StdProcessor Fail
- success :: StdProcessor Success
- empty :: StdProcessor EmptyRules
- open :: StdProcessor Open
- ite :: StdProcessor (Ite AnyProcessor AnyProcessor AnyProcessor)
- best :: StdProcessor (OneOf AnyProcessor)
- fastest :: StdProcessor (OneOf AnyProcessor)
- sequentially :: StdProcessor (OneOf AnyProcessor)
- matrix :: StdProcessor NaturalMI
- arctic :: StdProcessor ArcticMI
- mpo :: StdProcessor Mpo
- poly :: StdProcessor NaturalPI
- timeout :: StdProcessor (Timeout AnyProcessor)
- irr :: Transformation InnermostRuleRemoval AnyProcessor
- decomposeDG :: Transformation (DecomposeDG AnyProcessor AnyProcessor) AnyProcessor
- weightgap :: Transformation WeightGap AnyProcessor
- decompose :: Transformation (Decompose AnyProcessor) AnyProcessor
- toInnermost :: Transformation ToInnermost AnyProcessor
- dependencyPairs :: Transformation DPs AnyProcessor
- removeHead :: Transformation RemoveHead AnyProcessor
- removeWeakSuffix :: Transformation RemoveWeakSuffix AnyProcessor
- simpDPRHS :: Transformation SimpRHS AnyProcessor
- simpPE :: Transformation (SimpPE AnyProcessor) AnyProcessor
- usableRules :: Transformation UR AnyProcessor
- pathAnalysis :: Transformation PathAnalysis AnyProcessor
- uncurry :: Transformation Uncurry AnyProcessor
Documentation
isDuplicating :: StdProcessor Predicate
- on :: strict|weak|both|union (optional)
- Chooses the TRS from the problem on which the predicate is applied (only applies to predicates on TRSs).
isConstructor :: StdProcessor Predicate
- on :: strict|weak|both|union (optional)
- Chooses the TRS from the problem on which the predicate is applied (only applies to predicates on TRSs).
isCollapsing :: StdProcessor Predicate
- on :: strict|weak|both|union (optional)
- Chooses the TRS from the problem on which the predicate is applied (only applies to predicates on TRSs).
isGround :: StdProcessor Predicate
- on :: strict|weak|both|union (optional)
- Chooses the TRS from the problem on which the predicate is applied (only applies to predicates on TRSs).
isLeftLinear :: StdProcessor Predicate
- on :: strict|weak|both|union (optional)
- Chooses the TRS from the problem on which the predicate is applied (only applies to predicates on TRSs).
isRightLinear :: StdProcessor Predicate
- on :: strict|weak|both|union (optional)
- Chooses the TRS from the problem on which the predicate is applied (only applies to predicates on TRSs).
isWellFormed :: StdProcessor Predicate
- on :: strict|weak|both|union (optional)
- Chooses the TRS from the problem on which the predicate is applied (only applies to predicates on TRSs).
isOutermost :: StdProcessor Predicate
- on :: strict|weak|both|union (optional)
- Chooses the TRS from the problem on which the predicate is applied (only applies to predicates on TRSs).
isInnermost :: StdProcessor Predicate
- on :: strict|weak|both|union (optional)
- Chooses the TRS from the problem on which the predicate is applied (only applies to predicates on TRSs).
isFull :: StdProcessor Predicate
- on :: strict|weak|both|union (optional)
- Chooses the TRS from the problem on which the predicate is applied (only applies to predicates on TRSs).
isContextSensitive :: StdProcessor Predicate
- on :: strict|weak|both|union (optional)
- Chooses the TRS from the problem on which the predicate is applied (only applies to predicates on TRSs).
isDCProblem :: StdProcessor Predicate
- on :: strict|weak|both|union (optional)
- Chooses the TRS from the problem on which the predicate is applied (only applies to predicates on TRSs).
isRCProblem :: StdProcessor Predicate
- on :: strict|weak|both|union (optional)
- Chooses the TRS from the problem on which the predicate is applied (only applies to predicates on TRSs).
popstar :: StdProcessor PopStar
This processor implements orientation of the input problem using 'polynomial path orders', a technique applicable for innermost runtime-complexity analysis. Polynomial path orders are a miniaturisation of 'multiset path orders', restricted so that compatibility assesses a polynomial bound on the innermost runtime-complexity. The implementation for DP problems additionally employs argument filterings.
- ps :: On|Off (optional)
- Parameter substitution: If enabled, parameter substitution is allowed, strengthening the order.
- wsc :: On|Off (optional)
- Weak Safe Composition: If enabled then composition is restricted to weak safe composition.
- deg :: <nat>|none (optional)
- Deg: If set and applicable, polynomially bounded runtime complexity with given degree is proven. This flag only works in combination with product extension and weak safe composition, cf.
popstarSmall
.
ppopstar :: StdProcessor PopStar
This processor implements orientation of the input problem using 'polynomial path orders' with product extension, c.f. processor 'popstar'.
- ps :: On|Off (optional)
- Parameter substitution: If enabled, parameter substitution is allowed, strengthening the order.
- wsc :: On|Off (optional)
- Weak Safe Composition: If enabled then composition is restricted to weak safe composition.
- deg :: <nat>|none (optional)
- Deg: If set and applicable, polynomially bounded runtime complexity with given degree is proven. This flag only works in combination with product extension and weak safe composition, cf.
popstarSmall
.
This processor implements orientation of the input problem using 'light multiset path orders', a technique applicable for innermost runtime-complexity analysis. Light multiset path orders are a miniaturisation of 'multiset path orders', restricted so that compatibility assesses polytime computability of the functions defined. Further, it induces exponentially bounded innermost runtime-complexity.
- ps :: On|Off (optional)
- Parameter substitution: If enabled, parameter substitution is allowed, strengthening the order.
- wsc :: On|Off (optional)
- Weak Safe Composition: If enabled then composition is restricted to weak safe composition.
- deg :: <nat>|none (optional)
- Deg: If set and applicable, polynomially bounded runtime complexity with given degree is proven. This flag only works in combination with product extension and weak safe composition, cf.
popstarSmall
.
This processor implements the (match|roof|top)-bounds technique that induces linear derivational- and runtime-complexity for right-linear problems. For non-right-linear problems this processor fails immediately.
- initial :: minimal|perSymbol (optional)
- The employed initial automaton.
If
perSymbol
is set then the initial automaton admits one dedicated state per function symbols. Ifminimal
is set then the initial automaton admits exactly one state for derivational-complexity analysis. For runtime-complexity analysis, two states are used in order to distinguish defined symbols from constructors. - enrichment :: match|roof|top (optional)
- The employed enrichment.
fail :: StdProcessor Fail
Processor 'fail' always returns the answer 'No'.
success :: StdProcessor Success
Processor 'success' always returns the answer 'Yes(?,?)'.
empty :: StdProcessor EmptyRules
Processor 'empty' returns 'Yes(O(1),O(1))' if the strict component of the problem is empty.
open :: StdProcessor Open
ite :: StdProcessor (Ite AnyProcessor AnyProcessor AnyProcessor)
This processor implements conditional branching
- guard :: <processor>
- The guard processor. It succeeds if it returns 'Yes(*,*)'.
- then :: <processor>
- The processor that is applied if guard succeeds.
- else :: <processor>
- The processor that is applied if guard fails.
best :: StdProcessor (OneOf AnyProcessor)
Processor 'Best' applies the given list of processors in parallel and returns the proof admitting the lowest complexity certificate.
- subprocessors :: <processor>...
- a list of subprocessors
fastest :: StdProcessor (OneOf AnyProcessor)
Processor 'Fastest' applies the given list of processors in parallel and returns the first successful proof.
- subprocessors :: <processor>...
- a list of subprocessors
sequentially :: StdProcessor (OneOf AnyProcessor)
Processor 'Sequentially' applies the given list of processors sequentially and returns the first successful proof.
- subprocessors :: <processor>...
- a list of subprocessors
matrix :: StdProcessor NaturalMI
This processor orients the problem using matrix-interpretation over natural numbers.
- cert :: algebraic|automaton|nothing (optional)
- This argument specifies restrictions on the matrix-interpretation which induce polynomial growth of
the interpretation of the considered starting terms relative to their size.
Here
algebraic
refers to simple algebraic restrictions on matrices (in the current implementation, they are simply restricted to triangular shape, i.e. matrices where coefficients in the lower-left half below the diagonal are zero. Such matrix-interpretations induce polynomial derivational-complexity. Ifautomaton
is given as argument, then criteria from the theory of weighted automata are used instead (in the current implementation, the negations of the criteria EDA, and possibly IDA(n), in the case that the flagdegree
is set, are used). Ifnothing
is given, then matrix-interpretations of all function symbols are unrestricted. Note that matrix interpretations produced with this option do not induce polynomial complexities in general. The default value isautomaton
. - degree :: <nat>|none (optional)
- This argument ensures that the complexity induced by the searched matrix interpretation is bounded by a
polynomial of the given degree. Its internal effect is dictated by the value the argument
cert
is set to. If it is set toalgebraic
, this restricts the number of non-zero entries in the diagonals of the matrices. If it is set toautomaton
, this set the paramtern
in the criterion 'not IDA(n)'. Finally, if it is set tounrestricted
, the effect of setting thedegree
argument is unspecified. - dim :: <nat> (optional)
- This argument specifies the dimension of the vectors and square-matrices appearing in the matrix-interpretation.
- bound :: <nat> (optional)
- This argument specifies an upper-bound on coefficients appearing in the interpretation. Such an upper-bound is necessary as we employ bit-blasting to SAT internally when searching for compatible matrix interpretations.
- bits :: <nat>|none (optional)
- This argument plays the same role as
bound
, but instead of an upper-bound the number of bits is specified. This argument overrides the argumentbound
. - cbits :: <nat>|none (optional)
- This argument specifies the number of bits used for intermediate results, as for instance coefficients of matrices obtained by interpreting left- and right-hand sides.
- uargs :: On|Off (optional)
- This argument specifies whether usable arguments are computed (if applicable) in order to relax the monotonicity constraints on the interpretation.
arctic :: StdProcessor ArcticMI
This processor orients the problem using matrix-interpretation over the arctic semiring.
- dim :: <nat> (optional)
- This argument specifies the dimension of the vectors and square-matrices appearing in the matrix-interpretation.
- bound :: <nat> (optional)
- This argument specifies an upper-bound on coefficients appearing in the interpretation. Such an upper-bound is necessary as we employ bit-blasting to SAT internally when searching for compatible matrix interpretations.
- bits :: <nat>|none (optional)
- This argument plays the same role as
bound
, but instead of an upper-bound the number of bits is specified. This argument overrides the argumentbound
. - cbits :: <nat>|none (optional)
- This argument specifies the number of bits used for intermediate results, as for instance coefficients of matrices obtained by interpreting left- and right-hand sides.
- uargs :: On|Off (optional)
- This argument specifies whether usable arguments are computed (if applicable) in order to relax the monotonicity constraints on the interpretation.
mpo :: StdProcessor Mpo
This processor implements 'multiset path orders' as found in the literature.
poly :: StdProcessor NaturalPI
This processor orients the problem using polynomial interpretation over natural numbers.
- kind :: linear|stronglylinear|simple|simplemixed|quadratic (optional)
- This argument specifies the shape of the polynomials used in the interpretation.
Allowed values are
stronglylinear
,linear
,simple
,simplemixed
, andquadratic
, referring to the respective shapes of the abstract polynomials used. The deault value isstronglylinear
. - bound :: <nat> (optional)
- This argument specifies an upper-bound on coefficients appearing in the interpretation. Such an upper-bound is necessary as we employ bit-blasting to SAT internally when searching for compatible matrix interpretations.
- bits :: <nat>|none (optional)
- This argument plays the same role as
bound
, but instead of an upper-bound the number of bits is specified. This argument overrides the argumentbound
. - cbits :: <nat>|none (optional)
- This argument specifies the number of bits used for intermediate results, as for instance coefficients of matrices obtained by interpreting left- and right-hand sides.
- uargs :: On|Off (optional)
- This argument specifies whether usable arguments are computed (if applicable) in order to relax the monotonicity constraints on the interpretation.
timeout :: StdProcessor (Timeout AnyProcessor)
The processor either returns the result of the given processor or, if the timeout elapses, aborts the computation and returns MAYBE.
- timeout :: <nat>
- The timeout in seconds
- processor :: <processor>
- The processor to apply with timeout
irr :: Transformation InnermostRuleRemoval AnyProcessor
This processor removes rules 'f(l_1,...,l_n) -> r' for which l_i (1 <= i <=n) is not a normal form. The processor applies only to innermost problems.
- subprocessor :: <processor>
- The processor that is applied on the transformed problem(s)
- strict :: On|Off (optional)
- If this flag is set and the transformation fails, this processor aborts. Otherwise, it applies the subprocessor on the untransformed input.
- parallel :: On|Off (optional)
- Decides whether the given subprocessor should be applied in parallel.
- checkSubsumed :: On|Off (optional)
- This flag determines whether the processor should reuse proofs in case that one generated problem subsumes another one. A problem (A) is subsumed by problem (B) if the complexity of (A) is bounded from above by the complexity of (B). Currently we only take subset-inclusions of the different components into account.
decomposeDG :: Transformation (DecomposeDG AnyProcessor AnyProcessor) AnyProcessor
This processor implements processor 'decompose' specifically for the (weak) dependency pair setting. It tries to estimate the complexity of the input problem based on the complexity of dependency pairs of upper congruence classes (with respect to the congruence graph) relative to the dependency pairs in the remaining lower congruence classes. The overall upper bound for the complexity of the input problem is estimated by multiplication of upper bounds of the sub problems. Note that the processor allows the optional specification of processors that are applied on the two individual subproblems. The transformation results into the systems which could not be oriented by those processors.
- subprocessor :: <processor>
- The processor that is applied on the transformed problem(s)
- strict :: On|Off (optional)
- If this flag is set and the transformation fails, this processor aborts. Otherwise, it applies the subprocessor on the untransformed input.
- parallel :: On|Off (optional)
- Decides whether the given subprocessor should be applied in parallel.
- checkSubsumed :: On|Off (optional)
- This flag determines whether the processor should reuse proofs in case that one generated problem subsumes another one. A problem (A) is subsumed by problem (B) if the complexity of (A) is bounded from above by the complexity of (B). Currently we only take subset-inclusions of the different components into account.
- split :: (optional)
- This problem determines the strict rules of the selected upper congruence rules.
- sub-processor-A :: <processor>|none (optional)
- If given, applied on the problem reflecting the upper congruence classes.
- sub-processor-B :: <processor>|none (optional)
- If given, applied on the problem reflecting the lower congruence classes.
weightgap :: Transformation WeightGap AnyProcessor
Uses the weight gap principle to shift some strict rules to the weak part of the problem.
- subprocessor :: <processor>
- The processor that is applied on the transformed problem(s)
- strict :: On|Off (optional)
- If this flag is set and the transformation fails, this processor aborts. Otherwise, it applies the subprocessor on the untransformed input.
- parallel :: On|Off (optional)
- Decides whether the given subprocessor should be applied in parallel.
- checkSubsumed :: On|Off (optional)
- This flag determines whether the processor should reuse proofs in case that one generated problem subsumes another one. A problem (A) is subsumed by problem (B) if the complexity of (A) is bounded from above by the complexity of (B). Currently we only take subset-inclusions of the different components into account.
- on :: trs|any (optional)
- This flag determine which rules have to be strictly oriented by the the matrix interpretation for
the weight gap principle. Here
trs
refers to all strict non-dependency-pair rules of the considered problem, whileany
only demands any rule at all to be strictly oriented. The default value istrs
. - cert :: algebraic|automaton|nothing (optional)
- This argument specifies restrictions on the matrix-interpretation for the weight gap condition which induce polynomial growth of
the interpretation of the considered starting terms relative to their size.
Here
algebraic
refers to simple algebraic restrictions on matrices (in the current implementation, they are simply restricted to triangular shape, i.e. matrices where coefficients in the lower-left half below the diagonal are zero. Such matrix-interpretations induce polynomial derivational-complexity. Ifautomaton
is given as argument, then criteria from the theory of weighted automata are used instead (in the current implementation, the negations of the criteria EDA, and possibly IDA(n), in the case that the flagdegree
is set, are used). Ifnothing
is given, then matrix-interpretations of all function symbols are unrestricted. Note that matrix interpretations produced with this option do not induce polynomial complexities in general. The default value isautomaton
. - degree :: <nat>|none (optional)
- This argument ensures that the complexity induced by the searched matrix interpretation for the weight gap condition is bounded by a
polynomial of the given degree. Its internal effect is dictated by the value the argument
cert
is set to. If it is set toalgebraic
, this restricts the number of non-zero entries in the diagonals of the matrices. If it is set toautomaton
, this set the paramtern
in the criterion 'not IDA(n)'. Finally, if it is set tounrestricted
, the effect of setting thedegree
argument is unspecified. - dim :: <nat> (optional)
- This argument specifies the dimension of the vectors and square-matrices appearing in the matrix-interpretation for the weight gap condition.
- bound :: <nat> (optional)
- This argument specifies an upper-bound on coefficients appearing in the interpretation. Such an upper-bound is necessary as we employ bit-blasting to SAT internally when searching for compatible matrix interpretations for the weight gap condition.
- bits :: <nat>|none (optional)
- This argument plays the same role as
bound
, but instead of an upper-bound the number of bits is specified. This argument overrides the argumentbound
. - cbits :: <nat>|none (optional)
- This argument specifies the number of bits used for intermediate results, computed for the matrix interpretation of the weight gap condition.
- uargs :: On|Off (optional)
- This argument specifies whether usable arguments are computed (if applicable) in order to relax the monotonicity constraints on the interpretation.
decompose :: Transformation (Decompose AnyProcessor) AnyProcessor
This transformation implements techniques for splitting the complexity problem into two complexity problems (A) and (B) so that the complexity of the input problem can be estimated by the complexity of the transformed problem. The processor closely follows the ideas presented in /Complexity Bounds From Relative Termination Proofs/ (<http://www.imn.htwk-leipzig.de/~waldmann/talk/06/rpt/rel/main.pdf>)
- subprocessor :: <processor>
- The processor applied on subproblem (A).
- subprocessor :: <processor>
- The processor that is applied on the transformed problem(s)
- strict :: On|Off (optional)
- If this flag is set and the transformation fails, this processor aborts. Otherwise, it applies the subprocessor on the untransformed input.
- parallel :: On|Off (optional)
- Decides whether the given subprocessor should be applied in parallel.
- checkSubsumed :: On|Off (optional)
- This flag determines whether the processor should reuse proofs in case that one generated problem subsumes another one. A problem (A) is subsumed by problem (B) if the complexity of (A) is bounded from above by the complexity of (B). Currently we only take subset-inclusions of the different components into account.
- split :: dynamic (optional)
- This argument of type
Partitioning
determines strict rules of problem (A). Usually, this should be set toDynamic
, in which case the given processor determines selection of rules dynamically. - allow :: Add|Mult|Compose (optional)
- This argument type
ComposeBound
determines how the complexity certificate should be obtained from subproblems (A) and (B). Consequently, this argument also determines the shape of (B). The third argument defines a processor that is applied on problem (A). If this processor succeeds, the input problem is transformed into (B). Note that for compose boundMult
the transformation only succeeds if applied to non size-increasing Problems.
toInnermost :: Transformation ToInnermost AnyProcessor
Switches to innermost rewriting on overlay and right-linear input.
- subprocessor :: <processor>
- The processor that is applied on the transformed problem(s)
- strict :: On|Off (optional)
- If this flag is set and the transformation fails, this processor aborts. Otherwise, it applies the subprocessor on the untransformed input.
- parallel :: On|Off (optional)
- Decides whether the given subprocessor should be applied in parallel.
- checkSubsumed :: On|Off (optional)
- This flag determines whether the processor should reuse proofs in case that one generated problem subsumes another one. A problem (A) is subsumed by problem (B) if the complexity of (A) is bounded from above by the complexity of (B). Currently we only take subset-inclusions of the different components into account.
dependencyPairs :: Transformation DPs AnyProcessor
Applies the (weak) depencency pair transformation.
- subprocessor :: <processor>
- The processor that is applied on the transformed problem(s)
- strict :: On|Off (optional)
- If this flag is set and the transformation fails, this processor aborts. Otherwise, it applies the subprocessor on the untransformed input.
- parallel :: On|Off (optional)
- Decides whether the given subprocessor should be applied in parallel.
- checkSubsumed :: On|Off (optional)
- This flag determines whether the processor should reuse proofs in case that one generated problem subsumes another one. A problem (A) is subsumed by problem (B) if the complexity of (A) is bounded from above by the complexity of (B). Currently we only take subset-inclusions of the different components into account.
- usetuples :: On|Off (optional)
- This argument specifies whether dependency tuples instead of pairs should be used.
removeHead :: Transformation RemoveHead AnyProcessor
Recursively removes all nodes that are either leafs in the dependency-graph or from the given problem. Only applicable if the strict component is empty.
- subprocessor :: <processor>
- The processor that is applied on the transformed problem(s)
- strict :: On|Off (optional)
- If this flag is set and the transformation fails, this processor aborts. Otherwise, it applies the subprocessor on the untransformed input.
- parallel :: On|Off (optional)
- Decides whether the given subprocessor should be applied in parallel.
- checkSubsumed :: On|Off (optional)
- This flag determines whether the processor should reuse proofs in case that one generated problem subsumes another one. A problem (A) is subsumed by problem (B) if the complexity of (A) is bounded from above by the complexity of (B). Currently we only take subset-inclusions of the different components into account.
simpDPRHS :: Transformation SimpRHS AnyProcessor
Simplify right hand sides of dependency pairs by removing marked subterms whose root symbols are undefined. Only applicable if the strict component is empty.
- subprocessor :: <processor>
- The processor that is applied on the transformed problem(s)
- strict :: On|Off (optional)
- If this flag is set and the transformation fails, this processor aborts. Otherwise, it applies the subprocessor on the untransformed input.
- parallel :: On|Off (optional)
- Decides whether the given subprocessor should be applied in parallel.
- checkSubsumed :: On|Off (optional)
- This flag determines whether the processor should reuse proofs in case that one generated problem subsumes another one. A problem (A) is subsumed by problem (B) if the complexity of (A) is bounded from above by the complexity of (B). Currently we only take subset-inclusions of the different components into account.
simpPE :: Transformation (SimpPE AnyProcessor) AnyProcessor
Moves a strict dependency into the weak component if all predecessors in the dependency graph are strict and there is no edge from the rule to itself. Only
- subprocessor :: <processor>
- The processor that is applied on the transformed problem(s)
- strict :: On|Off (optional)
- If this flag is set and the transformation fails, this processor aborts. Otherwise, it applies the subprocessor on the untransformed input.
- parallel :: On|Off (optional)
- Decides whether the given subprocessor should be applied in parallel.
- checkSubsumed :: On|Off (optional)
- This flag determines whether the processor should reuse proofs in case that one generated problem subsumes another one. A problem (A) is subsumed by problem (B) if the complexity of (A) is bounded from above by the complexity of (B). Currently we only take subset-inclusions of the different components into account.
usableRules :: Transformation UR AnyProcessor
This processor restricts the strict- and weak-rules to usable rules with respect to the dependency pairs.
- subprocessor :: <processor>
- The processor that is applied on the transformed problem(s)
- strict :: On|Off (optional)
- If this flag is set and the transformation fails, this processor aborts. Otherwise, it applies the subprocessor on the untransformed input.
- parallel :: On|Off (optional)
- Decides whether the given subprocessor should be applied in parallel.
- checkSubsumed :: On|Off (optional)
- This flag determines whether the processor should reuse proofs in case that one generated problem subsumes another one. A problem (A) is subsumed by problem (B) if the complexity of (A) is bounded from above by the complexity of (B). Currently we only take subset-inclusions of the different components into account.
pathAnalysis :: Transformation PathAnalysis AnyProcessor
This processor implements path-analysis as described in the dependency pair paper.
- subprocessor :: <processor>
- The processor that is applied on the transformed problem(s)
- strict :: On|Off (optional)
- If this flag is set and the transformation fails, this processor aborts. Otherwise, it applies the subprocessor on the untransformed input.
- parallel :: On|Off (optional)
- Decides whether the given subprocessor should be applied in parallel.
- checkSubsumed :: On|Off (optional)
- This flag determines whether the processor should reuse proofs in case that one generated problem subsumes another one. A problem (A) is subsumed by problem (B) if the complexity of (A) is bounded from above by the complexity of (B). Currently we only take subset-inclusions of the different components into account.
uncurry :: Transformation Uncurry AnyProcessor
This processor implements 'Uncurrying' for left-head-variable-free ATRSs
- subprocessor :: <processor>
- The processor that is applied on the transformed problem(s)
- strict :: On|Off (optional)
- If this flag is set and the transformation fails, this processor aborts. Otherwise, it applies the subprocessor on the untransformed input.
- parallel :: On|Off (optional)
- Decides whether the given subprocessor should be applied in parallel.
- checkSubsumed :: On|Off (optional)
- This flag determines whether the processor should reuse proofs in case that one generated problem subsumes another one. A problem (A) is subsumed by problem (B) if the complexity of (A) is bounded from above by the complexity of (B). Currently we only take subset-inclusions of the different components into account.