From: Andrew Reynolds Date: Tue, 8 May 2018 16:47:53 +0000 (-0500) Subject: Infrastructure for CEGQI handled status (#1873) X-Git-Tag: cvc5-1.0.0~5080 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0240450cbac4b7043db5c29002f0c76f7d0b6381;p=cvc5.git Infrastructure for CEGQI handled status (#1873) --- diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 6e59363e2..2ef2563b3 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -18,12 +18,14 @@ #include "options/quantifiers_options.h" #include "smt/term_formula_removal.h" #include "theory/arith/arith_msum.h" +#include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/quant_epr.h" +#include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers/ematching/trigger.h" #include "theory/theory_engine.h" using namespace std; @@ -60,6 +62,18 @@ std::ostream& operator<<(std::ostream& os, CegInstPhase phase) } return os; } +std::ostream& operator<<(std::ostream& os, CegHandledStatus status) +{ + switch (status) + { + case CEG_UNHANDLED: os << "unhandled"; break; + case CEG_PARTIALLY_HANDLED: os << "partially_handled"; break; + case CEG_HANDLED: os << "handled"; break; + case CEG_HANDLED_UNCONDITIONAL: os << "unhandled_unc"; break; + default: Unreachable(); + } + return os; +} CegInstantiator::CegInstantiator(QuantifiersEngine* qe, CegqiOutput* out, @@ -127,21 +141,219 @@ bool CegInstantiator::isEligible( Node n ) { return d_inelig.find( n )==d_inelig.end(); } -bool CegInstantiator::isCbqiKind(Kind k) +CegHandledStatus CegInstantiator::isCbqiKind(Kind k) { if (quantifiers::TermUtil::isBoolConnective(k) || k == PLUS || k == GEQ || k == EQUAL || k == MULT || k == NONLINEAR_MULT) { - return true; + return CEG_HANDLED; + } + + // CBQI typically works for satisfaction-complete theories + TheoryId t = kindToTheoryId(k); + if (t == THEORY_BV || t == THEORY_DATATYPES || t == THEORY_BOOL) + { + return CEG_HANDLED; + } + return CEG_UNHANDLED; +} + +CegHandledStatus CegInstantiator::isCbqiTerm(Node n) +{ + CegHandledStatus ret = CEG_HANDLED; + std::unordered_set visited; + std::vector visit; + TNode cur; + visit.push_back(n); + do + { + cur = visit.back(); + visit.pop_back(); + if (visited.find(cur) == visited.end()) + { + visited.insert(cur); + if (cur.getKind() != BOUND_VARIABLE && TermUtil::hasBoundVarAttr(cur)) + { + if (cur.getKind() == FORALL || cur.getKind() == CHOICE) + { + visit.push_back(cur[1]); + } + else + { + CegHandledStatus curr = isCbqiKind(cur.getKind()); + if (curr < ret) + { + ret = curr; + Trace("cbqi-debug2") << "Non-cbqi kind : " << cur.getKind() + << " in " << n << std::endl; + if (curr == CEG_UNHANDLED) + { + return CEG_UNHANDLED; + } + } + for (const Node& nc : cur) + { + visit.push_back(nc); + } + } + } + } + } while (!visit.empty()); + return ret; +} + +CegHandledStatus CegInstantiator::isCbqiSort(TypeNode tn, QuantifiersEngine* qe) +{ + std::map visited; + return isCbqiSort(tn, visited, qe); +} + +CegHandledStatus CegInstantiator::isCbqiSort( + TypeNode tn, + std::map& visited, + QuantifiersEngine* qe) +{ + std::map::iterator itv = visited.find(tn); + if (itv != visited.end()) + { + return itv->second; + } + CegHandledStatus ret = CEG_UNHANDLED; + if (tn.isInteger() || tn.isReal() || tn.isBoolean() || tn.isBitVector()) + { + ret = CEG_HANDLED; + } + else if (tn.isDatatype()) + { + // recursive calls to this datatype are handlable + visited[tn] = CEG_HANDLED; + // if not recursive, it is finite and we can handle it regardless of body + // hence, we initialize ret to CEG_HANDLED_UNCONDITIONAL. + ret = CEG_HANDLED_UNCONDITIONAL; + const Datatype& dt = static_cast(tn.toType()).getDatatype(); + for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) + { + for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++) + { + TypeNode crange = TypeNode::fromType( + static_cast(dt[i][j].getType()).getRangeType()); + CegHandledStatus cret = isCbqiSort(crange, visited, qe); + if (cret == CEG_UNHANDLED) + { + visited[tn] = CEG_UNHANDLED; + return CEG_UNHANDLED; + } + else if (cret < ret) + { + ret = cret; + } + } + } + } + else if (tn.isSort()) + { + QuantEPR* qepr = qe != nullptr ? qe->getQuantEPR() : nullptr; + if (qepr != nullptr) + { + if (qepr->isEPR(tn)) + { + ret = CEG_HANDLED_UNCONDITIONAL; + } + } + } + // sets, arrays, functions and others are not supported + visited[tn] = ret; + return ret; +} + +CegHandledStatus CegInstantiator::isCbqiQuantPrefix(Node q, + QuantifiersEngine* qe) +{ + CegHandledStatus hmin = CEG_HANDLED_UNCONDITIONAL; + for (const Node& v : q[0]) + { + TypeNode tn = v.getType(); + CegHandledStatus handled = isCbqiSort(tn, qe); + if (handled == CEG_UNHANDLED) + { + return CEG_UNHANDLED; + } + else if (handled < hmin) + { + hmin = handled; + } + } + return hmin; +} + +CegHandledStatus CegInstantiator::isCbqiQuant(Node q, QuantifiersEngine* qe) +{ + // compute attributes + QAttributes qa; + QuantAttributes::computeQuantAttributes(q, qa); + if (qa.d_quant_elim) + { + return CEG_HANDLED; + } + if (qa.d_sygus) + { + return CEG_UNHANDLED; + } + Assert(!qa.d_quant_elim_partial); + // if has an instantiation pattern, don't do it + if (q.getNumChildren() == 3) + { + for (const Node& pat : q[2]) + { + if (pat.getKind() == INST_PATTERN) + { + return CEG_UNHANDLED; + } + } + } + CegHandledStatus ret = CEG_HANDLED; + // if quantifier has a non-handled variable, then do not use cbqi + // if quantifier has an APPLY_UF term, then do not use cbqi unless EPR + CegHandledStatus ncbqiv = CegInstantiator::isCbqiQuantPrefix(q, qe); + Trace("cbqi-quant-debug") << "isCbqiQuantPrefix returned " << ncbqiv + << std::endl; + if (ncbqiv == CEG_UNHANDLED) + { + // unhandled variable type + ret = CEG_UNHANDLED; } else { - // CBQI typically works for satisfaction-complete theories - TheoryId t = kindToTheoryId(k); - return t == THEORY_BV || t == THEORY_DATATYPES || t == THEORY_BOOL; + CegHandledStatus cbqit = CegInstantiator::isCbqiTerm(q); + Trace("cbqi-quant-debug") << "isCbqiTerm returned " << cbqit << std::endl; + if (cbqit == CEG_UNHANDLED) + { + if (ncbqiv == CEG_HANDLED_UNCONDITIONAL) + { + // all variables are fully handled, this implies this will be handlable + // regardless of body (e.g. for EPR) + // so, try but not exclusively + ret = CEG_PARTIALLY_HANDLED; + } + else + { + // cannot be handled + ret = CEG_UNHANDLED; + } + } + else if (cbqit == CEG_PARTIALLY_HANDLED) + { + ret = CEG_PARTIALLY_HANDLED; + } + } + if (ret == CEG_UNHANDLED && options::cbqiAll()) + { + // try but not exclusively + ret = CEG_PARTIALLY_HANDLED; } + return ret; } bool CegInstantiator::hasVariable( Node n, Node pv ) { diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h index 6cbc7418c..b1da66d18 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h @@ -186,6 +186,24 @@ enum CegInstPhase std::ostream& operator<<(std::ostream& os, CegInstPhase phase); +/** + * The handled status of a sort/term/quantified formula, indicating whether + * counterexample-guided instantiation handles it. + */ +enum CegHandledStatus +{ + // the sort/term/quantified formula is unhandled by cegqi + CEG_UNHANDLED, + // the sort/term/quantified formula is partially handled by cegqi + CEG_PARTIALLY_HANDLED, + // the sort/term/quantified formula is handled by cegqi + CEG_HANDLED, + // the sort/term/quantified formula is handled by cegqi, regardless of + // additional factors + CEG_HANDLED_UNCONDITIONAL, +}; +std::ostream& operator<<(std::ostream& os, CegHandledStatus status); + /** Ceg instantiator * * This class manages counterexample-guided quantifier instantiation @@ -297,14 +315,56 @@ class CegInstantiator { bool useVtsInfinity() { return d_use_vts_inf; } /** are we processing a nested quantified formula? */ bool hasNestedQuantification() { return d_is_nested_quant; } + //------------------------------------ static queries /** Is k a kind for which counterexample-guided instantiation is possible? * - * This typically corresponds to kinds that correspond to operators that - * have total interpretations and are a part of the signature of - * satisfaction complete theories (see Reynolds et al., CAV 2015). - */ - static bool isCbqiKind(Kind k); - + * If this method returns CEG_UNHANDLED, then we prohibit cegqi for terms + * involving this kind. If this method returns CEG_HANDLED, our approaches + * for cegqi fully handle the kind. + * + * This typically corresponds to kinds that correspond to operators that + * have total interpretations and are a part of the signature of + * satisfaction complete theories (see Reynolds et al., CAV 2015). + */ + static CegHandledStatus isCbqiKind(Kind k); + /** is cbqi term? + * + * This method returns whether the term is handled by cegqi techniques, i.e. + * whether all subterms of n have kinds that can be handled by cegqi. + */ + static CegHandledStatus isCbqiTerm(Node n); + /** is cbqi sort? + * + * This method returns whether the type tn is handled by cegqi techniques. + * If the result is CEG_HANDLED_UNCONDITIONAL, then this indicates that a + * variable of this type is handled regardless of the formula it appears in. + * + * The argument qe is used if handling sort tn is conditional on the + * strategies initialized in qe. For example, uninterpreted sorts are + * handled if dedicated support for EPR is enabled. + */ + static CegHandledStatus isCbqiSort(TypeNode tn, + QuantifiersEngine* qe = nullptr); + /** is cbqi quantifier prefix + * + * This returns the minimum value of the above method for a bound variable + * in the prefix of quantified formula q. + */ + static CegHandledStatus isCbqiQuantPrefix(Node q, + QuantifiersEngine* qe = nullptr); + /** is cbqi quantified formula + * + * This returns whether quantified formula q can and should be handled by + * counterexample-guided instantiation. If this function returns + * a status CEG_HANDLED or above, then q is fully handled by counterexample + * guided quantifier instantiation and need not be processed by any other + * strategy for quantifiers (e.g. E-matching). Otherwise, if this function + * returns CEG_PARTIALLY_HANDLED, then it may be worthwhile to handle the + * quantified formula using cegqi, however other strategies should also be + * tried. + */ + static CegHandledStatus isCbqiQuant(Node q, QuantifiersEngine* qe = nullptr); + //------------------------------------ end static queries private: /** quantified formula associated with this instantiator */ QuantifiersEngine* d_qe; @@ -542,6 +602,18 @@ class CegInstantiator { bool doAddInstantiation(std::vector& vars, std::vector& subs, std::vector& lemmas); + + //------------------------------------ static queries + /** is cbqi sort + * + * Helper function for isCbqiSort. This function recurses over the structure + * of the type tn, where visited stores the types we have visited. + */ + static CegHandledStatus isCbqiSort( + TypeNode tn, + std::map& visited, + QuantifiersEngine* qe); + //------------------------------------ end static queries }; /** Instantiator class diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp index d2aa75288..4b79c4e79 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp @@ -289,9 +289,9 @@ bool InstStrategyCbqi::checkComplete() { } bool InstStrategyCbqi::checkCompleteFor( Node q ) { - std::map< Node, int >::iterator it = d_do_cbqi.find( q ); + std::map::iterator it = d_do_cbqi.find(q); if( it!=d_do_cbqi.end() ){ - return it->second>0; + return it->second != CEG_UNHANDLED; }else{ return false; } @@ -346,7 +346,8 @@ Node InstStrategyCbqi::getIdMarkedQuantNode( Node n, std::map< Node, Node >& vis void InstStrategyCbqi::preRegisterQuantifier( Node q ) { if( d_quantEngine->getOwner( q )==NULL && doCbqi( q ) ){ - if( d_do_cbqi[q]==2 ){ + if (d_do_cbqi[q] == CEG_HANDLED) + { //take full ownership of the quantified formula d_quantEngine->setOwner( q, this ); @@ -355,8 +356,9 @@ void InstStrategyCbqi::preRegisterQuantifier( Node q ) { std::map< Node, Node > visited; Node mq = getIdMarkedQuantNode( q[1], visited ); if( mq!=q[1] ){ - //do not do cbqi - d_do_cbqi[q] = false; + // do not do cbqi, we are reducing this quantified formula to a marked + // one + d_do_cbqi[q] = CEG_UNHANDLED; //instead do reduction std::vector< Node > qqc; qqc.push_back( q[0] ); @@ -479,130 +481,15 @@ void InstStrategyCbqi::registerCounterexampleLemma( Node q, Node lem ){ d_quantEngine->addLemma( lem, false ); } -bool InstStrategyCbqi::hasNonCbqiOperator( Node n, std::map< Node, bool >& visited ){ - if( visited.find( n )==visited.end() ){ - visited[n] = true; - if( n.getKind()!=BOUND_VARIABLE && TermUtil::hasBoundVarAttr( n ) ){ - if (!CegInstantiator::isCbqiKind(n.getKind())) - { - Trace("cbqi-debug2") << "Non-cbqi kind : " << n.getKind() << " in " << n << std::endl; - return true; - } - else if (n.getKind() == FORALL || n.getKind() == CHOICE) - { - return hasNonCbqiOperator( n[1], visited ); - }else{ - for( unsigned i=0; i& visited ) { - std::map< TypeNode, int >::iterator itv = visited.find( tn ); - if( itv==visited.end() ){ - visited[tn] = 0; - int ret = -1; - if( tn.isInteger() || tn.isReal() || tn.isBoolean() || tn.isBitVector() ){ - ret = 0; - }else if( tn.isDatatype() ){ - ret = 1; - const Datatype& dt = ((DatatypeType)tn.toType()).getDatatype(); - for( unsigned i=0; igetQuantEPR(); - if( qepr!=NULL ){ - ret = qepr->isEPR( tn ) ? 1 : -1; - } - } - visited[tn] = ret; - return ret; - }else{ - return itv->second; - } -} - -int InstStrategyCbqi::hasNonCbqiVariable( Node q ){ - int hmin = 1; - for( unsigned i=0; i visited; - int handled = isCbqiSort( tn, visited ); - if( handled==-1 ){ - return -1; - }else if( handled::iterator it = d_do_cbqi.find( q ); + std::map::iterator it = d_do_cbqi.find(q); if( it==d_do_cbqi.end() ){ - int ret = 2; - if( !d_quantEngine->getQuantAttributes()->isQuantElim( q ) ){ - Assert( !d_quantEngine->getQuantAttributes()->isQuantElimPartial( q ) ); - //if has an instantiation pattern, don't do it - if( q.getNumChildren()==3 && options::eMatching() && options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ){ - for( unsigned i=0; igetQuantAttributes()->isSygus( q ) ){ - ret = 0; - } - if( ret!=0 ){ - //if quantifier has a non-handled variable, then do not use cbqi - //if quantifier has an APPLY_UF term, then do not use cbqi unless EPR - int ncbqiv = hasNonCbqiVariable( q ); - if( ncbqiv==0 || ncbqiv==1 ){ - std::map< Node, bool > visited; - if( hasNonCbqiOperator( q[1], visited ) ){ - if( ncbqiv==1 ){ - //all variables are fully handled, this implies this will be handlable regardless of body (e.g. for EPR) - // so, try but not exclusively - ret = 1; - }else{ - //cannot be handled - ret = 0; - } - } - }else{ - // unhandled variable type - ret = 0; - } - if( ret==0 && options::cbqiAll() ){ - //try but not exclusively - ret = 1; - } - } - } + CegHandledStatus ret = CegInstantiator::isCbqiQuant(q, d_quantEngine); Trace("cbqi-quant") << "doCbqi " << q << " returned " << ret << std::endl; d_do_cbqi[q] = ret; - return ret!=0; - }else{ - return it->second!=0; + return ret != CEG_UNHANDLED; } + return it->second != CEG_UNHANDLED; } Node InstStrategyCbqi::getNextDecisionRequestProc( Node q, std::map< Node, bool >& proc ) { diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h index 2bc86ef4e..5a4db0e53 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h @@ -47,19 +47,13 @@ class InstStrategyCbqi : public QuantifiersModule { std::map< Node, std::vector< Node > > d_parent_quant; std::map< Node, std::vector< Node > > d_children_quant; std::map< Node, bool > d_active_quant; - /** whether we have instantiated quantified formulas */ - //NodeSet d_added_inst; - /** whether to do cbqi for this quantified formula 0 : no, 2 : yes, 1 : yes but not exclusively, -1 : heuristically */ - std::map< Node, int > d_do_cbqi; + /** Whether cegqi handles each quantified formula. */ + std::map d_do_cbqi; /** register ce lemma */ bool registerCbqiLemma( Node q ); virtual void registerCounterexampleLemma( Node q, Node lem ); /** has added cbqi lemma */ bool hasAddedCbqiLemma( Node q ) { return d_added_cbqi_lemma.find( q )!=d_added_cbqi_lemma.end(); } - /** helper functions */ - int hasNonCbqiVariable( Node q ); - bool hasNonCbqiOperator( Node n, std::map< Node, bool >& visited ); - int isCbqiSort( TypeNode tn, std::map< TypeNode, int >& visited ); /** get next decision request with dependency checking */ Node getNextDecisionRequestProc( Node q, std::map< Node, bool >& proc ); /** process functions */