tct-2.0.1: A Complexity Analyser for Term Rewrite Systems

Portabilityunportable
Stabilityunstable
MaintainerMartin Avanzini <martin.avanzini@uibk.ac.at>
Safe HaskellSafe-Infered

Tct.Method.RuleSelector

Contents

Description

Rule selectors give a general method to select rules from a problem.

Synopsis

Documentation

data RuleSelector a

This datatype is used to select a subset of rules recorded in a problem.

Constructors

RuleSelector 

Fields

rsName :: String

Name of the rule selector.

rsSelect :: Problem -> a

Given a problem, computes an SelectorExpression that determines which rules to selct.

RuleSet Selectors

Constructors

selRules :: RuleSetSelector

Select rewrite rules, i.e., non dependency pair rules.

selDPs :: RuleSetSelector

Select dependency pairs.

selStricts :: RuleSetSelector

Select strict rules.

selWeaks :: RuleSetSelector

Select strict rules.

selFromWDG :: (DG -> Ruleset) -> RuleSetSelector

Select from the dependency graph, using the given function. The first parameter should specify a short name for the rule-selector.

selFromCWDG :: (CDG -> Ruleset) -> RuleSetSelector

Select from the congruence dependency graph, using the given function. The first parameter should specify a short name for the rule-selector.

Combinators

selInverse :: RuleSetSelector -> RuleSetSelector

Inverses the selection.

selCombine :: (String -> String -> String) -> (Trs -> Trs -> Trs) -> RuleSetSelector -> RuleSetSelector -> RuleSetSelector

Combine two rule-selectors component-wise.

selUnion :: RuleSetSelector -> RuleSetSelector -> RuleSetSelector

Select union of selections of given rule-selectors.

selInter :: RuleSetSelector -> RuleSetSelector -> RuleSetSelector

Select intersection of selections of given rule-selectors.

Instances Based on DG Analysis

selFirstCongruence :: RuleSetSelector

Selects all rules from root-nodes in the congruence graph.

selFirstStrictCongruence :: RuleSetSelector

Selects all rules from nodes n of the CWDG that satisfy (i) the node n references at least one strict rule, and (ii) there is no node between a root of the CWDG and n containing a strict rule.

Selector Expressions

data SelectorExpression

Defines a notion of selected rules, specified as monotone Boolean Formula. SelectorExpressions are used for instance in solvePartial to determine which rules should be oriented by a processor.

Boolean Selectors

Misc

rules :: SelectorExpression -> (Trs, Trs)

returns the pair of dps and rules mentioned in a SelectorExpression

selFirstAlternative :: ExpressionSelector -> ExpressionSelector

Selects the first alternative from the given rule selector.