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.)

4 files changed, 54 insertions, 16 deletions

diff --git a/src/smt/options b/src/smt/options
index 3ee3dbecb..0dc416474 100644
--- a/src/smt/options
+++ b/src/smt/options
@@ -25,7 +25,7 @@ option expandDefinitions expand-definitions bool :default false
  always expand symbol definitions in output
 common-option produceModels produce-models -m --produce-models bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/smt_engine.h"
  support the get-value and get-model commands
-option checkModels check-models --check-models bool :link --produce-models --interactive :link-smt produce-models :link-smt interactive-mode :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
+option checkModels check-models --check-models bool :link --produce-models --produce-assertions :link-smt produce-models :link-smt produce-assertions :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
  after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions
 option dumpModels --dump-models bool :default false :link --produce-models
  output models after every SAT/INVALID/UNKNOWN response
@@ -45,10 +45,10 @@ option dumpUnsatCores --dump-unsat-cores bool :default false :link --produce-uns
 option produceAssignments produce-assignments --produce-assignments bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
  support the get-assignment command
 
-# This could go in src/main/options, but by SMT-LIBv2 spec, "interactive"
-# is a mode in which the assertion list must be kept.  So it belongs here.
-common-option interactive interactive-mode --interactive bool :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" :read-write
- force interactive mode
+undocumented-option interactiveMode interactive-mode bool :predicate CVC4::smt::beforeSearch CVC4::smt::setProduceAssertions :predicate-include "smt/options_handlers.h" :read-write
+ deprecated name for produce-assertions
+common-option produceAssertions produce-assertions --produce-assertions bool :predicate CVC4::smt::beforeSearch CVC4::smt::setProduceAssertions :predicate-include "smt/options_handlers.h" :read-write
+ keep an assertions list (enables get-assertions command)
 
 option doITESimp --ite-simp bool :read-write
  turn on ite simplification (Kim (and Somenzi) et al., SAT 2009)
@@ -93,7 +93,7 @@ common-option perCallMillisecondLimit  tlimit-per --tlimit-per=MS "unsigned long
  enable time limiting per query (give milliseconds)
 common-option cumulativeResourceLimit rlimit --rlimit=N "unsigned long"
  enable resource limiting (currently, roughly the number of SAT conflicts)
-common-option perCallResourceLimit rlimit-per --rlimit-per=N "unsigned long"
+common-option perCallResourceLimit reproducible-resource-limit --rlimit-per=N "unsigned long"
  enable resource limiting per query
 
 expert-option rewriteApplyToConst rewrite-apply-to-const --rewrite-apply-to-const bool :default false
diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h
index fcd625267..d02b88fd2 100644
--- a/src/smt/options_handlers.h
+++ b/src/smt/options_handlers.h
@@ -299,6 +299,11 @@ inline void beforeSearch(std::string option, bool value, SmtEngine* smt) throw(M
   }
 }
 
+inline void setProduceAssertions(std::string option, bool value, SmtEngine* smt) throw() {
+  options::produceAssertions.set(value);
+  options::interactiveMode.set(value);
+}
+
 // ensure we are a proof-enabled build of CVC4
 inline void proofEnabledBuild(std::string option, bool value, SmtEngine* smt) throw(OptionException) {
 #ifndef CVC4_PROOF
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 19bfe3ca5..d0a920653 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -603,7 +603,9 @@ public:
       val = d_smt.d_nodeManager->mkAbstractValue(n.getType());
       d_abstractValueMap.addSubstitution(val, n);
     }
-    return val;
+    // We are supposed to ascribe types to all abstract values that go out.
+    Node retval = d_smt.d_nodeManager->mkNode(kind::APPLY_TYPE_ASCRIPTION, d_smt.d_nodeManager->mkConst(AscriptionType(n.getType().toType())), val);
+    return retval;
   }
 
   std::hash_map<Node, Node, NodeHashFunction> rewriteApplyToConstCache;
@@ -675,6 +677,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
   d_modelCommands(NULL),
   d_dumpCommands(),
   d_logic(),
+  d_originalOptions(em->getOptions()),
   d_pendingPops(0),
   d_fullyInited(false),
   d_problemExtended(false),
@@ -737,7 +740,7 @@ void SmtEngine::finishInit() {
   // cleanup ordering issue and Nodes/TNodes.  If SAT is popped
   // first, some user-context-dependent TNodes might still exist
   // with rc == 0.
-  if(options::interactive() ||
+  if(options::produceAssertions() ||
      options::incrementalSolving()) {
     // In the case of incremental solving, we appear to need these to
     // ensure the relevant Nodes remain live.
@@ -961,9 +964,9 @@ void SmtEngine::setDefaults() {
   }
 
   if(options::checkModels()) {
-    if(! options::interactive()) {
-      Notice() << "SmtEngine: turning on interactive-mode to support check-models" << endl;
-      setOption("interactive-mode", SExpr("true"));
+    if(! options::produceAssertions()) {
+      Notice() << "SmtEngine: turning on produce-assertions to support check-models" << endl;
+      setOption("produce-assertions", SExpr("true"));
     }
   }
 
@@ -1450,8 +1453,23 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
   } else if(key == "smt-lib-version") {
     if( (value.isInteger() && value.getIntegerValue() == Integer(2)) ||
         (value.isRational() && value.getRationalValue() == Rational(2)) ||
-        (value.getValue() == "2") ) {
+        value.getValue() == "2" ||
+        value.getValue() == "2.0" ) {
       // supported SMT-LIB version
+      if(!options::outputLanguage.wasSetByUser() &&
+         options::outputLanguage() == language::output::LANG_SMTLIB_V2_5) {
+        options::outputLanguage.set(language::output::LANG_SMTLIB_V2_0);
+        *options::out() << Expr::setlanguage(language::output::LANG_SMTLIB_V2_0);
+      }
+      return;
+    } else if( (value.isRational() && value.getRationalValue() == Rational(5, 2)) ||
+               value.getValue() == "2.5" ) {
+      // supported SMT-LIB version
+      if(!options::outputLanguage.wasSetByUser() &&
+         options::outputLanguage() == language::output::LANG_SMTLIB_V2_0) {
+        options::outputLanguage.set(language::output::LANG_SMTLIB_V2_5);
+        *options::out() << Expr::setlanguage(language::output::LANG_SMTLIB_V2_5);
+      }
       return;
     }
     Warning() << "Warning: unsupported smt-lib-version: " << value << endl;
@@ -1530,6 +1548,8 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const
       throw ModalException("Can't get-info :reason-unknown when the "
                            "last result wasn't unknown!");
     }
+  } else if(key == "assertion-stack-levels") {
+    return SExpr(d_userLevels.size());
   } else if(key == "all-options") {
     // get the options, like all-statistics
     return Options::current().getOptions();
@@ -3660,6 +3680,7 @@ Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckin
 
   if(options::abstractValues() && resultNode.getType().isArray()) {
     resultNode = d_private->mkAbstractValue(resultNode);
+    Trace("smt") << "--- abstract value >> " << resultNode << endl;
   }
 
   return resultNode.toExpr();
@@ -3824,8 +3845,8 @@ Model* SmtEngine::getModel() throw(ModalException) {
 }
 
 void SmtEngine::checkModel(bool hardFailure) {
-  // --check-model implies --interactive, which enables the assertion list,
-  // so we should be ok.
+  // --check-model implies --produce-assertions, which enables the
+  // assertion list, so we should be ok.
   Assert(d_assertionList != NULL, "don't have an assertion list to check in SmtEngine::checkModel()");
 
   TimerStat::CodeTimer checkModelTimer(d_stats->d_checkModelTime);
@@ -4070,9 +4091,9 @@ vector<Expr> SmtEngine::getAssertions() throw(ModalException) {
     Dump("benchmark") << GetAssertionsCommand();
   }
   Trace("smt") << "SMT getAssertions()" << endl;
-  if(!options::interactive()) {
+  if(!options::produceAssertions()) {
     const char* msg =
-      "Cannot query the current assertion list when not in interactive mode.";
+      "Cannot query the current assertion list when not in produce-assertions mode.";
     throw ModalException(msg);
   }
   Assert(d_assertionList != NULL);
@@ -4196,13 +4217,20 @@ void SmtEngine::reset() throw() {
   if(Dump.isOn("benchmark")) {
     Dump("benchmark") << ResetCommand();
   }
+  Options opts = d_originalOptions;
   this->~SmtEngine();
+  NodeManager::fromExprManager(em)->getOptions() = opts;
   new(this) SmtEngine(em);
 }
 
 void SmtEngine::resetAssertions() throw() {
   SmtScope smts(this);
 
+  Trace("smt") << "SMT resetAssertions()" << endl;
+  if(Dump.isOn("benchmark")) {
+    Dump("benchmark") << ResetAssertionsCommand();
+  }
+
   while(!d_userLevels.empty()) {
     pop();
   }
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 30f84346a..489d34d79 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -190,6 +190,11 @@ class CVC4_PUBLIC SmtEngine {
   LogicInfo d_logic;
 
   /**
+   * Keep a copy of the original option settings (for reset()).
+   */
+  Options d_originalOptions;
+
+  /**
    * Number of internal pops that have been deferred.
    */
   unsigned d_pendingPops;