| java.lang.Object de.uka.ilkd.key.proof.decproc.smtlib.Formula de.uka.ilkd.key.proof.decproc.smtlib.TruthValueFormula
TruthValueFormula | final public class TruthValueFormula extends Formula (Code) | | Represents a truth value as defined in the SMT-Lib specification, and specialized in the
(QF_)AUFLIA sublogic.
Thereby 'true' and 'false' are the only truth value constants allowed in (QF_)AUFLIA.
TruthValueFormula are immutable; their attribute values cannot be changed after they are
created. Due to their immutability, TruthValueFormula instances can be cached
author: akuwertz version: 1.3, 12/09/2005 (Adjustments to superclass V1.5) |
TruthValueFormula | public TruthValueFormula(boolean value)(Code) | | Creates a TruthValueFormula, representing the given truth value
Parameters: value - the truth value to be represented |
getInstance | public static TruthValueFormula getInstance(boolean value)(Code) | | A factory method returning for instances of TruthValueFormula.
The instances returned by this method are cached to reduce memory footprint. Therefore
successive calls with the same truth value result in the same object being returned.
Parameters: value - the truth value to be represented a TruthValueFormula instance representing value |
hashCode | public int hashCode()(Code) | | |
|
|