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 an uninterpreted function term as defined in the SMT-Lib specification,
023: * and specialized in the (QF_)AUFLIA sublogic.
024: * <p>
025: * Each uninterpreted function is identified by its function name, which is an arbitrary legal
026: * identifier <tt>String</tt>. An identifier is legal in (QF_)AUFLIA if it begins with a letter and
027: * consists only of letters, digits and the characters '.' , '_' and ''' (single quotation mark).
028: * <p>
029: * UninterpretedFuncTerms are immutable; their attribute values cannot be changed after they
030: * are created.
031: *
032: * @author akuwertz
033: * @version 1.5, 12/04/2005 (Adjustments to changes in superclass; added further comments)
034: */
035:
036: public final class UninterpretedFuncTerm extends Term {
037:
038: /* Additional fields */
039:
040: /** The signature of this uninterpreted function */
041: private final Signature signature;
042:
043: /** A int to cache the hash code for this <tt>UninterpretedFuncTerm</tt> */
044: private int cachedHashCode;
045:
046: /* String constants for failures during Term creation */
047: private static final String creationFailurefNameNull = "Function name is null!";
048: private static final String creationFailurefNameIllgSymb = "Function name is no legal identifier!";
049: private static final String creationFailurefArgsContNull = "Function argument array contains a null pointer at position !";
050: private static final String creationFailureSigNull = "Signature is null!";
051: private static final String creationFailureArity = "Argument count does not match signature!";
052: private static final String creationFailureInterpreted = "Operator is interpreted!";
053:
054: /* Constructor */
055:
056: /** Creates a new <tt>UninterpretedFuncTerm</tt>, representing an uninterpreted function.
057: * <p>
058: * Every uninterpreted function is associated with a signature. It contains one more sort symbol
059: * than the function contains arguments; the last sort symbol represents the return type of this
060: * <tt>UninterpretedFuncTerm</tt>
061: * <p>
062: * To create an uninterpreted constant, <tt>fArgs</tt> can be either <tt>null</tt> or an empty
063: * array; choosing <tt>null</tt> reduces the memory footprint through shared objects
064: *
065: * @param fName the name of the uninterpreted function
066: * @param fArgs the array of function arguments
067: * @param sig the signature of this uninterpreted function
068: * @throws NullPointerException if <tt>fName</tt> or <tt>sig</tt> is <tt>null</tt>
069: * or if <tt>fArgs</tt> contains a null pointer
070: * @throws IllegalArgumentException if <tt>fName</tt> is no legal identifier in (QF_)AUFLIA or
071: * if it equals an interpreted symbol or if the given signature
072: * does not match the function argument count
073: */
074: public UninterpretedFuncTerm(String fName, Term[] fArgs,
075: Signature sig) {
076: super (fName, fArgs, Term.marker, null);
077:
078: // Check if fName is syntactically correct and if arguments are not null
079: if (fName == null)
080: throw new NullPointerException(creationFailurefNameNull);
081: if (!isLegalIdentifier(fName))
082: throw new IllegalArgumentException(
083: creationFailurefNameIllgSymb);
084: if (fArgs != null) {
085: for (int i = 0; i < fArgs.length; i++)
086: if (fArgs[i] == null)
087: throw new NullPointerException(
088: creationFailurefArgsContNull + i);
089: }
090: if (sig == null)
091: throw new NullPointerException(creationFailureSigNull);
092:
093: // Check that fName doesn't equal an interpreted symbol
094: String[] interpretedOps = DecisionProcedureSmtAufliaOp
095: .getAllSmtOperators();
096: for (int i = 0; i < interpretedOps.length; i++) {
097: if (fName.equals(interpretedOps[i]))
098: throw new IllegalArgumentException(
099: creationFailureInterpreted);
100: }
101:
102: // Check if signature and arguments match
103: if (fArgs == null) {
104: if (sig.getLength() != 1)
105: throw new IllegalArgumentException(creationFailureArity);
106: } else if (fArgs.length + 1 != sig.getLength()) {
107: throw new IllegalArgumentException(creationFailureArity);
108: }
109:
110: // Ok, set additional fields: signatures are immutable
111: signature = sig;
112: }
113:
114: // Public method implementation
115:
116: /* (non-Javadoc)
117: * @see de.uka.ilkd.key.proof.decproc.smtlib.Term#equals(de.uka.ilkd.key.proof.decproc.smtlib.Term)
118: */
119: public boolean equals(Object o) {
120: if (this == o)
121: return true;
122: if (super .equals(o)) {
123: if (o instanceof UninterpretedFuncTerm) {
124: UninterpretedFuncTerm t = (UninterpretedFuncTerm) o;
125: return signature.equals(t.getSignature());
126: }
127: }
128: return false;
129: }
130:
131: /** Returns an int value representing the hash code of this <tt>UninterpretedFuncTerm</tt>.
132: * <p>
133: * This hash code is calculated by combining the <tt>Term</tt> hash code of this
134: * <tt>UninterpretedFuncTerm</tt> with the hash code of its <tt>Signature</tt>
135: *
136: * @return the hash code of this <tt>UninterpretedFuncTerm</tt>
137: */
138: public int hashCode() {
139: if (cachedHashCode == 0) {
140: cachedHashCode = 37 * super .hashCode()
141: + signature.hashCode();
142: }
143: return cachedHashCode;
144: }
145:
146: /* (non-Javadoc)
147: * @see de.uka.ilkd.key.proof.decproc.smtlib.Term#toString()
148: */
149: public String toString() {
150: Term[] this FuncArgs = getFuncArgs();
151: // An uninterpreted constant has got no brackets
152: if (this FuncArgs.length == 0)
153: return getFunction();
154: String representation = "(" + getFunction();
155: for (int i = 0; i < this FuncArgs.length; i++) {
156: representation += " " + this FuncArgs[i].toString();
157: }
158: representation += ")";
159: return representation;
160: }
161:
162: /** Returns the signature of this <tt>UninterpretedFuncTerm</tt>
163: *
164: * @return the signature of this <tt>UninterpretedFuncTerm</tt>
165: */
166: public Signature getSignature() {
167: return signature;
168: }
169:
170: /* (non-Javadoc)
171: * @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)
172: */
173: public Term replaceTermVar(TermVariable termVar, Term replacement) {
174: if (!containsTerm(termVar))
175: return this ;
176: Term[] newSubterms = getFuncArgs();
177: for (int i = 0; i < newSubterms.length; i++) {
178: newSubterms[i] = newSubterms[i].replaceTermVar(termVar,
179: replacement);
180: }
181: return new UninterpretedFuncTerm(getFunction(), newSubterms,
182: signature);
183: }
184:
185: /* (non-Javadoc)
186: * @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)
187: */
188: public Term replaceFormVarIteTerm(FormulaVariable formVar,
189: Formula replacement) {
190: if (!containsFormulaIteTerm(formVar))
191: return this ;
192: Term[] newFuncArgs = getFuncArgs();
193: for (int i = 0; i < newFuncArgs.length; i++) {
194: newFuncArgs[i] = newFuncArgs[i].replaceFormVarIteTerm(
195: formVar, replacement);
196: }
197: return new UninterpretedFuncTerm(getFunction(), newFuncArgs,
198: signature);
199: }
200: }
|