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.HashSet;
021: import java.util.Set;
022:
023: import de.uka.ilkd.key.proof.decproc.DecisionProcedureSmtAufliaOp;
024:
025: /** Represents a quantified formula as defined in the SMT-Lib specification, and specialized in
026: * the (QF_)AUFLIA sublogic.<br>
027: * Thereby the usual quantifiers FORALL and EXISTS are allowed operators. A
028: * <tt>QuantifierFormula</tt> takes one or more <tt>TermVariable</tt>s and an arbitrary
029: * <tt>Formula</tt> and quantifies the given <tt>TermVariable</tt>s in the given <tt>Formula</tt>
030: * <p>
031: * QuantifierFormula are immutable; their attribute values cannot be changed after they are
032: * created.
033: *
034: * @author akuwertz
035: * @version 1.1, 10/06/2006 (Added support for many quantified variables)
036: */
037:
038: public class QuantifierFormula extends Formula {
039:
040: /* Additional fields */
041:
042: /* String constants for failures during Formula creation */
043: private static final String creationFailureOpNull = "Operator is null!";
044: private static final String creationFailureVarNull = "The array of term variables is null!";
045: private static final String creationFailureNoQuantVars = "The array of term variables is empty!";
046: private static final String creationFailureVarContainsNull = "The array of termvariables contains a null pointer!";
047: private static final String creationFailureFormulaNull = "The formula is null!";
048: private static final String creationFailureNoQuantifier = "The given operator represents no quantifier!";
049: private static final String creationFailureVarNotContained = "The variables to quantify must be contained in the specified formula!";
050: private static final String creationFailureDuplicateVar = "Duplicate term variable contained array quantVars!";
051:
052: /* Constructor */
053:
054: /** Creates a new <tt>QuantifierFormula</tt> out of a given array of <tt>TermVariable</tt>s
055: * and a given <tt>Formula</tt>.
056: * <p>
057: * The operator <tt>op</tt> must be one of the static quantifier operator <tt>String</tt>s
058: * defined in <tt>DecisionProcedureSmtAufliaOp</tt>.
059: *
060: * @param op the quantifier used to quantify the variables in <tt>quantVars</tt>
061: * @param quantVars the array of <tt>TermVariable</tt>s being quantified by <tt>op</tt>
062: * @param formula the <tt>Formula</tt> in which the variables in <tt>quantVars</tt> should
063: * be quantified
064: *
065: * @throws NullPointerException if <tt>op</tt>, <tt>quantVars</tt> or one of the contained
066: * <tt>TermVariables</tt>s, or <tt>formula</tt> is <tt>null</tt>
067: * @throws IllegalArgumentException if <tt>op</tt> represents no quantifier in (QF_)AUFLIA
068: * or if <tt>quantVars</tt> is empty or if at least one of
069: * the specified <tt>TermVariables</tt>s is not contained in
070: * <tt>formula</tt> or if duplicate <tt>TermVariable</tt>s
071: * are contained in <tt>quantVars</tt>
072: *
073: * @see de.uka.ilkd.key.logic.op.DecisionProcedureSmtAufliaOp
074: */
075: public QuantifierFormula(String op, TermVariable[] quantVars,
076: Formula formula) {
077: super (op, new Formula[] { formula }, quantVars);
078:
079: if (op == null)
080: throw new NullPointerException(creationFailureOpNull);
081: if (quantVars == null)
082: throw new NullPointerException(creationFailureVarNull);
083: if (formula == null)
084: throw new NullPointerException(creationFailureFormulaNull);
085:
086: if (op != DecisionProcedureSmtAufliaOp.FORALL
087: && op != DecisionProcedureSmtAufliaOp.EXISTS)
088: throw new IllegalArgumentException(
089: creationFailureNoQuantifier);
090:
091: if (quantVars.length == 0)
092: throw new IllegalArgumentException(
093: creationFailureNoQuantVars);
094: Set containedVars = new HashSet();
095: for (int i = 0; i < quantVars.length; i++) {
096: if (quantVars[i] == null)
097: throw new NullPointerException(
098: creationFailureVarContainsNull);
099: if (!formula.containsTerm(quantVars[i]))
100: throw new IllegalArgumentException(
101: creationFailureVarNotContained);
102: if (!containedVars.add(quantVars[i]))
103: throw new IllegalArgumentException(
104: creationFailureDuplicateVar);
105: }
106: }
107:
108: // Public method implementation
109:
110: /** Returns true if this <tt>QuantifierFormula</tt> contains the <tt>Term</tt> <tt>term</tt>.
111: * <p>
112: * In a <tt>QuantifierFormula</tt> the quantified <tt>Term</tt> variables are not contained,
113: * i.e. if this method is called with a quantified <tt>TermVariable</tt> as argument, it
114: * will return <tt>false</tt>
115: *
116: * @param term the <tt>Term</tt> be checked for containment in this <tt>QuantifierFormula</tt>
117: * @return true if this <tt>QuantifierFormula</tt> contains <tt>term</tt> and if <tt>term</tt>
118: * is unequal to its quantified variables
119: */
120: public boolean containsTerm(Term term) {
121: TermVariable[] quantVars = (TermVariable[]) getSubterms();
122: for (int i = 0; i < quantVars.length; i++) {
123: if (term.equals(quantVars[i]))
124: return false;
125: }
126: return getSubformulae()[0].containsTerm(term);
127: }
128:
129: /* (non-Javadoc)
130: * @see de.uka.ilkd.key.proof.decproc.smtlib.Formula#equals(java.lang.Object)
131: */
132: public boolean equals(Object o) {
133: if (o == this )
134: return true;
135: if (super .equals(o)) {
136: return (o instanceof QuantifierFormula);
137: }
138: return false;
139: }
140:
141: /* (non-Javadoc)
142: * @see de.uka.ilkd.key.proof.decproc.smtlib.Formula#hashCode()
143: */
144: public int hashCode() {
145: return super .hashCode();
146: }
147:
148: /* (non-Javadoc)
149: * @see de.uka.ilkd.key.proof.decproc.smtlib.Formula#toString()
150: */
151: public String toString() {
152: TermVariable[] quantVars = (TermVariable[]) getSubterms();
153: String representation = "(" + getOp() + " ";
154: for (int i = 0; i < quantVars.length; i++) {
155: representation += "(" + quantVars[i] + " "
156: + quantVars[i].getSignature() + ") ";
157: }
158: representation += getSubformulae()[0] + ")";
159: return representation;
160: }
161:
162: /* (non-Javadoc)
163: * @see Formula#replaceFormVar(FormulaVariable, Formula)
164: */
165: public Formula replaceFormVar(FormulaVariable formVar,
166: Formula replacement) {
167: if (!containsFormula(formVar))
168: return this ;
169: Formula replacedFormula = getSubformulae()[0].replaceFormVar(
170: formVar, replacement);
171: return new QuantifierFormula(getOp(),
172: (TermVariable[]) getSubterms(), replacedFormula);
173: }
174:
175: /* (non-Javadoc)
176: * @see Formula#replaceTermVar(TermVariable, Term)
177: */
178: public Formula replaceTermVar(TermVariable termVar, Term replacement) {
179: if (!containsTerm(termVar))
180: return this ;
181: Formula replacedFormula = getSubformulae()[0].replaceTermVar(
182: termVar, replacement);
183: return new QuantifierFormula(getOp(),
184: (TermVariable[]) getSubterms(), replacedFormula);
185: }
186:
187: }
|