diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-09-26 07:56:55 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-09-26 07:56:55 -0400 |
commit | 42deb51e8606005d9092c171f725f84c890b747f (patch) | |
tree | 840d42f14c1ecb1d774be5ea78658b709c02b19b /src/theory | |
parent | ba9d9d0cfab0e23aa2bb11ff4f9cd7b20550a97b (diff) |
Finer-grained resource-limiting in quantifiers.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 6 |
1 files 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<f[0].getNumChildren(); i++ ){ |