| java.lang.Object
 de.uka.ilkd.key.proof.decproc.smtlib.Formula
de.uka.ilkd.key.proof.decproc.smtlib.ConnectiveFormula
| ConnectiveFormula | | final public class ConnectiveFormula extends Formula (Code) | | Represents a complex formula composed of other formulae and a connective operator
as defined in the SMT-Lib specification, and specialized in the (QF_)AUFLIA sublogic.
The different connective operators in QF_AULFIA are:
- the logical AND
- the logical OR
- the logical XOR,
- the logical implication IMP
- the logical equivalence EQV
- the logical NOT
- an 'if-then-else'-construct IFTHENELSE, for convenience
ConnectiveFormulae are immutable; their attribute values cannot be changed after they are created.
author:
akuwertz
version:
1.3, 12/12/2005 (Adjustments to superclass V1.5, further comments) |
| Constructor Summary | |
| public | ConnectiveFormula(String op, Formula[] subForms)
Creates a new ConnectiveFormula out of existing formulae and a connective operator.
The connective operator op must be one of the static connective operator
Strings defined in DecisionProcedureSmtAufliaOp.
Namely, these are AND, OR, XOR, EQV, IMP, NOT and IFTHENELSE.
All mentioned connectives but NOT and IFTHENELSE are of arity two. |
| ConnectiveFormula | | public ConnectiveFormula(String op, Formula[] subForms)(Code) | | Creates a new ConnectiveFormula out of existing formulae and a connective operator.
The connective operator op must be one of the static connective operator
Strings defined in DecisionProcedureSmtAufliaOp.
Namely, these are AND, OR, XOR, EQV, IMP, NOT and IFTHENELSE.
All mentioned connectives but NOT and IFTHENELSE are of arity two. NOT is of arity one and
IFTHENELSE of arity three.
The AND, OR, XOR and EQV connectives are treated as commutative operators.
Parameters:
op - the logical connective operator
Parameters:
subForms - the existing Formulae to be connected
throws:
NullPointerException - if op, subForms or one of theFormulae contained in subForms isnull
throws:
IllegalArgumentException - if op is no connective symbol or if the numberof given arguments doesn't match the expected arity
See Also: de.uka.ilkd.key.logic.op.DecisionProcedureSmtAufliaOp
See Also: |
| equals | | public boolean equals(Object o)(Code) | | Compares this ConnectiveFormula to the specified Object o.
This ConnectiveFormula is considered equal to o if o is an
instance of ConnectiveFormula and has the same subformulae as this
ConnectiveFormula.
If the represented connective symbol is commutative, i.e. if this ConnetiveFormula
represents one of the connectives AND, OR, XOR or EQV, the order of arguments does
not matter for equality. For all other connective symbols in (QF_)AUFLIA, the order of
arguments matters for equality.
Parameters:
o - the Object to compare with true if this ConnectiveFormula is the same as the specifiedObject; otherwise false. |
| hashCode | | public int hashCode()(Code) | | Returns an int value representing the hash code of this ConnectiveFormula.
The hash code for a ConnectiveFormula is calculated by combining the hash code of
its connective symbol with the hash codes of its subformulae.
If this ConnectiveFormula represents a commutative connective operator, i.e. if it
represents the AND, OR, XOR or EQV connective, the order of Formula arguments
doesn't not matter for the calculation, otherwise it does
the hash code of this PredicateFormula |
|
|