Parsing and infrastructure support for SMT-LIBv2.5 input and output languages.

* support for new commands meta-info, declare-const, echo, get-model,
  reset, and reset-assertions
* support for set-option :global-declarations
* support for set-option :produce-assertions
* support for set-option :reproducible-resource-limit
* support for get-info :assertion-stack-levels
* support for set-info :smt-lib-version 2.5
* ascribe types for abstract values (the new 2.5 standard clarifies that
  this is required)
* SMT-LIB v2.5 string literals (we still support 2.0 string literals when
  in 2.0 mode)

What's still to do:
* check-sat-assumptions/get-unsat-assumptions (still being hotly debated).
  Also set-option :produce-unsat-assumptions.
* define-fun-rec doesn't allow mutual recursion
* All options should be restored to defaults with (reset) command.
  (Currently :incremental and maybe others get "stuck" due to late driver
  integration.)

1 files changed, 10 insertions, 2 deletions

diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp
index c1e177dc4..22c2fd9a7 100644
--- a/src/parser/smt2/smt2_input.cpp
+++ b/src/parser/smt2/smt2_input.cpp
@@ -29,8 +29,9 @@ namespace CVC4 {
 namespace parser {
 
 /* Use lookahead=2 */
-Smt2Input::Smt2Input(AntlrInputStream& inputStream) :
+Smt2Input::Smt2Input(AntlrInputStream& inputStream, InputLanguage lang) :
   AntlrInput(inputStream, 2) {
+
   pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream();
   assert( input != NULL );
 
@@ -50,14 +51,21 @@ Smt2Input::Smt2Input(AntlrInputStream& inputStream) :
   }
 
   setAntlr3Parser(d_pSmt2Parser->pParser);
-}
 
+  setLanguage(lang);
+}
 
 Smt2Input::~Smt2Input() {
   d_pSmt2Lexer->free(d_pSmt2Lexer);
   d_pSmt2Parser->free(d_pSmt2Parser);
 }
 
+void Smt2Input::setLanguage(InputLanguage lang) {
+  CheckArgument(lang == language::input::LANG_SMTLIB_V2_0 ||
+                lang == language::input::LANG_SMTLIB_V2_5, lang);
+  d_lang = lang;
+}
+
 Command* Smt2Input::parseCommand() {
   return d_pSmt2Parser->parseCommand(d_pSmt2Parser);
 }