Uses of Interface
org.smtlib.IPos

Packages that use IPos

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.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.
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 IPos in org.smtlib

Fields in org.smtlib declared as IPos

Modifier and Type	Field	Description
protected IPos	IParser.ParserException.pos	The location of the parsing problem
IPos	IVisitor.VisitorException.pos	Position information about the textual location of the error

Methods in org.smtlib that return IPos

Modifier and Type	Method	Description
IPos	ISort.IErrorDefinition.errorPos()	The source position of the error
IPos	IParser.ParserException.pos()	Returns the error position
IPos	IPos.IPosable.pos()	Textual position of this object
IPos	IResponse.IError.pos()	Returns the textual location for the response, if available and applicable, otherwise null.
IPos	IVisitor.VisitorException.pos()

Methods in org.smtlib with parameters of type IPos

Modifier and Type	Method	Description
static List<IResponse>	TypeChecker.checkFcn(SymbolTable symTable, IExpr.IIdentifier id, List<ISort> sorts, ISort result, IPos pos)
ISort.IErrorDefinition	ISort.IFactory.createErrorDefinition(IExpr.IIdentifier id, String errorMessage, IPos pos)	Creates an error-placeholder definition (suppresses cascading errors).
IResponse.IError	IResponse.IFactory.error(String msg, IPos pos)
protected void	TypeChecker.error(String msg, IPos pos)	Utility method for recording an error
ILogic	Utils.findLogic(String name, IPos pos)	Reads a logic file, parses it, validates the name, and checks the version.
IResponse	Utils.loadLogic(String logicName, SymbolTable symTable, IPos pos)	Finds and loads a logic into the given symbol table
static String	Log.locationIndication(IPos pos, String prompt, SMT.Configuration smtConfig)	Creates a two-line, compiler-style caret diagnostic pointing at the given position; the returned value does not have a final line termination.
protected boolean	TypeChecker.noVariables(List<?> list, String binder, IPos pos)	Reports a binder with no variables; returns true if the list is empty
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.
IResponse	AbstractSolver.set_logic(String logicName, IPos pos)	A set-logic the solver accepts ends sat or unsat mode; one it rejects (as SMT-LIB requires outside start mode) changes nothing.
IResponse	ISolver.set_logic(String logicName, IPos pos)	Sets the logic the solver should use.
void	IPos.IPosable.setPos(IPos pos)	Setting the textual position
void	IVisitor.VisitorException.setPos(IPos pos)

Constructors in org.smtlib with parameters of type IPos

Modifier	Constructor	Description
	ParserException(String msg, IPos pos)	Creates a parse exception from the given error message and problem location
	SyntaxException(String msg, IPos pos)	Creates an exception from the given error message and problem location
	VisitorException(String msg, IPos pos)	Constructor for an exception
	VisitorException(Throwable e, IPos pos)	Constructor taking an exception

Uses of IPos in org.smtlib.impl

Classes in org.smtlib.impl that implement IPos

Modifier and Type	Class	Description
class	Pos	Represents a range of characters in a source - used to indicate the location of errors

Fields in org.smtlib.impl declared as IPos

Modifier and Type	Field	Description
protected IPos	Pos.Posable.pos

Methods in org.smtlib.impl that return IPos

Modifier and Type	Method	Description
IPos	Sort.ErrorDefinition.errorPos()
IPos	Pos.Posable.pos()

Methods in org.smtlib.impl with parameters of type IPos

Modifier and Type	Method	Description
ISort.IErrorDefinition	Factory.createErrorDefinition(IExpr.IIdentifier id, String errorMessage, IPos pos)
static IParser.ParserException	Command.error(SMT.Configuration smt, String msg, IPos pos)	Creates a ParserException with the given message and position.
IResponse.IError	Response.Factory.error(String msg, IPos pos)
void	Pos.Posable.setPos(IPos pos)
<T extends IPos.IPosable> T	Response.Error.setPos(T t, IPos p)	Setting the textual position of the command

Constructors in org.smtlib.impl with parameters of type IPos

Modifier	Constructor	Description
	Error(String errorMsg, IPos pos)
	ErrorDefinition(IExpr.IIdentifier id, String error, IPos pos)	Creates an error placeholder for the given identifier, error message, and source position.

Uses of IPos in org.smtlib.logic

Methods in org.smtlib.logic with parameters of type IPos

Modifier and Type	Method	Description
protected void	Logic.checkArraySorts(ISort sort, IPos pos)	Checks every Array sort within sort, expanding abbreviations, against Logic.allowedArraySort(org.smtlib.ISort.IApplication).

Uses of IPos in org.smtlib.sexpr

Fields in org.smtlib.sexpr declared as IPos

Modifier and Type	Field	Description
protected IPos	Lexer.badWhitespace	The position of a vertical tab or form feed, outside a comment, in the white space before the token last scanned, or null: \p{Space} reads them as white space, which SMT-LIB's white space is not; the Parser reports them (the Lexer reports nothing itself, #148)

Methods in org.smtlib.sexpr that return IPos

Modifier and Type	Method	Description
IPos	ILexToken.pos()	The lexical position of the token
IPos	Lexer.IPLexToken.pos()
IPos	Lexer.LexToken.pos()
IPos	Lexer.pos(int start, int end)	Creates an IPos object with the given start and end and the source for this Lexer
IPos	Parser.pos(int start, int end)	Returns an IPos object for the given character start and end positions and including a reference to the parser's source object.
IPos	Parser.pos(IPos start, IPos end)	Returns an IPos object for the given character start and end positions and including a reference to the parser's source object.
IPos	Lexer.skipThruRP()	Reads and discards tokens until an unmatched right parenthesis or end-of-data is read

Methods in org.smtlib.sexpr with parameters of type IPos

Modifier and Type	Method	Description
IParser.ParserException	Parser.error(String msg, IPos pos)	Creates a ParserException with the given message and position; callers should throw the result.
IPos	Parser.pos(IPos start, IPos end)	Returns an IPos object for the given character start and end positions and including a reference to the parser's source object.
protected static <T extends IPos.IPosable> T	Lexer.setPos(T t, IPos pos)	A static helper method that sets the position of an AST node, but returns the same type

Uses of IPos in org.smtlib.solvers

Methods in org.smtlib.solvers with parameters of type IPos

Modifier and Type	Method	Description
IResponse	Solver_bitwuzla.set_logic(String logicName, IPos pos)	Bitwuzla (0.9.1) accepts a second set-logic, which SMT-LIB forbids outside start mode, so that is reported here (--relax allows it).
IResponse	Solver_simplify.set_logic(String logicName, IPos pos)
IResponse	Solver_test.set_logic(String logicName, IPos pos)
IResponse	Solver_z3_4_3.set_logic(String logicName, IPos pos)