From: ajreynol Date: Wed, 11 Mar 2015 14:43:56 +0000 (+0100) Subject: Minor fixes and improvements to cegqi-si for linear arithmetic. X-Git-Tag: cvc5-1.0.0~6379 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e99c176931f0673ac47eb4525365b813df99112e;p=cvc5.git Minor fixes and improvements to cegqi-si for linear arithmetic. --- diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index bcad52087..7553eb736 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -261,6 +261,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { Trace("cegqi-lemma") << "Single invocation lemma : " << lems[j] << std::endl; d_quantEngine->addLemma( lems[j] ); } + d_statistics.d_cegqi_si_lemmas += lems.size(); Trace("cegqi-engine") << " ...try single invocation." << std::endl; return; } @@ -317,6 +318,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { d_last_inst_si = false; Trace("cegqi-lemma") << "Counterexample lemma : " << lem << std::endl; d_quantEngine->addLemma( lem ); + ++(d_statistics.d_cegqi_lemmas_ce); Trace("cegqi-engine") << " ...find counterexample." << std::endl; } @@ -364,6 +366,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { Trace("cegqi-lemma") << "Candidate refinement lemma : " << lem << std::endl; Trace("cegqi-engine") << " ...refine candidate." << std::endl; d_quantEngine->addLemma( lem ); + ++(d_statistics.d_cegqi_lemmas_refine); conj->d_refine_count++; } } @@ -553,4 +556,21 @@ void CegInstantiation::collectDisjuncts( Node n, std::vector< Node >& d ) { } } +CegInstantiation::Statistics::Statistics(): + d_cegqi_lemmas_ce("CegInstantiation::cegqi_lemmas_ce", 0), + d_cegqi_lemmas_refine("CegInstantiation::cegqi_lemmas_refine", 0), + d_cegqi_si_lemmas("CegInstantiation::cegqi_lemmas_si", 0) +{ + StatisticsRegistry::registerStat(&d_cegqi_lemmas_ce); + StatisticsRegistry::registerStat(&d_cegqi_lemmas_refine); + StatisticsRegistry::registerStat(&d_cegqi_si_lemmas); +} + +CegInstantiation::Statistics::~Statistics(){ + StatisticsRegistry::unregisterStat(&d_cegqi_lemmas_ce); + StatisticsRegistry::unregisterStat(&d_cegqi_lemmas_refine); + StatisticsRegistry::unregisterStat(&d_cegqi_si_lemmas); +} + + } diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h index 95f491dc9..786db12a9 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/ce_guided_instantiation.h @@ -132,6 +132,16 @@ public: void printSynthSolution( std::ostream& out ); /** collect disjuncts */ static void collectDisjuncts( Node n, std::vector< Node >& ex ); +public: + class Statistics { + public: + IntStat d_cegqi_lemmas_ce; + IntStat d_cegqi_lemmas_refine; + IntStat d_cegqi_si_lemmas; + Statistics(); + ~Statistics(); + };/* class CegInstantiation::Statistics */ + Statistics d_statistics; }; } diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index e5f5327c8..3ddd5e157 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -438,222 +438,242 @@ void CegConjectureSingleInv::computeProgVars( Node n ){ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ, - unsigned i, std::vector< Node >& lems ){ + unsigned i, std::vector< Node >& lems, unsigned effort ){ if( i==d_single_inv_sk.size() ){ return addInstantiationCoeff( subs, vars, coeff, has_coeff, subs_typ, 0, lems ); }else{ eq::EqualityEngine* ee = d_qe->getMasterEqualityEngine(); - std::map< Node, std::map< Node, bool > > subs_proc; + std::map< int, std::map< Node, std::map< Node, bool > > > subs_proc; Node v = d_single_inv_map_to_prog[d_single_inv[0][i]]; Node pv = d_single_inv_sk[i]; TypeNode pvtn = pv.getType(); - Node pvr; - //[1] easy case : pv is in the equivalence class as another term not containing pv - if( ee->hasTerm( pv ) ){ - pvr = ee->getRepresentative( pv ); - eq::EqClassIterator eqc_i = eq::EqClassIterator( pvr, ee ); - while( !eqc_i.isFinished() ){ - Node n = *eqc_i; - if( n!=pv ){ - Trace("cegqi-si-inst-debug") << i << "...try based on equal term " << n << std::endl; - //compute d_subs_fv, which program variables are contained in n - computeProgVars( n ); - //must be an eligible term - if( d_inelig.find( n )==d_inelig.end() ){ - Node ns; - Node pv_coeff; //coefficient of pv in the equality we solve (null is 1) - bool proc = false; - if( !d_prog_var[n].empty() ){ - ns = applySubstitution( n, subs, vars, coeff, has_coeff, pv_coeff, false ); - if( !ns.isNull() ){ - computeProgVars( ns ); - //substituted version must be new and cannot contain pv - proc = subs_proc[pv_coeff].find( ns )==subs_proc[pv_coeff].end() && d_prog_var[ns].find( pv )==d_prog_var[ns].end(); - } - }else{ - ns = n; - proc = true; - } - if( proc ){ - //try the substitution - subs_proc[ns][pv_coeff] = true; - if( addInstantiationInc( ns, pv, pv_coeff, 0, subs, vars, coeff, has_coeff, subs_typ, i, lems ) ){ - return true; - } - } - } - } - ++eqc_i; - } - } - - //[2] : we can solve an equality for pv - ///iterate over equivalence classes to find cases where we can solve for the variable - if( pvtn.isInteger() || pvtn.isReal() ){ - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); - while( !eqcs_i.isFinished() ){ - Node r = *eqcs_i; - TypeNode rtn = r.getType(); - if( rtn.isInteger() || rtn.isReal() ){ - std::vector< Node > lhs; - std::vector< bool > lhs_v; - std::vector< Node > lhs_coeff; - eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); - while( !eqc_i.isFinished() ){ - Node n = *eqc_i; + if( (i+1)hasTerm( pv ) ){ + Node pvr = ee->getRepresentative( pv ); + eq::EqClassIterator eqc_i = eq::EqClassIterator( pvr, ee ); + while( !eqc_i.isFinished() ){ + Node n = *eqc_i; + if( n!=pv ){ + Trace("cegqi-si-inst-debug") << i << "...try based on equal term " << n << std::endl; + //compute d_subs_fv, which program variables are contained in n computeProgVars( n ); //must be an eligible term if( d_inelig.find( n )==d_inelig.end() ){ Node ns; - Node pv_coeff; + Node pv_coeff; //coefficient of pv in the equality we solve (null is 1) + bool proc = false; if( !d_prog_var[n].empty() ){ - ns = applySubstitution( n, subs, vars, coeff, has_coeff, pv_coeff ); + ns = applySubstitution( n, subs, vars, coeff, has_coeff, pv_coeff, false ); if( !ns.isNull() ){ computeProgVars( ns ); + //substituted version must be new and cannot contain pv + proc = subs_proc[0][pv_coeff].find( ns )==subs_proc[0][pv_coeff].end() && d_prog_var[ns].find( pv )==d_prog_var[ns].end(); } }else{ ns = n; + proc = true; } - if( !ns.isNull() ){ - bool hasVar = d_prog_var[ns].find( pv )!=d_prog_var[ns].end(); - for( unsigned j=0; jmkNode( MULT, pv_coeff, eq_lhs ); - eq_lhs = Rewriter::rewrite( eq_lhs ); - } - if( !lhs_coeff[j].isNull() ){ - Trace("cegqi-si-inst-debug") << "...mult rhs by " << lhs_coeff[j] << std::endl; - eq_rhs = NodeManager::currentNM()->mkNode( MULT, lhs_coeff[j], eq_rhs ); - eq_rhs = Rewriter::rewrite( eq_rhs ); - } - } - Node eq = eq_lhs.eqNode( eq_rhs ); - eq = Rewriter::rewrite( eq ); - Trace("cegqi-si-inst-debug") << "...equality is " << eq << std::endl; - std::map< Node, Node > msum; - if( QuantArith::getMonomialSumLit( eq, msum ) ){ - if( Trace.isOn("cegqi-si-inst-debug") ){ - Trace("cegqi-si-inst-debug") << "...got monomial sum: " << std::endl; - QuantArith::debugPrintMonomialSum( msum, "cegqi-si-inst-debug" ); - Trace("cegqi-si-inst-debug") << "isolate for " << pv << "..." << std::endl; + if( proc ){ + //try the substitution + subs_proc[0][ns][pv_coeff] = true; + if( addInstantiationInc( ns, pv, pv_coeff, 0, subs, vars, coeff, has_coeff, subs_typ, i, lems, effort ) ){ + return true; + } + } + } + } + ++eqc_i; + } + } + + //[2] : we can solve an equality for pv + ///iterate over equivalence classes to find cases where we can solve for the variable + if( pvtn.isInteger() || pvtn.isReal() ){ + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); + while( !eqcs_i.isFinished() ){ + Node r = *eqcs_i; + TypeNode rtn = r.getType(); + if( rtn.isInteger() || rtn.isReal() ){ + std::vector< Node > lhs; + std::vector< bool > lhs_v; + std::vector< Node > lhs_coeff; + eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); + while( !eqc_i.isFinished() ){ + Node n = *eqc_i; + computeProgVars( n ); + //must be an eligible term + if( d_inelig.find( n )==d_inelig.end() ){ + Node ns; + Node pv_coeff; + if( !d_prog_var[n].empty() ){ + ns = applySubstitution( n, subs, vars, coeff, has_coeff, pv_coeff ); + if( !ns.isNull() ){ + computeProgVars( ns ); + } + }else{ + ns = n; + } + if( !ns.isNull() ){ + bool hasVar = d_prog_var[ns].find( pv )!=d_prog_var[ns].end(); + for( unsigned j=0; jmkNode( MULT, pv_coeff, eq_lhs ); + eq_lhs = Rewriter::rewrite( eq_lhs ); + } + if( !lhs_coeff[j].isNull() ){ + Trace("cegqi-si-inst-debug") << "...mult rhs by " << lhs_coeff[j] << std::endl; + eq_rhs = NodeManager::currentNM()->mkNode( MULT, lhs_coeff[j], eq_rhs ); + eq_rhs = Rewriter::rewrite( eq_rhs ); + } } - Node veq; - if( QuantArith::isolate( pv, msum, veq, EQUAL, true )!=0 ){ - Trace("cegqi-si-inst-debug") << "...isolated equality " << veq << "." << std::endl; - Node veq_c; - if( veq[0]!=pv ){ - Node veq_v; - if( QuantArith::getMonomial( veq[0], veq_c, veq_v ) ){ - Assert( veq_v==pv ); - } + Node eq = eq_lhs.eqNode( eq_rhs ); + eq = Rewriter::rewrite( eq ); + Trace("cegqi-si-inst-debug") << "...equality is " << eq << std::endl; + std::map< Node, Node > msum; + if( QuantArith::getMonomialSumLit( eq, msum ) ){ + if( Trace.isOn("cegqi-si-inst-debug") ){ + Trace("cegqi-si-inst-debug") << "...got monomial sum: " << std::endl; + QuantArith::debugPrintMonomialSum( msum, "cegqi-si-inst-debug" ); + Trace("cegqi-si-inst-debug") << "isolate for " << pv << "..." << std::endl; } - if( subs_proc[veq[1]].find( veq_c )==subs_proc[veq[1]].end() ){ - subs_proc[veq[1]][veq_c] = true; - if( addInstantiationInc( veq[1], pv, veq_c, 0, subs, vars, coeff, has_coeff, subs_typ, i, lems ) ){ - return true; + Node veq; + if( QuantArith::isolate( pv, msum, veq, EQUAL, true )!=0 ){ + Trace("cegqi-si-inst-debug") << "...isolated equality " << veq << "." << std::endl; + Node veq_c; + if( veq[0]!=pv ){ + Node veq_v; + if( QuantArith::getMonomial( veq[0], veq_c, veq_v ) ){ + Assert( veq_v==pv ); + } + } + if( subs_proc[0][veq[1]].find( veq_c )==subs_proc[0][veq[1]].end() ){ + subs_proc[0][veq[1]][veq_c] = true; + if( addInstantiationInc( veq[1], pv, veq_c, 0, subs, vars, coeff, has_coeff, subs_typ, i, lems, effort ) ){ + return true; + } } } } } } + lhs.push_back( ns ); + lhs_v.push_back( hasVar ); + lhs_coeff.push_back( pv_coeff ); } - lhs.push_back( ns ); - lhs_v.push_back( hasVar ); - lhs_coeff.push_back( pv_coeff ); } + ++eqc_i; } - ++eqc_i; } + ++eqcs_i; } - ++eqcs_i; } - } - - //[3] directly look at assertions - TheoryId tid = Theory::theoryOf( pv ); - Theory* theory = d_qe->getTheoryEngine()->theoryOf( tid ); - if (theory && d_qe->getTheoryEngine()->isTheoryEnabled(tid)) { - context::CDList::const_iterator it = theory->facts_begin(), it_end = theory->facts_end(); - for (unsigned j = 0; it != it_end; ++ it, ++j) { - Node lit = (*it).assertion; - Node atom = lit.getKind()==NOT ? lit[0] : lit; - bool pol = lit.getKind()!=NOT; - if( tid==THEORY_ARITH ){ - if( atom.getKind()==GEQ ){ - Assert( atom[1].isConst() ); - computeProgVars( atom[0] ); - //must be an eligible term - if( d_inelig.find( atom[0] )==d_inelig.end() ){ - //apply substitution to LHS of atom - Node atom_lhs; - Node atom_rhs; - if( !d_prog_var[atom[0]].empty() ){ - Node atom_lhs_coeff; - atom_lhs = applySubstitution( atom[0], subs, vars, coeff, has_coeff, atom_lhs_coeff ); - if( !atom_lhs.isNull() ){ - computeProgVars( atom_lhs ); - atom_rhs = atom[1]; - if( !atom_lhs_coeff.isNull() ){ - atom_rhs = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, atom_lhs_coeff, atom_rhs ) ); + + //[3] directly look at assertions + TheoryId tid = Theory::theoryOf( pv ); + Theory* theory = d_qe->getTheoryEngine()->theoryOf( tid ); + if (theory && d_qe->getTheoryEngine()->isTheoryEnabled(tid)) { + context::CDList::const_iterator it = theory->facts_begin(), it_end = theory->facts_end(); + for (unsigned j = 0; it != it_end; ++ it, ++j) { + Node lit = (*it).assertion; + Node atom = lit.getKind()==NOT ? lit[0] : lit; + bool pol = lit.getKind()!=NOT; + if( tid==THEORY_ARITH ){ + if( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol ) ){ + Assert( atom[1].isConst() ); + computeProgVars( atom[0] ); + //must be an eligible term + if( d_inelig.find( atom[0] )==d_inelig.end() ){ + //apply substitution to LHS of atom + Node atom_lhs; + Node atom_rhs; + if( !d_prog_var[atom[0]].empty() ){ + Node atom_lhs_coeff; + atom_lhs = applySubstitution( atom[0], subs, vars, coeff, has_coeff, atom_lhs_coeff ); + if( !atom_lhs.isNull() ){ + computeProgVars( atom_lhs ); + atom_rhs = atom[1]; + if( !atom_lhs_coeff.isNull() ){ + atom_rhs = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, atom_lhs_coeff, atom_rhs ) ); + } } + }else{ + atom_lhs = atom[0]; + atom_rhs = atom[1]; } - }else{ - atom_lhs = atom[0]; - atom_rhs = atom[1]; - } - //if it contains pv - if( d_prog_var[atom_lhs].find( pv )!=d_prog_var[atom_lhs].end() ){ - Node satom = NodeManager::currentNM()->mkNode( GEQ, atom_lhs, atom_rhs ); - Trace("cegqi-si-inst-debug") << "From assertion : " << atom << ", pol = " << pol << std::endl; - Trace("cegqi-si-inst-debug") << " substituted : " << satom << ", pol = " << pol << std::endl; - std::map< Node, Node > msum; - if( QuantArith::getMonomialSumLit( satom, msum ) ){ - if( Trace.isOn("cegqi-si-inst-debug") ){ - Trace("cegqi-si-inst-debug") << "...got monomial sum: " << std::endl; - QuantArith::debugPrintMonomialSum( msum, "cegqi-si-inst-debug" ); - Trace("cegqi-si-inst-debug") << "isolate for " << pv << "..." << std::endl; - } - Node vatom; - //isolate pv in the inequality - int ires = QuantArith::isolate( pv, msum, vatom, atom.getKind(), true ); - if( ires!=0 ){ - Trace("cegqi-si-inst-debug") << "...isolated atom " << vatom << "." << std::endl; - Node val = vatom[ ires==1 ? 1 : 0 ]; - Node pvm = vatom[ ires==1 ? 0 : 1 ]; - //get monomial - Node veq_c; - if( pvm!=pv ){ - Node veq_v; - if( QuantArith::getMonomial( pvm, veq_c, veq_v ) ){ - Assert( veq_v==pv ); - } + //if it contains pv + if( !atom_lhs.isNull() && d_prog_var[atom_lhs].find( pv )!=d_prog_var[atom_lhs].end() ){ + Node satom = NodeManager::currentNM()->mkNode( atom.getKind(), atom_lhs, atom_rhs ); + Trace("cegqi-si-inst-debug") << "From assertion : " << atom << ", pol = " << pol << std::endl; + Trace("cegqi-si-inst-debug") << " substituted : " << satom << ", pol = " << pol << std::endl; + std::map< Node, Node > msum; + if( QuantArith::getMonomialSumLit( satom, msum ) ){ + if( Trace.isOn("cegqi-si-inst-debug") ){ + Trace("cegqi-si-inst-debug") << "...got monomial sum: " << std::endl; + QuantArith::debugPrintMonomialSum( msum, "cegqi-si-inst-debug" ); + Trace("cegqi-si-inst-debug") << "isolate for " << pv << "..." << std::endl; } - //push negation downwards - if( !pol ){ - ires = -ires; - if( pvtn.isInteger() ){ - val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( ires ) ) ); - val = Rewriter::rewrite( val ); - }else if( pvtn.isReal() ){ - //now is strict inequality - ires = ires*2; - }else{ - Assert( false ); + Node vatom; + //isolate pv in the inequality + int ires = QuantArith::isolate( pv, msum, vatom, atom.getKind(), true ); + if( ires!=0 ){ + Trace("cegqi-si-inst-debug") << "...isolated atom " << vatom << "." << std::endl; + Node val = vatom[ ires==1 ? 1 : 0 ]; + Node pvm = vatom[ ires==1 ? 0 : 1 ]; + //get monomial + Node veq_c; + if( pvm!=pv ){ + Node veq_v; + if( QuantArith::getMonomial( pvm, veq_c, veq_v ) ){ + Assert( veq_v==pv ); + } } - } - if( subs_proc[val].find( veq_c )==subs_proc[val].end() ){ - subs_proc[val][veq_c] = true; - if( addInstantiationInc( val, pv, veq_c, ires, subs, vars, coeff, has_coeff, subs_typ, i, lems ) ){ - return true; + //disequalities are both strict upper and lower bounds + unsigned rmax = atom.getKind()==GEQ ? 1 : 2; + for( unsigned r=0; rmkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) ); + uval = Rewriter::rewrite( uval ); + }else if( pvtn.isReal() ){ + //now is strict inequality + uires = uires*2; + }else{ + Assert( false ); + } + } + }else{ + Assert( atom.getKind()==EQUAL && !pol ); + if( pvtn.isInteger() ){ + uires = r==0 ? -1 : 1; + uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) ); + uval = Rewriter::rewrite( uval ); + }else if( pvtn.isReal() ){ + uires = r==0 ? -2 : 2; + }else{ + Assert( false ); + } + } + if( subs_proc[uires][uval].find( veq_c )==subs_proc[uires][uval].end() ){ + subs_proc[uires][uval][veq_c] = true; + if( addInstantiationInc( uval, pv, veq_c, uires, subs, vars, coeff, has_coeff, subs_typ, i, lems, effort ) ){ + return true; + } + } } } } @@ -666,17 +686,21 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::v } //[4] resort to using value in model - Node mv = d_qe->getModel()->getValue( pv ); - Node pv_coeff_m; - Trace("cegqi-si-inst-debug") << i << "...try model value " << mv << std::endl; - return addInstantiationInc( mv, pv, pv_coeff_m, 0, subs, vars, coeff, has_coeff, subs_typ, i, lems ); + if( effort>0 ){ + Node mv = d_qe->getModel()->getValue( pv ); + Node pv_coeff_m; + Trace("cegqi-si-inst-debug") << i << "...try model value " << mv << std::endl; + return addInstantiationInc( mv, pv, pv_coeff_m, 9, subs, vars, coeff, has_coeff, subs_typ, i, lems, 1 ); + }else{ + return false; + } } } bool CegConjectureSingleInv::addInstantiationInc( Node n, Node pv, Node pv_coeff, int styp, std::vector< Node >& subs, std::vector< Node >& vars, std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ, - unsigned i, std::vector< Node >& lems ) { + unsigned i, std::vector< Node >& lems, unsigned effort ) { //must ensure variables have been computed for n computeProgVars( n ); //substitute into previous substitutions, when applicable @@ -691,6 +715,7 @@ bool CegConjectureSingleInv::addInstantiationInc( Node n, Node pv, Node pv_coeff a_has_coeff.push_back( pv ); } + bool success = true; std::map< int, Node > prev_subs; std::map< int, Node > prev_coeff; std::vector< Node > new_has_coeff; @@ -701,46 +726,57 @@ bool CegConjectureSingleInv::addInstantiationInc( Node n, Node pv, Node pv_coeff TNode tv = pv; TNode ts = n; Node a_pv_coeff; - subs[j] = applySubstitution( subs[j], a_subs, a_var, a_coeff, a_has_coeff, a_pv_coeff, true ); - if( !a_pv_coeff.isNull() ){ - prev_coeff[j] = coeff[j]; - if( coeff[j].isNull() ){ - Assert( std::find( has_coeff.begin(), has_coeff.end(), vars[j] )==has_coeff.end() ); - //now has coefficient - new_has_coeff.push_back( vars[j] ); - has_coeff.push_back( vars[j] ); - coeff[j] = a_pv_coeff; - }else{ - coeff[j] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, coeff[j], a_pv_coeff ) ); + Node new_subs = applySubstitution( subs[j], a_subs, a_var, a_coeff, a_has_coeff, a_pv_coeff, true ); + if( !new_subs.isNull() ){ + subs[j] = new_subs; + if( !a_pv_coeff.isNull() ){ + prev_coeff[j] = coeff[j]; + if( coeff[j].isNull() ){ + Assert( std::find( has_coeff.begin(), has_coeff.end(), vars[j] )==has_coeff.end() ); + //now has coefficient + new_has_coeff.push_back( vars[j] ); + has_coeff.push_back( vars[j] ); + coeff[j] = a_pv_coeff; + }else{ + coeff[j] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, coeff[j], a_pv_coeff ) ); + } } - } - if( subs[j]!=prev_subs[j] ){ - computeProgVars( subs[j] ); + if( subs[j]!=prev_subs[j] ){ + computeProgVars( subs[j] ); + } + }else{ + success = false; + break; } } } - subs.push_back( n ); - vars.push_back( pv ); - coeff.push_back( pv_coeff ); - if( !pv_coeff.isNull() ){ - has_coeff.push_back( pv ); - } - subs_typ.push_back( styp ); - Trace("cegqi-si-inst-debug") << i << ": "; - if( !pv_coeff.isNull() ){ - Trace("cegqi-si-inst-debug") << pv_coeff << "*"; + if( success ){ + subs.push_back( n ); + vars.push_back( pv ); + coeff.push_back( pv_coeff ); + if( !pv_coeff.isNull() ){ + has_coeff.push_back( pv ); + } + subs_typ.push_back( styp ); + Trace("cegqi-si-inst-debug") << i << ": "; + if( !pv_coeff.isNull() ){ + Trace("cegqi-si-inst-debug") << pv_coeff << "*"; + } + Trace("cegqi-si-inst-debug") << pv << " -> " << n << std::endl; + success = addInstantiation( subs, vars, coeff, has_coeff, subs_typ, i+1, lems, effort ); + if( !success ){ + subs.pop_back(); + vars.pop_back(); + coeff.pop_back(); + if( !pv_coeff.isNull() ){ + has_coeff.pop_back(); + } + subs_typ.pop_back(); + } } - Trace("cegqi-si-inst-debug") << pv << " -> " << n << std::endl; - if( addInstantiation( subs, vars, coeff, has_coeff, subs_typ, i+1, lems ) ){ + if( success ){ return true; }else{ - subs.pop_back(); - vars.pop_back(); - coeff.pop_back(); - if( !pv_coeff.isNull() ){ - has_coeff.pop_back(); - } - subs_typ.pop_back(); //revert substitution information for( std::map< int, Node >::iterator it = prev_subs.begin(); it != prev_subs.end(); it++ ){ subs[it->first] = it->second; @@ -761,6 +797,7 @@ bool CegConjectureSingleInv::addInstantiationCoeff( std::vector< Node >& subs, s if( j==has_coeff.size() ){ return addInstantiation( subs, vars, subs_typ, lems ); }else{ + Assert( std::find( vars.begin(), vars.end(), has_coeff[j] )!=vars.end() ); unsigned index = std::find( vars.begin(), vars.end(), has_coeff[j] )-vars.begin(); Node prev = subs[index]; Assert( !coeff[index].isNull() ); @@ -787,7 +824,7 @@ bool CegConjectureSingleInv::addInstantiationCoeff( std::vector< Node >& subs, s subs[index] = veq[1]; if( !veq_c.isNull() ){ subs[index] = NodeManager::currentNM()->mkNode( INTS_DIVISION, veq[1], veq_c ); - if( subs_typ[index]>0 ){ + if( subs_typ[index]>=1 && subs_typ[index]<=2 ){ subs[index] = NodeManager::currentNM()->mkNode( PLUS, subs[index], NodeManager::currentNM()->mkNode( ITE, NodeManager::currentNM()->mkNode( EQUAL, @@ -801,8 +838,9 @@ bool CegConjectureSingleInv::addInstantiationCoeff( std::vector< Node >& subs, s Trace("cegqi-si-inst-debug") << "...normalize integers : " << subs[index] << std::endl; if( addInstantiationCoeff( subs, vars, coeff, has_coeff, subs_typ, j+1, lems ) ){ return true; - }else{ + } //equalities are both upper and lower bounds + /* if( subs_typ[index]==0 && !veq_c.isNull() ){ subs[index] = NodeManager::currentNM()->mkNode( PLUS, subs[index], NodeManager::currentNM()->mkNode( ITE, @@ -816,7 +854,7 @@ bool CegConjectureSingleInv::addInstantiationCoeff( std::vector< Node >& subs, s return true; } } - } + */ } } }else if( vars[index].getType().isReal() ){ @@ -844,17 +882,19 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::v prev[i] = subs[i]; if( d_n_delta.isNull() ){ d_n_delta = NodeManager::currentNM()->mkSkolem( "delta", vars[i].getType(), "delta for cegqi" ); - lems.push_back( NodeManager::currentNM()->mkNode( GT, d_n_delta, NodeManager::currentNM()->mkConst( Rational( 0 ) ) ) ); + Node delta_lem = NodeManager::currentNM()->mkNode( GT, d_n_delta, NodeManager::currentNM()->mkConst( Rational( 0 ) ) ); + d_qe->getOutputChannel().lemma( delta_lem ); } subs[i] = NodeManager::currentNM()->mkNode( subs_typ[i]==2 ? PLUS : MINUS, subs[i], d_n_delta ); } } - Trace("cegqi-engine") << " * single invocation: " << std::endl; + std::stringstream siss; + siss << " * single invocation: " << std::endl; for( unsigned j=0; j " << subs[j] << std::endl; + siss << " * " << v; + siss << " (" << vars[j] << ")"; + siss << " -> " << ( subs_typ[j]==9 ? "M:" : "") << subs[j] << std::endl; } //check if we have already added this instantiation bool alreadyExists; @@ -863,7 +903,8 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::v }else{ alreadyExists = !d_inst_match_trie.addInstMatch( d_qe, d_single_inv, subs ); } - Trace("cegqi-engine") << " * success = " << !alreadyExists << std::endl; + Trace("cegqi-si-inst-debug") << siss.str(); + Trace("cegqi-si-inst-debug") << " * success = " << !alreadyExists << std::endl; if( alreadyExists ){ //revert the substitution for( std::map< int, Node >::iterator it = prev.begin(); it != prev.end(); ++it ){ @@ -871,6 +912,7 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::v } return false; }else{ + Trace("cegqi-engine") << siss.str() << std::endl; Node lem = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), subs.begin(), subs.end() ); lem = Rewriter::rewrite( lem ); Trace("cegqi-si") << "Single invocation lemma : " << lem << std::endl; @@ -888,6 +930,7 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::v Node CegConjectureSingleInv::applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& vars, std::vector< Node >& coeff, std::vector< Node >& has_coeff, Node& pv_coeff, bool try_coeff ) { Assert( d_prog_var.find( n )!=d_prog_var.end() ); + Assert( n==Rewriter::rewrite( n ) ); bool req_coeff = false; if( !has_coeff.empty() ){ for( std::map< Node, bool >::iterator it = d_prog_var[n].begin(); it != d_prog_var[n].end(); ++it ){ @@ -900,7 +943,7 @@ Node CegConjectureSingleInv::applySubstitution( Node n, std::vector< Node >& sub if( !req_coeff ){ Node nret = n.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); if( n!=nret ){ - Rewriter::rewrite( nret ); + nret = Rewriter::rewrite( nret ); } //result is nret return nret; @@ -957,6 +1000,8 @@ Node CegConjectureSingleInv::applySubstitution( Node n, std::vector< Node >& sub nret = Rewriter::rewrite( nret ); //result is ( nret / pv_coeff ) return nret; + }else{ + Trace("cegqi-si-apply-subs-debug") << "Failed to find monomial sum " << n << std::endl; } } // failed to apply the substitution @@ -966,15 +1011,18 @@ Node CegConjectureSingleInv::applySubstitution( Node n, std::vector< Node >& sub void CegConjectureSingleInv::check( std::vector< Node >& lems ) { if( !d_single_inv.isNull() ) { - std::vector< Node > subs; - std::vector< Node > vars; - std::vector< Node > coeff; - std::vector< Node > has_coeff; - std::vector< int > subs_typ; - //try to add an instantiation - if( !addInstantiation( subs, vars, coeff, has_coeff, subs_typ, 0, lems ) ){ - Trace("cegqi-engine") << " WARNING : unable to find CEGQI single invocation instantiation." << std::endl; + for( unsigned r=0; r<2; r++ ){ + std::vector< Node > subs; + std::vector< Node > vars; + std::vector< Node > coeff; + std::vector< Node > has_coeff; + std::vector< int > subs_typ; + //try to add an instantiation + if( addInstantiation( subs, vars, coeff, has_coeff, subs_typ, 0, lems, r==0 ? 0 : 2 ) ){ + return; + } } + Trace("cegqi-engine") << " WARNING : unable to find CEGQI single invocation instantiation." << std::endl; } } diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h index b8865d243..3bc870d78 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h @@ -74,12 +74,13 @@ private: Node d_n_delta; //for adding instantiations during check void computeProgVars( Node n ); + // effort=0 : do not use model value, 1: use model value, 2: one must use model value bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ, - unsigned i, std::vector< Node >& lems ); + unsigned i, std::vector< Node >& lems, unsigned effort ); bool addInstantiationInc( Node n, Node pv, Node pv_coeff, int styp, std::vector< Node >& subs, std::vector< Node >& vars, std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ, - unsigned i, std::vector< Node >& lems ); + unsigned i, std::vector< Node >& lems, unsigned effort ); bool addInstantiationCoeff( std::vector< Node >& subs, std::vector< Node >& vars, std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ, unsigned j, std::vector< Node >& lems ); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 890f04aad..a475a8912 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -909,15 +909,7 @@ void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){ // Node req = qe->getPhaseReqEquality( f, trNodes[i] ); // trNodes[i] = NodeManager::currentNM()->mkNode( EQUAL, trNodes[i], req ); //} - if( nodeChanged ){ - Debug("literal-matching") << " Make " << prev << " -> " << nodes[i] << std::endl; - ++(d_statistics.d_lit_phase_req); - }else{ - ++(d_statistics.d_lit_phase_nreq); - } } - }else{ - d_statistics.d_lit_phase_nreq += (int)nodes.size(); } } @@ -961,8 +953,6 @@ QuantifiersEngine::Statistics::Statistics(): d_instantiations("QuantifiersEngine::Instantiations_Total", 0), d_inst_duplicate("QuantifiersEngine::Duplicate_Inst", 0), d_inst_duplicate_eq("QuantifiersEngine::Duplicate_Inst_Eq", 0), - d_lit_phase_req("QuantifiersEngine::lit_phase_req", 0), - d_lit_phase_nreq("QuantifiersEngine::lit_phase_nreq", 0), d_triggers("QuantifiersEngine::Triggers", 0), d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0), d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0), @@ -974,8 +964,6 @@ QuantifiersEngine::Statistics::Statistics(): StatisticsRegistry::registerStat(&d_instantiations); StatisticsRegistry::registerStat(&d_inst_duplicate); StatisticsRegistry::registerStat(&d_inst_duplicate_eq); - StatisticsRegistry::registerStat(&d_lit_phase_req); - StatisticsRegistry::registerStat(&d_lit_phase_nreq); StatisticsRegistry::registerStat(&d_triggers); StatisticsRegistry::registerStat(&d_simple_triggers); StatisticsRegistry::registerStat(&d_multi_triggers); @@ -989,8 +977,6 @@ QuantifiersEngine::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_instantiations); StatisticsRegistry::unregisterStat(&d_inst_duplicate); StatisticsRegistry::unregisterStat(&d_inst_duplicate_eq); - StatisticsRegistry::unregisterStat(&d_lit_phase_req); - StatisticsRegistry::unregisterStat(&d_lit_phase_nreq); StatisticsRegistry::unregisterStat(&d_triggers); StatisticsRegistry::unregisterStat(&d_simple_triggers); StatisticsRegistry::unregisterStat(&d_multi_triggers); diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index bdb2795b4..3ed6d369f 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -315,8 +315,6 @@ public: IntStat d_instantiations; IntStat d_inst_duplicate; IntStat d_inst_duplicate_eq; - IntStat d_lit_phase_req; - IntStat d_lit_phase_nreq; IntStat d_triggers; IntStat d_simple_triggers; IntStat d_multi_triggers;