| Interface | Description |
|---|---|
| FormulaLet.LetFilter | |
| Model |
A minimal interface for model queries.
|
| NonRecursive.Walker |
Walker that does some piece of work.
|
| Script |
Basic interface for the interaction with an SMTLIB version 2 compliant
solver.
|
| Class | Description |
|---|---|
| AnnotatedTerm |
Representation of annotated terms in SMTLIB 2.
|
| Annotation |
Representation of an annotation in a formula.
|
| ApplicationTerm |
Represents a function application term.
|
| Assignments |
Class used as a response to get-assignments.
|
| CheckClosedTerm |
Class to check if a term is closed.
|
| ComputeFreeVariables |
Helper to compute the free variables contained in a term.
|
| ConstantTerm |
A term representing constants.
|
| FormulaLet |
Compute the common-subexpression-elimination (cse) form of a term.
|
| FormulaUnLet |
This class removes all let terms from the formula.
|
| FunctionSymbol |
Represents a function symbol.
|
| IRAConstantFormatter | |
| LetTerm |
Representation of a let term.
|
| LoggingScript |
A logging script variant.
|
| MutableRational |
Mutable version of the
Rational class. |
| NonRecursive |
This class does a recursive algorithm by using an explicit stack on
the heap.
|
| NonRecursive.TermWalker |
Walker that walks non-recursively over terms.
|
| NoopScript |
Simple implementation of a script, that supports building terms and sorts,
but does not support setting and getting options, checking for satisfiabilty,
or getting any other results.
|
| PrintTerm |
This class converts a term into an Appendable (StringBuilder,
OutputStreamWriter, etc).
|
| QuantifiedFormula |
Represents a quantified formula in SMTLIB 2.
|
| QuotedObject |
A quoted object is used as value for string literals in SMTLIB 2.
|
| Rational |
Class that represents a rational number num/denom,
where num and denom are BigInteger.
|
| Sort |
Represents an SMTLIB sort.
|
| SortSymbol |
A sort symbol is the name of an SMTLIB sort.
|
| Term |
This is the base class for representing SMTLIB 2 terms.
|
| TermEquivalence |
This class checks if two terms are syntactically equivalent modulo
renaming of variables.
|
| TermTransformer |
This is the base class for transforming formulas.
|
| TermTransformer.BuildAnnotation |
Collect the sub term and annotations of an annotated formula from
the converted stack.
|
| TermTransformer.BuildApplicationTerm |
Collect the arguments of an application term from the converted stack
and finish the conversion of appTerm.
|
| TermTransformer.BuildLetTerm |
Collect the sub term and the values of a let term from the
converted stack and finish the conversion of let term.
|
| TermTransformer.BuildQuantifier |
Collect the sub term of a quantified formula and build the converted
formula.
|
| TermTransformer.StartLetTerm |
Walker that is called after the variable values are transformed
and before the let body starts.
|
| TermVariable | |
| Util |
This class contains some static methods to help creating terms, checking
formulas, etc.
|
| Enum | Description |
|---|---|
| FormulaUnLet.UnletType | |
| Logics |
All logics configured in SMTLIB and some extensions supported by SMTInterpol.
|
| ReasonUnknown |
The reason why we returned unknown.
|
| Script.LBool |
A lifted three valued Boolean datatype.
|
| Exception | Description |
|---|---|
| SMTLIBException |
This is the exception thrown by the script interface when an error occurs.
|