api: Remove DatatypeConstructor::getSelectorTerm(). (#8535)

diff --git a/examples/api/cpp/datatypes.cpp b/examples/api/cpp/datatypes.cpp
index 6d201cc3b729375d386f873f911c4f42aacfc2ab..75e4a97d1256ec906b961d31319b06c4870acd41 100644 (file)
--- a/examples/api/cpp/datatypes.cpp
+++ b/examples/api/cpp/datatypes.cpp
@@ -56,7 +56,8 @@ void test(Solver& slv, Sort& consListSort)
   // consList["cons"]) in order to get the "head" selector symbol
   // to apply.
   Term t2 =
-      slv.mkTerm(APPLY_SELECTOR, {consList["cons"].getSelectorTerm("head"), t});
+      slv.mkTerm(APPLY_SELECTOR,
+                 {consList["cons"].getSelector("head").getSelectorTerm(), t});
 
   std::cout << "t2 is " << t2 << std::endl
             << "simplify(t2) is " << slv.simplify(t2) << std::endl
@@ -131,8 +132,9 @@ void test(Solver& slv, Sort& consListSort)
   Term a = slv.mkConst(paramConsIntListSort, "a");
   std::cout << "term " << a << " is of sort " << a.getSort() << std::endl;
 
-  Term head_a = slv.mkTerm(APPLY_SELECTOR,
-                           {paramConsList["cons"].getSelectorTerm("head"), a});
+  Term head_a = slv.mkTerm(
+      APPLY_SELECTOR,
+      {paramConsList["cons"].getSelector("head").getSelectorTerm(), a});
   std::cout
       << "head_a is " << head_a << " of sort " << head_a.getSort() << std::endl
       << "sort of cons is "

diff --git a/examples/api/java/Datatypes.java b/examples/api/java/Datatypes.java
index c60ca79087c52f7a4d95ce5f63d847cfbdbd50b3..0f70ce0dcf6bdea0dd1855bec7ba82af3e934f36 100644 (file)
--- a/examples/api/java/Datatypes.java
+++ b/examples/api/java/Datatypes.java
@@ -48,8 +48,9 @@ public class Datatypes
     // Here we first get the DatatypeConstructor for cons (with
     // consList["cons"]) in order to get the "head" selector symbol
     // to apply.
-    Term t2 =
-        slv.mkTerm(Kind.APPLY_SELECTOR, consList.getConstructor("cons").getSelectorTerm("head"), t);
+    Term t2 = slv.mkTerm(Kind.APPLY_SELECTOR,
+        consList.getConstructor("cons").getSelector("head").getSelectorTerm(),
+        t);
 
     System.out.println("t2 is " + t2 + "\n"
         + "simplify(t2) is " + slv.simplify(t2) + "\n");
@@ -123,8 +124,9 @@ public class Datatypes
     Term a = slv.mkConst(paramConsIntListSort, "a");
     System.out.println("term " + a + " is of sort " + a.getSort());
 
-    Term head_a = slv.mkTerm(
-        Kind.APPLY_SELECTOR, paramConsList.getConstructor("cons").getSelectorTerm("head"), a);
+    Term head_a = slv.mkTerm(Kind.APPLY_SELECTOR,
+        paramConsList.getConstructor("cons").getSelector("head").getSelectorTerm(),
+        a);
     System.out.println("head_a is " + head_a + " of sort " + head_a.getSort() + "\n"
         + "sort of cons is " + paramConsList.getConstructor("cons").getConstructorTerm().getSort()
         + "\n");

diff --git a/examples/api/python/datatypes.py b/examples/api/python/datatypes.py
index 85cecc9e4f089d1bd6fd14cc8e008d0421a79aeb..39642297cafd9ba598967ca9125062cd281f7738 100644 (file)
--- a/examples/api/python/datatypes.py
+++ b/examples/api/python/datatypes.py
@@ -38,8 +38,9 @@ def test(slv, consListSort):
             Kind.APPLY_CONSTRUCTOR,
             consList.getConstructor("cons").getConstructorTerm(),
             slv.mkInteger(0),
-            slv.mkTerm(Kind.APPLY_CONSTRUCTOR,
-            consList.getConstructor("nil").getConstructorTerm()))
+            slv.mkTerm(
+                Kind.APPLY_CONSTRUCTOR,
+                consList.getConstructor("nil").getConstructorTerm()))
 
     print("t is {}\nsort of cons is {}\n sort of nil is {}".format(
         t,
@@ -53,7 +54,9 @@ def test(slv, consListSort):
     # to apply.
 
     t2 = slv.mkTerm(
-            Kind.APPLY_SELECTOR, consList["cons"].getSelectorTerm("head"), t)
+            Kind.APPLY_SELECTOR,
+            consList["cons"].getSelector("head").getSelectorTerm(),
+            t)
 
     print("t2 is {}\nsimplify(t2) is {}\n\n".format(t2, slv.simplify(t2)))
 
@@ -99,7 +102,7 @@ def test(slv, consListSort):
 
     head_a = slv.mkTerm(
             Kind.APPLY_SELECTOR,
-            paramConsList["cons"].getSelectorTerm("head"),
+            paramConsList["cons"].getSelector("head").getSelectorTerm(),
             a)
     print("head_a is {} of sort {}".format(head_a, head_a.getSort()))
     print("sort of cons is",

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 89cd72f3f02d731134150c36fcad13126eadcbc7..26da68abca26f3e94b3eb813e7890b0a1560fc8d 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -3762,16 +3762,6 @@ DatatypeSelector DatatypeConstructor::getSelector(const std::string& name) const
   CVC5_API_TRY_CATCH_END;
 }
 
-Term DatatypeConstructor::getSelectorTerm(const std::string& name) const
-{
-  CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_CHECK_NOT_NULL;
-  //////// all checks before this line
-  return getSelector(name).getSelectorTerm();
-  ////////
-  CVC5_API_TRY_CATCH_END;
-}
-
 DatatypeConstructor::const_iterator DatatypeConstructor::begin() const
 {
   return DatatypeConstructor::const_iterator(d_solver, *d_ctor, true);

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 3470884e1cdc500880b8dc5de3a7c7f96d4333dc..7bf71accdb19d89e601f9bcd32d0bdb21b8d62d2 100644 (file)
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -2155,16 +2155,14 @@ class CVC5_EXPORT DatatypeConstructor
    * @return the first datatype selector with the given name
    */
   DatatypeSelector operator[](const std::string& name) const;
-  DatatypeSelector getSelector(const std::string& name) const;
-
   /**
-   * Get the term representation of the datatype selector with the given name.
-   * This is a linear search through the arguments, so in case of multiple,
-   * similarly-named arguments, the selector for the first is returned.
+   * Get the datatype selector with the given name.
+   * This is a linear search through the selectors, so in case of
+   * multiple, similarly-named selectors, the first is returned.
    * @param name the name of the datatype selector
-   * @return a term representing the datatype selector with the given name
+   * @return the first datatype selector with the given name
    */
-  Term getSelectorTerm(const std::string& name) const;
+  DatatypeSelector getSelector(const std::string& name) const;
 
   /**
    * @return true if this DatatypeConstructor is a null object

diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h
index 464415372e326fefe7cf3f804c3a7e3c02e03826..1d5c2da90c25d062163c56ff8b4cf157e9d1c97b 100644 (file)
--- a/src/api/cpp/cvc5_kind.h
+++ b/src/api/cpp/cvc5_kind.h
@@ -2555,7 +2555,7 @@ enum Kind : int32_t
    *
    * - Arity: ``2``
    *
-   *   - ``1:`` DatatypeSelector Term (see DatatypeSelector::getSelectorTerm() const, DatatypeConstructor::getSelectorTerm(const std::string&) const)
+   *   - ``1:`` DatatypeSelector Term (see DatatypeSelector::getSelectorTerm() const)
    *   - ``2:`` Term of the codomain Sort of the selector
    *
    * - Create Term of this Kind with:

diff --git a/src/api/java/io/github/cvc5/DatatypeConstructor.java b/src/api/java/io/github/cvc5/DatatypeConstructor.java
index 80832894673dc39c26fed5bb090ad2872388faf8..e3e482feef4c7cbc0fb132f903aca0a92d44399d 100644 (file)
--- a/src/api/java/io/github/cvc5/DatatypeConstructor.java
+++ b/src/api/java/io/github/cvc5/DatatypeConstructor.java
@@ -137,20 +137,6 @@ public class DatatypeConstructor extends AbstractPointer implements Iterable<Dat
   }
   private native long getSelector(long pointer, String name);
 
-  /**
-   * Get the term representation of the datatype selector with the given name.
-   * This is a linear search through the arguments, so in case of multiple,
-   * similarly-named arguments, the selector for the first is returned.
-   * @param name the name of the datatype selector
-   * @return a term representing the datatype selector with the given name
-   */
-  public Term getSelectorTerm(String name)
-  {
-    long termPointer = getSelectorTerm(pointer, name);
-    return new Term(solver, termPointer);
-  }
-  private native long getSelectorTerm(long pointer, String name);
-
   /**
    * @return true if this DatatypeConstructor is a null object
    */

diff --git a/src/api/java/jni/datatype_constructor.cpp b/src/api/java/jni/datatype_constructor.cpp
index c39793bac331a6a23d6a3d8dcb045e461d1d64e1..1631674fe8092c7b425b9750662bba35841730b9 100644 (file)
--- a/src/api/java/jni/datatype_constructor.cpp
+++ b/src/api/java/jni/datatype_constructor.cpp
@@ -152,27 +152,6 @@ Java_io_github_cvc5_DatatypeConstructor_getSelector__JLjava_lang_String_2(
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 }
 
-/*
- * Class:     io_github_cvc5_DatatypeConstructor
- * Method:    getSelectorTerm
- * Signature: (JLjava/lang/String;)J
- */
-JNIEXPORT jlong JNICALL
-Java_io_github_cvc5_DatatypeConstructor_getSelectorTerm(JNIEnv* env,
-                                                            jobject,
-                                                            jlong pointer,
-                                                            jstring jName)
-{
-  CVC5_JAVA_API_TRY_CATCH_BEGIN;
-  DatatypeConstructor* current = (DatatypeConstructor*)pointer;
-  const char* s = env->GetStringUTFChars(jName, nullptr);
-  std::string cName(s);
-  Term* retPointer = new Term(current->getSelectorTerm(cName));
-  env->ReleaseStringUTFChars(jName, s);
-  return (jlong)retPointer;
-  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
-}
-
 /*
  * Class:     io_github_cvc5_DatatypeConstructor
  * Method:    isNull

diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index 7f5bf10efc97403f3c9a61d5e67d52ff54ad7673..65bb821f9edbf6682d5952e723aacf509a22a06a 100644 (file)
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -90,7 +90,6 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5":
         Term getTesterTerm() except +
         size_t getNumSelectors() except +
         DatatypeSelector getSelector(const string& name) except +
-        Term getSelectorTerm(const string& name) except +
         bint isNull() except +
         string toString() except +
         cppclass const_iterator:

diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index f39b9cf0426dcbc223a38d3373ece7938c5be72f..8fc4904e7dcf15c676289d08e931ec4788bb183f 100644 (file)
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -333,16 +333,6 @@ cdef class DatatypeConstructor:
         ds.cds = self.cdc.getSelector(name.encode())
         return ds
 
-    def getSelectorTerm(self, str name):
-        """
-            :param name: The name of the datatype selector.
-            :return: A term representing the firstdatatype selector with the
-                     given name.
-        """
-        cdef Term term = Term(self.solver)
-        term.cterm = self.cdc.getSelectorTerm(name.encode())
-        return term
-
     def isNull(self):
         """
             :return: True if this DatatypeConstructor is a null object.

diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index cf048ce4f1549d6e5a233e3664032b58bb1fa1f0..7461a879eeeffd8dbc78d8b53d6425c4fb33b937 100644 (file)
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -854,10 +854,8 @@ TEST_F(TestApiBlackSolver, mkTermFromOp)
   // list datatype constructor and selector operator terms
   Term consTerm = list.getConstructor("cons").getConstructorTerm();
   Term nilTerm = list.getConstructor("nil").getConstructorTerm();
-  Term headTerm1 = list["cons"].getSelectorTerm("head");
-  Term headTerm2 = list["cons"].getSelector("head").getSelectorTerm();
-  Term tailTerm1 = list["cons"].getSelectorTerm("tail");
-  Term tailTerm2 = list["cons"]["tail"].getSelectorTerm();
+  Term headTerm = list["cons"].getSelector("head").getSelectorTerm();
+  Term tailTerm = list["cons"]["tail"].getSelectorTerm();
 
   // mkTerm(Op op, Term term) const
   ASSERT_NO_THROW(d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilTerm}));
@@ -866,15 +864,15 @@ TEST_F(TestApiBlackSolver, mkTermFromOp)
   ASSERT_THROW(d_solver.mkTerm(APPLY_CONSTRUCTOR, {consTerm}),
                CVC5ApiException);
   ASSERT_THROW(d_solver.mkTerm(opterm1), CVC5ApiException);
-  ASSERT_THROW(d_solver.mkTerm(APPLY_SELECTOR, {headTerm1}), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkTerm(APPLY_SELECTOR, {headTerm}), CVC5ApiException);
   ASSERT_THROW(d_solver.mkTerm(opterm1), CVC5ApiException);
   ASSERT_THROW(slv.mkTerm(APPLY_CONSTRUCTOR, {nilTerm}), CVC5ApiException);
 
   // mkTerm(Op op, Term child) const
   ASSERT_NO_THROW(d_solver.mkTerm(opterm1, {a}));
   ASSERT_NO_THROW(d_solver.mkTerm(opterm2, {d_solver.mkInteger(1)}));
-  ASSERT_NO_THROW(d_solver.mkTerm(APPLY_SELECTOR, {headTerm1, c}));
-  ASSERT_NO_THROW(d_solver.mkTerm(APPLY_SELECTOR, {tailTerm2, c}));
+  ASSERT_NO_THROW(d_solver.mkTerm(APPLY_SELECTOR, {headTerm, c}));
+  ASSERT_NO_THROW(d_solver.mkTerm(APPLY_SELECTOR, {tailTerm, c}));
   ASSERT_THROW(d_solver.mkTerm(opterm2, {a}), CVC5ApiException);
   ASSERT_THROW(d_solver.mkTerm(opterm1, {Term()}), CVC5ApiException);
   ASSERT_THROW(
@@ -1502,7 +1500,7 @@ TEST_F(TestApiBlackSolver, getOp)
 
   Term consTerm = consList.getConstructor("cons").getConstructorTerm();
   Term nilTerm = consList.getConstructor("nil").getConstructorTerm();
-  Term headTerm = consList["cons"].getSelectorTerm("head");
+  Term headTerm = consList["cons"].getSelector("head").getSelectorTerm();
 
   Term listnil = d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilTerm});
   Term listcons1 = d_solver.mkTerm(APPLY_CONSTRUCTOR,
@@ -2371,8 +2369,9 @@ TEST_F(TestApiBlackSolver, simplify)
        d_solver.mkTerm(APPLY_CONSTRUCTOR,
                        {consList.getConstructor("nil").getConstructorTerm()})});
   ASSERT_NO_THROW(d_solver.simplify(dt1));
-  Term dt2 = d_solver.mkTerm(APPLY_SELECTOR,
-                             {consList["cons"].getSelectorTerm("head"), dt1});
+  Term dt2 = d_solver.mkTerm(
+      APPLY_SELECTOR,
+      {consList["cons"].getSelector("head").getSelectorTerm(), dt1});
   ASSERT_NO_THROW(d_solver.simplify(dt2));
 
   Term b1 = d_solver.mkVar(bvSort, "b1");
@@ -2974,11 +2973,13 @@ TEST_F(TestApiBlackSolver, proj_issue378)
   Term t1507 = d_solver.mkTerm(
       APPLY_CONSTRUCTOR,
       {s9.getDatatype().getConstructor("_x184").getConstructorTerm(), t7});
-  ASSERT_NO_THROW(d_solver.mkTerm(
-      APPLY_UPDATER,
-      {s9.getDatatype().getConstructor("_x186").getSelectorTerm("_x185"),
-       t1507,
-       t7}));
+  ASSERT_NO_THROW(d_solver.mkTerm(APPLY_UPDATER,
+                                  {s9.getDatatype()
+                                       .getConstructor("_x186")
+                                       .getSelector("_x185")
+                                       .getSelectorTerm(),
+                                   t1507,
+                                   t7}));
 }
 
 TEST_F(TestApiBlackSolver, proj_issue379)
@@ -3342,9 +3343,11 @@ TEST_F(TestApiBlackSolver, projIssue431)
   Sort s14 = slv.mkDatatypeSorts({_dt46})[0];
   Term t31 = slv.mkConst(s7, "_x100");
   Term t47 = slv.mkConst(s14, "_x112");
-  Term sel =
-      t47.getSort().getDatatype().getConstructor("_cons64").getSelectorTerm(
-          "_sel62");
+  Term sel = t47.getSort()
+                 .getDatatype()
+                 .getConstructor("_cons64")
+                 .getSelector("_sel62")
+                 .getSelectorTerm();
   Term t274 = slv.mkTerm(APPLY_SELECTOR, {sel, t47});
   Term t488 = slv.mkTerm(Kind::APPLY_UF, {t31, t274});
   slv.assertFormula({t488});

diff --git a/test/unit/api/cpp/solver_white.cpp b/test/unit/api/cpp/solver_white.cpp
index 037f686b0426c766d3bbd2757528c5af6ee5786b..ab2b878311d7b0f16cd34ab992ec917b705ded8b 100644 (file)
--- a/test/unit/api/cpp/solver_white.cpp
+++ b/test/unit/api/cpp/solver_white.cpp
@@ -38,7 +38,7 @@ TEST_F(TestApiWhiteSolver, getOp)
 
   Term nilTerm = consList.getConstructor("nil").getConstructorTerm();
   Term consTerm = consList.getConstructor("cons").getConstructorTerm();
-  Term headTerm = consList["cons"].getSelectorTerm("head");
+  Term headTerm = consList["cons"].getSelector("head").getSelectorTerm();
 
   Term listnil = d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilTerm});
   Term listcons1 = d_solver.mkTerm(APPLY_CONSTRUCTOR,

diff --git a/test/unit/api/cpp/term_black.cpp b/test/unit/api/cpp/term_black.cpp
index 82417abe40e04c91f66538c6c30932975e93f442..c1034cf1d0cb43477273854c6fa08d6b2ce69f71 100644 (file)
--- a/test/unit/api/cpp/term_black.cpp
+++ b/test/unit/api/cpp/term_black.cpp
@@ -190,8 +190,8 @@ TEST_F(TestApiBlackTerm, getOp)
   // list datatype constructor and selector operator terms
   Term consOpTerm = list.getConstructor("cons").getConstructorTerm();
   Term nilOpTerm = list.getConstructor("nil").getConstructorTerm();
-  Term headOpTerm = list["cons"].getSelectorTerm("head");
-  Term tailOpTerm = list["cons"].getSelectorTerm("tail");
+  Term headOpTerm = list["cons"].getSelector("head").getSelectorTerm();
+  Term tailOpTerm = list["cons"].getSelector("tail").getSelectorTerm();
 
   Term nilTerm = d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilOpTerm});
   Term consTerm = d_solver.mkTerm(APPLY_CONSTRUCTOR,

diff --git a/test/unit/api/cpp/term_white.cpp b/test/unit/api/cpp/term_white.cpp
index 8f79e1bb68b7de5756df74379262b5303ba27017..470dd4db80ef261d687bf254a80f31099ee00e62 100644 (file)
--- a/test/unit/api/cpp/term_white.cpp
+++ b/test/unit/api/cpp/term_white.cpp
@@ -65,8 +65,8 @@ TEST_F(TestApiWhiteTerm, getOp)
   // list datatype constructor and selector operator terms
   Term consOpTerm = list.getConstructor("cons").getConstructorTerm();
   Term nilOpTerm = list.getConstructor("nil").getConstructorTerm();
-  Term headOpTerm = list["cons"].getSelectorTerm("head");
-  Term tailOpTerm = list["cons"].getSelectorTerm("tail");
+  Term headOpTerm = list["cons"].getSelector("head").getSelectorTerm();
+  Term tailOpTerm = list["cons"].getSelector("tail").getSelectorTerm();
 
   Term nilTerm = d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilOpTerm});
   Term consTerm = d_solver.mkTerm(APPLY_CONSTRUCTOR,

diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java
index 4d5c35472327c442e58672ab249724c3c555b93c..0865d604571918858c4cb22d02580132241745d2 100644 (file)
--- a/test/unit/api/java/SolverTest.java
+++ b/test/unit/api/java/SolverTest.java
@@ -836,10 +836,8 @@ class SolverTest
     // list datatype constructor and selector operator terms
     Term consTerm = list.getConstructor("cons").getConstructorTerm();
     Term nilTerm = list.getConstructor("nil").getConstructorTerm();
-    Term headTerm1 = list.getConstructor("cons").getSelectorTerm("head");
-    Term headTerm2 = list.getConstructor("cons").getSelector("head").getSelectorTerm();
-    Term tailTerm1 = list.getConstructor("cons").getSelectorTerm("tail");
-    Term tailTerm2 = list.getConstructor("cons").getSelector("tail").getSelectorTerm();
+    Term headTerm = list.getConstructor("cons").getSelector("head").getSelectorTerm();
+    Term tailTerm = list.getConstructor("cons").getSelector("tail").getSelectorTerm();
 
     // mkTerm(Op op, Term term) const
     assertDoesNotThrow(() -> d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm));
@@ -847,15 +845,15 @@ class SolverTest
     assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(APPLY_SELECTOR, consTerm));
     assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(APPLY_CONSTRUCTOR, consTerm));
     assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(opterm1));
-    assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(APPLY_SELECTOR, headTerm1));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(APPLY_SELECTOR, headTerm));
     assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(opterm1));
     assertThrows(CVC5ApiException.class, () -> slv.mkTerm(APPLY_CONSTRUCTOR, nilTerm));
 
     // mkTerm(Op op, Term child) const
     assertDoesNotThrow(() -> d_solver.mkTerm(opterm1, a));
     assertDoesNotThrow(() -> d_solver.mkTerm(opterm2, d_solver.mkInteger(1)));
-    assertDoesNotThrow(() -> d_solver.mkTerm(APPLY_SELECTOR, headTerm1, c));
-    assertDoesNotThrow(() -> d_solver.mkTerm(APPLY_SELECTOR, tailTerm2, c));
+    assertDoesNotThrow(() -> d_solver.mkTerm(APPLY_SELECTOR, headTerm, c));
+    assertDoesNotThrow(() -> d_solver.mkTerm(APPLY_SELECTOR, tailTerm, c));
     assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(opterm2, a));
     assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(opterm1, d_solver.getNullTerm()));
     assertThrows(CVC5ApiException.class,
@@ -1545,7 +1543,7 @@ class SolverTest
 
     Term consTerm = consList.getConstructor("cons").getConstructorTerm();
     Term nilTerm = consList.getConstructor("nil").getConstructorTerm();
-    Term headTerm = consList.getConstructor("cons").getSelectorTerm("head");
+    Term headTerm = consList.getConstructor("cons").getSelector("head").getSelectorTerm();
 
     Term listnil = d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm);
     Term listcons1 = d_solver.mkTerm(APPLY_CONSTRUCTOR, consTerm, d_solver.mkInteger(1), listnil);
@@ -2421,7 +2419,7 @@ class SolverTest
         d_solver.mkTerm(APPLY_CONSTRUCTOR, consList.getConstructor("nil").getConstructorTerm()));
     assertDoesNotThrow(() -> d_solver.simplify(dt1));
     Term dt2 = d_solver.mkTerm(
-        APPLY_SELECTOR, consList.getConstructor("cons").getSelectorTerm("head"), dt1);
+        APPLY_SELECTOR, consList.getConstructor("cons").getSelector("head").getSelectorTerm(), dt1);
     assertDoesNotThrow(() -> d_solver.simplify(dt2));
 
     Term b1 = d_solver.mkVar(bvSort, "b1");

diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py
index 4520701c536f3f837622d836f4f274d103d6f37e..fb09cdee24dfb74d6a383cac3f98801d64ab66a2 100644 (file)
--- a/test/unit/api/python/test_solver.py
+++ b/test/unit/api/python/test_solver.py
@@ -829,10 +829,8 @@ def test_mk_term_from_op(solver):
     # list datatype constructor and selector operator terms
     consTerm = lis.getConstructor("cons").getConstructorTerm()
     nilTerm = lis.getConstructor("nil").getConstructorTerm()
-    headTerm1 = lis["cons"].getSelectorTerm("head")
-    headTerm2 = lis["cons"].getSelector("head").getSelectorTerm()
-    tailTerm1 = lis["cons"].getSelectorTerm("tail")
-    tailTerm2 = lis["cons"]["tail"].getSelectorTerm()
+    headTerm = lis["cons"].getSelector("head").getSelectorTerm()
+    tailTerm = lis["cons"]["tail"].getSelectorTerm()
 
     # mkTerm(Op op, Term term) const
     solver.mkTerm(Kind.APPLY_CONSTRUCTOR, nilTerm)
@@ -846,7 +844,7 @@ def test_mk_term_from_op(solver):
     with pytest.raises(RuntimeError):
         solver.mkTerm(opterm1)
     with pytest.raises(RuntimeError):
-        solver.mkTerm(Kind.APPLY_SELECTOR, headTerm1)
+        solver.mkTerm(Kind.APPLY_SELECTOR, headTerm)
     with pytest.raises(RuntimeError):
         solver.mkTerm(opterm1)
     with pytest.raises(RuntimeError):
@@ -855,8 +853,8 @@ def test_mk_term_from_op(solver):
     # mkTerm(Op op, Term child) const
     solver.mkTerm(opterm1, a)
     solver.mkTerm(opterm2, solver.mkInteger(1))
-    solver.mkTerm(Kind.APPLY_SELECTOR, headTerm1, c)
-    solver.mkTerm(Kind.APPLY_SELECTOR, tailTerm2, c)
+    solver.mkTerm(Kind.APPLY_SELECTOR, headTerm, c)
+    solver.mkTerm(Kind.APPLY_SELECTOR, tailTerm, c)
     with pytest.raises(RuntimeError):
         solver.mkTerm(opterm2, a)
     with pytest.raises(RuntimeError):
@@ -1161,7 +1159,7 @@ def test_get_op(solver):
 
     consTerm = consList.getConstructor("cons").getConstructorTerm()
     nilTerm = consList.getConstructor("nil").getConstructorTerm()
-    headTerm = consList["cons"].getSelectorTerm("head")
+    headTerm = consList["cons"].getSelector("head").getSelectorTerm()
 
     listnil = solver.mkTerm(Kind.APPLY_CONSTRUCTOR, nilTerm)
     listcons1 = solver.mkTerm(Kind.APPLY_CONSTRUCTOR, consTerm,
@@ -1733,7 +1731,9 @@ def test_simplify(solver):
             consList.getConstructor("nil").getConstructorTerm()))
     solver.simplify(dt1)
     dt2 = solver.mkTerm(
-      Kind.APPLY_SELECTOR, consList["cons"].getSelectorTerm("head"), dt1)
+      Kind.APPLY_SELECTOR,
+      consList["cons"].getSelector("head").getSelectorTerm(),
+      dt1)
     solver.simplify(dt2)
 
     b1 = solver.mkVar(bvSort, "b1")

diff --git a/test/unit/api/python/test_term.py b/test/unit/api/python/test_term.py
index 5af769267179e8f6150ee72102506ef9e63b81cf..c070b00ec97f95f19af5cdb91eeac33a2187066e 100644 (file)
--- a/test/unit/api/python/test_term.py
+++ b/test/unit/api/python/test_term.py
@@ -189,8 +189,8 @@ def test_get_op(solver):
     # list datatype constructor and selector operator terms
     consOpTerm = list1.getConstructor("cons").getConstructorTerm()
     nilOpTerm = list1.getConstructor("nil").getConstructorTerm()
-    headOpTerm = list1["cons"].getSelectorTerm("head")
-    tailOpTerm = list1["cons"].getSelectorTerm("tail")
+    headOpTerm = list1["cons"].getSelector("head").getSelectorTerm()
+    tailOpTerm = list1["cons"].getSelector("tail").getSelectorTerm()
 
     nilTerm = solver.mkTerm(Kind.APPLY_CONSTRUCTOR, nilOpTerm)
     consTerm = solver.mkTerm(Kind.APPLY_CONSTRUCTOR, consOpTerm,