Package org.smtlib.impl

package org.smtlib.impl

This package is an implementation of the interfaces defined in org.smtlib. This implementation uses the conventional concrete syntax. In particular, there are implementations of ISort, IPos (and ISource), ICommand, IResponse, IExpr and its subtypes, along with factories for all of these concrete classes.

Related Packages

Package	Description
org.smtlib	This package contains the main classes and abstract interfaces for this SMT-LIB tool; the tool provides a stand-alone SMT-LIB-compliant command-line application, an application that responds to SMT-LIB commands over a network port, and an SMT-LIB Java API.
org.smtlib.command	This package contains implementations of the SMT-LIB commands, implementing the interfaces defined in ICommand; these implementations are independent of the concrete syntax that might be used, except that each command object has methods that can parse or print representations of the command in the standard (or potentially other) concrete syntaxes.
org.smtlib.ext	This package contains commands that are extensions to SMT-LIB.
org.smtlib.logic	This package contains implementations of classes that implement the constraints of individual logics.
org.smtlib.sexpr	This package is a concrete implementation of a particular concrete syntax for the abstract SMT-LIB semantics.
org.smtlib.solvers	This package implements various instances of org.smtlib.ISolver, which are specific solvers that wrap and interact with various off-the-shelf SMT solvers currently available.

Classes

Class	Description
Command	This abstract class is the base class for all commands within this implementation.
Factory	Implements a factory for SMT-LIB expressions using the standard concrete syntax.
Pos	Represents a range of characters in a source - used to indicate the location of errors
Pos.AbstractExpr	A Printable that also implements IExpr, additionally holding the sort computed for the expression by the type checker (null if not yet, or never, computed).
Pos.Posable	An implementation of IPosable, holding an instance of Pos, that can be used as a base class if necessary
Pos.Printable	A Posable that also implements INode, with toString() delegating to Printer.
Pos.Source	An implementation of the ISource interface
Response	This class holds subclasses that are implementations of the various IResponse interfaces.
Response.AssertionsResponse	Implements the IResponse.IAssertionsResponse interface
Response.AssignmentResponse	Implements the IResponse.IAssignmentResponse interface
Response.Error	Implements the IResponse.IError interface
Response.Factory	Implements the IResponse.IFactory interface
Response.Pair<T1,T2>	Implements the IResponse.IPair interface
Response.ProofResponse	Implements the IResponse.IProofResponse interface
Response.Seq	Implementation of IAttributeList: a list of attributes returned by get-info.
Response.UnsatAssumptionsResponse	Implements the IResponse.IUnsatAssumptionsResponse interface
Response.UnsatCoreResponse	Implements the IResponse.IUnsatCoreResponse interface
Response.ValueResponse	Implements the IResponse.IValueResponse interface
Script	This class implements the IScript interface, representing SMT-LIB command scripts
SMTExpr	This class defines a number of subclasses that implement the SMT-LIB abstract AST; they are used by commands and expressions.
SMTExpr.AsIdentifier	This class represents an SMT as-identifier AST
SMTExpr.Attribute<TT extends IAttributeValue>	Represents an SMT-LIB attribute: a keyword optionally paired with a value.
SMTExpr.AttributedExpr	Represents an SMT-LIB attributed expression ((! expr attrs...)).
SMTExpr.BinaryLiteral	Represents an SMT-LIB binary literal (e.g.
SMTExpr.Binding	Represents a let-binding: a symbol bound to an expression.
SMTExpr.Constructor	Represents a constructor declaration within a datatype, consisting of a name and a list of selectors.
SMTExpr.Datatype	Represents a datatype body: a list of constructors and (for parametric forms) a list of sort parameter symbols.
SMTExpr.Decimal	This class represents an SMT Decimal literal expression or syntax token
SMTExpr.Declaration	Represents a sorted variable declaration (parameter name and its sort), used in forall/exists/define-fun.
SMTExpr.Error	Represents an expression-level error node inserted during parsing to allow error recovery.
SMTExpr.Exists	Represents an SMT-LIB existential quantifier expression.
SMTExpr.FcnExpr	Represents a function-application expression: a qualified identifier applied to a list of argument expressions.
SMTExpr.Forall	Represents an SMT-LIB universal quantifier expression.
SMTExpr.FunctionDeclaration	Represents a function declaration header (name, sorted parameters, result sort), used in define-funs-rec.
SMTExpr.HexLiteral	Represents an SMT-LIB hex literal (e.g.
SMTExpr.Keyword	This class represents an SMT Keyword syntax token
SMTExpr.Lambda	Represents an SMT-LIB lambda expression (SMT-LIB 2.7ff, HO-Core theory).
SMTExpr.Let	Represents an SMT-LIB let expression: a list of bindings and a body expression.
SMTExpr.Literal<T>	Abstract base class for all literal value AST nodes; holds the typed value and provides a shared implementation.
SMTExpr.Logic
SMTExpr.Match	Represents an SMT-LIB 2.7 match expression: an expression matched against a list of cases.
SMTExpr.MatchCase	Represents a single case in a match expression: a pattern and its result body.
SMTExpr.Numeral	This class represents an SMT Numeral expression or syntax token
SMTExpr.ParameterizedIdentifier	This class represents an SMT parameterized-identifier AST (e.g.
SMTExpr.Pattern	Represents a match pattern: a constructor name applied to zero or more variable symbols.
SMTExpr.PatternTerms	Represents the value of a :pattern attribute: a list of trigger terms.
SMTExpr.Selector	Represents a selector declaration within a datatype constructor.
SMTExpr.SortDeclaration	Represents a sort declaration (symbol and arity) used in declare-datatype and declare-datatypes.
SMTExpr.StringLiteral	This class represents an SMT String literal expression or syntax token
SMTExpr.Symbol	This class represents an SMT Symbol
SMTExpr.Theory
Sort	This class implements the abstract ISort interface
Sort.Abbreviation	Implements a Sort abbreviation (parameterized definition, possibly with no parameters)
Sort.Application	Represents a sort expression consisting of a sort symbol or sort abbreviation symbol applied to a corresponding number of sort arguments
Sort.ErrorDefinition	A placeholder sort definition used when a sort declaration is ill-formed, to suppress cascading errors.
Sort.Family	Represents a new sort symbol, with a given identifier and arity
Sort.FcnSort	Represents the class of the sort of a function symbol.
Sort.Parameter	Represents a Sort parameter, such as in either the parameter list or the expression of a Sort abbreviation