Uses of Class
org.smtlib.impl.Pos.Posable

Packages that use Pos.Posable

Package	Description
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.impl	This package is an implementation of the interfaces defined in org.smtlib.
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.

Uses of Pos.Posable in org.smtlib.command

Subclasses of Pos.Posable in org.smtlib.command

Modifier and Type	Class	Description
class	C_assert	Implements the assert command
class	C_check_sat	Implements the check-sat command
class	C_check_sat_assuming	Implements the check-sat-assuming command
class	C_comment	A synthetic pseudo-command representing a comment that appeared immediately before a real command in a script -- not part of the SMT-LIB command grammar itself, but modeled as a real, typed ICommand.Icomment (see issue #115) rather than a generic ICommand, so execution, typed-visitor traversal, and printing all dispatch to it the same way every other command does, with no reflection-based or generic-fallback special case.
class	C_declare_const	Implements the declare-const command (syntactic sugar for declare-fun with no argument sorts)
class	C_declare_datatype	Implements the declare-datatype command
class	C_declare_datatypes	Implements the declare-datatypes command
class	C_declare_fun	Implements the declare-fun command
class	C_declare_sort	Implements the declare-sort command
class	C_declare_sort_parameter	Implements the declare-sort-parameter command
class	C_define_const	Implements the define-const command: syntactic sugar for define-fun with no parameters
class	C_define_fun	Implements the define-fun command
class	C_define_fun_rec	Implements the define-fun-rec command (recursive function definition); syntactically identical to define-fun (see C_define_fun), differing only in the dispatch target -- shares that class's fields, accessors, and constructor.
class	C_define_funs_rec	Implements the define-funs-rec command
class	C_define_sort	Implements the define-sort command
class	C_echo	Implements the echo command
class	C_exit	Implements the exit command
class	C_get_assertions	Implements the get-assertions command
class	C_get_assignment	Implements the get-assignment command
class	C_get_info	Implements the get-info command.
class	C_get_model	Implements the get-model command
class	C_get_option	Implements the get-option command
class	C_get_proof	Implements the get-proof command
class	C_get_unsat_assumptions	Implements the get-unsat-assumptions command
class	C_get_unsat_core	Implements the get-unsat-core command
class	C_get_value	Implements the get-value command
class	C_pop	Implements the pop command
class	C_push	Implements the push command
class	C_reset	Implements the reset command
class	C_reset_assertions	Implements the reset-assertions command
class	C_set_info	Implements the set-info command
class	C_set_logic	Implements the set-logic command.
class	C_set_option	Implements the set-option command

Uses of Pos.Posable in org.smtlib.ext

Subclasses of Pos.Posable in org.smtlib.ext

Modifier and Type	Class	Description
class	C_exec	Implements the non-standard exec command
class	C_what	Implements the non-standard what command.

Uses of Pos.Posable in org.smtlib.impl

Subclasses of Pos.Posable in org.smtlib.impl

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

Uses of Pos.Posable in org.smtlib.logic

Subclasses of Pos.Posable in org.smtlib.logic

Modifier and Type	Class	Description
class	ALL
class	AUFLIA
class	AUFLIRA
class	AUFNIRA
class	DifferenceLogic	Common base for the difference logics QF_IDL and QF_RDL.
class	LIA
class	Logic	Common base for this package's per-logic syntactic-restriction classes (QF_IDL, LRA, QF_UF, etc).
class	LRA	This logic does not allow uninterpreted functions or nonlinear arithmetic terms
class	QF_ABV	This logic does not allow quantifiers or uninterpreted functions
class	QF_AUFBV	This logic does not allow quantifiers; all array terms have sort (Array (_ BitVec i) (_ BitVec j))
class	QF_AUFLIA
class	QF_AX
class	QF_BV
class	QF_EIA
class	QF_FP	Not an official SMT-LIB logic -- see QF_FP.smt2's own :notes: a jSMTLIB-invented convenience logic for exercising the FloatingPoint theory in this project's own test suite without needing the broad ALL logic.
class	QF_IDL	QF_IDL atoms (QF_IDL.smt2): (op x y), (op (- x y) n) and (op (- x y) (- n)), with x, y free constants of sort Int and n a numeral.
class	QF_LIA
class	QF_LRA
class	QF_NIA
class	QF_NRA
class	QF_RDL	QF_RDL atoms (QF_RDL.smt2): (op x y), (op (- x y) c), (op (- (+ x ...
class	QF_UF
class	QF_UFBV	Quantifier-free, with uninterpreted functions and sorts permitted -- identical restrictions to QF_UF, all inherited from it (the bit-vector vs.
class	QF_UFIDL
class	QF_UFLIA
class	QF_UFLRA
class	QF_UFNRA
class	UFLRA
class	UFNIA

Uses of Pos.Posable in org.smtlib.sexpr

Subclasses of Pos.Posable in org.smtlib.sexpr

Modifier and Type	Class	Description
class	Sexpr	This is the root class for S-expressions in the concrete syntax
static class	Sexpr.Seq	The class corresponding to sequences of S-expressions
static class	Sexpr.Token<T>	Represents a single S-expression token with intrinsic type T