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 java.util.Vector;
021:
022: import de.uka.ilkd.key.proof.decproc.DecisionProcedureSmtAufliaOp;
023:
024: /** Represents a predicate formula as defined in the SMT-Lib specification, and specialized
025: * in the (QF_)AUFLIA sublogic.
026: * <p>
027: * Thereby only the predicates '=', '<=', '<', '>=' and '>' are supported in (QF_)AUFLIA; for
028: * convenience there's also the 'distinct'-construct.
029: * <p>
030: * PredicateFormula are immutable; their attribute values cannot be changed after they are created.
031: *
032: * @author akuwertz
033: * @version 1.3, 12/09/2005 (Adjustments to superclass V1.5, further comments)
034: */
035:
036: public final class PredicateFormula extends Formula {
037:
038: /* Additional fields */
039:
040: /** A int used to cache the hash code of this <tt>PredicateFormula</tt> if it represents a
041: * commutative function */
042: private int cachedCommHashCode;
043:
044: /* String constants for failures during Formula creation */
045: private static final String creationFailureOpNull = "Operator is null!";
046: private static final String creationFailureSubsNull = "Subterm array is null!";
047: private static final String creationFailureSubsContNull = "Subterm array contains a null pointer at position ";
048: private static final String creationFailureArity = "Argument count does not match function arity!";
049: private static final String creationFailureNoPred = "Operator is not a predicate symbol!";
050:
051: /* An array of all interpreted predicate symbols */
052: private static final String[] predicateSymbols = {
053: DecisionProcedureSmtAufliaOp.GEQ,
054: DecisionProcedureSmtAufliaOp.GT,
055: DecisionProcedureSmtAufliaOp.LEQ,
056: DecisionProcedureSmtAufliaOp.LT,
057: DecisionProcedureSmtAufliaOp.EQUALS,
058: DecisionProcedureSmtAufliaOp.DISTINCT };
059:
060: /* Constructor */
061:
062: /** Creates a new <tt>PredicateFormula</tt> representing an interpreted predicate.
063: * <p>
064: * The predicate symbol <tt>op</tt> must be one of the static <tt>String</tt>s defined in
065: * <tt>DecisionProcedureSmtAufliaOp</tt>. Namely, these are EQUALS, GEQ, GT, LEQ, LT and DISTINCT.
066: * <p>
067: * All mentioned predicates but the DISTINCT predicate are of arity two. For DISTINCT, any
068: * integer value greater than one is allowed as number of argument <tt>Term</tt>s.<br>
069: * Only the DISTINCT and the EQUALS predicate are commutative
070: *
071: * @param op the predicate symbol to be represented
072: * @param subTerms the array of <tt>Term</tt> arguments of this <tt>PredicateFormula</tt>
073: * @throws NullPointerException if <tt>op</tt> or one of the <tt>Term</tt>s contained
074: * in <tt>subTerms</tt> is <tt>null</tt>
075: * @throws IllegalArgumentException if <tt>op</tt> represents no interpreted predicate in
076: * (QF_)AUFLIA or if the specified argument <tt>Term</tt>s
077: * don't match the predicate arity
078: *
079: * @see de.uka.ilkd.key.logic.op.DecisionProcedureSmtAufliaOp
080: */
081: public PredicateFormula(String op, Term[] subTerms) {
082: super (op, null, subTerms);
083: if (op == null)
084: throw new NullPointerException(creationFailureOpNull);
085: if (subTerms == null)
086: throw new NullPointerException(creationFailureSubsNull);
087: for (int i = 0; i < subTerms.length; i++) {
088: if (subTerms[i] == null)
089: throw new NullPointerException(
090: creationFailureSubsContNull + i);
091: }
092:
093: // Check if operator is a predicate symbol
094: boolean isPredicate = false;
095: for (int i = 0; i < predicateSymbols.length; i++) {
096: if (op == predicateSymbols[i]) {
097: isPredicate = true;
098: i = predicateSymbols.length;
099: }
100: }
101: if (!isPredicate)
102: throw new IllegalArgumentException(creationFailureNoPred);
103:
104: // Check arity
105: if ((op != DecisionProcedureSmtAufliaOp.DISTINCT & subTerms.length != 2)
106: | (op == DecisionProcedureSmtAufliaOp.DISTINCT & subTerms.length < 2))
107: throw new IllegalArgumentException(creationFailureArity);
108: }
109:
110: // Public method implementation
111:
112: /**
113: * Compares this <tt>Formula</tt> to the specified <tt>Object</tt> <tt>o</tt>.
114: * <p>
115: * This <tt>PredicateFormula</tt> is considered equal to <tt>o</tt> if <tt>o</tt> is an
116: * instance of <tt>PredicateFormula</tt> and has the same subterms as this
117: * <tt>PredicateFormula</tt>.<br>
118: * If the represented predicate is commutative, i.e. if this <tt>PredicateFormula</tt>
119: * represents the EQU or DISTINCT predicate, the order of arguments does not matter for
120: * equality. For all other interpreted predicates in (QF_)AUFLIA, the order of arguments matters
121: * for equality.
122: *
123: * @param o
124: * the <tt>Object</tt> to compare with
125: * @return true if this <tt>PredicateFormula</tt> is the same as the specified <tt>Object</tt>;
126: * otherwise false.
127: */
128: public boolean equals(Object o) {
129: if (o == this )
130: return true;
131: if (o instanceof PredicateFormula) {
132: // Non commutative predicates, and commutative with same argument order
133: if (super .equals(o))
134: return true;
135: // Commutative predicates (argument order does not matter)
136: PredicateFormula f = (PredicateFormula) o;
137: String this Op = getOp();
138: if (this Op == DecisionProcedureSmtAufliaOp.DISTINCT
139: | this Op == DecisionProcedureSmtAufliaOp.EQUALS) {
140: Vector subterms = toVector(getSubterms());
141: Vector fSubterms = toVector(f.getSubterms());
142: if (subterms.containsAll(fSubterms)
143: && fSubterms.containsAll(subterms))
144: return true;
145: }
146: }
147: return false;
148: }
149:
150: /** Returns an int value representing the hash code of this <tt>PredicateFormula</tt>.
151: * <p>
152: * The hash code for a <tt>PredicateFormula</tt> is calculated by combining the hash code of
153: * its predicate symbol (operator) with the hash codes of its <tt>Term</tt> arguments.
154: * <p>
155: * If this <tt>PredicateFormula</tt> represents a commutative predicate, i.e. if it represents
156: * the EQU or DISTINCT predicate, the order of <tt>Term</tt> arguments doesn't not matter for
157: * the calculation, otherwise it does
158: *
159: * @return the hash code of this <tt>PredicateFormula</tt>
160: */
161: public int hashCode() {
162: String this Op = getOp();
163: // Non commutative predicates
164: if (this Op != DecisionProcedureSmtAufliaOp.EQUALS
165: && this Op != DecisionProcedureSmtAufliaOp.DISTINCT) {
166: return super .hashCode();
167: }
168: // Commutative predicates
169: if (cachedCommHashCode == 0) {
170: Term[] this Subterms = getSubterms();
171: int result = 17;
172: result = 37 * result + this Op.hashCode();
173: int[] hashCodes = new int[this Subterms.length];
174: for (int i = 0; i < this Subterms.length; i++) {
175: hashCodes[i] = this Subterms[i].hashCode();
176: }
177: // Use the sum and the product of calculated argument hashes
178: int sum = 0;
179: int product = 1;
180: for (int i = 0; i < hashCodes.length; i++) {
181: sum += hashCodes[i];
182: product *= hashCodes[i];
183: }
184: result = 37 * result + sum;
185: result = 37 * result + product;
186: cachedCommHashCode = result;
187: }
188: return cachedCommHashCode;
189: }
190:
191: /* (non-Javadoc)
192: * @see de.uka.ilkd.key.proof.decproc.smtlib.Formula#toString()
193: */
194: public String toString() {
195: String representation = "(" + getOp();
196: Term[] this Subterms = getSubterms();
197: for (int i = 0; i < this Subterms.length; i++) {
198: representation += " " + this Subterms[i].toString();
199: }
200: representation += ")";
201: return representation;
202: }
203:
204: /* (non-Javadoc)
205: * @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)
206: */
207: public Formula replaceFormVar(FormulaVariable formVar,
208: Formula replacement) {
209: // A PredicateFormula cannot contain any FormulaVariable, but the contained terms
210: // could be IteTerms containing a Formula
211: if (!containsFormula(formVar))
212: return this ;
213: Term[] newSubterms = getSubterms();
214: for (int i = 0; i < newSubterms.length; i++) {
215: newSubterms[i] = newSubterms[i].replaceFormVarIteTerm(
216: formVar, replacement);
217: }
218: return new PredicateFormula(getOp(), newSubterms);
219: }
220:
221: /* (non-Javadoc)
222: * @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)
223: */
224: public Formula replaceTermVar(TermVariable termVar, Term replacement) {
225: if (!containsTerm(termVar))
226: return this ;
227: Term[] newSubterms = getSubterms();
228: for (int i = 0; i < newSubterms.length; i++) {
229: newSubterms[i] = newSubterms[i].replaceTermVar(termVar,
230: replacement);
231: }
232: return new PredicateFormula(getOp(), newSubterms);
233: }
234: }
|