From: ajreynol Date: Mon, 24 Aug 2015 16:34:25 +0000 (+0200) Subject: Improvements to vts in cbqi, bug fix vts for non-atomic terms containing vts symbols... X-Git-Tag: cvc5-1.0.0~6252^2~10 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d7dc7c2b3038b862af5ea55e7cf6b1fc4e1fe684;p=cvc5.git Improvements to vts in cbqi, bug fix vts for non-atomic terms containing vts symbols. Move presolve for sygus to cbqi. Enable --cbqi-recurse by default, add option --cbqi-min-bound. Enable qcf for finite model finding by default. --- diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 192485dcc..8fdec25c2 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1375,9 +1375,6 @@ void SmtEngine::setDefaults() { if( !options::eMatching.wasSetByUser() ){ options::eMatching.set( options::fmfInstEngine() ); } - if( !options::quantConflictFind.wasSetByUser() ){ - options::quantConflictFind.set( false ); - } if( ! options::instWhenMode.wasSetByUser()){ //instantiate only on last call if( options::eMatching() ){ @@ -1440,7 +1437,7 @@ void SmtEngine::setDefaults() { options::cbqi2.set( true ); } } - if( options::recurseCbqi() || options::cbqi2() ){ + if( options::cbqi2() ){ options::cbqi.set( true ); } if( options::cbqi2() ){ diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index e10ba0fef..dce9c088c 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -29,18 +29,18 @@ using namespace std; namespace CVC4 { -CegConjecture::CegConjecture( context::Context* c ) : d_active( c, false ), d_infeasible( c, false ), d_curr_lit( c, 0 ){ +CegConjecture::CegConjecture( QuantifiersEngine * qe, context::Context* c ) : d_qe( qe ), d_active( c, false ), d_infeasible( c, false ), d_curr_lit( c, 0 ){ d_refine_count = 0; - d_ceg_si = new CegConjectureSingleInv( this ); + d_ceg_si = new CegConjectureSingleInv( qe, this ); } -void CegConjecture::assign( QuantifiersEngine * qe, Node q ) { +void CegConjecture::assign( Node q ) { Assert( d_quant.isNull() ); Assert( q.getKind()==FORALL ); d_assert_quant = q; //register with single invocation if applicable - if( qe->getTermDatabase()->isQAttrSygus( d_assert_quant ) && options::cegqiSingleInv() ){ - d_ceg_si->initialize( qe, q ); + if( d_qe->getTermDatabase()->isQAttrSygus( d_assert_quant ) && options::cegqiSingleInv() ){ + d_ceg_si->initialize( q ); if( q!=d_ceg_si->d_quant ){ //Node red_lem = NodeManager::currentNM()->mkNode( OR, q.negate(), d_cegqi_si->d_quant ); //may have rewritten quantified formula (for invariant synthesis) @@ -53,9 +53,9 @@ void CegConjecture::assign( QuantifiersEngine * qe, Node q ) { } Trace("cegqi") << "Base quantified fm is : " << q << std::endl; //construct base instantiation - d_base_inst = Rewriter::rewrite( qe->getInstantiation( q, d_candidates ) ); + d_base_inst = Rewriter::rewrite( d_qe->getInstantiation( q, d_candidates ) ); Trace("cegqi") << "Base instantiation is : " << d_base_inst << std::endl; - if( qe->getTermDatabase()->isQAttrSygus( d_assert_quant ) ){ + if( d_qe->getTermDatabase()->isQAttrSygus( d_assert_quant ) ){ CegInstantiation::collectDisjuncts( d_base_inst, d_base_disj ); Trace("cegqi") << "Conjecture has " << d_base_disj.size() << " disjuncts." << std::endl; //store the inner variables for each disjunct @@ -70,7 +70,7 @@ void CegConjecture::assign( QuantifiersEngine * qe, Node q ) { } } d_syntax_guided = true; - }else if( qe->getTermDatabase()->isQAttrSynthesis( d_assert_quant ) ){ + }else if( d_qe->getTermDatabase()->isQAttrSynthesis( d_assert_quant ) ){ d_syntax_guided = false; }else{ Assert( false ); @@ -150,7 +150,7 @@ bool CegConjecture::needsCheck() { } CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ){ - d_conj = new CegConjecture( qe->getSatContext() ); + d_conj = new CegConjecture( qe, qe->getSatContext() ); d_last_inst_si = false; } @@ -178,7 +178,7 @@ void CegInstantiation::registerQuantifier( Node q ) { if( d_quantEngine->getOwner( q )==this ){ if( !d_conj->isAssigned() ){ Trace("cegqi") << "Register conjecture : " << q << std::endl; - d_conj->assign( d_quantEngine, q ); + d_conj->assign( q ); //fairness if( d_conj->getCegqiFairMode()!=CEGQI_FAIR_NONE ){ diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h index af3a19d62..9228f11b6 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/ce_guided_instantiation.h @@ -29,8 +29,10 @@ namespace quantifiers { /** a synthesis conjecture */ class CegConjecture { +private: + QuantifiersEngine * d_qe; public: - CegConjecture( context::Context* c ); + CegConjecture( QuantifiersEngine * qe, context::Context* c ); /** is conjecture active */ context::CDO< bool > d_active; /** is conjecture infeasible */ @@ -65,7 +67,7 @@ public: /** refine count */ unsigned d_refine_count; /** assign */ - void assign( QuantifiersEngine * qe, Node q ); + void assign( Node q ); /** is assigned */ bool isAssigned() { return !d_quant.isNull(); } /** current extential quantifeirs whose couterexamples we must refine */ diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index a1aa9dad8..398415ca8 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -45,11 +45,18 @@ bool CegqiOutputSingleInv::addLemma( Node n ) { } -CegConjectureSingleInv::CegConjectureSingleInv( CegConjecture * p ) : d_parent( p ){ - d_sol = NULL; - d_c_inst_match_trie = NULL; - d_cinst = NULL; +CegConjectureSingleInv::CegConjectureSingleInv( QuantifiersEngine * qe, CegConjecture * p ) : d_qe( qe ), d_parent( p ){ d_has_ites = true; + if( options::incrementalSolving() ){ + d_c_inst_match_trie = new inst::CDInstMatchTrie( qe->getUserContext() ); + }else{ + d_c_inst_match_trie = NULL; + } + CegqiOutputSingleInv * cosi = new CegqiOutputSingleInv( this ); + // third and fourth arguments set to (false,false) until we have solution reconstruction for delta and infinity + d_cinst = new CegInstantiator( qe, cosi, false, false ); + + d_sol = new CegConjectureSingleInvSol( qe ); } Node CegConjectureSingleInv::getSingleInvLemma( Node guard ) { @@ -73,15 +80,9 @@ Node CegConjectureSingleInv::getSingleInvLemma( Node guard ) { inst = TermDb::simpleNegate( inst ); Trace("cegqi-si") << "Single invocation initial lemma : " << inst << std::endl; - //initialize the instantiator for this - if( !d_single_inv_sk.empty() ){ - CegqiOutputSingleInv * cosi = new CegqiOutputSingleInv( this ); - // 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; - } + //copy variables to instantiator + d_cinst->d_vars.clear(); + d_cinst->d_vars.insert( d_cinst->d_vars.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() ); return NodeManager::currentNM()->mkNode( OR, guard.negate(), inst ); }else{ @@ -89,14 +90,9 @@ Node CegConjectureSingleInv::getSingleInvLemma( Node guard ) { } } -void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) { +void CegConjectureSingleInv::initialize( Node q ) { //initialize data - d_sol = new CegConjectureSingleInvSol( qe ); - d_qe = qe; d_quant = q; - if( options::incrementalSolving() ){ - d_c_inst_match_trie = new inst::CDInstMatchTrie( qe->getUserContext() ); - } //process Trace("cegqi-si") << "Initialize cegqi-si for " << q << std::endl; // conj -> conj* @@ -457,63 +453,8 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) { exit( 0 ); } }else{ - if( options::cegqiSingleInvPreRegInst() && d_single_inv.getKind()==FORALL ){ - Trace("cegqi-si-presolve") << "Check " << d_single_inv << std::endl; - //at preregister time, add proxy of obvious instantiations up front, which helps learning during preprocessing - std::vector< Node > vars; - std::map< Node, std::vector< Node > > teq; - for( unsigned i=0; i terms; - std::vector< Node > conj; - getPresolveEqConjuncts( vars, terms, teq, d_single_inv, conj ); - - if( !conj.empty() ){ - Node lem = conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj ); - Node g = NodeManager::currentNM()->mkSkolem( "g", NodeManager::currentNM()->booleanType() ); - lem = NodeManager::currentNM()->mkNode( OR, g, lem ); - d_qe->getOutputChannel().lemma( lem, false, true ); - } - } - } -} - -void CegConjectureSingleInv::collectPresolveEqTerms( Node n, std::map< Node, std::vector< Node > >& teq ) { - if( n.getKind()==EQUAL ){ - for( unsigned i=0; i<2; i++ ){ - std::map< Node, std::vector< Node > >::iterator it = teq.find( n[i] ); - if( it!=teq.end() ){ - Node nn = n[ i==0 ? 1 : 0 ]; - if( std::find( it->second.begin(), it->second.end(), nn )==it->second.end() ){ - it->second.push_back( nn ); - Trace("cegqi-si-presolve") << " - " << n[i] << " = " << nn << std::endl; - } - } - } - } - for( unsigned i=0; i& vars, std::vector< Node >& terms, - std::map< Node, std::vector< Node > >& teq, Node f, std::vector< Node >& conj ) { - if( conj.size()<1000 ){ - if( terms.size()==f[0].getNumChildren() ){ - Node c = f[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); - conj.push_back( c ); - }else{ - unsigned i = terms.size(); - Node v = f[0][i]; - terms.push_back( Node::null() ); - for( unsigned j=0; jpresolve( d_single_inv ); } } } @@ -746,7 +687,7 @@ bool CegConjectureSingleInv::addLemma( Node n ) { } void CegConjectureSingleInv::check( std::vector< Node >& lems ) { - if( !d_single_inv.isNull() && d_cinst!=NULL ) { + if( !d_single_inv.isNull() ) { d_curr_lemmas.clear(); //call check for instantiator d_cinst->check(); diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h index 2c955db5d..7df859337 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h @@ -103,7 +103,7 @@ private: // add lemma bool addLemma( Node lem ); public: - CegConjectureSingleInv( CegConjecture * p ); + CegConjectureSingleInv( QuantifiersEngine * qe, CegConjecture * p ); // original conjecture Node d_quant; // single invocation version of quant @@ -116,7 +116,7 @@ public: //get the single invocation lemma Node getSingleInvLemma( Node guard ); //initialize - void initialize( QuantifiersEngine * qe, Node q ); + void initialize( Node q ); //check void check( std::vector< Node >& lems ); //get solution diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index bf0168c64..3d33f01ca 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -195,12 +195,6 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< } } 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 ) ){ @@ -222,9 +216,12 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< //[3] directly look at assertions Trace("cbqi-inst-debug") << "[3] try based on assertions." << std::endl; + Node vts_sym[2]; + vts_sym[0] = d_qe->getTermDatabase()->getVtsInfinity( pvtn, false, false ); + vts_sym[1] = d_qe->getTermDatabase()->getVtsDelta( false, false ); std::vector< Node > mbp_bounds[2]; std::vector< Node > mbp_coeff[2]; - std::vector< bool > mbp_strict[2]; + std::vector< Node > mbp_vts_coeff[2][2]; std::vector< Node > mbp_lit[2]; unsigned rmax = Theory::theoryOf( pv )==Theory::theoryOf( pv.getType() ) ? 1 : 2; for( unsigned r=0; r& subs, std::vector< 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; } + //get the coefficient of infinity and remove it from msum + Node vts_coeff[2]; + for( unsigned t=0; t<2; t++ ){ + if( !vts_sym[t].isNull() ){ + std::map< Node, Node >::iterator itminf = msum.find( vts_sym[t] ); + if( itminf!=msum.end() ){ + vts_coeff[t] = itminf->second; + if( vts_coeff[t].isNull() ){ + vts_coeff[t] = NodeManager::currentNM()->mkConst( Rational( 1 ) ); + } + //negate if coefficient on variable is positive + std::map< Node, Node >::iterator itv = msum.find( pv ); + if( itv!=msum.end() ){ + if( itv->second.isNull() || itv->second.getConst().sgn()==1 ){ + vts_coeff[t] = QuantArith::negate(vts_coeff[t]); + Trace("cbqi-inst-debug") << "negate vts[" << t<< "] coefficient." << std::endl; + } + } + Trace("cbqi-inst-debug") << "vts[" << t << "] coefficient is " << vts_coeff[t] << std::endl; + msum.erase( vts_sym[t] ); + } + } + } + + Trace("cbqi-inst-debug") << "isolate for " << pv << "..." << std::endl; Node vatom; //isolate pv in the inequality int ires = QuantArith::isolate( pv, msum, vatom, atom.getKind(), true ); @@ -294,12 +315,6 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< Assert( veq_v==pv ); } } - //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(); - } //disequalities are either strict upper or lower bounds unsigned rmax = ( atom.getKind()==GEQ && options::cbqiModel() ) ? 1 : 2; @@ -320,29 +335,38 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< } } }else{ - unsigned use_r = r; + bool is_upper = ( r==0 ); if( options::cbqiModel() ){ // disequality is a disjunction : only consider the bound in the direction of the model - Node rhs_value = d_qe->getModel()->getValue( val ); - Node lhs_value = pv_value; - if( !veq_c.isNull() ){ - lhs_value = NodeManager::currentNM()->mkNode( MULT, lhs_value, veq_c ); - lhs_value = Rewriter::rewrite( lhs_value ); + //first check if there is an infinity... + if( !vts_coeff[0].isNull() ){ + //coefficient or val won't make a difference, just compare with zero + Trace("cbqi-inst-debug") << "Disequality : check infinity polarity " << vts_coeff[0] << std::endl; + Assert( vts_coeff[0].isConst() ); + is_upper = ( vts_coeff[0].getConst().sgn()==1 ); + }else{ + Node rhs_value = d_qe->getModel()->getValue( val ); + Node lhs_value = pv_value; + if( !veq_c.isNull() ){ + lhs_value = NodeManager::currentNM()->mkNode( MULT, lhs_value, veq_c ); + lhs_value = Rewriter::rewrite( lhs_value ); + } + Trace("cbqi-inst-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 ); + Assert( cmp.isConst() ); + is_upper = ( cmp!=d_true ); } - Assert( lhs_value!=rhs_value ); - Node cmp = NodeManager::currentNM()->mkNode( GEQ, lhs_value, rhs_value ); - cmp = Rewriter::rewrite( cmp ); - Assert( cmp.isConst() ); - use_r = cmp==d_true ? 1 : 0; } Assert( atom.getKind()==EQUAL && !pol ); if( pvtn.isInteger() ){ - uires = use_r==0 ? -1 : 1; + uires = is_upper ? -1 : 1; uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) ); uval = Rewriter::rewrite( uval ); }else{ Assert( pvtn.isReal() ); - uires = use_r==0 ? -2 : 2; + uires = is_upper ? -2 : 2; } } Trace("cbqi-bound-inf") << "From " << lit << ", got : "; @@ -350,29 +374,38 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< Trace("cbqi-bound-inf") << veq_c << " * "; } Trace("cbqi-bound-inf") << pv << " -> " << uval << ", styp = " << uires << std::endl; + //take into account delta + if( d_use_vts_delta && ( uires==2 || uires==-2 ) ){ + if( options::cbqiModel() ){ + Node delta_coeff = NodeManager::currentNM()->mkConst( Rational( uires > 0 ? 1 : -1 ) ); + if( vts_coeff[1].isNull() ){ + vts_coeff[1] = delta_coeff; + }else{ + vts_coeff[1] = NodeManager::currentNM()->mkNode( PLUS, vts_coeff[1], delta_coeff ); + vts_coeff[1] = Rewriter::rewrite( vts_coeff[1] ); + } + }else{ + Node delta = d_qe->getTermDatabase()->getVtsDelta(); + uval = NodeManager::currentNM()->mkNode( uires==2 ? PLUS : MINUS, uval, delta ); + uval = Rewriter::rewrite( uval ); + } + } 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 ); + for( unsigned t=0; t<2; t++ ){ + mbp_vts_coeff[index][t].push_back( vts_coeff[t] ); + } 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 ); - } - } + //try this bound 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; } } } @@ -387,8 +420,11 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< if( options::cbqiModel() ){ if( pvtn.isInteger() || pvtn.isReal() ){ bool upper_first = false; + if( options::cbqiMinBounds() ){ + upper_first = mbp_bounds[1].size() t_values[2]; + std::vector< Node > t_values[3]; //try optimal bounds for( unsigned r=0; r<2; r++ ){ int rr = upper_first ? (1-r) : r; @@ -397,6 +433,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< Trace("cbqi-bound") << "No " << ( rr==0 ? "lower" : "upper" ) << " bounds for " << pv << " (type=" << pvtn << ")" << std::endl; //no bounds, we do +- infinity Node val = d_qe->getTermDatabase()->getVtsInfinity( pvtn ); + //TODO : rho value for infinity? if( rr==0 ){ val = NodeManager::currentNM()->mkNode( UMINUS, val ); val = Rewriter::rewrite( val ); @@ -408,57 +445,116 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< }else{ Trace("cbqi-bound") << ( rr==0 ? "Lower" : "Upper" ) << " bounds for " << pv << " (type=" << pvtn << ") : " << std::endl; int best = -1; - Node best_bound_value; + Node best_bound_value[3]; 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)"; + Node value[3]; + if( Trace.isOn("cbqi-bound") ){ + Assert( !mbp_bounds[rr][j].isNull() ); + Trace("cbqi-bound") << " " << j << ": " << mbp_bounds[rr][j]; + if( !mbp_vts_coeff[rr][0][j].isNull() ){ + Trace("cbqi-bound") << " (+ " << mbp_vts_coeff[rr][0][j] << " * INF)"; + } + if( !mbp_vts_coeff[rr][1][j].isNull() ){ + Trace("cbqi-bound") << " (+ " << mbp_vts_coeff[rr][1][j] << " * DELTA)"; + } + if( !mbp_coeff[rr][j].isNull() ){ + Trace("cbqi-bound") << " (div " << mbp_coeff[rr][j] << ")"; + } + Trace("cbqi-bound") << ", value = "; } - 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; + t_values[rr].push_back( Node::null() ); + //check if it is better than the current best bound : lexicographic order infinite/finite/infinitesimal parts + bool new_best = true; + for( unsigned t=0; t<3; t++ ){ + //get the value + if( t==0 ){ + value[0] = mbp_vts_coeff[rr][0][j]; + if( !value[0].isNull() ){ + Trace("cbqi-bound") << "( " << value[0] << " * INF ) + "; + }else{ + value[0] = d_zero; + } + }else if( t==1 ){ + Node t_value = d_qe->getModel()->getValue( mbp_bounds[rr][j] ); + t_values[rr][j] = t_value; + value[1] = t_value; + Trace("cbqi-bound") << value[1]; + }else{ + value[2] = mbp_vts_coeff[rr][1][j]; + if( !value[2].isNull() ){ + Trace("cbqi-bound") << " + ( " << value[2] << " * DELTA )"; + }else{ + value[2] = d_zero; + } + } + //multiply by coefficient + if( value[t]!=d_zero && !mbp_coeff[rr][j].isNull() ){ + Assert( mbp_coeff[rr][j].isConst() ); + value[t] = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(1) / mbp_coeff[rr][j].getConst() ), value[t] ); + value[t] = Rewriter::rewrite( value[t] ); + } + //check if new best + if( best!=-1 ){ + Assert( !value[t].isNull() && !best_bound_value[t].isNull() ); + if( value[t]!=best_bound_value[t] ){ + Kind k = rr==0 ? GEQ : LEQ; + Node cmp_bound = NodeManager::currentNM()->mkNode( k, value[t], best_bound_value[t] ); + cmp_bound = Rewriter::rewrite( cmp_bound ); + if( cmp_bound!=d_true ){ + new_best = false; + break; + } + } } } + Trace("cbqi-bound") << std::endl; if( new_best ){ - best_bound_value = value; + for( unsigned t=0; t<3; t++ ){ + best_bound_value[t] = value[t]; + } best = j; } } if( best!=-1 ){ - Trace("cbqi-bound") << "...best bound is " << best << " : " << best_bound_value << std::endl; + Trace("cbqi-bound") << "...best bound is " << best << " : "; + if( best_bound_value[0]!=d_zero ){ + Trace("cbqi-bound") << "( " << best_bound_value[0] << " * INF ) + "; + } + Trace("cbqi-bound") << best_bound_value[1]; + if( best_bound_value[2]!=d_zero ){ + Trace("cbqi-bound") << " + ( " << best_bound_value[2] << " * DELTA )"; + } + Trace("cbqi-bound") << 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; + Node val = mbp_bounds[rr][best]; + val = getModelBasedProjectionValue( val, rr==0, mbp_coeff[rr][best], pv_value, t_values[rr][best], theta, + mbp_vts_coeff[rr][0][best], vts_sym[0], mbp_vts_coeff[rr][1][best], vts_sym[1] ); + if( !val.isNull() ){ + if( subs_proc[val].find( mbp_coeff[rr][best] )==subs_proc[val].end() ){ + subs_proc[val][mbp_coeff[rr][best]] = true; + if( addInstantiationInc( val, pv, mbp_coeff[rr][best], subs, vars, coeff, has_coeff, theta, i, effort ) ){ + return true; + } + } } } } } - //try non-optimal bounds (heuristic) + //try non-optimal bounds (heuristic, may help when nested quantification) ? + Trace("cbqi-bound") << "Try non-optimal bounds..." << std::endl; for( unsigned r=0; r<2; r++ ){ int rr = upper_first ? (1-r) : r; for( unsigned j=0; j& subs, std::vector< } //[4] resort to using value in model - if( effort>0 || ( pvtn.isBoolean() && ( (i+1)0 || pvtn.isBoolean() ){ Node mv = d_qe->getModel()->getValue( pv ); Node pv_coeff_m; 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( !options::cbqiUseInfInt() || !options::cbqiUseInfReal() || pvtn.isBoolean() ); + Assert( ( pvtn.isInteger() ? !options::cbqiUseInfInt() : !options::cbqiUseInfReal() ) || pvtn.isBoolean() ); #endif if( addInstantiationInc( mv, pv, pv_coeff_m, subs, vars, coeff, has_coeff, theta, i, new_effort ) ){ return true; @@ -739,21 +835,10 @@ Node CegInstantiator::applySubstitution( Node n, std::vector< Node >& subs, std: } } -Node CegInstantiator::getModelBasedProjectionValue( Node t, bool strict, bool isLower, Node c, Node me, Node mt, Node theta ) { +Node CegInstantiator::getModelBasedProjectionValue( Node t, bool isLower, Node c, Node me, Node mt, Node theta, + Node inf_coeff, Node vts_inf, Node delta_coeff, Node vts_delta ) { 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; @@ -788,6 +873,19 @@ Node CegInstantiator::getModelBasedProjectionValue( Node t, bool strict, bool is val = Rewriter::rewrite( val ); Trace("cbqi-bound2") << "(after rho) : " << val << std::endl; } + if( !inf_coeff.isNull() ){ + Assert( !vts_inf.isNull() ); + val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, inf_coeff, vts_inf ) ); + val = Rewriter::rewrite( val ); + } + if( !delta_coeff.isNull() ){ + //create delta here if necessary + if( vts_delta.isNull() ){ + vts_delta = d_qe->getTermDatabase()->getVtsDelta(); + } + val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, delta_coeff, vts_delta ) ); + val = Rewriter::rewrite( val ); + } return val; } @@ -812,25 +910,67 @@ bool CegInstantiator::check() { return false; } -void setAuxRep( std::map< Node, Node >& aux_uf, std::map< Node, Node >& aux_subs, Node n1, Node n2 ){ - Assert( aux_uf.find( n1 )==aux_uf.end() ); - Assert( aux_uf.find( n2 )==aux_uf.end() ); - //only merge if not in substitution - if( aux_subs.find( n1 )==aux_subs.end() ){ - aux_uf[n1] = n2; - }else if( aux_subs.find( n2 )==aux_subs.end() ){ - aux_uf[n2] = n1; +void collectPresolveEqTerms( Node n, std::map< Node, std::vector< Node > >& teq ) { + if( n.getKind()==FORALL || n.getKind()==EXISTS ){ + //do nothing + }else{ + if( n.getKind()==EQUAL ){ + for( unsigned i=0; i<2; i++ ){ + std::map< Node, std::vector< Node > >::iterator it = teq.find( n[i] ); + if( it!=teq.end() ){ + Node nn = n[ i==0 ? 1 : 0 ]; + if( std::find( it->second.begin(), it->second.end(), nn )==it->second.end() ){ + it->second.push_back( nn ); + Trace("cbqi-presolve") << " - " << n[i] << " = " << nn << std::endl; + } + } + } + } + for( unsigned i=0; i& aux_uf, Node n ){ - std::map< Node, Node >::iterator it = aux_uf.find( n ); - if( it!=aux_uf.end() ){ - Node r = getAuxRep( aux_uf, it->second ); - aux_uf[n] = r; - return r; - }else{ - return n; +void getPresolveEqConjuncts( std::vector< Node >& vars, std::vector< Node >& terms, + std::map< Node, std::vector< Node > >& teq, Node f, std::vector< Node >& conj ) { + if( conj.size()<1000 ){ + if( terms.size()==f[0].getNumChildren() ){ + Node c = f[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); + conj.push_back( c ); + }else{ + unsigned i = terms.size(); + Node v = f[0][i]; + terms.push_back( Node::null() ); + for( unsigned j=0; j vars; + std::map< Node, std::vector< Node > > teq; + for( unsigned i=0; i terms; + std::vector< Node > conj; + getPresolveEqConjuncts( vars, terms, teq, q, conj ); + + if( !conj.empty() ){ + Node lem = conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj ); + Node g = NodeManager::currentNM()->mkSkolem( "g", NodeManager::currentNM()->booleanType() ); + lem = NodeManager::currentNM()->mkNode( OR, g, lem ); + Trace("cbqi-presolve-debug") << "Presolve lemma : " << lem << std::endl; + d_qe->getOutputChannel().lemma( lem, false, true ); } } @@ -843,9 +983,7 @@ void CegInstantiator::processAssertions() { eq::EqualityEngine* ee = d_qe->getMasterEqualityEngine(); //to eliminate identified illegal terms - std::map< Node, Node > aux_uf; std::map< Node, Node > aux_subs; - std::map< Node, bool > aux_subs_inelig; //for each variable bool has_arith_var = false; @@ -875,34 +1013,7 @@ void CegInstantiator::processAssertions() { Trace("cbqi-proc") << "......add substitution : " << itae2->first << " -> " << itae2->second << std::endl; } } - } - /* - if( lit.getKind()==EQUAL ){ - //check if it is an auxiliary variable (for instance, from ITE removal). If so, solve for it. - for( unsigned k=0; k<2; k++ ){ - Node s = lit[k]; - if( std::find( d_aux_vars.begin(), d_aux_vars.end(), s )!=d_aux_vars.end() ){ - Node sr = getAuxRep( aux_uf, s ); - if( std::find( d_aux_vars.begin(), d_aux_vars.end(), lit[1-k] )!=d_aux_vars.end() ){ - Node ssr = getAuxRep( aux_uf, lit[1-k] ); - //merge in the union find - if( sr!=ssr ){ - Trace("cbqi-proc") << "...merge : " << sr << " = " << ssr << std::endl; - setAuxRep( aux_uf, aux_subs, sr, ssr ); - } - //if we don't have yet a substitution yet or the substitution is ineligible - }else if( aux_subs.find( sr )==aux_subs.end() || aux_subs_inelig[sr] ){ - computeProgVars( lit[1-k] ); - bool isInelig = d_inelig.find( lit[1-k] )!=d_inelig.end(); - //equality for auxiliary variable : will add to substitution - Trace("cbqi-proc") << "...add to substitution : " << sr << " -> " << lit[1-k] << std::endl; - aux_subs[sr] = lit[1-k]; - aux_subs_inelig[sr] = isInelig; - } - } - } } - */ } } } @@ -951,20 +1062,18 @@ void CegInstantiator::processAssertions() { std::vector< Node > subs_lhs; std::vector< Node > subs_rhs; for( unsigned i=0; i::iterator it = aux_subs.find( r ); if( it!=aux_subs.end() ){ - addToAuxVarSubstitution( subs_lhs, subs_rhs, l, it->second ); + addToAuxVarSubstitution( subs_lhs, subs_rhs, r, it->second ); }else{ - Trace("cbqi-proc") << "....no substitution found for auxiliary variable " << l << "!!!" << std::endl; + Trace("cbqi-proc") << "....no substitution found for auxiliary variable " << r << "!!!" << std::endl; #ifdef MBP_STRICT_ASSERTIONS Assert( false ); #endif } } - //apply substitutions to everything, if necessary if( !subs_lhs.empty() ){ Trace("cbqi-proc") << "Applying substitution : " << std::endl; @@ -1407,14 +1516,14 @@ int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) { //heuristic for now, until we know how to do nested quantification Node delta = d_quantEngine->getTermDatabase()->getVtsDelta( true, false ); if( !delta.isNull() ){ - Trace("cegqi") << "Delta lemma for " << d_small_const << std::endl; + Trace("quant-vts-debug") << "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 ); } std::vector< Node > inf; d_quantEngine->getTermDatabase()->getVtsTerms( inf, true, false, false ); for( unsigned i=0; imkNode( GT, inf[i], NodeManager::currentNM()->mkConst( Rational(1)/d_small_const.getConst() ) ); d_quantEngine->getOutputChannel().lemma( inf_lem_lb ); } @@ -1457,11 +1566,10 @@ CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) { } } - - - - - - - +void InstStrategyCegqi::registerQuantifier( Node q ) { + if( options::cbqiSingleInvPreRegInst() ){ + CegInstantiator * cinst = getInstantiator( q ); + cinst->presolve( q ); + } +} diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index f7cb290b2..c7c046e51 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -79,7 +79,8 @@ private: 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 ); + Node getModelBasedProjectionValue( Node t, bool isLower, Node c, Node me, Node mt, Node theta, + Node inf_coeff, Node vts_inf, Node delta_coeff, Node vts_delta ); void processAssertions(); void addToAuxVarSubstitution( std::vector< Node >& subs_lhs, std::vector< Node >& subs_rhs, Node l, Node r ); public: @@ -92,6 +93,8 @@ public: std::map< Node, std::map< Node, Node > > d_aux_eq; //check : add instantiations based on valuation of d_vars bool check(); + //presolve for quantified formula + void presolve( Node q ); }; class InstStrategySimplex : public InstStrategy{ @@ -170,9 +173,11 @@ public: bool addLemma( Node lem ); /** identify */ std::string identify() const { return std::string("Cegqi"); } - + //get instantiator for quantifier CegInstantiator * getInstantiator( Node q ); + //register quantifier + void registerQuantifier( Node q ); }; } diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 3dad74044..6cf64407f 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -102,7 +102,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ //add counterexample lemma lem = Rewriter::rewrite( lem ); Trace("cbqi") << "Counterexample lemma : " << lem << std::endl; - + //must explicitly remove ITEs so that we record dependencies IteSkolemMap iteSkolemMap; std::vector< Node > lems; @@ -140,7 +140,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ } } } - + addedLemma = true; } } @@ -289,6 +289,9 @@ bool InstantiationEngine::checkComplete() { void InstantiationEngine::registerQuantifier( Node f ){ if( d_quantEngine->hasOwnership( f, this ) ){ + for( unsigned i=0; iregisterQuantifier( f ); + } //Notice() << "do cbqi " << f << " ? " << std::endl; if( options::cbqi() ){ Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( f ); diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h index 44612a85c..d6cde9e7f 100644 --- a/src/theory/quantifiers/instantiation_engine.h +++ b/src/theory/quantifiers/instantiation_engine.h @@ -49,6 +49,8 @@ public: virtual int process( Node f, Theory::Effort effort, int e ) = 0; /** identify */ virtual std::string identify() const { return std::string("Unknown"); } + /** register quantifier */ + virtual void registerQuantifier( Node q ) {} };/* class InstStrategy */ class InstantiationEngine : public QuantifiersModule diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 66de51f39..c693adef5 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -208,8 +208,6 @@ option cegqiSingleInvReconstruct --cegqi-si-reconstruct bool :default true reconstruct solutions for single invocation conjectures in original grammar option cegqiSingleInvReconstructConst --cegqi-si-reconstruct-const bool :default true include constants when reconstruct solutions for single invocation conjectures in original grammar -option cegqiSingleInvPreRegInst --cegqi-si-prereg-inst bool :default true - preregister ground instantiations when single invocation option cegqiSingleInvAbort --cegqi-si-abort bool :default false abort if synthesis conjecture is not single invocation option cegqiSingleInvMultiInstAbort --cegqi-si-multi-inst-abort bool :default false @@ -236,7 +234,7 @@ option cbqi --cbqi bool :read-write :default false turns on counterexample-based quantifier instantiation option cbqi2 --cbqi2 bool :read-write :default false turns on new implementation of counterexample-based quantifier instantiation -option recurseCbqi --cbqi-recurse bool :default false +option recurseCbqi --cbqi-recurse bool :default true turns on recursive counterexample-based quantifier instantiation option cbqiSat --cbqi-sat bool :read-write :default true answer sat when quantifiers are asserted with counterexample-based quantifier instantiation @@ -246,7 +244,10 @@ option cbqiUseInfInt --cbqi-use-inf-int bool :read-write :default false use integer infinity for vts in counterexample-based quantifier instantiation option cbqiUseInfReal --cbqi-use-inf-real bool :read-write :default false use real infinity for vts in counterexample-based quantifier instantiation - +option cbqiSingleInvPreRegInst --cbqi-prereg-inst bool :default false + preregister ground instantiations in counterexample-based quantifier instantiation +option cbqiMinBounds --cbqi-min-bounds bool :default false + use minimally constrained lower/upper bound for counterexample-based quantifier instantiation ### local theory extensions options diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index 938245871..ebeb4b871 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -115,10 +115,14 @@ int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind (children.size()==1 ? children[0] : NodeManager::currentNM()->mkConst( Rational(0) )); Node vc = v; if( !r.isOne() && !r.isNegativeOne() ){ - if( doCoeff ){ - vc = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( r.abs() ), vc ); + if( vc.getType().isInteger() ){ + if( doCoeff ){ + vc = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( r.abs() ), vc ); + }else{ + return 0; + } }else{ - return 0; + veq = NodeManager::currentNM()->mkNode( MULT, veq, NodeManager::currentNM()->mkConst( Rational(1) / r.abs() ) ); } } if( r.sgn()==1 ){ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 58f0a265e..52aee392b 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1312,7 +1312,7 @@ void TermDb::getVtsTerms( std::vector< Node >& t, bool isFree, bool create, bool Node TermDb::getVtsDelta( bool isFree, bool create ) { if( create ){ if( d_vts_delta_free.isNull() ){ - d_vts_delta_free = NodeManager::currentNM()->mkSkolem( "delta", NodeManager::currentNM()->realType(), "free delta for virtual term substitution" ); + d_vts_delta_free = NodeManager::currentNM()->mkSkolem( "delta_free", NodeManager::currentNM()->realType(), "free delta for virtual term substitution" ); Node delta_lem = NodeManager::currentNM()->mkNode( GT, d_vts_delta_free, NodeManager::currentNM()->mkConst( Rational( 0 ) ) ); d_quantEngine->getOutputChannel().lemma( delta_lem ); } @@ -1326,7 +1326,7 @@ Node TermDb::getVtsDelta( bool isFree, bool create ) { Node TermDb::getVtsInfinity( TypeNode tn, bool isFree, bool create ) { if( create ){ if( d_vts_inf_free[tn].isNull() ){ - d_vts_inf_free[tn] = NodeManager::currentNM()->mkSkolem( "inf", tn, "free infinity for virtual term substitution" ); + d_vts_inf_free[tn] = NodeManager::currentNM()->mkSkolem( "inf_free", tn, "free infinity for virtual term substitution" ); } if( d_vts_inf[tn].isNull() ){ d_vts_inf[tn] = NodeManager::currentNM()->mkSkolem( "inf", tn, "infinity for virtual term substitution" ); @@ -1346,6 +1346,19 @@ Node TermDb::getVtsInfinityIndex( int i, bool isFree, bool create ) { } } +Node TermDb::substituteVtsFreeTerms( Node n ) { + std::vector< Node > vars; + getVtsTerms( vars, false, false ); + std::vector< Node > vars_free; + getVtsTerms( vars_free, true, false ); + Assert( vars.size()==vars_free.size() ); + if( !vars.empty() ){ + return n.substitute( vars.begin(), vars.end(), vars_free.begin(), vars_free.end() ); + }else{ + return n; + } +} + Node TermDb::rewriteVtsSymbols( Node n ) { if( ( n.getKind()==EQUAL || n.getKind()==GEQ ) ){ Trace("quant-vts-debug") << "VTS : process " << n << std::endl; @@ -1379,63 +1392,58 @@ Node TermDb::rewriteVtsSymbols( Node n ) { } } if( !rew_vts_inf.isNull() || rew_delta ){ - if( n.getKind()==EQUAL ){ - return d_false; - }else{ - std::map< Node, Node > msum; - if( QuantArith::getMonomialSumLit( n, msum ) ){ - if( Trace.isOn("quant-vts-debug") ){ - Trace("quant-vts-debug") << "VTS got monomial sum : " << std::endl; - QuantArith::debugPrintMonomialSum( msum, "quant-vts-debug" ); - } - Node vts_sym = !rew_vts_inf.isNull() ? rew_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 ){ - Trace("quant-vts-debug") << "VTS isolated : -> " << iso_n << ", res = " << res << std::endl; - 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]==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; - } - } - Node nlit; - if( res==1 ){ - if( !rew_vts_inf.isNull() ){ - nlit = d_true; - }else{ - nlit = NodeManager::currentNM()->mkNode( GEQ, d_zero, slv ); - } + std::map< Node, Node > msum; + if( QuantArith::getMonomialSumLit( n, msum ) ){ + if( Trace.isOn("quant-vts-debug") ){ + Trace("quant-vts-debug") << "VTS got monomial sum : " << std::endl; + QuantArith::debugPrintMonomialSum( msum, "quant-vts-debug" ); + } + Node vts_sym = !rew_vts_inf.isNull() ? rew_vts_inf : d_vts_delta; + Assert( !vts_sym.isNull() ); + Node iso_n; + Node nlit; + int res = QuantArith::isolate( vts_sym, msum, iso_n, n.getKind(), true ); + if( res!=0 ){ + Trace("quant-vts-debug") << "VTS isolated : -> " << iso_n << ", res = " << res << std::endl; + Node slv = iso_n[res==1 ? 1 : 0]; + //ensure the vts terms have been eliminated + if( containsVtsTerm( slv ) ){ + Trace("quant-vts-warn") << "Bad vts literal : " << n << ", contains " << vts_sym << " but bad solved form " << slv << "." << std::endl; + nlit = substituteVtsFreeTerms( n ); + Trace("quant-vts-debug") << "...return " << nlit << std::endl; + //Assert( false ); + //safe case: just convert to free symbols + return nlit; + }else{ + if( !rew_vts_inf.isNull() ){ + nlit = ( n.getKind()==GEQ && res==1 ) ? d_true : d_false; }else{ - if( !rew_vts_inf.isNull() ){ + Assert( iso_n[res==1 ? 0 : 1]==d_vts_delta ); + if( n.getKind()==EQUAL ){ nlit = d_false; + }else if( res==1 ){ + nlit = NodeManager::currentNM()->mkNode( GEQ, d_zero, slv ); }else{ nlit = NodeManager::currentNM()->mkNode( GT, slv, d_zero ); } } - Trace("quant-vts-debug") << "Return " << nlit << std::endl; - return nlit; } + Trace("quant-vts-debug") << "Return " << nlit << std::endl; + return nlit; + }else{ + Trace("quant-vts-warn") << "Bad vts literal : " << n << ", contains " << vts_sym << " but could not isolate." << std::endl; + //safe case: just convert to free symbols + nlit = substituteVtsFreeTerms( n ); + Trace("quant-vts-debug") << "...return " << nlit << std::endl; + //Assert( false ); + return nlit; } } } return n; }else if( n.getKind()==FORALL ){ //cannot traverse beneath quantifiers - std::vector< Node > vars; - getVtsTerms( vars, false ); - std::vector< Node > vars_free; - getVtsTerms( vars_free, true ); - Assert( vars.size()==vars_free.size() ); - if( !vars.empty() ){ - n = n.substitute( vars.begin(), vars.end(), vars_free.begin(), vars_free.end() ); - } - return n; + return substituteVtsFreeTerms( n ); }else{ bool childChanged = false; std::vector< Node > children; diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 529207390..9c5a7cc56 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -353,6 +353,8 @@ private: std::map< TypeNode, Node > d_vts_inf_free; /** get vts infinity index */ Node getVtsInfinityIndex( int i, bool isFree = false, bool create = true ); + /** substitute vts free terms */ + Node substituteVtsFreeTerms( Node n ); public: /** get vts delta */ Node getVtsDelta( bool isFree = false, bool create = true ); diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 649d34922..373a8a0da 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -169,7 +169,7 @@ Node TheoryQuantifiers::getNextDecisionRequest(){ void TheoryQuantifiers::assertUniversal( Node n ){ Assert( n.getKind()==FORALL ); - if( options::recurseCbqi() || !TermDb::hasInstConstAttr(n) ){ + if( !options::cbqi() || options::recurseCbqi() || !TermDb::hasInstConstAttr(n) ){ getQuantifiersEngine()->assertQuantifier( n, true ); } } diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index d1a268950..ca16d2ab1 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -620,9 +620,9 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std //do virtual term substitution if( doVts ){ body = Rewriter::rewrite( body ); - Trace("inst-debug") << "Rewrite vts symbols in " << body << std::endl; + Trace("quant-vts-debug") << "Rewrite vts symbols in " << body << std::endl; Node body_r = d_term_db->rewriteVtsSymbols( body ); - Trace("inst-debug") << " ...result: " << body_r << std::endl; + Trace("quant-vts-debug") << " ...result: " << body_r << std::endl; body = body_r; } Trace("inst-assert") << "(assert " << body << ")" << std::endl; @@ -804,15 +804,15 @@ bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, b bool QuantifiersEngine::addLemma( Node lem, bool doCache ){ if( doCache ){ lem = Rewriter::rewrite(lem); - Trace("inst-add-debug2") << "Adding lemma : " << lem << std::endl; + Trace("inst-add-debug") << "Adding lemma : " << lem << std::endl; if( d_lemmas_produced_c.find( lem )==d_lemmas_produced_c.end() ){ //d_curr_out->lemma( lem, false, true ); d_lemmas_produced_c[ lem ] = true; d_lemmas_waiting.push_back( lem ); - Trace("inst-add-debug2") << "Added lemma" << std::endl; + Trace("inst-add-debug") << "Added lemma" << std::endl; return true; }else{ - Trace("inst-add-debug2") << "Duplicate." << std::endl; + Trace("inst-add-debug") << "Duplicate." << std::endl; return false; } }else{ diff --git a/test/regress/regress0/quantifiers/ARI176e1.smt2 b/test/regress/regress0/quantifiers/ARI176e1.smt2 index dbeb96f29..caed9c603 100644 --- a/test/regress/regress0/quantifiers/ARI176e1.smt2 +++ b/test/regress/regress0/quantifiers/ARI176e1.smt2 @@ -1,5 +1,5 @@ ; COMMAND-LINE: --cbqi-recurse ; EXPECT: unsat -(set-logic UFLIA) +(set-logic LIA) (assert (forall ((U Int) (V Int)) (not (= (* 3 U) (+ 22 (* (- 5) V)))) ) ) (check-sat)