Minor changes to sep logic, epr, quantifier splitting.

diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
index 5aff1a848a50520e6f192d8d8c1c76c6854620b7..35b3e1f9e751ab103df4999edc496bd59d7ed79e 100644 (file)
--- a/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -48,7 +48,7 @@ void QuantDSplit::preRegisterQuantifier( Node q ) {
       }else{
         int score = -1;
         if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_AGG ){
-          score = dt.isInterpretedFinite() ? 1 : -1;
+          score = dt.isInterpretedFinite() ? 1 : 0;
         }else if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_DEFAULT ){
           score = dt.isInterpretedFinite() ? 1 : -1;
         }

diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index 8ba6aa611a18e45bdc6acc54ba3c69ef8ec743f7..9158734e4204aebb54e15f33294e997285cc947a 100644 (file)
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -423,10 +423,15 @@ void QuantEPR::registerNode( Node n, std::map< int, std::map< Node, bool > >& vi
   int vindex = hasPol ? ( pol ? 1 : -1 ) : 0;
   if( visited[vindex].find( n )==visited[vindex].end() ){
     visited[vindex][n] = true;
+    Trace("quant-epr-debug") << "QuantEPR::registerNode " << n << std::endl;
     if( n.getKind()==FORALL ){
       if( beneathQuant || !hasPol || !pol ){
         for( unsigned i=0; i<n[0].getNumChildren(); i++ ){
-          d_non_epr[n[0][i].getType()] = true;
+          TypeNode tn = n[0][i].getType();
+          if( d_non_epr.find( tn )==d_non_epr.end() ){
+            Trace("quant-epr") << "Sort " << tn << " is non-EPR because of nested quantification." << std::endl;
+            d_non_epr[tn] = true;
+          }
         }
       }else{
         beneathQuant = true;
@@ -455,6 +460,7 @@ void QuantEPR::registerNode( Node n, std::map< int, std::map< Node, bool > >& vi
         }
       }else if( std::find( d_consts[tn].begin(), d_consts[tn].end(), n )==d_consts[tn].end() ){
         d_consts[tn].push_back( n );
+        Trace("quant-epr") << "...constant of type " << tn << " : " << n << std::endl;
       }
     }
   }
@@ -466,10 +472,14 @@ void QuantEPR::registerAssertion( Node assertion ) {
 }
 
 void QuantEPR::finishInit() {
+  Trace("quant-epr-debug") << "QuantEPR::finishInit" << std::endl;
   for( std::map< TypeNode, std::vector< Node > >::iterator it = d_consts.begin(); it != d_consts.end(); ++it ){
+    Trace("quant-epr-debug") << "process " << it->first << std::endl;
     if( d_non_epr.find( it->first )!=d_non_epr.end() ){
+      Trace("quant-epr-debug") << "...non-epr" << std::endl;
       it->second.clear();
     }else{
+      Trace("quant-epr-debug") << "...epr, #consts = " << it->second.size() << std::endl;
       if( it->second.empty() ){
         it->second.push_back( NodeManager::currentNM()->mkSkolem( "e", it->first, "EPR base constant" ) );
       }

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index dc3f0cdd500bee24bdce6e7d593db6c61f38a399..5b50526c498f27e67a5570fe30a4ad95730b81a8 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -349,7 +349,7 @@ void QuantifiersEngine::presolve() {
 }
 
 void QuantifiersEngine::ppNotifyAssertions( std::vector< Node >& assertions ) {
-  Trace("quant-engine-proc") << "ppNotifyAssertions in QE" << std::endl;
+  Trace("quant-engine-proc") << "ppNotifyAssertions in QE, #assertions = " << assertions.size() << " check epr = " << (d_qepr!=NULL) << std::endl;
   if( ( options::instLevelInputOnly() && options::instMaxLevel()!=-1 ) || d_qepr!=NULL ){
     for( unsigned i=0; i<assertions.size(); i++ ) {
       if( options::instLevelInputOnly() && options::instMaxLevel()!=-1 ){

diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 714688142afdef0548509101cbfb8277eae7bac3..e96badfd33ca7465e28894087306311af8c125bd 100644 (file)
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -1028,6 +1028,13 @@ void TheorySep::initializeBounds() {
           qepr->d_consts[tn].push_back( e );
         }
       }
+      //EPR must include nil ref    
+      if( qepr && qepr->isEPR( tn ) ){
+        Node nr = getNilRef( tn );
+        if( !qepr->isEPRConstant( tn, nr ) ){
+          qepr->d_consts[tn].push_back( nr );
+        }
+      }      
     }
   }
 }