From 3d97646be5eb3f2b50028875f4d899698228e8c7 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 12 Oct 2010 21:10:36 +0000 Subject: [PATCH] hooked up "we are incomplete" flag after conversation with Tim (a theory notifies the theory engine through its output channel); some cleanup; add a regression for bug #216 --- src/prop/prop_engine.cpp | 10 ++++--- src/smt/smt_engine.cpp | 6 +++- src/theory/output_channel.h | 28 +++++++++++++----- src/theory/theory_engine.cpp | 1 + src/theory/theory_engine.h | 36 +++++++++++++++++++---- test/regress/regress0/bug216.smt2 | 8 +++++ test/unit/expr/node_self_iterator_black.h | 1 + test/unit/theory/theory_black.h | 20 +++++++++---- test/unit/theory/theory_engine_white.h | 3 ++ 9 files changed, 90 insertions(+), 23 deletions(-) create mode 100644 test/regress/regress0/bug216.smt2 diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index de60b5f7d..d7b1e6d99 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -58,13 +58,12 @@ public: }; PropEngine::PropEngine(const Options* opts, DecisionEngine* de, - TheoryEngine* te, Context* context) -: d_inCheckSat(false), + TheoryEngine* te, Context* context) : + d_inCheckSat(false), d_options(opts), d_decisionEngine(de), d_theoryEngine(te), - d_context(context) -{ + d_context(context) { Debug("prop") << "Constructing the PropEngine" << endl; d_satSolver = new SatSolver(this, d_theoryEngine, d_context, d_options); d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver); @@ -129,6 +128,9 @@ Result PropEngine::checkSat() { Debug("prop") << "PropEngine::checkSat() => " << (result ? "true" : "false") << endl; + if(result && d_theoryEngine->isIncomplete()) { + return Result(Result::SAT_UNKNOWN, Result::INCOMPLETE); + } return Result(result ? Result::SAT : Result::UNSAT); } diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index e3c8c584c..2f2fba848 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -530,7 +530,7 @@ bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) { n.getMetaKind() == kind::metakind::VARIABLE ), e, "expected variable or defined-function application " "in addToAssignment(),\ngot %s", e.toString().c_str() ); - if(!d_options->interactive || !d_options->produceAssignments) { + if(!d_options->produceAssignments) { return false; } if(d_assignments == NULL) { @@ -557,6 +557,10 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) { throw ModalException(msg); } + if(d_assignments == NULL) { + return SExpr(); + } + NodeManagerScope nms(d_nodeManager); vector sexprs; TypeNode boolType = d_nodeManager->booleanType(); diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index cdc1e1cc2..cc51c7a7c 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -76,7 +76,8 @@ public: * * @param safe - whether it is safe to be interrupted */ - virtual void conflict(TNode n, bool safe = false) throw(Interrupted, AssertionException) = 0; + virtual void conflict(TNode n, bool safe = false) + throw(Interrupted, AssertionException) = 0; /** * Propagate a theory literal. @@ -85,7 +86,8 @@ public: * * @param safe - whether it is safe to be interrupted */ - virtual void propagate(TNode n, bool safe = false) throw(Interrupted, AssertionException) = 0; + virtual void propagate(TNode n, bool safe = false) + throw(Interrupted, AssertionException) = 0; /** * Tell the core that a valid theory lemma at decision level 0 has @@ -94,16 +96,19 @@ public: * @param n - a theory lemma valid at decision level 0 * @param safe - whether it is safe to be interrupted */ - virtual void lemma(TNode n, bool safe = false) throw(Interrupted, AssertionException) = 0; + virtual void lemma(TNode n, bool safe = false) + throw(Interrupted, AssertionException) = 0; /** - * Tell the core to add the following valid lemma as if it were a user assertion. - * This should NOT be called during solving, only preprocessing. + * Tell the core to add the following valid lemma as if it were a + * user assertion. This should NOT be called during solving, only + * preprocessing. * * @param n - a theory lemma valid to be asserted * @param safe - whether it is safe to be interrupted */ - virtual void augmentingLemma(TNode n, bool safe = false) throw(Interrupted, AssertionException) = 0; + virtual void augmentingLemma(TNode n, bool safe = false) + throw(Interrupted, AssertionException) = 0; /** * Provide an explanation in response to an explanation request. @@ -111,7 +116,16 @@ public: * @param n - an explanation * @param safe - whether it is safe to be interrupted */ - virtual void explanation(TNode n, bool safe = false) throw(Interrupted, AssertionException) = 0; + virtual void explanation(TNode n, bool safe = false) + throw(Interrupted, AssertionException) = 0; + + /** + * Notification from a theory that it realizes it is incomplete at + * this context level. If SAT is later determined by the + * TheoryEngine, it should actually return an UNKNOWN result. + */ + virtual void setIncomplete() + throw(Interrupted, AssertionException) = 0; };/* class OutputChannel */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 29aed8426..4113466d7 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -130,6 +130,7 @@ TheoryEngine::TheoryEngine(context::Context* ctxt, const Options* opts) : d_propEngine(NULL), d_theoryOut(this, ctxt), d_hasShutDown(false), + d_incomplete(ctxt, false), d_statistics() { d_sharedTermManager = new SharedTermManager(this, ctxt); diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 85e6d2cfc..ca39001fe 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -83,8 +83,10 @@ class TheoryEngine { void newFact(TNode n); - void conflict(TNode conflictNode, bool safe) throw(theory::Interrupted, AssertionException) { - Debug("theory") << "EngineOutputChannel::conflict(" << conflictNode << ")" << std::endl; + void conflict(TNode conflictNode, bool safe) + throw(theory::Interrupted, AssertionException) { + Debug("theory") << "EngineOutputChannel::conflict(" + << conflictNode << ")" << std::endl; d_conflictNode = conflictNode; ++(d_engine->d_statistics.d_statConflicts); if(safe) { @@ -92,23 +94,32 @@ class TheoryEngine { } } - void propagate(TNode lit, bool) throw(theory::Interrupted, AssertionException) { + void propagate(TNode lit, bool) + throw(theory::Interrupted, AssertionException) { d_propagatedLiterals.push_back(lit); ++(d_engine->d_statistics.d_statPropagate); } - void lemma(TNode node, bool) throw(theory::Interrupted, AssertionException) { + void lemma(TNode node, bool) + throw(theory::Interrupted, AssertionException) { ++(d_engine->d_statistics.d_statLemma); d_engine->newLemma(node); } - void augmentingLemma(TNode node, bool) throw(theory::Interrupted, AssertionException) { + void augmentingLemma(TNode node, bool) + throw(theory::Interrupted, AssertionException) { ++(d_engine->d_statistics.d_statAugLemma); d_engine->newAugmentingLemma(node); } - void explanation(TNode explanationNode, bool) throw(theory::Interrupted, AssertionException) { + void explanation(TNode explanationNode, bool) + throw(theory::Interrupted, AssertionException) { d_explanationNode = explanationNode; ++(d_engine->d_statistics.d_statExplanation); } + + void setIncomplete() + throw(theory::Interrupted, AssertionException) { + d_engine->d_incomplete = true; + } };/* class EngineOutputChannel */ EngineOutputChannel d_theoryOut; @@ -129,6 +140,12 @@ class TheoryEngine { */ bool d_hasShutDown; + /** + * True if a theory has notified us of incompleteness (at this + * context level or below). + */ + context::CDO d_incomplete; + /** * Check whether a node is in the pre-rewrite cache or not. */ @@ -205,6 +222,13 @@ public: d_propEngine = propEngine; } + /** + * Return whether or not we are incomplete (in the current context). + */ + bool isIncomplete() { + return d_incomplete; + } + /** * This is called at shutdown time by the SmtEngine, just before * destruction. It is important because there are destruction diff --git a/test/regress/regress0/bug216.smt2 b/test/regress/regress0/bug216.smt2 new file mode 100644 index 000000000..78e0f716c --- /dev/null +++ b/test/regress/regress0/bug216.smt2 @@ -0,0 +1,8 @@ +(set-logic QF_UF) +(declare-fun x () Bool) +(declare-fun y () Bool) +(assert (=> x y)) +(check-sat) ; returns sat +(assert (=> y x)) +(assert (and x (not y))) +(check-sat) ; returns sat --> ERROR diff --git a/test/unit/expr/node_self_iterator_black.h b/test/unit/expr/node_self_iterator_black.h index 5627a9db5..4e7c198ee 100644 --- a/test/unit/expr/node_self_iterator_black.h +++ b/test/unit/expr/node_self_iterator_black.h @@ -71,6 +71,7 @@ public: TS_ASSERT(j == NodeSelfIterator::selfEnd(x_and_y)); TS_ASSERT(i == x_and_y.end()); TS_ASSERT(j == x_and_y.end()); + i = x_and_y.begin(); TS_ASSERT(i != x_and_y.end()); TS_ASSERT(*i == x); diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index 57ce0c78e..f0da885c7 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -52,25 +52,35 @@ public: void safePoint() throw(Interrupted, AssertionException) {} - void conflict(TNode n, bool safe = false) throw(Interrupted, AssertionException) { + void conflict(TNode n, bool safe = false) + throw(Interrupted, AssertionException) { push(CONFLICT, n); } - void propagate(TNode n, bool safe = false) throw(Interrupted, AssertionException) { + void propagate(TNode n, bool safe = false) + throw(Interrupted, AssertionException) { push(PROPAGATE, n); } - void lemma(TNode n, bool safe = false) throw(Interrupted, AssertionException){ + void lemma(TNode n, bool safe = false) + throw(Interrupted, AssertionException) { push(LEMMA, n); } - void augmentingLemma(TNode n, bool safe = false) throw(Interrupted, AssertionException){ + void augmentingLemma(TNode n, bool safe = false) + throw(Interrupted, AssertionException) { Unreachable(); } - void explanation(TNode n, bool safe = false) throw(Interrupted, AssertionException) { + void explanation(TNode n, bool safe = false) + throw(Interrupted, AssertionException) { push(EXPLANATION, n); } + void setIncomplete() + throw(Interrupted, AssertionException) { + Unreachable(); + } + void clear() { d_callHistory.clear(); } diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index 965857684..6adbba207 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -62,6 +62,9 @@ class FakeOutputChannel : public OutputChannel { void explanation(TNode n, bool safe) throw(AssertionException) { Unimplemented(); } + void setIncomplete() throw(AssertionException) { + Unimplemented() + } };/* class FakeOutputChannel */ class FakeTheory; -- 2.30.2