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 predicate formula as defined in the SMT-Lib specification, and
023: * specialized in the (QF_)AUFLIA sublogic.
024: * <p>
025: * Uninterpreted predicates are identified by their top-level operator, i.e. their name. This name
026: * therefore has to be a legal identifier in (QF_)AUFLIA, i.e. it must begin with a letter and may
027: * consist only of letters, digits and the characters '.' , '_' and ''' (single quotation mark).
028: * <br> Uninterpreted predicates are treated as non commutative predicates.
029: * <p>
030: * UninterpretedPredFormula are immutable; their attribute values cannot be changed after they
031: * are created.
032: *
033: * @author akuwertz
034: * @version 1.5, 12/11/2005 (Adjustments to superclass V1.5; further comments)
035: */
036:
037: public final class UninterpretedPredFormula extends Formula {
038:
039: /* Additional fields */
040:
041: /** The signature of this <tt>UninterpretedPredFormula</tt> */
042: private final Signature signature;
043:
044: /* String constants for failures during Formula creation */
045: private static final String creationFailureOpNull = "Operator is null!";
046: private static final String creationFailureOpIllgId = "Operator is no legal identifier!";
047: private static final String creationFailureSubsContNull = "Subterm array contains a null pointer at position ";
048: private static final String creationFailureSigNull = "The signature is null!";
049: private static final String creationFailureArity = "Argument count does not match function arity!";
050: private static final String creationFailureInterpreted = "Operator is an interpreted one!";
051:
052: /* Constructor */
053:
054: /** Creates a new <tt>UninterpretedPredFormula</tt> representing an uninterpreted predicate.
055: * <p>
056: * Every uninterpreted predicate is associated with a signature, which describes the number
057: * and sorts of <tt>Term</tt> arguments of this <tt>UninterpretedPredFormula</tt>
058: * <p>
059: * To create an uninterpreted constant, <tt>subTerms</tt> can be either <tt>null</tt> or an
060: * empty array; choosing <tt>null</tt> reduces the memory footprint through shared objects
061: *
062: * @param op the name assigned to the uninterpreted predicate to be represented
063: * @param subTerms the array of argument <tt>Term</tt>s of this
064: * <tt>UninterpretedPredFormula</tt>
065: * @param sig the signature of this <tt>UninterpretedPredFormula</tt>
066: * @throws NullPointerException if <tt>op</tt> or <tt>sig</tt> or one of the <tt>Term</tt>s
067: * contained in <tt>subTerms</tt> is <tt>null</tt>
068: * @throws IllegalArgumentException
069: */
070: public UninterpretedPredFormula(String op, Term[] subTerms,
071: Signature sig) {
072: super (op, null, subTerms, true);
073: if (op == null)
074: throw new NullPointerException(creationFailureOpNull);
075: if (subTerms != null) {
076: for (int i = 0; i < subTerms.length; i++)
077: if (subTerms[i] == null)
078: throw new NullPointerException(
079: creationFailureSubsContNull + i);
080: }
081: if (sig == null)
082: throw new NullPointerException(creationFailureSigNull);
083:
084: // Check if op is syntactically correct
085: if (!isLegalIdentifier(op))
086: throw new IllegalArgumentException(creationFailureOpIllgId);
087:
088: // Check if the operator op equals an interpreted operator. If yes, throw Exception.
089: String[] interpretedOps = DecisionProcedureSmtAufliaOp
090: .getAllSmtOperators();
091: for (int i = 0; i < interpretedOps.length; i++) {
092: if (interpretedOps[i].equals(op))
093: throw new IllegalArgumentException(
094: creationFailureInterpreted);
095: }
096:
097: // Argument count and signature length must be equal
098: if (subTerms == null) {
099: if (sig.getLength() != 0)
100: throw new IllegalArgumentException(creationFailureArity);
101: } else if (subTerms.length != sig.getLength()) {
102: throw new IllegalArgumentException(creationFailureArity);
103: }
104:
105: // Set signature
106: signature = sig;
107: }
108:
109: // Public method implementation
110:
111: /* (non-Javadoc)
112: * @see de.uka.ilkd.key.proof.decproc.smtlib.Formula#equals(java.lang.Object)
113: */
114: public boolean equals(Object o) {
115: if (o == this )
116: return true;
117: if (super .equals(o)) {
118: // Uninterpreted predicates are treated non commutativ
119: return (o instanceof UninterpretedPredFormula);
120: }
121: return false;
122: }
123:
124: /** Returns an int value representing the hash code of this <tt>UninterpretedPredFormula</tt>.
125: * <p>
126: * This hash code is calculated by combining the <tt>Formula</tt> hash code of this
127: * <tt>UninterpretedPredFormula</tt> with the hash code of its <tt>Signature</tt>
128: *
129: * @return the hash code of this <tt>UninterpretedPredFormula</tt>
130: */
131: public int hashCode() {
132: return 37 * super .hashCode() + signature.hashCode();
133: }
134:
135: /* (non-Javadoc)
136: * @see de.uka.ilkd.key.proof.decproc.smtlib.Formula#toString()
137: */
138: public String toString() {
139: Term[] this Subterms = getSubterms();
140: if (this Subterms.length == 0)
141: return getOp();
142: String representation = "(" + getOp();
143: for (int i = 0; i < this Subterms.length; i++) {
144: representation += " " + this Subterms[i].toString();
145: }
146: representation += ")";
147: return representation;
148: }
149:
150: /** Returns the signature of this <tt>UninterpretedPredFormula</tt>
151: *
152: * @return the signature of this <tt>UninterpretedPredFormula</tt>
153: */
154: public Signature getSignature() {
155: return signature;
156: }
157:
158: /* (non-Javadoc)
159: * @see de.uka.ilkd.key.proof.decproc.smtlib.Formula#replaceFormVar(de.uka.ilkd.key.proof.decproc.smtlib.FormulaVariable, de.uka.ilkd.key.proof.decproc.smtlib.Formula)
160: */
161: public Formula replaceFormVar(FormulaVariable formVar,
162: Formula replacement) {
163: if (!containsFormula(formVar))
164: return this ;
165: Term[] newSubterms = getSubterms();
166: for (int i = 0; i < newSubterms.length; i++) {
167: newSubterms[i] = newSubterms[i].replaceFormVarIteTerm(
168: formVar, replacement);
169: }
170: return new UninterpretedPredFormula(getOp(), newSubterms,
171: signature);
172: }
173:
174: /* (non-Javadoc)
175: * @see de.uka.ilkd.key.proof.decproc.smtlib.Formula#replaceTermVar(de.uka.ilkd.key.proof.decproc.smtlib.TermVariable, de.uka.ilkd.key.proof.decproc.smtlib.Term)
176: */
177: public Formula replaceTermVar(TermVariable termVar, Term replacement) {
178: if (!containsTerm(termVar))
179: return this ;
180: Term[] newSubterms = getSubterms();
181: for (int i = 0; i < newSubterms.length; i++) {
182: newSubterms[i] = newSubterms[i].replaceTermVar(termVar,
183: replacement);
184: }
185: return new UninterpretedPredFormula(getOp(), newSubterms,
186: signature);
187: }
188: }
|