Class SMTLIBv2BaseVisitor<Result>

This class provides an empty implementation of ISMTLIBv2Visitor<Result>, which can be extended to create a visitor which only needs to handle a subset of the available methods.

Inheritance

System.Object

SMTLIBv2BaseVisitor<Result>

Implements

ISMTLIBv2Visitor<Result>

IParseTreeVisitor<Result>

Namespace: GCore.Antlr.Grammers.Smtlibv2

Assembly: Smtlibv2.dll

Syntax

public class SMTLIBv2BaseVisitor<Result> : AbstractParseTreeVisitor<Result>, ISMTLIBv2Visitor<Result>, IParseTreeVisitor<Result>

Type Parameters

Name	Description
Result	The return type of the visit operation.

Methods

VisitAttribute(SMTLIBv2Parser.AttributeContext)

Visit a parse tree produced by attribute().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitAttribute(SMTLIBv2Parser.AttributeContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.AttributeContext	context	The parse tree.

Returns

Type	Description
Result

VisitAttribute_value(SMTLIBv2Parser.Attribute_valueContext)

Visit a parse tree produced by attribute_value().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitAttribute_value(SMTLIBv2Parser.Attribute_valueContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Attribute_valueContext	context	The parse tree.

Returns

Type	Description
Result

VisitB_value(SMTLIBv2Parser.B_valueContext)

Visit a parse tree produced by b_value().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitB_value(SMTLIBv2Parser.B_valueContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.B_valueContext	context	The parse tree.

Returns

Type	Description
Result

VisitBinary(SMTLIBv2Parser.BinaryContext)

Visit a parse tree produced by binary().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitBinary(SMTLIBv2Parser.BinaryContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.BinaryContext	context	The parse tree.

Returns

Type	Description
Result

VisitCheck_sat_response(SMTLIBv2Parser.Check_sat_responseContext)

Visit a parse tree produced by check_sat_response().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitCheck_sat_response(SMTLIBv2Parser.Check_sat_responseContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Check_sat_responseContext	context	The parse tree.

Returns

Type	Description
Result

VisitCmd_assert(SMTLIBv2Parser.Cmd_assertContext)

Visit a parse tree produced by cmd_assert().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitCmd_assert(SMTLIBv2Parser.Cmd_assertContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Cmd_assertContext	context	The parse tree.

Returns

Type	Description
Result

VisitCmd_checkSat(SMTLIBv2Parser.Cmd_checkSatContext)

Visit a parse tree produced by cmd_checkSat().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitCmd_checkSat(SMTLIBv2Parser.Cmd_checkSatContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Cmd_checkSatContext	context	The parse tree.

Returns

Type	Description
Result

VisitCmd_checkSatAssuming(SMTLIBv2Parser.Cmd_checkSatAssumingContext)

Visit a parse tree produced by cmd_checkSatAssuming().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitCmd_checkSatAssuming(SMTLIBv2Parser.Cmd_checkSatAssumingContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Cmd_checkSatAssumingContext	context	The parse tree.

Returns

Type	Description
Result

VisitCmd_declareConst(SMTLIBv2Parser.Cmd_declareConstContext)

Visit a parse tree produced by cmd_declareConst().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitCmd_declareConst(SMTLIBv2Parser.Cmd_declareConstContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Cmd_declareConstContext	context	The parse tree.

Returns

Type	Description
Result

VisitCmd_declareDatatype(SMTLIBv2Parser.Cmd_declareDatatypeContext)

Visit a parse tree produced by cmd_declareDatatype().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitCmd_declareDatatype(SMTLIBv2Parser.Cmd_declareDatatypeContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Cmd_declareDatatypeContext	context	The parse tree.

Returns

Type	Description
Result

VisitCmd_declareDatatypes(SMTLIBv2Parser.Cmd_declareDatatypesContext)

Visit a parse tree produced by cmd_declareDatatypes().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitCmd_declareDatatypes(SMTLIBv2Parser.Cmd_declareDatatypesContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Cmd_declareDatatypesContext	context	The parse tree.

Returns

Type	Description
Result

VisitCmd_declareFun(SMTLIBv2Parser.Cmd_declareFunContext)

Visit a parse tree produced by cmd_declareFun().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitCmd_declareFun(SMTLIBv2Parser.Cmd_declareFunContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Cmd_declareFunContext	context	The parse tree.

Returns

Type	Description
Result

VisitCmd_declareSort(SMTLIBv2Parser.Cmd_declareSortContext)

Visit a parse tree produced by cmd_declareSort().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitCmd_declareSort(SMTLIBv2Parser.Cmd_declareSortContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Cmd_declareSortContext	context	The parse tree.

Returns

Type	Description
Result

VisitCmd_defineFun(SMTLIBv2Parser.Cmd_defineFunContext)

Visit a parse tree produced by cmd_defineFun().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitCmd_defineFun(SMTLIBv2Parser.Cmd_defineFunContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Cmd_defineFunContext	context	The parse tree.

Returns

Type	Description
Result

VisitCmd_defineFunRec(SMTLIBv2Parser.Cmd_defineFunRecContext)

Visit a parse tree produced by cmd_defineFunRec().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitCmd_defineFunRec(SMTLIBv2Parser.Cmd_defineFunRecContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Cmd_defineFunRecContext	context	The parse tree.

Returns

Type	Description
Result

VisitCmd_defineFunsRec(SMTLIBv2Parser.Cmd_defineFunsRecContext)

Visit a parse tree produced by cmd_defineFunsRec().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitCmd_defineFunsRec(SMTLIBv2Parser.Cmd_defineFunsRecContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Cmd_defineFunsRecContext	context	The parse tree.

Returns

Type	Description
Result

VisitCmd_defineSort(SMTLIBv2Parser.Cmd_defineSortContext)

Visit a parse tree produced by cmd_defineSort().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitCmd_defineSort(SMTLIBv2Parser.Cmd_defineSortContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Cmd_defineSortContext	context	The parse tree.

Returns

Type	Description
Result

VisitCmd_echo(SMTLIBv2Parser.Cmd_echoContext)

Visit a parse tree produced by cmd_echo().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitCmd_echo(SMTLIBv2Parser.Cmd_echoContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Cmd_echoContext	context	The parse tree.

Returns

Type	Description
Result

VisitCmd_exit(SMTLIBv2Parser.Cmd_exitContext)

Visit a parse tree produced by cmd_exit().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitCmd_exit(SMTLIBv2Parser.Cmd_exitContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Cmd_exitContext	context	The parse tree.

Returns

Type	Description
Result

VisitCmd_getAssertions(SMTLIBv2Parser.Cmd_getAssertionsContext)

Visit a parse tree produced by cmd_getAssertions().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitCmd_getAssertions(SMTLIBv2Parser.Cmd_getAssertionsContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Cmd_getAssertionsContext	context	The parse tree.

Returns

Type	Description
Result

VisitCmd_getAssignment(SMTLIBv2Parser.Cmd_getAssignmentContext)

Visit a parse tree produced by cmd_getAssignment().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitCmd_getAssignment(SMTLIBv2Parser.Cmd_getAssignmentContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Cmd_getAssignmentContext	context	The parse tree.

Returns

Type	Description
Result

VisitCmd_getInfo(SMTLIBv2Parser.Cmd_getInfoContext)

Visit a parse tree produced by cmd_getInfo().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitCmd_getInfo(SMTLIBv2Parser.Cmd_getInfoContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Cmd_getInfoContext	context	The parse tree.

Returns

Type	Description
Result

VisitCmd_getModel(SMTLIBv2Parser.Cmd_getModelContext)

Visit a parse tree produced by cmd_getModel().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitCmd_getModel(SMTLIBv2Parser.Cmd_getModelContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Cmd_getModelContext	context	The parse tree.

Returns

Type	Description
Result

VisitCmd_getOption(SMTLIBv2Parser.Cmd_getOptionContext)

Visit a parse tree produced by cmd_getOption().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitCmd_getOption(SMTLIBv2Parser.Cmd_getOptionContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Cmd_getOptionContext	context	The parse tree.

Returns

Type	Description
Result

VisitCmd_getProof(SMTLIBv2Parser.Cmd_getProofContext)

Visit a parse tree produced by cmd_getProof().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitCmd_getProof(SMTLIBv2Parser.Cmd_getProofContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Cmd_getProofContext	context	The parse tree.

Returns

Type	Description
Result

VisitCmd_getUnsatAssumptions(SMTLIBv2Parser.Cmd_getUnsatAssumptionsContext)

Visit a parse tree produced by cmd_getUnsatAssumptions().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitCmd_getUnsatAssumptions(SMTLIBv2Parser.Cmd_getUnsatAssumptionsContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Cmd_getUnsatAssumptionsContext	context	The parse tree.

Returns

Type	Description
Result

VisitCmd_getUnsatCore(SMTLIBv2Parser.Cmd_getUnsatCoreContext)

Visit a parse tree produced by cmd_getUnsatCore().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitCmd_getUnsatCore(SMTLIBv2Parser.Cmd_getUnsatCoreContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Cmd_getUnsatCoreContext	context	The parse tree.

Returns

Type	Description
Result

VisitCmd_getValue(SMTLIBv2Parser.Cmd_getValueContext)

Visit a parse tree produced by cmd_getValue().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitCmd_getValue(SMTLIBv2Parser.Cmd_getValueContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Cmd_getValueContext	context	The parse tree.

Returns

Type	Description
Result

VisitCmd_pop(SMTLIBv2Parser.Cmd_popContext)

Visit a parse tree produced by cmd_pop().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitCmd_pop(SMTLIBv2Parser.Cmd_popContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Cmd_popContext	context	The parse tree.

Returns

Type	Description
Result

VisitCmd_push(SMTLIBv2Parser.Cmd_pushContext)

Visit a parse tree produced by cmd_push().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitCmd_push(SMTLIBv2Parser.Cmd_pushContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Cmd_pushContext	context	The parse tree.

Returns

Type	Description
Result

VisitCmd_reset(SMTLIBv2Parser.Cmd_resetContext)

Visit a parse tree produced by cmd_reset().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitCmd_reset(SMTLIBv2Parser.Cmd_resetContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Cmd_resetContext	context	The parse tree.

Returns

Type	Description
Result

VisitCmd_resetAssertions(SMTLIBv2Parser.Cmd_resetAssertionsContext)

Visit a parse tree produced by cmd_resetAssertions().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitCmd_resetAssertions(SMTLIBv2Parser.Cmd_resetAssertionsContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Cmd_resetAssertionsContext	context	The parse tree.

Returns

Type	Description
Result

VisitCmd_setInfo(SMTLIBv2Parser.Cmd_setInfoContext)

Visit a parse tree produced by cmd_setInfo().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitCmd_setInfo(SMTLIBv2Parser.Cmd_setInfoContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Cmd_setInfoContext	context	The parse tree.

Returns

Type	Description
Result

VisitCmd_setLogic(SMTLIBv2Parser.Cmd_setLogicContext)

Visit a parse tree produced by cmd_setLogic().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitCmd_setLogic(SMTLIBv2Parser.Cmd_setLogicContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Cmd_setLogicContext	context	The parse tree.

Returns

Type	Description
Result

VisitCmd_setOption(SMTLIBv2Parser.Cmd_setOptionContext)

Visit a parse tree produced by cmd_setOption().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitCmd_setOption(SMTLIBv2Parser.Cmd_setOptionContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Cmd_setOptionContext	context	The parse tree.

Returns

Type	Description
Result

VisitCommand(SMTLIBv2Parser.CommandContext)

Visit a parse tree produced by command().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitCommand(SMTLIBv2Parser.CommandContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.CommandContext	context	The parse tree.

Returns

Type	Description
Result

VisitConstructor_dec(SMTLIBv2Parser.Constructor_decContext)

Visit a parse tree produced by constructor_dec().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitConstructor_dec(SMTLIBv2Parser.Constructor_decContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Constructor_decContext	context	The parse tree.

Returns

Type	Description
Result

VisitDatatype_dec(SMTLIBv2Parser.Datatype_decContext)

Visit a parse tree produced by datatype_dec().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitDatatype_dec(SMTLIBv2Parser.Datatype_decContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Datatype_decContext	context	The parse tree.

Returns

Type	Description
Result

VisitDecimal(SMTLIBv2Parser.DecimalContext)

Visit a parse tree produced by .

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitDecimal(SMTLIBv2Parser.DecimalContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.DecimalContext	context	The parse tree.

Returns

Type	Description
Result

VisitEcho_response(SMTLIBv2Parser.Echo_responseContext)

Visit a parse tree produced by echo_response().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitEcho_response(SMTLIBv2Parser.Echo_responseContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Echo_responseContext	context	The parse tree.

Returns

Type	Description
Result

VisitError_behaviour(SMTLIBv2Parser.Error_behaviourContext)

Visit a parse tree produced by error_behaviour().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitError_behaviour(SMTLIBv2Parser.Error_behaviourContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Error_behaviourContext	context	The parse tree.

Returns

Type	Description
Result

VisitFun_symbol_decl(SMTLIBv2Parser.Fun_symbol_declContext)

Visit a parse tree produced by fun_symbol_decl().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitFun_symbol_decl(SMTLIBv2Parser.Fun_symbol_declContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Fun_symbol_declContext	context	The parse tree.

Returns

Type	Description
Result

VisitFunction_dec(SMTLIBv2Parser.Function_decContext)

Visit a parse tree produced by function_dec().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitFunction_dec(SMTLIBv2Parser.Function_decContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Function_decContext	context	The parse tree.

Returns

Type	Description
Result

VisitFunction_def(SMTLIBv2Parser.Function_defContext)

Visit a parse tree produced by function_def().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitFunction_def(SMTLIBv2Parser.Function_defContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Function_defContext	context	The parse tree.

Returns

Type	Description
Result

VisitGeneral_response(SMTLIBv2Parser.General_responseContext)

Visit a parse tree produced by general_response().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitGeneral_response(SMTLIBv2Parser.General_responseContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.General_responseContext	context	The parse tree.

Returns

Type	Description
Result

VisitGeneralReservedWord(SMTLIBv2Parser.GeneralReservedWordContext)

Visit a parse tree produced by generalReservedWord().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitGeneralReservedWord(SMTLIBv2Parser.GeneralReservedWordContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.GeneralReservedWordContext	context	The parse tree.

Returns

Type	Description
Result

VisitGet_assertions_response(SMTLIBv2Parser.Get_assertions_responseContext)

Visit a parse tree produced by get_assertions_response().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitGet_assertions_response(SMTLIBv2Parser.Get_assertions_responseContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Get_assertions_responseContext	context	The parse tree.

Returns

Type	Description
Result

VisitGet_assignment_response(SMTLIBv2Parser.Get_assignment_responseContext)

Visit a parse tree produced by get_assignment_response().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitGet_assignment_response(SMTLIBv2Parser.Get_assignment_responseContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Get_assignment_responseContext	context	The parse tree.

Returns

Type	Description
Result

VisitGet_info_response(SMTLIBv2Parser.Get_info_responseContext)

Visit a parse tree produced by get_info_response().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitGet_info_response(SMTLIBv2Parser.Get_info_responseContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Get_info_responseContext	context	The parse tree.

Returns

Type	Description
Result

VisitGet_model_response(SMTLIBv2Parser.Get_model_responseContext)

Visit a parse tree produced by get_model_response().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitGet_model_response(SMTLIBv2Parser.Get_model_responseContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Get_model_responseContext	context	The parse tree.

Returns

Type	Description
Result

VisitGet_option_response(SMTLIBv2Parser.Get_option_responseContext)

Visit a parse tree produced by get_option_response().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitGet_option_response(SMTLIBv2Parser.Get_option_responseContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Get_option_responseContext	context	The parse tree.

Returns

Type	Description
Result

VisitGet_proof_response(SMTLIBv2Parser.Get_proof_responseContext)

Visit a parse tree produced by get_proof_response().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitGet_proof_response(SMTLIBv2Parser.Get_proof_responseContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Get_proof_responseContext	context	The parse tree.

Returns

Type	Description
Result

VisitGet_unsat_assump_response(SMTLIBv2Parser.Get_unsat_assump_responseContext)

Visit a parse tree produced by get_unsat_assump_response().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitGet_unsat_assump_response(SMTLIBv2Parser.Get_unsat_assump_responseContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Get_unsat_assump_responseContext	context	The parse tree.

Returns

Type	Description
Result

VisitGet_unsat_core_response(SMTLIBv2Parser.Get_unsat_core_responseContext)

Visit a parse tree produced by get_unsat_core_response().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitGet_unsat_core_response(SMTLIBv2Parser.Get_unsat_core_responseContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Get_unsat_core_responseContext	context	The parse tree.

Returns

Type	Description
Result

VisitGet_value_response(SMTLIBv2Parser.Get_value_responseContext)

Visit a parse tree produced by get_value_response().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitGet_value_response(SMTLIBv2Parser.Get_value_responseContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Get_value_responseContext	context	The parse tree.

Returns

Type	Description
Result

VisitHexadecimal(SMTLIBv2Parser.HexadecimalContext)

Visit a parse tree produced by hexadecimal().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitHexadecimal(SMTLIBv2Parser.HexadecimalContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.HexadecimalContext	context	The parse tree.

Returns

Type	Description
Result

VisitIdentifier(SMTLIBv2Parser.IdentifierContext)

Visit a parse tree produced by identifier().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitIdentifier(SMTLIBv2Parser.IdentifierContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.IdentifierContext	context	The parse tree.

Returns

Type	Description
Result

VisitIndex(SMTLIBv2Parser.IndexContext)

Visit a parse tree produced by index().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitIndex(SMTLIBv2Parser.IndexContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.IndexContext	context	The parse tree.

Returns

Type	Description
Result

VisitInfo_flag(SMTLIBv2Parser.Info_flagContext)

Visit a parse tree produced by info_flag().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitInfo_flag(SMTLIBv2Parser.Info_flagContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Info_flagContext	context	The parse tree.

Returns

Type	Description
Result

VisitInfo_response(SMTLIBv2Parser.Info_responseContext)

Visit a parse tree produced by info_response().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitInfo_response(SMTLIBv2Parser.Info_responseContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Info_responseContext	context	The parse tree.

Returns

Type	Description
Result

VisitKeyword(SMTLIBv2Parser.KeywordContext)

Visit a parse tree produced by keyword().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitKeyword(SMTLIBv2Parser.KeywordContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.KeywordContext	context	The parse tree.

Returns

Type	Description
Result

VisitLogic(SMTLIBv2Parser.LogicContext)

Visit a parse tree produced by logic().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitLogic(SMTLIBv2Parser.LogicContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.LogicContext	context	The parse tree.

Returns

Type	Description
Result

VisitLogic_attribue(SMTLIBv2Parser.Logic_attribueContext)

Visit a parse tree produced by logic_attribue().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitLogic_attribue(SMTLIBv2Parser.Logic_attribueContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Logic_attribueContext	context	The parse tree.

Returns

Type	Description
Result

VisitMatch_case(SMTLIBv2Parser.Match_caseContext)

Visit a parse tree produced by match_case().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitMatch_case(SMTLIBv2Parser.Match_caseContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Match_caseContext	context	The parse tree.

Returns

Type	Description
Result

VisitMeta_spec_constant(SMTLIBv2Parser.Meta_spec_constantContext)

Visit a parse tree produced by meta_spec_constant().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitMeta_spec_constant(SMTLIBv2Parser.Meta_spec_constantContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Meta_spec_constantContext	context	The parse tree.

Returns

Type	Description
Result

VisitModel_response(SMTLIBv2Parser.Model_responseContext)

Visit a parse tree produced by model_response().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitModel_response(SMTLIBv2Parser.Model_responseContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Model_responseContext	context	The parse tree.

Returns

Type	Description
Result

VisitNumeral(SMTLIBv2Parser.NumeralContext)

Visit a parse tree produced by numeral().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitNumeral(SMTLIBv2Parser.NumeralContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.NumeralContext	context	The parse tree.

Returns

Type	Description
Result

VisitOption(SMTLIBv2Parser.OptionContext)

Visit a parse tree produced by option().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitOption(SMTLIBv2Parser.OptionContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.OptionContext	context	The parse tree.

Returns

Type	Description
Result

VisitPar_fun_symbol_decl(SMTLIBv2Parser.Par_fun_symbol_declContext)

Visit a parse tree produced by par_fun_symbol_decl().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitPar_fun_symbol_decl(SMTLIBv2Parser.Par_fun_symbol_declContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Par_fun_symbol_declContext	context	The parse tree.

Returns

Type	Description
Result

VisitPattern(SMTLIBv2Parser.PatternContext)

Visit a parse tree produced by pattern().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitPattern(SMTLIBv2Parser.PatternContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.PatternContext	context	The parse tree.

Returns

Type	Description
Result

VisitPredefKeyword(SMTLIBv2Parser.PredefKeywordContext)

Visit a parse tree produced by predefKeyword().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitPredefKeyword(SMTLIBv2Parser.PredefKeywordContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.PredefKeywordContext	context	The parse tree.

Returns

Type	Description
Result

VisitPredefSymbol(SMTLIBv2Parser.PredefSymbolContext)

Visit a parse tree produced by predefSymbol().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitPredefSymbol(SMTLIBv2Parser.PredefSymbolContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.PredefSymbolContext	context	The parse tree.

Returns

Type	Description
Result

VisitProp_literal(SMTLIBv2Parser.Prop_literalContext)

Visit a parse tree produced by prop_literal().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitProp_literal(SMTLIBv2Parser.Prop_literalContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Prop_literalContext	context	The parse tree.

Returns

Type	Description
Result

VisitQual_identifer(SMTLIBv2Parser.Qual_identiferContext)

Visit a parse tree produced by qual_identifer().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitQual_identifer(SMTLIBv2Parser.Qual_identiferContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Qual_identiferContext	context	The parse tree.

Returns

Type	Description
Result

VisitQuotedSymbol(SMTLIBv2Parser.QuotedSymbolContext)

Visit a parse tree produced by quotedSymbol().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitQuotedSymbol(SMTLIBv2Parser.QuotedSymbolContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.QuotedSymbolContext	context	The parse tree.

Returns

Type	Description
Result

VisitReason_unknown(SMTLIBv2Parser.Reason_unknownContext)

Visit a parse tree produced by reason_unknown().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitReason_unknown(SMTLIBv2Parser.Reason_unknownContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Reason_unknownContext	context	The parse tree.

Returns

Type	Description
Result

VisitS_expr(SMTLIBv2Parser.S_exprContext)

Visit a parse tree produced by s_expr().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitS_expr(SMTLIBv2Parser.S_exprContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.S_exprContext	context	The parse tree.

Returns

Type	Description
Result

VisitScript(SMTLIBv2Parser.ScriptContext)

Visit a parse tree produced by script().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitScript(SMTLIBv2Parser.ScriptContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.ScriptContext	context	The parse tree.

Returns

Type	Description
Result

VisitSelector_dec(SMTLIBv2Parser.Selector_decContext)

Visit a parse tree produced by selector_dec().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitSelector_dec(SMTLIBv2Parser.Selector_decContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Selector_decContext	context	The parse tree.

Returns

Type	Description
Result

VisitSimpleSymbol(SMTLIBv2Parser.SimpleSymbolContext)

Visit a parse tree produced by simpleSymbol().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitSimpleSymbol(SMTLIBv2Parser.SimpleSymbolContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.SimpleSymbolContext	context	The parse tree.

Returns

Type	Description
Result

VisitSort(SMTLIBv2Parser.SortContext)

Visit a parse tree produced by sort().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitSort(SMTLIBv2Parser.SortContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.SortContext	context	The parse tree.

Returns

Type	Description
Result

VisitSort_dec(SMTLIBv2Parser.Sort_decContext)

Visit a parse tree produced by sort_dec().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitSort_dec(SMTLIBv2Parser.Sort_decContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Sort_decContext	context	The parse tree.

Returns

Type	Description
Result

VisitSort_symbol_decl(SMTLIBv2Parser.Sort_symbol_declContext)

Visit a parse tree produced by sort_symbol_decl().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitSort_symbol_decl(SMTLIBv2Parser.Sort_symbol_declContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Sort_symbol_declContext	context	The parse tree.

Returns

Type	Description
Result

VisitSorted_var(SMTLIBv2Parser.Sorted_varContext)

Visit a parse tree produced by sorted_var().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitSorted_var(SMTLIBv2Parser.Sorted_varContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Sorted_varContext	context	The parse tree.

Returns

Type	Description
Result

VisitSpec_constant(SMTLIBv2Parser.Spec_constantContext)

Visit a parse tree produced by spec_constant().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitSpec_constant(SMTLIBv2Parser.Spec_constantContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Spec_constantContext	context	The parse tree.

Returns

Type	Description
Result

VisitSpecific_success_response(SMTLIBv2Parser.Specific_success_responseContext)

Visit a parse tree produced by specific_success_response().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitSpecific_success_response(SMTLIBv2Parser.Specific_success_responseContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Specific_success_responseContext	context	The parse tree.

Returns

Type	Description
Result

VisitStart(SMTLIBv2Parser.StartContext)

Visit a parse tree produced by start().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitStart(SMTLIBv2Parser.StartContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.StartContext	context	The parse tree.

Returns

Type	Description
Result

VisitString(SMTLIBv2Parser.StringContext)

Visit a parse tree produced by .

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitString(SMTLIBv2Parser.StringContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.StringContext	context	The parse tree.

Returns

Type	Description
Result

VisitSymbol(SMTLIBv2Parser.SymbolContext)

Visit a parse tree produced by symbol().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitSymbol(SMTLIBv2Parser.SymbolContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.SymbolContext	context	The parse tree.

Returns

Type	Description
Result

VisitT_valuation_pair(SMTLIBv2Parser.T_valuation_pairContext)

Visit a parse tree produced by t_valuation_pair().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitT_valuation_pair(SMTLIBv2Parser.T_valuation_pairContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.T_valuation_pairContext	context	The parse tree.

Returns

Type	Description
Result

VisitTerm(SMTLIBv2Parser.TermContext)

Visit a parse tree produced by term().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitTerm(SMTLIBv2Parser.TermContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.TermContext	context	The parse tree.

Returns

Type	Description
Result

VisitTheory_attribute(SMTLIBv2Parser.Theory_attributeContext)

Visit a parse tree produced by theory_attribute().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitTheory_attribute(SMTLIBv2Parser.Theory_attributeContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Theory_attributeContext	context	The parse tree.

Returns

Type	Description
Result

VisitTheory_decl(SMTLIBv2Parser.Theory_declContext)

Visit a parse tree produced by theory_decl().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitTheory_decl(SMTLIBv2Parser.Theory_declContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Theory_declContext	context	The parse tree.

Returns

Type	Description
Result

VisitValuation_pair(SMTLIBv2Parser.Valuation_pairContext)

Visit a parse tree produced by valuation_pair().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitValuation_pair(SMTLIBv2Parser.Valuation_pairContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Valuation_pairContext	context	The parse tree.

Returns

Type	Description
Result

VisitVar_binding(SMTLIBv2Parser.Var_bindingContext)

Visit a parse tree produced by var_binding().

The default implementation returns the result of calling on context.

Declaration

public virtual Result VisitVar_binding(SMTLIBv2Parser.Var_bindingContext context)

Parameters

Type	Name	Description
SMTLIBv2Parser.Var_bindingContext	context	The parse tree.

Returns

Type	Description
Result

Implements

ISMTLIBv2Visitor<Result>

IParseTreeVisitor<>