Package org.smtlib
Interface INode
- All Known Subinterfaces:
IAttributeValue,ICommand,ICommand.Iassert,ICommand.Icheck_sat,ICommand.Icheck_sat_assuming,ICommand.Icomment,ICommand.Ideclare_const,ICommand.Ideclare_datatype,ICommand.Ideclare_datatypes,ICommand.Ideclare_fun,ICommand.Ideclare_sort,ICommand.Ideclare_sort_parameter,ICommand.Idefine_const,ICommand.Idefine_fun,ICommand.Idefine_fun_rec,ICommand.Idefine_funs_rec,ICommand.Idefine_sort,ICommand.Iecho,ICommand.Iexit,ICommand.Iget_assertions,ICommand.Iget_assignment,ICommand.Iget_info,ICommand.Iget_model,ICommand.Iget_option,ICommand.Iget_proof,ICommand.Iget_unsat_assumptions,ICommand.Iget_unsat_core,ICommand.Iget_value,ICommand.Ipop,ICommand.Ipush,ICommand.Ireset,ICommand.Ireset_assertions,ICommand.IScript,ICommand.Iset_info,ICommand.Iset_logic,ICommand.Iset_option,Iexec,IExpr,IExpr.IAsIdentifier,IExpr.IAttribute<TT>,IExpr.IAttributedExpr,IExpr.IBinaryLiteral,IExpr.IBinding,IExpr.IConstructor,IExpr.IDecimal,IExpr.IDeclaration,IExpr.IError,IExpr.IExists,IExpr.IFcnExpr,IExpr.IForall,IExpr.IFunctionDeclaration,IExpr.IHexLiteral,IExpr.IIdentifier,IExpr.IIndex,IExpr.IKeyword,IExpr.ILambda,IExpr.ILet,IExpr.ILiteral,IExpr.IMatch,IExpr.IMatchCase,IExpr.INumeral,IExpr.IParameterizedIdentifier,IExpr.IPattern,IExpr.IPatternTerms,IExpr.IQualifiedIdentifier,IExpr.ISelector,IExpr.ISortDeclaration,IExpr.IStringLiteral,IExpr.ISymbol,ILogic,IResponse,IResponse.IAssertionsResponse,IResponse.IAssignmentResponse,IResponse.IAttributeList,IResponse.IError,IResponse.IProofResponse,IResponse.IUnsatAssumptionsResponse,IResponse.IUnsatCoreResponse,IResponse.IValueResponse,ISexpr,ISexpr.ISeq,ISexpr.IToken<T>,ISort,ISort.IAbbreviation,ISort.IApplication,ISort.IDatatype,ISort.IDefinition,ISort.IErrorDefinition,ISort.IFamily,ISort.IFcnSort,ISort.IParameter,ITheory,Iwhat
- All Known Implementing Classes:
AbstractSolver.Pending,ALL,AUFLIA,AUFLIRA,AUFNIRA,C_assert,C_check_sat,C_check_sat_assuming,C_comment,C_declare_const,C_declare_datatype,C_declare_datatypes,C_declare_fun,C_declare_sort,C_declare_sort_parameter,C_define_const,C_define_fun,C_define_fun_rec,C_define_funs_rec,C_define_sort,C_echo,C_exec,C_exit,C_get_assertions,C_get_assignment,C_get_info,C_get_model,C_get_option,C_get_proof,C_get_unsat_assumptions,C_get_unsat_core,C_get_value,C_pop,C_push,C_reset,C_reset_assertions,C_set_info,C_set_logic,C_set_option,C_what,Command,DifferenceLogic,LIA,Logic,LRA,Pos.AbstractExpr,Pos.Printable,QF_ABV,QF_AUFBV,QF_AUFLIA,QF_AX,QF_BV,QF_EIA,QF_FP,QF_IDL,QF_LIA,QF_LRA,QF_NIA,QF_NRA,QF_RDL,QF_UF,QF_UFBV,QF_UFIDL,QF_UFLIA,QF_UFLRA,QF_UFNRA,Response.AssertionsResponse,Response.AssignmentResponse,Response.Error,Response.ProofResponse,Response.Seq,Response.UnsatAssumptionsResponse,Response.UnsatCoreResponse,Response.ValueResponse,Script,Sexpr,Sexpr.Seq,Sexpr.Token,SMTExpr,SMTExpr.AsIdentifier,SMTExpr.Attribute,SMTExpr.AttributedExpr,SMTExpr.BinaryLiteral,SMTExpr.Binding,SMTExpr.Constructor,SMTExpr.Datatype,SMTExpr.Decimal,SMTExpr.Declaration,SMTExpr.Error,SMTExpr.Exists,SMTExpr.FcnExpr,SMTExpr.Forall,SMTExpr.FunctionDeclaration,SMTExpr.HexLiteral,SMTExpr.Keyword,SMTExpr.Lambda,SMTExpr.Let,SMTExpr.Literal,SMTExpr.Logic,SMTExpr.Match,SMTExpr.MatchCase,SMTExpr.Numeral,SMTExpr.ParameterizedIdentifier,SMTExpr.Pattern,SMTExpr.PatternTerms,SMTExpr.Selector,SMTExpr.SortDeclaration,SMTExpr.StringLiteral,SMTExpr.Symbol,SMTExpr.Theory,Sort,Sort.Abbreviation,Sort.Application,Sort.ErrorDefinition,Sort.Family,Sort.FcnSort,Sort.Parameter,UFLRA,UFNIA
public interface INode
This interface is defined and implemented as a marker that
the accept method is available and to ensure that
subtypes implement the accept method.
Most implementations extend org.smtlib.impl.Pos.Printable, whose
toString() delegates to the default Printer for debugger/IDE
display only - never rely on toString() for program logic; use
IPrinter/Printer explicitly for real output.
- Author:
- David Cok
-
Method Summary
-
Method Details
-
accept
The accept method corresponding to IVisitor, to be implemented in each subclass as { return v.visit(this); }- Type Parameters:
T- the return type desired from the visit methods- Parameters:
v- the visitor class- Returns:
- the value returned by the visit method
- Throws:
IVisitor.VisitorException
-