From 331ec1abc311a6be85eb5adc0ca70f4e3c0c79a2 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 19 Aug 2015 09:35:17 +0200 Subject: [PATCH] Implementation of model-based projection in cbqi, cleanup, add regressions. --- .../quantifiers/ce_guided_single_inv.cpp | 28 +- src/theory/quantifiers/ce_guided_single_inv.h | 4 +- src/theory/quantifiers/inst_strategy_cbqi.cpp | 692 ++++++++++-------- src/theory/quantifiers/inst_strategy_cbqi.h | 34 +- src/theory/quantifiers/term_database.cpp | 9 +- src/theory/quantifiers_engine.cpp | 9 +- test/regress/regress0/quantifiers/Makefile.am | 4 +- .../regress0/quantifiers/RND-small.smt2 | 9 + .../regress0/quantifiers/clock-10.smt2 | 5 + 9 files changed, 463 insertions(+), 331 deletions(-) create mode 100644 test/regress/regress0/quantifiers/RND-small.smt2 create mode 100644 test/regress/regress0/quantifiers/clock-10.smt2 diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index 4308e5172..17d85eb9b 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -32,8 +32,8 @@ using namespace std; namespace CVC4 { -bool CegqiOutputSingleInv::addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ) { - return d_out->addInstantiation( subs, subs_typ ); +bool CegqiOutputSingleInv::addInstantiation( std::vector< Node >& subs ) { + return d_out->addInstantiation( subs ); } bool CegqiOutputSingleInv::isEligibleForInstantiation( Node n ) { @@ -76,7 +76,8 @@ Node CegConjectureSingleInv::getSingleInvLemma( Node guard ) { //initialize the instantiator for this if( !d_single_inv_sk.empty() ){ CegqiOutputSingleInv * cosi = new CegqiOutputSingleInv( this ); - d_cinst = new CegInstantiator( d_qe, cosi ); + // third and fourth arguments set to (false,false) until we have solution reconstruction for delta and infinity + d_cinst = new CegInstantiator( d_qe, cosi, false, false ); d_cinst->d_vars.insert( d_cinst->d_vars.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() ); }else{ d_cinst = NULL; @@ -694,7 +695,7 @@ bool CegConjectureSingleInv::analyzeSygusTerm( Node n, std::map< Node, std::vect return true; } -bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ){ +bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs ){ std::stringstream siss; if( Trace.isOn("cegqi-si-inst-debug") || Trace.isOn("cegqi-engine") ){ siss << " * single invocation: " << std::endl; @@ -702,7 +703,7 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::v Node v = d_single_inv_map_to_prog[d_single_inv[0][j]]; siss << " * " << v; siss << " (" << d_single_inv_sk[j] << ")"; - siss << " -> " << ( subs_typ[j]==9 ? "M:" : "") << subs[j] << std::endl; + siss << " -> " << subs[j] << std::endl; } } bool alreadyExists; @@ -719,7 +720,9 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::v 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() ); Node delta = d_qe->getTermDatabase()->getVtsDelta( false, false ); - if( !delta.isNull() && TermDb::containsTerm( lem, delta ) ){ + Node inf = d_qe->getTermDatabase()->getVtsInfinity( false, false ); + if( ( !delta.isNull() && TermDb::containsTerm( lem, delta ) ) || + ( !inf.isNull() && TermDb::containsTerm( lem, inf ) ) ){ Trace("cegqi-engine-debug") << "Rewrite based on vts symbols..." << std::endl; lem = d_qe->getTermDatabase()->rewriteVtsSymbols( lem ); } @@ -748,15 +751,10 @@ bool CegConjectureSingleInv::addLemma( Node n ) { void CegConjectureSingleInv::check( std::vector< Node >& lems ) { if( !d_single_inv.isNull() && d_cinst!=NULL ) { d_curr_lemmas.clear(); - //check if there are delta lemmas - d_cinst->getDeltaLemmas( lems ); - //if not, do ce-guided instantiation - if( lems.empty() ){ - //call check for instantiator - d_cinst->check(); - //add lemmas - lems.insert( lems.end(), d_curr_lemmas.begin(), d_curr_lemmas.end() ); - } + //call check for instantiator + d_cinst->check(); + //add lemmas + lems.insert( lems.end(), d_curr_lemmas.begin(), d_curr_lemmas.end() ); } } diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h index 69981791f..2c955db5d 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h @@ -36,7 +36,7 @@ public: CegqiOutputSingleInv( CegConjectureSingleInv * out ) : d_out( out ){} ~CegqiOutputSingleInv() {} CegConjectureSingleInv * d_out; - bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ); + bool addInstantiation( std::vector< Node >& subs ); bool isEligibleForInstantiation( Node n ); bool addLemma( Node lem ); }; @@ -97,7 +97,7 @@ public: private: std::vector< Node > d_curr_lemmas; //add instantiation - bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ); + bool addInstantiation( std::vector< Node >& subs ); //is eligible for instantiation bool isEligibleForInstantiation( Node n ); // add lemma diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index d9ac190dc..dcbb79a35 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -31,11 +31,12 @@ using namespace CVC4::theory::arith; using namespace CVC4::theory::datatypes; #define ARITH_INSTANTIATOR_USE_MINUS_DELTA +//#define MBP_STRICT_ASSERTIONS - -CegInstantiator::CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out ) : d_qe( qe ), d_out( out ){ +CegInstantiator::CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out, bool use_vts_delta, bool use_vts_inf ) : +d_qe( qe ), d_out( out ), d_use_vts_delta( use_vts_delta ), d_use_vts_inf( use_vts_inf ){ d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); d_true = NodeManager::currentNM()->mkConst( true ); @@ -64,26 +65,28 @@ void CegInstantiator::computeProgVars( Node n ){ } bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, - std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ, + std::vector< Node >& coeff, std::vector< Node >& has_coeff, Node theta, unsigned i, unsigned effort ){ if( i==d_vars.size() ){ - return addInstantiationCoeff( subs, vars, coeff, has_coeff, subs_typ, 0 ); + return addInstantiationCoeff( subs, vars, coeff, has_coeff, 0 ); }else{ eq::EqualityEngine* ee = d_qe->getMasterEqualityEngine(); - std::map< int, std::map< Node, std::map< Node, bool > > > subs_proc; + 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_vars[i]; TypeNode pvtn = pv.getType(); + //if in effort=2, we must choose at least one model value if( (i+1)hasTerm( pv ) ){ + //std::vector< Node > eqc_sk; 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") << "[1] " << i << "...try based on equal term " << n << std::endl; + Trace("cbqi-inst-debug") << "[1] " << 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 @@ -96,7 +99,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< 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(); + 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; @@ -104,12 +107,16 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< } 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, effort ) ){ + subs_proc[ns][pv_coeff] = true; + if( addInstantiationInc( ns, pv, pv_coeff, subs, vars, coeff, has_coeff, theta, i, effort ) ){ return true; } } } + //record this as skolem + //if( n.getKind()==SKOLEM ){ + // eqc_sk.push_back( n ); + //} } ++eqc_i; } @@ -117,6 +124,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< //[2] : we can solve an equality for pv ///iterate over equivalence classes to find cases where we can solve for the variable + Node vts_inf = d_qe->getTermDatabase()->getVtsInfinity( false, false ); if( pvtn.isInteger() || pvtn.isReal() ){ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); while( !eqcs_i.isFinished() ){ @@ -147,46 +155,56 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< 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; + Trace("cbqi-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; - } - 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 ); - } + //cannot contain infinity + if( vts_inf.isNull() || !TermDb::containsTerm( eq, vts_inf ) ){ + Trace("cbqi-inst-debug") << "...equality is " << eq << std::endl; + std::map< Node, Node > msum; + if( QuantArith::getMonomialSumLit( eq, msum ) ){ + if( Trace.isOn("cbqi-inst-debug") ){ + Trace("cbqi-inst-debug") << "...got monomial sum: " << std::endl; + QuantArith::debugPrintMonomialSum( msum, "cbqi-inst-debug" ); + Trace("cbqi-inst-debug") << "isolate for " << pv << "..." << std::endl; } - 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, effort ) ){ - return true; + Node veq; + if( QuantArith::isolate( pv, msum, veq, EQUAL, true )!=0 ){ + Trace("cbqi-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 val = veq[1]; + //eliminate coefficient if real + if( !pvtn.isInteger() && !veq_c.isNull() ){ + val = NodeManager::currentNM()->mkNode( MULT, val, NodeManager::currentNM()->mkConst( Rational(1) / veq_c.getConst() ) ); + val = Rewriter::rewrite( val ); + veq_c = Node::null(); + } + if( subs_proc[val].find( veq_c )==subs_proc[val].end() ){ + subs_proc[val][veq_c] = true; + if( addInstantiationInc( val, pv, veq_c, subs, vars, coeff, has_coeff, theta, i, effort ) ){ + return true; + } } } } @@ -206,17 +224,21 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< } //[3] directly look at assertions + std::vector< Node > mbp_bounds[2]; + std::vector< Node > mbp_coeff[2]; + std::vector< bool > mbp_strict[2]; + std::vector< Node > mbp_lit[2]; unsigned rmax = Theory::theoryOf( pv )==Theory::theoryOf( pv.getType() ) ? 1 : 2; for( unsigned r=0; rgetTheoryEngine()->theoryOf( tid ); - Trace("cegqi-si-inst-debug2") << "Theory of " << pv << " (r=" << r << ") is " << tid << std::endl; + Trace("cbqi-inst-debug2") << "Theory of " << pv << " (r=" << r << ") is " << tid << std::endl; if (theory && d_qe->getTheoryEngine()->isTheoryEnabled(tid)) { - Trace("cegqi-si-inst-debug2") << "Look at assertions of " << tid << std::endl; + Trace("cbqi-inst-debug2") << "Look at assertions of " << tid << std::endl; 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; - Trace("cegqi-si-inst-debug2") << " look at " << lit << std::endl; + 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 @@ -247,71 +269,101 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< } } } - //if it contains pv + //if it contains pv, not infinity 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") << "[3] 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 ); - } + //cannot contain infinity + if( vts_inf.isNull() || !TermDb::containsTerm( atom_lhs, vts_inf ) ){ + Trace("cbqi-inst-debug") << "[3] From assertion : " << atom << ", pol = " << pol << std::endl; + Trace("cbqi-inst-debug") << " substituted : " << satom << ", pol = " << pol << std::endl; + std::map< Node, Node > msum; + if( QuantArith::getMonomialSumLit( satom, msum ) ){ + if( Trace.isOn("cbqi-inst-debug") ){ + Trace("cbqi-inst-debug") << "...got monomial sum: " << std::endl; + QuantArith::debugPrintMonomialSum( msum, "cbqi-inst-debug" ); + Trace("cbqi-inst-debug") << "isolate for " << pv << "..." << std::endl; } - //disequalities are both strict upper and lower bounds - unsigned rmax = atom.getKind()==GEQ ? 1 : 2; - for( unsigned r=0; rmkNode( MULT, val, NodeManager::currentNM()->mkConst( Rational(1) / veq_c.getConst() ) ); + val = Rewriter::rewrite( val ); + veq_c = Node::null(); + } + + //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{ + Assert( pvtn.isReal() ); + //now is strict inequality + uires = uires*2; + } + } + }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() ){ - //now is strict inequality - uires = uires*2; }else{ - Assert( false ); + Assert( pvtn.isReal() ); + uires = r==0 ? -2 : 2; } } - }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 ); + Trace("cbqi-bound-inf") << "From " << lit << ", got : "; + if( !veq_c.isNull() ){ + Trace("cbqi-bound-inf") << veq_c << " * "; } - } - 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, effort ) ){ - return true; + Trace("cbqi-bound-inf") << pv << " -> " << uval << ", styp = " << uires << std::endl; + if( options::cbqiModel() ){ + //just store bounds, will choose based on tighest bound + unsigned index = uires>0 ? 0 : 1; + mbp_bounds[index].push_back( uval ); + mbp_coeff[index].push_back( veq_c ); + mbp_strict[index].push_back( uires==2 || uires==-2 ); + mbp_lit[index].push_back( lit ); + }else{ + //take into account delta + if( uires==2 || uires==-2 ){ + if( d_use_vts_delta ){ + Node delta = d_qe->getTermDatabase()->getVtsDelta(); + uval = NodeManager::currentNM()->mkNode( uires==2 ? PLUS : MINUS, uval, delta ); + uval = Rewriter::rewrite( uval ); + } + } + if( subs_proc[uval].find( veq_c )==subs_proc[uval].end() ){ + subs_proc[uval][veq_c] = true; + if( addInstantiationInc( uval, pv, veq_c, subs, vars, coeff, has_coeff, theta, i, effort ) ){ + return true; + } + }else{ + Trace("cbqi-inst-debug") << "...already processed." << std::endl; + } } - }else{ - Trace("cegqi-si-inst-debug") << "...already processed." << std::endl; } } } @@ -322,14 +374,104 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< } } } + if( options::cbqiModel() ){ + if( pvtn.isInteger() || pvtn.isReal() ){ + bool upper_first = false; + unsigned best_used[2]; + std::vector< Node > t_values[2]; + Node pv_value = d_qe->getModel()->getValue( pv ); + Trace("cbqi-bound2") << "...M( " << pv << " ) = " << pv_value << std::endl; + //try optimal bounds + for( unsigned r=0; r<2; r++ ){ + int rr = upper_first ? (1-r) : r; + if( mbp_bounds[rr].empty() ){ + /* + if( d_use_vts_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(); + if( rr==0 ){ + val = NodeManager::currentNM()->mkNode( UMINUS, val ); + val = Rewriter::rewrite( val ); + } + if( addInstantiationInc( val, pv, Node::null(), subs, vars, coeff, has_coeff, theta, i, effort ) ){ + return true; + } + } + */ + }else{ + Trace("cbqi-bound") << ( rr==0 ? "Lower" : "Upper" ) << " bounds for " << pv << " (type=" << pvtn << ") : " << std::endl; + int best = -1; + Node best_bound_value; + for( unsigned j=0; jgetModel()->getValue( mbp_bounds[rr][j] ); + t_values[rr].push_back( t_value ); + Trace("cbqi-bound2") << "...M( " << mbp_bounds[rr][j] << " ) = " << t_value << std::endl; + Node value = t_value; + Trace("cbqi-bound") << " " << j << ": " << mbp_bounds[rr][j]; + if( !mbp_coeff[rr][j].isNull() ){ + Trace("cbqi-bound") << " (div " << mbp_coeff[rr][j] << ")"; + Assert( mbp_coeff[rr][j].isConst() ); + value = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(1) / mbp_coeff[rr][j].getConst() ), value ); + value = Rewriter::rewrite( value ); + } + if( mbp_strict[rr][j] ){ + Trace("cbqi-bound") << " (strict)"; + } + Trace("cbqi-bound") << ", value = " << value << std::endl; + bool new_best = false; + if( best==-1 ){ + new_best = true; + }else{ + Kind k = rr==0 ? GEQ : LEQ; + Node cmp_bound = NodeManager::currentNM()->mkNode( k, value, best_bound_value ); + cmp_bound = Rewriter::rewrite( cmp_bound ); + if( cmp_bound==d_true && ( !mbp_strict[rr][best] || mbp_strict[rr][j] ) ){ + new_best = true; + } + } + if( new_best ){ + best_bound_value = value; + best = j; + } + } + if( best!=-1 ){ + Trace("cbqi-bound") << "...best bound is " << best << " : " << best_bound_value << std::endl; + best_used[rr] = (unsigned)best; + Node val = getModelBasedProjectionValue( mbp_bounds[rr][best], mbp_strict[rr][best], rr==0, mbp_coeff[rr][best], pv_value, t_values[rr][best], theta ); + if( !val.isNull() && addInstantiationInc( val, pv, mbp_coeff[rr][best], subs, vars, coeff, has_coeff, theta, i, effort ) ){ + return true; + } + } + } + } + //try non-optimal bounds (heuristic) + for( unsigned r=0; r<2; r++ ){ + int rr = upper_first ? (1-r) : r; + for( unsigned j=0; j0 ){ + if( effort>0 || ( pvtn.isBoolean() && ( (i+1)getModel()->getValue( pv ); Node pv_coeff_m; - Trace("cegqi-si-inst-debug") << i << "[4] ...try model value " << mv << std::endl; - return addInstantiationInc( mv, pv, pv_coeff_m, 9, subs, vars, coeff, has_coeff, subs_typ, i, 1 ); + Trace("cbqi-inst-debug") << "[4] " << i << "...try model value " << mv << std::endl; + int new_effort = pvtn.isBoolean() ? effort : 1; +#ifdef MBP_STRICT_ASSERTIONS + //we only resort to values in the case of booleans + Assert( pvtn.isBoolean() ); +#endif + return addInstantiationInc( mv, pv, pv_coeff_m, subs, vars, coeff, has_coeff, theta, i, new_effort ); }else{ return false; } @@ -337,13 +479,17 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< } -bool CegInstantiator::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, unsigned effort ) { - if( styp==2 || styp==-2 ){ - Node delta = d_qe->getTermDatabase()->getVtsDelta(); - n = NodeManager::currentNM()->mkNode( styp==2 ? PLUS : MINUS, n, delta ); - n = Rewriter::rewrite( n ); +bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, std::vector< Node >& subs, std::vector< Node >& vars, + std::vector< Node >& coeff, std::vector< Node >& has_coeff, Node theta, unsigned i, unsigned effort ) { + if( Trace.isOn("cbqi-inst") ){ + for( unsigned i=0; i " << n << std::endl; } //must ensure variables have been computed for n computeProgVars( n ); @@ -389,6 +535,7 @@ bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int s computeProgVars( subs[j] ); } }else{ + Trace("cbqi-inst-debug") << "...failed to apply substitution to " << subs[j] << std::endl; success = false; break; } @@ -401,13 +548,21 @@ bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int s if( !pv_coeff.isNull() ){ has_coeff.push_back( pv ); } - subs_typ.push_back( styp ); - Trace("cegqi-si-inst-debug") << i << ": "; + Trace("cbqi-inst-debug") << i << ": "; if( !pv_coeff.isNull() ){ - Trace("cegqi-si-inst-debug") << pv_coeff << "*"; + Trace("cbqi-inst-debug") << pv_coeff << "*"; } - Trace("cegqi-si-inst-debug") << pv << " -> " << n << std::endl; - success = addInstantiation( subs, vars, coeff, has_coeff, subs_typ, i+1, effort ); + Trace("cbqi-inst-debug") << pv << " -> " << n << std::endl; + Node new_theta = theta; + if( !pv_coeff.isNull() ){ + if( new_theta.isNull() ){ + new_theta = pv_coeff; + }else{ + new_theta = NodeManager::currentNM()->mkNode( MULT, new_theta, pv_coeff ); + new_theta = Rewriter::rewrite( new_theta ); + } + } + success = addInstantiation( subs, vars, coeff, has_coeff, new_theta, i+1, effort ); if( !success ){ subs.pop_back(); vars.pop_back(); @@ -415,7 +570,6 @@ bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int s if( !pv_coeff.isNull() ){ has_coeff.pop_back(); } - subs_typ.pop_back(); } } if( success ){ @@ -436,88 +590,83 @@ bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int s } bool CegInstantiator::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 >& coeff, std::vector< Node >& has_coeff, unsigned j ) { if( j==has_coeff.size() ){ - return addInstantiation( subs, vars, subs_typ ); + return addInstantiation( subs, vars ); }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() ); - Trace("cegqi-si-inst-debug") << "Normalize substitution for " << coeff[index] << " * " << vars[index] << " = " << subs[index] << ", stype = " << subs_typ[index] << std::endl; - if( vars[index].getType().isInteger() ){ - //must ensure that divisibility constraints are met - //solve updated rewritten equality for vars[index], if coefficient is one, then we are successful - Node eq_lhs = NodeManager::currentNM()->mkNode( MULT, coeff[index], vars[index] ); - Node eq_rhs = subs[index]; - 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 ) ){ - Node veq; - if( QuantArith::isolate( vars[index], msum, veq, EQUAL, true )!=0 ){ - Node veq_c; - if( veq[0]!=vars[index] ){ - Node veq_v; - if( QuantArith::getMonomial( veq[0], veq_c, veq_v ) ){ - Assert( veq_v==vars[index] ); - } + Trace("cbqi-inst-debug") << "Normalize substitution for " << coeff[index] << " * " << vars[index] << " = " << subs[index] << std::endl; + Assert( vars[index].getType().isInteger() ); + //must ensure that divisibility constraints are met + //solve updated rewritten equality for vars[index], if coefficient is one, then we are successful + Node eq_lhs = NodeManager::currentNM()->mkNode( MULT, coeff[index], vars[index] ); + Node eq_rhs = subs[index]; + Node eq = eq_lhs.eqNode( eq_rhs ); + eq = Rewriter::rewrite( eq ); + Trace("cbqi-inst-debug") << "...equality is " << eq << std::endl; + std::map< Node, Node > msum; + if( QuantArith::getMonomialSumLit( eq, msum ) ){ + Node veq; + if( QuantArith::isolate( vars[index], msum, veq, EQUAL, true )!=0 ){ + Node veq_c; + if( veq[0]!=vars[index] ){ + Node veq_v; + if( QuantArith::getMonomial( veq[0], veq_c, veq_v ) ){ + Assert( veq_v==vars[index] ); } - subs[index] = veq[1]; - if( !veq_c.isNull() ){ - subs[index] = NodeManager::currentNM()->mkNode( INTS_DIVISION, veq[1], veq_c ); - 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, - NodeManager::currentNM()->mkNode( INTS_MODULUS, veq[1], veq_c ), - d_zero ), - d_zero, d_one ) - ); - } - } - Trace("cegqi-si-inst-debug") << "...normalize integers : " << subs[index] << std::endl; - if( addInstantiationCoeff( subs, vars, coeff, has_coeff, subs_typ, j+1 ) ){ - return true; + } + subs[index] = veq[1]; + if( !veq_c.isNull() ){ + subs[index] = NodeManager::currentNM()->mkNode( INTS_DIVISION, veq[1], veq_c ); + /* + 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, + NodeManager::currentNM()->mkNode( INTS_MODULUS, veq[1], veq_c ), + d_zero ), + d_zero, d_one ) + ); } - //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, - NodeManager::currentNM()->mkNode( EQUAL, - NodeManager::currentNM()->mkNode( INTS_MODULUS, veq[1], veq_c ), - NodeManager::currentNM()->mkConst( Rational( 0 ) ) ), - NodeManager::currentNM()->mkConst( Rational( 0 ) ), - NodeManager::currentNM()->mkConst( Rational( 1 ) ) ) - ); - if( addInstantiationCoeff( subs, vars, coeff, has_coeff, subs_typ, j+1 ) ){ - return true; - } - } - */ + */ } + Trace("cbqi-inst-debug") << "...normalize integers : " << subs[index] << std::endl; + if( addInstantiationCoeff( subs, vars, coeff, has_coeff, j+1 ) ){ + return true; + } + //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, + NodeManager::currentNM()->mkNode( EQUAL, + NodeManager::currentNM()->mkNode( INTS_MODULUS, veq[1], veq_c ), + NodeManager::currentNM()->mkConst( Rational( 0 ) ) ), + NodeManager::currentNM()->mkConst( Rational( 0 ) ), + NodeManager::currentNM()->mkConst( Rational( 1 ) ) ) + ); + if( addInstantiationCoeff( subs, vars, coeff, has_coeff, j+1 ) ){ + return true; + } + } + */ } - }else if( vars[index].getType().isReal() ){ - // can always invert - subs[index] = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(1) / coeff[index].getConst() ), subs[index] ); - subs[index] = Rewriter::rewrite( subs[index] ); - Trace("cegqi-si-inst-debug") << "...success, reals : " << subs[index] << std::endl; - if( addInstantiationCoeff( subs, vars, coeff, has_coeff, subs_typ, j+1 ) ){ - return true; - } - }else{ - Assert( false ); } subs[index] = prev; - Trace("cegqi-si-inst-debug") << "...failed." << std::endl; + Trace("cbqi-inst-debug") << "...failed." << std::endl; return false; } } -bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::vector< int >& subs_typ ) { - return d_out->addInstantiation( subs, subs_typ ); +bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars ) { + bool ret = d_out->addInstantiation( subs ); +#ifdef MBP_STRICT_ASSERTIONS + Assert( ret ); +#endif + return ret; } @@ -603,88 +752,71 @@ Node CegInstantiator::applySubstitution( Node n, std::vector< Node >& subs, std: } } -//check if delta has a lower bound L -// if so, add lemma L>0 => L>d -void CegInstantiator::getDeltaLemmas( std::vector< Node >& lems ) { - return; - /* disable for now - if( !d_n_delta.isNull() ){ - Theory* theory = d_qe->getTheoryEngine()->theoryOf( THEORY_ARITH ); - if( theory && d_qe->getTheoryEngine()->isTheoryEnabled( THEORY_ARITH ) ){ - 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( atom.getKind()==GEQ || ( pol && atom.getKind()==EQUAL ) ){ - Assert( atom.getKind()!=GEQ || atom[1].isConst() ); - Node atom_lhs; - Node atom_rhs; - if( atom.getKind()==GEQ ){ - atom_lhs = atom[0]; - atom_rhs = atom[1]; - }else{ - atom_lhs = NodeManager::currentNM()->mkNode( MINUS, atom[0], atom[1] ); - atom_lhs = Rewriter::rewrite( atom_lhs ); - atom_rhs = d_zero; - } - computeProgVars( atom_lhs ); - //must be an eligible term with delta - if( d_inelig.find( atom_lhs )==d_inelig.end() && d_has_delta.find( atom_lhs )!=d_has_delta.end() ){ - Node satom = NodeManager::currentNM()->mkNode( atom.getKind(), atom_lhs, atom_rhs ); - Trace("cegqi-delta") << "Delta assertion : " << atom << ", pol = " << pol << std::endl; - std::map< Node, Node > msum; - if( QuantArith::getMonomialSumLit( satom, msum ) ){ - Node vatom; - //isolate delta in the inequality - int ires = QuantArith::isolate( d_n_delta, msum, vatom, atom.getKind(), true ); - if( ((ires==1)==pol) || ( ires!=0 && lit.getKind()==EQUAL ) ){ - Node val = vatom[ ires==1 ? 1 : 0 ]; - Node pvm = vatom[ ires==1 ? 0 : 1 ]; - //get monomial - if( pvm!=d_n_delta ){ - Node veq_c; - Node veq_v; - if( QuantArith::getMonomial( pvm, veq_c, veq_v ) ){ - Assert( veq_v==d_n_delta ); - val = NodeManager::currentNM()->mkNode( MULT, val, NodeManager::currentNM()->mkConst( Rational(1) / veq_c.getConst() ) ); - val = Rewriter::rewrite( val ); - }else{ - val = Node::null(); - } - } - if( !val.isNull() ){ - Node lem1 = NodeManager::currentNM()->mkNode( GT, val, d_zero ); - lem1 = Rewriter::rewrite( lem1 ); - if( !lem1.isConst() || lem1==d_true ){ - Node lem2 = NodeManager::currentNM()->mkNode( GT, val, d_n_delta ); - Node lem = lem1==d_true ? lem2 : NodeManager::currentNM()->mkNode( OR, lem1.negate(), lem2 ); - lems.push_back( lem ); - Trace("cegqi-delta") << "...lemma : " << lem << std::endl; - } - } - }else{ - Trace("cegqi-delta") << "...wrong polarity." << std::endl; - } - } - } - } - } +Node CegInstantiator::getModelBasedProjectionValue( Node t, bool strict, bool isLower, Node c, Node me, Node mt, Node theta ) { + Node val = t; + Trace("cbqi-bound2") << "Value : " << val << std::endl; + //take into account strictness + if( strict ){ + if( !d_use_vts_delta ){ + return Node::null(); + }else{ + Node delta = d_qe->getTermDatabase()->getVtsDelta(); + Kind k = isLower ? PLUS : MINUS; + val = NodeManager::currentNM()->mkNode( k, val, delta ); + val = Rewriter::rewrite( val ); + Trace("cbqi-bound2") << "(after strict) : " << val << std::endl; } } - */ + //add rho value + //get the value of c*e + Node ceValue = me; + Node new_theta = theta; + if( !c.isNull() ){ + ceValue = NodeManager::currentNM()->mkNode( MULT, ceValue, c ); + ceValue = Rewriter::rewrite( ceValue ); + if( new_theta.isNull() ){ + new_theta = c; + }else{ + 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; + } + if( !new_theta.isNull() ){ + Node rho; + if( isLower ){ + rho = NodeManager::currentNM()->mkNode( MINUS, ceValue, mt ); + }else{ + 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 << " = "; + rho = NodeManager::currentNM()->mkNode( INTS_MODULUS_TOTAL, rho, new_theta ); + rho = Rewriter::rewrite( rho ); + Trace("cbqi-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; + } + return val; } bool CegInstantiator::check() { - + if( d_qe->getTheoryEngine()->needCheck() ){ + Trace("cegqi-engine") << " CEGQI instantiator : wait until all ground theories are finished." << std::endl; + return false; + } 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; + Node theta; //try to add an instantiation - if( addInstantiation( subs, vars, coeff, has_coeff, subs_typ, 0, r==0 ? 0 : 2 ) ){ + if( addInstantiation( subs, vars, coeff, has_coeff, theta, 0, r==0 ? 0 : 2 ) ){ return true; } } @@ -1015,8 +1147,8 @@ Node InstStrategySimplex::getTableauxValue( ArithVar v, bool minus_delta ){ //new implementation -bool CegqiOutputInstStrategy::addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ) { - return d_out->addInstantiation( subs, subs_typ ); +bool CegqiOutputInstStrategy::addInstantiation( std::vector< Node >& subs ) { + return d_out->addInstantiation( subs ); } bool CegqiOutputInstStrategy::isEligibleForInstantiation( Node n ) { @@ -1030,11 +1162,11 @@ bool CegqiOutputInstStrategy::addLemma( Node lem ) { InstStrategyCegqi::InstStrategyCegqi( QuantifiersEngine * qe ) : InstStrategy( qe ) { d_out = new CegqiOutputInstStrategy( this ); + d_small_const = NodeManager::currentNM()->mkConst( Rational(1)/Rational(1000000) ); } void InstStrategyCegqi::processResetInstantiationRound( Theory::Effort effort ) { - d_check_delta_lemma = true; - d_check_delta_lemma_lc = true; + d_check_vts_lemma_lc = true; } int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) { @@ -1052,31 +1184,6 @@ int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) { }else{ cinst = it->second; } - if( d_check_delta_lemma ){ - //minimize the free delta heuristically - Trace("inst-alg") << "-> Get delta lemmas for cegqi..." << std::endl; - Node delta = d_quantEngine->getTermDatabase()->getVtsDelta( true, false ); - if( !delta.isNull() ){ - if( d_n_delta_ub.isNull() ){ - d_n_delta_ub = NodeManager::currentNM()->mkConst( Rational(1)/Rational(1000000) ); - } - d_check_delta_lemma = false; - std::vector< Node > dlemmas; - cinst->getDeltaLemmas( dlemmas ); - Trace("inst-alg") << "...got " << dlemmas.size() << " delta lemmas." << std::endl; - if( !dlemmas.empty() ){ - bool addedLemma = false; - for( unsigned i=0; i Run cegqi for " << f << std::endl; d_curr_quant = f; bool addedLemma = cinst->check(); @@ -1084,22 +1191,31 @@ int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) { return addedLemma ? STATUS_UNKNOWN : STATUS_UNFINISHED; }else if( e==2 ){ //minimize the free delta heuristically on demand - if( d_check_delta_lemma_lc ){ + if( d_check_vts_lemma_lc ){ Node delta = d_quantEngine->getTermDatabase()->getVtsDelta( true, false ); - if( !delta.isNull() ){ - d_check_delta_lemma_lc = false; - d_n_delta_ub = NodeManager::currentNM()->mkNode( MULT, d_n_delta_ub, d_n_delta_ub ); - d_n_delta_ub = Rewriter::rewrite( d_n_delta_ub ); - Trace("cegqi") << "Delta lemma for " << d_n_delta_ub << std::endl; - Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, delta, d_n_delta_ub ); - d_quantEngine->getOutputChannel().lemma( delta_lem_ub ); + Node inf = d_quantEngine->getTermDatabase()->getVtsInfinity( true, false ); + if( !delta.isNull() || !inf.isNull() ){ + d_check_vts_lemma_lc = false; + d_small_const = NodeManager::currentNM()->mkNode( MULT, d_small_const, d_small_const ); + d_small_const = Rewriter::rewrite( d_small_const ); + //heuristic for now, until we know how to do nested quantification + if( !delta.isNull() ){ + Trace("cegqi") << "Delta lemma for " << d_small_const << std::endl; + Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, delta, d_small_const ); + d_quantEngine->getOutputChannel().lemma( delta_lem_ub ); + } + if( !inf.isNull() ){ + Trace("cegqi") << "Infinity lemma for " << d_small_const << std::endl; + Node inf_lem_lb = NodeManager::currentNM()->mkNode( GT, inf, NodeManager::currentNM()->mkConst( Rational(1)/d_small_const.getConst() ) ); + d_quantEngine->getOutputChannel().lemma( inf_lem_lb ); + } } } } return STATUS_UNKNOWN; } -bool InstStrategyCegqi::addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ) { +bool InstStrategyCegqi::addInstantiation( std::vector< Node >& subs ) { Assert( !d_curr_quant.isNull() ); /* std::stringstream siss; @@ -1113,16 +1229,20 @@ bool InstStrategyCegqi::addInstantiation( std::vector< Node >& subs, std::vector } */ //check if we need virtual term substitution (if used delta) - bool used_delta = false; + bool used_vts = false; Node delta = d_quantEngine->getTermDatabase()->getVtsDelta( false, false ); - if( !delta.isNull() ){ + Node inf = d_quantEngine->getTermDatabase()->getVtsInfinity( false, false ); + if( !delta.isNull() || !inf.isNull() ){ for( unsigned i=0; iaddInstantiation( d_curr_quant, subs, false, false, false, used_delta ); + return d_quantEngine->addInstantiation( d_curr_quant, subs, false, false, false, used_vts ); } bool InstStrategyCegqi::addLemma( Node lem ) { diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index 0e6227606..4f5049cd8 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -40,7 +40,7 @@ class CegqiOutput { public: virtual ~CegqiOutput() {} - virtual bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ) = 0; + virtual bool addInstantiation( std::vector< Node >& subs ) = 0; virtual bool isEligibleForInstantiation( Node n ) = 0; virtual bool addLemma( Node lem ) = 0; }; @@ -48,11 +48,14 @@ public: class CegInstantiator { private: + QuantifiersEngine * d_qe; + CegqiOutput * d_out; + //constants Node d_zero; Node d_one; Node d_true; - QuantifiersEngine * d_qe; - CegqiOutput * d_out; + bool d_use_vts_delta; + bool d_use_vts_inf; //program variable contains cache std::map< Node, std::map< Node, bool > > d_prog_var; std::map< Node, bool > d_inelig; @@ -61,25 +64,23 @@ private: 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, + std::vector< Node >& coeff, std::vector< Node >& has_coeff, Node theta, unsigned i, 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, unsigned effort ); + bool addInstantiationInc( Node n, Node pv, Node pv_coeff, std::vector< Node >& subs, std::vector< Node >& vars, + std::vector< Node >& coeff, std::vector< Node >& has_coeff, Node theta, unsigned i, 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, + std::vector< Node >& coeff, std::vector< Node >& has_coeff, unsigned j ); - bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::vector< int >& subs_typ ); + bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars ); Node 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 = true ); + Node getModelBasedProjectionValue( Node t, bool strict, bool isLower, Node c, Node me, Node mt, Node theta ); public: - CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out ); + CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out, bool use_vts_delta = true, bool use_vts_inf = true ); //the CE variables std::vector< Node > d_vars; //check : add instantiations based on valuation of d_vars bool check(); - // get delta lemmas : on-demand force minimality of d_n_delta - void getDeltaLemmas( std::vector< Node >& lems ); }; class InstStrategySimplex : public InstStrategy{ @@ -134,7 +135,7 @@ class CegqiOutputInstStrategy : public CegqiOutput public: CegqiOutputInstStrategy( InstStrategyCegqi * out ) : d_out( out ){} InstStrategyCegqi * d_out; - bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ); + bool addInstantiation( std::vector< Node >& subs ); bool isEligibleForInstantiation( Node n ); bool addLemma( Node lem ); }; @@ -143,10 +144,9 @@ class InstStrategyCegqi : public InstStrategy { private: CegqiOutputInstStrategy * d_out; std::map< Node, CegInstantiator * > d_cinst; - Node d_n_delta_ub; + Node d_small_const; Node d_curr_quant; - bool d_check_delta_lemma; - bool d_check_delta_lemma_lc; + bool d_check_vts_lemma_lc; /** process functions */ void processResetInstantiationRound( Theory::Effort effort ); int process( Node f, Theory::Effort effort, int e ); @@ -154,7 +154,7 @@ public: InstStrategyCegqi( QuantifiersEngine * qe ); ~InstStrategyCegqi() throw() {} - bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ); + bool addInstantiation( std::vector< Node >& subs ); bool isEligibleForInstantiation( Node n ); bool addLemma( Node lem ); /** identify */ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 7973abcc6..eefa45770 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1312,10 +1312,10 @@ Node TermDb::getVtsDelta( bool isFree, bool create ) { Node TermDb::getVtsInfinity( bool isFree, bool create ) { if( create ){ if( d_vts_inf_free.isNull() ){ - d_vts_inf_free = NodeManager::currentNM()->mkSkolem( "inf", NodeManager::currentNM()->realType(), "free infinity for virtual term substitution" ); + d_vts_inf_free = NodeManager::currentNM()->mkSkolem( "inf", NodeManager::currentNM()->integerType(), "free infinity for virtual term substitution" ); } if( d_vts_inf.isNull() ){ - d_vts_inf = NodeManager::currentNM()->mkSkolem( "inf", NodeManager::currentNM()->realType(), "infinity for virtual term substitution" ); + d_vts_inf = NodeManager::currentNM()->mkSkolem( "inf", NodeManager::currentNM()->integerType(), "infinity for virtual term substitution" ); } } return isFree ? d_vts_inf_free : d_vts_inf; @@ -1326,6 +1326,7 @@ Node TermDb::rewriteVtsSymbols( Node n ) { Trace("quant-vts-debug") << "VTS : process " << n << std::endl; bool rew_inf = false; bool rew_delta = false; + //rewriting infinity always takes precedence over rewriting delta if( !d_vts_inf.isNull() && containsTerm( n, d_vts_inf ) ){ rew_inf = true; }else if( !d_vts_delta.isNull() && containsTerm( n, d_vts_delta ) ){ @@ -1342,6 +1343,7 @@ Node TermDb::rewriteVtsSymbols( Node n ) { QuantArith::debugPrintMonomialSum( msum, "quant-vts-debug" ); } Node vts_sym = rew_inf ? d_vts_inf : d_vts_delta; + Assert( !vts_sym.isNull() ); Node iso_n; int res = QuantArith::isolate( vts_sym, msum, iso_n, n.getKind(), true ); if( res!=0 ){ @@ -1349,9 +1351,10 @@ Node TermDb::rewriteVtsSymbols( Node n ) { int index = res==1 ? 0 : 1; Node slv = iso_n[res==1 ? 1 : 0]; if( iso_n[index]!=vts_sym ){ - if( iso_n[index].getKind()==MULT && iso_n[index].getNumChildren()==2 && iso_n[index][0].isConst() && iso_n[index][1]==d_vts_delta ){ + if( iso_n[index].getKind()==MULT && iso_n[index].getNumChildren()==2 && iso_n[index][0].isConst() && iso_n[index][1]==vts_sym ){ slv = NodeManager::currentNM()->mkNode( MULT, slv, NodeManager::currentNM()->mkConst( Rational(1)/iso_n[index][0].getConst() ) ); }else{ + Trace("quant-vts-debug") << "Failed, return " << n << std::endl; return n; } } diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index f034b3212..13c408d85 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -84,8 +84,6 @@ d_lemmas_produced_c(u){ d_eq_query = new EqualityQueryQuantifiersEngine( this ); d_term_db = new quantifiers::TermDb( c, u, this ); d_tr_trie = new inst::TriggerTrie; - //d_rr_tr_trie = new rrinst::TriggerTrie; - //d_eem = new EfficientEMatcher( this ); d_hasAddedLemma = false; bool needsBuilder = false; @@ -834,18 +832,15 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bo getOutputChannel().safePoint(options::quantifierStep()); Assert( terms.size()==f[0].getNumChildren() ); - Trace("inst-add-debug") << "For quantified formula " << f << "..." << std::endl; - Trace("inst-add-debug") << "Add instantiation: "; + Trace("inst-add-debug") << "For quantified formula " << f << ", add instantiation: " << std::endl; for( unsigned i=0; i0 ) Trace("inst-add-debug") << ", "; - Trace("inst-add-debug") << f[0][i] << " -> " << terms[i]; + Trace("inst-add-debug") << " " << f[0][i] << " -> " << terms[i] << std::endl; //make it representative, this is helpful for recognizing duplication if( mkRep ){ //pick the best possible representative for instantiation, based on past use and simplicity of term terms[i] = d_eq_query->getInternalRepresentative( terms[i], f, i ); } } - Trace("inst-add-debug") << std::endl; //check based on instantiation level if( options::instMaxLevel()!=-1 || options::lteRestrictInstClosure() ){ diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index eb004c184..092c1548f 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -51,7 +51,9 @@ TESTS = \ is-even-pred.smt2 \ delta-simp.smt2 \ nested-delta.smt2 \ - nested-inf.smt2 + nested-inf.smt2 \ + RND-small.smt2 \ + clock-10.smt2 diff --git a/test/regress/regress0/quantifiers/RND-small.smt2 b/test/regress/regress0/quantifiers/RND-small.smt2 new file mode 100644 index 000000000..1401e5de8 --- /dev/null +++ b/test/regress/regress0/quantifiers/RND-small.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --cbqi-recurse +; EXPECT: sat +(set-logic LRA) +(declare-fun y1 () Real) +(declare-fun y2 () Real) +(declare-fun x1 () Real) +(assert (forall ((?y1 Real)) (exists ((?y2 Real)) (or (and (>= (+ (+ (* 69 ?y2) (* (- 80) ?y1)) (* 48 x1)) (- 77)) (and (not (= (+ (* (- 1) ?y2) (* (- 48) x1)) 0)) (not (= (+ (* 14 ?y1) (* (- 98) x1)) 83)))) (and (and (<= (+ (+ (* (- 95) ?y2) (* 34 ?y1)) (* (- 54) x1)) 51) (= (+ (+ (* 27 ?y2) (* (- 17) ?y1)) (* 75 x1)) 24)) (not (= (+ (* (- 96) ?y1) (* 90 x1)) (- 39)))))))) +(check-sat) +(exit) diff --git a/test/regress/regress0/quantifiers/clock-10.smt2 b/test/regress/regress0/quantifiers/clock-10.smt2 new file mode 100644 index 000000000..6a55b50e1 --- /dev/null +++ b/test/regress/regress0/quantifiers/clock-10.smt2 @@ -0,0 +1,5 @@ +(set-logic LIA) +(set-info :status unsat) +(declare-fun t () Int) +(assert (forall ((s Int) (m Int)) (or (not (= (+ (* 10 m) s) t)) (< s 0) (>= s 10)))) +(check-sat) \ No newline at end of file -- 2.30.2