summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/instantiation_engine.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/instantiation_engine.cpp')
-rw-r--r--src/theory/quantifiers/instantiation_engine.cpp10
1 files changed, 5 insertions, 5 deletions
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 49f561234..16cecb657 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -100,7 +100,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
if( !d_quantEngine->hasAddedLemma() ){
return false;
}else{
- Trace("inst-engine") << "Added lemmas = " << (int)(d_quantEngine->d_lemmas_waiting.size()-lastWaiting) << std::endl;
+ Trace("inst-engine") << "Added lemmas = " << (int)(d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl;
return true;
}
}
@@ -186,14 +186,14 @@ void InstantiationEngine::registerQuantifier( Node f ){
}
}
-void InstantiationEngine::addUserPattern( Node f, Node pat ){
+void InstantiationEngine::addUserPattern( Node q, Node pat ){
if( d_isup ){
- d_isup->addUserPattern( f, pat );
+ d_isup->addUserPattern( q, pat );
}
}
-void InstantiationEngine::addUserNoPattern( Node f, Node pat ){
+void InstantiationEngine::addUserNoPattern( Node q, Node pat ){
if( d_i_ag ){
- d_i_ag->addUserNoPattern( f, pat );
+ d_i_ag->addUserNoPattern( q, pat );
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback