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.math.BigInteger;
021: import java.util.HashMap;
022:
023: /** Represents a non negative integer number constant as defined in the SMT-Lib specification
024: * and specialized in the (QF_)AUFLIA sublogic. Thereby number constants are terms.
025: * <p>
026: * NumberConstantTerms are immutable; their attribute values cannot be changed after they are
027: * created. Due to this immutability, created instances of this class can be cached internally
028: *
029: * @author akuwertz
030: * @version 1.5, 01/31/2006 (Added support for BigIntegers)
031: */
032:
033: public final class NumberConstantTerm extends Term {
034:
035: /* Additional fields */
036: private static final String creationFailure = "Number constant must be non negative!";
037:
038: /** A cache for created <tt>NumberConstantTerm</tt> objects, provided to reduce memory
039: * footprint */
040: private static final HashMap objectCache = new HashMap();
041:
042: /* Constructor */
043:
044: /** Creates a new <tt>NumberConstantTerm</tt>, representing an non negative integer constant
045: *
046: * @param numberConstant the integer constant to be represented
047: * @throws IllegalArgumentException if <tt>numberConstant</tt> is negative
048: */
049: public NumberConstantTerm(BigInteger numberConstant) {
050: super (numberConstant.toString(), null, null, null);
051: if (numberConstant.signum() == -1)
052: throw new IllegalArgumentException(creationFailure);
053: }
054:
055: /* Public methods implementation */
056:
057: /** A factory method that returns an instance of <tt>NumberConstantTerm</tt>, which represents
058: * the specified non negative integer constant.
059: * <p>
060: * Calling this method has mostly the same effect as using the constructor of
061: * <tt>NumberConstantTerm</tt>, with the only difference that this method caches the created
062: * objects. This means that every object returned by this method is cached internally; successive
063: * calls of this method with same integer arguments result in same <tt>NumberConstantTerm</tt>
064: * objects.
065: * <p>
066: * This cache is provided to reduce memory footprint. It can be cleared using the
067: * <tt>clearNumConstCache()</tt> method
068: *
069: * @param numberConstant the <tt>BigInteger</tt> number constant to be represented
070: * @return a <tt>NumberConstantTerm</tt> representing the specified number constant
071: * @throws IllegalArgumentException if <tt>numberConstant</tt> is negative
072: *
073: * @see #clearNumConstCache()
074: */
075: public static NumberConstantTerm getInstance(
076: BigInteger numberConstant) {
077: if (numberConstant.signum() == -1)
078: throw new IllegalArgumentException(creationFailure);
079: if (objectCache.containsKey(numberConstant)) {
080: return (NumberConstantTerm) objectCache.get(numberConstant);
081: }
082: NumberConstantTerm newNumConstTerm = new NumberConstantTerm(
083: numberConstant);
084: objectCache.put(numberConstant, newNumConstTerm);
085: return newNumConstTerm;
086: }
087:
088: /** Clear the internal cache for <tt>NumberConstantTerm</tt> objects created with the
089: * <tt>NumberConstantTermInstance</tt> method
090: *
091: *@see #getInstance( BigInteger )
092: */
093: public static void clearNumConstCache() {
094: objectCache.clear();
095: }
096:
097: /* (non-Javadoc)
098: * @see de.uka.ilkd.key.proof.decproc.smtlib.Term#equals(de.uka.ilkd.key.proof.decproc.smtlib.Term)
099: */
100: public boolean equals(Object o) {
101: if (o == this )
102: return true;
103: if (super .equals(o)) {
104: return o instanceof NumberConstantTerm;
105: }
106: return false;
107: }
108:
109: /* (non-Javadoc)
110: * @see de.uka.ilkd.key.proof.decproc.smtlib.Term#hashCode()
111: */
112: public int hashCode() {
113: return super .hashCode();
114: }
115:
116: /* (non-Javadoc)
117: * @see de.uka.ilkd.key.proof.decproc.smtlib.Term#toString()
118: */
119: public String toString() {
120: return getFunction();
121: }
122:
123: /* (non-Javadoc)
124: * @see de.uka.ilkd.key.proof.decproc.smtlib.Term#replaceTermVar(de.uka.ilkd.key.proof.decproc.smtlib.TermVariable, de.uka.ilkd.key.proof.decproc.smtlib.Term)
125: */
126: public Term replaceTermVar(TermVariable termVar, Term replacement) {
127: // A NumberConstant cannot contain any TermVariable
128: return this ;
129: }
130:
131: /* (non-Javadoc)
132: * @see de.uka.ilkd.key.proof.decproc.smtlib.Term#replaceFormVarIteTerm(de.uka.ilkd.key.proof.decproc.smtlib.FormulaVariable, de.uka.ilkd.key.proof.decproc.smtlib.Formula)
133: */
134: public Term replaceFormVarIteTerm(FormulaVariable formVar,
135: Formula replacement) {
136: return this;
137: }
138: }
|