| java.lang.Object
 de.uka.ilkd.key.proof.decproc.smtlib.Formula
de.uka.ilkd.key.proof.decproc.smtlib.UninterpretedPredFormula
| UninterpretedPredFormula | | final public class UninterpretedPredFormula extends Formula (Code) | | Represents an uninterpreted predicate formula as defined in the SMT-Lib specification, and
specialized in the (QF_)AUFLIA sublogic.
Uninterpreted predicates are identified by their top-level operator, i.e. their name. This name
therefore has to be a legal identifier in (QF_)AUFLIA, i.e. it must begin with a letter and may
consist only of letters, digits and the characters '.' , '_' and ''' (single quotation mark).
Uninterpreted predicates are treated as non commutative predicates.
UninterpretedPredFormula are immutable; their attribute values cannot be changed after they
are created.
author:
akuwertz
version:
1.5, 12/11/2005 (Adjustments to superclass V1.5; further comments) |
| UninterpretedPredFormula | | public UninterpretedPredFormula(String op, Term[] subTerms, Signature sig)(Code) | | Creates a new UninterpretedPredFormula representing an uninterpreted predicate.
Every uninterpreted predicate is associated with a signature, which describes the number
and sorts of Term arguments of this UninterpretedPredFormula
To create an uninterpreted constant, subTerms can be either null or an
empty array; choosing null reduces the memory footprint through shared objects
Parameters:
op - the name assigned to the uninterpreted predicate to be represented
Parameters:
subTerms - the array of argument Terms of this UninterpretedPredFormula
Parameters:
sig - the signature of this UninterpretedPredFormula
throws:
NullPointerException - if op or sig or one of the Termscontained in subTerms is null
throws:
IllegalArgumentException - |
| getSignature | | public Signature getSignature()(Code) | | Returns the signature of this UninterpretedPredFormula
the signature of this UninterpretedPredFormula |
| hashCode | | public int hashCode()(Code) | | Returns an int value representing the hash code of this UninterpretedPredFormula.
This hash code is calculated by combining the Formula hash code of this
UninterpretedPredFormula with the hash code of its Signature
the hash code of this UninterpretedPredFormula |
|
|