001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //This file is part of KeY - Integrated Deductive Software Design
009: //Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
010: // Universitaet Koblenz-Landau, Germany
011: // Chalmers University of Technology, Sweden
012: //
013: //The KeY system is protected by the GNU General Public License.
014: //See LICENSE.TXT for details.
015: //
016: //
017:
018: package de.uka.ilkd.key.proof.decproc.smtlib;
019:
020: import de.uka.ilkd.key.proof.decproc.DecisionProcedureSmtAufliaOp;
021:
022: /** Represents a term variable as defined in the SMT-Lib specification, and specialized
023: * in the (QF_)AUFLIA sublogic. Thereby a term variable is a variable (identifier) that
024: * respresent an arbitrary term. The identifier is a String, starting with a letter and
025: * containing only letters, digits, "_", "'" and "."
026: * <p>
027: * TermsVariables are immutable; their attribute values cannot be changed once they are
028: * created.
029: *
030: * @author akuwertz
031: * @version 1.5, 09/29/2006 (Added signatures to term variables)
032: */
033:
034: public final class TermVariable extends Term {
035:
036: /* Additional fields */
037:
038: /** String constant, representing the term variable prefix in AUFLIA */
039: private static final String termVarPrefix = "?";
040:
041: /** A <tt>Signature</tt> representing the sort of this <tt>TermVariable</tt> */
042: private final Signature sort;
043:
044: /** A int to cache the hash code for this <tt>TermVariable</tt> */
045: private int cachedHashCode;
046:
047: /* String constants for failures during Term creation */
048: private static final String creationFailureIdNull = "Variable name is null!";
049: private static final String creationFailureIdIllg = "Variable name is no legal identifier!!";
050: private static final String creationFailureInterpreted = "Variable name equals an interpreted operator!";
051: private static final String creationFailureSigNull = "The signature is null!";
052: private static final String creationFailureWrongSig = "The signature must contain exactly one sort";
053:
054: /* Constructor */
055:
056: /** Creates a new <tt>TermVariable</tt>
057: *
058: * @param varName the identifier of the <tt>Term</tt> variable to be represented
059: * @param sig the <tt>Signature</tt> denoting the sort of this <tt>Term</tt> variable
060: * @throws NullPointerException if <tt>varName</tt> is <tt>null</tt>
061: * @throws IllegalArgumentException if <tt>varName</tt> contains an illegal character
062: * or equals an interpreted symbol in (QF_)AUFLIA
063: */
064: public TermVariable(String varName, Signature sig) {
065: super (varName, new Term[0], null, null);
066:
067: // Check if varName is syntactically correct
068: if (varName == null)
069: throw new NullPointerException(creationFailureIdNull);
070: if (!isLegalIdentifier(varName))
071: throw new IllegalArgumentException(creationFailureIdIllg);
072:
073: // Check if varName equals an interpreted operator in AUFLIA
074: String[] interpretedOps = DecisionProcedureSmtAufliaOp
075: .getAllSmtOperators();
076: for (int i = 0; i < interpretedOps.length; i++) {
077: if (varName.equals(interpretedOps[i]))
078: throw new IllegalArgumentException(
079: creationFailureInterpreted);
080: }
081:
082: if (sig == null)
083: throw new NullPointerException(creationFailureSigNull);
084: if (sig.getLength() != 1)
085: throw new IllegalArgumentException(creationFailureWrongSig);
086: sort = sig;
087: }
088:
089: // Public method implementation
090:
091: /* (non-Javadoc)
092: * @see de.uka.ilkd.key.proof.decproc.smtlib.Term#equals(de.uka.ilkd.key.proof.decproc.smtlib.Term)
093: */
094: public boolean equals(Object o) {
095: if (this == o)
096: return true;
097: if (super .equals(o)) {
098: if (o instanceof TermVariable)
099: return sort.equals(((TermVariable) o).getSignature());
100: }
101: return false;
102: }
103:
104: /** Returns an int value representing the hash code of this <tt>TermVariable</tt>.
105: * <p>
106: * This hash code is calculated by combining the <tt>Term</tt> hash code of this
107: * <tt>TermVariable</tt> with the hash code of its <tt>Signature</tt>
108: *
109: * @return the hash code of this <tt>TermVariable</tt>
110: */
111: public int hashCode() {
112: if (cachedHashCode == 0) {
113: cachedHashCode = 37 * super .hashCode() + sort.hashCode();
114: }
115: return cachedHashCode;
116: }
117:
118: /* (non-Javadoc)
119: * @see de.uka.ilkd.key.proof.decproc.smtlib.Term#toString()
120: */
121: public String toString() {
122: return termVarPrefix + getFunction();
123: }
124:
125: /* (non-Javadoc)
126: * @see de.uka.ilkd.key.proof.decproc.smtlib.Term#replaceTermVar(de.uka.ilkd.key.proof.decproc.smtlib.TermVariable, de.uka.ilkd.key.proof.decproc.smtlib.Term)
127: */
128: public Term replaceTermVar(TermVariable termVar, Term replacement) {
129: // If this TermVariable is to be replaced, do it, otherwise let it unchanged
130: return equals(termVar) ? replacement : this ;
131: }
132:
133: /* (non-Javadoc)
134: * @see de.uka.ilkd.key.proof.decproc.smtlib.Term#replaceFormVarIteTerm(de.uka.ilkd.key.proof.decproc.smtlib.FormulaVariable, de.uka.ilkd.key.proof.decproc.smtlib.Formula)
135: */
136: public Term replaceFormVarIteTerm(FormulaVariable formVar,
137: Formula replacement) {
138: return this ;
139: }
140:
141: /** Returns the signature (sort) of this <tt>TermVariable</tt>
142: *
143: * @return the signature of this <tt>TermVariable</tt>
144: */
145: public Signature getSignature() {
146: return sort;
147: }
148: }
|