Improvements to vts in cbqi, bug fix vts for non-atomic terms containing vts symbols. Move presolve for sygus to cbqi. Enable --cbqi-recurse by default, add option --cbqi-min-bound. Enable qcf for finite model finding by default.

1 files changed, 5 insertions, 2 deletions

diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 3dad74044..6cf64407f 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -102,7 +102,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
           //add counterexample lemma
           lem = Rewriter::rewrite( lem );
           Trace("cbqi") << "Counterexample lemma : " << lem << std::endl;
-          
+
           //must explicitly remove ITEs so that we record dependencies
           IteSkolemMap iteSkolemMap;
           std::vector< Node > lems;
@@ -140,7 +140,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
               }
             }
           }
-          
+
           addedLemma = true;
         }
       }
@@ -289,6 +289,9 @@ bool InstantiationEngine::checkComplete() {
 
 void InstantiationEngine::registerQuantifier( Node f ){
   if( d_quantEngine->hasOwnership( f, this ) ){
+    for( unsigned i=0; i<d_instStrategies.size(); ++i ){
+      d_instStrategies[i]->registerQuantifier( f );
+    }
     //Notice() << "do cbqi " << f << " ? " << std::endl;
     if( options::cbqi() ){
       Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( f );