From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Thu, 18 Sep 2014 23:15:26 +0000 (-0400)
Subject: Resource spending support in theories (and especially in quantifiers).
X-Git-Tag: cvc5-1.0.0~6625
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=49747c4574eec3cfa192ffb6e6a2451b949e8b3e;p=cvc5.git

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

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index a02e40e32..1572dfa88 100644
--- 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 23b3ac50a..4855083a8 100644
--- 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 19409faf7..073f2ab94 100644
--- 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) {