Update dynamic splitting strategy for quantifiers (#3162)

1 files changed, 79 insertions, 56 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);
   }
 }