Uses of Class
org.smtlib.IVisitor.VisitorException

Packages that use IVisitor.VisitorException

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

Methods in org.smtlib that throw IVisitor.VisitorException

Modifier and Type	Method	Description
<T> T	AbstractSolver.Pending.accept(IVisitor<T> v)
<T> T	INode.accept(IVisitor<T> v)	The accept method corresponding to IVisitor, to be implemented in each subclass as { return v.visit(this); }
void	ILanguage.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)	Checks whether the given function declaration is permitted in the language, throwing an exception if not
void	ILanguage.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)	Checks whether the given sort declaration is permitted in the language, throwing an exception if not
static void	TypeChecker.clearSorts(IExpr expr)	Walks the given expression subtree, nulling out the sort recorded on each node (e.g.
<T extends INode> void	IPrinter.print(T expr)	Prints the argument to the receiver
protected String	AbstractSolver.translate(INode sexpr)	Translates an in-memory node into the text sent to the solver process.
void	ILanguage.validExpression(IExpr expression)	Checks whether the given expression is permitted in the language, throwing an exception if not
T	IVisitor.TreeVisitor.visit(ICommand e)
T	IVisitor.TreeVisitor.visit(ICommand.Iassert e)
T	IVisitor.TreeVisitor.visit(ICommand.Icheck_sat e)
T	IVisitor.TreeVisitor.visit(ICommand.Icheck_sat_assuming e)
T	IVisitor.TreeVisitor.visit(ICommand.Icomment e)
T	IVisitor.TreeVisitor.visit(ICommand.Ideclare_const e)
T	IVisitor.TreeVisitor.visit(ICommand.Ideclare_datatype e)
T	IVisitor.TreeVisitor.visit(ICommand.Ideclare_datatypes e)
T	IVisitor.TreeVisitor.visit(ICommand.Ideclare_fun e)
T	IVisitor.TreeVisitor.visit(ICommand.Ideclare_sort e)
T	IVisitor.TreeVisitor.visit(ICommand.Ideclare_sort_parameter e)
T	IVisitor.TreeVisitor.visit(ICommand.Idefine_const e)
T	IVisitor.TreeVisitor.visit(ICommand.Idefine_fun e)
T	IVisitor.TreeVisitor.visit(ICommand.Idefine_fun_rec e)
T	IVisitor.TreeVisitor.visit(ICommand.Idefine_funs_rec e)
T	IVisitor.TreeVisitor.visit(ICommand.Idefine_sort e)
T	IVisitor.TreeVisitor.visit(ICommand.Iecho e)
T	IVisitor.TreeVisitor.visit(ICommand.Iexit e)
T	IVisitor.TreeVisitor.visit(ICommand.Iget_assertions e)
T	IVisitor.TreeVisitor.visit(ICommand.Iget_assignment e)
T	IVisitor.TreeVisitor.visit(ICommand.Iget_info e)
T	IVisitor.TreeVisitor.visit(ICommand.Iget_model e)
T	IVisitor.TreeVisitor.visit(ICommand.Iget_option e)
T	IVisitor.TreeVisitor.visit(ICommand.Iget_proof e)
T	IVisitor.TreeVisitor.visit(ICommand.Iget_unsat_assumptions e)
T	IVisitor.TreeVisitor.visit(ICommand.Iget_unsat_core e)
T	IVisitor.TreeVisitor.visit(ICommand.Iget_value e)
T	IVisitor.TreeVisitor.visit(ICommand.Ipop e)
T	IVisitor.TreeVisitor.visit(ICommand.Ipush e)
T	IVisitor.TreeVisitor.visit(ICommand.Ireset e)
T	IVisitor.TreeVisitor.visit(ICommand.Ireset_assertions e)
T	IVisitor.TreeVisitor.visit(ICommand.IScript e)
T	IVisitor.TreeVisitor.visit(ICommand.Iset_info e)
T	IVisitor.TreeVisitor.visit(ICommand.Iset_logic e)
T	IVisitor.TreeVisitor.visit(ICommand.Iset_option e)
T	IVisitor.TreeVisitor.visit(IExpr.IAsIdentifier e)
T	IVisitor.TreeVisitor.visit(IExpr.IAttribute<?> e)
T	IVisitor.TreeVisitor.visit(IExpr.IAttributedExpr e)
T	IVisitor.TreeVisitor.visit(IExpr.IBinaryLiteral e)
T	IVisitor.TreeVisitor.visit(IExpr.IBinding e)
T	IVisitor.TreeVisitor.visit(IExpr.IConstructor e)
T	IVisitor.TreeVisitor.visit(IExpr.IDecimal e)
T	IVisitor.TreeVisitor.visit(IExpr.IDeclaration e)
T	IVisitor.TreeVisitor.visit(IExpr.IError e)
T	IVisitor.TreeVisitor.visit(IExpr.IExists e)
T	IVisitor.TreeVisitor.visit(IExpr.IFcnExpr e)
T	IVisitor.TreeVisitor.visit(IExpr.IForall e)
T	IVisitor.TreeVisitor.visit(IExpr.IFunctionDeclaration e)
T	IVisitor.TreeVisitor.visit(IExpr.IHexLiteral e)
T	IVisitor.TreeVisitor.visit(IExpr.IKeyword e)
T	IVisitor.TreeVisitor.visit(IExpr.ILambda e)
T	IVisitor.TreeVisitor.visit(IExpr.ILet e)
T	IVisitor.TreeVisitor.visit(IExpr.IMatch e)
T	IVisitor.TreeVisitor.visit(IExpr.IMatchCase e)
T	IVisitor.TreeVisitor.visit(IExpr.INumeral e)
T	IVisitor.TreeVisitor.visit(IExpr.IParameterizedIdentifier e)
T	IVisitor.TreeVisitor.visit(IExpr.IPattern e)
T	IVisitor.TreeVisitor.visit(IExpr.IPatternTerms e)
T	IVisitor.TreeVisitor.visit(IExpr.ISelector e)
T	IVisitor.TreeVisitor.visit(IExpr.ISortDeclaration e)
T	IVisitor.TreeVisitor.visit(IExpr.IStringLiteral e)
T	IVisitor.TreeVisitor.visit(IExpr.ISymbol e)
T	IVisitor.TreeVisitor.visit(ILogic s)
T	IVisitor.TreeVisitor.visit(IResponse e)
T	IVisitor.TreeVisitor.visit(IResponse.IAssertionsResponse e)
T	IVisitor.TreeVisitor.visit(IResponse.IAssignmentResponse e)
T	IVisitor.TreeVisitor.visit(IResponse.IAttributeList e)
T	IVisitor.TreeVisitor.visit(IResponse.IError e)
T	IVisitor.TreeVisitor.visit(IResponse.IProofResponse e)
T	IVisitor.TreeVisitor.visit(IResponse.IUnsatAssumptionsResponse e)
T	IVisitor.TreeVisitor.visit(IResponse.IUnsatCoreResponse e)
T	IVisitor.TreeVisitor.visit(IResponse.IValueResponse e)
T	IVisitor.TreeVisitor.visit(ISort.IAbbreviation s)
T	IVisitor.TreeVisitor.visit(ISort.IApplication s)
T	IVisitor.TreeVisitor.visit(ISort.IDatatype e)
T	IVisitor.TreeVisitor.visit(ISort.IFamily s)
T	IVisitor.TreeVisitor.visit(ISort.IFcnSort s)
T	IVisitor.TreeVisitor.visit(ISort.IParameter s)
T	IVisitor.TreeVisitor.visit(ITheory s)
T	IVisitor.TreeVisitor.visit(ISexpr.ISeq e)	Iterative, since a list (e.g.
T	IVisitor.TreeVisitor.visit(ISexpr.IToken<?> e)
T	IVisitor.visit(ICommand e)
default T	IVisitor.visit(ICommand.Iassert e)
default T	IVisitor.visit(ICommand.Icheck_sat e)
default T	IVisitor.visit(ICommand.Icheck_sat_assuming e)
default T	IVisitor.visit(ICommand.Icomment e)
default T	IVisitor.visit(ICommand.Ideclare_const e)
default T	IVisitor.visit(ICommand.Ideclare_datatype e)
default T	IVisitor.visit(ICommand.Ideclare_datatypes e)
default T	IVisitor.visit(ICommand.Ideclare_fun e)
default T	IVisitor.visit(ICommand.Ideclare_sort e)
default T	IVisitor.visit(ICommand.Ideclare_sort_parameter e)
default T	IVisitor.visit(ICommand.Idefine_const e)
default T	IVisitor.visit(ICommand.Idefine_fun e)
default T	IVisitor.visit(ICommand.Idefine_fun_rec e)
default T	IVisitor.visit(ICommand.Idefine_funs_rec e)
default T	IVisitor.visit(ICommand.Idefine_sort e)
default T	IVisitor.visit(ICommand.Iecho e)
default T	IVisitor.visit(ICommand.Iexit e)
default T	IVisitor.visit(ICommand.Iget_assertions e)
default T	IVisitor.visit(ICommand.Iget_assignment e)
default T	IVisitor.visit(ICommand.Iget_info e)
default T	IVisitor.visit(ICommand.Iget_model e)
default T	IVisitor.visit(ICommand.Iget_option e)
default T	IVisitor.visit(ICommand.Iget_proof e)
default T	IVisitor.visit(ICommand.Iget_unsat_assumptions e)
default T	IVisitor.visit(ICommand.Iget_unsat_core e)
default T	IVisitor.visit(ICommand.Iget_value e)
default T	IVisitor.visit(ICommand.Ipop e)
default T	IVisitor.visit(ICommand.Ipush e)
default T	IVisitor.visit(ICommand.Ireset e)
default T	IVisitor.visit(ICommand.Ireset_assertions e)
T	IVisitor.visit(ICommand.IScript e)
default T	IVisitor.visit(ICommand.Iset_info e)
default T	IVisitor.visit(ICommand.Iset_logic e)
default T	IVisitor.visit(ICommand.Iset_option e)
T	IVisitor.visit(IExpr.IAsIdentifier e)
T	IVisitor.visit(IExpr.IAttribute<?> e)
T	IVisitor.visit(IExpr.IAttributedExpr e)
T	IVisitor.visit(IExpr.IBinaryLiteral e)
T	IVisitor.visit(IExpr.IBinding e)
T	IVisitor.visit(IExpr.IConstructor e)
T	IVisitor.visit(IExpr.IDecimal e)
T	IVisitor.visit(IExpr.IDeclaration e)
T	IVisitor.visit(IExpr.IError e)
T	IVisitor.visit(IExpr.IExists e)
T	IVisitor.visit(IExpr.IFcnExpr e)
T	IVisitor.visit(IExpr.IForall e)
T	IVisitor.visit(IExpr.IFunctionDeclaration e)
T	IVisitor.visit(IExpr.IHexLiteral e)
T	IVisitor.visit(IExpr.IKeyword e)
T	IVisitor.visit(IExpr.ILambda e)
T	IVisitor.visit(IExpr.ILet e)
T	IVisitor.visit(IExpr.IMatch e)
T	IVisitor.visit(IExpr.IMatchCase e)
T	IVisitor.visit(IExpr.INumeral e)
T	IVisitor.visit(IExpr.IParameterizedIdentifier e)
T	IVisitor.visit(IExpr.IPattern e)
default T	IVisitor.visit(IExpr.IPatternTerms e)	Visits the value of a programmatically built :pattern attribute; by default does nothing.
T	IVisitor.visit(IExpr.ISelector e)
T	IVisitor.visit(IExpr.ISortDeclaration e)
T	IVisitor.visit(IExpr.IStringLiteral e)
T	IVisitor.visit(IExpr.ISymbol e)
T	IVisitor.visit(ILogic s)
T	IVisitor.visit(IResponse e)
T	IVisitor.visit(IResponse.IAssertionsResponse e)
T	IVisitor.visit(IResponse.IAssignmentResponse e)
T	IVisitor.visit(IResponse.IAttributeList e)
T	IVisitor.visit(IResponse.IError e)
T	IVisitor.visit(IResponse.IProofResponse e)
T	IVisitor.visit(IResponse.IUnsatAssumptionsResponse e)
T	IVisitor.visit(IResponse.IUnsatCoreResponse e)
T	IVisitor.visit(IResponse.IValueResponse e)
T	IVisitor.visit(ISort.IAbbreviation s)
T	IVisitor.visit(ISort.IApplication s)
T	IVisitor.visit(ISort.IDatatype e)
T	IVisitor.visit(ISort.IFamily s)
T	IVisitor.visit(ISort.IFcnSort s)
T	IVisitor.visit(ISort.IParameter s)
T	IVisitor.visit(ITheory s)
T	IVisitor.visit(ISexpr.ISeq e)
T	IVisitor.visit(ISexpr.IToken<?> e)
ISort	TypeChecker.visit(ICommand e)
ISort	TypeChecker.visit(ICommand.IScript e)
ISort	TypeChecker.visit(IExpr.IAsIdentifier e)
ISort	TypeChecker.visit(IExpr.IAttribute<?> e)
ISort	TypeChecker.visit(IExpr.IAttributedExpr e)
ISort	TypeChecker.visit(IExpr.IBinaryLiteral e)
ISort	TypeChecker.visit(IExpr.IBinding e)
ISort	TypeChecker.visit(IExpr.IConstructor e)
ISort	TypeChecker.visit(IExpr.IDeclaration e)
ISort	TypeChecker.visit(IExpr.IExists e)
ISort	TypeChecker.visit(IExpr.IFcnExpr e)
ISort	TypeChecker.visit(IExpr.IForall e)
ISort	TypeChecker.visit(IExpr.IFunctionDeclaration e)
ISort	TypeChecker.visit(IExpr.IHexLiteral e)
ISort	TypeChecker.visit(IExpr.ILambda e)	Type-checks a lambda expression: (lambda (sorted_var+) term), SMT-LIB 2.7ff (the optional HO-Core theory -- see SMT/logics/HO-Core.smt2).
ISort	TypeChecker.visit(IExpr.ILet e)
ISort	TypeChecker.visit(IExpr.IMatch e)
ISort	TypeChecker.visit(IExpr.IMatchCase e)
ISort	TypeChecker.visit(IExpr.IParameterizedIdentifier e)
ISort	TypeChecker.visit(IExpr.IPattern e)
ISort	TypeChecker.visit(IExpr.ISelector e)
ISort	TypeChecker.visit(IExpr.ISortDeclaration e)
ISort	TypeChecker.visit(ILogic s)
ISort	TypeChecker.visit(IResponse e)
ISort	TypeChecker.visit(IResponse.IAssertionsResponse e)
ISort	TypeChecker.visit(IResponse.IAssignmentResponse e)
ISort	TypeChecker.visit(IResponse.IAttributeList e)
ISort	TypeChecker.visit(IResponse.IError e)
ISort	TypeChecker.visit(IResponse.IProofResponse e)
ISort	TypeChecker.visit(IResponse.IUnsatAssumptionsResponse e)
ISort	TypeChecker.visit(IResponse.IUnsatCoreResponse e)
ISort	TypeChecker.visit(IResponse.IValueResponse e)
ISort	TypeChecker.visit(ISort.IAbbreviation s)
ISort	TypeChecker.visit(ISort.IApplication s)
ISort	TypeChecker.visit(ISort.IDatatype e)
ISort	TypeChecker.visit(ISort.IFamily s)
ISort	TypeChecker.visit(ISort.IFcnSort s)
ISort	TypeChecker.visit(ISort.IParameter s)
ISort	TypeChecker.visit(ITheory s)
ISort	TypeChecker.visit(ISexpr.ISeq e)
ISort	TypeChecker.visit(ISexpr.IToken<?> e)

Uses of IVisitor.VisitorException in org.smtlib.command

Methods in org.smtlib.command that throw IVisitor.VisitorException

Modifier and Type	Method	Description
<T> T	C_assert.accept(IVisitor<T> v)
<T> T	C_check_sat_assuming.accept(IVisitor<T> v)
<T> T	C_check_sat.accept(IVisitor<T> v)
<T> T	C_comment.accept(IVisitor<T> v)
<T> T	C_declare_const.accept(IVisitor<T> v)
<T> T	C_declare_datatype.accept(IVisitor<T> v)
<T> T	C_declare_datatypes.accept(IVisitor<T> v)
<T> T	C_declare_fun.accept(IVisitor<T> v)
<T> T	C_declare_sort_parameter.accept(IVisitor<T> v)
<T> T	C_declare_sort.accept(IVisitor<T> v)
<T> T	C_define_const.accept(IVisitor<T> v)
<T> T	C_define_fun_rec.accept(IVisitor<T> v)
<T> T	C_define_fun.accept(IVisitor<T> v)
<T> T	C_define_funs_rec.accept(IVisitor<T> v)
<T> T	C_define_sort.accept(IVisitor<T> v)
<T> T	C_echo.accept(IVisitor<T> v)
<T> T	C_exit.accept(IVisitor<T> v)
<T> T	C_get_assertions.accept(IVisitor<T> v)
<T> T	C_get_assignment.accept(IVisitor<T> v)
<T> T	C_get_info.accept(IVisitor<T> v)
<T> T	C_get_model.accept(IVisitor<T> v)
<T> T	C_get_option.accept(IVisitor<T> v)
<T> T	C_get_proof.accept(IVisitor<T> v)
<T> T	C_get_unsat_assumptions.accept(IVisitor<T> v)
<T> T	C_get_unsat_core.accept(IVisitor<T> v)
<T> T	C_get_value.accept(IVisitor<T> v)
<T> T	C_pop.accept(IVisitor<T> v)
<T> T	C_push.accept(IVisitor<T> v)
<T> T	C_reset_assertions.accept(IVisitor<T> v)
<T> T	C_reset.accept(IVisitor<T> v)
<T> T	C_set_info.accept(IVisitor<T> v)
<T> T	C_set_logic.accept(IVisitor<T> v)
<T> T	C_set_option.accept(IVisitor<T> v)

Uses of IVisitor.VisitorException in org.smtlib.ext

Methods in org.smtlib.ext that throw IVisitor.VisitorException

Modifier and Type	Method	Description
<T> T	C_exec.accept(IVisitor<T> v)
<T> T	C_what.accept(IVisitor<T> v)

Uses of IVisitor.VisitorException in org.smtlib.impl

Methods in org.smtlib.impl that throw IVisitor.VisitorException

Modifier and Type	Method	Description
<T> T	Response.AssertionsResponse.accept(IVisitor<T> v)
<T> T	Response.AssignmentResponse.accept(IVisitor<T> v)
<T> T	Response.Error.accept(IVisitor<T> v)
<T> T	Response.ProofResponse.accept(IVisitor<T> v)
<T> T	Response.Seq.accept(IVisitor<T> v)
<T> T	Response.UnsatAssumptionsResponse.accept(IVisitor<T> v)
<T> T	Response.UnsatCoreResponse.accept(IVisitor<T> v)
<T> T	Response.ValueResponse.accept(IVisitor<T> v)
<T> T	Script.accept(IVisitor<T> v)	The accept method for visitor classes; the type parameter is the return type of the accept and visit methods
<T> T	SMTExpr.AsIdentifier.accept(IVisitor<T> v)
<T> T	SMTExpr.Attribute.accept(IVisitor<T> v)
<T> T	SMTExpr.AttributedExpr.accept(IVisitor<T> v)
<T> T	SMTExpr.BinaryLiteral.accept(IVisitor<T> v)
<T> T	SMTExpr.Binding.accept(IVisitor<T> v)
<T> T	SMTExpr.Constructor.accept(IVisitor<T> v)
<T> T	SMTExpr.Datatype.accept(IVisitor<T> v)
<T> T	SMTExpr.Decimal.accept(IVisitor<T> v)
<T> T	SMTExpr.Declaration.accept(IVisitor<T> v)
<T> T	SMTExpr.Error.accept(IVisitor<T> v)
<T> T	SMTExpr.Exists.accept(IVisitor<T> v)
<T> T	SMTExpr.FcnExpr.accept(IVisitor<T> v)
<T> T	SMTExpr.Forall.accept(IVisitor<T> v)
<T> T	SMTExpr.FunctionDeclaration.accept(IVisitor<T> v)
<T> T	SMTExpr.HexLiteral.accept(IVisitor<T> v)
<T> T	SMTExpr.Keyword.accept(IVisitor<T> v)
<T> T	SMTExpr.Lambda.accept(IVisitor<T> v)
<T> T	SMTExpr.Let.accept(IVisitor<T> v)
<T> T	SMTExpr.Logic.accept(IVisitor<T> v)
<T> T	SMTExpr.Match.accept(IVisitor<T> v)
<T> T	SMTExpr.MatchCase.accept(IVisitor<T> v)
<T> T	SMTExpr.Numeral.accept(IVisitor<T> v)
<T> T	SMTExpr.ParameterizedIdentifier.accept(IVisitor<T> v)
<T> T	SMTExpr.Pattern.accept(IVisitor<T> v)
<T> T	SMTExpr.PatternTerms.accept(IVisitor<T> v)
<T> T	SMTExpr.Selector.accept(IVisitor<T> v)
<T> T	SMTExpr.SortDeclaration.accept(IVisitor<T> v)
<T> T	SMTExpr.StringLiteral.accept(IVisitor<T> v)
<T> T	SMTExpr.Symbol.accept(IVisitor<T> v)
<T> T	SMTExpr.Theory.accept(IVisitor<T> v)
<T> T	Sort.Abbreviation.accept(IVisitor<T> v)
<T> T	Sort.Application.accept(IVisitor<T> v)
<T> T	Sort.ErrorDefinition.accept(IVisitor<T> v)
<T> T	Sort.Family.accept(IVisitor<T> v)
<T> T	Sort.FcnSort.accept(IVisitor<T> v)
<T> T	Sort.Parameter.accept(IVisitor<T> v)
void	SMTExpr.Logic.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	SMTExpr.Logic.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	SMTExpr.Logic.validExpression(IExpr expr)
void	Command.write(Printer p)	Writes the full command: (commandName() <writeArgs output>), followed by its trailingText (if any) -- see Command.trailingText.
void	Command.writeArgs(Printer p)	Writes the command arguments (everything between the opening parenthesis + command name and the closing parenthesis); called by Command.write(org.smtlib.sexpr.Printer).

Uses of IVisitor.VisitorException in org.smtlib.logic

Methods in org.smtlib.logic that return IVisitor.VisitorException

Modifier and Type	Method	Description
protected IVisitor.VisitorException	Logic.restrictionError(String message, IExpr e)	Builds a VisitorException for a restriction violation (e.g.

Methods in org.smtlib.logic that throw IVisitor.VisitorException

Modifier and Type	Method	Description
protected void	Logic.checkArraySorts(List<ISort> argSorts, ISort resultSort, IExpr.IIdentifier id)	Checks the Array sorts in a function's argument and result sorts
protected void	Logic.checkArraySorts(ISort sort, IPos pos)	Checks every Array sort within sort, expanding abbreviations, against Logic.allowedArraySort(org.smtlib.ISort.IApplication).
protected abstract void	DifferenceLogic.checkAtom(IExpr.IFcnExpr atom, IExpr lhs, IExpr rhs)	Checks the arguments of a binary arithmetic atom (op lhs rhs).
protected void	QF_IDL.checkAtom(IExpr.IFcnExpr e, IExpr lhs, IExpr rhs)
protected void	QF_RDL.checkAtom(IExpr.IFcnExpr e, IExpr lhs, IExpr rhs)
protected void	Logic.checkBoundArraySorts(IExpr expression)	Checks the Array sorts of the variables bound by quantifiers in expression
void	ALL.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	AUFLIA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	AUFLIRA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	AUFNIRA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	LIA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	LRA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_ABV.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_AUFBV.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_AUFLIA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_AX.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_BV.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_EIA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_FP.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_IDL.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_NIA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_NRA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_RDL.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_UF.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_UFIDL.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_UFLIA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_UFLRA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	QF_UFNRA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	UFLRA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	UFNIA.checkFcnDeclaration(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	ALL.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	AUFLIA.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	AUFLIRA.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	AUFNIRA.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	LIA.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	LRA.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	QF_ABV.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	QF_AUFBV.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	QF_AUFLIA.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	QF_AX.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	QF_BV.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	QF_EIA.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	QF_FP.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	QF_IDL.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	QF_NIA.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	QF_NRA.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	QF_RDL.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	QF_UFIDL.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	QF_UFLIA.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	QF_UFLRA.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	QF_UFNRA.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	UFLRA.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	UFNIA.checkSortDeclaration(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	Logic.noExponentiation(IExpr expression)
void	Logic.noFunctions(IExpr.IIdentifier id, List<ISort> argSorts, ISort resultSort, IExpr definition)
void	Logic.noQuantifiers(IExpr expression)
void	Logic.noSorts(IExpr.IIdentifier id, List<ISort.IParameter> params, ISort expr)
void	ALL.validExpression(IExpr expression)
void	AUFLIA.validExpression(IExpr expression)
void	AUFLIRA.validExpression(IExpr expression)
void	AUFNIRA.validExpression(IExpr expression)
void	DifferenceLogic.validExpression(IExpr expression)
void	LIA.validExpression(IExpr expression)
void	LRA.validExpression(IExpr expression)
void	QF_AUFLIA.validExpression(IExpr expression)
void	QF_AX.validExpression(IExpr expression)
void	QF_BV.validExpression(IExpr expression)
void	QF_EIA.validExpression(IExpr expression)
void	QF_FP.validExpression(IExpr expression)
void	QF_LIA.validExpression(IExpr expression)
void	QF_LRA.validExpression(IExpr expression)
void	QF_NIA.validExpression(IExpr expression)
void	QF_NRA.validExpression(IExpr expression)
void	QF_UF.validExpression(IExpr expression)
void	QF_UFIDL.validExpression(IExpr expression)	QF_UFIDL's :language: no quantifiers; Int symbols as above; and "for every term of the form (op t1 t2) with op in {+, -}, at least one of t1 and t2 is a numeral".
void	QF_UFLIA.validExpression(IExpr expression)
void	QF_UFLRA.validExpression(IExpr expression)
void	UFNIA.validExpression(IExpr expression)

Uses of IVisitor.VisitorException in org.smtlib.sexpr

Methods in org.smtlib.sexpr that return IVisitor.VisitorException

Modifier and Type	Method	Description
IVisitor.VisitorException	Printer.exc(Exception ex, Object possiblePos)	Utility function to create an exception using the message from the first argument and the position from the second, if it is IPosable.

Methods in org.smtlib.sexpr that throw IVisitor.VisitorException

Modifier and Type	Method	Description
<TT> TT	Sexpr.Seq.accept(IVisitor<TT> v)
<TT> TT	Sexpr.Token.accept(IVisitor<TT> v)
protected void	Printer.append(String s)	Appends a string to the writer, converting any IOException to VisitorException.
protected void	Printer.flush()	Flushes the writer, converting any IOException to VisitorException.
<T extends INode> void	Printer.print(T expr)	Prints the argument to the receiver
protected Void	Printer.printCommand(ICommand e)	Prints a no-argument command: (commandName()).
protected Void	Printer.printCommand(ICommand e, Printer.PrintArgs args)	Prints (commandName() args) — the space between name and args is emitted here, so the args lambda should not prepend one.
void	Printer.PrintArgs.run()
Void	Printer.visit(ICommand e)	Fallback for extension command types not covered by a specific visit method; uses reflection to invoke write(Printer) on the command object.
Void	Printer.visit(ICommand.Iassert e)
Void	Printer.visit(ICommand.Icheck_sat e)
Void	Printer.visit(ICommand.Icheck_sat_assuming e)
Void	Printer.visit(ICommand.Icomment e)	A comment is never "(commandName args)" S-expression syntax to begin with, so this doesn't go through printCommand() like every other command here -- instead it's printed directly, now that Comment is a real, typed command rather than going through the generic visit(ICommand) fallback's reflection-based write() lookup (see issue #115; this logic used to live in a write() override on C_comment itself, invoked only via that reflection call -- moved here instead, so printing for every command, including this one, lives in exactly one place: Printer's own typed visit() methods).
Void	Printer.visit(ICommand.Ideclare_const e)
Void	Printer.visit(ICommand.Ideclare_datatype e)
Void	Printer.visit(ICommand.Ideclare_datatypes e)
Void	Printer.visit(ICommand.Ideclare_fun e)
Void	Printer.visit(ICommand.Ideclare_sort e)
Void	Printer.visit(ICommand.Ideclare_sort_parameter e)
Void	Printer.visit(ICommand.Idefine_const e)
Void	Printer.visit(ICommand.Idefine_fun e)
Void	Printer.visit(ICommand.Idefine_fun_rec e)
Void	Printer.visit(ICommand.Idefine_funs_rec e)
Void	Printer.visit(ICommand.Idefine_sort e)
Void	Printer.visit(ICommand.Iecho e)
Void	Printer.visit(ICommand.Iexit e)
Void	Printer.visit(ICommand.Iget_assertions e)
Void	Printer.visit(ICommand.Iget_assignment e)
Void	Printer.visit(ICommand.Iget_info e)
Void	Printer.visit(ICommand.Iget_model e)
Void	Printer.visit(ICommand.Iget_option e)
Void	Printer.visit(ICommand.Iget_proof e)
Void	Printer.visit(ICommand.Iget_unsat_assumptions e)
Void	Printer.visit(ICommand.Iget_unsat_core e)
Void	Printer.visit(ICommand.Iget_value e)
Void	Printer.visit(ICommand.Ipop e)
Void	Printer.visit(ICommand.Ipush e)
Void	Printer.visit(ICommand.Ireset e)
Void	Printer.visit(ICommand.Ireset_assertions e)
Void	Printer.visit(ICommand.IScript e)
Void	Printer.visit(ICommand.Iset_info e)
Void	Printer.visit(ICommand.Iset_logic e)
Void	Printer.visit(ICommand.Iset_option e)
Void	Printer.visit(IExpr.IAsIdentifier e)
Void	Printer.visit(IExpr.IAttribute<? extends IAttributeValue> e)
Void	Printer.visit(IExpr.IAttributedExpr e)
Void	Printer.visit(IExpr.IBinaryLiteral e)
Void	Printer.visit(IExpr.IBinding e)
Void	Printer.visit(IExpr.IConstructor e)
Void	Printer.visit(IExpr.IDecimal e)
Void	Printer.visit(IExpr.IDeclaration e)
Void	Printer.visit(IExpr.IError e)
Void	Printer.visit(IExpr.IExists e)
Void	Printer.visit(IExpr.IFcnExpr e)
Void	Printer.visit(IExpr.IForall e)
Void	Printer.visit(IExpr.IFunctionDeclaration e)
Void	Printer.visit(IExpr.IHexLiteral e)
Void	Printer.visit(IExpr.IKeyword e)
Void	Printer.visit(IExpr.ILambda e)
Void	Printer.visit(IExpr.ILet e)
Void	Printer.visit(IExpr.IMatch e)
Void	Printer.visit(IExpr.IMatchCase e)
Void	Printer.visit(IExpr.INumeral e)
Void	Printer.visit(IExpr.IParameterizedIdentifier e)
Void	Printer.visit(IExpr.IPattern e)
Void	Printer.visit(IExpr.IPatternTerms e)
Void	Printer.visit(IExpr.ISelector e)
Void	Printer.visit(IExpr.ISortDeclaration e)
Void	Printer.visit(IExpr.IStringLiteral e)
Void	Printer.visit(IExpr.ISymbol e)
Void	Printer.visit(ILogic s)
Void	Printer.visit(IResponse e)
Void	Printer.visit(IResponse.IAssertionsResponse e)
Void	Printer.visit(IResponse.IAssignmentResponse e)
Void	Printer.visit(IResponse.IAttributeList e)
Void	Printer.visit(IResponse.IError e)
Void	Printer.visit(IResponse.IProofResponse e)	Prints the proof s-expression compactly; a proof that is a list of lists (e.g.
Void	Printer.visit(IResponse.IUnsatAssumptionsResponse e)
Void	Printer.visit(IResponse.IUnsatCoreResponse e)
Void	Printer.visit(IResponse.IValueResponse e)
Void	Printer.visit(ISort.IAbbreviation s)
Void	Printer.visit(ISort.IApplication s)
Void	Printer.visit(ISort.IDatatype e)
Void	Printer.visit(ISort.IFamily s)
Void	Printer.visit(ISort.IFcnSort s)
Void	Printer.visit(ISort.IParameter s)
Void	Printer.visit(ITheory s)
Void	Printer.visit(ISexpr.ISeq e)
Void	Printer.visit(ISexpr.IToken<?> e)
Void	Printer.WithLines.visit(ICommand.IScript e)
static <T extends INode> void	Printer.WithLines.write(SMT.Configuration smtConfig, PrintStream w, T e)	Writes the given expression to the given stream, following the given Configuration's rules.
static <T extends INode> void	Printer.WithLines.write(SMT.Configuration smtConfig, Writer w, T e)	Writes the given expression to the given writer, following the given Configuration's rules.
static <T extends INode> void	Printer.write(SMT.Configuration smtConfig, PrintStream w, T e)	Writes the given expression to the given stream, following the given Configuration's rules.
static <T extends INode> void	Printer.write(SMT.Configuration smtConfig, Writer w, T e)	Writes the given expression to the given writer, following the given Configuration's rules.

Uses of IVisitor.VisitorException in org.smtlib.solvers

Methods in org.smtlib.solvers that throw IVisitor.VisitorException

Modifier and Type	Method	Description
protected <T extends IExpr> void	Solver_z3_4_3.Translator.leftassoc(String fcnname, int length, Iterator<T> iter)
String	Solver_simplify.translate(IExpr expr)
protected String	Solver_smt.translate(INode sexpr)	Translates an S-expression into SMT syntax; this solver uses the standard S-expression concrete syntax except for a Bool-quantifier workaround (see Printer).
protected String	Solver_z3_4_3.translate(INode sexpr)	Translates an S-expression into Z3 syntax
protected String	Solver_z3_4_5.translate(INode node)	z3 4.5 rejects every check-sat-assuming ("invalid check-sat-assuming command, '(', expected", a parser bug), so it is sent as z3's legacy (check-sat a1 ...
Void	Printer.visit(IExpr.IExists e)
Void	Printer.visit(IExpr.IForall e)
String	Solver_simplify.Translator.visit(ICommand e)
String	Solver_simplify.Translator.visit(ICommand.IScript e)
String	Solver_simplify.Translator.visit(IExpr.IAsIdentifier e)
String	Solver_simplify.Translator.visit(IExpr.IAttribute<?> e)
String	Solver_simplify.Translator.visit(IExpr.IAttributedExpr e)
String	Solver_simplify.Translator.visit(IExpr.IBinaryLiteral e)
String	Solver_simplify.Translator.visit(IExpr.IBinding e)
String	Solver_simplify.Translator.visit(IExpr.IConstructor e)
String	Solver_simplify.Translator.visit(IExpr.IDecimal e)
String	Solver_simplify.Translator.visit(IExpr.IDeclaration e)
String	Solver_simplify.Translator.visit(IExpr.IError e)
String	Solver_simplify.Translator.visit(IExpr.IExists e)
String	Solver_simplify.Translator.visit(IExpr.IFcnExpr e)
String	Solver_simplify.Translator.visit(IExpr.IForall e)
String	Solver_simplify.Translator.visit(IExpr.IFunctionDeclaration e)
String	Solver_simplify.Translator.visit(IExpr.IHexLiteral e)
String	Solver_simplify.Translator.visit(IExpr.IKeyword e)
String	Solver_simplify.Translator.visit(IExpr.ILambda e)
String	Solver_simplify.Translator.visit(IExpr.ILet e)
String	Solver_simplify.Translator.visit(IExpr.IMatch e)
String	Solver_simplify.Translator.visit(IExpr.IMatchCase e)
String	Solver_simplify.Translator.visit(IExpr.INumeral e)
String	Solver_simplify.Translator.visit(IExpr.IParameterizedIdentifier e)
String	Solver_simplify.Translator.visit(IExpr.IPattern e)
String	Solver_simplify.Translator.visit(IExpr.ISelector e)
String	Solver_simplify.Translator.visit(IExpr.ISortDeclaration e)
String	Solver_simplify.Translator.visit(IExpr.IStringLiteral e)
String	Solver_simplify.Translator.visit(IExpr.ISymbol e)
String	Solver_simplify.Translator.visit(ILogic s)
String	Solver_simplify.Translator.visit(IResponse e)
String	Solver_simplify.Translator.visit(IResponse.IAssertionsResponse e)
String	Solver_simplify.Translator.visit(IResponse.IAssignmentResponse e)
String	Solver_simplify.Translator.visit(IResponse.IAttributeList e)
String	Solver_simplify.Translator.visit(IResponse.IError e)
String	Solver_simplify.Translator.visit(IResponse.IProofResponse e)
String	Solver_simplify.Translator.visit(IResponse.IUnsatAssumptionsResponse e)
String	Solver_simplify.Translator.visit(IResponse.IUnsatCoreResponse e)
String	Solver_simplify.Translator.visit(IResponse.IValueResponse e)
String	Solver_simplify.Translator.visit(ISort.IAbbreviation s)
String	Solver_simplify.Translator.visit(ISort.IApplication s)
String	Solver_simplify.Translator.visit(ISort.IDatatype e)
String	Solver_simplify.Translator.visit(ISort.IFamily s)
String	Solver_simplify.Translator.visit(ISort.IFcnSort s)
String	Solver_simplify.Translator.visit(ISort.IParameter s)
String	Solver_simplify.Translator.visit(ITheory s)
String	Solver_simplify.Translator.visit(ISexpr.ISeq e)
String	Solver_simplify.Translator.visit(ISexpr.IToken<?> e)
Void	Solver_z3_4_3.Translator.visit(IExpr.IFcnExpr e)
static <T extends INode> void	Printer.write(SMT.Configuration smtConfig, PrintStream w, T e)	Writes the given expression to the given stream, following the given Configuration's rules.
static <T extends INode> void	Printer.write(SMT.Configuration smtConfig, Writer w, T e)	Writes the given expression to the given writer, following the given Configuration's rules.