diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-10-13 04:14:38 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-10-13 04:14:38 +0000 |
commit | 3cbb76ef86a769cfe3dac5976a14e1bc43c42ca6 (patch) | |
tree | e08efdc63abd663de4f5750db9326b69c79829e5 /src/theory | |
parent | 3a7aafccadbfa1543c435b7dfe4f53116224a11f (diff) |
Interruption, time-out, and deterministic time-out ("resource-out") features.
Details here: http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_October_14,_2011#Resource.2Ftime_limiting_API
This will need more work, but it's a start.
Also implemented TheoryEngine::properPropagation().
Other minor things.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_core.h | 2 | ||||
-rw-r--r-- | src/theory/output_channel.h | 14 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 38 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 14 |
4 files changed, 59 insertions, 9 deletions
diff --git a/src/theory/bv/theory_bv_rewrite_rules_core.h b/src/theory/bv/theory_bv_rewrite_rules_core.h index 941b9d0b4..851a6893c 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_core.h +++ b/src/theory/bv/theory_bv_rewrite_rules_core.h @@ -277,7 +277,7 @@ bool RewriteRule<ReflexivityEq>::applies(Node node) { template<> Node RewriteRule<ReflexivityEq>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<ReflexivityEq>(" << node << ")" << std::endl; - return node[1].eqNode(node[0]);; + return node[1].eqNode(node[0]); } } diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index f5bf620bf..625abc580 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -105,6 +105,20 @@ public: */ virtual void setIncomplete() throw(AssertionException) = 0; + /** + * "Spend" a "resource." The meaning is specific to the context in + * which the theory is operating, and may even be ignored. The + * intended meaning is that if the user has set a limit on the "units + * of resource" that can be expended in a search, and that limit is + * exceeded, then the search is terminated. Note that the check for + * termination occurs in the main search loop, so while theories + * should call OutputChannel::spendResource() during particularly + * long-running operations, they cannot rely on resource() to break + * out of infinite or intractable computations. + */ + virtual void spendResource() throw() { + } + };/* class OutputChannel */ }/* CVC4::theory namespace */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 2d4672776..2cd3f4d72 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -100,6 +100,8 @@ void TheoryEngine::preRegister(TNode preprocessed) { */ void TheoryEngine::check(Theory::Effort effort) { + d_propEngine->checkTime(); + #ifdef CVC4_FOR_EACH_THEORY_STATEMENT #undef CVC4_FOR_EACH_THEORY_STATEMENT #endif @@ -263,20 +265,38 @@ bool TheoryEngine::properConflict(TNode conflict) const { bool value; if (conflict.getKind() == kind::AND) { for (unsigned i = 0; i < conflict.getNumChildren(); ++ i) { - if (!getPropEngine()->hasValue(conflict[i], value)) return false; - if (!value) return false; + if (! getPropEngine()->hasValue(conflict[i], value)) { + Debug("properConflict") << "Bad conflict is due to unassigned atom: " + << conflict[i] << endl; + return false; + } + if (! value) { + Debug("properConflict") << "Bad conflict is due to false atom: " + << conflict[i] << endl; + return false; + } } } else { - if (!getPropEngine()->hasValue(conflict, value)) return false; - return value; + if (! getPropEngine()->hasValue(conflict, value)) { + Debug("properConflict") << "Bad conflict is due to unassigned atom: " + << conflict << endl; + return false; + } + if(! value) { + Debug("properConflict") << "Bad conflict is due to false atom: " + << conflict << endl; + return false; + } } return true; } bool TheoryEngine::properPropagation(TNode lit) const { - Assert(!lit.isNull()); -#warning implement TheoryEngine::properPropagation() - return true; + if(!getPropEngine()->isTranslatedSatLiteral(lit)) { + return false; + } + bool b; + return !getPropEngine()->hasValue(lit, b); } bool TheoryEngine::properExplanation(TNode node, TNode expl) const { @@ -471,6 +491,8 @@ void TheoryEngine::assertFact(TNode node) { Trace("theory") << "TheoryEngine::assertFact(" << node << ")" << std::endl; + d_propEngine->checkTime(); + // Get the atom TNode atom = node.getKind() == kind::NOT ? node[0] : node; @@ -497,6 +519,8 @@ void TheoryEngine::assertFact(TNode node) void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { Debug("theory") << "EngineOutputChannel::propagate(" << literal << ")" << std::endl; + + d_propEngine->checkTime(); if(Dump.isOn("t-propagations")) { Dump("t-propagations") << CommentCommand("negation of theory propagation: expect valid") << std::endl diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 915373074..be3068a45 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -209,6 +209,11 @@ class TheoryEngine { void setIncomplete() throw(AssertionException) { d_engine->setIncomplete(d_theory); } + + void spendResource() throw() { + d_engine->spendResource(); + } + };/* class EngineOutputChannel */ /** @@ -223,7 +228,7 @@ class TheoryEngine { void conflict(TNode conflict) { - Assert(properConflict(conflict)); + Assert(properConflict(conflict), "not a proper conflict: %s", conflict.toString().c_str()); // Mark that we are in conflict d_inConflict = true; @@ -257,6 +262,13 @@ class TheoryEngine { } /** + * "Spend" a resource during a search or preprocessing. + */ + void spendResource() throw() { + d_propEngine->spendResource(); + } + + /** * Is the theory active. */ bool isActive(theory::TheoryId theory) { |