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

    Modifier and Type
    Method
    Description
    <T> T
    The accept method corresponding to IVisitor, to be implemented in each subclass as { return v.visit(this); }
  • Method Details

    • accept

      <T> T accept(IVisitor<T> v) throws IVisitor.VisitorException
      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