diff options
Diffstat (limited to 'src/parser/smtlib.ypp')
-rw-r--r-- | src/parser/smtlib.ypp | 69 |
1 files changed, 28 insertions, 41 deletions
diff --git a/src/parser/smtlib.ypp b/src/parser/smtlib.ypp index 1bc22675a..97f61e715 100644 --- a/src/parser/smtlib.ypp +++ b/src/parser/smtlib.ypp @@ -1,45 +1,34 @@ -%{ -/*****************************************************************************/ -/*! - * \file smtlib.y - * - * Author: Clark Barrett - * - * Created: Apr 30 2005 - * - * <hr> - * - * License to use, copy, modify, sell and/or distribute this software - * and its documentation for any purpose is hereby granted without - * royalty, subject to the terms and conditions defined in the \ref - * LICENSE file provided with this distribution. - * - * <hr> - * - */ -/*****************************************************************************/ -/* - This file contains the bison code for the parser that reads in CVC - commands in SMT-LIB language. -*/ +%{/******************* -*- C++ -*- */ +/** smtlib.ypp + ** This file is part of the CVC4 prototype. + ** + ** Reference-counted encapsulation of a pointer to an expression. + ** + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** + ** This file contains the bison code for the parser that reads in CVC + ** commands in SMT-LIB language. + **/ #include "vc.h" #include "parser_exception.h" -#include "parser_temp.h" +#include "parser_state.h" // Exported shared data -namespace CVC4 { +namespace CVC3 { extern ParserTemp* parserTemp; } // Define shortcuts for various things -#define TMP CVC4::parserTemp -#define EXPR CVC4::parserTemp->expr -#define VC (CVC4::parserTemp->vc) -#define ARRAYSENABLED (CVC4::parserTemp->arrFlag) -#define BVENABLED (CVC4::parserTemp->bvFlag) -#define BVSIZE (CVC4::parserTemp->bvSize) -#define RAT(args) CVC4::newRational args -#define QUERYPARSED CVC4::parserTemp->queryParsed +#define TMP CVC3::parserTemp +#define EXPR CVC3::parserTemp->expr +#define VC (CVC3::parserTemp->vc) +#define ARRAYSENABLED (CVC3::parserTemp->arrFlag) +#define BVENABLED (CVC3::parserTemp->bvFlag) +#define BVSIZE (CVC3::parserTemp->bvSize) +#define RAT(args) CVC3::newRational args +#define QUERYPARSED CVC3::parserTemp->queryParsed // Suppress the bogus warning suppression in bison (it generates // compile error) @@ -51,9 +40,9 @@ extern int smtliblex(void); int smtliberror(const char *s) { std::ostringstream ss; - ss << CVC4::parserTemp->fileName << ":" << CVC4::parserTemp->lineNum + ss << CVC3::parserTemp->fileName << ":" << CVC3::parserTemp->lineNum << ": " << s; - return CVC4::parserTemp->error(ss.str()); + return CVC3::parserTemp->error(ss.str()); } @@ -66,9 +55,9 @@ int smtliberror(const char *s) %union { std::string *str; std::vector<std::string> *strvec; - CVC4::Expr *node; - std::vector<CVC4::Expr> *vec; - std::pair<std::vector<CVC4::Expr>, std::vector<std::string> > *pat_ann; + CVC3::Expr *node; + std::vector<CVC3::Expr> *vec; + std::pair<std::vector<CVC3::Expr>, std::vector<std::string> > *pat_ann; }; @@ -1548,6 +1537,4 @@ fun_pred_symb: } ; - - %% |