diff options
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/Makefile.am | 4 | ||||
-rw-r--r-- | src/parser/Makefile.antlr_tracing | 3 | ||||
-rw-r--r-- | src/parser/antlr_input.cpp | 93 | ||||
-rw-r--r-- | src/parser/antlr_input.h | 7 | ||||
-rw-r--r-- | src/parser/antlr_line_buffered_input.cpp | 379 | ||||
-rw-r--r-- | src/parser/antlr_line_buffered_input.h | 36 | ||||
-rw-r--r-- | src/parser/antlr_tracing.h | 4 | ||||
-rw-r--r-- | src/parser/bounded_token_buffer.cpp | 6 | ||||
-rw-r--r-- | src/parser/cvc/Cvc.g | 299 | ||||
-rw-r--r-- | src/parser/input.cpp | 15 | ||||
-rw-r--r-- | src/parser/input.h | 6 | ||||
-rw-r--r-- | src/parser/parser.cpp | 38 | ||||
-rw-r--r-- | src/parser/parser.h | 32 | ||||
-rw-r--r-- | src/parser/parser_builder.cpp | 11 | ||||
-rw-r--r-- | src/parser/parser_builder.h | 6 | ||||
-rw-r--r-- | src/parser/smt/smt.cpp | 11 | ||||
-rw-r--r-- | src/parser/smt/smt.h | 3 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 67 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 8 |
19 files changed, 892 insertions, 136 deletions
diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index 4f00cfb3d..f14941d01 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -45,6 +45,8 @@ libcvc4parser_la_SOURCES = \ antlr_input.h \ antlr_input.cpp \ antlr_input_imports.cpp \ + antlr_line_buffered_input.h \ + antlr_line_buffered_input.cpp \ bounded_token_buffer.h \ bounded_token_buffer.cpp \ bounded_token_factory.h \ @@ -64,6 +66,8 @@ libcvc4parser_noinst_la_SOURCES = \ antlr_input.h \ antlr_input.cpp \ antlr_input_imports.cpp \ + antlr_line_buffered_input.h \ + antlr_line_buffered_input.cpp \ bounded_token_buffer.h \ bounded_token_buffer.cpp \ bounded_token_factory.h \ diff --git a/src/parser/Makefile.antlr_tracing b/src/parser/Makefile.antlr_tracing index 087554c52..fa79337b4 100644 --- a/src/parser/Makefile.antlr_tracing +++ b/src/parser/Makefile.antlr_tracing @@ -3,7 +3,8 @@ # This makefile is included from parser directories in order to # do antlr tracing. THIS IS VERY MUCH A HACK, and is only enabled # if CVC4_TRACE_ANTLR is defined (and not 0). In ANTLR 3.2, we -# have to #define +# have to #define "println" and "System," etc., because the +# generator erroneously puts Java in C output! # ifeq ($(CVC4_TRACE_ANTLR),) diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index e52145d4e..67d873a48 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -24,6 +24,7 @@ #include "parser/input.h" #include "parser/bounded_token_buffer.h" #include "parser/bounded_token_factory.h" +#include "parser/antlr_line_buffered_input.h" #include "parser/memory_mapped_input_buffer.h" #include "parser/parser_exception.h" #include "parser/parser.h" @@ -60,8 +61,8 @@ pANTLR3_INPUT_STREAM AntlrInputStream::getAntlr3InputStream() const { return d_input; } -AntlrInputStream* -AntlrInputStream::newFileInputStream(const std::string& name, +AntlrInputStream* +AntlrInputStream::newFileInputStream(const std::string& name, bool useMmap) throw (InputStreamException, AssertionException) { pANTLR3_INPUT_STREAM input = NULL; @@ -81,63 +82,84 @@ AntlrInputStream::newFileInputStream(const std::string& name, return new AntlrInputStream( name, input ); } -AntlrInputStream* -AntlrInputStream::newStreamInputStream(std::istream& input, - const std::string& name) +AntlrInputStream* +AntlrInputStream::newStreamInputStream(std::istream& input, + const std::string& name, + bool lineBuffered) throw (InputStreamException, AssertionException) { - // Since these are all NULL on entry, realloc will be called - char *basep = NULL, *boundp = NULL, *cp = NULL; - /* 64KB seems like a reasonable default size. */ - size_t bufSize = 0x10000; + pANTLR3_INPUT_STREAM inputStream = NULL; - /* Keep going until we can't go no more. */ - while( !input.eof() && !input.fail() ) { + if(lineBuffered) { +#ifdef CVC4_ANTLR3_OLD_INPUT_STREAM + inputStream = + antlr3LineBufferedStreamNew(input, + 0, + (pANTLR3_UINT8) strdup(name.c_str())); +#else /* CVC4_ANTLR3_OLD_INPUT_STREAM */ + inputStream = + antlr3LineBufferedStreamNew(input, + ANTLR3_ENC_8BIT, + (pANTLR3_UINT8) strdup(name.c_str())); +#endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */ + } else { - if( cp == boundp ) { - /* We ran out of room in the buffer. Realloc at double the size. */ - ptrdiff_t offset = cp - basep; - basep = (char *) realloc(basep, bufSize); - if( basep == NULL ) { - throw InputStreamException("Failed buffering input stream: " + name); + // Since these are all NULL on entry, realloc will be called + char *basep = NULL, *boundp = NULL, *cp = NULL; + /* 64KB seems like a reasonable default size. */ + size_t bufSize = 0x10000; + + /* Keep going until we can't go no more. */ + while( !input.eof() && !input.fail() ) { + + if( cp == boundp ) { + /* We ran out of room in the buffer. Realloc at double the size. */ + ptrdiff_t offset = cp - basep; + basep = (char *) realloc(basep, bufSize); + if( basep == NULL ) { + throw InputStreamException("Failed buffering input stream: " + name); + } + cp = basep + offset; + boundp = basep + bufSize; + bufSize *= 2; } - cp = basep + offset; - boundp = basep + bufSize; - bufSize *= 2; - } - /* Read as much as we have room for. */ - input.read( cp, boundp - cp ); - cp += input.gcount(); - } + /* Read as much as we have room for. */ + input.read( cp, boundp - cp ); + cp += input.gcount(); + } - /* Make sure the fail bit didn't get set. */ - if( !input.eof() ) { - throw InputStreamException("Stream input failed: " + name); - } + /* Make sure the fail bit didn't get set. */ + if( !input.eof() ) { + throw InputStreamException("Stream input failed: " + name); + } - /* Create an ANTLR input backed by the buffer. */ + /* Create an ANTLR input backed by the buffer. */ #ifdef CVC4_ANTLR3_OLD_INPUT_STREAM - pANTLR3_INPUT_STREAM inputStream = + inputStream = antlr3NewAsciiStringInPlaceStream((pANTLR3_UINT8) basep, cp - basep, (pANTLR3_UINT8) strdup(name.c_str())); #else /* CVC4_ANTLR3_OLD_INPUT_STREAM */ - pANTLR3_INPUT_STREAM inputStream = + inputStream = antlr3StringStreamNew((pANTLR3_UINT8) basep, ANTLR3_ENC_8BIT, cp - basep, (pANTLR3_UINT8) strdup(name.c_str())); #endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */ - if( inputStream==NULL ) { + + } + + if( inputStream == NULL ) { throw InputStreamException("Couldn't initialize input: " + name); } + return new AntlrInputStream( name, inputStream ); } -AntlrInputStream* -AntlrInputStream::newStringInputStream(const std::string& input, +AntlrInputStream* +AntlrInputStream::newStringInputStream(const std::string& input, const std::string& name) throw (InputStreamException, AssertionException) { char* inputStr = strdup(input.c_str()); @@ -309,6 +331,5 @@ void AntlrInput::setAntlr3Parser(pANTLR3_PARSER pParser) { d_parser->rec->mismatch; } - }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index dca26ab75..a39defd14 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -77,7 +77,8 @@ public: /** Create an input from an istream. */ static AntlrInputStream* newStreamInputStream(std::istream& input, - const std::string& name) + const std::string& name, + bool lineBuffered = false) throw (InputStreamException, AssertionException); /** Create a string input. @@ -88,7 +89,7 @@ public: static AntlrInputStream* newStringInputStream(const std::string& input, const std::string& name) throw (InputStreamException, AssertionException); -}; +};/* class AntlrInputStream */ class Parser; @@ -209,7 +210,7 @@ protected: /** Set the Parser object for this input. */ virtual void setParser(Parser& parser); -}; +};/* class AntlrInput */ inline std::string AntlrInput::getUnparsedText() { const char *base = (const char *)d_antlr3InputStream->data; diff --git a/src/parser/antlr_line_buffered_input.cpp b/src/parser/antlr_line_buffered_input.cpp new file mode 100644 index 000000000..b42562f72 --- /dev/null +++ b/src/parser/antlr_line_buffered_input.cpp @@ -0,0 +1,379 @@ +/********************* */ +/*! \file antlr_line_buffered_input.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 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.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include <antlr3.h> +#include <iostream> +#include <string> + +#include "util/output.h" +#include "util/Assert.h" + +namespace CVC4 { +namespace parser { + +typedef struct ANTLR3_LINE_BUFFERED_INPUT_STREAM { + ANTLR3_INPUT_STREAM antlr; + std::istream* in; +} *pANTLR3_LINE_BUFFERED_INPUT_STREAM; + +static pANTLR3_INPUT_STREAM antlr3CreateLineBufferedStream(std::istream& in); + +static void +setupInputStream(pANTLR3_INPUT_STREAM input) +{ +#if 0 + ANTLR3_BOOLEAN isBigEndian; + + // Used to determine the endianness of the machine we are currently + // running on. + // + ANTLR3_UINT16 bomTest = 0xFEFF; + + // What endianess is the machine we are running on? If the incoming + // encoding endianess is the same as this machine's natural byte order + // then we can use more efficient API calls. + // + if (*((pANTLR3_UINT8)(&bomTest)) == 0xFE) + { + isBigEndian = ANTLR3_TRUE; + } + else + { + isBigEndian = ANTLR3_FALSE; + } + + // What encoding did the user tell us {s}he thought it was? I am going + // to get sick of the questions on antlr-interest, I know I am. + // + switch (input->encoding) + { + case ANTLR3_ENC_UTF8: + + // See if there is a BOM at the start of this UTF-8 sequence + // and just eat it if there is. Windows .TXT files have this for instance + // as it identifies UTF-8 even though it is of no consequence for byte order + // as UTF-8 does not have a byte order. + // + if ( (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar)) == 0xEF + && (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar+1)) == 0xBB + && (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar+2)) == 0xBF + ) + { + // The UTF8 BOM is present so skip it + // + input->nextChar = (void *)((pANTLR3_UINT8)input->nextChar + 3); + } + + // Install the UTF8 input routines + // + antlr3UTF8SetupStream(input); + break; + + case ANTLR3_ENC_UTF16: + + // See if there is a BOM at the start of the input. If not then + // we assume that the byte order is the natural order of this + // machine (or it is really UCS2). If there is a BOM we determine if the encoding + // is the same as the natural order of this machine. + // + if ( (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar)) == 0xFE + && (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar+1)) == 0xFF + ) + { + // BOM Present, indicates Big Endian + // + input->nextChar = (void *)((pANTLR3_UINT8)input->nextChar + 2); + + antlr3UTF16SetupStream(input, isBigEndian, ANTLR3_TRUE); + } + else if ( (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar)) == 0xFF + && (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar+1)) == 0xFE + ) + { + // BOM present, indicates Little Endian + // + input->nextChar = (void *)((pANTLR3_UINT8)input->nextChar + 2); + + antlr3UTF16SetupStream(input, isBigEndian, ANTLR3_FALSE); + } + else + { + // No BOM present, assume local computer byte order + // + antlr3UTF16SetupStream(input, isBigEndian, isBigEndian); + } + break; + + case ANTLR3_ENC_UTF32: + + // See if there is a BOM at the start of the input. If not then + // we assume that the byte order is the natural order of this + // machine. If there is we determine if the encoding + // is the same as the natural order of this machine. + // + if ( (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar)) == 0x00 + && (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar+1)) == 0x00 + && (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar+2)) == 0xFE + && (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar+3)) == 0xFF + ) + { + // BOM Present, indicates Big Endian + // + input->nextChar = (void *)((pANTLR3_UINT8)input->nextChar + 4); + + antlr3UTF32SetupStream(input, isBigEndian, ANTLR3_TRUE); + } + else if ( (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar)) == 0xFF + && (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar+1)) == 0xFE + && (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar+1)) == 0x00 + && (ANTLR3_UINT8)(*((pANTLR3_UINT8)input->nextChar+1)) == 0x00 + ) + { + // BOM present, indicates Little Endian + // + input->nextChar = (void *)((pANTLR3_UINT8)input->nextChar + 4); + + antlr3UTF32SetupStream(input, isBigEndian, ANTLR3_FALSE); + } + else + { + // No BOM present, assume local computer byte order + // + antlr3UTF32SetupStream(input, isBigEndian, isBigEndian); + } + break; + + case ANTLR3_ENC_UTF16BE: + + // Encoding is definately Big Endian with no BOM + // + antlr3UTF16SetupStream(input, isBigEndian, ANTLR3_TRUE); + break; + + case ANTLR3_ENC_UTF16LE: + + // Encoding is definately Little Endian with no BOM + // + antlr3UTF16SetupStream(input, isBigEndian, ANTLR3_FALSE); + break; + + case ANTLR3_ENC_UTF32BE: + + // Encoding is definately Big Endian with no BOM + // + antlr3UTF32SetupStream(input, isBigEndian, ANTLR3_TRUE); + break; + + case ANTLR3_ENC_UTF32LE: + + // Encoding is definately Little Endian with no BOM + // + antlr3UTF32SetupStream(input, isBigEndian, ANTLR3_FALSE); + break; + + case ANTLR3_ENC_EBCDIC: + + // EBCDIC is basically the same as ASCII but with an on the + // fly translation to ASCII + // + antlr3EBCDICSetupStream(input); + break; + + case ANTLR3_ENC_8BIT: + default: + + // Standard 8bit/ASCII + // + antlr38BitSetupStream(input); + break; + } +#endif /* 0 */ +} + +static ANTLR3_UCHAR +myLA(pANTLR3_INT_STREAM is, ANTLR3_INT32 la) { + pANTLR3_INPUT_STREAM input; + + input = ((pANTLR3_INPUT_STREAM) (is->super)); + + Debug("pipe") << "LA" << std::endl; + if (( ((pANTLR3_UINT8)input->nextChar) + la - 1) >= (((pANTLR3_UINT8)input->data) + input->sizeBuf)) + { + std::istream& in = *((pANTLR3_LINE_BUFFERED_INPUT_STREAM)input)->in; + if(!in) { + Debug("pipe") << "EOF" << std::endl; + return ANTLR3_CHARSTREAM_EOF; + } + Debug("pipe") << "READ" << std::endl; + if(input->data == NULL) { + Debug("pipe") << "ALLOC" << std::endl; + input->data = malloc(1024); + input->nextChar = input->data; + } else { + Debug("pipe") << "REALLOC" << std::endl; + size_t pos = (char*)input->nextChar - (char*)input->data; + input->data = realloc(input->data, input->sizeBuf + 1024); + input->nextChar = (char*)input->data + pos; + } + in.getline((((char*)input->data) + input->sizeBuf), 1024); + while(in.fail() && !in.eof()) { + Debug("pipe") << "input string too long, reallocating" << std::endl; + input->sizeBuf += strlen(((char*)input->data) + input->sizeBuf); + size_t pos = (char*)input->nextChar - (char*)input->data; + input->data = realloc(input->data, input->sizeBuf + 1024); + input->nextChar = (char*)input->data + pos; + in.clear(); + in.getline((((char*)input->data) + input->sizeBuf), 1024); + } + input->sizeBuf += strlen(((char*)input->data) + input->sizeBuf); + Assert(*(((char*)input->data) + input->sizeBuf) == '\0'); + Debug("pipe") << "SIZEBUF now " << input->sizeBuf << std::endl; + *(((char*)input->data) + input->sizeBuf) = '\n'; + ++input->sizeBuf; + } + + Debug("pipe") << "READ POINTER[" << la << "] AT: >>" << std::string(((char*)input->nextChar), input->sizeBuf - (((char*)input->nextChar) - (char*)input->data) + 1) << "<< returning '" << (char)(*((pANTLR3_UINT8)input->nextChar + la - 1)) << "' (" << (unsigned)(*((pANTLR3_UINT8)input->nextChar + la - 1)) << ")" << std::endl; + return (ANTLR3_UCHAR)(*((pANTLR3_UINT8)input->nextChar + la - 1)); +} + + +static void +myConsume(pANTLR3_INT_STREAM is) +{ + pANTLR3_INPUT_STREAM input; + + input = ((pANTLR3_INPUT_STREAM) (is->super)); + + Debug("pipe") << "consume! '" << *(char*)input->nextChar << "' (" << (unsigned)*(char*)input->nextChar << ")" << std::endl; + if ((pANTLR3_UINT8)(input->nextChar) < (((pANTLR3_UINT8)input->data) + input->sizeBuf)) + { + /* Indicate one more character in this line + */ + input->charPositionInLine++; + + if ((ANTLR3_UCHAR)(*((pANTLR3_UINT8)input->nextChar)) == input->newlineChar) + { + /* Reset for start of a new line of input + */ + input->line++; + input->charPositionInLine = 0; + input->currentLine = (void *)(((pANTLR3_UINT8)input->nextChar) + 1); + Debug("pipe") << "-- newline!" << std::endl; + } + + /* Increment to next character position + */ + input->nextChar = (void *)(((pANTLR3_UINT8)input->nextChar) + 1); + Debug("pipe") << "-- advance nextChar! looking at '" << *(char*)input->nextChar << "' (" << (unsigned)*(char*)input->nextChar << ")" << std::endl; + } else Debug("pipe") << "-- nothing!" << std::endl; +} + +pANTLR3_INPUT_STREAM +antlr3LineBufferedStreamNew(std::istream& in, ANTLR3_UINT32 encoding, pANTLR3_UINT8 name) +{ + pANTLR3_INPUT_STREAM input; + + if(!in) { + return NULL; + } + + // First order of business is to set up the stream and install the data pointer. + // Then we will work out the encoding and byte order and adjust the API functions that are installed for the + // default 8Bit stream accordingly. + // + input = antlr3CreateLineBufferedStream(in); + if (input == NULL) + { + return NULL; + } + + // Size (in bytes) of the given 'string' + // + input->sizeBuf = 0; + + input->istream->_LA = myLA; + input->istream->consume = myConsume; + +#ifndef CVC4_ANTLR3_OLD_INPUT_STREAM + // We have the data in memory now so we can deal with it according to + // the encoding scheme we were given by the user. + // + input->encoding = encoding; +#endif /* ! CVC4_ANTLR3_OLD_INPUT_STREAM */ + + // Now we need to work out the endian type and install any + // API functions that differ from 8Bit + // + setupInputStream(input); + + // Now we can set up the file name + // + input->istream->streamName = input->strFactory->newStr8(input->strFactory, name); + input->fileName = input->istream->streamName; + + return input; +} + +static pANTLR3_INPUT_STREAM +antlr3CreateLineBufferedStream(std::istream& in) +{ + // Pointer to the input stream we are going to create + // + pANTLR3_INPUT_STREAM input; + + if (!in) + { + return NULL; + } + + // Allocate memory for the input stream structure + // + input = (pANTLR3_INPUT_STREAM) + ANTLR3_CALLOC(1, sizeof(ANTLR3_LINE_BUFFERED_INPUT_STREAM)); + + if (input == NULL) + { + return NULL; + } + + // Structure was allocated correctly, now we can install the pointer + // + input->data = malloc(1024); + input->isAllocated = ANTLR3_FALSE; + + ((pANTLR3_LINE_BUFFERED_INPUT_STREAM)input)->in = ∈ + + // Call the common 8 bit input stream handler + // initialization. + // +#ifdef CVC4_ANTLR3_OLD_INPUT_STREAM + antlr3AsciiSetupStream(input, ANTLR3_CHARSTREAM); +#else /* CVC4_ANTLR3_OLD_INPUT_STREAM */ + antlr38BitSetupStream(input); + // In some libantlr3c 3.4-beta versions, this call is not included in the above. + // This is probably an erroneously-deleted line in the libantlr3c source since 3.2. + antlr3GenericSetupStream(input); +#endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */ + + return input; +} + +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ + diff --git a/src/parser/antlr_line_buffered_input.h b/src/parser/antlr_line_buffered_input.h new file mode 100644 index 000000000..b59645dd7 --- /dev/null +++ b/src/parser/antlr_line_buffered_input.h @@ -0,0 +1,36 @@ +/********************* */ +/*! \file antlr_line_buffered_input.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 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.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "cvc4parser_private.h" + +#ifndef __CVC4__PARSER__ANTLR_LINE_BUFFERED_INPUT_H +#define __CVC4__PARSER__ANTLR_LINE_BUFFERED_INPUT_H + +#include <antlr3.h> + +namespace CVC4 { +namespace parser { + +pANTLR3_INPUT_STREAM +antlr3LineBufferedStreamNew(std::istream& in, ANTLR3_UINT32 encoding, pANTLR3_UINT8 name); + +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__PARSER__ANTLR_LINE_BUFFERED_INPUT_H */ diff --git a/src/parser/antlr_tracing.h b/src/parser/antlr_tracing.h index 2c3e66c12..95f6100f4 100644 --- a/src/parser/antlr_tracing.h +++ b/src/parser/antlr_tracing.h @@ -54,7 +54,7 @@ static struct __Cvc4System { struct JavaPrinter { template <class T> JavaPrinter operator+(const T& t) const { - ::CVC4::Message() << t; + Message() << t; return JavaPrinter(); } };/* struct JavaPrinter */ @@ -67,7 +67,7 @@ static struct __Cvc4System { * to the call-by-value semantics of C. All that's left to * do is print the newline. */ - void println(JavaPrinter) { ::CVC4::Message() << std::endl; } + void println(JavaPrinter) { Message() << std::endl; } } out; } System; diff --git a/src/parser/bounded_token_buffer.cpp b/src/parser/bounded_token_buffer.cpp index d77f72bfa..d63d3afe0 100644 --- a/src/parser/bounded_token_buffer.cpp +++ b/src/parser/bounded_token_buffer.cpp @@ -308,19 +308,19 @@ setTokenSource ( pANTLR3_TOKEN_STREAM ts, static pANTLR3_STRING toString (pANTLR3_TOKEN_STREAM ts) { - Unreachable(); + Unimplemented("toString(ts)"); } static pANTLR3_STRING toStringSS(pANTLR3_TOKEN_STREAM ts, ANTLR3_UINT32 start, ANTLR3_UINT32 stop) { - Unreachable(); + Unimplemented("toStringSS(ts, %u, %u)", start, stop); } static pANTLR3_STRING toStringTT (pANTLR3_TOKEN_STREAM ts, pANTLR3_COMMON_TOKEN start, pANTLR3_COMMON_TOKEN stop) { - Unreachable(); + Unimplemented("toStringTT(ts, %u, %u)", start, stop); } /** Move the input pointer to the next incoming token. The stream diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 9f0c2cddb..657a2fe2c 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -132,9 +132,6 @@ tokens { PARENHASH = '(#'; HASHPAREN = '#)'; - //DOT = '.'; - DOTDOT = '..'; - // Operators ARROW_TOK = '->'; @@ -198,6 +195,12 @@ tokens { BVSGT_TOK = 'BVSGT'; BVSLE_TOK = 'BVSLE'; BVSGE_TOK = 'BVSGE'; + + // these are parsed by special NUMBER_OR_RANGEOP rule, below + DECIMAL_LITERAL; + INTEGER_LITERAL; + DOT; + DOTDOT; }/* tokens */ @parser::members { @@ -312,7 +315,8 @@ Kind getOperatorKind(int type, bool& negate) { case PLUS_TOK: return kind::PLUS; case MINUS_TOK: return kind::MINUS; case STAR_TOK: return kind::MULT; - case INTDIV_TOK: Unhandled(CvcParserTokenNames[type]); + case INTDIV_TOK: return kind::INTS_DIVISION; + case MOD_TOK: return kind::INTS_MODULUS; case DIV_TOK: return kind::DIVISION; case EXP_TOK: Unhandled(CvcParserTokenNames[type]); @@ -363,9 +367,14 @@ Expr createPrecedenceTree(ExprManager* em, unsigned pivot = findPivot(operators, startIndex, stopIndex - 1); //Debug("prec") << "pivot[" << startIndex << "," << stopIndex - 1 << "] at " << pivot << std::endl; bool negate; - Expr e = em->mkExpr(getOperatorKind(operators[pivot], negate), - createPrecedenceTree(em, expressions, operators, startIndex, pivot), - createPrecedenceTree(em, expressions, operators, pivot + 1, stopIndex)); + Kind k = getOperatorKind(operators[pivot], negate); + Expr lhs = createPrecedenceTree(em, expressions, operators, startIndex, pivot); + Expr rhs = createPrecedenceTree(em, expressions, operators, pivot + 1, stopIndex); + if(k == kind::EQUAL && lhs.getType().isBoolean()) { + WarningOnce() << "Warning: converting BOOL = BOOL to BOOL <=> BOOL" << std::endl; + k = kind::IFF; + } + Expr e = em->mkExpr(k, lhs, rhs); return negate ? em->mkExpr(kind::NOT, e) : e; }/* createPrecedenceTree() recursive variant */ @@ -497,6 +506,8 @@ namespace CVC4 { #include "util/output.h" #include <vector> +#include <string> +#include <sstream> #define REPEAT_COMMAND(k, CommandCtor) \ ({ \ @@ -691,8 +702,8 @@ mainCommand[CVC4::Command*& cmd] { UNSUPPORTED("CALL command"); } | ECHO_TOK - ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } ) - { Message() << s << std::endl; } + ( simpleSymbolicExpr[sexpr] + { Message() << sexpr << std::endl; } | { Message() << std::endl; } ) @@ -732,17 +743,30 @@ mainCommand[CVC4::Command*& cmd] | toplevelDeclaration[cmd] ; -symbolicExpr[CVC4::SExpr& sexpr] +simpleSymbolicExpr[CVC4::SExpr& sexpr] @declarations { - std::vector<SExpr> children; std::string s; + CVC4::Rational r; } - : INTEGER_LITERAL ('.' DIGIT+)? - { sexpr = SExpr((const char*)$symbolicExpr.text->chars); } + : INTEGER_LITERAL + { sexpr = SExpr(AntlrInput::tokenText($INTEGER_LITERAL)); } + | DECIMAL_LITERAL + { sexpr = SExpr(AntlrInput::tokenText($DECIMAL_LITERAL)); } + | HEX_LITERAL + { sexpr = SExpr(AntlrInput::tokenText($HEX_LITERAL)); } + | BINARY_LITERAL + { sexpr = SExpr(AntlrInput::tokenText($BINARY_LITERAL)); } | str[s] { sexpr = SExpr(s); } | IDENTIFIER { sexpr = SExpr(AntlrInput::tokenText($IDENTIFIER)); } + ; + +symbolicExpr[CVC4::SExpr& sexpr] +@declarations { + std::vector<SExpr> children; +} + : simpleSymbolicExpr[sexpr] | LPAREN (symbolicExpr[sexpr] { children.push_back(sexpr); } )* RPAREN { sexpr = SExpr(children); } ; @@ -1020,9 +1044,12 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t, bool& lhs] @init { Type t2; - Expr f; + Expr f, f2; std::string id; std::vector<Type> types; + std::vector< std::pair<std::string, Type> > typeIds; + DeclarationScope* declScope; + Parser* parser; lhs = false; } /* named types */ @@ -1056,24 +1083,33 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t, { t = EXPR_MANAGER->mkArrayType(t, t2); } /* subtypes */ - | SUBTYPE_TOK LPAREN formula[f] ( COMMA formula[f] )? RPAREN - { UNSUPPORTED("subtypes not supported yet"); - t = Type(); } + | SUBTYPE_TOK LPAREN + /* A bit tricky: this LAMBDA expression cannot refer to constants + * declared in the outer context. What follows isn't quite right, + * though, since type aliases and function definitions should be + * retained in the set of current declarations. */ + { /*declScope = PARSER_STATE->getDeclarationScope(); + PARSER_STATE->useDeclarationsFrom(new DeclarationScope());*/ } + formula[f] ( COMMA formula[f2] )? RPAREN + { /*DeclarationScope* old = PARSER_STATE->getDeclarationScope(); + PARSER_STATE->useDeclarationsFrom(declScope); + delete old;*/ + t = f2.isNull() ? + EXPR_MANAGER->mkPredicateSubtype(f) : + EXPR_MANAGER->mkPredicateSubtype(f, f2); + } /* subrange types */ | LBRACKET k1=bound DOTDOT k2=bound RBRACKET - { std::stringstream ss; - ss << "subranges not supported yet: [" << k1 << ":" << k2 << ']'; - UNSUPPORTED(ss.str()); - if(k1.hasBound() && k2.hasBound() && + { if(k1.hasBound() && k2.hasBound() && k1.getBound() > k2.getBound()) { - ss.str(""); + std::stringstream ss; ss << "Subrange [" << k1.getBound() << ".." << k2.getBound() << "] inappropriate: range must be nonempty!"; PARSER_STATE->parseError(ss.str()); } - Debug("subranges") << ss.str() << std::endl; - t = Type(); } + t = EXPR_MANAGER->mkSubrangeType(SubrangeBounds(k1, k2)); + } /* tuple types / old-style function types */ | LBRACKET type[t,check] { types.push_back(t); } @@ -1087,15 +1123,14 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t, } } else { // tuple type [ T, U, V... ] - t = EXPR_MANAGER->mkTupleType(types); + t = PARSER_STATE->mkTupleType(types); } } /* record types */ - | SQHASH identifier[id,CHECK_NONE,SYM_SORT] COLON type[t,check] - ( COMMA identifier[id,CHECK_NONE,SYM_SORT] COLON type[t,check] )* HASHSQ - { UNSUPPORTED("records not supported yet"); - t = Type(); } + | SQHASH identifier[id,CHECK_NONE,SYM_SORT] COLON type[t,check] { typeIds.push_back(std::make_pair(id, t)); } + ( COMMA identifier[id,CHECK_NONE,SYM_SORT] COLON type[t,check] { typeIds.push_back(std::make_pair(id, t)); } )* HASHSQ + { t = PARSER_STATE->mkRecordType(typeIds); } /* bitvector types */ | BITVECTOR_TOK LPAREN k=numeral RPAREN @@ -1321,14 +1356,20 @@ arithmeticBinop[unsigned& op] | MINUS_TOK | STAR_TOK | INTDIV_TOK + | MOD_TOK | DIV_TOK | EXP_TOK ; -/** Parses an array assignment term. */ +/** Parses an array/tuple/record assignment term. */ storeTerm[CVC4::Expr& f] : uminusTerm[f] - ( WITH_TOK arrayStore[f] ( COMMA arrayStore[f] )* )* + ( WITH_TOK + ( arrayStore[f] ( COMMA arrayStore[f] )* + | DOT ( tupleStore[f] ( COMMA DOT tupleStore[f] )* + | recordStore[f] ( COMMA DOT recordStore[f] )* ) ) + | /* nothing */ + ) ; /** @@ -1361,6 +1402,84 @@ arrayStore[CVC4::Expr& f] } ; +/** + * Parses just part of the tuple assignment (and constructs + * the store terms). + */ +tupleStore[CVC4::Expr& f] +@init { + Expr f2; +} + : k=numeral ASSIGN_TOK uminusTerm[f2] + { + Type t = f.getType(); + if(! t.isDatatype()) { + PARSER_STATE->parseError("tuple-update applied to non-tuple"); + } + Datatype tuple = DatatypeType(f.getType()).getDatatype(); + if(tuple.getName() != "__cvc4_tuple") { + PARSER_STATE->parseError("tuple-update applied to non-tuple"); + } + if(k < tuple[0].getNumArgs()) { + std::vector<Expr> args; + for(unsigned i = 0; i < tuple[0].getNumArgs(); ++i) { + if(i == k) { + args.push_back(f2); + } else { + Expr selectorOp = tuple[0][i].getSelector(); + Expr select = MK_EXPR(CVC4::kind::APPLY_SELECTOR, selectorOp, f); + args.push_back(select); + } + } + f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, tuple[0].getConstructor(), args); + } else { + std::stringstream ss; + ss << "tuple is of length " << tuple[0].getNumArgs() << "; cannot update index " << k; + PARSER_STATE->parseError(ss.str()); + } + } + ; + +/** + * Parses just part of the record assignment (and constructs + * the store terms). + */ +recordStore[CVC4::Expr& f] +@init { + std::string id; + Expr f2; +} + : identifier[id,CHECK_NONE,SYM_VARIABLE] ASSIGN_TOK uminusTerm[f2] + { + Type t = f.getType(); + if(! t.isDatatype()) { + PARSER_STATE->parseError("record-update applied to non-record"); + } + Datatype record = DatatypeType(f.getType()).getDatatype(); + if(record.getName() != "__cvc4_record") { + PARSER_STATE->parseError("record-update applied to non-record"); + } + const DatatypeConstructorArg* updateArg; + try { + updateArg = &record[0][id]; + } catch(IllegalArgumentException& e) { + PARSER_STATE->parseError(std::string("no such field `") + id + "' in record"); + } + std::vector<Expr> args; + for(unsigned i = 0; i < record[0].getNumArgs(); ++i) { + const DatatypeConstructorArg* thisArg = &record[0][i]; + if(thisArg == updateArg) { + args.push_back(f2); + } else { + Expr selectorOp = record[0][i].getSelector(); + Expr select = MK_EXPR(CVC4::kind::APPLY_SELECTOR, selectorOp, f); + args.push_back(select); + } + } + f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, record[0].getConstructor(), args); + } + ; + /** Parses a unary minus term. */ uminusTerm[CVC4::Expr& f] @init { @@ -1469,20 +1588,42 @@ postfixTerm[CVC4::Expr& f] } /* record / tuple select */ - // FIXME - clash in lexer between tuple-select and real; can - // resolve with syntactic predicate in ANTLR 3.3, but broken in - // 3.2 ? - /*| DOT + | DOT ( identifier[id,CHECK_NONE,SYM_VARIABLE] - { UNSUPPORTED("record select not implemented yet"); - f = Expr(); } + { Type t = f.getType(); + if(! t.isDatatype()) { + PARSER_STATE->parseError("record-select applied to non-record"); + } + Datatype record = DatatypeType(f.getType()).getDatatype(); + if(record.getName() != "__cvc4_record") { + PARSER_STATE->parseError("record-select applied to non-record"); + } + try { + Expr selectorOp = record[0][id].getSelector(); + f = MK_EXPR(CVC4::kind::APPLY_SELECTOR, selectorOp, f); + } catch(IllegalArgumentException& e) { + PARSER_STATE->parseError(std::string("no such field `") + id + "' in record"); + } + } | k=numeral - { UNSUPPORTED("tuple select not implemented yet"); - // This will assert-fail if k too big or f not a tuple - // that's ok for now, once a TUPLE_SELECT operator exists, - // that will do any necessary type checking - f = EXPR_MANAGER->mkVar(TupleType(f.getType()).getTypes()[k]); } - )*/ + { Type t = f.getType(); + if(! t.isDatatype()) { + PARSER_STATE->parseError("tuple-select applied to non-tuple"); + } + Datatype tuple = DatatypeType(f.getType()).getDatatype(); + if(tuple.getName() != "__cvc4_tuple") { + PARSER_STATE->parseError("tuple-select applied to non-tuple"); + } + try { + Expr selectorOp = tuple[0][k].getSelector(); + f = MK_EXPR(CVC4::kind::APPLY_SELECTOR, selectorOp, f); + } catch(IllegalArgumentException& e) { + std::stringstream ss; + ss << "tuple is of length " << tuple[0].getNumArgs() << "; cannot access index " << k; + PARSER_STATE->parseError(ss.str()); + } + } + ) )* ( typeAscription[f, t] { if(f.getKind() == CVC4::kind::APPLY_CONSTRUCTOR && t.isDatatype()) { @@ -1641,6 +1782,8 @@ simpleTerm[CVC4::Expr& f] @init { std::string name; std::vector<Expr> args; + std::vector<std::string> names; + Expr e; Debug("parser-extra") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl; Type t; } @@ -1654,7 +1797,12 @@ simpleTerm[CVC4::Expr& f] /* If args has elements, we must be a tuple literal. * Otherwise, f is already the sub-formula, and * there's nothing to do */ - f = EXPR_MANAGER->mkExpr(kind::TUPLE, args); + std::vector<Type> types; + for(std::vector<Expr>::const_iterator i = args.begin(); i != args.end(); ++i) { + types.push_back((*i).getType()); + } + DatatypeType t = PARSER_STATE->mkTupleType(types); + f = EXPR_MANAGER->mkExpr(kind::APPLY_CONSTRUCTOR, t.getDatatype()[0].getConstructor(), args); } } @@ -1677,9 +1825,16 @@ simpleTerm[CVC4::Expr& f] std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 4); f = MK_CONST( BitVector(binString, 2) ); } /* record literals */ - | PARENHASH recordEntry (COMMA recordEntry)+ HASHPAREN - { UNSUPPORTED("records not implemented yet"); - f = Expr(); } + | PARENHASH recordEntry[name,e] { names.push_back(name); args.push_back(e); } + ( COMMA recordEntry[name,e] { names.push_back(name); args.push_back(e); } )* HASHPAREN + { std::vector< std::pair<std::string, Type> > typeIds; + Assert(names.size() == args.size()); + for(unsigned i = 0; i < names.size(); ++i) { + typeIds.push_back(std::make_pair(names[i], args[i].getType())); + } + DatatypeType t = PARSER_STATE->mkRecordType(typeIds); + f = EXPR_MANAGER->mkExpr(kind::APPLY_CONSTRUCTOR, t.getDatatype()[0].getConstructor(), args); + } /* variable / zero-ary constructor application */ | identifier[name,CHECK_DECLARED,SYM_VARIABLE] @@ -1707,12 +1862,8 @@ typeAscription[const CVC4::Expr& f, CVC4::Type& t] /** * Matches an entry in a record literal. */ -recordEntry -@init { - std::string id; - Expr f; -} - : identifier[id,CHECK_DECLARED,SYM_VARIABLE] ASSIGN_TOK formula[f] +recordEntry[std::string& name, CVC4::Expr& ex] + : identifier[name,CHECK_NONE,SYM_VARIABLE] ASSIGN_TOK formula[ex] ; /** @@ -1824,22 +1975,6 @@ selector[CVC4::DatatypeConstructor& ctor] IDENTIFIER : (ALPHA | '_') (ALPHA | DIGIT | '_' | '\'' | '\\' | '?' | '$' | '~')*; /** - * Matches an integer literal. - */ -INTEGER_LITERAL - : ( '0' - | '1'..'9' DIGIT* - ) - ; - -/** - * Matches a decimal literal. - */ -DECIMAL_LITERAL - : INTEGER_LITERAL '.' DIGIT+ - ; - -/** * Same as an integer literal converted to an unsigned int, but * slightly more convenient AND works around a strange ANTLR bug (?) * in the BVPLUS/BVMINUS/BVMULT rules where $INTEGER_LITERAL was @@ -1901,6 +2036,32 @@ fragment ALPHA : 'a'..'z' | 'A'..'Z'; */ fragment DIGIT : '0'..'9'; +// This rule adapted from http://www.antlr.org/wiki/pages/viewpage.action?pageId=13828121 +// which reportedly comes from Tapestry (http://tapestry.apache.org/tapestry5/) +// +// Special rule that uses parsing tricks to identify numbers and ranges; it's all about +// the dot ('.'). +// Recognizes: +// '.' as DOT +// '..' as DOTDOT +// INTEGER_LITERAL (digit+) +// DECIMAL_LITERAL (digit* . digit+) +// Has to watch out for embedded rangeop (i.e. "1..10" is not "1." and ".10"). +// +// This doesn't ever generate the NUMBER_OR_RANGEOP token, it +// manipulates the $type inside to return the right token. +NUMBER_OR_RANGEOP + : DIGIT+ + ( + { LA(2) != '.' }? => '.' DIGIT* { $type = DECIMAL_LITERAL; } + | { $type = INTEGER_LITERAL; } + ) + | '.' + ( '.' {$type = DOTDOT; } + | {$type = DOT; } + ) + ; + /** * Matches the hexidecimal digits (0-9, a-f, A-F) */ diff --git a/src/parser/input.cpp b/src/parser/input.cpp index 70c887371..76aa47812 100644 --- a/src/parser/input.cpp +++ b/src/parser/input.cpp @@ -59,25 +59,26 @@ Input* Input::newFileInput(InputLanguage lang, bool useMmap) throw (InputStreamException, AssertionException) { AntlrInputStream *inputStream = - AntlrInputStream::newFileInputStream(filename,useMmap); - return AntlrInput::newInput(lang,*inputStream); + AntlrInputStream::newFileInputStream(filename, useMmap); + return AntlrInput::newInput(lang, *inputStream); } Input* Input::newStreamInput(InputLanguage lang, std::istream& input, - const std::string& name) + const std::string& name, + bool lineBuffered) throw (InputStreamException, AssertionException) { AntlrInputStream *inputStream = - AntlrInputStream::newStreamInputStream(input,name); - return AntlrInput::newInput(lang,*inputStream); + AntlrInputStream::newStreamInputStream(input, name, lineBuffered); + return AntlrInput::newInput(lang, *inputStream); } Input* Input::newStringInput(InputLanguage lang, const std::string& str, const std::string& name) throw (InputStreamException, AssertionException) { - AntlrInputStream *inputStream = AntlrInputStream::newStringInputStream(str,name); - return AntlrInput::newInput(lang,*inputStream); + AntlrInputStream *inputStream = AntlrInputStream::newStringInputStream(str, name); + return AntlrInput::newInput(lang, *inputStream); } }/* CVC4::parser namespace */ diff --git a/src/parser/input.h b/src/parser/input.h index 25023e1a8..8fa51a095 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -110,7 +110,7 @@ public: */ static Input* newFileInput(InputLanguage lang, const std::string& filename, - bool useMmap=false) + bool useMmap = false) throw (InputStreamException, AssertionException); /** Create an input for the given stream. @@ -121,7 +121,8 @@ public: */ static Input* newStreamInput(InputLanguage lang, std::istream& input, - const std::string& name) + const std::string& name, + bool lineBuffered = false) throw (InputStreamException, AssertionException); /** Create an input for the given string @@ -182,6 +183,7 @@ protected: /** Set the Parser object for this input. */ virtual void setParser(Parser& parser) = 0; + };/* class Input */ }/* CVC4::parser namespace */ diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 4418ea18f..3efc315cc 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -54,6 +54,7 @@ Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode, bool par } Expr Parser::getSymbol(const std::string& name, SymbolType type) { + checkDeclaration(name, CHECK_DECLARED, type); Assert( isDeclared(name, type) ); switch( type ) { @@ -77,12 +78,14 @@ Expr Parser::getFunction(const std::string& name) { Type Parser::getType(const std::string& var_name, SymbolType type) { + checkDeclaration(var_name, CHECK_DECLARED, type); Assert( isDeclared(var_name, type) ); Type t = getSymbol(var_name, type).getType(); return t; } Type Parser::getSort(const std::string& name) { + checkDeclaration(name, CHECK_DECLARED, SYM_SORT); Assert( isDeclared(name, SYM_SORT) ); Type t = d_declScope->lookupType(name); return t; @@ -90,12 +93,14 @@ Type Parser::getSort(const std::string& name) { Type Parser::getSort(const std::string& name, const std::vector<Type>& params) { + checkDeclaration(name, CHECK_DECLARED, SYM_SORT); Assert( isDeclared(name, SYM_SORT) ); Type t = d_declScope->lookupType(name, params); return t; } size_t Parser::getArity(const std::string& sort_name){ + checkDeclaration(sort_name, CHECK_DECLARED, SYM_SORT); Assert( isDeclared(sort_name, SYM_SORT) ); return d_declScope->lookupArity(sort_name); } @@ -236,7 +241,7 @@ SortType Parser::mkUnresolvedType(const std::string& name) { SortConstructorType Parser::mkUnresolvedTypeConstructor(const std::string& name, size_t arity) { - SortConstructorType unresolved = mkSortConstructor(name,arity); + SortConstructorType unresolved = mkSortConstructor(name, arity); d_unresolved.insert(unresolved); return unresolved; } @@ -325,6 +330,37 @@ Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) { return types; } +DatatypeType Parser::mkRecordType(const std::vector< std::pair<std::string, Type> >& typeIds) { + DatatypeType& dtt = d_recordTypes[typeIds]; + if(dtt.isNull()) { + Datatype dt("__cvc4_record"); +Debug("datatypes") << "make new record_ctor" << std::endl; + DatatypeConstructor c("__cvc4_record_ctor"); + for(std::vector< std::pair<std::string, Type> >::const_iterator i = typeIds.begin(); i != typeIds.end(); ++i) { + c.addArg((*i).first, (*i).second); + } + dt.addConstructor(c); + dtt = d_exprManager->mkDatatypeType(dt); + } else { +Debug("datatypes") << "use old record_ctor" << std::endl; +} + return dtt; +} + +DatatypeType Parser::mkTupleType(const std::vector<Type>& types) { + DatatypeType& dtt = d_tupleTypes[types]; + if(dtt.isNull()) { + Datatype dt("__cvc4_tuple"); + DatatypeConstructor c("__cvc4_tuple_ctor"); + for(std::vector<Type>::const_iterator i = types.begin(); i != types.end(); ++i) { + c.addArg("__cvc4_tuple_stor", *i); + } + dt.addConstructor(c); + dtt = d_exprManager->mkDatatypeType(dt); + } + return dtt; +} + bool Parser::isDeclared(const std::string& name, SymbolType type) { switch(type) { case SYM_VARIABLE: diff --git a/src/parser/parser.h b/src/parser/parser.h index 70bd45c31..405e397b8 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -142,6 +142,20 @@ class CVC4_PUBLIC Parser { /** Are we only parsing? */ bool d_parseOnly; + /** + * We might see the same record type multiple times; we have + * to match always to the same Type. This map contains all the + * record types we have. + */ + std::map<std::vector< std::pair<std::string, Type> >, DatatypeType> d_recordTypes; + + /** + * We might see the same tuple type multiple times; we have + * to match always to the same Type. This map contains all the + * tuple types we have. + */ + std::map<std::vector<Type>, DatatypeType> d_tupleTypes; + /** The set of operators available in the current logic. */ std::set<Kind> d_logicOperators; @@ -399,6 +413,16 @@ public: mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes); /** + * Create a record type, or if there's already a matching one, return that one. + */ + DatatypeType mkRecordType(const std::vector< std::pair<std::string, Type> >& typeIds); + + /** + * Create a tuple type, or if there's already a matching one, return that one. + */ + DatatypeType mkTupleType(const std::vector<Type>& types); + + /** * Add an operator to the current legal set. * * @param kind the built-in operator to add @@ -494,6 +518,14 @@ public: } } + inline void useDeclarationsFrom(DeclarationScope* scope) { + d_declScope = scope; + } + + inline DeclarationScope* getDeclarationScope() const { + return d_declScope; + } + /** * Gets the current declaration level. */ diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index c17956e62..dff5b93ac 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -66,6 +66,11 @@ Parser* ParserBuilder::build() case FILE_INPUT: input = Input::newFileInput(d_lang, d_filename, d_mmap); break; + case LINE_BUFFERED_STREAM_INPUT: + AlwaysAssert( d_streamInput != NULL, + "Uninitialized stream input in ParserBuilder::build()" ); + input = Input::newStreamInput(d_lang, *d_streamInput, d_filename, true); + break; case STREAM_INPUT: AlwaysAssert( d_streamInput != NULL, "Uninitialized stream input in ParserBuilder::build()" ); @@ -155,6 +160,12 @@ ParserBuilder& ParserBuilder::withStreamInput(std::istream& input) { return *this; } +ParserBuilder& ParserBuilder::withLineBufferedStreamInput(std::istream& input) { + d_inputType = LINE_BUFFERED_STREAM_INPUT; + d_streamInput = &input; + return *this; +} + ParserBuilder& ParserBuilder::withStringInput(const std::string& input) { d_inputType = STRING_INPUT; d_stringInput = input; diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h index ce01d3c53..095769ab5 100644 --- a/src/parser/parser_builder.h +++ b/src/parser/parser_builder.h @@ -44,6 +44,7 @@ class Parser; class CVC4_PUBLIC ParserBuilder { enum InputType { FILE_INPUT, + LINE_BUFFERED_STREAM_INPUT, STREAM_INPUT, STRING_INPUT }; @@ -90,7 +91,7 @@ public: const Options& options); /** Build the parser, using the current settings. */ - Parser *build() throw (InputStreamException,AssertionException); + Parser *build() throw (InputStreamException, AssertionException); /** Should semantic checks be enabled in the parser? (Default: yes) */ ParserBuilder& withChecks(bool flag = true); @@ -150,6 +151,9 @@ public: /** Set the parser to use the given stream for its input. */ ParserBuilder& withStreamInput(std::istream& input); + /** Set the parser to use the given stream for its input. */ + ParserBuilder& withLineBufferedStreamInput(std::istream& input); + /** Set the parser to use the given string for its input. */ ParserBuilder& withStringInput(const std::string& input); };/* class ParserBuilder */ diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp index 0ee6944d4..508bfe352 100644 --- a/src/parser/smt/smt.cpp +++ b/src/parser/smt/smt.cpp @@ -41,6 +41,9 @@ std::hash_map<const std::string, Smt::Logic, CVC4::StringHashFunction> Smt::newL logicMap["QF_UFIDL"] = QF_UFIDL; logicMap["QF_UFLRA"] = QF_UFLRA; logicMap["QF_UFLIA"] = QF_UFLIA; + logicMap["QF_UFLIRA"] = QF_UFLIRA; + logicMap["QF_UFNIA"] = QF_UFNIA; + logicMap["QF_UFNIRA"] = QF_UFNIRA; logicMap["QF_AUFLIA"] = QF_AUFLIA; logicMap["QF_AUFLIRA"] = QF_AUFLIRA; return logicMap; @@ -159,6 +162,7 @@ void Smt::setLogic(const std::string& name) { case QF_UFIDL: case QF_UFLIA: + case QF_UFNIA:// nonstandard logic addTheory(THEORY_INTS); addUf(); break; @@ -169,6 +173,13 @@ void Smt::setLogic(const std::string& name) { addUf(); break; + case QF_UFLIRA:// nonstandard logic + case QF_UFNIRA:// nonstandard logic + addTheory(THEORY_INTS); + addTheory(THEORY_REALS); + addUf(); + break; + case QF_UF: addUf(); break; diff --git a/src/parser/smt/smt.h b/src/parser/smt/smt.h index a99f81998..62bb24336 100644 --- a/src/parser/smt/smt.h +++ b/src/parser/smt/smt.h @@ -54,7 +54,10 @@ public: QF_UF, QF_UFIDL, QF_UFLIA, + QF_UFNIA, // nonstandard QF_UFLRA, + QF_UFLIRA, // nonstandard + QF_UFNIRA, // nonstandard QF_UFNRA, UFNIA }; diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 791e550b9..926ce1718 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -67,7 +67,6 @@ options { #include "parser/smt2/smt2.h" #include "parser/antlr_input.h" -#include "parser/antlr_tracing.h" using namespace CVC4; using namespace CVC4::parser; @@ -79,6 +78,7 @@ using namespace CVC4::parser; @parser::includes { #include "expr/command.h" #include "parser/parser.h" +#include "parser/antlr_tracing.h" namespace CVC4 { class Expr; @@ -358,7 +358,12 @@ command returns [CVC4::Command* cmd = NULL] extendedCommand[CVC4::Command*& cmd] @declarations { std::vector<CVC4::Datatype> dts; + Type t; Expr e; + SExpr sexpr; + std::string name; + std::vector<std::string> names; + std::vector<Type> sorts; } /* Z3's extended SMT-LIBv2 set of commands syntax */ : DECLARE_DATATYPES_TOK @@ -368,33 +373,43 @@ extendedCommand[CVC4::Command*& cmd] { PARSER_STATE->popScope(); cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); } - | DECLARE_SORTS_TOK | DECLARE_FUNS_TOK + LPAREN_TOK + ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] nonemptySortList[sorts] RPAREN_TOK )+ + RPAREN_TOK | DECLARE_PREDS_TOK - | DEFINE_TOK + LPAREN_TOK + ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] sortList[sorts] RPAREN_TOK )+ + RPAREN_TOK + | DEFINE_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] term[e] | DEFINE_SORTS_TOK - | DECLARE_CONST_TOK - + LPAREN_TOK + ( LPAREN_TOK ( symbol[name,CHECK_UNDECLARED,SYM_SORT] LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK | + symbol[name,CHECK_UNDECLARED,SYM_SORT] symbol[name,CHECK_NONE,SYM_SORT] ) RPAREN_TOK RPAREN_TOK )+ + RPAREN_TOK + | DECLARE_CONST_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] sortSymbol[t,CHECK_DECLARED] + | SIMPLIFY_TOK term[e] { cmd = new SimplifyCommand(e); } | ECHO_TOK - ( STRING_LITERAL - { Message() << AntlrInput::tokenText($STRING_LITERAL) << std::endl; } + ( simpleSymbolicExpr[sexpr] + { Message() << sexpr << std::endl; } | { Message() << std::endl; } ) + { cmd = new EmptyCommand; } ; -symbolicExpr[CVC4::SExpr& sexpr] +simpleSymbolicExpr[CVC4::SExpr& sexpr] @declarations { - std::vector<SExpr> children; CVC4::Kind k; + std::string s; } : INTEGER_LITERAL { sexpr = SExpr(AntlrInput::tokenText($INTEGER_LITERAL)); } | DECIMAL_LITERAL { sexpr = SExpr(AntlrInput::tokenText($DECIMAL_LITERAL)); } - | STRING_LITERAL - { sexpr = SExpr(AntlrInput::tokenText($STRING_LITERAL)); } + | str[s] + { sexpr = SExpr(s); } | SYMBOL { sexpr = SExpr(AntlrInput::tokenText($SYMBOL)); } | builtinOp[k] @@ -404,6 +419,13 @@ symbolicExpr[CVC4::SExpr& sexpr] } | KEYWORD { sexpr = SExpr(AntlrInput::tokenText($KEYWORD)); } + ; + +symbolicExpr[CVC4::SExpr& sexpr] +@declarations { + std::vector<SExpr> children; +} + : simpleSymbolicExpr[sexpr] | LPAREN_TOK (symbolicExpr[sexpr] { children.push_back(sexpr); } )* RPAREN_TOK @@ -611,6 +633,17 @@ termList[std::vector<CVC4::Expr>& formulas, CVC4::Expr& expr] ; /** + * Matches a string, and strips off the quotes. + */ +str[std::string& s] + : STRING_LITERAL + { s = AntlrInput::tokenText($STRING_LITERAL); + /* strip off the quotes */ + s = s.substr(1, s.size() - 2); + } + ; + +/** * Matches a builtin operator symbol and sets kind to its associated Expr kind. */ builtinOp[CVC4::Kind& kind] @@ -637,6 +670,8 @@ builtinOp[CVC4::Kind& kind] | MINUS_TOK { $kind = CVC4::kind::MINUS; } | STAR_TOK { $kind = CVC4::kind::MULT; } | DIV_TOK { $kind = CVC4::kind::DIVISION; } + | INTS_DIV_TOK { $kind = CVC4::kind::INTS_DIVISION; } + | INTS_MOD_TOK { $kind = CVC4::kind::INTS_MODULUS; } | SELECT_TOK { $kind = CVC4::kind::SELECT; } | STORE_TOK { $kind = CVC4::kind::STORE; } @@ -705,6 +740,13 @@ sortList[std::vector<CVC4::Type>& sorts] : ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )* ; +nonemptySortList[std::vector<CVC4::Type>& sorts] +@declarations { + Type t; +} + : ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )+ + ; + /** * Matches a sequence of (variable,sort) symbol pairs and fills them * into the given vector. @@ -937,6 +979,9 @@ STORE_TOK : 'store'; // TILDE_TOK : '~'; XOR_TOK : 'xor'; +INTS_DIV_TOK : 'div'; +INTS_MOD_TOK : 'mod'; + CONCAT_TOK : 'concat'; BVNOT_TOK : 'bvnot'; BVAND_TOK : 'bvand'; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 7d6f27aa5..39eaf5b95 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -127,6 +127,7 @@ void Smt2::setLogic(const std::string& name) { case Smt::QF_UFIDL: case Smt::QF_UFLIA: + case Smt::QF_UFNIA:// nonstandard logic addTheory(THEORY_INTS); addOperator(kind::APPLY_UF); break; @@ -137,6 +138,13 @@ void Smt2::setLogic(const std::string& name) { addOperator(kind::APPLY_UF); break; + case Smt::QF_UFLIRA:// nonstandard logic + case Smt::QF_UFNIRA:// nonstandard logic + addOperator(kind::APPLY_UF); + addTheory(THEORY_INTS); + addTheory(THEORY_REALS); + break; + case Smt::QF_BV: addTheory(THEORY_BITVECTORS); break; |