Uses of Interface
org.smtlib.IVisitor

Packages that use IVisitor

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

Classes in org.smtlib that implement IVisitor

Modifier and Type	Class	Description
static class	IVisitor.TreeVisitor<T>	This class is an implementation of IVisitor meant for further derivation: each visitor is implemented to visit its children without doing anything else; the default return value is null.
class	TypeChecker	This class is a visitor that type-checks a formula

Methods in org.smtlib with parameters of type IVisitor

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); }

Uses of IVisitor in org.smtlib.command

Methods in org.smtlib.command with parameters of type IVisitor

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

Methods in org.smtlib.ext with parameters of type IVisitor

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

Uses of IVisitor in org.smtlib.impl

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

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)

Uses of IVisitor in org.smtlib.sexpr

Classes in org.smtlib.sexpr that implement IVisitor

Modifier and Type	Class	Description
class	Printer	This class writes out SMT-LIB ASTs as concrete S-expression syntax; aside from white space between tokens it should simply reverse what the Parser class does.
static class	Printer.WithLines

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

Modifier and Type	Method	Description
<TT> TT	Sexpr.Seq.accept(IVisitor<TT> v)
<TT> TT	Sexpr.Token.accept(IVisitor<TT> v)

Uses of IVisitor in org.smtlib.solvers

Classes in org.smtlib.solvers that implement IVisitor

Modifier and Type	Class	Description
class	Printer
static class	Solver_simplify.Translator
class	Solver_z3_4_3.Translator