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 truth value as defined in the SMT-Lib specification, and specialized in the
023: * (QF_)AUFLIA sublogic.
024: * <p>
025: * Thereby 'true' and 'false' are the only truth value constants allowed in (QF_)AUFLIA.
026: * <p>
027: * TruthValueFormula are immutable; their attribute values cannot be changed after they are
028: * created. Due to their immutability, <tt>TruthValueFormula</tt> instances can be cached
029: *
030: * @author akuwertz
031: * @version 1.3, 12/09/2005 (Adjustments to superclass V1.5)
032: */
033:
034: public final class TruthValueFormula extends Formula {
035:
036: /* Additional fields */
037:
038: /** A cache for the two unequal <tt>TruthValueFormula</tt> instances */
039: private static final TruthValueFormula[] instanceCache = new TruthValueFormula[2];
040:
041: /* Constructor */
042:
043: /** Creates a <tt>TruthValueFormula</tt>, representing the given truth value
044: *
045: * @param value the truth value to be represented
046: */
047: public TruthValueFormula(boolean value) {
048: super (value ? DecisionProcedureSmtAufliaOp.TRUE
049: : DecisionProcedureSmtAufliaOp.FALSE, null, null);
050: }
051:
052: /* Public method implementation */
053:
054: /** A factory method returning for instances of <tt>TruthValueFormula</tt>.
055: * <p>
056: * The instances returned by this method are cached to reduce memory footprint. Therefore
057: * successive calls with the same truth value result in the same object being returned.
058: *
059: * @param value the truth value to be represented
060: * @return a <tt>TruthValueFormula</tt> instance representing <tt>value</tt>
061: */
062: public static TruthValueFormula getInstance(boolean value) {
063: int index = value ? 1 : 0;
064: if (instanceCache[index] == null)
065: instanceCache[index] = new TruthValueFormula(value);
066: return instanceCache[index];
067: }
068:
069: /* (non-Javadoc)
070: * @see de.uka.ilkd.key.proof.decproc.smtlib.Formula#equals(java.lang.Object)
071: */
072: public boolean equals(Object o) {
073: if (o == this )
074: return true;
075: if (super .equals(o)) {
076: return (o instanceof TruthValueFormula);
077: }
078: return false;
079: }
080:
081: /* (non-Javadoc)
082: * @see de.uka.ilkd.key.proof.decproc.smtlib.Formula#hashCode()
083: */
084: public int hashCode() {
085: return super .hashCode();
086: }
087:
088: /* (non-Javadoc)
089: * @see de.uka.ilkd.key.proof.decproc.smtlib.Formula#toString()
090: */
091: public String toString() {
092: return getOp();
093: }
094:
095: /* (non-Javadoc)
096: * @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)
097: */
098: public Formula replaceFormVar(FormulaVariable formVar,
099: Formula replacement) {
100: // A TruthValue cannot contain any FormulaVariable
101: return this ;
102: }
103:
104: /* (non-Javadoc)
105: * @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)
106: */
107: public Formula replaceTermVar(TermVariable termVar, Term replacement) {
108: // A TruthValue cannot contain any TermVariable
109: return this;
110: }
111: }
|