/** \file

 *  This C source file was generated by $ANTLR version 3.4

 *

 *     -  From the grammar source file : /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-14/src/parser/cvc/Cvc.g

 *     -                            On : 2021-09-14 01:05:14

 *     -                for the parser : CvcParserParser

 *

 * Editing it, at least manually, is not wise.

 *

 * C language generator and runtime by Jim Idle, jimi|hereisanat|idle|dotgoeshere|ws.

 *

 *

*/

// [The "BSD license"]

// Copyright (c) 2005-2009 Jim Idle, Temporal Wave LLC

// http://www.temporal-wave.com

// http://www.linkedin.com/in/jimidle

//

// All rights reserved.

//

// Redistribution and use in source and binary forms, with or without

// modification, are permitted provided that the following conditions

// are met:

// 1. Redistributions of source code must retain the above copyright

//    notice, this list of conditions and the following disclaimer.

// 2. Redistributions in binary form must reproduce the above copyright

//    notice, this list of conditions and the following disclaimer in the

//    documentation and/or other materials provided with the distribution.

// 3. The name of the author may not be used to endorse or promote products

//    derived from this software without specific prior written permission.

//

// THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR

// IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES

// OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED.

// IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT,

// INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT

// NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,

// DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY

// THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT

// (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF

// THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

/* =============================================================================

 * This is what the grammar programmer asked us to put at the top of every file.

 */

/* ****************************************************************************

 * This file is part of the cvc5 project.

 *

 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS

 * in the top-level source directory and their institutional affiliations.

 * All rights reserved.  See the file COPYING in the top-level source

 * directory for licensing information.

 * ****************************************************************************

 */

/* End of Header action.

 * =============================================================================

 */

/* -----------------------------------------

 * Include the ANTLR3 generated header file.

 */

#include    "CvcParser.h"

#include <sstream>

#include <string>

#include <vector>

#include "base/output.h"

#include "parser/antlr_input.h"

#include "parser/parser.h"

#define REPEAT_COMMAND(k, CommandCtor)                      \

  ({                                                        \

    unsigned __k = (k);                                     \

    (__k <= 1)                                              \

      ? (Command*) new CommandCtor                          \

      : ({                                                  \

          CommandSequence* __seq = new CommandSequence();   \

          while(__k-- > 0) {                                \

            __seq->addCommand(new CommandCtor);             \

          }                                                 \

          (Command*) __seq;                                 \

        });                                                 \

  })

using namespace cvc5;

using namespace cvc5::parser;

/* These need to be macros so they can refer to the PARSER macro, which will be defined

 * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */

#undef PARSER_STATE

#define PARSER_STATE ((Parser*)PARSER->super)

#undef SOLVER

#define SOLVER PARSER_STATE->getSolver()

#undef MK_TERM

#define MK_TERM SOLVER->mkTerm

#define UNSUPPORTED PARSER_STATE->unimplementedFeature

#define ENSURE_BV_SIZE(k, f)                                   \

{                                                              \

  unsigned size = f.getSort().getBVSize();        \

  if(k > size) {                                               \

    f = SOLVER->mkTerm(SOLVER->mkOp(api::BITVECTOR_ZERO_EXTEND,k - size), f); \

  } else if (k < size) {                                       \

    f = SOLVER->mkTerm(SOLVER->mkOp(api::BITVECTOR_EXTRACT, k - 1, 0), f); \

  }                                                            \

}

/* ----------------------------------------- */

/* MACROS that hide the C interface implementations from the

 * generated code, which makes it a little more understandable to the human eye.

 * I am very much against using C pre-processor macros for function calls and bits

 * of code as you cannot see what is happening when single stepping in debuggers

 * and so on. The exception (in my book at least) is for generated code, where you are

 * not maintaining it, but may wish to read and understand it. If you single step it, you know that input()

 * hides some indirect calls, but is always referring to the input stream. This is

 * probably more readable than ctx->input->istream->input(snarfle0->blarg) and allows me to rejig

 * the runtime interfaces without changing the generated code too often, without

 * confusing the reader of the generated output, who may not wish to know the gory

 * details of the interface inheritance.

 */

#define		CTX	ctx

/* Aids in accessing scopes for grammar programmers

 */

#undef	SCOPE_TYPE

#undef	SCOPE_STACK

#undef	SCOPE_TOP

#define	SCOPE_TYPE(scope)   pCvcParser_##scope##_SCOPE

#define SCOPE_STACK(scope)  pCvcParser_##scope##Stack

#define	SCOPE_TOP(scope)    ctx->pCvcParser_##scope##Top

#define	SCOPE_SIZE(scope)		ctx->pCvcParser_##scope##Stack_limit

#define SCOPE_INSTANCE(scope, i)	(ctx->SCOPE_STACK(scope)->get(ctx->SCOPE_STACK(scope),i))

/* Macros for accessing things in the parser

 */

#undef	    PARSER

#undef	    RECOGNIZER

#undef	    HAVEPARSEDRULE

#undef		MEMOIZE

#undef	    INPUT

#undef	    STRSTREAM

#undef	    HASEXCEPTION

#undef	    EXCEPTION

#undef	    MATCHT

#undef	    MATCHANYT

#undef	    FOLLOWSTACK

#undef	    FOLLOWPUSH

#undef	    FOLLOWPOP

#undef	    PRECOVER

#undef	    PREPORTERROR

#undef	    LA

#undef	    LT

#undef	    CONSTRUCTEX

#undef	    CONSUME

#undef	    MARK

#undef	    REWIND

#undef	    REWINDLAST

#undef	    PERRORRECOVERY

#undef	    HASFAILED

#undef	    FAILEDFLAG

#undef	    RECOVERFROMMISMATCHEDSET

#undef	    RECOVERFROMMISMATCHEDELEMENT

#undef		INDEX

#undef      ADAPTOR

#undef		SEEK

#undef	    RULEMEMO

#undef		DBG

#define	    PARSER				ctx->pParser

#define	    RECOGNIZER				PARSER->rec

#define	    PSRSTATE				RECOGNIZER->state

#define	    HAVEPARSEDRULE(r)			RECOGNIZER->alreadyParsedRule(RECOGNIZER, r)

#define	    MEMOIZE(ri,si)			RECOGNIZER->memoize(RECOGNIZER, ri, si)

#define	    INPUT				PARSER->tstream

#define	    STRSTREAM				INPUT

#define	    ISTREAM				INPUT->istream

#define	    INDEX()				ISTREAM->index(INPUT->istream)

#define	    HASEXCEPTION()			(PSRSTATE->error == ANTLR3_TRUE)

#define	    EXCEPTION				PSRSTATE->exception

#define	    MATCHT(t, fs)			RECOGNIZER->match(RECOGNIZER, t, fs)

#define	    MATCHANYT()				RECOGNIZER->matchAny(RECOGNIZER)

#define	    FOLLOWSTACK				PSRSTATE->following

#ifdef  SKIP_FOLLOW_SETS

#define	    FOLLOWPUSH(x)

#define	    FOLLOWPOP()

#else

#define	    FOLLOWPUSH(x)			FOLLOWSTACK->push(FOLLOWSTACK, ((void *)(&(x))), NULL)

#define	    FOLLOWPOP()				FOLLOWSTACK->pop(FOLLOWSTACK)

#endif

#define	    PRECOVER()				RECOGNIZER->recover(RECOGNIZER)

#define	    PREPORTERROR()			RECOGNIZER->reportError(RECOGNIZER)

#define	    LA(n)				INPUT->istream->_LA(ISTREAM, n)

#define	    LT(n)				INPUT->_LT(INPUT, n)

#define	    CONSTRUCTEX()			RECOGNIZER->exConstruct(RECOGNIZER)

#define	    CONSUME()				ISTREAM->consume(ISTREAM)

#define	    MARK()				ISTREAM->mark(ISTREAM)

#define	    REWIND(m)				ISTREAM->rewind(ISTREAM, m)

#define	    REWINDLAST()			ISTREAM->rewindLast(ISTREAM)

#define	    SEEK(n)				ISTREAM->seek(ISTREAM, n)

#define	    PERRORRECOVERY			PSRSTATE->errorRecovery

#define	    FAILEDFLAG				PSRSTATE->failed

#define	    HASFAILED()				(FAILEDFLAG == ANTLR3_TRUE)

#define	    BACKTRACKING			PSRSTATE->backtracking

#define	    RECOVERFROMMISMATCHEDSET(s)		RECOGNIZER->recoverFromMismatchedSet(RECOGNIZER, s)

#define	    RECOVERFROMMISMATCHEDELEMENT(e)	RECOGNIZER->recoverFromMismatchedElement(RECOGNIZER, s)

#define     ADAPTOR                         ctx->adaptor

#define		RULEMEMO						PSRSTATE->ruleMemo

#define		DBG								RECOGNIZER->debugger

#define		TOKTEXT(tok, txt)				tok, (pANTLR3_UINT8)txt

/* The 4 tokens defined below may well clash with your own #defines or token types. If so

 * then for the present you must use different names for your defines as these are hard coded

 * in the code generator. It would be better not to use such names internally, and maybe

 * we can change this in a forthcoming release. I deliberately do not #undef these

 * here as this will at least give you a redefined error somewhere if they clash.

 */

#define	    UP	    ANTLR3_TOKEN_UP

#define	    DOWN    ANTLR3_TOKEN_DOWN

#define	    EOR	    ANTLR3_TOKEN_EOR

#define	    INVALID ANTLR3_TOKEN_INVALID

/* =============================================================================

 * Functions to create and destroy scopes. First come the rule scopes, followed

 * by the global declared scopes.

 */

/* ============================================================================= */

/* =============================================================================

 * Start of recognizer

 */

/** \brief Table of all token names in symbolic order, mainly used for

 *         error reporting.

 */

pANTLR3_UINT8   CvcParserTokenNames[205+4]

     = {

        (pANTLR3_UINT8) "<invalid>",       /* String to print to indicate an invalid token */

        (pANTLR3_UINT8) "<EOR>",

        (pANTLR3_UINT8) "<DOWN>",

        (pANTLR3_UINT8) "<UP>",

        (pANTLR3_UINT8) "ABS_TOK",

        (pANTLR3_UINT8) "ALPHA",

        (pANTLR3_UINT8) "AND_TOK",

        (pANTLR3_UINT8) "ARITH_VAR_ORDER_TOK",

        (pANTLR3_UINT8) "ARRAY_TOK",

        (pANTLR3_UINT8) "ARROW_TOK",

        (pANTLR3_UINT8) "ASSERTIONS_TOK",

        (pANTLR3_UINT8) "ASSERT_TOK",

        (pANTLR3_UINT8) "ASSIGN_TOK",

        (pANTLR3_UINT8) "ASSUMPTIONS_TOK",

        (pANTLR3_UINT8) "BAR",

        (pANTLR3_UINT8) "BINARY_LITERAL",

        (pANTLR3_UINT8) "BITVECTOR_TOK",

        (pANTLR3_UINT8) "BOOLEAN_TOK",

        (pANTLR3_UINT8) "BVAND_TOK",

        (pANTLR3_UINT8) "BVASHR_TOK",

        (pANTLR3_UINT8) "BVCOMP_TOK",

        (pANTLR3_UINT8) "BVGE_TOK",

        (pANTLR3_UINT8) "BVGT_TOK",

        (pANTLR3_UINT8) "BVLE_TOK",

        (pANTLR3_UINT8) "BVLSHR_TOK",

        (pANTLR3_UINT8) "BVLT_TOK",

        (pANTLR3_UINT8) "BVMULT_TOK",

        (pANTLR3_UINT8) "BVNAND_TOK",

        (pANTLR3_UINT8) "BVNEG_TOK",

        (pANTLR3_UINT8) "BVNOR_TOK",

        (pANTLR3_UINT8) "BVPLUS_TOK",

        (pANTLR3_UINT8) "BVREPEAT_TOK",

        (pANTLR3_UINT8) "BVROTL_TOK",

        (pANTLR3_UINT8) "BVROTR_TOK",

        (pANTLR3_UINT8) "BVSDIV_TOK",

        (pANTLR3_UINT8) "BVSGE_TOK",

        (pANTLR3_UINT8) "BVSGT_TOK",

        (pANTLR3_UINT8) "BVSHL_TOK",

        (pANTLR3_UINT8) "BVSLE_TOK",

        (pANTLR3_UINT8) "BVSLT_TOK",

        (pANTLR3_UINT8) "BVSMOD_TOK",

        (pANTLR3_UINT8) "BVSREM_TOK",

        (pANTLR3_UINT8) "BVSUB_TOK",

        (pANTLR3_UINT8) "BVUDIV_TOK",

        (pANTLR3_UINT8) "BVUMINUS_TOK",

        (pANTLR3_UINT8) "BVUREM_TOK",

        (pANTLR3_UINT8) "BVXNOR_TOK",

        (pANTLR3_UINT8) "BVXOR_TOK",

        (pANTLR3_UINT8) "BVZEROEXTEND_TOK",

        (pANTLR3_UINT8) "CALL_TOK",

        (pANTLR3_UINT8) "CHECKSAT_TOK",

        (pANTLR3_UINT8) "CHECK_TYPE_TOK",

        (pANTLR3_UINT8) "COLON",

        (pANTLR3_UINT8) "COMMA",

        (pANTLR3_UINT8) "COMMENT",

        (pANTLR3_UINT8) "CONCAT_TOK",

        (pANTLR3_UINT8) "CONTEXT_TOK",

        (pANTLR3_UINT8) "CONTINUE_TOK",

        (pANTLR3_UINT8) "COUNTEREXAMPLE_TOK",

        (pANTLR3_UINT8) "COUNTERMODEL_TOK",

        (pANTLR3_UINT8) "DATATYPE_TOK",

        (pANTLR3_UINT8) "DBG_TOK",

        (pANTLR3_UINT8) "DECIMAL_LITERAL",

        (pANTLR3_UINT8) "DIGIT",

        (pANTLR3_UINT8) "DISEQUAL_TOK",

        (pANTLR3_UINT8) "DISTINCT_TOK",

        (pANTLR3_UINT8) "DIVISIBLE_TOK",

        (pANTLR3_UINT8) "DIV_TOK",

        (pANTLR3_UINT8) "DOT",

        (pANTLR3_UINT8) "DOTDOT",

        (pANTLR3_UINT8) "DUMP_ASSUMPTIONS_TOK",

        (pANTLR3_UINT8) "DUMP_CLOSURE_PROOF_TOK",

        (pANTLR3_UINT8) "DUMP_CLOSURE_TOK",

        (pANTLR3_UINT8) "DUMP_PROOF_TOK",

        (pANTLR3_UINT8) "DUMP_SIG_TOK",

        (pANTLR3_UINT8) "DUMP_TCC_ASSUMPTIONS_TOK",

        (pANTLR3_UINT8) "DUMP_TCC_PROOF_TOK",

        (pANTLR3_UINT8) "DUMP_TCC_TOK",

        (pANTLR3_UINT8) "DUMP_UNSAT_CORE_TOK",

        (pANTLR3_UINT8) "ECHO_TOK",

        (pANTLR3_UINT8) "ELSEIF_TOK",

        (pANTLR3_UINT8) "ELSE_TOK",

        (pANTLR3_UINT8) "ENDIF_TOK",

        (pANTLR3_UINT8) "END_TOK",

        (pANTLR3_UINT8) "EQUAL_TOK",

        (pANTLR3_UINT8) "ESCAPE",

        (pANTLR3_UINT8) "EXISTS_TOK",

        (pANTLR3_UINT8) "EXIT_TOK",

        (pANTLR3_UINT8) "EXP_TOK",

        (pANTLR3_UINT8) "FALSE_TOK",

        (pANTLR3_UINT8) "FLOOR_TOK",

        (pANTLR3_UINT8) "FMF_CARD_TOK",

        (pANTLR3_UINT8) "FORALL_TOK",

        (pANTLR3_UINT8) "FORGET_TOK",

        (pANTLR3_UINT8) "GEQ_TOK",

        (pANTLR3_UINT8) "GET_CHILD_TOK",

        (pANTLR3_UINT8) "GET_OP_TOK",

        (pANTLR3_UINT8) "GET_TYPE_TOK",

        (pANTLR3_UINT8) "GET_VALUE_TOK",

        (pANTLR3_UINT8) "GT_TOK",

        (pANTLR3_UINT8) "HASHPAREN",

        (pANTLR3_UINT8) "HASHSQ",

        (pANTLR3_UINT8) "HELP_TOK",

        (pANTLR3_UINT8) "HEX_DIGIT",

        (pANTLR3_UINT8) "HEX_LITERAL",

        (pANTLR3_UINT8) "IDENTIFIER",

        (pANTLR3_UINT8) "IDEN_TOK",

        (pANTLR3_UINT8) "IFF_TOK",

        (pANTLR3_UINT8) "IF_TOK",

        (pANTLR3_UINT8) "IMPLIES_TOK",

        (pANTLR3_UINT8) "INCLUDE_TOK",

        (pANTLR3_UINT8) "INTDIV_TOK",

        (pANTLR3_UINT8) "INTEGER_LITERAL",

        (pANTLR3_UINT8) "INT_TOK",

        (pANTLR3_UINT8) "IN_TOK",

        (pANTLR3_UINT8) "IS_INTEGER_TOK",

        (pANTLR3_UINT8) "JOIN_IMAGE_TOK",

        (pANTLR3_UINT8) "JOIN_TOK",

        (pANTLR3_UINT8) "LAMBDA_TOK",

        (pANTLR3_UINT8) "LBRACE",

        (pANTLR3_UINT8) "LBRACKET",

        (pANTLR3_UINT8) "LEFTSHIFT_TOK",

        (pANTLR3_UINT8) "LEQ_TOK",

        (pANTLR3_UINT8) "LET_TOK",

        (pANTLR3_UINT8) "LPAREN",

        (pANTLR3_UINT8) "LT_TOK",

        (pANTLR3_UINT8) "MEMBER_TOK",

        (pANTLR3_UINT8) "MINUS_TOK",

        (pANTLR3_UINT8) "MOD_TOK",

        (pANTLR3_UINT8) "NOT_TOK",

        (pANTLR3_UINT8) "NUMBER_OR_RANGEOP",

        (pANTLR3_UINT8) "OF_TOK",

        (pANTLR3_UINT8) "OPTION_TOK",

        (pANTLR3_UINT8) "OR_TOK",

        (pANTLR3_UINT8) "PARENHASH",

        (pANTLR3_UINT8) "PATTERN_TOK",

        (pANTLR3_UINT8) "PLUS_TOK",

        (pANTLR3_UINT8) "POPTO_SCOPE_TOK",

        (pANTLR3_UINT8) "POPTO_TOK",

        (pANTLR3_UINT8) "POP_SCOPE_TOK",

        (pANTLR3_UINT8) "POP_TOK",

        (pANTLR3_UINT8) "PRINT_TOK",

        (pANTLR3_UINT8) "PRINT_TYPE_TOK",

        (pANTLR3_UINT8) "PRODUCT_TOK",

        (pANTLR3_UINT8) "PUSH_SCOPE_TOK",

        (pANTLR3_UINT8) "PUSH_TOK",

        (pANTLR3_UINT8) "QUERY_TOK",

        (pANTLR3_UINT8) "RBRACE",

        (pANTLR3_UINT8) "RBRACKET",

        (pANTLR3_UINT8) "REAL_TOK",

        (pANTLR3_UINT8) "RECURSIVE_FUNCTION_TOK",

        (pANTLR3_UINT8) "REGEXP_COMPLEMENT_TOK",

        (pANTLR3_UINT8) "REGEXP_CONCAT_TOK",

        (pANTLR3_UINT8) "REGEXP_EMPTY_TOK",

        (pANTLR3_UINT8) "REGEXP_INTER_TOK",

        (pANTLR3_UINT8) "REGEXP_LOOP_TOK",

        (pANTLR3_UINT8) "REGEXP_OPT_TOK",

        (pANTLR3_UINT8) "REGEXP_PLUS_TOK",

        (pANTLR3_UINT8) "REGEXP_RANGE_TOK",

        (pANTLR3_UINT8) "REGEXP_SIGMA_TOK",

        (pANTLR3_UINT8) "REGEXP_STAR_TOK",

        (pANTLR3_UINT8) "REGEXP_UNION_TOK",

        (pANTLR3_UINT8) "RESET_TOK",

        (pANTLR3_UINT8) "RESTART_TOK",

        (pANTLR3_UINT8) "RIGHTSHIFT_TOK",

        (pANTLR3_UINT8) "RPAREN",

        (pANTLR3_UINT8) "SEMICOLON",

        (pANTLR3_UINT8) "SEQ_UNIT_TOK",

        (pANTLR3_UINT8) "SETS_CARD_TOK",

        (pANTLR3_UINT8) "SETS_CHOOSE_TOK",

        (pANTLR3_UINT8) "SET_TOK",

        (pANTLR3_UINT8) "SQHASH",

        (pANTLR3_UINT8) "STAR_TOK",

        (pANTLR3_UINT8) "STRING_CHARAT_TOK",

        (pANTLR3_UINT8) "STRING_CONCAT_TOK",

        (pANTLR3_UINT8) "STRING_CONTAINS_TOK",

        (pANTLR3_UINT8) "STRING_INDEXOF_TOK",

        (pANTLR3_UINT8) "STRING_ITOS_TOK",

        (pANTLR3_UINT8) "STRING_LENGTH_TOK",

        (pANTLR3_UINT8) "STRING_LITERAL",

        (pANTLR3_UINT8) "STRING_PREFIXOF_TOK",

        (pANTLR3_UINT8) "STRING_REPLACE_ALL_TOK",

        (pANTLR3_UINT8) "STRING_REPLACE_TOK",

        (pANTLR3_UINT8) "STRING_REV_TOK",

        (pANTLR3_UINT8) "STRING_STOI_TOK",

        (pANTLR3_UINT8) "STRING_SUBSTR_TOK",

        (pANTLR3_UINT8) "STRING_SUFFIXOF_TOK",

        (pANTLR3_UINT8) "STRING_TOK",

        (pANTLR3_UINT8) "STRING_TOLOWER_TOK",

        (pANTLR3_UINT8) "STRING_TOUPPER_TOK",

        (pANTLR3_UINT8) "STRING_TO_REGEXP_TOK",

        (pANTLR3_UINT8) "SUBSTITUTE_TOK",

        (pANTLR3_UINT8) "SUBTYPE_TOK",

        (pANTLR3_UINT8) "SX_TOK",

        (pANTLR3_UINT8) "THEN_TOK",

        (pANTLR3_UINT8) "TRACE_TOK",

        (pANTLR3_UINT8) "TRANSCLOSURE_TOK",

        (pANTLR3_UINT8) "TRANSFORM_TOK",

        (pANTLR3_UINT8) "TRANSPOSE_TOK",

        (pANTLR3_UINT8) "TRUE_TOK",

        (pANTLR3_UINT8) "TUPLE_TOK",

        (pANTLR3_UINT8) "TYPE_TOK",

        (pANTLR3_UINT8) "UNDERSCORE",

        (pANTLR3_UINT8) "UNIVSET_TOK",

        (pANTLR3_UINT8) "UNTRACE_TOK",

        (pANTLR3_UINT8) "WHERE_TOK",

        (pANTLR3_UINT8) "WHITESPACE",

        (pANTLR3_UINT8) "WITH_TOK",

        (pANTLR3_UINT8) "XOR_TOK"

       };

// Forward declare the locally static matching functions we have generated.

//

static

 cvc5::api::Term

	parseExpr    (pCvcParser ctx);

static

 cvc5::Command*

	parseCommand    (pCvcParser ctx);

static

 void

	command    (pCvcParser ctx, std::unique_ptr<cvc5::Command>* cmd);

static

 void

	typeOrVarLetDecl    (pCvcParser ctx, cvc5::parser::DeclarationCheck check);

static

 void

	mainCommand    (pCvcParser ctx, std::unique_ptr<cvc5::Command>* cmd);

static

 void

	simpleSymbolicExpr    (pCvcParser ctx, std::string& s);

static

 void

	symbolicExpr    (pCvcParser ctx, cvc5::api::Term& sexpr);

static

 void

	toplevelDeclaration    (pCvcParser ctx, std::unique_ptr<cvc5::Command>* cmd);

static

 void

	boundVarDecl    (pCvcParser ctx, std::vector<std::string>& ids, cvc5::api::Sort& t);

static

 void

	boundVarDecls    (pCvcParser ctx);

static

 void

	boundVarDeclsReturn    (pCvcParser ctx, std::vector<cvc5::api::Term>& terms, std::vector<cvc5::api::Sort>& types);

static

 void

	boundVarDeclReturn    (pCvcParser ctx, std::vector<cvc5::api::Term>& terms, std::vector<cvc5::api::Sort>& types);

static

 void

	declareTypes    (pCvcParser ctx, std::unique_ptr<cvc5::Command>* cmd, const std::vector<std::string>& idList);

static

 void

	declareVariables    (pCvcParser ctx, std::unique_ptr<cvc5::Command>* cmd, cvc5::api::Sort& t, const std::vector<std::string>& idList, bool topLevel);

static

 void

	identifierList    (pCvcParser ctx, std::vector<std::string>& idList, cvc5::parser::DeclarationCheck check, cvc5::parser::SymbolType type);

static

 void

	identifier    (pCvcParser ctx, std::string& id, cvc5::parser::DeclarationCheck check, cvc5::parser::SymbolType type);

static

 void

	type    (pCvcParser ctx, cvc5::api::Sort& t, cvc5::parser::DeclarationCheck check);

static

 void

	restrictedType    (pCvcParser ctx, cvc5::api::Sort& t, cvc5::parser::DeclarationCheck check);

static

 void

	restrictedTypePossiblyFunctionLHS    (pCvcParser ctx, cvc5::api::Sort& t, cvc5::parser::DeclarationCheck check, bool& lhs);

static

 void

	parameterization    (pCvcParser ctx, cvc5::parser::DeclarationCheck check, std::vector<cvc5::api::Sort>& params);

static

 void

	typeLetDecl    (pCvcParser ctx, cvc5::parser::DeclarationCheck check);

static

 void

	formula    (pCvcParser ctx, cvc5::api::Term& f);

static

 size_t

	morecomparisons    (pCvcParser ctx, std::vector<cvc5::api::Term>& expressions, std::vector<unsigned>& operators);

static

 size_t

	nots    (pCvcParser ctx);

static

 void

	prefixFormula    (pCvcParser ctx, cvc5::api::Term& f);

static

 void

	instantiationPatterns    (pCvcParser ctx, cvc5::api::Term& expr);

static

 void

	letDecl    (pCvcParser ctx);

static

 void

	booleanBinop    (pCvcParser ctx, unsigned& op);

static

 void

	comparison    (pCvcParser ctx, cvc5::api::Term& f);

static

 void

	comparisonBinop    (pCvcParser ctx, unsigned& op);

static

 void

	arithmeticBinop    (pCvcParser ctx, unsigned& op);

static

 void

	term    (pCvcParser ctx, cvc5::api::Term& f);

static

 void

	arrayStore    (pCvcParser ctx, cvc5::api::Term& f);

static

 void

	tupleStore    (pCvcParser ctx, cvc5::api::Term& f);

static

 void

	recordStore    (pCvcParser ctx, cvc5::api::Term& f);

static

 void

	uminusTerm    (pCvcParser ctx, cvc5::api::Term& f);

static

 void

	bvBinaryOpTerm    (pCvcParser ctx, cvc5::api::Term& f);

static

 void

	bvBinop    (pCvcParser ctx, unsigned& op);

static

 void

	bvNegTerm    (pCvcParser ctx, cvc5::api::Term& f);

static

 void

	relationBinop    (pCvcParser ctx, unsigned& op);

static

 void

	relationBinopTerm    (pCvcParser ctx, cvc5::api::Term& f);

static

 void

	postfixTerm    (pCvcParser ctx, cvc5::api::Term& f);

static

 void

	relationTerm    (pCvcParser ctx, cvc5::api::Term& f);

static

 void

	bvTerm    (pCvcParser ctx, cvc5::api::Term& f);

static

 void

	stringTerm    (pCvcParser ctx, cvc5::api::Term& f);

static

 void

	setsTerm    (pCvcParser ctx, cvc5::api::Term& f);

static

 void

	simpleTerm    (pCvcParser ctx, cvc5::api::Term& f);

static

 void

	typeAscription    (pCvcParser ctx, const cvc5::api::Term& f, cvc5::api::Sort& t);

static

 void

	recordEntry    (pCvcParser ctx, std::string& name, cvc5::api::Term& ex);

static

 void

	iteTerm    (pCvcParser ctx, cvc5::api::Term& f);

static

 void

	iteElseTerm    (pCvcParser ctx, cvc5::api::Term& f);

static

 void

	datatypeDef    (pCvcParser ctx, std::vector<cvc5::api::DatatypeDecl>& datatypes);

static

 void

	constructorDef    (pCvcParser ctx, cvc5::api::DatatypeDecl& type);

static

 void

	selector    (pCvcParser ctx, std::unique_ptr<cvc5::api::DatatypeConstructorDecl>* ctor);

static

 unsigned

	numeral    (pCvcParser ctx);

static

 void

	str    (pCvcParser ctx, std::string& s);

static

 ANTLR3_BOOLEAN

	synpred1_Cvc    (pCvcParser ctx);

static void	CvcParserFree(pCvcParser ctx);

static void     CvcParserReset (pCvcParser ctx);

/* For use in tree output where we are accumulating rule labels via label += ruleRef

 * we need a function that knows how to free a return scope when the list is destroyed.

 * We cannot just use ANTLR3_FREE because in debug tracking mode, this is a macro.

 */

{

/** \brief Name of the grammar file that generated this code

 */

static const char fileName[] = "/barrett/scratch/cvc4-nightly/src/cvc5-2021-09-14/src/parser/cvc/Cvc.g";

/** \brief Return the name of the grammar file that generated this code.

 */

{

}

/** \brief Create a new CvcParser parser and return a context for it.

 *

 * \param[in] instream Pointer to an input stream interface.

 *

 * \return Pointer to new parser context upon success.

 */

ANTLR3_API pCvcParser

{

	// See if we can create a new parser with the standard constructor

	//

}

/** \brief Create a new CvcParser parser and return a context for it.

 *

 * \param[in] instream Pointer to an input stream interface.

 *

 * \return Pointer to new parser context upon success.

 */

ANTLR3_API pCvcParser

{

    pCvcParser ctx;	    /* Context structure we will build and return   */

    {

		// Failed to allocate memory for parser context

		//

    }

    /* -------------------------------------------------------------------

     * Memory for basic structure is allocated, now to fill in

     * the base ANTLR3 structures. We initialize the function pointers

     * for the standard ANTLR3 parser function set, but upon return

     * from here, the programmer may set the pointers to provide custom

     * implementations of each function.

     *

     * We don't use the macros defined in CvcParser.h here, in order that you can get a sense

     * of what goes where.

     */

    /* Create a base parser/recognizer, using the supplied token stream

     */

    /* Install the implementation of our CvcParser interface

     */

    /* Install the scope pushing methods.

     */

    /* Install the token table

     */

    /* Return the newly built parser to the caller

     */

}

static void

{

/** Free the parser resources

 */

 static void

 {

    /* Free any scope memory

     */

	// Free this parser

	//

    /* Everything is released, so we can return

     */

 }

/** Return token names used by this

parser

 *

 * The returned pointer is used as an index into the token names table (using the token

 * number as the index).

 *

 * \return Pointer to first char * in the table.

 */

{

}

    // Idea and code guidance from Sam Harwell,

    // http://www.antlr.org/wiki/display/ANTLR3/Operator+precedence+parser

      // return true here for any operators that are right-to-left associative

      }

    }/* isRightToLeft() */

      //case DOT:

      case BVSLE_TOK:

      case BVSGT_TOK:

      case BVLE_TOK:

      case BVGT_TOK:

      case BVZEROEXTEND_TOK:

      case BVREPEAT_TOK:

      case BVROTL_TOK:

      case BVSDIV_TOK:

      case BVUREM_TOK:

      case BVSREM_TOK:

      case BVSMOD_TOK:

      case BVSHL_TOK:

      case BVASHR_TOK:

      case BVPLUS_TOK:

    //case UMINUS_TOK: return 20;

      case INTDIV_TOK:

      case DIV_TOK:

      case TUPLE_TOK:

      case MINUS_TOK:

      case JOIN_TOK:

      case TRANSPOSE_TOK:

      case PRODUCT_TOK:

      case IDEN_TOK:

      case JOIN_IMAGE_TOK:

      case TRANSCLOSURE_TOK:

      case LT_TOK:

      case GEQ_TOK:

      case GT_TOK:

      case MEMBER_TOK:

      case SETS_CARD_TOK:

      }

    }/* getOperatorPrecedence() */

        // booleanBinop

        // comparisonBinop

        // arithmeticBinop

        // bvBinop

      }

    }/* getOperatorKind() */

                       unsigned startIndex, unsigned stopIndex) {

      /*Debug("prec") << "initial pivot at " << pivot

                    << "(" << CvcParserTokenNames[operators[pivot]] << ") "

                    << "level " << pivotRank << std::endl;*/

          /*Debug("prec") << "new pivot at " << i

                        << "(" << CvcParserTokenNames[operators[i]] << ") "

                        << "level " << current << " rtl == " << rtl << std::endl;*/

        }

      }

    }/* findPivot() */

                              const std::vector<cvc5::api::Term>& expressions,

                              const std::vector<unsigned>& operators,

                              unsigned startIndex, unsigned stopIndex) {

      }

      //Debug("prec") << "pivot[" << startIndex << "," << stopIndex - 1 << "] at " << pivot << std::endl;

      bool negate;

      cvc5::api::Term lhs = createPrecedenceTree(

      cvc5::api::Term rhs = createPrecedenceTree(

      {

        {

        }

      }

      {

        {

        }

      }

    }/* createPrecedenceTree() recursive variant */

                              const std::vector<cvc5::api::Term>& expressions,

                              const std::vector<unsigned>& operators) {

          }

        }

      }

      api::Term e = createPrecedenceTree(

      }

    }/* createPrecedenceTree() base variant */

    /** Add n NOTs to the front of e and return the result. */

      }

    }/* addNots() */

/* Declare the bitsets

 */

/** Bitset defining follow set for error recovery in rule state: FOLLOW_formula_in_parseExpr1906  */

static	ANTLR3_BITWORD FOLLOW_formula_in_parseExpr1906_bits[]	= { ANTLR3_UINT64_LIT(0x0000000000000002) };

static  ANTLR3_BITSET_LIST FOLLOW_formula_in_parseExpr1906	= { FOLLOW_formula_in_parseExpr1906_bits, 1	};

/** Bitset defining follow set for error recovery in rule state: FOLLOW_EOF_in_parseExpr1913  */

static	ANTLR3_BITWORD FOLLOW_EOF_in_parseExpr1913_bits[]	= { ANTLR3_UINT64_LIT(0x0000000000000002) };

static  ANTLR3_BITSET_LIST FOLLOW_EOF_in_parseExpr1913	= { FOLLOW_EOF_in_parseExpr1913_bits, 1	};

/** Bitset defining follow set for error recovery in rule state: FOLLOW_command_in_parseCommand1944  */

static	ANTLR3_BITWORD FOLLOW_command_in_parseCommand1944_bits[]	= { ANTLR3_UINT64_LIT(0x0000000000000002) };

static  ANTLR3_BITSET_LIST FOLLOW_command_in_parseCommand1944	= { FOLLOW_command_in_parseCommand1944_bits, 1	};

/** Bitset defining follow set for error recovery in rule state: FOLLOW_LPAREN_in_parseCommand1951  */

static	ANTLR3_BITWORD FOLLOW_LPAREN_in_parseCommand1951_bits[]	= { ANTLR3_UINT64_LIT(0x0000000000000000), ANTLR3_UINT64_LIT(0x0000020000000000) };

static  ANTLR3_BITSET_LIST FOLLOW_LPAREN_in_parseCommand1951	= { FOLLOW_LPAREN_in_parseCommand1951_bits, 2	};

/** Bitset defining follow set for error recovery in rule state: FOLLOW_IDENTIFIER_in_parseCommand1953  */

static	ANTLR3_BITWORD FOLLOW_IDENTIFIER_in_parseCommand1953_bits[]	= { ANTLR3_UINT64_LIT(0x0000000000000002) };

static  ANTLR3_BITSET_LIST FOLLOW_IDENTIFIER_in_parseCommand1953	= { FOLLOW_IDENTIFIER_in_parseCommand1953_bits, 1	};

/** Bitset defining follow set for error recovery in rule state: FOLLOW_EOF_in_parseCommand1965  */

static	ANTLR3_BITWORD FOLLOW_EOF_in_parseCommand1965_bits[]	= { ANTLR3_UINT64_LIT(0x0000000000000002) };

static  ANTLR3_BITSET_LIST FOLLOW_EOF_in_parseCommand1965	= { FOLLOW_EOF_in_parseCommand1965_bits, 1	};

/** Bitset defining follow set for error recovery in rule state: FOLLOW_mainCommand_in_command1984  */

static	ANTLR3_BITWORD FOLLOW_mainCommand_in_command1984_bits[]	= { ANTLR3_UINT64_LIT(0x0000000000000000), ANTLR3_UINT64_LIT(0x0000000000000000), ANTLR3_UINT64_LIT(0x0000004000000000) };

static  ANTLR3_BITSET_LIST FOLLOW_mainCommand_in_command1984	= { FOLLOW_mainCommand_in_command1984_bits, 3	};

/** Bitset defining follow set for error recovery in rule state: FOLLOW_SEMICOLON_in_command1987  */

static	ANTLR3_BITWORD FOLLOW_SEMICOLON_in_command1987_bits[]	= { ANTLR3_UINT64_LIT(0x0000000000000002) };

static  ANTLR3_BITSET_LIST FOLLOW_SEMICOLON_in_command1987	= { FOLLOW_SEMICOLON_in_command1987_bits, 1	};

/** Bitset defining follow set for error recovery in rule state: FOLLOW_SEMICOLON_in_command1995  */

static	ANTLR3_BITWORD FOLLOW_SEMICOLON_in_command1995_bits[]	= { ANTLR3_UINT64_LIT(0x0000000000000002) };

static  ANTLR3_BITSET_LIST FOLLOW_SEMICOLON_in_command1995	= { FOLLOW_SEMICOLON_in_command1995_bits, 1	};

/** Bitset defining follow set for error recovery in rule state: FOLLOW_LET_TOK_in_command2003  */

static	ANTLR3_BITWORD FOLLOW_LET_TOK_in_command2003_bits[]	= { ANTLR3_UINT64_LIT(0x0000000000000000), ANTLR3_UINT64_LIT(0x0000020000000000) };

static  ANTLR3_BITSET_LIST FOLLOW_LET_TOK_in_command2003	= { FOLLOW_LET_TOK_in_command2003_bits, 2	};

/** Bitset defining follow set for error recovery in rule state: FOLLOW_typeOrVarLetDecl_in_command2013  */

static	ANTLR3_BITWORD FOLLOW_typeOrVarLetDecl_in_command2013_bits[]	= { ANTLR3_UINT64_LIT(0x0020000000000000), ANTLR3_UINT64_LIT(0x0004000000000000) };

static  ANTLR3_BITSET_LIST FOLLOW_typeOrVarLetDecl_in_command2013	= { FOLLOW_typeOrVarLetDecl_in_command2013_bits, 2	};

/** Bitset defining follow set for error recovery in rule state: FOLLOW_COMMA_in_command2028  */

static	ANTLR3_BITWORD FOLLOW_COMMA_in_command2028_bits[]	= { ANTLR3_UINT64_LIT(0x0000000000000000), ANTLR3_UINT64_LIT(0x0000020000000000) };

static  ANTLR3_BITSET_LIST FOLLOW_COMMA_in_command2028	= { FOLLOW_COMMA_in_command2028_bits, 2	};

/** Bitset defining follow set for error recovery in rule state: FOLLOW_typeOrVarLetDecl_in_command2030  */

static	ANTLR3_BITWORD FOLLOW_typeOrVarLetDecl_in_command2030_bits[]	= { ANTLR3_UINT64_LIT(0x0020000000000000), ANTLR3_UINT64_LIT(0x0004000000000000) };

static  ANTLR3_BITSET_LIST FOLLOW_typeOrVarLetDecl_in_command2030	= { FOLLOW_typeOrVarLetDecl_in_command2030_bits, 2	};

/** Bitset defining follow set for error recovery in rule state: FOLLOW_IN_TOK_in_command2042  */

static	ANTLR3_BITWORD FOLLOW_IN_TOK_in_command2042_bits[]	= { ANTLR3_UINT64_LIT(0x3F0E000000002C80), ANTLR3_UINT64_LIT(0x08004247A080FFC0), ANTLR3_UINT64_LIT(0x8000004C00477E10), ANTLR3_UINT64_LIT(0x0000000000003028) };

static  ANTLR3_BITSET_LIST FOLLOW_IN_TOK_in_command2042	= { FOLLOW_IN_TOK_in_command2042_bits, 4	};

/** Bitset defining follow set for error recovery in rule state: FOLLOW_command_in_command2044  */

static	ANTLR3_BITWORD FOLLOW_command_in_command2044_bits[]	= { ANTLR3_UINT64_LIT(0x0000000000000002) };

static  ANTLR3_BITSET_LIST FOLLOW_command_in_command2044	= { FOLLOW_command_in_command2044_bits, 1	};

/** Bitset defining follow set for error recovery in rule state: FOLLOW_IDENTIFIER_in_command2071  */

static	ANTLR3_BITWORD FOLLOW_IDENTIFIER_in_command2071_bits[]	= { ANTLR3_UINT64_LIT(0x0000000000000000), ANTLR3_UINT64_LIT(0x0000000000000000), ANTLR3_UINT64_LIT(0x0000004000000000) };

static  ANTLR3_BITSET_LIST FOLLOW_IDENTIFIER_in_command2071	= { FOLLOW_IDENTIFIER_in_command2071_bits, 3	};

/** Bitset defining follow set for error recovery in rule state: FOLLOW_SEMICOLON_in_command2073  */

static	ANTLR3_BITWORD FOLLOW_SEMICOLON_in_command2073_bits[]	= { ANTLR3_UINT64_LIT(0x0000000000000002) };

static  ANTLR3_BITSET_LIST FOLLOW_SEMICOLON_in_command2073	= { FOLLOW_SEMICOLON_in_command2073_bits, 1	};

/** Bitset defining follow set for error recovery in rule state: FOLLOW_letDecl_in_typeOrVarLetDecl2104  */

static	ANTLR3_BITWORD FOLLOW_letDecl_in_typeOrVarLetDecl2104_bits[]	= { ANTLR3_UINT64_LIT(0x0000000000000002) };

static  ANTLR3_BITSET_LIST FOLLOW_letDecl_in_typeOrVarLetDecl2104	= { FOLLOW_letDecl_in_typeOrVarLetDecl2104_bits, 1	};

/** Bitset defining follow set for error recovery in rule state: FOLLOW_typeLetDecl_in_typeOrVarLetDecl2108  */

static	ANTLR3_BITWORD FOLLOW_typeLetDecl_in_typeOrVarLetDecl2108_bits[]	= { ANTLR3_UINT64_LIT(0x0000000000000002) };