| java.lang.Object
 de.uka.ilkd.key.proof.decproc.smtlib.Formula
All known Subclasses: de.uka.ilkd.key.proof.decproc.smtlib.UninterpretedPredFormula, de.uka.ilkd.key.proof.decproc.smtlib.FormulaVariable, de.uka.ilkd.key.proof.decproc.smtlib.LetFormula, de.uka.ilkd.key.proof.decproc.smtlib.FletFormula, de.uka.ilkd.key.proof.decproc.smtlib.PredicateFormula, de.uka.ilkd.key.proof.decproc.smtlib.QuantifierFormula, de.uka.ilkd.key.proof.decproc.smtlib.ConnectiveFormula, de.uka.ilkd.key.proof.decproc.smtlib.TruthValueFormula,
| Formula | | abstract public class Formula (Code) | | Represents a formula as defined in the SMT-Lib specification, and specialized in one of the
AUFLIA sublogics. These are QF_AUFLIA and AUFLIA, whereas QF_AUFLIA is the quantifier free
version of AUFLIA. Thereby a formula represents an object which can be assigned a truth
value, i.e. one predicate or many logical connected predicates.
This class is abstract because it is intended as a frame for realizing subclasses which
specialize in representing one class of predicates in (QF_)-AUFLIA (e.g. uninterpreted predicates).
Formulae are immutable; their attribute values cannot be changed after they are created.
This class also contains methods with protected access intended to be used by realizing
subclasses for convenience, as well as methods to access the lists of all uninterpreted functions
and predicates contained in this formula, which are provided for the simple integration of terms
and formulae and into benchmarks.
author:
akuwertz
version:
1.5, 12/06/2005 (Restructuring and further commenting)
See Also: QF_AUFLIA
See Also: AUFLIA
See Also: SMT-LIB |
| Method Summary | |
| public boolean | containsFormula(Formula f)
Returns true if this Formula contains f as a subformula.
This implementation tries to determine containment by first checking if f
equals this Formula. | | public boolean | containsTerm(Term t)
Returns true if this Formula contains the Term t.
This implementation tries to determine containment recursively by calling
containsTerm first on the subformulae of this Formula, then on its
subterms, returning true if one of these subelements contains t.
If t is a TermVariable, this method will only check for free
term variables, i.e. | | public boolean | equals(Object o)
Compares this Formula to the specified Object o.
This implementation tries to determine equality by first checking if o is an instance
of Formula. | | final public String | getOp()
| | final public Formula[] | getSubformulae()
| | final public Term[] | getSubterms()
| | final public Vector | getUIF()
| | final public Vector | getUIPredicates()
| | public int | hashCode()
Returns an int value representing the hash code of this Formula. | | final protected static boolean | isLegalIdentifier(String identifier)
Determines if a given identifier represents a legal identifier symbol in (QF_)AUFLIA. | | abstract public Formula | replaceFormVar(FormulaVariable formVar, Formula replacement)
Replaces all occurrences of a specified FormulaVariable by a specified
Formula in a this Formula. | | abstract public Formula | replaceTermVar(TermVariable termVar, Term replacement)
Replaces all occurrences of a specified TermVariable by a specified Term
in a this Formula. | | abstract public String | toString()
Returns a String representation of this Formula, containing the String
representation of each of its subformulae and/or subterms. | | final protected static Vector | toVector(Object[] objects)
|
| Formula | | protected Formula(String operator, Formula[] forms, Term[] terms, boolean addThisUip)(Code) | | Sole constructor. For invocation by constructors of realizing subclasses.
This explicit constructor sets the internal fields to the specified values or rather to
values computed out of the given ones. Thereby the top-level operator and the subformulae
and subterms are set directly, whereby the Vector of uninterpreted predicates and
functions respectively are computed out of the uninterpreted predicates and functions
contained in the subformulae and subterms.
Therefor all Formulae and Terms contained as subelements are searched for
uninterpreted predicates (and functions respectively) and the results are merged into a
Vector, eleminating duplicate entries.
The boolean addThisUip is a flag serving as indicator to the constructor
that the calling subclass instance also wishes to be added to the Vector of
uninterpreted predicates. If it is set to true, the calling instance will be
added to the Vector of uninterpreted predicates as its first element.
This implementation checks for null pointers in the specified arguments. If a null pointer
is found in the top-level operator op, all fields will be set to null
without throwing any exceptions. This is done to enable realizing subclasses to throw
specific exceptions on their part. It implicates that every subclass realizing this class
must check op for being a null pointer, and, if so, throw an exception. Otherwise
the methods defined in this class could fail with a NullPointerException, if called
on the created subclass instance.
The same holds for the Formulae and Terms contained in the subformulae and
subterms arrays. If one of the specified arrays contains any null pointers, all fields of
this Formula instance will become undefined, without throwing an exception.
Realizing subclasses therefore have to check or ensure that forms and
terms contain no null pointers; otherwise the methods defined in this class could
fail with a NullPointerException.
In contrary to this, null pointers are allowed for the array objects theirselves. This is done for
convenience and has to same effects as empty arrays would have.
Parameters:
operator - the top-level operator of this Formula
Parameters:
forms - the array of subformulae for this Formula
Parameters:
terms - the array of subterms for this Formula
Parameters:
addThisUip - a flag; if set to true, the calling subclass instance will beadded the to uninterpreted predicate Vector of this Formula |
| containsFormula | | public boolean containsFormula(Formula f)(Code) | | Returns true if this Formula contains f as a subformula.
This implementation tries to determine containment by first checking if f
equals this Formula. If not, it calls containsFormula recursively
first on the subformulae of this Formula, then on its subterms, returning
true if one of these subelements contains f
If this method is called on an FletFormula with the FormulaVariable
which will be semantically replaced in the FletFormula as argument, it will
only check the replaced Formula for occurences of f
Parameters:
f - the Formula to be checked for containment in this Formula true if this Formula contains f
See Also: FletFormula.containsFormula(Formula) |
| containsTerm | | public boolean containsTerm(Term t)(Code) | | Returns true if this Formula contains the Term t.
This implementation tries to determine containment recursively by calling
containsTerm first on the subformulae of this Formula, then on its
subterms, returning true if one of these subelements contains t.
If t is a TermVariable, this method will only check for free
term variables, i.e. if this method is called on a QuantifierFormula or a
LetFormula with the quantified or rather bound TermVariable as argument,
it will return false
Parameters:
t - the Term to be checked for containment in this Formula true if this Formula contains t
See Also: QuantifierFormula.containsTerm(Term)
See Also: LetFormula.containsTerm(Term) |
| equals | | public boolean equals(Object o)(Code) | | Compares this Formula to the specified Object o.
This implementation tries to determine equality by first checking if o is an instance
of Formula. If so, it checks if the top-level operator of o is equal to that
of this Formula. If true, it checks if all subformulae and subterms contained in this
Formula are equal to those contained in o, and in the same order. If all these
constraints are satisfied, true is returned.
Overriding methods are recommended to check for object equality in addition; this is not done in
this implementation.
Parameters:
o - the Object to compare with true if this Formula is the same as the specified Object;otherwise false. |
| getOp | | final public String getOp()(Code) | | Returns the top-level operator of this Formula
the top-level operator of this Formula |
| getSubformulae | | final public Formula[] getSubformulae()(Code) | | Returns a shallow copy of the subformulae array of this Formula
the array of subformulae of this Formula |
| getSubterms | | final public Term[] getSubterms()(Code) | | Returns a shallow copy of the subterms array of this Formula
the array of subterms of this Formula |
| getUIF | | final public Vector getUIF()(Code) | | Returns a Vector of all uninterpreted functions contained in this Formula
as a shallow copy
a Vector of all uninterpreted functions contained in this Formula |
| getUIPredicates | | final public Vector getUIPredicates()(Code) | | Returns a Vector of all uninterpreted predicates contained in this Formula
a Vector of all uninterpreted predicates contained in this Formula |
| hashCode | | public int hashCode()(Code) | | Returns an int value representing the hash code of this Formula.
The hash code for a Formula is calculated during its creation. This is done by
combining the hash code of its operator with the hash codes of, if available, its subformulae
and its subterms to a new hash code. The order of subformulae and subterms matters for this
implementation
the hashCode of this Term |
| isLegalIdentifier | | final protected static boolean isLegalIdentifier(String identifier)(Code) | | Determines if a given identifier represents a legal identifier symbol in (QF_)AUFLIA.
An identifier is legal if it begins with a letter and consists only of letters, digits and
the characters '.' , '_' and ''' (single quotation mark)
Parameters:
identifier - the String to be checked true if the specified String represents a legal identifier symbol; otherwise false
throws:
NullPointerException - if identifier is null |
| replaceFormVar | | abstract public Formula replaceFormVar(FormulaVariable formVar, Formula replacement)(Code) | | Replaces all occurrences of a specified FormulaVariable by a specified
Formula in a this Formula.
Thereby this Formula and the returned replaced Formula share the
same objects in their fields, except for those objects which contained the
specified FormulaVariable.
This implicates that if formVar is not contained in this Formula,
this Formula is returned without changes.
Parameters:
formVar - the FormulaVariable to be replaced
Parameters:
replacement - the Formula used to replace formVar the Formula obtained by replacing every (free) occurence of formVarby replacement in this Formula |
| replaceTermVar | | abstract public Formula replaceTermVar(TermVariable termVar, Term replacement)(Code) | | Replaces all occurrences of a specified TermVariable by a specified Term
in a this Formula.
Thereby this Formula and the returned replaced Formula share the
same objects in their fields, except for those objects which contained the
specified TermVariable.
This implicates that if termVar is not contained in this Formula,
this Formula is returned without changes.
Parameters:
termVar - the TermVariable to be replaced
Parameters:
replacement - the Term used to replace termVar the Formula obtained by replacing every (free) occurence of termVarby replacement in this Formula |
| toString | | abstract public String toString()(Code) | | Returns a String representation of this Formula, containing the String
representation of each of its subformulae and/or subterms. The returned String
is formatted and can be parsed according to the SMT-Lib grammar specification (chapter seven,
"Concrete Syntax").
See Also:
* The SMT-LIB Standard: Version 1.1 a String representation of this Formula |
| toVector | | final protected static Vector toVector(Object[] objects)(Code) | | Converts an array into a Vector, preserving element order
Parameters:
objects - The array which should be converted into a Vector a Vector containing all the Objects in the specified array,in the same order |
|
|