From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 31 Mar 2022 18:28:16 +0000 (-0500)
Subject: Do not export dt.size (#8483)
X-Git-Tag: cvc5-1.0.0~89
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fa0068aa7b53e4cd87b274dbbeed27ebc403e949;p=cvc5.git

Do not export dt.size (#8483)

This kind is hardcoded only to work for sygus. I am not sure we want to support general constraints over it, or even if the token dt.size is the appropriate one.

Also adds a missing experimental warning that I had missed.

Fixes cvc5/cvc5-projects#504.
---

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 1d1e0f5ec..1bb4d8c26 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -273,7 +273,6 @@ const static std::unordered_map<Kind, std::pair<internal::Kind, std::string>>
         KIND_ENUM(APPLY_CONSTRUCTOR, internal::Kind::APPLY_CONSTRUCTOR),
         KIND_ENUM(APPLY_TESTER, internal::Kind::APPLY_TESTER),
         KIND_ENUM(APPLY_UPDATER, internal::Kind::APPLY_UPDATER),
-        KIND_ENUM(DT_SIZE, internal::Kind::DT_SIZE),
         KIND_ENUM(MATCH, internal::Kind::MATCH),
         KIND_ENUM(MATCH_CASE, internal::Kind::MATCH_CASE),
         KIND_ENUM(MATCH_BIND_CASE, internal::Kind::MATCH_BIND_CASE),
@@ -589,7 +588,6 @@ const static std::unordered_map<internal::Kind,
         {internal::Kind::APPLY_CONSTRUCTOR, APPLY_CONSTRUCTOR},
         {internal::Kind::APPLY_TESTER, APPLY_TESTER},
         {internal::Kind::APPLY_UPDATER, APPLY_UPDATER},
-        {internal::Kind::DT_SIZE, DT_SIZE},
         {internal::Kind::MATCH, MATCH},
         {internal::Kind::MATCH_CASE, MATCH_CASE},
         {internal::Kind::MATCH_BIND_CASE, MATCH_BIND_CASE},
diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h
index 50b44d0f4..1506321b9 100644
--- a/src/api/cpp/cvc5_kind.h
+++ b/src/api/cpp/cvc5_kind.h
@@ -343,6 +343,11 @@ enum Kind : int32_t
    * - Arity: `0`
    * - Create Term of this Kind with:
    *   - Solver::mkCardinalityConstraint(const Sort&, uint32_t) const
+   *
+   * \rst
+   * .. warning:: This kind is experimental and may be changed or removed in
+   *              future versions.
+   * \endrst
    */
   CARDINALITY_CONSTRAINT,
   /**
@@ -2257,23 +2262,6 @@ enum Kind : int32_t
    *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
    */
   MATCH_BIND_CASE,
-  /**
-   * Datatypes size operator.
-   *
-   * An operator mapping a datatype term to an integer denoting the number of
-   * non-nullary applications of constructors it contains.
-   *
-   * - Arity: `1`
-   *   - `1:` Term of datatype Sort
-   *
-   * - Create Term of this Kind with:
-   *   - Solver::mkTerm(Kind, const std::vector<Term>&) const
-   *   - Solver::mkTerm(const Op&, const std::vector<Term>&) const
-   *
-   * - Create Op of this kind with:
-   *   - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
-   */
-  DT_SIZE,
   /**
    * Tuple projection.
    *
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 3538f40d3..b27d477c9 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -132,7 +132,6 @@ void Smt2::addDatatypesOperators()
   if (!strictModeEnabled())
   {
     Parser::addOperator(cvc5::APPLY_UPDATER);
-    addOperator(cvc5::DT_SIZE, "dt.size");
     // Notice that tuple operators, we use the generic APPLY_SELECTOR and
     // APPLY_UPDATER kinds. These are processed based on the context
     // in which they are parsed, e.g. when parsing identifiers.
diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index 6ae165883..b2c46cf17 100644
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -95,6 +95,7 @@ typerule APPLY_TYPE_ASCRIPTION ::cvc5::internal::theory::datatypes::DatatypeAscr
 # constructor applications are constant if they are applied only to constants
 construle APPLY_CONSTRUCTOR ::cvc5::internal::theory::datatypes::DatatypeConstructorTypeRule
 
+# the remaining kinds are used only by the sygus extension
 operator DT_SIZE 1 "datatypes size"
 typerule DT_SIZE ::cvc5::internal::theory::datatypes::DtSizeTypeRule
 
diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index 97129787c..651b432a7 100644
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -3159,7 +3159,8 @@ TEST_F(TestApiBlackSolver, proj_issue420)
   Sort s5 = slv.mkSequenceSort(s2);
   Term t3 = slv.mkConst(s5, "_x18");
   Term t7 = slv.mkConst(s4, "_x22");
-  Term t13 = slv.mkTerm(Kind::DT_SIZE, {t7});
+  // was initially a dt size application
+  Term t13 = slv.mkConst(slv.getIntegerSort(), "t13");
   Term t53 = slv.mkTerm(Kind::SEQ_NTH, {t3, t13});
   ASSERT_NO_THROW(slv.checkSat());
   ASSERT_NO_THROW(slv.blockModelValues({t53, t7}));