From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 26 Sep 2014 11:56:55 +0000 (-0400)
Subject: Finer-grained resource-limiting in quantifiers.
X-Git-Tag: cvc5-1.0.0~6616
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=42deb51e8606005d9092c171f725f84c890b747f;p=cvc5.git

Finer-grained resource-limiting in quantifiers.
---

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 5dd3816c5..a4d7aaec1 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -576,9 +576,6 @@ 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);
@@ -603,6 +600,9 @@ void QuantifiersEngine::addRequirePhase( Node lit, bool req ){
 }
 
 bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool mkRep, bool modEq, bool modInst ){
+  // For resource-limiting (also does a time check).
+  getOutputChannel().spendResource();
+
   std::vector< Node > terms;
   //make sure there are values for each variable we are instantiating
   for( size_t i=0; i<f[0].getNumChildren(); i++ ){