From: Andrew Reynolds Date: Wed, 8 Dec 2021 17:17:51 +0000 (-0600) Subject: Fix type rule for datatype updater for parametric sorts (#7762) X-Git-Tag: cvc5-1.0.0~702 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e7fd8a7af69c52dcbd4faf8e1132a85be578ae90;p=cvc5.git 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 d3c06d1f3..78bc67868 100644 --- 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 cb4160f58..b565895ba 100644 --- 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 index 000000000..0b4af0287 --- /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 23aec2386..c268ee4f8 100644 --- 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