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.

diff --git a/config/mkbuilddir b/config/mkbuilddir
index 1ed5eda92ea503ff1362cf08c03366b8a695e7a1..ddec670235e785bb5360037f086968ea7a3a6118 100755 (executable)
--- 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 bf74ab844eb6fb983bbdf3e304b6371f6562e5cd..99d830077f461b3d0f95268766742c48f64c578f 100644 (file)
--- 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 d8d9f4b542c01c204e5def7b73dd00ab8c08552a..b8a72dc389979643fe1ac659c5f732d76ca04f54 100644 (file)
--- 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.
    */
@@ -156,6 +164,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).
    */

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 9f4fdce898b10215b74f002640c5f5850b402b83..73901c328be495e2a0d242908e3d193d6de971fe 100644 (file)
--- 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 (file)
index 0000000..9a8435b
--- /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 38d72022754f914c8bc45fc27f76a0f3bd88ffb9..f56abb386e90dda92db8fcaa6263ede48374f559 100644 (file)
--- 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 90be7d7847904c012d30595edee5a9969470f129..5d492db324a9a0d0b799552694c4f87e5e2a7872 100644 (file)
--- 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 1109840834809d62a6a49a08251ee9e8614b0922..c951aaf2e682f7ecb2440023ab62aceb460e60bd 100644 (file)
--- 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 25245f36a2e8c530e484a748c3ecf9b2b704a1a2..55212bb079ae2e9de4ddc8edccafccd7bfca576a 100644 (file)
--- 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 614f02f0f310b54666e0dd39cdd0e6dc9161814b..9c0eaa9dbfe95046a8aba0b2b1fa7c06b193bde1 100755 (executable)
--- 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"