kites.logic
Class CheckTRS

java.lang.Object
  extended by kites.logic.CheckTRS

public class CheckTRS
extends java.lang.Object

This class is able to perform various syntax checks on TRSs. These syntax checks are needed to decide whether the TRS can be interpreted at all, and in which mode.


Field Summary
(package private)  TRSFile rulelist
           
 
Constructor Summary
CheckTRS(TRSFile rulelist)
           
 
Method Summary
 void checkLeftLinear()
          Check whether all the rules in the ruleset are left-linear.
private  void CheckVarRightSide(ASTNode node, java.util.HashSet<java.lang.String> variables)
          Checks whether variables not in variables is present in the tree node and throws a SyntaxErrorException if this is the case.
private  java.util.HashMap<java.lang.String,java.lang.Integer> gammaSigNode(ASTNode node, java.util.HashMap<java.lang.String,java.lang.Integer> signature)
          Create the Gamma-signature for a tree.
private  java.util.HashMap<java.lang.String,java.lang.Integer> getGammaSignature()
          Create the Gamma-signature of the rule set.
private  java.util.HashMap<java.lang.String,java.lang.Integer> getSigmaSignature()
          Create the Sigma-signature of the rule set.
private  java.util.HashSet<java.lang.String> GetVariables(ASTNode node, java.util.HashSet<java.lang.String> variables)
          Creates a set of variables used in a tree.
static void instanceCheck(ASTNode node, java.util.HashMap<java.lang.String,java.lang.Integer> signature)
          Check an instance for its compliance with a given signature.
private  void isLeftLinear(ASTNode tree, java.util.HashSet<java.lang.String> varSet)
          Checks whether a tree is linear, i.
 void isSigmaGammaInstance(ASTNode instance)
          Checks whether an instance conforms to the Sigma- Gamma-signatures given by the rule set.
 void isSigmaGammaSystem()
          Checks whether the given rule set is a Sigma-Gamma- program system.
private  void sigCheckNode(java.util.HashMap<java.lang.String,java.lang.Integer> signature, ASTNode node)
          Create the signature for a (sub-) tree.
private  java.util.HashMap<java.lang.String,java.lang.Integer> sigmaSigNode(ASTNode node, java.util.HashMap<java.lang.String,java.lang.Integer> signature, boolean root)
          Create the Sigma-signature of a tree, adding to a previously existing signature.
 java.util.HashMap<java.lang.String,java.lang.Integer> signatureCheck()
          Check whether the rule system is consistent, i.
 void unifiabilityCheck()
          Checks whether two rules in the rule set are unifiable.
private  boolean unifiable(ASTNode left, ASTNode right)
          Checks whether two trees are unifiable.
 void variableCheck()
          Check the set of rules for their compliance with left-linearity and also check whether there are variables used on the right-hand side of a rule that were not used on the left-hand side.
private  void variableCheckRule(Rule rule)
          Check for left-linearity of a rule.
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

rulelist

TRSFile rulelist
Constructor Detail

CheckTRS

public CheckTRS(TRSFile rulelist)
Parameters:
rulelist - The TRS object that the checks shall be performed upon
Method Detail

isSigmaGammaInstance

public void isSigmaGammaInstance(ASTNode instance)
                          throws SyntaxErrorException
Checks whether an instance conforms to the Sigma- Gamma-signatures given by the rule set. If not, a SyntaxErrorException with a meaningful message is thrown. Basically, this just tests whether the root node of the instance is a symbol from the Gamma signature.

Parameters:
instance - The instance to be checked
Throws:
SyntaxErrorException

isSigmaGammaSystem

public void isSigmaGammaSystem()
                        throws SyntaxErrorException
Checks whether the given rule set is a Sigma-Gamma- program system. First it creates both signatures then performs the following checks: - do they overlap? This would mean there is at least one rule that starts with a Sigma-symbol Throws a SyntaxErrorException with a meaningful message if any check fails.

Throws:
SyntaxErrorException

getGammaSignature

private java.util.HashMap<java.lang.String,java.lang.Integer> getGammaSignature()
                                                                         throws SyntaxErrorException
Create the Gamma-signature of the rule set. In a program system the root node in the tree representing a left-hand side of a rule needs to belong to the Gamma- signature, which is created by this method

Returns:
the signature as a map: name --> arity
Throws:
SyntaxErrorException

gammaSigNode

private java.util.HashMap<java.lang.String,java.lang.Integer> gammaSigNode(ASTNode node,
                                                                           java.util.HashMap<java.lang.String,java.lang.Integer> signature)
                                                                    throws SyntaxErrorException
Create the Gamma-signature for a tree. Checks whether the root node is already in the signature. If not, it is added. If a node is found to contradict the signature a SyntaxErrorException is thrown. This is also the case when a tree with a Variable as root is detected.

Parameters:
node - The tree to genereate the signature from
signature - The signature to which entries shall be added
Returns:
The new signature
Throws:
SyntaxErrorException

getSigmaSignature

private java.util.HashMap<java.lang.String,java.lang.Integer> getSigmaSignature()
                                                                         throws SyntaxErrorException
Create the Sigma-signature of the rule set. In a program system all nodes except the root node in the tree representing a left-hand side of a rule need to belong to the Sigma-signature, which is created by this method.

Returns:
The Sigma-signature of the rule set
Throws:
SyntaxErrorException - When signature is found to be contradicted by a wrong parameter count

sigmaSigNode

private java.util.HashMap<java.lang.String,java.lang.Integer> sigmaSigNode(ASTNode node,
                                                                           java.util.HashMap<java.lang.String,java.lang.Integer> signature,
                                                                           boolean root)
                                                                    throws SyntaxErrorException
Create the Sigma-signature of a tree, adding to a previously existing signature.

Parameters:
node - The tree to be checked
signature - The pre-existing signature
root - Indicates whether we are at the root of the tree
Throws:
SyntaxErrorException - On encountering a node contradicting the signature

instanceCheck

public static void instanceCheck(ASTNode node,
                                 java.util.HashMap<java.lang.String,java.lang.Integer> signature)
                          throws SyntaxErrorException
Check an instance for its compliance with a given signature. This only checks for correct parameter count, not for consistency with a Gamma-Signature as needed for interpretation as a program. Use instanceCheckGamma for that! This also checks that there are no Variables present in the instance. If a violation occurs, a SyntaxErrorException is thrown.

Parameters:
node - The instance to be checked
signature - The signature to be checked against.
Throws:
SyntaxErrorException

unifiabilityCheck

public void unifiabilityCheck()
                       throws SyntaxErrorException
Checks whether two rules in the rule set are unifiable. If that is the case a SyntaxErrorException is thrown.

Throws:
SyntaxErrorException

unifiable

private boolean unifiable(ASTNode left,
                          ASTNode right)
                   throws SyntaxErrorException
Checks whether two trees are unifiable.

Parameters:
left - The one tree
right - The other tree
Returns:
true when trees are unifiable, false otherwise.
Throws:
SyntaxErrorException

signatureCheck

public java.util.HashMap<java.lang.String,java.lang.Integer> signatureCheck()
                                                                     throws SyntaxErrorException
Check whether the rule system is consistent, i. e. whether nodes with the same name always have the same parameter count. The first occurence of a node determines the signature. If a mismatch is encountered this throws a SyntaxErrorException.

Returns:
The signature of the rule set
Throws:
SyntaxErrorException

sigCheckNode

private void sigCheckNode(java.util.HashMap<java.lang.String,java.lang.Integer> signature,
                          ASTNode node)
                   throws SyntaxErrorException
Create the signature for a (sub-) tree. Checks the tree for compliance with an already existing signature and adds new nodes that are not yet present in the signature. If a mismatch is encountered, this throws a SyntaxErrorException

Parameters:
signature - The pre-existing signature
node - The node to be checked
Throws:
SyntaxErrorException

variableCheck

public void variableCheck()
                   throws SyntaxErrorException
Check the set of rules for their compliance with left-linearity and also check whether there are variables used on the right-hand side of a rule that were not used on the left-hand side. When violations occur, a SyntaxErrorException is thrown.

Throws:
SyntaxErrorException

variableCheckRule

private void variableCheckRule(Rule rule)
                        throws SyntaxErrorException
Check for left-linearity of a rule. This gathers a list of the variables used on the left-hand side of a rule. If a variable is used more than once on the left-hand side this throws a SyntaxErrorException with an appropriate message. Then the method goes on and checks if a variable that was not used on the left-hand side was used on the right-hand side. If this is the case, a SyntaxErrorException with an appropriate message is thrown.

Parameters:
rule - The rule to be checked
Throws:
SyntaxErrorException - See description

CheckVarRightSide

private void CheckVarRightSide(ASTNode node,
                               java.util.HashSet<java.lang.String> variables)
                        throws SyntaxErrorException
Checks whether variables not in variables is present in the tree node and throws a SyntaxErrorException if this is the case.

Parameters:
node - The (sub-) tree to be checked
variables - Set of variables to check against
Throws:
SyntaxErrorException

GetVariables

private java.util.HashSet<java.lang.String> GetVariables(ASTNode node,
                                                         java.util.HashSet<java.lang.String> variables)
                                                  throws SyntaxErrorException
Creates a set of variables used in a tree. If a variable is encountered more than once, a SyntaxErrorException is thrown, as this violates left-linearity.

Parameters:
node - The tree to be checked
variables - Temporary cache of already gathered variables. Initialize with an empty HashSet unless you know what you are doing.
Returns:
The set of variables used in the tree
Throws:
SyntaxErrorException

checkLeftLinear

public void checkLeftLinear()
                     throws SyntaxErrorException
Check whether all the rules in the ruleset are left-linear. This means that a variable may not appear more than once on the left-hand side of a rule. This is a prerequisite for interpretation in program mode, as systems without this property may not be confluent.

Throws:
SyntaxErrorException - If a rule is not left-linear.

isLeftLinear

private void isLeftLinear(ASTNode tree,
                          java.util.HashSet<java.lang.String> varSet)
                   throws SyntaxErrorException
Checks whether a tree is linear, i. e. that no variable appears more than once in it.

Parameters:
tree - The tree to be checked
varSet - A pre-existing number of variables. This should be initialized as an empty set.
Throws:
SyntaxErrorException - If the tree is not linear.