diff options
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/Makefile.am | 8 | ||||
| -rw-r--r-- | src/parser/parser.cpp | 5 | ||||
| -rw-r--r-- | src/parser/parser_state.h | 5 | ||||
| -rw-r--r-- | src/parser/pl.ypp | 9 | ||||
| -rw-r--r-- | src/parser/pl_scanner.lpp | 11 | ||||
| -rw-r--r-- | src/parser/smtlib.ypp | 39 | ||||
| -rw-r--r-- | src/parser/smtlib_scanner.lpp | 11 |
7 files changed, 49 insertions, 39 deletions
diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index 8cf9f4a6d..a9560ab93 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -12,10 +12,10 @@ libparser_a_SOURCES = \ BUILT_SOURCES = \ pl_scanner.cpp \ pl.cpp \ - pl.h \ + pl.hpp \ smtlib_scanner.cpp \ smtlib.cpp \ - smtlib.h + smtlib.hpp # produce headers too AM_YFLAGS = -d @@ -25,11 +25,11 @@ pl_scanner.cpp: pl_scanner.lpp smtlib_scanner.cpp: smtlib_scanner.lpp $(LEX) $(AM_LFLAGS) $(LFLAGS) -P smtlib -o $@ $< -pl_scanner.o: pl.h +pl_scanner.o: pl.hpp pl.cpp: pl.ypp $(YACC) $(AM_YFLAGS) $(YFLAGS) -p PL -o $@ $< -smtlib_scanner.o: smtlib.h +smtlib_scanner.o: smtlib.hpp smtlib.cpp: smtlib.ypp $(YACC) $(AM_YFLAGS) $(YFLAGS) -p smtlib -o $@ $< diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 35ca74ecd..89170beeb 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -1,6 +1,11 @@ /********************* -*- C++ -*- */ /** parser.cpp ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. ** ** Parser implementation. ** diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h index 4444925e2..6ab0ada49 100644 --- a/src/parser/parser_state.h +++ b/src/parser/parser_state.h @@ -1,6 +1,11 @@ /********************* -*- C++ -*- */ /** parser_state.h ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. ** ** Extra state of the parser shared by the lexer and parser. ** diff --git a/src/parser/pl.ypp b/src/parser/pl.ypp index e9aeab78e..d8fd57c8c 100644 --- a/src/parser/pl.ypp +++ b/src/parser/pl.ypp @@ -1,12 +1,11 @@ /********************* -*- C++ -*- */ -/** smtlib.ypp +/** pl.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) + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. ** ** This file contains the bison code for the parser that reads in CVC ** commands in the presentation language (hence "PL"). diff --git a/src/parser/pl_scanner.lpp b/src/parser/pl_scanner.lpp index d70937e34..ba8a8e85d 100644 --- a/src/parser/pl_scanner.lpp +++ b/src/parser/pl_scanner.lpp @@ -1,12 +1,13 @@ /********************* -*- C++ -*- */ /** pl_scanner.lpp ** This file is part of the CVC4 prototype. - ** - ** Reference-counted encapsulation of a pointer to an expression. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** CVC4 presentation language lexer. **/ %option interactive @@ -22,7 +23,7 @@ #include <iostream> #include "expr_manager.h" /* for the benefit of parsePL_defs.h */ #include "parser_state.h" -#include "pl.h" +#include "pl.hpp" #include "debug.h" namespace CVC4 { diff --git a/src/parser/smtlib.ypp b/src/parser/smtlib.ypp index 97f61e715..0f3aa8cf4 100644 --- a/src/parser/smtlib.ypp +++ b/src/parser/smtlib.ypp @@ -1,12 +1,11 @@ -%{/******************* -*- C++ -*- */ +%{/********************* -*- 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) + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. ** ** This file contains the bison code for the parser that reads in CVC ** commands in SMT-LIB language. @@ -17,18 +16,18 @@ #include "parser_state.h" // Exported shared data -namespace CVC3 { - extern ParserTemp* parserTemp; +namespace CVC4 { + extern ParserState* parserState; } // Define shortcuts for various things -#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 +#define TMP CVC4::parserState +#define EXPR CVC4::parserState->expr +#define VC (CVC4::parserState->vc) +#define ARRAYSENABLED (CVC4::parserState->arrFlag) +#define BVENABLED (CVC4::parserState->bvFlag) +#define BVSIZE (CVC4::parserState->bvSize) +#define RAT(args) CVC4::newRational args +#define QUERYPARSED CVC4::parserState->queryParsed // Suppress the bogus warning suppression in bison (it generates // compile error) @@ -40,9 +39,9 @@ extern int smtliblex(void); int smtliberror(const char *s) { std::ostringstream ss; - ss << CVC3::parserTemp->fileName << ":" << CVC3::parserTemp->lineNum + ss << CVC4::parserState->fileName << ":" << CVC4::parserState->lineNum << ": " << s; - return CVC3::parserTemp->error(ss.str()); + return CVC4::parserState->error(ss.str()); } @@ -55,9 +54,9 @@ int smtliberror(const char *s) %union { std::string *str; std::vector<std::string> *strvec; - CVC3::Expr *node; - std::vector<CVC3::Expr> *vec; - std::pair<std::vector<CVC3::Expr>, std::vector<std::string> > *pat_ann; + CVC4::Expr *node; + std::vector<CVC4::Expr> *vec; + std::pair<std::vector<CVC4::Expr>, std::vector<std::string> > *pat_ann; }; diff --git a/src/parser/smtlib_scanner.lpp b/src/parser/smtlib_scanner.lpp index b78b27a0d..bb5802aed 100644 --- a/src/parser/smtlib_scanner.lpp +++ b/src/parser/smtlib_scanner.lpp @@ -1,12 +1,13 @@ /********************* -*- C++ -*- */ /** smtlib_scanner.lpp ** This file is part of the CVC4 prototype. - ** - ** Reference-counted encapsulation of a pointer to an expression. - ** - ** The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** Lexer for smtlib format. **/ %option interactive @@ -19,7 +20,7 @@ %{ #include <iostream> -#include "smtlib.h" +#include "smtlib.hpp" #include "debug.h" namespace CVC4 { |