Refactoring, generalization of bounded inference module. Simplification of rep set iterator. Disable quantifiers dynamic splitting for variables that are inferred bounded. Minor changes to fmc mbqi. Add regressions.

1 files changed, 15 insertions, 2 deletions

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index a3b6293fb..2d79826a6 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -251,8 +251,7 @@ void QuantifiersEngine::finishInit(){
     d_lte_part_inst = new quantifiers::LtePartialInst( this, c );
     d_modules.push_back( d_lte_part_inst );
   }
-  if( ( options::finiteModelFind() && options::quantDynamicSplit()!=quantifiers::QUANT_DSPLIT_MODE_NONE ) ||
-      options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_AGG ){
+  if( options::quantDynamicSplit()!=quantifiers::QUANT_DSPLIT_MODE_NONE ){
     d_qsplit = new quantifiers::QuantDSplit( this, c );
     d_modules.push_back( d_qsplit );
   }
@@ -328,6 +327,20 @@ bool QuantifiersEngine::hasOwnership( Node q, QuantifiersModule * m ) {
   return mo==m || mo==NULL;
 }
 
+bool QuantifiersEngine::isFiniteBound( Node q, Node v ) {
+  if( getBoundedIntegers() && getBoundedIntegers()->isBoundVar( q, v ) ){
+    return true;
+  }else{
+    TypeNode tn = v.getType();
+    if( tn.isSort() && options::finiteModelFind() ){
+      return true;
+    }else if( getTermDatabase()->mayComplete( tn ) ){
+      return true;
+    }
+  }
+  return false;
+}
+
 void QuantifiersEngine::presolve() {
   Trace("quant-engine-proc") << "QuantifiersEngine : presolve " << std::endl;
   for( unsigned i=0; i<d_modules.size(); i++ ){