From 5e4ed407978b892e04de00994be535f58fb33257 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Sun, 10 Apr 2016 15:20:33 -0500 Subject: [PATCH] More work on instantiation propagation. Enable external filtering of instantiations. All quantifiers strategies terminate when a conflict can be established. --- src/theory/quantifiers/ambqi_builder.cpp | 2 +- .../quantifiers/ce_guided_single_inv.cpp | 18 +- src/theory/quantifiers/ce_guided_single_inv.h | 4 +- src/theory/quantifiers/ceg_instantiator.cpp | 56 +- src/theory/quantifiers/ceg_instantiator.h | 10 +- src/theory/quantifiers/full_model_check.cpp | 5 +- src/theory/quantifiers/inst_match.cpp | 65 +- src/theory/quantifiers/inst_match.h | 16 +- .../quantifiers/inst_match_generator.cpp | 20 +- src/theory/quantifiers/inst_propagator.cpp | 1402 +++++++++-------- src/theory/quantifiers/inst_propagator.h | 323 ++-- src/theory/quantifiers/inst_strategy_cbqi.cpp | 14 +- src/theory/quantifiers/inst_strategy_cbqi.h | 4 +- .../quantifiers/inst_strategy_e_matching.cpp | 13 +- .../quantifiers/instantiation_engine.cpp | 29 +- src/theory/quantifiers/instantiation_engine.h | 2 +- src/theory/quantifiers/model_builder.cpp | 9 +- src/theory/quantifiers/model_engine.cpp | 63 +- src/theory/quantifiers/rewrite_engine.cpp | 13 +- src/theory/quantifiers_engine.cpp | 99 +- src/theory/quantifiers_engine.h | 23 +- test/regress/regress0/fmf/Makefile.am | 1 - 22 files changed, 1180 insertions(+), 1011 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; jmkNode( 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& 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 - -#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=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& 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 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::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, const char * c ) { - for( unsigned i=0; i + +#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=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; imkNode( 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& 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 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::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, const char * c ) { + for( unsigned i=0; i -#include -#include -#include -#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 +#include +#include +#include +#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; egetNumAssertedQuantifiers(); 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; igetNumAssertedQuantifiers(); 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; igetTermDatabase()->getInstantiationConstant( f, i ) << " "; + if( Trace.isOn("fmf-exh-inst-debug") ){ + Trace("fmf-exh-inst-debug") << " Instantiation Constants: "; + for( size_t i=0; igetTermDatabase()->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 ){ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 839077a40..f98a3fd75 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -57,6 +57,8 @@ using namespace CVC4::theory::inst; QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te): d_te( te ), + //d_quants(u), + //d_quants_red(u), d_lemmas_produced_c(u), d_skolemized(u), d_ierCounter_c(c), @@ -71,10 +73,10 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* //utilities d_eq_query = new EqualityQueryQuantifiersEngine( c, this ); d_util.push_back( d_eq_query ); - + d_term_db = new quantifiers::TermDb( c, u, this ); d_util.push_back( d_term_db ); - + if( options::instPropagate() ){ d_inst_prop = new quantifiers::InstPropagator( this ); d_util.push_back( d_inst_prop ); @@ -84,6 +86,8 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* } d_tr_trie = new inst::TriggerTrie; + d_curr_effort_level = QEFFORT_NONE; + d_conflict = false; d_hasAddedLemma = false; //don't add true lemma d_lemmas_produced_c[d_term_db->d_true] = true; @@ -125,7 +129,6 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* d_rel_dom = NULL; d_builder = NULL; - d_curr_effort_level = QEFFORT_NONE; d_total_inst_count_debug = 0; //allow theory combination to go first, once initially d_ierCounter = options::instWhenTcFirst() ? 0 : 1; @@ -243,7 +246,7 @@ void QuantifiersEngine::finishInit(){ d_lte_part_inst = new quantifiers::LtePartialInst( this, c ); d_modules.push_back( d_lte_part_inst ); } - if( ( options::finiteModelFind() && options::quantDynamicSplit()!=quantifiers::QUANT_DSPLIT_MODE_NONE ) || + if( ( options::finiteModelFind() && options::quantDynamicSplit()!=quantifiers::QUANT_DSPLIT_MODE_NONE ) || options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_AGG ){ d_qsplit = new quantifiers::QuantDSplit( this, c ); d_modules.push_back( d_qsplit ); @@ -361,6 +364,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ } } + d_conflict = false; d_hasAddedLemma = false; bool setIncomplete = false; if( e==Theory::EFFORT_LAST_CALL ){ @@ -379,7 +383,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ if( d_hasAddedLemma ){ return; } - + if( Trace.isOn("quant-engine-debug") ){ Trace("quant-engine-debug") << "Quantifiers Engine check, level = " << e << std::endl; Trace("quant-engine-debug") << " depth : " << d_ierCounter_c << std::endl; @@ -404,7 +408,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ Trace("quant-engine-assert") << "Assertions : " << std::endl; getTheoryEngine()->printAssertions("quant-engine-assert"); } - + //reset utilities for( unsigned i=0; iidentify().c_str() << "..." << std::endl; @@ -426,7 +430,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ //reset the model d_model->reset_round(); - + //reset the modules for( unsigned i=0; iidentify().c_str() << std::endl; @@ -437,6 +441,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ flushLemmas(); if( d_hasAddedLemma ){ return; + } if( e==Theory::EFFORT_LAST_CALL ){ @@ -468,6 +473,10 @@ void QuantifiersEngine::check( Theory::Effort e ){ for( unsigned i=0; iidentify().c_str() << " at effort " << quant_e << "..." << std::endl; qm[i]->check( e, quant_e ); + if( d_conflict ){ + Trace("quant-engine-debug") << "...conflict!" << std::endl; + break; + } } } //flush all current lemmas @@ -476,6 +485,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ if( d_hasAddedLemma ){ break; }else{ + Assert( !d_conflict ); if( quant_e==QEFFORT_CONFLICT ){ if( e==Theory::EFFORT_FULL ){ //increment if a last call happened, we are not strictly enforcing interleaving, or already were in phase @@ -573,7 +583,7 @@ bool QuantifiersEngine::reduceQuantifier( Node q ) { d_quants_red[q] = false; return false; }else{ - return it->second; + return (*it).second; } } @@ -619,7 +629,7 @@ bool QuantifiersEngine::registerQuantifier( Node f ){ return true; } }else{ - return it->second; + return (*it).second; } } @@ -745,7 +755,11 @@ void QuantifiersEngine::computeTermVector( Node f, InstMatch& m, std::vector< No } -bool QuantifiersEngine::recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq, bool modInst ) { +bool QuantifiersEngine::recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq, bool modInst, bool addedLem ) { + if( !addedLem ){ + //record the instantiation for deletion later + //TODO + } if( options::incrementalSolving() ){ Trace("inst-add-debug") << "Adding into context-dependent inst trie, modEq = " << modEq << ", modInst = " << modInst << std::endl; inst::CDInstMatchTrie* imt; @@ -763,6 +777,19 @@ bool QuantifiersEngine::recordInstantiationInternal( Node q, std::vector< Node > } } +bool QuantifiersEngine::removeInstantiationInternal( Node q, std::vector< Node >& terms ) { + if( options::incrementalSolving() ){ + std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.find( q ); + if( it!=d_c_inst_match_trie.end() ){ + return it->second->removeInstMatch( this, q, terms ); + }else{ + return false; + } + }else{ + return d_inst_match_trie[q].removeInstMatch( this, q, terms ); + } +} + void QuantifiersEngine::setInstantiationLevelAttr( Node n, Node qn, uint64_t level ){ Trace("inst-level-debug2") << "IL : " << n << " " << qn << " " << level << std::endl; //if not from the vector of terms we instantiatied @@ -903,7 +930,8 @@ bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){ lem = Rewriter::rewrite(lem); } Trace("inst-add-debug") << "Adding lemma : " << lem << std::endl; - if( d_lemmas_produced_c.find( lem )==d_lemmas_produced_c.end() ){ + BoolMap::const_iterator itp = d_lemmas_produced_c.find( lem ); + if( itp==d_lemmas_produced_c.end() || !(*itp).second ){ //d_curr_out->lemma( lem, false, true ); d_lemmas_produced_c[ lem ] = true; d_lemmas_waiting.push_back( lem ); @@ -920,6 +948,17 @@ bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){ } } +bool QuantifiersEngine::removeLemma( Node lem ) { + std::vector< Node >::iterator it = std::find( d_lemmas_waiting.begin(), d_lemmas_waiting.end(), lem ); + if( it!=d_lemmas_waiting.end() ){ + d_lemmas_waiting.erase( it, it + 1 ); + d_lemmas_produced_c[ lem ] = false; + return true; + }else{ + return false; + } +} + void QuantifiersEngine::addRequirePhase( Node lit, bool req ){ d_phase_req_waiting[lit] = req; } @@ -933,7 +972,7 @@ bool QuantifiersEngine::addInstantiation( Node q, InstMatch& m, bool mkRep, bool bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bool mkRep, bool modEq, bool modInst, bool doVts ) { // For resource-limiting (also does a time check). getOutputChannel().safePoint(options::quantifierStep()); - + Assert( !d_conflict ); Assert( terms.size()==q[0].getNumChildren() ); Trace("inst-add-debug") << "For quantified formula " << q << ", add instantiation: " << std::endl; for( unsigned i=0; i& terms, bo } Trace("inst-add-debug") << " -> " << terms[i] << std::endl; if( terms[i].isNull() ){ - Trace("inst-add-debug") << " -> Failed to make term vector, due to term/type restrictions." << std::endl; + Trace("inst-add-debug") << " --> Failed to make term vector, due to term/type restrictions." << std::endl; return false; } #ifdef CVC4_ASSERTIONS @@ -967,7 +1006,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo bad_inst = true; }else{ bad_inst = quantifiers::TermDb::containsTerms( terms[i], d_term_db->d_inst_constants[q] ); - } + } } } //this assertion is critical to soundness @@ -977,7 +1016,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo Trace("inst") << " " << terms[j] << std::endl; } Assert( false ); - } + } #endif } @@ -989,7 +1028,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo } } } - + //check for positive entailment if( options::instNoEntail() ){ //TODO: check consistency of equality engine (if not aborting on utility's reset) @@ -998,7 +1037,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo subs[q[0][i]] = terms[i]; } if( d_term_db->isEntailed( q[1], subs, false, true ) ){ - Trace("inst-add-debug") << " -> Currently entailed." << std::endl; + Trace("inst-add-debug") << " --> Currently entailed." << std::endl; return false; } //Node eval = d_term_db->evaluateTerm( q[1], subs, false, true ); @@ -1009,7 +1048,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo //check for term vector duplication bool alreadyExists = !recordInstantiationInternal( q, terms, modEq, modInst ); if( alreadyExists ){ - Trace("inst-add-debug") << " -> Already exists." << std::endl; + Trace("inst-add-debug") << " --> Already exists." << std::endl; ++(d_statistics.d_inst_duplicate_eq); return false; } @@ -1021,7 +1060,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo body = quantifiers::QuantifiersRewriter::preprocess( body, true ); Trace("inst-debug") << "...preprocess to " << body << std::endl; - //construct the lemma + //construct the lemma Trace("inst-assert") << "(assert " << body << ")" << std::endl; body = Rewriter::rewrite(body); Node lem = NodeManager::currentNM()->mkNode( kind::OR, q.negate(), body ); @@ -1055,17 +1094,21 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo } setInstantiationLevelAttr( body, q[1], maxInstLevel+1 ); } - if( d_curr_effort_level>QEFFORT_CONFLICT ){ + if( d_curr_effort_level>QEFFORT_CONFLICT && d_curr_effort_levelnotifyInstantiation( d_curr_effort_level, q, lem, terms, body ); + if( !d_inst_notify[j]->notifyInstantiation( d_curr_effort_level, q, lem, terms, body ) ){ + Trace("inst-add-debug") << "...we are in conflict." << std::endl; + d_conflict = true; + Assert( !d_lemmas_waiting.empty() ); + } } } - Trace("inst-add-debug") << " -> Success." << std::endl; + Trace("inst-add-debug") << " --> Success." << std::endl; ++(d_statistics.d_instantiations); return true; }else{ - Trace("inst-add-debug") << " -> Lemma already exists." << std::endl; + Trace("inst-add-debug") << " --> Lemma already exists." << std::endl; ++(d_statistics.d_inst_duplicate); return false; } @@ -1090,6 +1133,16 @@ bool QuantifiersEngine::addSplitEquality( Node n1, Node n2, bool reqPhase, bool return addSplit( fm ); } +bool QuantifiersEngine::removeInstantiation( Node q, Node lem, std::vector< Node >& terms ) { + //lem must occur in d_waiting_lemmas + if( removeLemma( lem ) ){ + return removeInstantiationInternal( q, terms ); + }else{ + return false; + } +} + + bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) { Trace("quant-engine-debug2") << "Get inst when needs check, counts=" << d_ierCounter << ", " << d_ierCounter_lc << std::endl; //determine if we should perform check, based on instWhenMode diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 9ee967eb0..bad9c0169 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -47,7 +47,7 @@ namespace quantifiers { class InstantiationNotify { public: InstantiationNotify(){} - virtual void notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) = 0; + virtual bool notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) = 0; }; namespace quantifiers { @@ -151,9 +151,14 @@ public: //effort levels //none QEFFORT_NONE, }; -private: +private: //this information is reset during check /** current effort level */ unsigned d_curr_effort_level; + /** are we in conflict */ + bool d_conflict; + /** has added lemma this round */ + bool d_hasAddedLemma; +private: /** list of all quantifiers seen */ std::map< Node, bool > d_quants; /** quantifiers reduced */ @@ -165,8 +170,6 @@ private: std::vector< Node > d_lemmas_waiting; /** phase requirements waiting */ std::map< Node, bool > d_phase_req_waiting; - /** has added lemma this round */ - bool d_hasAddedLemma; /** list of all instantiations produced for each quantifier */ std::map< Node, inst::InstMatchTrie > d_inst_match_trie; std::map< Node, inst::CDInstMatchTrie* > d_c_inst_match_trie; @@ -282,7 +285,9 @@ private: /** compute term vector */ void computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms ); /** record instantiation, return true if it was non-duplicate */ - bool recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq = false, bool modInst = false ); + bool recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq = false, bool modInst = false, bool addedLem = true ); + /** remove instantiation */ + bool removeInstantiationInternal( Node q, std::vector< Node >& terms ); /** set instantiation level attr */ static void setInstantiationLevelAttr( Node n, Node qn, uint64_t level ); /** flush lemmas */ @@ -298,18 +303,24 @@ public: Node getSubstitute( Node n, std::vector< Node >& terms ); /** add lemma lem */ bool addLemma( Node lem, bool doCache = true, bool doRewrite = true ); + /** remove pending lemma */ + bool removeLemma( Node lem ); /** add require phase */ void addRequirePhase( Node lit, bool req ); /** do instantiation specified by m */ bool addInstantiation( Node q, InstMatch& m, bool mkRep = true, bool modEq = false, bool modInst = false, bool doVts = false ); /** add instantiation */ bool addInstantiation( Node q, std::vector< Node >& terms, bool mkRep = true, bool modEq = false, bool modInst = false, bool doVts = false ); + /** remove pending instantiation */ + bool removeInstantiation( Node q, Node lem, std::vector< Node >& terms ); /** split on node n */ bool addSplit( Node n, bool reqPhase = false, bool reqPhasePol = true ); /** add split equality */ bool addSplitEquality( Node n1, Node n2, bool reqPhase = false, bool reqPhasePol = true ); /** has added lemma */ bool hasAddedLemma() { return !d_lemmas_waiting.empty() || d_hasAddedLemma; } + /** is in conflict */ + bool inConflict() { return d_conflict; } /** get number of waiting lemmas */ unsigned getNumLemmasWaiting() { return d_lemmas_waiting.size(); } /** get needs check */ @@ -328,7 +339,7 @@ public: /** get trigger database */ inst::TriggerTrie* getTriggerDatabase() { return d_tr_trie; } /** add term to database */ - void addTermToDatabase( Node n, bool withinQuant = false, bool withinInstClosure = false ); + void addTermToDatabase( Node n, bool withinQuant = false, bool withinInstClosure = false ); /** notification when master equality engine is updated */ void eqNotifyNewClass(TNode t); void eqNotifyPreMerge(TNode t1, TNode t2); diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index 575aa4159..91e0c37d4 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -38,7 +38,6 @@ TESTS = \ lst-no-self-rev-exp.smt2 \ fib-core.smt2 \ fore19-exp2-core.smt2 \ - with-ind-104-core.smt2 \ syn002-si-real-int.smt2 \ krs-sat.smt2 \ forall_unit_data2.smt2 \ -- 2.30.2