Infrastructure for CEGQI handled status (#1873)

4 files changed, 309 insertions, 144 deletions

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<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 ) {
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<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
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<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;
   }
@@ -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<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 ) {
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<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 */