Partial merge from kind-backend branch, including Minisat and CNF work to

support incrementality.

Some clean-up work will likely follow, but the CNF/Minisat stuff should be
left pretty much untouched.

Expected performance change negligible; slightly better on memory:
  http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3705&reference_id=3697&mode=&category=&p=5
Note that there are crashes, but that these are exhibited in the nightly
regression run too!

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 = &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;