SmtEngine now fails with a ModalException if --incremental is not enabled

but a push/pop or multiple query is attempted (previously it could give
incorrect answers)

Also, fix some multi-query and push-pop tests that had wrong answers, and
support a new "% COMMAND-LINE: " gesture in regression tests so that a
test can pass additional, specific command line flags it wants to run
with (here, --incremental).

Also fix mkbuilddir script for when it's called from contrib/switch-config.

2 files changed, 38 insertions, 4 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index bf74ab844..99d830077 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -146,11 +146,14 @@ void SmtEngine::init(const Options& opts) throw() {
 
   d_assignments = NULL;
   d_haveAdditions = false;
+  d_queryMade = false;
 
   d_typeChecking = opts.typeChecking;
   d_lazyDefinitionExpansion = opts.lazyDefinitionExpansion;
   d_produceModels = opts.produceModels;
   d_produceAssignments = opts.produceAssignments;
+
+  d_incrementalSolving = opts.incrementalSolving;
 }
 
 void SmtEngine::shutdown() {
@@ -456,6 +459,12 @@ Result SmtEngine::checkSat(const BoolExpr& e) {
   Assert(e.getExprManager() == d_exprManager);
   NodeManagerScope nms(d_nodeManager);
   Debug("smt") << "SMT checkSat(" << e << ")" << endl;
+  if(d_queryMade && !d_incrementalSolving) {
+    throw ModalException("Cannot make multiple queries unless "
+                         "incremental solving is enabled "
+                         "(try --incremental)");
+  }
+  d_queryMade = true;
   ensureBoolean(e);// ensure expr is type-checked at this point
   internalPush();
   SmtEnginePrivate::addFormula(*this, e.getNode());
@@ -471,6 +480,12 @@ Result SmtEngine::query(const BoolExpr& e) {
   Assert(e.getExprManager() == d_exprManager);
   NodeManagerScope nms(d_nodeManager);
   Debug("smt") << "SMT query(" << e << ")" << endl;
+  if(d_queryMade && !d_incrementalSolving) {
+    throw ModalException("Cannot make multiple queries unless "
+                         "incremental solving is enabled "
+                         "(try --incremental)");
+  }
+  d_queryMade = true;
   ensureBoolean(e);// ensure expr is type-checked at this point
   internalPush();
   SmtEnginePrivate::addFormula(*this, e.getNode().notNode());
@@ -633,6 +648,9 @@ vector<Expr> SmtEngine::getAssertions()
 void SmtEngine::push() {
   NodeManagerScope nms(d_nodeManager);
   Debug("smt") << "SMT push()" << endl;
+  if(!d_incrementalSolving) {
+    throw ModalException("Cannot push when not solving incrementally (use --incremental)");
+  }
   d_userLevels.push_back(d_userContext->getLevel());
   internalPush();
   Debug("userpushpop") << "SmtEngine: pushed to level "
@@ -642,7 +660,10 @@ void SmtEngine::push() {
 void SmtEngine::pop() {
   NodeManagerScope nms(d_nodeManager);
   Debug("smt") << "SMT pop()" << endl;
-  Assert(d_userLevels.size() > 0 && d_userLevels.back() < d_userContext->getLevel());
+  if(!d_incrementalSolving) {
+    throw ModalException("Cannot pop when not solving incrementally (use --incremental)");
+  }
+  AlwaysAssert(d_userLevels.size() > 0 && d_userLevels.back() < d_userContext->getLevel());
   while (d_userLevels.back() < d_userContext->getLevel()) {
     internalPop();
   }
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index d8d9f4b54..b8a72dc38 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -125,12 +125,20 @@ class CVC4_PUBLIC SmtEngine {
   std::string d_logic;
 
   /**
-   * Whether or not we have added any
-   * assertions/declarations/definitions since the last checkSat/query
-   * (and therefore we're not responsible for an assignment).
+   * Whether or not we have added any assertions/declarations/definitions
+   * since the last checkSat/query (and therefore we're not responsible
+   * for an assignment).
    */
   bool d_haveAdditions;
 
+  /**
+   * Whether or not a query() or checkSat() has already been made through
+   * this SmtEngine.  If true, and d_incrementalSolving is false, then
+   * attempting an additional query() or checkSat() will fail with a
+   * ModalException.
+   */
+  bool d_queryMade;
+
   /** 
    * Whether or not to type check input expressions.
    */
@@ -157,6 +165,11 @@ class CVC4_PUBLIC SmtEngine {
   bool d_produceAssignments;
 
   /**
+   * Whether multiple queries can be made, and also push/pop is enabled.
+   */
+  bool d_incrementalSolving;
+
+  /**
    * Most recent result of last checkSat/query or (set-info :status).
    */
   Result d_status;