| java.lang.Object
 de.uka.ilkd.key.proof.decproc.smtlib.Formula
de.uka.ilkd.key.proof.decproc.smtlib.PredicateFormula
| PredicateFormula | | final public class PredicateFormula extends Formula (Code) | | Represents a predicate formula as defined in the SMT-Lib specification, and specialized
in the (QF_)AUFLIA sublogic.
Thereby only the predicates '=', '<=', '<', '>=' and '>' are supported in (QF_)AUFLIA; for
convenience there's also the 'distinct'-construct.
PredicateFormula are immutable; their attribute values cannot be changed after they are created.
author:
akuwertz
version:
1.3, 12/09/2005 (Adjustments to superclass V1.5, further comments) |
| Constructor Summary | |
| public | PredicateFormula(String op, Term[] subTerms)
Creates a new PredicateFormula representing an interpreted predicate.
The predicate symbol op must be one of the static Strings defined in
DecisionProcedureSmtAufliaOp. |
| PredicateFormula | | public PredicateFormula(String op, Term[] subTerms)(Code) | | Creates a new PredicateFormula representing an interpreted predicate.
The predicate symbol op must be one of the static Strings defined in
DecisionProcedureSmtAufliaOp. Namely, these are EQUALS, GEQ, GT, LEQ, LT and DISTINCT.
All mentioned predicates but the DISTINCT predicate are of arity two. For DISTINCT, any
integer value greater than one is allowed as number of argument Terms.
Only the DISTINCT and the EQUALS predicate are commutative
Parameters:
op - the predicate symbol to be represented
Parameters:
subTerms - the array of Term arguments of this PredicateFormula
throws:
NullPointerException - if op or one of the Terms containedin subTerms is null
throws:
IllegalArgumentException - if op represents no interpreted predicate in (QF_)AUFLIA or if the specified argument Termsdon't match the predicate arity
See Also: de.uka.ilkd.key.logic.op.DecisionProcedureSmtAufliaOp
See Also: |
| equals | | public boolean equals(Object o)(Code) | | Compares this Formula to the specified Object o.
This PredicateFormula is considered equal to o if o is an
instance of PredicateFormula and has the same subterms as this
PredicateFormula.
If the represented predicate is commutative, i.e. if this PredicateFormula
represents the EQU or DISTINCT predicate, the order of arguments does not matter for
equality. For all other interpreted predicates in (QF_)AUFLIA, the order of arguments matters
for equality.
Parameters:
o - the Object to compare with true if this PredicateFormula is the same as the specified Object;otherwise false. |
| hashCode | | public int hashCode()(Code) | | Returns an int value representing the hash code of this PredicateFormula.
The hash code for a PredicateFormula is calculated by combining the hash code of
its predicate symbol (operator) with the hash codes of its Term arguments.
If this PredicateFormula represents a commutative predicate, i.e. if it represents
the EQU or DISTINCT predicate, the order of Term arguments doesn't not matter for
the calculation, otherwise it does
the hash code of this PredicateFormula |
|
|