diff options
-rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.cpp | 20 |
1 files changed, 19 insertions, 1 deletions
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index 3d33f01ca..ddf032ac1 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -419,6 +419,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< } if( options::cbqiModel() ){ if( pvtn.isInteger() || pvtn.isReal() ){ + bool use_inf = d_use_vts_inf && ( pvtn.isInteger() ? options::cbqiUseInfInt() : options::cbqiUseInfReal() ); bool upper_first = false; if( options::cbqiMinBounds() ){ upper_first = mbp_bounds[1].size()<mbp_bounds[0].size(); @@ -429,7 +430,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< for( unsigned r=0; r<2; r++ ){ int rr = upper_first ? (1-r) : r; if( mbp_bounds[rr].empty() ){ - if( d_use_vts_inf && ( pvtn.isInteger() ? options::cbqiUseInfInt() : options::cbqiUseInfReal() ) ){ + if( use_inf ){ Trace("cbqi-bound") << "No " << ( rr==0 ? "lower" : "upper" ) << " bounds for " << pv << " (type=" << pvtn << ")" << std::endl; //no bounds, we do +- infinity Node val = d_qe->getTermDatabase()->getVtsInfinity( pvtn ); @@ -540,6 +541,23 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< } } } + //if not using infinity, use model value of zero + if( !use_inf && mbp_bounds[0].empty() && mbp_bounds[1].empty() ){ + Node val = d_zero; + Node c; //null (one) coefficient + val = getModelBasedProjectionValue( val, true, c, pv_value, d_zero, theta, Node::null(), vts_sym[0], Node::null(), vts_sym[1] ); + if( !val.isNull() ){ + if( subs_proc[val].find( c )==subs_proc[val].end() ){ + subs_proc[val][c] = true; + if( addInstantiationInc( val, pv, c, subs, vars, coeff, has_coeff, theta, i, effort ) ){ + return true; + } + } + } + } +#ifdef MBP_STRICT_ASSERTIONS + Assert( false ); +#endif //try non-optimal bounds (heuristic, may help when nested quantification) ? Trace("cbqi-bound") << "Try non-optimal bounds..." << std::endl; for( unsigned r=0; r<2; r++ ){ |