| Portability | unportable |
|---|---|
| Stability | unstable |
| Maintainer | Martin Avanzini <martin.avanzini@uibk.ac.at> |
| Safe Haskell | Safe-Infered |
Tct.Method.ComposeRC
Contents
Description
This module provides the compose-RC transformation.
- decomposeDG :: TheTransformer (DecomposeDG AnyProcessor AnyProcessor)
- solveUpperWith :: (Processor p1, Processor p2, Processor p) => TheTransformer (DecomposeDG p1 p2) -> InstanceOf p -> TheTransformer (DecomposeDG p1 p)
- solveLowerWith :: (Processor p1, Processor p2, Processor p) => TheTransformer (DecomposeDG p1 p2) -> InstanceOf p -> TheTransformer (DecomposeDG p p2)
- selectLowerBy :: (Processor p1, Processor p2) => TheTransformer (DecomposeDG p1 p2) -> RuleSelector SelectorExpression -> TheTransformer (DecomposeDG p1 p2)
- decomposeDGselect :: ExpressionSelector
- data DecomposeDGProof p1 p2
- = DecomposeDGProof {
- cpRuleSelector :: ExpressionSelector
- cpUnselected :: Trs
- cpSelected :: Trs
- cpExtensionRules :: Trs
- cpProofD :: Maybe (Proof p1)
- cpProofU :: Maybe (Proof p2)
- cpProbD :: Problem
- cpProbU :: Problem
- cpWdg :: DG
- | DecomposeDGInapplicable String
- = DecomposeDGProof {
- decomposeDGProcessor :: Transformation (DecomposeDG AnyProcessor AnyProcessor) AnyProcessor
- data DecomposeDG p1 p2
Documentation
decomposeDG :: TheTransformer (DecomposeDG AnyProcessor AnyProcessor)
This processor implements processor 'dependency graph decomposition'. 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.
solveUpperWith :: (Processor p1, Processor p2, Processor p) => TheTransformer (DecomposeDG p1 p2) -> InstanceOf p -> TheTransformer (DecomposeDG p1 p)
Specify a processor to solve the upper component immediately. The Transformation aborts if the problem cannot be handled.
solveLowerWith :: (Processor p1, Processor p2, Processor p) => TheTransformer (DecomposeDG p1 p2) -> InstanceOf p -> TheTransformer (DecomposeDG p p2)
Specify a processor to solve the lower immediately. The Transformation aborts if the problem cannot be handled.
selectLowerBy :: (Processor p1, Processor p2) => TheTransformer (DecomposeDG p1 p2) -> RuleSelector SelectorExpression -> TheTransformer (DecomposeDG p1 p2)
Specify how the lower component should be selected.
decomposeDGselect :: ExpressionSelector
This is the default RuleSelector used with decomposeDG.
Proof Object
data DecomposeDGProof p1 p2
Constructors
| DecomposeDGProof | |
Fields
| |
| DecomposeDGInapplicable String | |
Processor
data DecomposeDG p1 p2
Instances
| (Processor p1, Processor p2) => Transformer (DecomposeDG p1 p2) | |
| (Processor p1, Processor p2) => TransformationProof (DecomposeDG p1 p2) |