Interface ISMTLIBv2Visitor<Result>
This interface defines a complete generic visitor for a parse tree produced by SMTLIBv2Parser.
Namespace: GCore.Antlr.Grammers.Smtlibv2
Assembly: Smtlibv2.dll
Syntax
public interface ISMTLIBv2Visitor<Result> : IParseTreeVisitor<Result>Type Parameters
| Name | Description |
|---|---|
| Result | The return type of the visit operation. |
Methods
| Improve this Doc View SourceVisitAttribute(SMTLIBv2Parser.AttributeContext)
Visit a parse tree produced by attribute().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
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().
Declaration
Result VisitVar_binding(SMTLIBv2Parser.Var_bindingContext context)Parameters
| Type | Name | Description |
|---|---|---|
| SMTLIBv2Parser.Var_bindingContext | context | The parse tree. |
Returns
| Type | Description |
|---|---|
| Result |