Uses of Class
org.smtlib.SymbolTable

Packages that use SymbolTable

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

Uses of SymbolTable in org.smtlib

Methods in org.smtlib with parameters of type SymbolTable

Modifier and Type	Method	Description
ISort	Utils.asSort(ISexpr sexpr, SymbolTable symtab)
static List<IResponse>	TypeChecker.check(SymbolTable symTable, IExpr expr)	The main entry point for type-checking an IExpr (expected to be a Bool)
static List<IResponse>	TypeChecker.checkAssertion(SymbolTable symTable, IExpr expr)	The main entry point for type-checking an assert expression (expected to be a Bool); unlike TypeChecker.check(SymbolTable,IExpr), this checks the expression within a pushed scope that is merged into the enclosing scope on success (or popped on error).
static List<IResponse>	TypeChecker.checkFcn(SymbolTable symTable, IExpr.IIdentifier id, List<IExpr.IDeclaration> params, ISort result, IExpr expr)
static List<IResponse>	TypeChecker.checkFcn(SymbolTable symTable, IExpr.IIdentifier id, List<ISort> sorts, ISort result, IPos pos)
static List<IResponse>	TypeChecker.checkFcnRec(SymbolTable symTable, boolean global, IExpr.ISymbol id, List<IExpr.IDeclaration> params, ISort result, IExpr expr)	Type-checks a define-fun-rec command: verifies the symbol is new, validates sorts, pre-adds the function to the symbol table so the body may call it recursively, then checks the body expression.
static List<IResponse>	TypeChecker.checkFcnsRec(SymbolTable symTable, boolean global, List<IExpr.IFunctionDeclaration> decls, List<IExpr> bodies)	Type-checks a define-funs-rec command: for each declaration verifies the symbol is new and sorts are valid, pre-adds all functions to the symbol table for mutual recursion, then checks each body expression.
static List<IResponse>	TypeChecker.checkSortAbbreviation(SymbolTable symTable, IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
static List<IResponse>	TypeChecker.checkTerm(SymbolTable symTable, IExpr expr)	Type-checks a term of any sort (e.g.
IResponse	Utils.loadLogic(String logicName, SymbolTable symTable, IPos pos)	Finds and loads a logic into the given symbol table
IResponse	Utils.loadLogic(ILogic logicExpr, SymbolTable symTable)
IResponse	Utils.loadTheory(String theoryName, SymbolTable symTable)	Loads a theory into the given symbol table.
IResponse	Utils.loadTheory(ITheory theory, SymbolTable symTable)
static ISort.IFcnSort	TypeChecker.resolveFcnSort(SymbolTable symTable, IExpr.IIdentifier id, List<ISort> sorts, ISort result, IPos pos, List<IResponse> errors)	Checks a function signature as checkFcn does, adding any errors to errors; returns the signature with its sorts resolved in the current scope (so a sort parameter in scope becomes its IParameter), or null if there were errors.
static List<IResponse>	TypeChecker.validateDatatypeNames(SymbolTable symTable, SMT.Configuration smtConfig, List<IExpr.ISortDeclaration> sortDecls, List<ISort.IDatatype> datatypes)	Checks that constructor and selector names introduced by a datatype group are not already defined (neither in the symbol table nor duplicated within the group).

Constructors in org.smtlib with parameters of type SymbolTable

Modifier	Constructor	Description
	Iterator(SymbolTable sym)	Constructs a new iterator, initialized at the beginning
	TypeChecker(SymbolTable symTable)	Constructs a formula typechecker from the current symbol table; sorts computed while checking are recorded directly on each IExpr node via IExpr.setSort().

Uses of SymbolTable in org.smtlib.solvers

Fields in org.smtlib.solvers declared as SymbolTable

Modifier and Type	Field	Description
SymbolTable	Solver_simplify.symTable	The symbol table used for this class's own local type-checking simulation (see the class Javadoc) -- a straight copy of Solver_test's own field of the same name and visibility (public for C_what's sake, though that extension command no longer recognizes this class as a symbol-table-bearing solver now that it isn't a Solver_test -- see this session's own restructuring notes; no test exercises "what" against Simplify).
SymbolTable	Solver_test.symTable	The symbol table used by this solver