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.

10 files changed, 78 insertions, 25 deletions

diff --git a/config/mkbuilddir b/config/mkbuilddir
index 1ed5eda92..ddec67023 100755
--- a/config/mkbuilddir
+++ b/config/mkbuilddir
@@ -21,10 +21,10 @@ fi
 target=$1
 build_type=$2
 
-: {$as_echo:=echo}
-: {$RM:=rm -f}
-: {$MKDIR_P:=mkdir -p}
-: {LN_S:=ln -s}
+: ${as_echo:=echo}
+: ${RM:=rm -f}
+: ${MKDIR_P:=mkdir -p}
+: ${LN_S:=ln -s}
 
 $as_echo "Setting up builds/$target/$build_type..."
 $RM config.log config.status confdefs.h builds/Makefile
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;
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 9f4fdce89..73901c328 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -22,8 +22,8 @@ SMT_TESTS = \
 	let2.smt \
 	simple.smt \
 	simple2.smt \
-        simple-lra.smt \
-        simple-rdl.smt \
+	simple-lra.smt \
+	simple-rdl.smt \
 	simple-uf.smt
 
 # Regression tests for SMT2 inputs
@@ -31,16 +31,16 @@ SMT2_TESTS = \
 	ite2.smt2 \
 	ite3.smt2 \
 	ite4.smt2 \
-        simple-lra.smt2 \
-        simple-rdl.smt2 \
-        simple-rdl-definefun.smt2 \
+	simple-lra.smt2 \
+	simple-rdl.smt2 \
+	simple-rdl-definefun.smt2 \
 	simple-uf.smt2
 
 # Regression tests for PL inputs
 CVC_TESTS = \
 	boolean-prec.cvc \
 	hole6.cvc \
-        ite.cvc \
+	ite.cvc \
 	logops.01.cvc \
 	logops.02.cvc \
 	logops.03.cvc \
@@ -48,8 +48,8 @@ CVC_TESTS = \
 	logops.05.cvc \
 	simple.cvc \
 	smallcnf.cvc \
-	test11.cvc \
 	test9.cvc \
+	test11.cvc \
 	uf20-03.cvc \
 	wiki.01.cvc \
 	wiki.02.cvc \
@@ -83,11 +83,13 @@ BUG_TESTS = \
 	bug167.smt \
 	bug168.smt \
 	bug187.smt2 \
+	bug216.smt2 \
 	bug220.smt2
 
 TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
 
-EXTRA_DIST = $(TESTS)
+EXTRA_DIST = $(TESTS) \
+	bug216.smt2.expect
 
 if CVC4_BUILD_PROFILE_COMPETITION
 else
diff --git a/test/regress/regress0/bug216.smt2.expect b/test/regress/regress0/bug216.smt2.expect
new file mode 100644
index 000000000..9a8435b2d
--- /dev/null
+++ b/test/regress/regress0/bug216.smt2.expect
@@ -0,0 +1,4 @@
+% COMMAND-LINE: --incremental
+% EXPECT: sat
+% EXPECT: unsat
+% EXIT: 20
diff --git a/test/regress/regress0/push-pop/test.00.cvc b/test/regress/regress0/push-pop/test.00.cvc
index 38d720227..f56abb386 100644
--- a/test/regress/regress0/push-pop/test.00.cvc
+++ b/test/regress/regress0/push-pop/test.00.cvc
@@ -1,3 +1,4 @@
+% COMMAND-LINE: --incremental
 x: BOOLEAN;
 
 PUSH;
@@ -6,6 +7,6 @@ ASSERT x;
 CHECKSAT;
 POP;
 ASSERT (NOT x);
-% EXPECT: unsat
+% EXPECT: sat
 CHECKSAT;
-% EXIT: 20
+% EXIT: 10
diff --git a/test/regress/regress0/push-pop/test.01.cvc b/test/regress/regress0/push-pop/test.01.cvc
index 90be7d784..5d492db32 100644
--- a/test/regress/regress0/push-pop/test.01.cvc
+++ b/test/regress/regress0/push-pop/test.01.cvc
@@ -1,3 +1,5 @@
+% COMMAND-LINE: --incremental
+
 x, y: BOOLEAN;
 
 ASSERT (x OR y);
diff --git a/test/regress/regress0/queries0.cvc b/test/regress/regress0/queries0.cvc
index 110984083..c951aaf2e 100644
--- a/test/regress/regress0/queries0.cvc
+++ b/test/regress/regress0/queries0.cvc
@@ -1,4 +1,5 @@
 % Tests the invariants for multiple queries.
+% COMMAND-LINE: --incremental
 
 a, b: BOOLEAN;
 
diff --git a/test/regress/regress0/test12.cvc b/test/regress/regress0/test12.cvc
index 25245f36a..55212bb07 100644
--- a/test/regress/regress0/test12.cvc
+++ b/test/regress/regress0/test12.cvc
@@ -1,3 +1,4 @@
+% COMMAND-LINE: --incremental
 % EXPECT: invalid
 % EXPECT: invalid
 % EXPECT: invalid
diff --git a/test/regress/run_regression b/test/regress/run_regression
index 614f02f0f..9c0eaa9db 100755
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -38,15 +38,17 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then
     expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'`
     expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark.expect" | sed 's,^% EXPECT-ERROR: ,,'`
     expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark.expect" | sed 's,^% EXIT: ,,'`
+    command_line=`grep '^% COMMAND-LINE: ' "$benchmark.expect" | sed 's,^% COMMAND-LINE: ,,'`
     if [ -z "$expected_exit_status" ]; then
       error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture"
     fi
-  elif grep -q '^% \(EXPECT\|EXPECT-ERROR\|EXIT\): ' "$benchmark" "$benchmark"; then
+  elif grep -q '^% \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark"; then
     expected_output=`grep '^% EXPECT: ' "$benchmark" | sed 's,^% EXPECT: ,,'`
     expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'`
     expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | sed 's,^% EXIT: ,,'`
+    command_line=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'`
     tmpbenchmark=`mktemp -t cvc4_benchmark.XXXXXXXXXX`.smt
-    grep -v '^% \(EXPECT\|EXPECT-ERROR\|EXIT\): ' "$benchmark" >"$tmpbenchmark"
+    grep -v '^% \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" >"$tmpbenchmark"
     if [ -z "$expected_exit_status" ]; then
       error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture"
     fi
@@ -54,9 +56,11 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then
   elif grep '^ *:status  *sat' "$benchmark" &>/dev/null; then
     expected_output=sat
     expected_exit_status=10
+    command_line=
   elif grep '^ *:status  *unsat' "$benchmark" &>/dev/null; then
     expected_output=unsat
     expected_exit_status=20
+    command_line=
   else
     error "cannot determine status of \`$benchmark'"
   fi
@@ -65,16 +69,17 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then
     expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'`
     expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark.expect" | sed 's,^% EXPECT-ERROR: ,,'`
     expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark.expect" | sed 's,^% EXIT: ,,'`
+    command_line=`grep '^% COMMAND-LINE: ' "$benchmark.expect" | sed 's,^% COMMAND-LINE: ,,'`
     if [ -z "$expected_exit_status" ]; then
       error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture"
     fi
-    benchmark=$tmpbenchmark
-  elif grep -q '^% \(EXPECT\|EXPECT-ERROR\|EXIT\): ' "$benchmark" "$benchmark"; then
+  elif grep -q '^% \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark"; then
     expected_output=`grep '^% EXPECT: ' "$benchmark" | sed 's,^% EXPECT: ,,'`
     expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'`
     expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | sed 's,^% EXIT: ,,'`
+    command_line=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'`
     tmpbenchmark=`mktemp -t cvc4_benchmark.XXXXXXXXXX`.smt2
-    grep -v '^% \(EXPECT\|EXPECT-ERROR\|EXIT\): ' "$benchmark" >"$tmpbenchmark"
+    grep -v '^% \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" >"$tmpbenchmark"
     if [ -z "$expected_exit_status" ]; then
       error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture"
     fi
@@ -82,9 +87,11 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then
   elif grep '^ *(set-info  *:status  *sat' "$benchmark" &>/dev/null; then
     expected_output=sat
     expected_exit_status=10
+    command_line=
   elif grep '^ *(set-info  *:status  *unsat' "$benchmark" &>/dev/null; then
     expected_output=unsat
     expected_exit_status=20
+    command_line=
   else
     error "cannot determine status of \`$benchmark'"
   fi
@@ -99,6 +106,7 @@ elif expr "$benchmark" : '.*\.cvc$' &>/dev/null; then
   if [ -z "$expected_exit_status" ]; then
     error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture"
   fi
+  command_line=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'`
 else
   error "benchmark \`$benchmark' must be *.cvc or *.smt or *.smt2"
 fi
@@ -130,9 +138,9 @@ if [ -z "$cvc4dirfull" ]; then
 fi
 cvc4base=`basename "$cvc4"`
 cvc4full="$cvc4dirfull/$cvc4base"
-echo  running $cvc4full `basename "$benchmark"` from `dirname "$benchmark"`
+echo running $cvc4full $CVC4_REGRESSION_ARGS $command_line --segv-nospin `basename "$benchmark"` [from working dir `dirname "$benchmark"`]
 ( cd `dirname "$benchmark"`;
-  "$cvc4full" $CVC4_REGRESSION_ARGS --segv-nospin `basename "$benchmark"`;
+  "$cvc4full" $CVC4_REGRESSION_ARGS $command_line --segv-nospin `basename "$benchmark"`;
   echo $? >"$exitstatusfile"
 ) > "$outfile" 2> "$errfile"