diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-11-16 19:18:19 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-11-16 19:18:19 +0000 |
commit | e66924cb0f425ca70969058532340e68c9c17a54 (patch) | |
tree | 6dfdb2d02621c45a17b9ca3202cc3db7c30d7da5 /src/smt | |
parent | d5d504da7c73538642b9be86c73f8407e08ab57a (diff) |
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.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 23 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 19 |
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; |