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