diff options
| -rw-r--r-- | src/theory/quantifiers/quant_split.cpp | 2 | ||||
| -rw-r--r-- | src/theory/quantifiers/quant_util.cpp | 12 | ||||
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 2 | ||||
| -rw-r--r-- | src/theory/sep/theory_sep.cpp | 7 |
4 files changed, 20 insertions, 3 deletions
diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index 5aff1a848..35b3e1f9e 100644 --- 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 8ba6aa611..9158734e4 100644 --- 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 dc3f0cdd5..5b50526c4 100644 --- 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 714688142..e96badfd3 100644 --- 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 ); + } + } } } } |