From: Andrew Reynolds Date: Thu, 28 Sep 2017 21:31:02 +0000 (-0500) Subject: Cegqi refactor prep bv (#1155) X-Git-Tag: cvc5-1.0.0~5602 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=516862b9cb4a3404af8155a91f0087d755f20968;p=cvc5.git Cegqi refactor prep bv (#1155) * Preparing for bv instantiation, initial working version. * Undoing bv changes to break up into smaller commit. --- diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index 9375ffb74..0386a0fdb 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -114,30 +114,44 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e if( i==d_vars.size() ){ //solved for all variables, now construct instantiation bool needsPostprocess = false; - std::map< Instantiator *, Node > pp_inst; + std::vector< Instantiator * > pp_inst; + std::map< Instantiator *, Node > pp_inst_to_var; + std::vector< Node > lemmas; for( std::map< Node, Instantiator * >::iterator ita = d_active_instantiators.begin(); ita != d_active_instantiators.end(); ++ita ){ - if( ita->second->needsPostProcessInstantiation( this, sf, ita->first, effort ) ){ + if( ita->second->needsPostProcessInstantiationForVariable( this, sf, ita->first, effort ) ){ needsPostprocess = true; - pp_inst[ ita->second ] = ita->first; + pp_inst_to_var[ ita->second ] = ita->first; } } if( needsPostprocess ){ //must make copy so that backtracking reverts sf SolvedForm sf_tmp = sf; + unsigned prev_var_size = sf.d_vars.size(); bool postProcessSuccess = true; - for( std::map< Instantiator *, Node >::iterator itp = pp_inst.begin(); itp != pp_inst.end(); ++itp ){ - if( !itp->first->postProcessInstantiation( this, sf_tmp, itp->second, effort ) ){ + for( std::map< Instantiator *, Node >::iterator itp = pp_inst_to_var.begin(); itp != pp_inst_to_var.end(); ++itp ){ + if( !itp->first->postProcessInstantiationForVariable( this, sf_tmp, itp->second, effort, lemmas ) ){ postProcessSuccess = false; break; } } + if( sf_tmp.d_vars.size()>prev_var_size ){ + // if we added substitutions during postprocess, process these now + std::vector< Node > new_vars; + std::vector< Node > new_subs; + for( unsigned i=0; isecond[j]; if( std::find( lits.begin(), lits.end(), lit )==lits.end() ){ lits.push_back( lit ); - if( vinst->hasProcessAssertion( this, sf, pv, lit, effort ) ){ + if( vinst->hasProcessAssertion( this, sf, pv, lit, effort ) ){ + Trace("cbqi-inst-debug2") << " look at " << lit << std::endl; // apply substitutions Node slit = applySubstitutionToLiteral( lit, sf ); if( !slit.isNull() ){ + Trace("cbqi-inst-debug") << "...try based on literal " << slit << std::endl; // check if contains pv if( hasVariable( slit, pv ) ){ if( vinst->processAssertion( this, sf, pv, slit, effort ) ){ @@ -369,10 +385,10 @@ bool CegInstantiator::doAddInstantiationInc( Node pv, Node n, TermProperties& pv Assert( d_inelig.find( n )==d_inelig.end() ); //substitute into previous substitutions, when applicable - std::vector< Node > a_subs; - a_subs.push_back( n ); std::vector< Node > a_var; a_var.push_back( pv ); + std::vector< Node > a_subs; + a_subs.push_back( n ); std::vector< TermProperties > a_prop; a_prop.push_back( pv_prop ); std::vector< Node > a_non_basic; @@ -398,16 +414,29 @@ bool CegInstantiator::doAddInstantiationInc( Node pv, Node n, TermProperties& pv sf.d_subs[j] = new_subs; // the substitution apply to this term resulted in a non-basic substitution relationship if( !a_pv_prop.isBasic() ){ + // we are processing: + // sf.d_props[j].getModifiedTerm( sf.d_vars[j] ) = sf.d_subs[j] { pv_prop.getModifiedTerm( pv ) -> n } + + // based on the above substitution, we have: + // x = sf.d_subs[j] { pv_prop.getModifiedTerm( pv ) -> n } + // is equivalent to + // a_pv_prop.getModifiedTerm( x ) = new_subs + + // thus we must compose substitutions: + // a_pv_prop.getModifiedTerm( sf.d_props[j].getModifiedTerm( sf.d_vars[j] ) ) = new_subs + prev_prop[j] = sf.d_props[j]; + bool prev_basic = sf.d_props[j].isBasic(); + + // now compose the property + sf.d_props[j].composeProperty( a_pv_prop ); + // if previously was basic, becomes non-basic - if( sf.d_props[j].isBasic() ){ + if( prev_basic && !sf.d_props[j].isBasic() ){ Assert( std::find( sf.d_non_basic.begin(), sf.d_non_basic.end(), sf.d_vars[j] )==sf.d_non_basic.end() ); new_non_basic.push_back( sf.d_vars[j] ); sf.d_non_basic.push_back( sf.d_vars[j] ); } - // now combine the property - sf.d_props[j].combineProperty( a_pv_prop ); - Assert( !sf.d_props[j].isBasic() ); } if( sf.d_subs[j]!=prev_subs[j] ){ computeProgVars( sf.d_subs[j] ); @@ -456,7 +485,7 @@ bool CegInstantiator::doAddInstantiationInc( Node pv, Node n, TermProperties& pv } } -bool CegInstantiator::doAddInstantiation( std::vector< Node >& subs, std::vector< Node >& vars ) { +bool CegInstantiator::doAddInstantiation( std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& lemmas ) { if( vars.size()>d_vars.size() ){ Trace("cbqi-inst-debug") << "Reconstructing instantiations...." << std::endl; std::map< Node, Node > subs_map; @@ -481,6 +510,9 @@ bool CegInstantiator::doAddInstantiation( std::vector< Node >& subs, std::vector } } bool ret = d_out->doAddInstantiation( subs ); + for( unsigned i=0; iaddLemma( lemmas[i] ); + } return ret; } diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h index 8ffba8d7b..88b3465ad 100644 --- a/src/theory/quantifiers/ceg_instantiator.h +++ b/src/theory/quantifiers/ceg_instantiator.h @@ -63,8 +63,9 @@ public: return pv; } } - // combine property - virtual void combineProperty( TermProperties& p ){ + // compose property, should be such that: + // p.getModifiedTerm( this.getModifiedTerm( x ) ) = this_updated.getModifiedTerm( x ) + virtual void composeProperty( TermProperties& p ){ if( !p.d_coeff.isNull() ){ if( d_coeff.isNull() ){ d_coeff = p.d_coeff; @@ -177,7 +178,8 @@ private: void computeProgVars( Node n ); // effort=0 : do not use model value, 1: use model value, 2: one must use model value bool doAddInstantiation( SolvedForm& sf, unsigned i, unsigned effort ); - bool doAddInstantiation( std::vector< Node >& subs, std::vector< Node >& vars ); + // called by the above function after we finalize the variables/substitution and auxiliary lemmas + bool doAddInstantiation( std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& lemmas ); //process void processAssertions(); void addToAuxVarSubstitution( std::vector< Node >& subs_lhs, std::vector< Node >& subs_rhs, Node l, Node r ); @@ -286,9 +288,9 @@ public: virtual bool allowModelValue( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return d_closed_enum_type; } //do we need to postprocess the solved form for pv? - virtual bool needsPostProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; } - // propocess the solved form for pv, returns true if we successfully postprocessed - virtual bool postProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; } + virtual bool needsPostProcessInstantiationForVariable( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; } + //postprocess the solved form for pv, returns true if we successfully postprocessed, lemmas is a set of lemmas we wish to return along with the instantiation + virtual bool postProcessInstantiationForVariable( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort, std::vector< Node >& lemmas ) { return true; } /** Identify this module (for debugging) */ virtual std::string identify() const { return "Default"; } diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp index 88aeacb1d..ddec91d49 100644 --- a/src/theory/quantifiers/ceg_t_instantiator.cpp +++ b/src/theory/quantifiers/ceg_t_instantiator.cpp @@ -35,7 +35,7 @@ using namespace CVC4::theory::quantifiers; Node ArithInstantiator::getModelBasedProjectionValue( CegInstantiator * ci, Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta, Node inf_coeff, Node delta_coeff ) { Node val = t; - Trace("cbqi-bound2") << "Value : " << val << std::endl; + Trace("cegqi-arith-bound2") << "Value : " << val << std::endl; Assert( !e.getType().isInteger() || t.getType().isInteger() ); Assert( !e.getType().isInteger() || mt.getType().isInteger() ); //add rho value @@ -52,8 +52,8 @@ Node ArithInstantiator::getModelBasedProjectionValue( CegInstantiator * ci, Node new_theta = NodeManager::currentNM()->mkNode( MULT, new_theta, c ); new_theta = Rewriter::rewrite( new_theta ); } - Trace("cbqi-bound2") << "...c*e = " << ceValue << std::endl; - Trace("cbqi-bound2") << "...theta = " << new_theta << std::endl; + Trace("cegqi-arith-bound2") << "...c*e = " << ceValue << std::endl; + Trace("cegqi-arith-bound2") << "...theta = " << new_theta << std::endl; } if( !new_theta.isNull() && e.getType().isInteger() ){ Node rho; @@ -67,15 +67,15 @@ Node ArithInstantiator::getModelBasedProjectionValue( CegInstantiator * ci, Node rho = NodeManager::currentNM()->mkNode( MINUS, mt, ceValue ); } rho = Rewriter::rewrite( rho ); - Trace("cbqi-bound2") << "...rho = " << me << " - " << mt << " = " << rho << std::endl; - Trace("cbqi-bound2") << "..." << rho << " mod " << new_theta << " = "; + Trace("cegqi-arith-bound2") << "...rho = " << me << " - " << mt << " = " << rho << std::endl; + Trace("cegqi-arith-bound2") << "..." << rho << " mod " << new_theta << " = "; rho = NodeManager::currentNM()->mkNode( INTS_MODULUS_TOTAL, rho, new_theta ); rho = Rewriter::rewrite( rho ); - Trace("cbqi-bound2") << rho << std::endl; + Trace("cegqi-arith-bound2") << rho << std::endl; Kind rk = isLower ? PLUS : MINUS; val = NodeManager::currentNM()->mkNode( rk, val, rho ); val = Rewriter::rewrite( val ); - Trace("cbqi-bound2") << "(after rho) : " << val << std::endl; + Trace("cegqi-arith-bound2") << "(after rho) : " << val << std::endl; } if( !inf_coeff.isNull() ){ Assert( !d_vts_sym[0].isNull() ); @@ -95,12 +95,12 @@ Node ArithInstantiator::getModelBasedProjectionValue( CegInstantiator * ci, Node // ensures val is Int if pv is Int, and val does not contain vts symbols int ArithInstantiator::solve_arith( CegInstantiator * ci, Node pv, Node atom, Node& veq_c, Node& val, Node& vts_coeff_inf, Node& vts_coeff_delta ) { int ires = 0; - Trace("cbqi-inst-debug") << "isolate for " << pv << " in " << atom << std::endl; + Trace("cegqi-arith-debug") << "isolate for " << pv << " in " << atom << std::endl; std::map< Node, Node > msum; if( QuantArith::getMonomialSumLit( atom, msum ) ){ - Trace("cbqi-inst-debug") << "got monomial sum: " << std::endl; - if( Trace.isOn("cbqi-inst-debug") ){ - QuantArith::debugPrintMonomialSum( msum, "cbqi-inst-debug" ); + Trace("cegqi-arith-debug") << "got monomial sum: " << std::endl; + if( Trace.isOn("cegqi-arith-debug") ){ + QuantArith::debugPrintMonomialSum( msum, "cegqi-arith-debug" ); } TypeNode pvtn = pv.getType(); //remove vts symbols from polynomial @@ -128,7 +128,7 @@ int ArithInstantiator::solve_arith( CegInstantiator * ci, Node pv, Node atom, No } } } - Trace("cbqi-inst-debug") << "vts[" << t << "] coefficient is " << vts_coeff[t] << std::endl; + Trace("cegqi-arith-debug") << "vts[" << t << "] coefficient is " << vts_coeff[t] << std::endl; msum.erase( d_vts_sym[t] ); } } @@ -137,17 +137,17 @@ int ArithInstantiator::solve_arith( CegInstantiator * ci, Node pv, Node atom, No ires = QuantArith::isolate( pv, msum, veq_c, val, atom.getKind() ); if( ires!=0 ){ Node realPart; - if( Trace.isOn("cbqi-inst-debug") ){ - Trace("cbqi-inst-debug") << "Isolate : "; + if( Trace.isOn("cegqi-arith-debug") ){ + Trace("cegqi-arith-debug") << "Isolate : "; if( !veq_c.isNull() ){ - Trace("cbqi-inst-debug") << veq_c << " * "; + Trace("cegqi-arith-debug") << veq_c << " * "; } - Trace("cbqi-inst-debug") << pv << " " << atom.getKind() << " " << val << std::endl; + Trace("cegqi-arith-debug") << pv << " " << atom.getKind() << " " << val << std::endl; } if( options::cbqiAll() ){ // when not pure LIA/LRA, we must check whether the lhs contains pv if( TermDb::containsTerm( val, pv ) ){ - Trace("cbqi-inst-debug") << "fail : contains bad term" << std::endl; + Trace("cegqi-arith-debug") << "fail : contains bad term" << std::endl; return 0; } } @@ -187,25 +187,25 @@ int ArithInstantiator::solve_arith( CegInstantiator * ci, Node pv, Node atom, No realPart = real_part.empty() ? ci->getQuantifiersEngine()->getTermDatabase()->d_zero : ( real_part.size()==1 ? real_part[0] : NodeManager::currentNM()->mkNode( PLUS, real_part ) ); Assert( ci->getOutput()->isEligibleForInstantiation( realPart ) ); //re-isolate - Trace("cbqi-inst-debug") << "Re-isolate..." << std::endl; + Trace("cegqi-arith-debug") << "Re-isolate..." << std::endl; ires = QuantArith::isolate( pv, msum, veq_c, val, atom.getKind() ); - Trace("cbqi-inst-debug") << "Isolate for mixed Int/Real : " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << std::endl; - Trace("cbqi-inst-debug") << " real part : " << realPart << std::endl; + Trace("cegqi-arith-debug") << "Isolate for mixed Int/Real : " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << std::endl; + Trace("cegqi-arith-debug") << " real part : " << realPart << std::endl; if( ires!=0 ){ int ires_use = ( msum[pv].isNull() || msum[pv].getConst().sgn()==1 ) ? 1 : -1; val = Rewriter::rewrite( NodeManager::currentNM()->mkNode( ires_use==-1 ? PLUS : MINUS, NodeManager::currentNM()->mkNode( ires_use==-1 ? MINUS : PLUS, val, realPart ), NodeManager::currentNM()->mkNode( TO_INTEGER, realPart ) ) ); //TODO: round up for upper bounds? - Trace("cbqi-inst-debug") << "result : " << val << std::endl; + Trace("cegqi-arith-debug") << "result : " << val << std::endl; Assert( val.getType().isInteger() ); } } } vts_coeff_inf = vts_coeff[0]; vts_coeff_delta = vts_coeff[1]; - Trace("cbqi-inst-debug") << "Return " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << ", vts = (" << vts_coeff_inf << ", " << vts_coeff_delta << ")" << std::endl; + Trace("cegqi-arith-debug") << "Return " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << ", vts = (" << vts_coeff_inf << ", " << vts_coeff_delta << ")" << std::endl; }else{ - Trace("cbqi-inst-debug") << "fail : could not get monomial sum" << std::endl; + Trace("cegqi-arith-debug") << "fail : could not get monomial sum" << std::endl; } return ires; } @@ -231,12 +231,12 @@ bool ArithInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, N //make the same coefficient if( rhs_coeff!=lhs_coeff ){ if( !rhs_coeff.isNull() ){ - Trace("cbqi-inst-debug") << "...mult lhs by " << rhs_coeff << std::endl; + Trace("cegqi-arith-debug") << "...mult lhs by " << rhs_coeff << std::endl; eq_lhs = NodeManager::currentNM()->mkNode( MULT, rhs_coeff, eq_lhs ); eq_lhs = Rewriter::rewrite( eq_lhs ); } if( !lhs_coeff.isNull() ){ - Trace("cbqi-inst-debug") << "...mult rhs by " << lhs_coeff << std::endl; + Trace("cegqi-arith-debug") << "...mult rhs by " << lhs_coeff << std::endl; eq_rhs = NodeManager::currentNM()->mkNode( MULT, lhs_coeff, eq_rhs ); eq_rhs = Rewriter::rewrite( eq_rhs ); } @@ -267,7 +267,6 @@ bool ArithInstantiator::hasProcessAssertion( CegInstantiator * ci, SolvedForm& s } bool ArithInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) { - Trace("cbqi-inst-debug2") << " look at " << lit << std::endl; Node atom = lit.getKind()==NOT ? lit[0] : lit; bool pol = lit.getKind()!=NOT; //arithmetic inequalities and disequalities @@ -275,7 +274,6 @@ bool ArithInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, // get model value for pv Node pv_value = ci->getModelValue( pv ); //cannot contain infinity? - Trace("cbqi-inst-debug") << "..[3] Substituted assertion : " << atom << ", pol = " << pol << std::endl; Node vts_coeff_inf; Node vts_coeff_delta; Node val; @@ -308,7 +306,7 @@ bool ArithInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, //first check if there is an infinity... if( !vts_coeff_inf.isNull() ){ //coefficient or val won't make a difference, just compare with zero - Trace("cbqi-inst-debug") << "Disequality : check infinity polarity " << vts_coeff_inf << std::endl; + Trace("cegqi-arith-debug") << "Disequality : check infinity polarity " << vts_coeff_inf << std::endl; Assert( vts_coeff_inf.isConst() ); is_upper = ( vts_coeff_inf.getConst().sgn()==1 ); }else{ @@ -318,7 +316,7 @@ bool ArithInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, lhs_value = pv_prop.getModifiedTerm( pv_value ); lhs_value = Rewriter::rewrite( lhs_value ); } - Trace("cbqi-inst-debug") << "Disequality : check model values " << lhs_value << " " << rhs_value << std::endl; + Trace("cegqi-arith-debug") << "Disequality : check model values " << lhs_value << " " << rhs_value << std::endl; Assert( lhs_value!=rhs_value ); Node cmp = NodeManager::currentNM()->mkNode( GEQ, lhs_value, rhs_value ); cmp = Rewriter::rewrite( cmp ); @@ -338,10 +336,10 @@ bool ArithInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, uires = is_upper ? -2 : 2; } } - if( Trace.isOn("cbqi-bound-inf") ){ + if( Trace.isOn("cegqi-arith-bound-inf") ){ Node pvmod = pv_prop.getModifiedTerm( pv ); - Trace("cbqi-bound-inf") << "From " << lit << ", got : "; - Trace("cbqi-bound-inf") << pvmod << " -> " << uval << ", styp = " << uires << std::endl; + Trace("cegqi-arith-bound-inf") << "From " << lit << ", got : "; + Trace("cegqi-arith-bound-inf") << pvmod << " -> " << uval << ", styp = " << uires << std::endl; } //take into account delta if( ci->useVtsDelta() && ( uires==2 || uires==-2 ) ){ @@ -364,7 +362,7 @@ bool ArithInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, unsigned index = uires>0 ? 0 : 1; d_mbp_bounds[index].push_back( uval ); d_mbp_coeff[index].push_back( pv_prop.d_coeff ); - Trace("cbqi-inst-debug") << "Store bound " << index << " " << uval << " " << pv_prop.d_coeff << " " << vts_coeff_inf << " " << vts_coeff_delta << " " << lit << std::endl; + Trace("cegqi-arith-debug") << "Store bound " << index << " " << uval << " " << pv_prop.d_coeff << " " << vts_coeff_inf << " " << vts_coeff_delta << " " << lit << std::endl; for( unsigned t=0; t<2; t++ ){ d_mbp_vts_coeff[index][t].push_back( t==0 ? vts_coeff_inf : vts_coeff_delta ); } @@ -401,7 +399,7 @@ bool ArithInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf, best_used[rr] = -1; if( d_mbp_bounds[rr].empty() ){ if( use_inf ){ - Trace("cbqi-bound") << "No " << ( rr==0 ? "lower" : "upper" ) << " bounds for " << pv << " (type=" << d_type << ")" << std::endl; + Trace("cegqi-arith-bound") << "No " << ( rr==0 ? "lower" : "upper" ) << " bounds for " << pv << " (type=" << d_type << ")" << std::endl; //no bounds, we do +- infinity Node val = ci->getQuantifiersEngine()->getTermDatabase()->getVtsInfinity( d_type ); //TODO : rho value for infinity? @@ -415,24 +413,24 @@ bool ArithInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf, } } }else{ - Trace("cbqi-bound") << ( rr==0 ? "Lower" : "Upper" ) << " bounds for " << pv << " (type=" << d_type << ") : " << std::endl; + Trace("cegqi-arith-bound") << ( rr==0 ? "Lower" : "Upper" ) << " bounds for " << pv << " (type=" << d_type << ") : " << std::endl; int best = -1; Node best_bound_value[3]; for( unsigned j=0; jgetModelValue( d_mbp_bounds[rr][j] ); t_values[rr][j] = t_value; value[1] = t_value; - Trace("cbqi-bound") << value[1]; + Trace("cegqi-arith-bound") << value[1]; }else{ value[2] = d_mbp_vts_coeff[rr][1][j]; if( !value[2].isNull() ){ - Trace("cbqi-bound") << " + ( " << value[2] << " * DELTA )"; + Trace("cegqi-arith-bound") << " + ( " << value[2] << " * DELTA )"; }else{ value[2] = zero; } @@ -479,7 +477,7 @@ bool ArithInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf, } } } - Trace("cbqi-bound") << std::endl; + Trace("cegqi-arith-bound") << std::endl; if( new_best ){ for( unsigned t=0; t<3; t++ ){ best_bound_value[t] = value[t]; @@ -488,15 +486,15 @@ bool ArithInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf, } } if( best!=-1 ){ - Trace("cbqi-bound") << "...best bound is " << best << " : "; + Trace("cegqi-arith-bound") << "...best bound is " << best << " : "; if( best_bound_value[0]!=zero ){ - Trace("cbqi-bound") << "( " << best_bound_value[0] << " * INF ) + "; + Trace("cegqi-arith-bound") << "( " << best_bound_value[0] << " * INF ) + "; } - Trace("cbqi-bound") << best_bound_value[1]; + Trace("cegqi-arith-bound") << best_bound_value[1]; if( best_bound_value[2]!=zero ){ - Trace("cbqi-bound") << " + ( " << best_bound_value[2] << " * DELTA )"; + Trace("cegqi-arith-bound") << " + ( " << best_bound_value[2] << " * DELTA )"; } - Trace("cbqi-bound") << std::endl; + Trace("cegqi-arith-bound") << std::endl; best_used[rr] = best; //if using cbqiMidpoint, only add the instance based on one bound if the bound is non-strict if( !options::cbqiMidpoint() || d_type.isInteger() || d_mbp_vts_coeff[rr][1][best].isNull() ){ @@ -530,7 +528,7 @@ bool ArithInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf, if( options::cbqiMidpoint() && !d_type.isInteger() ){ Node vals[2]; bool bothBounds = true; - Trace("cbqi-bound") << "Try midpoint of bounds..." << std::endl; + Trace("cegqi-arith-bound") << "Try midpoint of bounds..." << std::endl; for( unsigned rr=0; rr<2; rr++ ){ int best = best_used[rr]; if( best==-1 ){ @@ -540,7 +538,7 @@ bool ArithInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf, vals[rr] = getModelBasedProjectionValue( ci, pv, vals[rr], rr==0, Node::null(), pv_value, t_values[rr][best], sf.getTheta(), d_mbp_vts_coeff[rr][0][best], Node::null() ); } - Trace("cbqi-bound") << "Bound : " << vals[rr] << std::endl; + Trace("cegqi-arith-bound") << "Bound : " << vals[rr] << std::endl; } Node val; if( bothBounds ){ @@ -561,7 +559,7 @@ bool ArithInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf, val = Rewriter::rewrite( val ); } } - Trace("cbqi-bound") << "Midpoint value : " << val << std::endl; + Trace("cegqi-arith-bound") << "Midpoint value : " << val << std::endl; if( !val.isNull() ){ TermProperties pv_prop_midpoint; if( ci->doAddInstantiationInc( pv, val, pv_prop_midpoint, sf, effort ) ){ @@ -574,7 +572,7 @@ bool ArithInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf, if( options::cbqiNopt() ){ //try non-optimal bounds (heuristic, may help when nested quantification) ? - Trace("cbqi-bound") << "Try non-optimal bounds..." << std::endl; + Trace("cegqi-arith-bound") << "Try non-optimal bounds..." << std::endl; for( unsigned r=0; r<2; r++ ){ int rr = upper_first ? (1-r) : r; for( unsigned j=0; j& lemmas ) { Assert( std::find( sf.d_non_basic.begin(), sf.d_non_basic.end(), pv )!=sf.d_non_basic.end() ); Assert( std::find( sf.d_vars.begin(), sf.d_vars.end(), pv )!=sf.d_vars.end() ); unsigned index = std::find( sf.d_vars.begin(), sf.d_vars.end(), pv )-sf.d_vars.begin(); Assert( !sf.d_props[index].isBasic() ); Node eq_lhs = sf.d_props[index].getModifiedTerm( sf.d_vars[index] ); - if( Trace.isOn("cbqi-inst-debug") ){ - Trace("cbqi-inst-debug") << "Normalize substitution for "; - Trace("cbqi-inst-debug") << eq_lhs << " = " << sf.d_subs[index] << std::endl; + if( Trace.isOn("cegqi-arith-debug") ){ + Trace("cegqi-arith-debug") << "Normalize substitution for "; + Trace("cegqi-arith-debug") << eq_lhs << " = " << sf.d_subs[index] << std::endl; } Assert( sf.d_vars[index].getType().isInteger() ); //must ensure that divisibility constraints are met @@ -617,7 +616,7 @@ bool ArithInstantiator::postProcessInstantiation( CegInstantiator * ci, SolvedFo Node eq_rhs = sf.d_subs[index]; Node eq = eq_lhs.eqNode( eq_rhs ); eq = Rewriter::rewrite( eq ); - Trace("cbqi-inst-debug") << "...equality is " << eq << std::endl; + Trace("cegqi-arith-debug") << "...equality is " << eq << std::endl; std::map< Node, Node > msum; if( QuantArith::getMonomialSumLit( eq, msum ) ){ Node veq; @@ -632,7 +631,7 @@ bool ArithInstantiator::postProcessInstantiation( CegInstantiator * ci, SolvedFo sf.d_subs[index] = veq[1]; if( !veq_c.isNull() ){ sf.d_subs[index] = NodeManager::currentNM()->mkNode( INTS_DIVISION_TOTAL, veq[1], veq_c ); - Trace("cbqi-inst-debug") << "...bound type is : " << sf.d_props[index].d_type << std::endl; + Trace("cegqi-arith-debug") << "...bound type is : " << sf.d_props[index].d_type << std::endl; //intger division rounding up if from a lower bound if( sf.d_props[index].d_type==1 && options::cbqiRoundUpLowerLia() ){ sf.d_subs[index] = NodeManager::currentNM()->mkNode( PLUS, sf.d_subs[index], @@ -644,13 +643,13 @@ bool ArithInstantiator::postProcessInstantiation( CegInstantiator * ci, SolvedFo ); } } - Trace("cbqi-inst-debug") << "...normalize integers : " << sf.d_vars[index] << " -> " << sf.d_subs[index] << std::endl; + Trace("cegqi-arith-debug") << "...normalize integers : " << sf.d_vars[index] << " -> " << sf.d_subs[index] << std::endl; }else{ - Trace("cbqi-inst-debug") << "...failed to isolate." << std::endl; + Trace("cegqi-arith-debug") << "...failed to isolate." << std::endl; return false; } }else{ - Trace("cbqi-inst-debug") << "...failed to get monomial sum." << std::endl; + Trace("cegqi-arith-debug") << "...failed to get monomial sum." << std::endl; return false; } return true; @@ -661,7 +660,7 @@ void DtInstantiator::reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsig } Node DtInstantiator::solve_dt( Node v, Node a, Node b, Node sa, Node sb ) { - Trace("cbqi-inst-debug2") << "Solve dt : " << v << " " << a << " " << b << " " << sa << " " << sb << std::endl; + Trace("cegqi-arith-debug2") << "Solve dt : " << v << " " << a << " " << b << " " << sa << " " << sb << std::endl; Node ret; if( !a.isNull() && a==v ){ ret = sb; @@ -702,12 +701,12 @@ Node DtInstantiator::solve_dt( Node v, Node a, Node b, Node sa, Node sb ) { } bool DtInstantiator::processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort ) { - Trace("cbqi-inst-debug") << "[2] try based on constructors in equivalence class." << std::endl; + Trace("cegqi-dt-debug") << "[2] try based on constructors in equivalence class." << std::endl; //[2] look in equivalence class for a constructor for( unsigned k=0; k children; children.push_back( n.getOperator() ); const Datatype& dt = ((DatatypeType)(d_type).toType()).getDatatype(); @@ -764,10 +763,10 @@ void EprInstantiator::computeMatchScore( CegInstantiator * ci, Node pv, Node cat if( index==catom.getNumChildren() ){ Assert( tat->hasNodeData() ); Node gcatom = tat->getNodeData(); - Trace("epr-inst") << "Matched : " << catom << " and " << gcatom << std::endl; + Trace("cegqi-epr") << "Matched : " << catom << " and " << gcatom << std::endl; for( unsigned i=0; i& match_score ) { if( inst::Trigger::isAtomicTrigger( catom ) && TermDb::containsTerm( catom, pv ) ){ - Trace("epr-inst") << "Find matches for " << catom << "..." << std::endl; + Trace("cegqi-epr") << "Find matches for " << catom << "..." << std::endl; std::vector< Node > arg_reps; for( unsigned j=0; jgetQuantifiersEngine()->getMasterEqualityEngine()->getRepresentative( catom[j] ) ); @@ -793,7 +792,7 @@ void EprInstantiator::computeMatchScore( CegInstantiator * ci, Node pv, Node cat Node rep = ci->getQuantifiersEngine()->getMasterEqualityEngine()->getRepresentative( eqc ); Node op = ci->getQuantifiersEngine()->getTermDatabase()->getMatchOperator( catom ); TermArgTrie * tat = ci->getQuantifiersEngine()->getTermDatabase()->getTermArgTrie( rep, op ); - Trace("epr-inst") << "EPR instantiation match term : " << catom << ", check ground terms=" << (tat!=NULL) << std::endl; + Trace("cegqi-epr") << "EPR instantiation match term : " << catom << ", check ground terms=" << (tat!=NULL) << std::endl; if( tat ){ computeMatchScore( ci, pv, catom, arg_reps, tat, 0, match_score ); } diff --git a/src/theory/quantifiers/ceg_t_instantiator.h b/src/theory/quantifiers/ceg_t_instantiator.h index 51142f77d..457e07f7a 100644 --- a/src/theory/quantifiers/ceg_t_instantiator.h +++ b/src/theory/quantifiers/ceg_t_instantiator.h @@ -45,8 +45,8 @@ public: bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ); bool processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ); bool processAssertions( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& lits, unsigned effort ); - bool needsPostProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ); - bool postProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ); + bool needsPostProcessInstantiationForVariable( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ); + bool postProcessInstantiationForVariable( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort, std::vector< Node >& lemmas ); std::string identify() const { return "Arith"; } }; @@ -156,6 +156,7 @@ public: }; + } } }