From e66924cb0f425ca70969058532340e68c9c17a54 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 16 Nov 2010 19:18:19 +0000 Subject: [PATCH] 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. --- config/mkbuilddir | 8 ++++---- src/smt/smt_engine.cpp | 23 +++++++++++++++++++++- src/smt/smt_engine.h | 19 +++++++++++++++--- test/regress/regress0/Makefile.am | 18 +++++++++-------- test/regress/regress0/bug216.smt2.expect | 4 ++++ test/regress/regress0/push-pop/test.00.cvc | 5 +++-- test/regress/regress0/push-pop/test.01.cvc | 2 ++ test/regress/regress0/queries0.cvc | 1 + test/regress/regress0/test12.cvc | 1 + test/regress/run_regression | 22 ++++++++++++++------- 10 files changed, 78 insertions(+), 25 deletions(-) create mode 100644 test/regress/regress0/bug216.smt2.expect 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 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. */ @@ -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 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" -- 2.30.2