Fix type rule for datatype updater for parametric sorts (#7762)

Fixes cvc5/cvc5-projects#379.
Fixes cvc5/cvc5-projects#378.

diff --git a/src/theory/datatypes/theory_datatypes_type_rules.cpp b/src/theory/datatypes/theory_datatypes_type_rules.cpp
index d3c06d1f3635e6340e1742d7296c975a8387c976..78bc67868b3d1e50acae9f6dfcdda7dc270de40f 100644 (file)
--- a/src/theory/datatypes/theory_datatypes_type_rules.cpp
+++ b/src/theory/datatypes/theory_datatypes_type_rules.cpp
@@ -219,16 +219,17 @@ TypeNode DatatypeUpdateTypeRule::computeType(NodeManager* nodeManager,
   Assert(updType.getNumChildren() == 2);
   if (check)
   {
+    TypeNode t = updType[0];
     for (size_t i = 0; i < 2; i++)
     {
       TypeNode childType = n[i].getType(check);
-      TypeNode t = updType[i];
+      TypeNode targ = updType[i];
+      Trace("typecheck-idt") << "typecheck update: " << n << "[" << i
+                             << "]: " << targ << " " << childType << std::endl;
       if (t.isParametricDatatype())
       {
-        Debug("typecheck-idt")
-            << "typecheck parameterized update: " << n << std::endl;
         TypeMatcher m(t);
-        if (!m.doMatching(t, childType))
+        if (!m.doMatching(targ, childType))
         {
           throw TypeCheckingExceptionPrivate(
               n,
@@ -237,9 +238,7 @@ TypeNode DatatypeUpdateTypeRule::computeType(NodeManager* nodeManager,
       }
       else
       {
-        Debug("typecheck-idt") << "typecheck update: " << n << std::endl;
-        Debug("typecheck-idt") << "test type: " << updType << std::endl;
-        if (!t.isComparableTo(childType))
+        if (!targ.isComparableTo(childType))
         {
           throw TypeCheckingExceptionPrivate(n, "bad type for update argument");
         }
@@ -247,7 +246,7 @@ TypeNode DatatypeUpdateTypeRule::computeType(NodeManager* nodeManager,
     }
   }
   // type is the first argument
-  return updType[0];
+  return n[0].getType();
 }
 
 TypeNode DatatypeAscriptionTypeRule::computeType(NodeManager* nodeManager,

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index cb4160f582c65be2b70a322efcd4d3a724e224a9..b565895baccf9f093130d99d4e7ed90c3972938b 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -510,6 +510,7 @@ set(regress_0_tests
   regress0/datatypes/mutually-recursive.cvc.smt2
   regress0/datatypes/pair-bool-bool.cvc.smt2
   regress0/datatypes/pair-real-bool.smt2
+  regress0/datatypes/par-updater-type-rule.smt2 
   regress0/datatypes/parametric-alt-list.cvc.smt2
   regress0/datatypes/proj-issue172.smt2
   regress0/datatypes/rec1.cvc.smt2

diff --git a/test/regress/regress0/datatypes/par-updater-type-rule.smt2 b/test/regress/regress0/datatypes/par-updater-type-rule.smt2
new file mode 100644 (file)
index 0000000..0b4af02
--- /dev/null
+++ b/test/regress/regress0/datatypes/par-updater-type-rule.smt2
@@ -0,0 +1,11 @@
+(set-option :global-declarations true)
+(set-logic ALL)
+(set-info :status unsat)
+(declare-datatype _x0 ( (_x6 (_x1 Bool))))
+(declare-datatype _x36 ( (_x42 (_x37 Bool))))
+(declare-const _x53 Bool)
+(declare-const _x56 _x36)
+(declare-const _x58 _x0)
+(declare-datatype _x176 ( par ( _x178 ) ( (_x186 (_x185 _x178)) (_x184 (_x180 _x0)))) )
+(assert (let ((_let0 ((_ update _x185) (_x184 _x58) _x58)))(distinct _let0 _let0)))
+(check-sat)

diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index 23aec2386e3dfeaf1a45e84c67e203f3e589a267..c268ee4f8d3267adcdc65a1132944c616e16457d 100644 (file)
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -2671,6 +2671,77 @@ TEST_F(TestApiBlackSolver, doubleUseCons)
                CVC5ApiException);
 }
 
+TEST_F(TestApiBlackSolver, proj_issue378)
+{
+  DatatypeDecl dtdecl;
+  DatatypeConstructorDecl cdecl;
+
+  Sort s1 = d_solver.getBooleanSort();
+
+  dtdecl = d_solver.mkDatatypeDecl("_x0");
+  cdecl = d_solver.mkDatatypeConstructorDecl("_x6");
+  cdecl.addSelector("_x1", s1);
+  dtdecl.addConstructor(cdecl);
+  Sort s2 = d_solver.mkDatatypeSort(dtdecl);
+
+  dtdecl = d_solver.mkDatatypeDecl("_x36");
+  cdecl = d_solver.mkDatatypeConstructorDecl("_x42");
+  cdecl.addSelector("_x37", s1);
+  dtdecl.addConstructor(cdecl);
+  Sort s4 = d_solver.mkDatatypeSort(dtdecl);
+
+  Term t1 = d_solver.mkConst(s1, "_x53");
+  Term t4 = d_solver.mkConst(s4, "_x56");
+  Term t7 = d_solver.mkConst(s2, "_x58");
+
+  Sort sp = d_solver.mkParamSort("_x178");
+  dtdecl = d_solver.mkDatatypeDecl("_x176", sp);
+  cdecl = d_solver.mkDatatypeConstructorDecl("_x184");
+  cdecl.addSelector("_x180", s2);
+  dtdecl.addConstructor(cdecl);
+  cdecl = d_solver.mkDatatypeConstructorDecl("_x186");
+  cdecl.addSelector("_x185", sp);
+  dtdecl.addConstructor(cdecl);
+  Sort s7 = d_solver.mkDatatypeSort(dtdecl);
+  Sort s9 = s7.instantiate({s2});
+  Term t1507 = d_solver.mkTerm(
+      APPLY_CONSTRUCTOR, s9.getDatatype().getConstructorTerm("_x184"), t7);
+  ASSERT_NO_THROW(d_solver.mkTerm(
+      APPLY_UPDATER,
+      s9.getDatatype().getConstructor("_x186").getSelectorTerm("_x185"),
+      t1507,
+      t7));
+}
+
+TEST_F(TestApiBlackSolver, proj_issue379)
+{
+  Sort bsort = d_solver.getBooleanSort();
+  Sort psort = d_solver.mkParamSort("_x1");
+  DatatypeConstructorDecl cdecl;
+  DatatypeDecl dtdecl = d_solver.mkDatatypeDecl("x_0", psort);
+  cdecl = d_solver.mkDatatypeConstructorDecl("_x8");
+  cdecl.addSelector("_x7", bsort);
+  dtdecl.addConstructor(cdecl);
+  cdecl = d_solver.mkDatatypeConstructorDecl("_x6");
+  cdecl.addSelector("_x2", psort);
+  cdecl.addSelectorSelf("_x3");
+  cdecl.addSelector("_x4", psort);
+  cdecl.addSelector("_x5", bsort);
+  Sort s2 = d_solver.mkDatatypeSort(dtdecl);
+  Sort s6 = s2.instantiate({bsort});
+  Term t317 = d_solver.mkConst(bsort, "_x345");
+  Term t843 = d_solver.mkConst(s6, "_x346");
+  Term t879 = d_solver.mkTerm(APPLY_UPDATER,
+                              t843.getSort()
+                                  .getDatatype()
+                                  .getConstructor("_x8")
+                                  .getSelector("_x7")
+                                  .getUpdaterTerm(),
+                              t843,
+                              t317);
+  ASSERT_EQ(t879.getSort(), s6);
+}
+
 TEST_F(TestApiBlackSolver, getDatatypeArity)
 {
   DatatypeConstructorDecl ctor1 = d_solver.mkDatatypeConstructorDecl("_x21");
@@ -2678,5 +2749,6 @@ TEST_F(TestApiBlackSolver, getDatatypeArity)
   Sort s3 = d_solver.declareDatatype(std::string("_x17"), {ctor1, ctor2});
   ASSERT_EQ(s3.getDatatypeArity(), 0);
 }
+
 }  // namespace test
 }  // namespace cvc5