From 42deb51e8606005d9092c171f725f84c890b747f Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 26 Sep 2014 07:56:55 -0400 Subject: [PATCH] Finer-grained resource-limiting in quantifiers. --- src/theory/quantifiers_engine.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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