Resource spending support in theories (and especially in quantifiers).

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index a02e40e32426657c9ea766797f2bd64839e9dff8..1572dfa88d1569839e054bd5123b16dd203a7df5 100644 (file)
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -284,7 +284,7 @@ void PropEngine::interrupt() throw(ModalException) {
 }
 
 void PropEngine::spendResource() throw() {
-  // TODO implement me
+  d_satSolver->spendResource();
   checkTime();
 }
 

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 23b3ac50a2db404cb95ea7215176e50732266a6c..4855083a894577bdf4685e2573dbe6589338ca0e 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -577,6 +577,9 @@ bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, b
 }
 
 bool QuantifiersEngine::addLemma( Node lem, bool doCache ){
+  // For resource-limiting (also does a time check).
+  getOutputChannel().spendResource();
+
   if( doCache ){
     Debug("inst-engine-debug") << "Adding lemma : " << lem << std::endl;
     lem = Rewriter::rewrite(lem);

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 19409faf7afdadac38916f9fdbc22505875db67b..073f2ab944ade658ce99b4fe512e250a97840baa 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1341,6 +1341,8 @@ void TheoryEngine::ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::The
 }
 
 theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable, bool preprocess, theory::TheoryId atomsTo) {
+  // For resource-limiting (also does a time check).
+  spendResource();
 
   // Do we need to check atoms
   if (atomsTo != theory::THEORY_LAST) {