diff options
author | Paul Meng <baolmeng@gmail.com> | 2016-10-11 13:54:20 -0500 |
---|---|---|
committer | Paul Meng <baolmeng@gmail.com> | 2016-10-11 13:54:20 -0500 |
commit | 3395c5c13cd61d98aec0d9806e3b9bc3d707968a (patch) | |
tree | 0eadad9799862ec77d29f7abe03a46c300d80de8 /src/parser | |
parent | 773e7d27d606b71ff0f78e84efe1deef2653f016 (diff) | |
parent | 5f415d4585134612bc24e9a823289fee35541a01 (diff) |
Merge branch 'origin' of https://github.com/CVC4/CVC4.git
Conflicts:
src/options/quantifiers_options
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/bounded_token_buffer.cpp | 117 | ||||
-rw-r--r-- | src/parser/memory_mapped_input_buffer.cpp | 1 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 2 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 2 |
4 files changed, 63 insertions, 59 deletions
diff --git a/src/parser/bounded_token_buffer.cpp b/src/parser/bounded_token_buffer.cpp index c89005941..31a2219b9 100644 --- a/src/parser/bounded_token_buffer.cpp +++ b/src/parser/bounded_token_buffer.cpp @@ -133,70 +133,71 @@ antlr3CommonTokenDebugStreamSourceNew(ANTLR3_UINT32 hint, pANTLR3_TOKEN_SOURCE s return stream; }*/ -pBOUNDED_TOKEN_BUFFER -BoundedTokenBufferSourceNew(ANTLR3_UINT32 k, pANTLR3_TOKEN_SOURCE source) -{ - pBOUNDED_TOKEN_BUFFER buffer; - pANTLR3_COMMON_TOKEN_STREAM stream; - - - assert( k > 0 ); +pBOUNDED_TOKEN_BUFFER BoundedTokenBufferSourceNew(ANTLR3_UINT32 k, + pANTLR3_TOKEN_SOURCE source) { + pBOUNDED_TOKEN_BUFFER buffer; + pANTLR3_COMMON_TOKEN_STREAM stream; - /* Memory for the interface structure - */ - buffer = (pBOUNDED_TOKEN_BUFFER) ANTLR3_MALLOC(sizeof(BOUNDED_TOKEN_BUFFER_struct)); + assert(k > 0); - if (buffer == NULL) - { - return NULL; - } + /* Memory for the interface structure */ + buffer = + (pBOUNDED_TOKEN_BUFFER)ANTLR3_MALLOC(sizeof(BOUNDED_TOKEN_BUFFER_struct)); - buffer->tokenBuffer = (pANTLR3_COMMON_TOKEN*) ANTLR3_MALLOC(2*k*sizeof(pANTLR3_COMMON_TOKEN)); - buffer->currentIndex = 0; - buffer->maxIndex = 0; - buffer->k = k; - buffer->bufferSize = 2*k; - buffer->empty = ANTLR3_TRUE; - buffer->done = ANTLR3_FALSE; - - stream = antlr3CommonTokenStreamSourceNew(k,source); - if (stream == NULL) - { - return NULL; - } + if (buffer == NULL) { + return NULL; + } - stream->super = buffer; - buffer->commonTstream = stream; + buffer->tokenBuffer = (pANTLR3_COMMON_TOKEN*)ANTLR3_MALLOC( + 2 * k * sizeof(pANTLR3_COMMON_TOKEN)); + if (buffer->tokenBuffer == NULL) { + ANTLR3_FREE(buffer); + return NULL; + } - /* Defaults - */ - stream->p = -1; + buffer->currentIndex = 0; + buffer->maxIndex = 0; + buffer->k = k; + buffer->bufferSize = 2 * k; + buffer->empty = ANTLR3_TRUE; + buffer->done = ANTLR3_FALSE; + + stream = antlr3CommonTokenStreamSourceNew(k, source); + if (stream == NULL) { + ANTLR3_FREE(buffer->tokenBuffer); + ANTLR3_FREE(buffer); + return NULL; + } - /* Install the token stream API - */ - stream->tstream->_LT = tokLT; - stream->tstream->get = get; - stream->tstream->getTokenSource = getTokenSource; - stream->tstream->setTokenSource = setTokenSource; - stream->tstream->toString = toString; - stream->tstream->toStringSS = toStringSS; - stream->tstream->toStringTT = toStringTT; - stream->tstream->setDebugListener = setDebugListener; - - /* Install INT_STREAM interface - */ - stream->tstream->istream->_LA = _LA; - stream->tstream->istream->mark = mark; - stream->tstream->istream->release = release; - stream->tstream->istream->size = size; - stream->tstream->istream->index = tindex; - stream->tstream->istream->rewind = rewindStream; - stream->tstream->istream->rewindLast= rewindLast; - stream->tstream->istream->seek = seek; - stream->tstream->istream->consume = consume; - stream->tstream->istream->getSourceName = getSourceName; - - return buffer; + stream->super = buffer; + buffer->commonTstream = stream; + + /* Defaults */ + stream->p = -1; + + /* Install the token stream API */ + stream->tstream->_LT = tokLT; + stream->tstream->get = get; + stream->tstream->getTokenSource = getTokenSource; + stream->tstream->setTokenSource = setTokenSource; + stream->tstream->toString = toString; + stream->tstream->toStringSS = toStringSS; + stream->tstream->toStringTT = toStringTT; + stream->tstream->setDebugListener = setDebugListener; + + /* Install INT_STREAM interface */ + stream->tstream->istream->_LA = _LA; + stream->tstream->istream->mark = mark; + stream->tstream->istream->release = release; + stream->tstream->istream->size = size; + stream->tstream->istream->index = tindex; + stream->tstream->istream->rewind = rewindStream; + stream->tstream->istream->rewindLast = rewindLast; + stream->tstream->istream->seek = seek; + stream->tstream->istream->consume = consume; + stream->tstream->istream->getSourceName = getSourceName; + + return buffer; } // Install a debug listener adn switch to debug mode methods diff --git a/src/parser/memory_mapped_input_buffer.cpp b/src/parser/memory_mapped_input_buffer.cpp index c9515aa92..1554428f7 100644 --- a/src/parser/memory_mapped_input_buffer.cpp +++ b/src/parser/memory_mapped_input_buffer.cpp @@ -110,6 +110,7 @@ static ANTLR3_UINT32 MemoryMapFile(pANTLR3_INPUT_STREAM input, input->data = mmap(0, input->sizeBuf, PROT_READ, MAP_PRIVATE, fd, 0); errno = 0; + close(fd); if(intptr_t(input->data) == -1) { return ANTLR3_ERR_NOMEM; } diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 29d3e45b6..f88b30212 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1610,7 +1610,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] } else if(f.getKind() == CVC4::kind::SEP_NIL_REF) { //We don't want the nil reference to be a constant: for instance, it could be of type Int but is not a const rational. //However, the expression has 0 children. So we convert to a SEP_NIL variable. - expr = EXPR_MANAGER->mkSepNil(type); + expr = EXPR_MANAGER->mkUniqueVar(type, kind::SEP_NIL); } else { if(f.getType() != type) { PARSER_STATE->parseError("Type ascription not satisfied."); diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 9f3c43f09..30573cdff 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -372,6 +372,8 @@ void Smt2::setLogic(std::string name) { name = "UFBV"; } else if(name == "SLIA") { name = "UFSLIA"; + } else if(name == "SAT") { + name = "UF"; } else if(name == "ALL_SUPPORTED") { //no change } else { |