#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;
}
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,
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<TNode, TNodeHashFunction> visited;
+ std::vector<TNode> 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<TypeNode, CegHandledStatus> visited;
+ return isCbqiSort(tn, visited, qe);
+}
+
+CegHandledStatus CegInstantiator::isCbqiSort(
+ TypeNode tn,
+ std::map<TypeNode, CegHandledStatus>& visited,
+ QuantifiersEngine* qe)
+{
+ std::map<TypeNode, CegHandledStatus>::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<DatatypeType>(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<SelectorType>(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 ) {
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
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;
bool doAddInstantiation(std::vector<Node>& vars,
std::vector<Node>& subs,
std::vector<Node>& 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<TypeNode, CegHandledStatus>& visited,
+ QuantifiersEngine* qe);
+ //------------------------------------ end static queries
};
/** Instantiator class
}
bool InstStrategyCbqi::checkCompleteFor( Node q ) {
- std::map< Node, int >::iterator it = d_do_cbqi.find( q );
+ std::map<Node, CegHandledStatus>::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;
}
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 );
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] );
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<n.getNumChildren(); i++ ){
- if( hasNonCbqiOperator( n[i], visited ) ){
- return true;
- }
- }
- }
- }
- }
- return false;
-}
-
-// -1 : not cbqi sort, 0 : cbqi sort, 1 : cbqi sort regardless of quantifier body
-int InstStrategyCbqi::isCbqiSort( TypeNode tn, std::map< TypeNode, int >& 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; i<dt.getNumConstructors(); i++ ){
- for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
- TypeNode crange = TypeNode::fromType( ((SelectorType)dt[i][j].getType()).getRangeType() );
- int cret = isCbqiSort( crange, visited );
- if( cret==-1 ){
- visited[tn] = -1;
- return -1;
- }else if( cret<ret ){
- ret = cret;
- }
- }
- }
- }else if( tn.isSort() ){
- QuantEPR * qepr = d_quantEngine->getQuantEPR();
- 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<q[0].getNumChildren(); i++ ){
- TypeNode tn = q[0][i].getType();
- std::map< TypeNode, int > visited;
- int handled = isCbqiSort( tn, visited );
- if( handled==-1 ){
- return -1;
- }else if( handled<hmin ){
- hmin = handled;
- }
- }
- return hmin;
-}
-
bool InstStrategyCbqi::doCbqi( Node q ){
- std::map< Node, int >::iterator it = d_do_cbqi.find( q );
+ std::map<Node, CegHandledStatus>::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; i<q[2].getNumChildren(); i++ ){
- if( q[2][i].getKind()==INST_PATTERN ){
- ret = 0;
- }
- }
- }
- if( d_quantEngine->getQuantAttributes()->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 ) {
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<Node, CegHandledStatus> 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 */
projects / cvc5.git / commitdiff