| de.uka.ilkd.key.proof.decproc.smtlib |
|
| Java Source File Name | Type | Comment |
| Benchmark.java | Class | Represents a benchmark as defined in the SMT-Lib specification. |
| ConnectiveFormula.java | Class | 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. |
| FletFormula.java | Class | Represents a 'flet'-construct formula as defined in the SMT-Lib specification,
and specialized in the (QF_)AUFLIA sublogic. |
| Formula.java | Class | Represents a formula as defined in the SMT-Lib specification, and specialized in one of the
AUFLIA sublogics. |
| FormulaVariable.java | Class | Represents a formula variable as defined in the SMT-Lib specification, and specialized
in the (QF_)AUFLIA sublogic.
Thereby a formula variable is a variable, i.e. |
| InterpretedFuncTerm.java | Class | Represents an interpreted function as defined in the SMT-Lib specification,
and specialized in the (QF_)AUFLIA sublogic. |
| IteTerm.java | Class | Represents an if-then-else (ite) construct for terms as defined in the SMT-Lib
specification, and specialized in the (QF_)AUFLIA sublogic. |
| LetFormula.java | Class | Represents a 'let'-construct formula as defined in the SMT-Lib specification,
and specialized in the (QF_)AUFLIA sublogic.
Thereby a 'let'-construct consists of a formula f, a term variable termVar contained in f,
and a term t. |
| NumberConstantTerm.java | Class | Represents a non negative integer number constant as defined in the SMT-Lib specification
and specialized in the (QF_)AUFLIA sublogic. |
| PredicateFormula.java | Class | Represents a predicate formula as defined in the SMT-Lib specification, and specialized
in the (QF_)AUFLIA sublogic. |
| QuantifierFormula.java | Class | Represents a quantified formula as defined in the SMT-Lib specification, and specialized in
the (QF_)AUFLIA sublogic.
Thereby the usual quantifiers FORALL and EXISTS are allowed operators. |
| Signature.java | Class | Represents a signature for the uninterpreted terms and formulae of the SMT-Lib specification
and the QF_AUFLIA sublogic.
A signature thereby is a String array, with each String representing the
required sort for the corresponding argument and the result sort of an uninterpreted
function respectively.
A Signature is immutable, i.e. |
| Term.java | Class | Represents a term as defined in the SMT-Lib specification, and specialized in the
QF_AUFLIA sublogic. |
| TermVariable.java | Class | Represents a term variable as defined in the SMT-Lib specification, and specialized
in the (QF_)AUFLIA sublogic. |
| TruthValueFormula.java | Class | 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. |
| UninterpretedFuncTerm.java | Class | Represents an uninterpreted function term as defined in the SMT-Lib specification,
and specialized in the (QF_)AUFLIA sublogic.
Each uninterpreted function is identified by its function name, which is an arbitrary legal
identifier String. |
| UninterpretedPredFormula.java | Class | 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. |