Fix quantifiers dynamic split module for parametric datatypes (#7085)

Fixes #6838.

5 files changed, 53 insertions, 29 deletions

diff --git a/src/theory/datatypes/theory_datatypes_utils.cpp b/src/theory/datatypes/theory_datatypes_utils.cpp
index 582f11c72..3b36ad2f2 100644
--- a/src/theory/datatypes/theory_datatypes_utils.cpp
+++ b/src/theory/datatypes/theory_datatypes_utils.cpp
@@ -28,12 +28,11 @@ namespace datatypes {
 namespace utils {
 
 /** get instantiate cons */
-Node getInstCons(Node n, const DType& dt, int index)
+Node getInstCons(Node n, const DType& dt, size_t index)
 {
-  Assert(index >= 0 && index < (int)dt.getNumConstructors());
+  Assert(index < dt.getNumConstructors());
   std::vector<Node> children;
   NodeManager* nm = NodeManager::currentNM();
-  children.push_back(dt[index].getConstructor());
   TypeNode tn = n.getType();
   for (unsigned i = 0, nargs = dt[index].getNumArgs(); i < nargs; i++)
   {
@@ -41,30 +40,37 @@ Node getInstCons(Node n, const DType& dt, int index)
         APPLY_SELECTOR_TOTAL, dt[index].getSelectorInternal(tn, i), n);
     children.push_back(nc);
   }
-  Node n_ic = nm->mkNode(APPLY_CONSTRUCTOR, children);
+  Node n_ic = mkApplyCons(tn, dt, index, children);
+  Assert(n_ic.getType() == tn);
+  Assert(static_cast<size_t>(isInstCons(n, n_ic, dt)) == index);
+  return n_ic;
+}
+
+Node mkApplyCons(TypeNode tn,
+                 const DType& dt,
+                 size_t index,
+                 const std::vector<Node>& children)
+{
+  Assert(tn.isDatatype());
+  Assert(index < dt.getNumConstructors());
+  Assert(dt[index].getNumArgs() == children.size());
+  NodeManager* nm = NodeManager::currentNM();
+  std::vector<Node> cchildren;
+  cchildren.push_back(dt[index].getConstructor());
+  cchildren.insert(cchildren.end(), children.begin(), children.end());
   if (dt.isParametric())
   {
     // add type ascription for ambiguous constructor types
-    if (!n_ic.getType().isComparableTo(tn))
-    {
-      Debug("datatypes-parametric")
-          << "DtInstantiate: ambiguous type for " << n_ic << ", ascribe to "
-          << n.getType() << std::endl;
-      Debug("datatypes-parametric")
-          << "Constructor is " << dt[index] << std::endl;
-      TypeNode tspec = dt[index].getSpecializedConstructorType(n.getType());
-      Debug("datatypes-parametric")
-          << "Type specification is " << tspec << std::endl;
-      children[0] = nm->mkNode(APPLY_TYPE_ASCRIPTION,
-                               nm->mkConst(AscriptionType(tspec)),
-                               children[0]);
-      n_ic = nm->mkNode(APPLY_CONSTRUCTOR, children);
-      Assert(n_ic.getType() == tn);
-    }
+    Debug("datatypes-parametric")
+        << "Constructor is " << dt[index] << std::endl;
+    TypeNode tspec = dt[index].getSpecializedConstructorType(tn);
+    Debug("datatypes-parametric")
+        << "Type specification is " << tspec << std::endl;
+    cchildren[0] = nm->mkNode(APPLY_TYPE_ASCRIPTION,
+                              nm->mkConst(AscriptionType(tspec)),
+                              cchildren[0]);
   }
-  Assert(isInstCons(n, n_ic, dt) == index);
-  // n_ic = Rewriter::rewrite( n_ic );
-  return n_ic;
+  return nm->mkNode(APPLY_CONSTRUCTOR, cchildren);
 }
 
 int isInstCons(Node t, Node n, const DType& dt)
diff --git a/src/theory/datatypes/theory_datatypes_utils.h b/src/theory/datatypes/theory_datatypes_utils.h
index 705e867b9..1a6e6619b 100644
--- a/src/theory/datatypes/theory_datatypes_utils.h
+++ b/src/theory/datatypes/theory_datatypes_utils.h
@@ -34,7 +34,17 @@ namespace utils {
  * This returns the term C( sel^{C,1}( n ), ..., sel^{C,m}( n ) ),
  * where C is the index^{th} constructor of datatype dt.
  */
-Node getInstCons(Node n, const DType& dt, int index);
+Node getInstCons(Node n, const DType& dt, size_t index);
+/**
+ * Apply constructor, taking into account whether the datatype is parametric.
+ *
+ * Return the index^th constructor of dt applied to children, where tn is the
+ * datatype type for dt, instantiated if dt is parametric.
+ */
+Node mkApplyCons(TypeNode tn,
+                 const DType& dt,
+                 size_t index,
+                 const std::vector<Node>& children);
 /** is instantiation cons
  *
  * If this method returns a value >=0, then that value, call it index,
diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
index cc2525b78..941b94d23 100644
--- a/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -17,9 +17,10 @@
 
 #include "expr/dtype.h"
 #include "expr/dtype_cons.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/first_order_model.h"
 #include "options/quantifiers_options.h"
+#include "theory/datatypes/theory_datatypes_utils.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/term_database.h"
 
 using namespace cvc5::kind;
 
@@ -164,17 +165,18 @@ void QuantDSplit::check(Theory::Effort e, QEffort quant_e)
       for (unsigned j = 0, ncons = dt.getNumConstructors(); j < ncons; j++)
       {
         std::vector<Node> vars;
+        TypeNode dtjtn = dt[j].getSpecializedConstructorType(tn);
+        Assert(dtjtn.getNumChildren() == dt[j].getNumArgs() + 1);
         for (unsigned k = 0, nargs = dt[j].getNumArgs(); k < nargs; k++)
         {
-          TypeNode tns = dt[j][k].getRangeType();
+          TypeNode tns = dtjtn[k];
           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(), dt[j].getConstructor());
-        Node c = nm->mkNode(kind::APPLY_CONSTRUCTOR, vars);
+        Node c = datatypes::utils::mkApplyCons(tn, dt, j, vars);
         TNode ct = c;
         Node body = q[1].substitute(svar, ct);
         if (!bvs_cmb.empty())
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index ec6d04c1d..dca8860fd 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -911,6 +911,7 @@ set(regress_0_tests
   regress0/quantifiers/issue5645-dt-cm-spurious.smt2
   regress0/quantifiers/issue5693-prenex.smt2
   regress0/quantifiers/issue6603-dt-bool-cegqi.smt2
+  regress0/quantifiers/issue6838-qpdt.smt2
   regress0/quantifiers/issue6996-trivial-elim.smt2
   regress0/quantifiers/issue6999-deq-elim.smt2
   regress0/quantifiers/lra-triv-gn.smt2
diff --git a/test/regress/regress0/quantifiers/issue6838-qpdt.smt2 b/test/regress/regress0/quantifiers/issue6838-qpdt.smt2
new file mode 100644
index 000000000..8aad3c708
--- /dev/null
+++ b/test/regress/regress0/quantifiers/issue6838-qpdt.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL)
+(set-info :status unsat)
+(declare-datatype Box (par (A) ((box (unbox A)))))
+(assert (forall ((xy (Box Bool))) (unbox xy)))
+(check-sat)