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 a formula variable as defined in the SMT-Lib specification, and specialized
023: * in the (QF_)AUFLIA sublogic.
024: * <p>
025: * Thereby a formula variable is a variable, i.e. an identifier able to respresent an arbitrary
026: * formula. An identifier is considered (syntactically) legal in (QF_)AUFLIA if it begins with a
027: * letter and consists only of letters, digits and the characters '.' , '_' and '''
028: * (single quotation mark).
029: * <p>
030: * FormulaVariable 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)
034: */
035:
036: public final class FormulaVariable extends Formula {
037:
038: /* Additional fields */
039:
040: /** String constant, representing the formula variable prefix in AUFLIA */
041: private static final String formVarPrefix = "$";
042:
043: /* String constants for failures during Formula creation */
044: private static final String creationFailureIdNull = "Variable name is null!";
045: private static final String creationFailureIdentIllg = "Variable name is no legal identifier!";
046: private static final String creationFailureInterpreted = "Variable name equals an interpreted operator!";
047:
048: /* Constructor */
049:
050: /** Creates a <tt>FormulaVariable</tt>
051: *
052: * @param formVar the identifier of the <tt>FormulaVariable</tt> to be represented
053: * @throws NullPointerException if <tt>formVar</tt> is <tt>null</tt>
054: * @throws IllegalArgumentException if <tt>formVar</tt> is no legal identifier or equals
055: * an interpreted symbol in (QF_)AUFLIA
056: */
057: public FormulaVariable(String formVar) {
058: super (formVar, null, null);
059:
060: // Check if variable name formVar is syntactically correct
061: if (formVar == null)
062: throw new NullPointerException(creationFailureIdNull);
063: if (!isLegalIdentifier(formVar))
064: throw new IllegalArgumentException(creationFailureIdentIllg);
065:
066: // Check if formVar equals an interpreted operator in AUFLIA
067: String[] interpretedOps = DecisionProcedureSmtAufliaOp
068: .getAllSmtOperators();
069: for (int i = 0; i < interpretedOps.length; i++) {
070: if (formVar.equals(interpretedOps[i]))
071: throw new IllegalArgumentException(
072: creationFailureInterpreted);
073: }
074: }
075:
076: // Public method implementation
077:
078: /* (non-Javadoc)
079: * @see de.uka.ilkd.key.proof.decproc.smtlib.Formula#equals(java.lang.Object)
080: */
081: public boolean equals(Object o) {
082: if (o == this )
083: return true;
084: if (super .equals(o)) {
085: return (o instanceof TruthValueFormula);
086: }
087: return false;
088: }
089:
090: /* (non-Javadoc)
091: * @see de.uka.ilkd.key.proof.decproc.smtlib.Formula#hashCode()
092: */
093: public int hashCode() {
094: return super .hashCode();
095: }
096:
097: /* (non-Javadoc)
098: * @see de.uka.ilkd.key.proof.decproc.smtlib.Formula#toString()
099: */
100: public String toString() {
101: return formVarPrefix + getOp();
102: }
103:
104: /* (non-Javadoc)
105: * @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)
106: */
107: public Formula replaceFormVar(FormulaVariable formVar,
108: Formula replacement) {
109: return equals(formVar) ? replacement : this ;
110: }
111:
112: /* (non-Javadoc)
113: * @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)
114: */
115: public Formula replaceTermVar(TermVariable termVar, Term replacement) {
116: // A FormulaVariable cannot contain any TermVariable
117: return this;
118: }
119: }
|