Update dynamic splitting strategy for quantifiers (#3162)

4 files changed, 162 insertions, 66 deletions

diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
index 808c6006f..4e9441279 100644
--- a/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -35,9 +35,6 @@ void QuantDSplit::checkOwnership(Node q)
 {
   int max_index = -1;
   int max_score = -1;
-  if( q.getNumChildren()==3 ){
-    return;
-  }
   Trace("quant-dsplit-debug") << "Check split quantified formula : " << q << std::endl;
   for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
     TypeNode tn = q[0][i].getType();
@@ -50,10 +47,19 @@ void QuantDSplit::checkOwnership(Node q)
         if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_AGG ){
           score = dt.isInterpretedFinite( tn.toType() ) ? 1 : 0;
         }else if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_DEFAULT ){
-          //only split if goes from being unhandled -> handled by finite instantiation
-          //  an example is datatypes with uninterpreted sort fields, which are "interpreted finite" but not "finite"
           if( !d_quantEngine->isFiniteBound( q, q[0][i] ) ){
-            score = dt.isInterpretedFinite( tn.toType() ) ? 1 : -1;
+            if (dt.isInterpretedFinite(tn.toType()))
+            {
+              // split if goes from being unhandled -> handled by finite
+              // instantiation. An example is datatypes with uninterpreted sort
+              // fields which are "interpreted finite" but not "finite".
+              score = 1;
+            }
+            else if (dt.getNumConstructors() == 1 && !dt.isCodatatype())
+            {
+              // split if only one constructor
+              score = 1;
+            }
           }
         }
         Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is score " << score << " (" << dt.isInterpretedFinite( tn.toType() ) << " " << dt.isFinite( tn.toType() ) << ")" << std::endl;
@@ -86,62 +92,79 @@ bool QuantDSplit::checkCompleteFor( Node q ) {
 void QuantDSplit::check(Theory::Effort e, QEffort quant_e)
 {
   //add lemmas ASAP (they are a reduction)
-  if (quant_e == QEFFORT_CONFLICT)
+  if (quant_e != QEFFORT_CONFLICT)
   {
-    std::vector< Node > lemmas;
-    for(std::map< Node, int >::iterator it = d_quant_to_reduce.begin(); it != d_quant_to_reduce.end(); ++it) {
-      Node q = it->first;
-      if( d_quantEngine->getModel()->isQuantifierAsserted( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
-        if( d_added_split.find( q )==d_added_split.end() ){
-          d_added_split.insert( q );
-          std::vector< Node > bvs;
-          for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
-            if( (int)i!=it->second ){
-              bvs.push_back( q[0][i] );
-            }
-          }
-          std::vector< Node > disj;
-          disj.push_back( q.negate() );
-          TNode svar = q[0][it->second];
-          TypeNode tn = svar.getType();
-          if( tn.isDatatype() ){
-            std::vector< Node > cons;
-            const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-            for( unsigned j=0; j<dt.getNumConstructors(); j++ ){
-              std::vector< Node > vars;
-              for( unsigned k=0; k<dt[j].getNumArgs(); k++ ){
-                TypeNode tns = TypeNode::fromType( dt[j][k].getRangeType() );
-                Node v = NodeManager::currentNM()->mkBoundVar( tns );
-                vars.push_back( v );
-              }
-              std::vector< Node > bvs_cmb;
-              bvs_cmb.insert( bvs_cmb.end(), bvs.begin(), bvs.end() );
-              bvs_cmb.insert( bvs_cmb.end(), vars.begin(), vars.end() );
-              vars.insert( vars.begin(), Node::fromExpr( dt[j].getConstructor() ) );
-              Node c = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, vars );
-              TNode ct = c;
-              Node body = q[1].substitute( svar, ct );
-              if( !bvs_cmb.empty() ){
-                body = NodeManager::currentNM()->mkNode( kind::FORALL, NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, bvs_cmb ), body );
-              }
-              cons.push_back( body );
-            }
-            Node conc = cons.size()==1 ? cons[0] : NodeManager::currentNM()->mkNode( kind::AND, cons );
-            disj.push_back( conc );
-          }else{
-            Assert( false );
+    return;
+  }
+  NodeManager* nm = NodeManager::currentNM();
+  FirstOrderModel* m = d_quantEngine->getModel();
+  std::vector<Node> lemmas;
+  for (std::map<Node, int>::iterator it = d_quant_to_reduce.begin();
+       it != d_quant_to_reduce.end();
+       ++it)
+  {
+    Node q = it->first;
+    if (m->isQuantifierAsserted(q) && m->isQuantifierActive(q)
+        && d_added_split.find(q) == d_added_split.end())
+    {
+      d_added_split.insert(q);
+      std::vector<Node> bvs;
+      for (unsigned i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
+      {
+        if (static_cast<int>(i) != it->second)
+        {
+          bvs.push_back(q[0][i]);
+        }
+      }
+      std::vector<Node> disj;
+      disj.push_back(q.negate());
+      TNode svar = q[0][it->second];
+      TypeNode tn = svar.getType();
+      Assert(tn.isDatatype());
+      std::vector<Node> cons;
+      const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+      for (unsigned j = 0, ncons = dt.getNumConstructors(); j < ncons; j++)
+      {
+        std::vector<Node> vars;
+        for (unsigned k = 0, nargs = dt[j].getNumArgs(); k < nargs; k++)
+        {
+          TypeNode tns = TypeNode::fromType(dt[j][k].getRangeType());
+          Node v = nm->mkBoundVar(tns);
+          vars.push_back(v);
+        }
+        std::vector<Node> bvs_cmb;
+        bvs_cmb.insert(bvs_cmb.end(), bvs.begin(), bvs.end());
+        bvs_cmb.insert(bvs_cmb.end(), vars.begin(), vars.end());
+        vars.insert(vars.begin(), Node::fromExpr(dt[j].getConstructor()));
+        Node c = nm->mkNode(kind::APPLY_CONSTRUCTOR, vars);
+        TNode ct = c;
+        Node body = q[1].substitute(svar, ct);
+        if (!bvs_cmb.empty())
+        {
+          Node bvl = nm->mkNode(kind::BOUND_VAR_LIST, bvs_cmb);
+          std::vector<Node> children;
+          children.push_back(bvl);
+          children.push_back(body);
+          if (q.getNumChildren() == 3)
+          {
+            Node ipls = q[2].substitute(svar, ct);
+            children.push_back(ipls);
           }
-          lemmas.push_back( disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( kind::OR, disj ) );
+          body = nm->mkNode(kind::FORALL, children);
         }
+        cons.push_back(body);
       }
+      Node conc = cons.size() == 1 ? cons[0] : nm->mkNode(kind::AND, cons);
+      disj.push_back(conc);
+      lemmas.push_back(disj.size() == 1 ? disj[0] : nm->mkNode(kind::OR, disj));
     }
+  }
 
-    //add lemmas to quantifiers engine
-    for( unsigned i=0; i<lemmas.size(); i++ ){
-      Trace("quant-dsplit") << "QuantDSplit lemma : " << lemmas[i] << std::endl;
-      d_quantEngine->addLemma( lemmas[i], false );
-    }
-    //d_quant_to_reduce.clear();
+  // add lemmas to quantifiers engine
+  for (const Node& lem : lemmas)
+  {
+    Trace("quant-dsplit") << "QuantDSplit lemma : " << lem << std::endl;
+    d_quantEngine->addLemma(lem, false);
   }
 }
 
diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h
index e88e99a83..bea0c3439 100644
--- a/src/theory/quantifiers/quant_split.h
+++ b/src/theory/quantifiers/quant_split.h
@@ -27,28 +27,45 @@ class QuantifiersEngine;
 
 namespace quantifiers {
 
+/** Quantifiers dynamic splitting
+ *
+ * This module identifies quantified formulas that should be "split", e.g.
+ * based on datatype constructor case splitting.
+ *
+ * An example of a quantified formula that we may split is the following. Let:
+ *   optionPair := mkPair( U, U ) | none
+ * where U is an uninterpreted sort. The quantified formula:
+ *   forall x : optionPair. P( x )
+ * may be "split" via the lemma:
+ *   forall x : optionPair. P( x ) <=>
+ *   ( forall xy : U. P( mkPair( x, y ) ) OR P( none ) )
+ *
+ * Notice that such splitting may lead to exponential behavior, say if we
+ * quantify over 32 variables of type optionPair above gives 2^32 disjuncts.
+ * This class is used to compute this splitting dynamically, by splitting
+ * one variable per quantified formula at a time.
+ */
 class QuantDSplit : public QuantifiersModule {
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
-private:
-  /** list of relevant quantifiers asserted in the current context */
-  std::map< Node, int > d_quant_to_reduce;
-  /** whether we have instantiated quantified formulas */
-  NodeSet d_added_split;
-public:
+
+ public:
   QuantDSplit( QuantifiersEngine * qe, context::Context* c );
   /** determine whether this quantified formula will be reduced */
   void checkOwnership(Node q) override;
-
   /* whether this module needs to check this round */
   bool needsCheck(Theory::Effort e) override;
   /* Call during quantifier engine's check */
   void check(Theory::Effort e, QEffort quant_e) override;
-  /* Called for new quantifiers */
-  void registerQuantifier(Node q) override {}
-  void assertNode(Node n) override {}
+  /** check complete for */
   bool checkCompleteFor(Node q) override;
   /** Identify this module (for debugging, dynamic configuration, etc..) */
   std::string identify() const override { return "QuantDSplit"; }
+
+ private:
+  /** list of relevant quantifiers asserted in the current context */
+  std::map<Node, int> d_quant_to_reduce;
+  /** whether we have instantiated quantified formulas */
+  NodeSet d_added_split;
 };
 
 }
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index fb21d6895..f5159a630 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -1076,6 +1076,23 @@ bool QuantifiersRewriter::getVarElimLit(Node lit,
       }
     }
   }
+  else if (lit.getKind() == APPLY_TESTER && pol
+           && lit[0].getKind() == BOUND_VARIABLE && options::dtVarExpandQuant())
+  {
+    Trace("var-elim-dt") << "Expand datatype variable based on : " << lit
+                         << std::endl;
+    Expr testerExpr = lit.getOperator().toExpr();
+    unsigned index = Datatype::indexOf(testerExpr);
+    Node s = datatypeExpand(index, lit[0], args);
+    if (!s.isNull())
+    {
+      vars.push_back(lit[0]);
+      subs.push_back(s);
+      Trace("var-elim-dt") << "...apply substitution " << s << "/" << lit[0]
+                           << std::endl;
+      return true;
+    }
+  }
   if (lit.getKind() == BOUND_VARIABLE)
   {
     std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), lit );
@@ -1149,6 +1166,38 @@ bool QuantifiersRewriter::getVarElimLit(Node lit,
   return false;
 }
 
+Node QuantifiersRewriter::datatypeExpand(unsigned index,
+                                         Node v,
+                                         std::vector<Node>& args)
+{
+  if (!v.getType().isDatatype())
+  {
+    return Node::null();
+  }
+  std::vector<Node>::iterator ita = std::find(args.begin(), args.end(), v);
+  if (ita == args.end())
+  {
+    return Node::null();
+  }
+  const Datatype& dt =
+      static_cast<DatatypeType>(v.getType().toType()).getDatatype();
+  Assert(index < dt.getNumConstructors());
+  const DatatypeConstructor& c = dt[index];
+  std::vector<Node> newChildren;
+  newChildren.push_back(Node::fromExpr(c.getConstructor()));
+  std::vector<Node> newVars;
+  for (unsigned j = 0, nargs = c.getNumArgs(); j < nargs; j++)
+  {
+    TypeNode tn = TypeNode::fromType(c.getArgType(j));
+    Node vn = NodeManager::currentNM()->mkBoundVar(tn);
+    newChildren.push_back(vn);
+    newVars.push_back(vn);
+  }
+  args.erase(ita);
+  args.insert(args.end(), newVars.begin(), newVars.end());
+  return NodeManager::currentNM()->mkNode(APPLY_CONSTRUCTOR, newChildren);
+}
+
 bool QuantifiersRewriter::getVarElim(Node n,
                                      bool pol,
                                      std::vector<Node>& args,
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index b72619392..7703f01fd 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -50,6 +50,13 @@ private:
                                     std::map< Node, Node >& cache, std::map< Node, Node >& icache,
                                     std::vector< Node >& new_vars, std::vector< Node >& new_conds, bool elimExtArith );
   static void computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, std::vector< Node >& conj );
+  /** datatype expand
+   *
+   * If v occurs in args and has a datatype type whose index^th constructor is
+   * C, this method returns a node of the form C( x1, ..., xn ), removes v from
+   * args and adds x1...xn to args.
+   */
+  static Node datatypeExpand(unsigned index, Node v, std::vector<Node>& args);
   //-------------------------------------variable elimination
   /** is variable elimination
    *