diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-10 15:20:33 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-10 15:20:41 -0500 |
commit | 5e4ed407978b892e04de00994be535f58fb33257 (patch) | |
tree | 5ff2dfbf18845113c5ea0fa43e8792532498d2ec /src/theory/quantifiers | |
parent | c833e176a81eb193462c0efde0c6c2f28c5159fb (diff) |
More work on instantiation propagation. Enable external filtering of instantiations. All quantifiers strategies terminate when a conflict can be established.
Diffstat (limited to 'src/theory/quantifiers')
19 files changed, 1087 insertions, 981 deletions
diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp index 18496b173..dd6db951d 100644 --- a/src/theory/quantifiers/ambqi_builder.cpp +++ b/src/theory/quantifiers/ambqi_builder.cpp @@ -190,7 +190,7 @@ bool AbsDef::addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, success = true; } } - }while( !success && index<32 ); + }while( !qe->inConflict() && !success && index<32 ); //mark if we are incomplete osuccess = osuccess && success; } diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index b17286dba..33856d226 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -33,8 +33,8 @@ using namespace std; namespace CVC4 { -bool CegqiOutputSingleInv::addInstantiation( std::vector< Node >& subs ) { - return d_out->addInstantiation( subs ); +bool CegqiOutputSingleInv::doAddInstantiation( std::vector< Node >& subs ) { + return d_out->doAddInstantiation( subs ); } bool CegqiOutputSingleInv::isEligibleForInstantiation( Node n ) { @@ -55,12 +55,12 @@ CegConjectureSingleInv::CegConjectureSingleInv( QuantifiersEngine * qe, CegConje } d_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, d_cosi, false, false ); + d_cinst = new CegInstantiator( d_qe, d_cosi, false, false ); d_sol = new CegConjectureSingleInvSol( qe ); d_sip = new SingleInvocationPartition; - + if( options::cegqiSingleInvPartial() ){ d_ei = new CegEntailmentInfer( qe, d_sip ); }else{ @@ -104,7 +104,7 @@ void CegConjectureSingleInv::getInitialSingleInvLemma( std::vector< Node >& lems if( d_cinst ){ delete d_cinst; } - d_cinst = new CegInstantiator( d_qe, d_cosi, false, false ); + d_cinst = new CegInstantiator( d_qe, d_cosi, false, false ); d_cinst->registerCounterexampleLemma( lems, d_single_inv_sk ); } } @@ -480,7 +480,7 @@ void CegConjectureSingleInv::initializeNextSiConjecture() { if( d_single_inv.isNull() ){ if( d_ei->getEntailedConjecture( d_single_inv, d_single_inv_exp ) ){ Trace("cegqi-nsi") << "NSI : got : " << d_single_inv << std::endl; - Trace("cegqi-nsi") << "NSI : exp : " << d_single_inv_exp << std::endl; + Trace("cegqi-nsi") << "NSI : exp : " << d_single_inv_exp << std::endl; }else{ Trace("cegqi-nsi") << "NSI : failed to construct next conjecture." << std::endl; Notice() << "Incomplete due to --cegqi-si-partial." << std::endl; @@ -491,7 +491,7 @@ void CegConjectureSingleInv::initializeNextSiConjecture() { Trace("cegqi-nsi") << "NSI : have : " << d_single_inv << std::endl; Assert( d_single_inv_exp.isNull() ); } - + d_si_guard = Node::null(); d_ns_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "GS", NodeManager::currentNM()->booleanType() ) ); d_ns_guard = d_qe->getValuation().ensureLiteral( d_ns_guard ); @@ -508,7 +508,7 @@ void CegConjectureSingleInv::initializeNextSiConjecture() { Trace("cegqi-nsi") << "NSI : conjecture is " << d_single_inv << std::endl; } -bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs ){ +bool CegConjectureSingleInv::doAddInstantiation( std::vector< Node >& subs ){ std::stringstream siss; if( Trace.isOn("cegqi-si-inst-debug") || Trace.isOn("cegqi-engine") ){ siss << " * single invocation: " << std::endl; @@ -843,7 +843,7 @@ bool SingleInvocationPartition::init( Node n ) { std::vector< TypeNode > typs; std::map< Node, bool > visited; if( inferArgTypes( n, typs, visited ) ){ - return init( typs, n ); + return init( typs, n ); }else{ Trace("si-prt") << "Could not infer argument types." << std::endl; return false; diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h index 6d47b8d9a..4d2f9a0e5 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h @@ -37,7 +37,7 @@ public: CegqiOutputSingleInv( CegConjectureSingleInv * out ) : d_out( out ){} ~CegqiOutputSingleInv() {} CegConjectureSingleInv * d_out; - bool addInstantiation( std::vector< Node >& subs ); + bool doAddInstantiation( std::vector< Node >& subs ); bool isEligibleForInstantiation( Node n ); bool addLemma( Node lem ); }; @@ -102,7 +102,7 @@ public: private: std::vector< Node > d_curr_lemmas; //add instantiation - bool addInstantiation( std::vector< Node >& subs ); + bool doAddInstantiation( std::vector< Node >& subs ); //is eligible for instantiation bool isEligibleForInstantiation( Node n ); // add lemma diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index 6a56977b8..da488ea98 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -65,9 +65,9 @@ void CegInstantiator::computeProgVars( Node n ){ } } -bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars, - std::vector< int >& btyp, Node theta, unsigned i, unsigned effort, - std::map< Node, Node >& cons, std::vector< Node >& curr_var ){ +bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars, + std::vector< int >& btyp, Node theta, unsigned i, unsigned effort, + std::map< Node, Node >& cons, std::vector< Node >& curr_var ){ if( i==d_vars.size() ){ //solved for all variables, now construct instantiation if( !sf.d_has_coeff.empty() ){ @@ -75,12 +75,12 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve //use symbolic solved forms SolvedForm csf; csf.copy( ssf ); - return addInstantiationCoeff( csf, vars, btyp, 0, cons ); + return doAddInstantiationCoeff( csf, vars, btyp, 0, cons ); }else{ - return addInstantiationCoeff( sf, vars, btyp, 0, cons ); + return doAddInstantiationCoeff( sf, vars, btyp, 0, cons ); } }else{ - return addInstantiation( sf.d_subs, vars, cons ); + return doAddInstantiation( sf.d_subs, vars, cons ); } }else{ std::map< Node, std::map< Node, bool > > subs_proc; @@ -139,7 +139,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve if( proc ){ //try the substitution subs_proc[ns][pv_coeff] = true; - if( addInstantiationInc( ns, pv, pv_coeff, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ + if( doAddInstantiationInc( ns, pv, pv_coeff, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ return true; } } @@ -163,7 +163,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve for( unsigned j=0; j<dt[cindex].getNumArgs(); j++ ){ curr_var.push_back( NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex][j].getSelector() ), pv ) ); } - if( addInstantiation( sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ + if( doAddInstantiation( sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ return true; }else{ //cleanup @@ -270,7 +270,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve Node val = veq[1]; if( subs_proc[val].find( veq_c )==subs_proc[val].end() ){ subs_proc[val][veq_c] = true; - if( addInstantiationInc( val, pv, veq_c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ + if( doAddInstantiationInc( val, pv, veq_c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ return true; } } @@ -286,7 +286,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve if( success ){ if( subs_proc[val].find( veq_c )==subs_proc[val].end() ){ subs_proc[val][veq_c] = true; - if( addInstantiationInc( val, pv, veq_c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ + if( doAddInstantiationInc( val, pv, veq_c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ return true; } } @@ -455,7 +455,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve //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, uires>0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ + if( doAddInstantiationInc( uval, pv, veq_c, uires>0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ return true; } } @@ -492,7 +492,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve val = NodeManager::currentNM()->mkNode( UMINUS, val ); val = Rewriter::rewrite( val ); } - if( addInstantiationInc( val, pv, Node::null(), 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ + if( doAddInstantiationInc( val, pv, Node::null(), 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ return true; } } @@ -588,7 +588,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve 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], rr==0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ + if( doAddInstantiationInc( val, pv, mbp_coeff[rr][best], rr==0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ return true; } } @@ -605,7 +605,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve if( !val.isNull() ){ if( subs_proc[val].find( c )==subs_proc[val].end() ){ subs_proc[val][c] = true; - if( addInstantiationInc( val, pv, c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ + if( doAddInstantiationInc( val, pv, c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ return true; } } @@ -649,7 +649,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve if( !val.isNull() ){ if( subs_proc[val].find( Node::null() )==subs_proc[val].end() ){ subs_proc[val][Node::null()] = true; - if( addInstantiationInc( val, pv, Node::null(), 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ + if( doAddInstantiationInc( val, pv, Node::null(), 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ return true; } } @@ -670,7 +670,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve if( !val.isNull() ){ if( subs_proc[val].find( mbp_coeff[rr][j] )==subs_proc[val].end() ){ subs_proc[val][mbp_coeff[rr][j]] = true; - if( addInstantiationInc( val, pv, mbp_coeff[rr][j], rr==0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ + if( doAddInstantiationInc( val, pv, mbp_coeff[rr][j], rr==0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){ return true; } } @@ -694,7 +694,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve //we only resort to values in the case of booleans Assert( ( pvtn.isInteger() ? !options::cbqiUseInfInt() : !options::cbqiUseInfReal() ) || pvtn.isBoolean() ); #endif - if( addInstantiationInc( mv, pv, pv_coeff_m, 0, sf, ssf, vars, btyp, theta, i, new_effort, cons, curr_var ) ){ + if( doAddInstantiationInc( mv, pv, pv_coeff_m, 0, sf, ssf, vars, btyp, theta, i, new_effort, cons, curr_var ) ){ return true; } } @@ -704,9 +704,9 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve } -bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars, - std::vector< int >& btyp, Node theta, unsigned i, unsigned effort, - std::map< Node, Node >& cons, std::vector< Node >& curr_var ) { +bool CegInstantiator::doAddInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars, + std::vector< int >& btyp, Node theta, unsigned i, unsigned effort, + std::map< Node, Node >& cons, std::vector< Node >& curr_var ) { if( Trace.isOn("cbqi-inst") ){ for( unsigned j=0; j<sf.d_subs.size(); j++ ){ Trace("cbqi-inst") << " "; @@ -800,7 +800,7 @@ bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int b curr_var.pop_back(); is_cv = true; } - success = addInstantiation( sf, ssf, vars, btyp, new_theta, curr_var.empty() ? i+1 : i, effort, cons, curr_var ); + success = doAddInstantiation( sf, ssf, vars, btyp, new_theta, curr_var.empty() ? i+1 : i, effort, cons, curr_var ); if( !success ){ if( is_cv ){ curr_var.push_back( pv ); @@ -831,12 +831,12 @@ bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int b } } -bool CegInstantiator::addInstantiationCoeff( SolvedForm& sf, std::vector< Node >& vars, std::vector< int >& btyp, +bool CegInstantiator::doAddInstantiationCoeff( SolvedForm& sf, std::vector< Node >& vars, std::vector< int >& btyp, unsigned j, std::map< Node, Node >& cons ) { if( j==sf.d_has_coeff.size() ){ - return addInstantiation( sf.d_subs, vars, cons ); + return doAddInstantiation( sf.d_subs, vars, cons ); }else{ Assert( std::find( vars.begin(), vars.end(), sf.d_has_coeff[j] )!=vars.end() ); unsigned index = std::find( vars.begin(), vars.end(), sf.d_has_coeff[j] )-vars.begin(); @@ -894,7 +894,7 @@ bool CegInstantiator::addInstantiationCoeff( SolvedForm& sf, std::vector< Node > } } } - if( addInstantiationCoeff( sf, vars, btyp, j+1, cons ) ){ + if( doAddInstantiationCoeff( sf, vars, btyp, j+1, cons ) ){ return true; } } @@ -905,7 +905,7 @@ bool CegInstantiator::addInstantiationCoeff( SolvedForm& sf, std::vector< Node > } } -bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::map< Node, Node >& cons ) { +bool CegInstantiator::doAddInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::map< Node, Node >& cons ) { if( vars.size()>d_vars.size() ){ Trace("cbqi-inst-debug") << "Reconstructing instantiations...." << std::endl; std::map< Node, Node > subs_map; @@ -927,7 +927,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< subs.push_back( subs_orig[d_var_order_index[i]] ); } } - bool ret = d_out->addInstantiation( subs ); + bool ret = d_out->doAddInstantiation( subs ); #ifdef MBP_STRICT_ASSERTIONS Assert( ret ); #endif @@ -1127,7 +1127,7 @@ bool CegInstantiator::check() { std::map< Node, Node > cons; std::vector< Node > curr_var; //try to add an instantiation - if( addInstantiation( sf, ssf, vars, btyp, theta, 0, r==0 ? 0 : 2, cons, curr_var ) ){ + if( doAddInstantiation( sf, ssf, vars, btyp, theta, 0, r==0 ? 0 : 2, cons, curr_var ) ){ return true; } } @@ -1499,7 +1499,7 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st } } -//this isolates the atom into solved form +//this isolates the atom into solved form // veq_c * pv <> val + vts_coeff_delta * delta + vts_coeff_inf * inf // ensures val is Int if pv is Int, and val does not contain vts symbols int CegInstantiator::solve_arith( Node pv, Node atom, Node& veq_c, Node& val, Node& vts_coeff_inf, Node& vts_coeff_delta ) { diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h index 36c6f1bce..3d7bbcb55 100644 --- a/src/theory/quantifiers/ceg_instantiator.h +++ b/src/theory/quantifiers/ceg_instantiator.h @@ -33,7 +33,7 @@ namespace quantifiers { class CegqiOutput { public: virtual ~CegqiOutput() {} - virtual bool addInstantiation( std::vector< Node >& subs ) = 0; + virtual bool doAddInstantiation( std::vector< Node >& subs ) = 0; virtual bool isEligibleForInstantiation( Node n ) = 0; virtual bool addLemma( Node lem ) = 0; }; @@ -108,16 +108,16 @@ private: }; */ // effort=0 : do not use model value, 1: use model value, 2: one must use model value - bool addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars, + bool doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars, std::vector< int >& btyp, Node theta, unsigned i, unsigned effort, std::map< Node, Node >& cons, std::vector< Node >& curr_var ); - bool addInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars, + bool doAddInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars, std::vector< int >& btyp, Node theta, unsigned i, unsigned effort, std::map< Node, Node >& cons, std::vector< Node >& curr_var ); - bool addInstantiationCoeff( SolvedForm& sf, + bool doAddInstantiationCoeff( SolvedForm& sf, std::vector< Node >& vars, std::vector< int >& btyp, unsigned j, std::map< Node, Node >& cons ); - bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::map< Node, Node >& cons ); + bool doAddInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::map< Node, Node >& cons ); Node constructInstantiation( Node n, std::map< Node, Node >& subs_map, std::map< Node, Node >& cons ); Node applySubstitution( TypeNode tn, Node n, SolvedForm& sf, std::vector< Node >& vars, Node& pv_coeff, bool try_coeff = true ) { return applySubstitution( tn, n, sf.d_subs, sf.d_coeff, sf.d_has_coeff, vars, pv_coeff, try_coeff ); diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index d06e9f7f7..0276cf7ab 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -591,6 +591,7 @@ void FullModelChecker::debugPrint(const char * tr, Node n, bool dispStar) { bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { Trace("fmc") << "Full model check " << f << ", effort = " << effort << "..." << std::endl; + Assert( !d_qe->inConflict() ); if( optUseModel() ){ FirstOrderModelFmc * fmfmc = fm->asFirstOrderModelFmc(); if (effort==0) { @@ -684,7 +685,7 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, if( d_qe->addInstantiation( f, inst ) ){ Trace("fmc-debug-inst") << "** Added instantiation." << std::endl; d_addedLemmas++; - if( options::fmfOneInstPerRound() ){ + if( d_qe->inConflict() || options::fmfOneInstPerRound() ){ break; } }else{ @@ -812,7 +813,7 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No if( d_qe->addInstantiation( f, inst ) ){ Trace("fmc-exh-debug") << " ...success."; addedLemmas++; - if( options::fmfOneInstPerRound() ){ + if( d_qe->inConflict() || options::fmfOneInstPerRound() ){ break; } }else{ diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index 1751f3a87..55a4e8f8c 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -155,20 +155,6 @@ bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< No return ret; } } - /* - //check if m is an instance of another instantiation if modInst is true - if( modInst ){ - if( !n.isNull() ){ - Node nl; - std::map< Node, InstMatchTrie >::iterator itm = d_data.find( nl ); - if( itm!=d_data.end() ){ - if( !itm->second.addInstMatch( qe, f, m, modEq, modInst, imtio, true, index+1 ) ){ - return false; - } - } - } - } - */ if( modEq ){ //check modulo equality if any other instantiation match exists if( !n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){ @@ -195,6 +181,24 @@ bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< No } } +bool InstMatchTrie::removeInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, ImtIndexOrder* imtio, int index ) { + Assert( index<(int)q[0].getNumChildren() ); + Assert( !imtio || index<(int)imtio->d_order.size() ); + int i_index = imtio ? imtio->d_order[index] : index; + Node n = m[i_index]; + std::map< Node, InstMatchTrie >::iterator it = d_data.find( n ); + if( it!=d_data.end() ){ + if( (index+1)==(int)q[0].getNumChildren() || ( imtio && (index+1)==(int)imtio->d_order.size() ) ){ + d_data.erase( n ); + return true; + }else{ + return it->second.removeInstMatch( qe, q, m, imtio, index+1 ); + } + }else{ + return false; + } +} + void InstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& terms ) const { if( terms.size()==q[0].getNumChildren() ){ out << " ( "; @@ -257,20 +261,6 @@ bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< return reset || ret; } } - //check if m is an instance of another instantiation if modInst is true - /* - if( modInst ){ - if( !n.isNull() ){ - Node nl; - std::map< Node, CDInstMatchTrie* >::iterator itm = d_data.find( nl ); - if( itm!=d_data.end() ){ - if( !itm->second->addInstMatch( qe, f, m, c, modEq, modInst, index+1, true ) ){ - return false; - } - } - } - } - */ if( modEq ){ //check modulo equality if any other instantiation match exists if( !n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){ @@ -302,6 +292,25 @@ bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< } } +bool CDInstMatchTrie::removeInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, int index ) { + if( index==(int)q[0].getNumChildren() ){ + if( d_valid.get() ){ + d_valid.set( false ); + return true; + }else{ + return false; + } + }else{ + Node n = m[index]; + std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n ); + if( it!=d_data.end() ){ + return it->second->removeInstMatch( qe, q, m, index+1 ); + }else{ + return false; + } + } +} + void CDInstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& terms ) const{ if( d_valid.get() ){ if( terms.size()==q[0].getNumChildren() ){ diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index fbdef61c2..a87d2704e 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -128,6 +128,7 @@ public: } bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false, bool modInst = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 ); + bool removeInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, ImtIndexOrder* imtio = NULL, int index = 0 ); void print( std::ostream& out, Node q ) const{ std::vector< TNode > terms; print( out, q, terms ); @@ -157,24 +158,25 @@ public: modEq is if we check modulo equality modInst is if we return true if m is an instance of a match that exists */ - bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, bool modEq = false, + bool existsInstMatch( QuantifiersEngine* qe, Node q, InstMatch& m, context::Context* c, bool modEq = false, bool modInst = false, int index = 0 ) { - return !addInstMatch( qe, f, m, c, modEq, modInst, index, true ); + return !addInstMatch( qe, q, m, c, modEq, modInst, index, true ); } - bool existsInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, context::Context* c, bool modEq = false, + bool existsInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, context::Context* c, bool modEq = false, bool modInst = false, int index = 0 ) { - return !addInstMatch( qe, f, m, c, modEq, modInst, index, true ); + return !addInstMatch( qe, q, m, c, modEq, modInst, index, true ); } /** add match m for quantifier f, take into account equalities if modEq = true, if imtio is non-null, this is the order to add to trie return true if successful */ - bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, bool modEq = false, + bool addInstMatch( QuantifiersEngine* qe, Node q, InstMatch& m, context::Context* c, bool modEq = false, bool modInst = false, int index = 0, bool onlyExist = false ) { - return addInstMatch( qe, f, m.d_vals, c, modEq, modInst, index, onlyExist ); + return addInstMatch( qe, q, m.d_vals, c, modEq, modInst, index, onlyExist ); } - bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, context::Context* c, bool modEq = false, + bool addInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, context::Context* c, bool modEq = false, bool modInst = false, int index = 0, bool onlyExist = false ); + bool removeInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, int index = 0 ); void print( std::ostream& out, Node q ) const{ std::vector< TNode > terms; print( out, q, terms ); diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index cfa4190e4..29754d3e6 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -126,7 +126,7 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector< if( d_pattern.getKind()==NOT && ( d_pattern[0].getKind()==IFF || d_pattern[0].getKind()==EQUAL ) ){ ((inst::CandidateGeneratorQE*)d_cg)->excludeEqc( d_eq_class_rel ); d_eq_class_rel = Node::null(); - } + } }else if( d_match_pattern.getKind()==INST_CONSTANT ){ if( d_pattern.getKind()==APPLY_SELECTOR_TOTAL ){ Expr selectorExpr = qe->getTermDatabase()->getMatchOperator( d_pattern ).toExpr(); @@ -139,7 +139,7 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector< }else{ d_cg = new CandidateGeneratorQEAll( qe, d_match_pattern ); } - }else if( ( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ) && + }else if( ( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ) && d_match_pattern[0].getKind()==INST_CONSTANT && d_match_pattern[1].getKind()==INST_CONSTANT ){ //we will be producing candidates via literal matching heuristics if( d_pattern.getKind()!=NOT ){ @@ -307,6 +307,9 @@ void InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){ } bool InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ){ + if( qe->inConflict() ){ + return false; + } if( d_needsReset ){ Trace("matching") << "Reset not done yet, must do the reset..." << std::endl; reset( d_eq_class, qe ); @@ -767,15 +770,20 @@ void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngin m.setValue( v, t); addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) ); m.setValue( v, prev); + if( qe->inConflict() ){ + break; + } } } return; } } - Node r = qe->getEqualityQuery()->getRepresentative( d_match_pattern[argIndex] ); - std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.find( r ); - if( it!=tat->d_data.end() ){ - addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) ); + if( !qe->inConflict() ){ + Node r = qe->getEqualityQuery()->getRepresentative( d_match_pattern[argIndex] ); + std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.find( r ); + if( it!=tat->d_data.end() ){ + addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) ); + } } } } diff --git a/src/theory/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp index d20f3fd4a..863914567 100644 --- a/src/theory/quantifiers/inst_propagator.cpp +++ b/src/theory/quantifiers/inst_propagator.cpp @@ -1,674 +1,728 @@ -/********************* */
-/*! \file inst_propagator.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** Propagate mechanism for instantiations
- **/
-
-#include <vector>
-
-#include "theory/quantifiers/inst_propagator.h"
-#include "theory/rewriter.h"
-#include "theory/quantifiers/term_database.h"
-
-using namespace CVC4;
-using namespace std;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-using namespace CVC4::kind;
-
-
-EqualityQueryInstProp::EqualityQueryInstProp( QuantifiersEngine* qe ) : d_qe( qe ){
- d_true = NodeManager::currentNM()->mkConst( true );
- d_false = NodeManager::currentNM()->mkConst( false );
-}
-
-bool EqualityQueryInstProp::reset( Theory::Effort e ) {
- d_uf.clear();
- d_uf_exp.clear();
- d_diseq_list.clear();
- return true;
-}
-
-/** contains term */
-bool EqualityQueryInstProp::hasTerm( Node a ) {
- if( getEngine()->hasTerm( a ) ){
- return true;
- }else{
- std::vector< Node > exp;
- Node ar = getUfRepresentative( a, exp );
- return !ar.isNull() && getEngine()->hasTerm( ar );
- }
-}
-
-/** get the representative of the equivalence class of a */
-Node EqualityQueryInstProp::getRepresentative( Node a ) {
- if( getEngine()->hasTerm( a ) ){
- a = getEngine()->getRepresentative( a );
- }
- std::vector< Node > exp;
- Node ar = getUfRepresentative( a, exp );
- return ar.isNull() ? a : ar;
-}
-
-/** returns true if a and b are equal in the current context */
-bool EqualityQueryInstProp::areEqual( Node a, Node b ) {
- if( a==b ){
- return true;
- }else{
- eq::EqualityEngine* ee = getEngine();
- if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
- if( ee->areEqual( a, b ) ){
- return true;
- }
- }
- return false;
- }
-}
-
-/** returns true is a and b are disequal in the current context */
-bool EqualityQueryInstProp::areDisequal( Node a, Node b ) {
- if( a==b ){
- return true;
- }else{
- eq::EqualityEngine* ee = getEngine();
- if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
- if( ee->areDisequal( a, b, false ) ){
- return true;
- }
- }
- return false;
- }
-}
-
-/** get the equality engine associated with this query */
-eq::EqualityEngine* EqualityQueryInstProp::getEngine() {
- return d_qe->getMasterEqualityEngine();
-}
-
-/** get the equivalence class of a */
-void EqualityQueryInstProp::getEquivalenceClass( Node a, std::vector< Node >& eqc ) {
- //TODO?
-}
-
-TNode EqualityQueryInstProp::getCongruentTerm( Node f, std::vector< TNode >& args ) {
- TNode t = d_qe->getTermDatabase()->getCongruentTerm( f, args );
- if( !t.isNull() ){
- return t;
- }else{
- //TODO?
- return TNode::null();
- }
-}
-
-Node EqualityQueryInstProp::getRepresentativeExp( Node a, std::vector< Node >& exp ) {
- bool engine_has_a = getEngine()->hasTerm( a );
- if( engine_has_a ){
- a = getEngine()->getRepresentative( a );
- }
- //get union find representative, if this occurs in the equality engine, return it
- unsigned prev_size = exp.size();
- Node ar = getUfRepresentative( a, exp );
- if( !ar.isNull() ){
- if( engine_has_a || getEngine()->hasTerm( ar ) ){
- Assert( getEngine()->hasTerm( ar ) );
- Assert( getEngine()->getRepresentative( ar )==ar );
- return ar;
- }
- }else{
- if( engine_has_a ){
- return a;
- }
- }
- //retract explanation
- while( exp.size()>prev_size ){
- exp.pop_back();
- }
- return Node::null();
-}
-
-bool EqualityQueryInstProp::areEqualExp( Node a, Node b, std::vector< Node >& exp ) {
- if( areEqual( a, b ) ){
- return true;
- }else{
- std::vector< Node > exp_a;
- Node ar = getUfRepresentative( a, exp_a );
- if( !ar.isNull() ){
- std::vector< Node > exp_b;
- if( ar==getUfRepresentative( b, exp_b ) ){
- merge_exp( exp, exp_a );
- merge_exp( exp, exp_b );
- return true;
- }
- }
- return false;
- }
-}
-
-bool EqualityQueryInstProp::areDisequalExp( Node a, Node b, std::vector< Node >& exp ) {
- if( areDisequal( a, b ) ){
- return true;
- }else{
- //TODO?
- return false;
- }
-}
-
-Node EqualityQueryInstProp::getUfRepresentative( Node a, std::vector< Node >& exp ) {
- Assert( exp.empty() );
- std::map< Node, Node >::iterator it = d_uf.find( a );
- if( it!=d_uf.end() ){
- if( it->second==a ){
- Assert( d_uf_exp[ a ].empty() );
- return it->second;
- }else{
- Node m = getUfRepresentative( it->second, exp );
- Assert( !m.isNull() );
- if( m!=it->second ){
- //update union find
- d_uf[ a ] = m;
- //update explanation : merge the explanation of the parent
- merge_exp( d_uf_exp[ a ], exp );
- Trace("qip-eq") << "EqualityQueryInstProp::getUfRepresentative : merge " << a << " -> " << m << ", exp size=" << d_uf_exp[ a ].size() << std::endl;
- }
- //add current explanation to exp: note that exp is a subset of d_uf_exp[ a ], reset
- exp.clear();
- exp.insert( exp.end(), d_uf_exp[ a ].begin(), d_uf_exp[ a ].end() );
- return m;
- }
- }else{
- return Node::null();
- }
-}
-
-// set a == b with reason, return status, modify a and b to representatives pre-merge
-int EqualityQueryInstProp::setEqual( Node& a, Node& b, std::vector< Node >& reason ) {
- int status = STATUS_MERGED_UNKNOWN;
- Trace("qip-eq") << "EqualityQueryInstProp::setEqual " << a << ", " << b << ", reason size = " << reason.size() << std::endl;
- //get the representative for a
- std::vector< Node > exp_a;
- Node ar = getUfRepresentative( a, exp_a );
- if( ar.isNull() ){
- Assert( exp_a.empty() );
- ar = a;
- }
- if( ar==b ){
- Trace("qip-eq") << "EqualityQueryInstProp::setEqual : already equal" << std::endl;
- return STATUS_NONE;
- }
- bool swap = false;
- //get the representative for b
- std::vector< Node > exp_b;
- Node br = getUfRepresentative( b, exp_b );
- if( br.isNull() ){
- Assert( exp_b.empty() );
- br = b;
- if( !getEngine()->hasTerm( br ) ){
- if( ar!=a ){
- swap = true;
- }
- }else{
- if( getEngine()->hasTerm( ar ) ){
- status = STATUS_MERGED_KNOWN;
- }
- }
- }else{
- if( ar==br ){
- Trace("qip-eq") << "EqualityQueryInstProp::setEqual : already equal" << std::endl;
- return STATUS_NONE;
- }else if( getEngine()->hasTerm( ar ) ){
- if( getEngine()->hasTerm( br ) ){
- status = STATUS_MERGED_KNOWN;
- }else{
- swap = true;
- }
- }
- }
- if( swap ){
- //swap
- Node temp_r = ar;
- ar = br;
- br = temp_r;
- }
-
- Assert( ar!=br );
- Assert( !getEngine()->hasTerm( ar ) || getEngine()->hasTerm( br ) );
-
- //update the union find
- Assert( d_uf_exp[ar].empty() );
- Assert( d_uf_exp[br].empty() );
-
- d_uf[ar] = br;
- merge_exp( d_uf_exp[ar], exp_a );
- merge_exp( d_uf_exp[ar], exp_b );
- merge_exp( d_uf_exp[ar], reason );
-
- d_uf[br] = br;
- d_uf_exp[br].clear();
-
- Trace("qip-eq") << "EqualityQueryInstProp::setEqual : merge " << ar << " -> " << br << ", exp size = " << d_uf_exp[ar].size() << ", status = " << status << std::endl;
- a = ar;
- b = br;
- return status;
-}
-
-
-void EqualityQueryInstProp::addArgument( std::vector< TNode >& args, std::vector< TNode >& props, Node n, bool is_prop, bool pol ) {
- if( is_prop ){
- if( isLiteral( n ) ){
- props.push_back( pol ? n : n.negate() );
- return;
- }
- }
- args.push_back( n );
-}
-
-bool EqualityQueryInstProp::isLiteral( Node n ) {
- Kind ak = n.getKind()==NOT ? n[0].getKind() : n.getKind();
- Assert( ak!=NOT );
- return ak!=AND && ak!=OR && ak!=IFF && ak!=ITE;
-}
-
-//this is identical to TermDb::evaluateTerm2, but tracks more information
-Node EqualityQueryInstProp::evaluateTermExp( TNode n, std::vector< Node >& exp, std::map< TNode, Node >& visited, bool hasPol, bool pol,
- std::map< Node, bool >& watch_list_out, std::vector< TNode >& props ) {
- std::map< TNode, Node >::iterator itv = visited.find( n );
- if( itv != visited.end() ){
- return itv->second;
- }else{
- Trace("term-db-eval") << "evaluate term : " << n << std::endl;
- std::vector< Node > exp_n;
- Node ret = getRepresentativeExp( n, exp_n );
- if( ret.isNull() ){
- //term is not known to be equal to a representative in equality engine, evaluate it
- Kind k = n.getKind();
- if( k==FORALL ){
- ret = Node::null();
- }else{
- std::map< Node, bool > watch_list_out_curr;
- TNode f = d_qe->getTermDatabase()->getMatchOperator( n );
- std::vector< TNode > args;
- bool ret_set = false;
- bool childChanged = false;
- int abort_i = -1;
- //get the child entailed polarity
- Assert( n.getKind()!=IMPLIES );
- bool newHasPol, newPol;
- QuantPhaseReq::getEntailPolarity( n, 0, hasPol, pol, newHasPol, newPol );
- //for each child
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- TNode c = evaluateTermExp( n[i], exp, visited, newHasPol, newPol, watch_list_out_curr, props );
- if( c.isNull() ){
- ret = Node::null();
- ret_set = true;
- break;
- }else if( c==d_true || c==d_false ){
- //short-circuiting
- if( k==kind::AND || k==kind::OR ){
- if( (k==kind::AND)==(c==d_false) ){
- ret = c;
- ret_set = true;
- break;
- }else{
- //redundant
- c = Node::null();
- childChanged = true;
- }
- }else if( k==kind::ITE && i==0 ){
- Assert( watch_list_out_curr.empty() );
- ret = evaluateTermExp( n[ c==d_true ? 1 : 2], exp, visited, hasPol, pol, watch_list_out_curr, props );
- ret_set = true;
- break;
- }else if( k==kind::NOT ){
- ret = c==d_true ? d_false : d_true;
- ret_set = true;
- break;
- }
- }
- if( !c.isNull() ){
- childChanged = childChanged || n[i]!=c;
- if( !f.isNull() && !watch_list_out_curr.empty() ){
- // we are done if this is an UF application and an argument is unevaluated
- args.push_back( c );
- abort_i = i;
- break;
- }else if( ( k==kind::AND || k==kind::OR ) ){
- if( c.getKind()==k ){
- //flatten
- for( unsigned j=0; j<c.getNumChildren(); j++ ){
- addArgument( args, props, c[j], newHasPol, newPol );
- }
- }else{
- addArgument( args, props, c, newHasPol, newPol );
- }
- //if we are in a branching position
- if( hasPol && !newHasPol && args.size()>=2 ){
- //we are done if at least two args are unevaluated
- abort_i = i;
- break;
- }
- }else if( k==kind::ITE ){
- //we are done if we are ITE and condition is unevaluated
- Assert( i==0 );
- args.push_back( c );
- abort_i = i;
- break;
- }else{
- args.push_back( c );
- }
- }
- }
- //add remaining children if we aborted
- if( abort_i!=-1 ){
- for( int i=(abort_i+1); i<(int)n.getNumChildren(); i++ ){
- args.push_back( n[i] );
- }
- }
- //copy over the watch list
- for( std::map< Node, bool >::iterator itc = watch_list_out_curr.begin(); itc != watch_list_out_curr.end(); ++itc ){
- watch_list_out[itc->first] = itc->second;
- }
-
- //if we have not short-circuited evaluation
- if( !ret_set ){
- //if it is an indexed term, return the congruent term
- if( !f.isNull() && watch_list_out.empty() ){
- Assert( args.size()==n.getNumChildren() );
- //args contains terms known by the equality engine
- TNode nn = getCongruentTerm( f, args );
- Trace("term-db-eval") << " got congruent term " << nn << " from DB for " << n << std::endl;
- if( !nn.isNull() ){
- //successfully constructed representative in EE
- Assert( exp_n.empty() );
- ret = getRepresentativeExp( nn, exp_n );
- Trace("term-db-eval") << "return rep, exp size = " << exp_n.size() << std::endl;
- merge_exp( exp, exp_n );
- ret_set = true;
- Assert( !ret.isNull() );
- }
- }
- if( !ret_set ){
- if( childChanged ){
- Trace("term-db-eval") << "return rewrite" << std::endl;
- if( ( k==kind::AND || k==kind::OR ) ){
- if( args.empty() ){
- ret = k==kind::AND ? d_true : d_false;
- ret_set = true;
- }else if( args.size()==1 ){
- ret = args[0];
- ret_set = true;
- }
- }
- if( !ret_set ){
- Assert( args.size()==n.getNumChildren() );
- if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
- args.insert( args.begin(), n.getOperator() );
- }
- ret = NodeManager::currentNM()->mkNode( k, args );
- ret = Rewriter::rewrite( ret );
- watch_list_out[ret] = true;
- }
- }else{
- ret = n;
- watch_list_out[ret] = true;
- }
- }
- }
- }
- }else{
- Trace("term-db-eval") << "...exists in ee, return rep, exp size = " << exp_n.size() << std::endl;
- merge_exp( exp, exp_n );
- }
- Trace("term-db-eval") << "evaluated term : " << n << ", got : " << ret << ", exp size = " << exp.size() << std::endl;
- visited[n] = ret;
- return ret;
- }
-}
-
-void EqualityQueryInstProp::merge_exp( std::vector< Node >& v, std::vector< Node >& v_to_merge, int up_to_size ) {
- //TODO : optimize
- if( v.empty() ){
- Assert( up_to_size==-1 || up_to_size==(int)v_to_merge.size() );
- v.insert( v.end(), v_to_merge.begin(), v_to_merge.end() );
- }else{
- //std::vector< Node >::iterator v_end = v.end();
- up_to_size = up_to_size==-1 ? (int)v_to_merge.size() : up_to_size;
- for( int j=0; j<up_to_size; j++ ){
- if( std::find( v.begin(), v.end(), v_to_merge[j] )==v.end() ){
- v.push_back( v_to_merge[j] );
- }
- }
- }
-}
-
-
-void InstPropagator::InstInfo::init( Node q, Node lem, std::vector< Node >& terms, Node body ) {
- d_active = true;
- //information about the instance
- d_q = q;
- d_lem = lem;
- Assert( d_terms.empty() );
- d_terms.insert( d_terms.end(), terms.begin(), terms.end() );
- //the current lemma
- d_curr = body;
- d_curr_exp.push_back( body );
-}
-
-InstPropagator::InstPropagator( QuantifiersEngine* qe ) :
-d_qe( qe ), d_notify(*this), d_qy( qe ){
-}
-
-bool InstPropagator::reset( Theory::Effort e ) {
- d_icount = 0;
- d_ii.clear();
- for( unsigned i=0; i<2; i++ ){
- d_conc_to_id[i].clear();
- }
- d_conflict = false;
- d_watch_list.clear();
- d_relevant_inst.clear();
- return d_qy.reset( e );
-}
-
-void InstPropagator::notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) {
- if( !d_conflict ){
- if( Trace.isOn("qip-prop") ){
- Trace("qip-prop") << "InstPropagator:: Notify instantiation " << q << " : " << std::endl;
- for( unsigned i=0; i<terms.size(); i++ ){
- Trace("qip-prop") << " " << terms[i] << std::endl;
- }
- }
- unsigned id = d_icount;
- d_icount++;
- Trace("qip-prop") << "...assign id=" << id << std::endl;
- d_ii[id].init( q, lem, terms, body );
- //initialize the information
- if( cacheConclusion( id, body ) ){
- Assert( d_update_list.empty() );
- d_update_list.push_back( id );
- bool firstTime = true;
- //update infos in the update list until empty
- do {
- unsigned uid = d_update_list.back();
- d_update_list.pop_back();
- if( d_ii[uid].d_active ){
- update( uid, d_ii[uid], firstTime );
- }
- firstTime = false;
- }while( !d_update_list.empty() );
- }else{
- d_ii[id].d_active = false;
- Trace("qip-prop") << "...duplicate." << std::endl;
- }
- }
-}
-
-bool InstPropagator::update( unsigned id, InstInfo& ii, bool firstTime ) {
- Assert( !d_conflict );
- Assert( ii.d_active );
- Trace("qip-prop-debug") << "Update info [" << id << "]..." << std::endl;
- //update the evaluation of the current lemma
- std::map< TNode, Node > visited;
- std::map< Node, bool > watch_list;
- std::vector< TNode > props;
- Node eval = d_qy.evaluateTermExp( ii.d_curr, ii.d_curr_exp, visited, true, true, watch_list, props );
- if( eval.isNull() ){
- ii.d_active = false;
- }else if( firstTime || eval!=ii.d_curr ){
- if( EqualityQueryInstProp::isLiteral( eval ) ){
- props.push_back( eval );
- eval = d_qy.d_true;
- watch_list.clear();
- }
- if( Trace.isOn("qip-prop") ){
- Trace("qip-prop") << "Update info [" << id << "]..." << std::endl;
- Trace("qip-prop") << "...updated lemma " << ii.d_curr << " -> " << eval << ", exp = ";
- debugPrintExplanation( ii.d_curr_exp, "qip-prop" );
- Trace("qip-prop") << std::endl;
- Trace("qip-prop") << "...watch list: " << std::endl;
- for( std::map< Node, bool >::iterator itw = watch_list.begin(); itw!=watch_list.end(); ++itw ){
- Trace("qip-prop") << " " << itw->first << std::endl;
- }
- Trace("qip-prop") << "...new propagations: " << std::endl;
- for( unsigned i=0; i<props.size(); i++ ){
- Trace("qip-prop") << " " << props[i] << std::endl;
- }
- Trace("qip-prop") << std::endl;
- }
- //determine the status of eval
- if( eval==d_qy.d_false ){
- Assert( props.empty() );
- //we have inferred a conflict
- conflict( ii.d_curr_exp );
- return false;
- }else{
- for( unsigned i=0; i<props.size(); i++ ){
- //if we haven't propagated this literal yet
- if( cacheConclusion( id, props[i], 1 ) ){
- Node lit = props[i].getKind()==NOT ? props[i][0] : props[i];
- bool pol = props[i].getKind()!=NOT;
- if( lit.getKind()==EQUAL ){
- propagate( lit[0], lit[1], pol, ii.d_curr_exp );
- }else{
- propagate( lit, pol ? d_qy.d_true : d_qy.d_false, true, ii.d_curr_exp );
- }
- if( d_conflict ){
- return false;
- }
- }
- }
- //if we have not inferred this conclusion yet
- if( cacheConclusion( id, eval ) ){
- ii.d_curr = eval;
- //update the watch list
- Trace("qip-prop-debug") << "...updating watch list for [" << id << "], curr is " << ii.d_curr << std::endl;
- //Here, we need to be notified of enough terms such that if we are not notified, then update( ii ) will return no propagations.
- // Similar to two-watched literals, but since we are in UF, we need to watch all terms on a complete path of two terms.
- for( std::map< Node, bool >::iterator itw = watch_list.begin(); itw != watch_list.end(); ++itw ){
- d_watch_list[ itw->first ][ id ] = true;
- }
- }else{
- Trace("qip-prop-debug") << "...conclusion is duplicate." << std::endl;
- ii.d_active = false;
- }
- }
- }else{
- Trace("qip-prop-debug") << "...did not update." << std::endl;
- }
- Assert( !d_conflict );
- return true;
-}
-
-void InstPropagator::propagate( Node a, Node b, bool pol, std::vector< Node >& exp ) {
- if( Trace.isOn("qip-propagate") ){
- Trace("qip-propagate") << "* Propagate " << a << ( pol ? " == " : " != " ) << b << ", exp = ";
- debugPrintExplanation( exp, "qip-propagate" );
- Trace("qip-propagate") << "..." << std::endl;
- }
- if( pol ){
- std::vector< Node > exp_d;
- if( d_qy.areDisequalExp( a, b, exp_d ) ){
- Trace("qip-prop-debug") << "...conflict." << std::endl;
- EqualityQueryInstProp::merge_exp( exp, exp_d );
- conflict( exp );
- }else{
- //set equal
- int status = d_qy.setEqual( a, b, exp );
- if( status==EqualityQueryInstProp::STATUS_NONE ){
- Trace("qip-prop-debug") << "...already equal." << std::endl;
- return;
- }else if( status==EqualityQueryInstProp::STATUS_MERGED_KNOWN ){
- Assert( d_qy.getEngine()->hasTerm( a ) );
- Assert( d_qy.getEngine()->hasTerm( b ) );
- Trace("qip-prop-debug") << "...equality between known terms." << std::endl;
- addRelevantInstances( exp, "qip-propagate" );
- }
- Trace("qip-prop-debug") << "...merging " << a << " and " << b << std::endl;
- for( unsigned i=0; i<2; i++ ){
- //update terms from watched lists
- Node c = i==0 ? a : b;
- std::map< Node, std::map< unsigned, bool > >::iterator it = d_watch_list.find( c );
- if( it!=d_watch_list.end() ){
- Trace("qip-prop-debug") << "...update ids from watch list of " << c << ", size=" << it->second.size() << "..." << std::endl;
- for( std::map< unsigned, bool >::iterator itw = it->second.begin(); itw != it->second.end(); ++itw ){
- unsigned idw = itw->first;
- if( std::find( d_update_list.begin(), d_update_list.end(), idw )==d_update_list.end() ){
- Trace("qip-prop-debug") << "...will update " << idw << std::endl;
- d_update_list.push_back( idw );
- }
- }
- d_watch_list.erase( c );
- }
- }
- }
- }else{
- std::vector< Node > exp_e;
- if( d_qy.areEqualExp( a, b, exp_e ) ){
- EqualityQueryInstProp::merge_exp( exp, exp_e );
- conflict( exp );
- }else{
- //TODO?
- }
- }
-}
-
-void InstPropagator::conflict( std::vector< Node >& exp ) {
- Trace("qip-propagate") << "Conflict, exp size =" << exp.size() << std::endl;
- d_conflict = true;
- d_relevant_inst.clear();
- addRelevantInstances( exp, "qip-propagate" );
-}
-
-bool InstPropagator::cacheConclusion( unsigned id, Node body, int prop_index ) {
- Assert( prop_index==0 || prop_index==1 );
- //check if the conclusion is non-redundant
- if( d_conc_to_id[prop_index].find( body )==d_conc_to_id[prop_index].end() ){
- d_conc_to_id[prop_index][body] = id;
- return true;
- }else{
- return false;
- }
-}
-
-void InstPropagator::addRelevantInstances( std::vector< Node >& exp, const char * c ) {
- for( unsigned i=0; i<exp.size(); i++ ){
- Assert( d_conc_to_id[0].find( exp[i] )!=d_conc_to_id[0].end() );
- Trace(c) << " relevant instance id : " << d_conc_to_id[0][ exp[i] ] << std::endl;
- d_relevant_inst[ d_conc_to_id[0][ exp[i] ] ] = true;
- }
-}
-
-void InstPropagator::debugPrintExplanation( std::vector< Node >& exp, const char * c ) {
- for( unsigned i=0; i<exp.size(); i++ ){
- Assert( d_conc_to_id[0].find( exp[i] )!=d_conc_to_id[0].end() );
- Trace(c) << d_conc_to_id[0][ exp[i] ] << " ";
- }
-}
-
+/********************* */ +/*! \file inst_propagator.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** Propagate mechanism for instantiations + **/ + +#include <vector> + +#include "theory/quantifiers/inst_propagator.h" +#include "theory/rewriter.h" +#include "theory/quantifiers/term_database.h" + +using namespace CVC4; +using namespace std; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; +using namespace CVC4::kind; + + +EqualityQueryInstProp::EqualityQueryInstProp( QuantifiersEngine* qe ) : d_qe( qe ){ + d_true = NodeManager::currentNM()->mkConst( true ); + d_false = NodeManager::currentNM()->mkConst( false ); +} + +bool EqualityQueryInstProp::reset( Theory::Effort e ) { + d_uf.clear(); + d_uf_exp.clear(); + d_diseq_list.clear(); + return true; +} + +/** contains term */ +bool EqualityQueryInstProp::hasTerm( Node a ) { + if( getEngine()->hasTerm( a ) ){ + return true; + }else{ + std::vector< Node > exp; + Node ar = getUfRepresentative( a, exp ); + return !ar.isNull() && getEngine()->hasTerm( ar ); + } +} + +/** get the representative of the equivalence class of a */ +Node EqualityQueryInstProp::getRepresentative( Node a ) { + if( getEngine()->hasTerm( a ) ){ + a = getEngine()->getRepresentative( a ); + } + std::vector< Node > exp; + Node ar = getUfRepresentative( a, exp ); + return ar.isNull() ? a : ar; +} + +/** returns true if a and b are equal in the current context */ +bool EqualityQueryInstProp::areEqual( Node a, Node b ) { + if( a==b ){ + return true; + }else{ + eq::EqualityEngine* ee = getEngine(); + if( ee->hasTerm( a ) && ee->hasTerm( b ) ){ + if( ee->areEqual( a, b ) ){ + return true; + } + } + return false; + } +} + +/** returns true is a and b are disequal in the current context */ +bool EqualityQueryInstProp::areDisequal( Node a, Node b ) { + if( a==b ){ + return false; + }else{ + eq::EqualityEngine* ee = getEngine(); + if( ee->hasTerm( a ) && ee->hasTerm( b ) ){ + if( ee->areDisequal( a, b, false ) ){ + return true; + } + } + return false; + } +} + +/** get the equality engine associated with this query */ +eq::EqualityEngine* EqualityQueryInstProp::getEngine() { + return d_qe->getMasterEqualityEngine(); +} + +/** get the equivalence class of a */ +void EqualityQueryInstProp::getEquivalenceClass( Node a, std::vector< Node >& eqc ) { + //TODO? +} + +TNode EqualityQueryInstProp::getCongruentTerm( Node f, std::vector< TNode >& args ) { + TNode t = d_qe->getTermDatabase()->getCongruentTerm( f, args ); + if( !t.isNull() ){ + return t; + }else{ + //TODO? + return TNode::null(); + } +} + +Node EqualityQueryInstProp::getRepresentativeExp( Node a, std::vector< Node >& exp ) { + bool engine_has_a = getEngine()->hasTerm( a ); + if( engine_has_a ){ + a = getEngine()->getRepresentative( a ); + } + //get union find representative, if this occurs in the equality engine, return it + unsigned prev_size = exp.size(); + Node ar = getUfRepresentative( a, exp ); + if( !ar.isNull() ){ + if( engine_has_a || getEngine()->hasTerm( ar ) ){ + Assert( getEngine()->hasTerm( ar ) ); + Assert( getEngine()->getRepresentative( ar )==ar ); + return ar; + } + }else{ + if( engine_has_a ){ + return a; + } + } + //retract explanation + while( exp.size()>prev_size ){ + exp.pop_back(); + } + return Node::null(); +} + +bool EqualityQueryInstProp::areEqualExp( Node a, Node b, std::vector< Node >& exp ) { + if( areEqual( a, b ) ){ + return true; + }else{ + std::vector< Node > exp_a; + Node ar = getUfRepresentative( a, exp_a ); + if( !ar.isNull() ){ + std::vector< Node > exp_b; + if( ar==getUfRepresentative( b, exp_b ) ){ + merge_exp( exp, exp_a ); + merge_exp( exp, exp_b ); + return true; + } + } + return false; + } +} + +bool EqualityQueryInstProp::areDisequalExp( Node a, Node b, std::vector< Node >& exp ) { + if( areDisequal( a, b ) ){ + return true; + }else{ + //TODO? + return false; + } +} + +Node EqualityQueryInstProp::getUfRepresentative( Node a, std::vector< Node >& exp ) { + Assert( exp.empty() ); + std::map< Node, Node >::iterator it = d_uf.find( a ); + if( it!=d_uf.end() ){ + if( it->second==a ){ + Assert( d_uf_exp[ a ].empty() ); + return it->second; + }else{ + Node m = getUfRepresentative( it->second, exp ); + Assert( !m.isNull() ); + if( m!=it->second ){ + //update union find + d_uf[ a ] = m; + //update explanation : merge the explanation of the parent + merge_exp( d_uf_exp[ a ], exp ); + Trace("qip-eq") << "EqualityQueryInstProp::getUfRepresentative : merge " << a << " -> " << m << ", exp size=" << d_uf_exp[ a ].size() << std::endl; + } + //add current explanation to exp: note that exp is a subset of d_uf_exp[ a ], reset + exp.clear(); + exp.insert( exp.end(), d_uf_exp[ a ].begin(), d_uf_exp[ a ].end() ); + return m; + } + }else{ + return Node::null(); + } +} + +// set a == b with reason, return status, modify a and b to representatives pre-merge +int EqualityQueryInstProp::setEqual( Node& a, Node& b, bool pol, std::vector< Node >& reason ) { + if( a==b ){ + return pol ? STATUS_NONE : STATUS_CONFLICT; + } + int status = pol ? STATUS_MERGED_UNKNOWN : STATUS_NONE; + Trace("qip-eq") << "EqualityQueryInstProp::setEqual " << a << ", " << b << ", pol = " << pol << ", reason size = " << reason.size() << std::endl; + //get the representative for a + std::vector< Node > exp_a; + Node ar = getUfRepresentative( a, exp_a ); + if( ar.isNull() ){ + Assert( exp_a.empty() ); + ar = a; + } + if( ar==b ){ + Trace("qip-eq") << "EqualityQueryInstProp::setEqual : already equal" << std::endl; + if( pol ){ + return STATUS_NONE; + }else{ + merge_exp( reason, exp_a ); + return STATUS_CONFLICT; + } + } + bool swap = false; + //get the representative for b + std::vector< Node > exp_b; + Node br = getUfRepresentative( b, exp_b ); + if( br.isNull() ){ + Assert( exp_b.empty() ); + br = b; + if( !getEngine()->hasTerm( br ) ){ + if( ar!=a || getEngine()->hasTerm( ar ) ){ + swap = true; + } + }else{ + if( getEngine()->hasTerm( ar ) ){ + status = STATUS_MERGED_KNOWN; + } + } + }else{ + if( ar==br ){ + Trace("qip-eq") << "EqualityQueryInstProp::setEqual : already equal" << std::endl; + if( pol ){ + return STATUS_NONE; + }else{ + merge_exp( reason, exp_a ); + merge_exp( reason, exp_b ); + return STATUS_CONFLICT; + } + }else if( getEngine()->hasTerm( ar ) ){ + if( getEngine()->hasTerm( br ) ){ + status = STATUS_MERGED_KNOWN; + }else{ + swap = true; + } + } + } + + if( swap ){ + //swap + Node temp_r = ar; + ar = br; + br = temp_r; + } + + Assert( !getEngine()->hasTerm( ar ) || getEngine()->hasTerm( br ) ); + Assert( ar!=br ); + + std::vector< Node > exp_d; + if( areDisequalExp( ar, br, exp_d ) ){ + if( pol ){ + merge_exp( reason, exp_b ); + merge_exp( reason, exp_b ); + merge_exp( reason, exp_d ); + return STATUS_CONFLICT; + }else{ + return STATUS_NONE; + } + }else{ + if( pol ){ + //update the union find + Assert( d_uf_exp[ar].empty() ); + Assert( d_uf_exp[br].empty() ); + + d_uf[ar] = br; + merge_exp( d_uf_exp[ar], exp_a ); + merge_exp( d_uf_exp[ar], exp_b ); + merge_exp( d_uf_exp[ar], reason ); + + d_uf[br] = br; + d_uf_exp[br].clear(); + + Trace("qip-eq") << "EqualityQueryInstProp::setEqual : merge " << ar << " -> " << br << ", exp size = " << d_uf_exp[ar].size() << ", status = " << status << std::endl; + a = ar; + b = br; + return status; + }else{ + //TODO? + return STATUS_NONE; + } + } +} + +void EqualityQueryInstProp::addArgument( std::vector< Node >& args, std::vector< Node >& props, Node n, bool is_prop, bool pol ) { + if( is_prop ){ + if( isLiteral( n ) ){ + props.push_back( pol ? n : n.negate() ); + return; + } + } + args.push_back( n ); +} + +bool EqualityQueryInstProp::isLiteral( Node n ) { + Kind ak = n.getKind()==NOT ? n[0].getKind() : n.getKind(); + Assert( ak!=NOT ); + return ak!=AND && ak!=OR && ak!=IFF && ak!=ITE; +} + +//this is identical to TermDb::evaluateTerm2, but tracks more information +Node EqualityQueryInstProp::evaluateTermExp( Node n, std::vector< Node >& exp, std::map< Node, Node >& visited, bool hasPol, bool pol, + std::map< Node, bool >& watch_list_out, std::vector< Node >& props ) { + std::map< Node, Node >::iterator itv = visited.find( n ); + if( itv != visited.end() ){ + return itv->second; + }else{ + visited[n] = n; + Trace("qip-eval") << "evaluate term : " << n << std::endl; + std::vector< Node > exp_n; + Node ret = getRepresentativeExp( n, exp_n ); + if( ret.isNull() ){ + //term is not known to be equal to a representative in equality engine, evaluate it + Kind k = n.getKind(); + if( k==FORALL ){ + ret = Node::null(); + }else{ + std::map< Node, bool > watch_list_out_curr; + TNode f = d_qe->getTermDatabase()->getMatchOperator( n ); + std::vector< Node > args; + bool ret_set = false; + bool childChanged = false; + int abort_i = -1; + //get the child entailed polarity + Assert( n.getKind()!=IMPLIES ); + bool newHasPol, newPol; + QuantPhaseReq::getEntailPolarity( n, 0, hasPol, pol, newHasPol, newPol ); + //for each child + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + Node c = evaluateTermExp( n[i], exp, visited, newHasPol, newPol, watch_list_out_curr, props ); + if( c.isNull() ){ + ret = Node::null(); + ret_set = true; + break; + }else if( c==d_true || c==d_false ){ + //short-circuiting + if( k==kind::AND || k==kind::OR ){ + if( (k==kind::AND)==(c==d_false) ){ + ret = c; + ret_set = true; + break; + }else{ + //redundant + c = Node::null(); + childChanged = true; + } + }else if( k==kind::ITE && i==0 ){ + Assert( watch_list_out_curr.empty() ); + ret = evaluateTermExp( n[ c==d_true ? 1 : 2], exp, visited, hasPol, pol, watch_list_out_curr, props ); + ret_set = true; + break; + }else if( k==kind::NOT ){ + ret = c==d_true ? d_false : d_true; + ret_set = true; + break; + } + } + if( !c.isNull() ){ + childChanged = childChanged || n[i]!=c; + if( !f.isNull() && !watch_list_out_curr.empty() ){ + // we are done if this is an UF application and an argument is unevaluated + args.push_back( c ); + abort_i = i; + break; + }else if( ( k==kind::AND || k==kind::OR ) ){ + if( c.getKind()==k ){ + //flatten + for( unsigned j=0; j<c.getNumChildren(); j++ ){ + addArgument( args, props, c[j], newHasPol, newPol ); + } + }else{ + addArgument( args, props, c, newHasPol, newPol ); + } + //if we are in a branching position + if( hasPol && !newHasPol && args.size()>=2 ){ + //we are done if at least two args are unevaluated + abort_i = i; + break; + } + }else if( k==kind::ITE ){ + //we are done if we are ITE and condition is unevaluated + Assert( i==0 ); + args.push_back( c ); + abort_i = i; + break; + }else{ + args.push_back( c ); + } + } + } + //add remaining children if we aborted + if( abort_i!=-1 ){ + for( int i=(abort_i+1); i<(int)n.getNumChildren(); i++ ){ + args.push_back( n[i] ); + } + } + //copy over the watch list + for( std::map< Node, bool >::iterator itc = watch_list_out_curr.begin(); itc != watch_list_out_curr.end(); ++itc ){ + watch_list_out[itc->first] = itc->second; + } + + //if we have not short-circuited evaluation + if( !ret_set ){ + //if it is an indexed term, return the congruent term + if( !f.isNull() && watch_list_out.empty() ){ + std::vector< TNode > t_args; + for( unsigned i=0; i<args.size(); i++ ) { + t_args.push_back( args[i] ); + } + Assert( args.size()==n.getNumChildren() ); + //args contains terms known by the equality engine + TNode nn = getCongruentTerm( f, t_args ); + Trace("qip-eval") << " got congruent term " << nn << " from DB for " << n << std::endl; + if( !nn.isNull() ){ + //successfully constructed representative in EE + Assert( exp_n.empty() ); + ret = getRepresentativeExp( nn, exp_n ); + Trace("qip-eval") << "return rep, exp size = " << exp_n.size() << std::endl; + merge_exp( exp, exp_n ); + ret_set = true; + Assert( !ret.isNull() ); + } + } + if( !ret_set ){ + if( childChanged ){ + Trace("qip-eval") << "return rewrite" << std::endl; + if( ( k==kind::AND || k==kind::OR ) ){ + if( args.empty() ){ + ret = k==kind::AND ? d_true : d_false; + ret_set = true; + }else if( args.size()==1 ){ + ret = args[0]; + ret_set = true; + } + }else{ + Assert( args.size()==n.getNumChildren() ); + } + if( !ret_set ){ + if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ + args.insert( args.begin(), n.getOperator() ); + } + ret = NodeManager::currentNM()->mkNode( k, args ); + ret = Rewriter::rewrite( ret ); + //re-evaluate + Node ret_eval = getRepresentativeExp( ret, exp_n ); + if( !ret_eval.isNull() ){ + ret = ret_eval; + watch_list_out.clear(); + }else{ + watch_list_out[ret] = true; + } + } + }else{ + ret = n; + watch_list_out[ret] = true; + } + } + } + } + }else{ + Trace("qip-eval") << "...exists in ee, return rep, exp size = " << exp_n.size() << std::endl; + merge_exp( exp, exp_n ); + } + Trace("qip-eval") << "evaluated term : " << n << ", got : " << ret << ", exp size = " << exp.size() << std::endl; + visited[n] = ret; + return ret; + } +} + +void EqualityQueryInstProp::merge_exp( std::vector< Node >& v, std::vector< Node >& v_to_merge, int up_to_size ) { + //TODO : optimize + if( v.empty() ){ + Assert( up_to_size==-1 || up_to_size==(int)v_to_merge.size() ); + v.insert( v.end(), v_to_merge.begin(), v_to_merge.end() ); + }else{ + //std::vector< Node >::iterator v_end = v.end(); + up_to_size = up_to_size==-1 ? (int)v_to_merge.size() : up_to_size; + for( int j=0; j<up_to_size; j++ ){ + if( std::find( v.begin(), v.end(), v_to_merge[j] )==v.end() ){ + v.push_back( v_to_merge[j] ); + } + } + } +} + + +void InstPropagator::InstInfo::init( Node q, Node lem, std::vector< Node >& terms, Node body ) { + d_active = true; + //information about the instance + d_q = q; + d_lem = lem; + Assert( d_terms.empty() ); + d_terms.insert( d_terms.end(), terms.begin(), terms.end() ); + //the current lemma + d_curr = body; + d_curr_exp.push_back( body ); +} + +InstPropagator::InstPropagator( QuantifiersEngine* qe ) : +d_qe( qe ), d_notify(*this), d_qy( qe ){ +} + +bool InstPropagator::reset( Theory::Effort e ) { + d_icount = 1; + d_ii.clear(); + for( unsigned i=0; i<2; i++ ){ + d_conc_to_id[i].clear(); + d_conc_to_id[i][d_qy.d_true] = 0; + } + d_conflict = false; + d_watch_list.clear(); + d_update_list.clear(); + d_relevant_inst.clear(); + return d_qy.reset( e ); +} + +bool InstPropagator::notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) { + if( !d_conflict ){ + if( Trace.isOn("qip-prop") ){ + Trace("qip-prop") << "InstPropagator:: Notify instantiation " << q << " : " << std::endl; + for( unsigned i=0; i<terms.size(); i++ ){ + Trace("qip-prop") << " " << terms[i] << std::endl; + } + } + unsigned id = d_icount; + d_icount++; + Trace("qip-prop") << "...assign id=" << id << std::endl; + d_ii[id].init( q, lem, terms, body ); + //initialize the information + if( cacheConclusion( id, body ) ){ + Assert( d_update_list.empty() ); + d_update_list.push_back( id ); + bool firstTime = true; + //update infos in the update list until empty + do { + unsigned uid = d_update_list.back(); + d_update_list.pop_back(); + if( d_ii[uid].d_active ){ + update( uid, d_ii[uid], firstTime ); + } + firstTime = false; + }while( !d_conflict && !d_update_list.empty() ); + }else{ + d_ii[id].d_active = false; + Trace("qip-prop") << "...duplicate." << std::endl; + } + Trace("qip-prop") << "...finished notify instantiation." << std::endl; + return !d_conflict; + }else{ + return true; + } +} + +bool InstPropagator::update( unsigned id, InstInfo& ii, bool firstTime ) { + Assert( !d_conflict ); + Assert( ii.d_active ); + Trace("qip-prop-debug") << "Update info [" << id << "]..." << std::endl; + //update the evaluation of the current lemma + std::map< Node, Node > visited; + std::map< Node, bool > watch_list; + std::vector< Node > props; + Node eval = d_qy.evaluateTermExp( ii.d_curr, ii.d_curr_exp, visited, true, true, watch_list, props ); + if( eval.isNull() ){ + ii.d_active = false; + }else if( firstTime || eval!=ii.d_curr ){ + if( EqualityQueryInstProp::isLiteral( eval ) ){ + props.push_back( eval ); + eval = d_qy.d_true; + watch_list.clear(); + } + if( Trace.isOn("qip-prop") ){ + Trace("qip-prop") << "Update info [" << id << "]..." << std::endl; + Trace("qip-prop") << "...updated lemma " << ii.d_curr << " -> " << eval << ", exp = "; + debugPrintExplanation( ii.d_curr_exp, "qip-prop" ); + Trace("qip-prop") << std::endl; + Trace("qip-prop") << "...watch list: " << std::endl; + for( std::map< Node, bool >::iterator itw = watch_list.begin(); itw!=watch_list.end(); ++itw ){ + Trace("qip-prop") << " " << itw->first << std::endl; + } + Trace("qip-prop") << "...new propagations: " << std::endl; + for( unsigned i=0; i<props.size(); i++ ){ + Trace("qip-prop") << " " << props[i] << std::endl; + } + Trace("qip-prop") << std::endl; + } + //determine the status of eval + if( eval==d_qy.d_false ){ + Assert( props.empty() ); + //we have inferred a conflict + conflict( ii.d_curr_exp ); + return false; + }else{ + for( unsigned i=0; i<props.size(); i++ ){ + Trace("qip-prop-debug2") << "Process propagation " << props[i] << std::endl; + //if we haven't propagated this literal yet + if( cacheConclusion( id, props[i], 1 ) ){ + Node lit = props[i].getKind()==NOT ? props[i][0] : props[i]; + bool pol = props[i].getKind()!=NOT; + if( lit.getKind()==EQUAL ){ + propagate( lit[0], lit[1], pol, ii.d_curr_exp ); + }else{ + propagate( lit, pol ? d_qy.d_true : d_qy.d_false, true, ii.d_curr_exp ); + } + if( d_conflict ){ + return false; + } + } + Trace("qip-prop-debug2") << "Done process propagation " << props[i] << std::endl; + } + //if we have not inferred this conclusion yet + if( cacheConclusion( id, eval ) ){ + ii.d_curr = eval; + //update the watch list + Trace("qip-prop-debug") << "...updating watch list for [" << id << "], curr is " << ii.d_curr << std::endl; + //Here, we need to be notified of enough terms such that if we are not notified, then update( ii ) will return no propagations. + // Similar to two-watched literals, but since we are in UF, we need to watch all terms on a complete path of two terms. + for( std::map< Node, bool >::iterator itw = watch_list.begin(); itw != watch_list.end(); ++itw ){ + d_watch_list[ itw->first ][ id ] = true; + } + }else{ + Trace("qip-prop-debug") << "...conclusion " << eval << " is duplicate." << std::endl; + ii.d_active = false; + } + } + }else{ + Trace("qip-prop-debug") << "...did not update." << std::endl; + } + Assert( !d_conflict ); + return true; +} + +void InstPropagator::propagate( Node a, Node b, bool pol, std::vector< Node >& exp ) { + if( Trace.isOn("qip-propagate") ){ + Trace("qip-propagate") << "* Propagate " << a << ( pol ? " == " : " != " ) << b << ", exp = "; + debugPrintExplanation( exp, "qip-propagate" ); + Trace("qip-propagate") << "..." << std::endl; + } + //set equal + int status = d_qy.setEqual( a, b, pol, exp ); + if( status==EqualityQueryInstProp::STATUS_NONE ){ + Trace("qip-prop-debug") << "...already equal/no conflict." << std::endl; + return; + }else if( status==EqualityQueryInstProp::STATUS_CONFLICT ){ + Trace("qip-prop-debug") << "...conflict." << std::endl; + conflict( exp ); + return; + } + if( pol ){ + if( status==EqualityQueryInstProp::STATUS_MERGED_KNOWN ){ + Assert( d_qy.getEngine()->hasTerm( a ) ); + Assert( d_qy.getEngine()->hasTerm( b ) ); + Trace("qip-prop-debug") << "...equality between known terms." << std::endl; + addRelevantInstances( exp, "qip-propagate" ); + } + Trace("qip-prop-debug") << "...merged representatives " << a << " and " << b << std::endl; + for( unsigned i=0; i<2; i++ ){ + //update terms from watched lists + Node c = i==0 ? a : b; + std::map< Node, std::map< unsigned, bool > >::iterator it = d_watch_list.find( c ); + if( it!=d_watch_list.end() ){ + Trace("qip-prop-debug") << "...update ids from watch list of " << c << ", size=" << it->second.size() << "..." << std::endl; + for( std::map< unsigned, bool >::iterator itw = it->second.begin(); itw != it->second.end(); ++itw ){ + unsigned idw = itw->first; + if( std::find( d_update_list.begin(), d_update_list.end(), idw )==d_update_list.end() ){ + Trace("qip-prop-debug") << "...will update " << idw << std::endl; + d_update_list.push_back( idw ); + } + } + d_watch_list.erase( c ); + } + } + } +} + +void InstPropagator::conflict( std::vector< Node >& exp ) { + Trace("qip-propagate") << "Conflict, exp size =" << exp.size() << std::endl; + d_conflict = true; + d_relevant_inst.clear(); + addRelevantInstances( exp, "qip-propagate" ); + + //now, inform quantifiers engine which instances should be retracted + for( std::map< unsigned, InstInfo >::iterator it = d_ii.begin(); it != d_ii.end(); ++it ){ + if( d_relevant_inst.find( it->first )==d_relevant_inst.end() ){ + if( !d_qe->removeInstantiation( it->second.d_q, it->second.d_lem, it->second.d_terms ) ){ + Trace("qip-warn") << "WARNING : did not remove instantiation id " << it->first << std::endl; + Assert( false ); + } + } + } + //will interupt the quantifiers engine + Trace("quant-engine-conflict") << "-----> InstPropagator::conflict with " << exp.size() << " instances." << std::endl; +} + +bool InstPropagator::cacheConclusion( unsigned id, Node body, int prop_index ) { + Assert( prop_index==0 || prop_index==1 ); + //check if the conclusion is non-redundant + if( d_conc_to_id[prop_index].find( body )==d_conc_to_id[prop_index].end() ){ + d_conc_to_id[prop_index][body] = id; + return true; + }else{ + return false; + } +} + +void InstPropagator::addRelevantInstances( std::vector< Node >& exp, const char * c ) { + for( unsigned i=0; i<exp.size(); i++ ){ + Assert( d_conc_to_id[0].find( exp[i] )!=d_conc_to_id[0].end() ); + Trace(c) << " relevant instance id : " << d_conc_to_id[0][ exp[i] ] << std::endl; + d_relevant_inst[ d_conc_to_id[0][ exp[i] ] ] = true; + } +} + +void InstPropagator::debugPrintExplanation( std::vector< Node >& exp, const char * c ) { + for( unsigned i=0; i<exp.size(); i++ ){ + Assert( d_conc_to_id[0].find( exp[i] )!=d_conc_to_id[0].end() ); + Trace(c) << d_conc_to_id[0][ exp[i] ] << " "; + } +} + diff --git a/src/theory/quantifiers/inst_propagator.h b/src/theory/quantifiers/inst_propagator.h index 0e21dc0d4..a6f76ef44 100644 --- a/src/theory/quantifiers/inst_propagator.h +++ b/src/theory/quantifiers/inst_propagator.h @@ -1,160 +1,163 @@ -/********************* */
-/*! \file inst_propagator.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Propagate mechanism for instantiations
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__QUANTIFIERS_INST_PROPAGATOR_H
-#define __CVC4__QUANTIFIERS_INST_PROPAGATOR_H
-
-#include <iostream>
-#include <string>
-#include <vector>
-#include <map>
-#include "expr/node.h"
-#include "expr/type_node.h"
-#include "theory/quantifiers_engine.h"
-#include "theory/quantifiers/term_database.h"
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-class EqualityQueryInstProp : public EqualityQuery {
-private:
- /** pointer to quantifiers engine */
- QuantifiersEngine* d_qe;
-public:
- EqualityQueryInstProp( QuantifiersEngine* qe );
- ~EqualityQueryInstProp(){};
- /** reset */
- bool reset( Theory::Effort e );
- /** identify */
- std::string identify() const { return "EqualityQueryInstProp"; }
- /** extends engine */
- bool extendsEngine() { return true; }
- /** contains term */
- bool hasTerm( Node a );
- /** get the representative of the equivalence class of a */
- Node getRepresentative( Node a );
- /** returns true if a and b are equal in the current context */
- bool areEqual( Node a, Node b );
- /** returns true is a and b are disequal in the current context */
- bool areDisequal( Node a, Node b );
- /** get the equality engine associated with this query */
- eq::EqualityEngine* getEngine();
- /** get the equivalence class of a */
- void getEquivalenceClass( Node a, std::vector< Node >& eqc );
- /** get congruent term */
- TNode getCongruentTerm( Node f, std::vector< TNode >& args );
-public:
- /** get the representative of the equivalence class of a, with explanation */
- Node getRepresentativeExp( Node a, std::vector< Node >& exp );
- /** returns true if a and b are equal in the current context */
- bool areEqualExp( Node a, Node b, std::vector< Node >& exp );
- /** returns true is a and b are disequal in the current context */
- bool areDisequalExp( Node a, Node b, std::vector< Node >& exp );
-private:
- /** term index */
- std::map< Node, TermArgTrie > d_func_map_trie;
- /** union find for terms beyond what is stored in equality engine */
- std::map< Node, Node > d_uf;
- std::map< Node, std::vector< Node > > d_uf_exp;
- Node getUfRepresentative( Node a, std::vector< Node >& exp );
- /** disequality list, stores explanations */
- std::map< Node, std::map< Node, Node > > d_diseq_list;
- /** add arg */
- void addArgument( std::vector< TNode >& args, std::vector< TNode >& props, Node n, bool is_prop, bool pol );
-public:
- enum {
- STATUS_MERGED_KNOWN,
- STATUS_MERGED_UNKNOWN,
- STATUS_NONE,
- };
- /** set equal */
- int setEqual( Node& a, Node& b, std::vector< Node >& reason );
- Node d_true;
- Node d_false;
-public:
- //for explanations
- static void merge_exp( std::vector< Node >& v, std::vector< Node >& v_to_merge, int up_to_size = -1 );
-
- Node evaluateTermExp( TNode n, std::vector< Node >& exp, std::map< TNode, Node >& visited, bool hasPol, bool pol,
- std::map< Node, bool >& watch_list_out, std::vector< TNode >& props );
- static bool isLiteral( Node n );
-};
-
-class InstPropagator : public QuantifiersUtil {
-private:
- /** pointer to quantifiers engine */
- QuantifiersEngine* d_qe;
- /** notify class */
- class InstantiationNotifyInstPropagator : public InstantiationNotify {
- InstPropagator& d_ip;
- public:
- InstantiationNotifyInstPropagator(InstPropagator& ip): d_ip(ip) {}
- virtual void notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) { d_ip.notifyInstantiation( quant_e, q, lem, terms, body ); }
- };
- InstantiationNotifyInstPropagator d_notify;
- /** notify instantiation method */
- void notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body );
- /** equality query */
- EqualityQueryInstProp d_qy;
- class InstInfo {
- public:
- bool d_active;
- Node d_q;
- Node d_lem;
- std::vector< Node > d_terms;
- // the current entailed body
- Node d_curr;
- //explanation for current entailed body
- std::vector< Node > d_curr_exp;
- void init( Node q, Node lem, std::vector< Node >& terms, Node body );
- };
- /** instantiation count/info */
- unsigned d_icount;
- std::map< unsigned, InstInfo > d_ii;
- std::map< TNode, unsigned > d_conc_to_id[2];
- /** are we in conflict */
- bool d_conflict;
- /** watch list */
- std::map< Node, std::map< unsigned, bool > > d_watch_list;
- /** update list */
- std::vector< unsigned > d_update_list;
- /** relevant instances */
- std::map< unsigned, bool > d_relevant_inst;
-private:
- bool update( unsigned id, InstInfo& i, bool firstTime = false );
- void propagate( Node a, Node b, bool pol, std::vector< Node >& exp );
- void conflict( std::vector< Node >& exp );
- bool cacheConclusion( unsigned id, Node body, int prop_index = 0 );
- void addRelevantInstances( std::vector< Node >& exp, const char * c );
-
- void debugPrintExplanation( std::vector< Node >& exp, const char * c );
-public:
- InstPropagator( QuantifiersEngine* qe );
- ~InstPropagator(){}
- /** reset */
- bool reset( Theory::Effort e );
- /** identify */
- std::string identify() const { return "InstPropagator"; }
- /** get the notify mechanism */
- InstantiationNotify* getInstantiationNotify() { return &d_notify; }
-};
-
-}
-}
-}
-
-#endif
+/********************* */ +/*! \file inst_propagator.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Propagate mechanism for instantiations + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__QUANTIFIERS_INST_PROPAGATOR_H +#define __CVC4__QUANTIFIERS_INST_PROPAGATOR_H + +#include <iostream> +#include <string> +#include <vector> +#include <map> +#include "expr/node.h" +#include "expr/type_node.h" +#include "theory/quantifiers_engine.h" +#include "theory/quantifiers/term_database.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +class EqualityQueryInstProp : public EqualityQuery { +private: + /** pointer to quantifiers engine */ + QuantifiersEngine* d_qe; +public: + EqualityQueryInstProp( QuantifiersEngine* qe ); + ~EqualityQueryInstProp(){}; + /** reset */ + bool reset( Theory::Effort e ); + /** identify */ + std::string identify() const { return "EqualityQueryInstProp"; } + /** extends engine */ + bool extendsEngine() { return true; } + /** contains term */ + bool hasTerm( Node a ); + /** get the representative of the equivalence class of a */ + Node getRepresentative( Node a ); + /** returns true if a and b are equal in the current context */ + bool areEqual( Node a, Node b ); + /** returns true is a and b are disequal in the current context */ + bool areDisequal( Node a, Node b ); + /** get the equality engine associated with this query */ + eq::EqualityEngine* getEngine(); + /** get the equivalence class of a */ + void getEquivalenceClass( Node a, std::vector< Node >& eqc ); + /** get congruent term */ + TNode getCongruentTerm( Node f, std::vector< TNode >& args ); +public: + /** get the representative of the equivalence class of a, with explanation */ + Node getRepresentativeExp( Node a, std::vector< Node >& exp ); + /** returns true if a and b are equal in the current context */ + bool areEqualExp( Node a, Node b, std::vector< Node >& exp ); + /** returns true is a and b are disequal in the current context */ + bool areDisequalExp( Node a, Node b, std::vector< Node >& exp ); +private: + /** term index */ + std::map< Node, TermArgTrie > d_func_map_trie; + /** union find for terms beyond what is stored in equality engine */ + std::map< Node, Node > d_uf; + std::map< Node, std::vector< Node > > d_uf_exp; + Node getUfRepresentative( Node a, std::vector< Node >& exp ); + /** disequality list, stores explanations */ + std::map< Node, std::map< Node, Node > > d_diseq_list; + /** add arg */ + void addArgument( std::vector< Node >& args, std::vector< Node >& props, Node n, bool is_prop, bool pol ); +public: + enum { + STATUS_CONFLICT, + STATUS_MERGED_KNOWN, + STATUS_MERGED_UNKNOWN, + STATUS_NONE, + }; + /** set equal */ + int setEqual( Node& a, Node& b, bool pol, std::vector< Node >& reason ); + Node d_true; + Node d_false; +public: + //for explanations + static void merge_exp( std::vector< Node >& v, std::vector< Node >& v_to_merge, int up_to_size = -1 ); + + Node evaluateTermExp( Node n, std::vector< Node >& exp, std::map< Node, Node >& visited, bool hasPol, bool pol, + std::map< Node, bool >& watch_list_out, std::vector< Node >& props ); + static bool isLiteral( Node n ); +}; + +class InstPropagator : public QuantifiersUtil { +private: + /** pointer to quantifiers engine */ + QuantifiersEngine* d_qe; + /** notify class */ + class InstantiationNotifyInstPropagator : public InstantiationNotify { + InstPropagator& d_ip; + public: + InstantiationNotifyInstPropagator(InstPropagator& ip): d_ip(ip) {} + virtual bool notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) { + return d_ip.notifyInstantiation( quant_e, q, lem, terms, body ); + } + }; + InstantiationNotifyInstPropagator d_notify; + /** notify instantiation method */ + bool notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ); + /** equality query */ + EqualityQueryInstProp d_qy; + class InstInfo { + public: + bool d_active; + Node d_q; + Node d_lem; + std::vector< Node > d_terms; + // the current entailed body + Node d_curr; + //explanation for current entailed body + std::vector< Node > d_curr_exp; + void init( Node q, Node lem, std::vector< Node >& terms, Node body ); + }; + /** instantiation count/info */ + unsigned d_icount; + std::map< unsigned, InstInfo > d_ii; + std::map< Node, unsigned > d_conc_to_id[2]; + /** are we in conflict */ + bool d_conflict; + /** watch list */ + std::map< Node, std::map< unsigned, bool > > d_watch_list; + /** update list */ + std::vector< unsigned > d_update_list; + /** relevant instances */ + std::map< unsigned, bool > d_relevant_inst; +private: + bool update( unsigned id, InstInfo& i, bool firstTime = false ); + void propagate( Node a, Node b, bool pol, std::vector< Node >& exp ); + void conflict( std::vector< Node >& exp ); + bool cacheConclusion( unsigned id, Node body, int prop_index = 0 ); + void addRelevantInstances( std::vector< Node >& exp, const char * c ); + + void debugPrintExplanation( std::vector< Node >& exp, const char * c ); +public: + InstPropagator( QuantifiersEngine* qe ); + ~InstPropagator(){} + /** reset */ + bool reset( Theory::Effort e ); + /** identify */ + std::string identify() const { return "InstPropagator"; } + /** get the notify mechanism */ + InstantiationNotify* getInstantiationNotify() { return &d_notify; } +}; + +} +} +} + +#endif diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index e38304c68..cc9b56a7c 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -107,6 +107,7 @@ void InstStrategyCbqi::reset_round( Theory::Effort effort ) { void InstStrategyCbqi::check( Theory::Effort e, unsigned quant_e ) { if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){ + Assert( !d_quantEngine->inConflict() ); double clSet = 0; if( Trace.isOn("cbqi-engine") ){ clSet = double(clock())/double(CLOCKS_PER_SEC); @@ -118,9 +119,12 @@ void InstStrategyCbqi::check( Theory::Effort e, unsigned quant_e ) { Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){ process( q, e, ee ); + if( d_quantEngine->inConflict() ){ + break; + } } } - if( d_quantEngine->getNumLemmasWaiting()>lastWaiting ){ + if( d_quantEngine->inConflict() || d_quantEngine->getNumLemmasWaiting()>lastWaiting ){ break; } } @@ -567,8 +571,8 @@ Node InstStrategySimplex::getTableauxValue( ArithVar v, bool minus_delta ){ //new implementation -bool CegqiOutputInstStrategy::addInstantiation( std::vector< Node >& subs ) { - return d_out->addInstantiation( subs ); +bool CegqiOutputInstStrategy::doAddInstantiation( std::vector< Node >& subs ) { + return d_out->doAddInstantiation( subs ); } bool CegqiOutputInstStrategy::isEligibleForInstantiation( Node n ) { @@ -636,13 +640,13 @@ void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) { } } -bool InstStrategyCegqi::addInstantiation( std::vector< Node >& subs ) { +bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) { Assert( !d_curr_quant.isNull() ); //if doing partial quantifier elimination, record the instantiation and set the incomplete flag instead of sending instantiation lemma if( d_quantEngine->getTermDatabase()->isQAttrQuantElimPartial( d_curr_quant ) ){ d_cbqi_set_quant_inactive = true; d_incomplete_check = true; - d_quantEngine->recordInstantiationInternal( d_curr_quant, subs, false, false ); + d_quantEngine->recordInstantiationInternal( d_curr_quant, subs, false, false, true ); return true; }else{ //check if we need virtual term substitution (if used delta or infinity) diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index d53d9d81c..8ed59778b 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -122,7 +122,7 @@ class CegqiOutputInstStrategy : public CegqiOutput { public: CegqiOutputInstStrategy( InstStrategyCegqi * out ) : d_out( out ){} InstStrategyCegqi * d_out; - bool addInstantiation( std::vector< Node >& subs ); + bool doAddInstantiation( std::vector< Node >& subs ); bool isEligibleForInstantiation( Node n ); bool addLemma( Node lem ); }; @@ -143,7 +143,7 @@ public: InstStrategyCegqi( QuantifiersEngine * qe ); ~InstStrategyCegqi() throw(); - bool addInstantiation( std::vector< Node >& subs ); + bool doAddInstantiation( std::vector< Node >& subs ); bool isEligibleForInstantiation( Node n ); bool addLemma( Node lem ); /** identify */ diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 8c3154c1c..6d6991476 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -106,7 +106,9 @@ int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){ if( d_user_gen[f][i]->isMultiTrigger() ){ d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst; } - //d_quantEngine->d_hasInstantiated[f] = true; + if( d_quantEngine->inConflict() ){ + break; + } } } } @@ -229,11 +231,13 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ) if( r==1 ){ d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst; } - //d_quantEngine->d_hasInstantiated[f] = true; + if( d_quantEngine->inConflict() ){ + break; + } } } } - if( hasInst && options::multiTriggerPriority() ){ + if( d_quantEngine->inConflict() || ( hasInst && options::multiTriggerPriority() ) ){ break; } } @@ -575,6 +579,9 @@ void FullSaturation::check( Theory::Effort e, unsigned quant_e ) { if( process( q, fullEffort ) ){ //added lemma addedLemmas++; + if( d_quantEngine->inConflict() ){ + break; + } } } } diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 8e88d3434..b59734720 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -60,7 +60,7 @@ void InstantiationEngine::presolve() { } } -bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ +void InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting(); //iterate over an internal effort level e int e = 0; @@ -83,8 +83,10 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ InstStrategy* is = d_instStrategies[j]; Trace("inst-engine-debug") << "Do " << is->identify() << " " << e_use << std::endl; int quantStatus = is->process( q, effort, e_use ); - Trace("inst-engine-debug") << " -> status is " << quantStatus << std::endl; - if( quantStatus==InstStrategy::STATUS_UNFINISHED ){ + Trace("inst-engine-debug") << " -> status is " << quantStatus << ", conflict=" << d_quantEngine->inConflict() << std::endl; + if( d_quantEngine->inConflict() ){ + return; + }else if( quantStatus==InstStrategy::STATUS_UNFINISHED ){ finished = false; } } @@ -96,13 +98,6 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ } e++; } - //Notice() << "All instantiators finished, # added lemmas = " << (int)d_lemmas_waiting.size() << std::endl; - if( !d_quantEngine->hasAddedLemma() ){ - return false; - }else{ - Trace("inst-engine") << "Added lemmas = " << (int)(d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl; - return true; - } } bool InstantiationEngine::needsCheck( Theory::Effort e ){ @@ -138,8 +133,18 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){ Trace("inst-engine-debug") << "InstEngine: check: # asserted quantifiers " << d_quants.size() << "/"; Trace("inst-engine-debug") << d_quantEngine->getModel()->getNumAssertedQuantifiers() << " " << quantActive << std::endl; if( quantActive ){ - bool addedLemmas = doInstantiationRound( e ); - Trace("inst-engine-debug") << "Add lemmas = " << addedLemmas << std::endl; + unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting(); + doInstantiationRound( e ); + if( d_quantEngine->inConflict() ){ + Assert( d_quantEngine->getNumLemmasWaiting()>lastWaiting ); + Trace("inst-engine") << "Conflict, size = " << d_quantEngine->getNumLemmasWaiting(); + if( lastWaiting>0 ){ + Trace("inst-engine") << " (prev " << lastWaiting << ")"; + } + Trace("inst-engine") << std::endl; + }else if( d_quantEngine->hasAddedLemma() ){ + Trace("inst-engine") << "Added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl; + } }else{ d_quants.clear(); } diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h index 4d1d4a20f..d2b3740a1 100644 --- a/src/theory/quantifiers/instantiation_engine.h +++ b/src/theory/quantifiers/instantiation_engine.h @@ -70,7 +70,7 @@ private: /** is the engine incomplete for this quantifier */ bool isIncomplete( Node q ); /** do instantiation round */ - bool doInstantiationRound( Theory::Effort effort ); + void doInstantiationRound( Theory::Effort effort ); public: InstantiationEngine( QuantifiersEngine* qe ); ~InstantiationEngine(); diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index bcd36f37a..bdb416b6b 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -155,11 +155,15 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) { int lems = initializeQuantifier( f, f ); d_statistics.d_init_inst_gen_lemmas += lems; d_addedLemmas += lems; + if( d_qe->inConflict() ){ + break; + } } } if( d_addedLemmas>0 ){ Trace("model-engine") << "Initialize, Added Lemmas = " << d_addedLemmas << std::endl; }else{ + Assert( !d_qe->inConflict() ); //initialize model fm->initialize(); //analyze the functions @@ -202,7 +206,7 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) { }else{ d_numQuantNoSelForm++; } - if( options::fmfInstGenOneQuantPerRound() && lems>0 ){ + if( d_qe->inConflict() || ( options::fmfInstGenOneQuantPerRound() && lems>0 ) ){ break; } }else if( d_quant_sat.find( f )!=d_quant_sat.end() ){ @@ -428,6 +432,9 @@ bool QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i //add as instantiation if( d_qe->addInstantiation( f, m ) ){ d_addedLemmas++; + if( d_qe->inConflict() ){ + break; + } //if the instantiation is show to be false, and we wish to skip multiple instantiations at once if( eval==-1 ){ riter.increment2( depIndex ); diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 51dccae49..a7e272be0 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -62,6 +62,7 @@ void ModelEngine::reset_round( Theory::Effort e ) { void ModelEngine::check( Theory::Effort e, unsigned quant_e ){ if( quant_e==QuantifiersEngine::QEFFORT_MODEL ){ + Assert( !d_quantEngine->inConflict() ); int addedLemmas = 0; FirstOrderModel* fm = d_quantEngine->getModel(); @@ -100,8 +101,6 @@ void ModelEngine::check( Theory::Effort e, unsigned quant_e ){ //CVC4 will answer SAT or unknown Trace("fmf-consistent") << std::endl; debugPrint("fmf-consistent"); - }else{ - //otherwise, the search will continue } } } @@ -194,33 +193,40 @@ int ModelEngine::checkModel(){ // FMC uses two sub-effort levels int e_max = options::mbqiMode()==MBQI_FMC || options::mbqiMode()==MBQI_FMC_INTERVAL ? 2 : ( options::mbqiMode()==MBQI_TRUST ? 0 : 1 ); for( int e=0; e<e_max; e++) { - if (d_addedLemmas==0) { - for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ - Node f = fm->getAssertedQuantifier( i ); - Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << f << ", effort = " << e << "..." << std::endl; - //determine if we should check this quantifier - if( considerQuantifiedFormula( f ) ){ - exhaustiveInstantiate( f, e ); - if( Trace.isOn("model-engine-warn") ){ - if( d_addedLemmas>10000 ){ - Debug("fmf-exit") << std::endl; - debugPrint("fmf-exit"); - exit( 0 ); - } - } - if( optOneQuantPerRound() && d_addedLemmas>0 ){ - break; + for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ + Node f = fm->getAssertedQuantifier( i ); + Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << f << ", effort = " << e << "..." << std::endl; + //determine if we should check this quantifier + if( considerQuantifiedFormula( f ) ){ + exhaustiveInstantiate( f, e ); + if( Trace.isOn("model-engine-warn") ){ + if( d_addedLemmas>10000 ){ + Debug("fmf-exit") << std::endl; + debugPrint("fmf-exit"); + exit( 0 ); } - }else{ - Trace("fmf-exh-inst") << "-> Inactive : " << f << std::endl; } + if( d_quantEngine->inConflict() || ( optOneQuantPerRound() && d_addedLemmas>0 ) ){ + break; + } + }else{ + Trace("fmf-exh-inst") << "-> Inactive : " << f << std::endl; } } + if( d_addedLemmas>0 ){ + break; + }else{ + Assert( !d_quantEngine->inConflict() ); + } } //print debug information - Trace("model-engine") << "Added Lemmas = " << d_addedLemmas << " / " << d_triedLemmas << " / "; - Trace("model-engine") << d_totalLemmas << std::endl; + if( d_quantEngine->inConflict() ){ + Trace("model-engine") << "Conflict, size = " << d_quantEngine->getNumLemmasWaiting() << std::endl; + }else{ + Trace("model-engine") << "Added Lemmas = " << d_addedLemmas << " / " << d_triedLemmas << " / "; + Trace("model-engine") << d_totalLemmas << std::endl; + } return d_addedLemmas; } @@ -266,11 +272,13 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ d_incomplete_check = d_incomplete_check || mb->d_incomplete_check; d_statistics.d_mbqi_inst_lemmas += mb->d_addedLemmas; }else{ - Trace("fmf-exh-inst-debug") << " Instantiation Constants: "; - for( size_t i=0; i<f[0].getNumChildren(); i++ ){ - Trace("fmf-exh-inst-debug") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " "; + if( Trace.isOn("fmf-exh-inst-debug") ){ + Trace("fmf-exh-inst-debug") << " Instantiation Constants: "; + for( size_t i=0; i<f[0].getNumChildren(); i++ ){ + Trace("fmf-exh-inst-debug") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " "; + } + Trace("fmf-exh-inst-debug") << std::endl; } - Trace("fmf-exh-inst-debug") << std::endl; //create a rep set iterator and iterate over the (relevant) domain of the quantifier RepSetIterator riter( d_quantEngine, &(d_quantEngine->getModel()->d_rep_set) ); if( riter.setQuantifier( f ) ){ @@ -289,6 +297,9 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ //add as instantiation if( d_quantEngine->addInstantiation( f, m ) ){ addedLemmas++; + if( d_quantEngine->inConflict() ){ + break; + } }else{ Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl; } diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index c5ccd9d82..5bf8d8a8d 100644 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -68,7 +68,7 @@ bool RewriteEngine::needsCheck( Theory::Effort e ){ void RewriteEngine::check( Theory::Effort e, unsigned quant_e ) { if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){ - //if( e==Theory::EFFORT_FULL ){ + Assert( !d_quantEngine->inConflict() ); Trace("rewrite-engine") << "---Rewrite Engine Round, effort = " << e << "---" << std::endl; //if( e==Theory::EFFORT_LAST_CALL ){ // if( !d_quantEngine->getModel()->isModelSet() ){ @@ -95,7 +95,7 @@ void RewriteEngine::check( Theory::Effort e, unsigned quant_e ) { //per priority level int index = 0; bool success = true; - while( success && index<(int)d_priority_order.size() ) { + while( !d_quantEngine->inConflict() && success && index<(int)d_priority_order.size() ) { addedLemmas += checkRewriteRule( d_priority_order[index], e ); index++; if( index<(int)d_priority_order.size() ){ @@ -104,11 +104,6 @@ void RewriteEngine::check( Theory::Effort e, unsigned quant_e ) { } Trace("rewrite-engine") << "Finished rewrite engine, added " << addedLemmas << " lemmas." << std::endl; - if (addedLemmas==0) { - - }else{ - //otherwise, the search will continue - } } } @@ -129,7 +124,7 @@ int RewriteEngine::checkRewriteRule( Node f, Theory::Effort e ) { Trace("rewrite-engine-inst-debug") << " Reset round..." << std::endl; qi->reset_round( qcf ); Trace("rewrite-engine-inst-debug") << " Get matches..." << std::endl; - while( qi->getNextMatch( qcf ) && + while( !d_quantEngine->inConflict() && qi->getNextMatch( qcf ) && ( addedLemmas==0 || !options::rrOneInstPerRound() ) ){ Trace("rewrite-engine-inst-debug") << " Got match to complete..." << std::endl; qi->debugPrintMatch( "rewrite-engine-inst-debug" ); @@ -138,7 +133,7 @@ int RewriteEngine::checkRewriteRule( Node f, Theory::Effort e ) { bool doContinue = false; bool success = true; int tempAddedLemmas = 0; - while( tempAddedLemmas==0 && success && ( addedLemmas==0 || !options::rrOneInstPerRound() ) ){ + while( !d_quantEngine->inConflict() && tempAddedLemmas==0 && success && ( addedLemmas==0 || !options::rrOneInstPerRound() ) ){ success = qi->completeMatch( qcf, assigned, doContinue ); doContinue = true; if( success ){ |