Raptor.LogicParser.Formula
Class LLVar

java.lang.Object
  extended by Raptor.LogicParser.Formula.Term
      extended by Raptor.LogicParser.Formula.LLVar
All Implemented Interfaces:
java.io.Serializable, java.lang.Cloneable

public class LLVar
extends Term

Creates an length variable term for an array used in the proof.
Extends abstract class Term.

See Also:
Serialized Form

Constructor Summary
LLVar(java.lang.String pName)
          Constructs a new length variable.
 
Method Summary
 void addToSignature(PanSignature pSignature)
          This method adds this Term to the passed PanSignature IF it is not already in the signature.
 java.lang.String clashes(PanSignature pSignature)
          Returns a String of error message if this Term clashes with the passed PanSignature.
 LLVar clone()
          Returns a copy(clone) of this Term.
 java.lang.String display()
          Returns a String to display the length variable.
 boolean equals(Term pTerm)
          Returns true if the passed Term is equal to this Term.
 java.lang.String getName()
          Returns the name of the Term.
 boolean isIn(PanSignature pSignature)
          Returns true if this Term is in the passed PanSignature
 Term regenerate()
          Returns a new copy of this Term
 void setVars(Var pVar)
          This method adds Var v to the list of variables this Term is bound to.
 Term sub(Term pTermX, Term pTermY)
          Substitutes all the occurrences of Term pTermX by Term pTermY.
 
Methods inherited from class Raptor.LogicParser.Formula.Term
concatNoDup, getVars, isIn, isInVars
 
Methods inherited from class java.lang.Object
equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Constructor Detail

LLVar

public LLVar(java.lang.String pName)
Constructs a new length variable.

Parameters:
pName - the name of the length variable
Method Detail

display

public java.lang.String display()
Returns a String to display the length variable.

Specified by:
display in class Term

equals

public boolean equals(Term pTerm)
Returns true if the passed Term is equal to this Term.

Overrides:
equals in class Term
Parameters:
pTerm - represents the Term to be compared against.

sub

public Term sub(Term pTermX,
                Term pTermY)
Substitutes all the occurrences of Term pTermX by Term pTermY.

Specified by:
sub in class Term
Parameters:
pTermX - represents the Term to be substituted.
pTermY - represents the Term to substitute the Term pTermX with.

clone

public LLVar clone()
Returns a copy(clone) of this Term.

Specified by:
clone in class Term

clashes

public java.lang.String clashes(PanSignature pSignature)
Returns a String of error message if this Term clashes with the passed PanSignature.

Specified by:
clashes in class Term
Parameters:
pSignature - PanSignature Represents the signature to be compared against.

getName

public java.lang.String getName()
Returns the name of the Term.

Specified by:
getName in class Term

addToSignature

public void addToSignature(PanSignature pSignature)
This method adds this Term to the passed PanSignature IF it is not already in the signature.

Specified by:
addToSignature in class Term
Parameters:
pSignature - PanSignature represents the signature to add this Formula to.

isIn

public boolean isIn(PanSignature pSignature)
Returns true if this Term is in the passed PanSignature

Specified by:
isIn in class Term
Parameters:
pSignature - PanSignature represents the signature it is to be searched in.

setVars

public void setVars(Var pVar)
This method adds Var v to the list of variables this Term is bound to.

Specified by:
setVars in class Term
Parameters:
pVar - Var represents the Var to be added to the list of this Term's variables.

regenerate

public Term regenerate()
Returns a new copy of this Term