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 getassignments.

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 commonsubexpressionelimination (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 nonrecursively 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.
