From: ajreynol Date: Tue, 25 Aug 2015 15:53:17 +0000 (+0200) Subject: Use zero in cbqi when not using infinities. X-Git-Tag: cvc5-1.0.0~6252^2~6 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d9c22c34d122a34d8a8a914936d9186be9a638fe;p=cvc5.git Use zero in cbqi when not using infinities. --- 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()& 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++ ){