api: Remove Datatype::getConstructorTerm(). (#8529)

diff --git a/examples/api/cpp/datatypes.cpp b/examples/api/cpp/datatypes.cpp
index 08346568e47e300a523a9e5ae453ee451c581e0a..6d201cc3b729375d386f873f911c4f42aacfc2ab 100644 (file)
--- a/examples/api/cpp/datatypes.cpp
+++ b/examples/api/cpp/datatypes.cpp
@@ -37,14 +37,17 @@ void test(Solver& slv, Sort& consListSort)
   // APPLY_CONSTRUCTOR, even though it has no arguments.
   Term t = slv.mkTerm(
       APPLY_CONSTRUCTOR,
-      {consList.getConstructorTerm("cons"),
+      {consList.getConstructor("cons").getConstructorTerm(),
        slv.mkInteger(0),
-       slv.mkTerm(APPLY_CONSTRUCTOR, {consList.getConstructorTerm("nil")})});
+       slv.mkTerm(APPLY_CONSTRUCTOR,
+                  {consList.getConstructor("nil").getConstructorTerm()})});
 
   std::cout << "t is " << t << std::endl
             << "sort of cons is "
-            << consList.getConstructorTerm("cons").getSort() << std::endl
-            << "sort of nil is " << consList.getConstructorTerm("nil").getSort()
+            << consList.getConstructor("cons").getConstructorTerm().getSort()
+            << std::endl
+            << "sort of nil is "
+            << consList.getConstructor("nil").getConstructorTerm().getSort()
             << std::endl;
 
   // t2 = head(cons 0 nil), and of course this can be evaluated
@@ -130,11 +133,12 @@ void test(Solver& slv, Sort& consListSort)
 
   Term head_a = slv.mkTerm(APPLY_SELECTOR,
                            {paramConsList["cons"].getSelectorTerm("head"), a});
-  std::cout << "head_a is " << head_a << " of sort " << head_a.getSort()
-            << std::endl
-            << "sort of cons is "
-            << paramConsList.getConstructorTerm("cons").getSort() << std::endl
-            << std::endl;
+  std::cout
+      << "head_a is " << head_a << " of sort " << head_a.getSort() << std::endl
+      << "sort of cons is "
+      << paramConsList.getConstructor("cons").getConstructorTerm().getSort()
+      << std::endl
+      << std::endl;
 
   Term assertion = slv.mkTerm(GT, {head_a, slv.mkInteger(50)});
   std::cout << "Assert " << assertion << std::endl;

diff --git a/examples/api/java/Datatypes.java b/examples/api/java/Datatypes.java
index 35d6914f12c1e6dfbad4ae482054c20c34aa35bc..c60ca79087c52f7a4d95ce5f63d847cfbdbd50b3 100644 (file)
--- a/examples/api/java/Datatypes.java
+++ b/examples/api/java/Datatypes.java
@@ -35,13 +35,13 @@ public class Datatypes
     // "nil" is a constructor too, so it needs to be applied with
     // APPLY_CONSTRUCTOR, even though it has no arguments.
     Term t = slv.mkTerm(Kind.APPLY_CONSTRUCTOR,
-        consList.getConstructorTerm("cons"),
+        consList.getConstructor("cons").getConstructorTerm(),
         slv.mkInteger(0),
-        slv.mkTerm(Kind.APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil")));
+        slv.mkTerm(Kind.APPLY_CONSTRUCTOR, consList.getConstructor("nil").getConstructorTerm()));
 
     System.out.println("t is " + t + "\n"
-        + "sort of cons is " + consList.getConstructorTerm("cons").getSort() + "\n"
-        + "sort of nil is " + consList.getConstructorTerm("nil").getSort());
+        + "sort of cons is " + consList.getConstructor("cons").getConstructorTerm().getSort() + "\n"
+        + "sort of nil is " + consList.getConstructor("nil").getConstructorTerm().getSort());
 
     // t2 = head(cons 0 nil), and of course this can be evaluated
     //
@@ -126,7 +126,8 @@ public class Datatypes
     Term head_a = slv.mkTerm(
         Kind.APPLY_SELECTOR, paramConsList.getConstructor("cons").getSelectorTerm("head"), a);
     System.out.println("head_a is " + head_a + " of sort " + head_a.getSort() + "\n"
-        + "sort of cons is " + paramConsList.getConstructorTerm("cons").getSort() + "\n");
+        + "sort of cons is " + paramConsList.getConstructor("cons").getConstructorTerm().getSort()
+        + "\n");
     Term assertion = slv.mkTerm(Kind.GT, head_a, slv.mkInteger(50));
     System.out.println("Assert " + assertion);
     slv.assertFormula(assertion);

diff --git a/examples/api/python/datatypes.py b/examples/api/python/datatypes.py
index 23704fa7c1ca49c9564fc19a1810a983aaf7f482..85cecc9e4f089d1bd6fd14cc8e008d0421a79aeb 100644 (file)
--- a/examples/api/python/datatypes.py
+++ b/examples/api/python/datatypes.py
@@ -35,15 +35,16 @@ def test(slv, consListSort):
     # "nil" is a constructor too
 
     t = slv.mkTerm(
-            Kind.APPLY_CONSTRUCTOR, consList.getConstructorTerm("cons"),
+            Kind.APPLY_CONSTRUCTOR,
+            consList.getConstructor("cons").getConstructorTerm(),
             slv.mkInteger(0),
-            slv.mkTerm(
-                Kind.APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil")))
+            slv.mkTerm(Kind.APPLY_CONSTRUCTOR,
+            consList.getConstructor("nil").getConstructorTerm()))
 
     print("t is {}\nsort of cons is {}\n sort of nil is {}".format(
         t,
-        consList.getConstructorTerm("cons").getSort(),
-        consList.getConstructorTerm("nil").getSort()))
+        consList.getConstructor("cons").getConstructorTerm().getSort(),
+        consList.getConstructor("nil").getConstructorTerm().getSort()))
 
     # t2 = head(cons 0 nil), and of course this can be evaluated
     #
@@ -101,7 +102,8 @@ def test(slv, consListSort):
             paramConsList["cons"].getSelectorTerm("head"),
             a)
     print("head_a is {} of sort {}".format(head_a, head_a.getSort()))
-    print("sort of cons is", paramConsList.getConstructorTerm("cons").getSort())
+    print("sort of cons is",
+          paramConsList.getConstructor("cons").getConstructorTerm().getSort())
 
     assertion = slv.mkTerm(Kind.GT, head_a, slv.mkInteger(50))
     print("Assert", assertion)

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index beaa4887ae5a38f0b9cbeb1cc02e09b7b9584faf..b4cc4cab2b6b420f5f881dc8493726e1fdfb7a49 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -3943,16 +3943,6 @@ DatatypeConstructor Datatype::getConstructor(const std::string& name) const
   CVC5_API_TRY_CATCH_END;
 }
 
-Term Datatype::getConstructorTerm(const std::string& name) const
-{
-  CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_CHECK_NOT_NULL;
-  //////// all checks before this line
-  return getConstructorForName(name).getConstructorTerm();
-  ////////
-  CVC5_API_TRY_CATCH_END;
-}
-
 DatatypeSelector Datatype::getSelector(const std::string& name) const
 {
   CVC5_API_TRY_CATCH_BEGIN;

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 147700fe5fd67c8365a1fbcc886d4beb73efc220..65337fc51e097395f5b55b846d0d4ef1d6a6ab6e 100644 (file)
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -2283,16 +2283,6 @@ class CVC5_EXPORT Datatype
   DatatypeConstructor operator[](const std::string& name) const;
   DatatypeConstructor getConstructor(const std::string& name) const;
 
-  /**
-   * Get a term representing the datatype constructor with the given name.
-   * This is a linear search through the constructors, so in case of multiple,
-   * similarly-named constructors, the
-   * first is returned.
-   * @param name the name of the datatype constructor
-   * @return a Term representing the datatype constructor with the given name
-   */
-  Term getConstructorTerm(const std::string& name) const;
-
   /**
    * Get the datatype constructor with the given name.
    * This is a linear search through the constructors and their selectors, so

diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h
index 1506321b9222d798be9edb0f006916ec07064e5c..e8fe14a4bb790b55ed26aa250d4225318bed8a6e 100644 (file)
--- a/src/api/cpp/cvc5_kind.h
+++ b/src/api/cpp/cvc5_kind.h
@@ -2110,8 +2110,7 @@ enum Kind : int32_t
    *
    * - Arity: `n > 0`
    *   - `1:` DatatypeConstructor Term
-   *          (see DatatypeConstructor::getConstructorTerm() const,
-   *          Datatype::getConstructorTerm(const std::string&) const)
+   *          (see DatatypeConstructor::getConstructorTerm() const)
    *   - `2..n:` Terms of the Sorts of the selectors of the constructor (the arguments to the constructor)
    *
    * - Create Term of this Kind with:

diff --git a/src/api/java/io/github/cvc5/Datatype.java b/src/api/java/io/github/cvc5/Datatype.java
index cfe0614ef313ecdd60e2b77ef32f4928ec107ab3..06ceaa67fb4aa8d2d62e9146883dd0c7a6fad827 100644 (file)
--- a/src/api/java/io/github/cvc5/Datatype.java
+++ b/src/api/java/io/github/cvc5/Datatype.java
@@ -63,22 +63,6 @@ public class Datatype extends AbstractPointer implements Iterable<DatatypeConstr
 
   private native long getConstructor(long pointer, String name);
 
-  /**
-   * Get a term representing the datatype constructor with the given name.
-   * This is a linear search through the constructors, so in case of multiple,
-   * similarly-named constructors, the
-   * first is returned.
-   * @param name the name of the datatype constructor
-   * @return a Term representing the datatype constructor with the given name
-   */
-  public Term getConstructorTerm(String name)
-  {
-    long termPointer = getConstructorTerm(pointer, name);
-    return new Term(solver, termPointer);
-  }
-
-  private native long getConstructorTerm(long pointer, String name);
-
   /**
    * Get the datatype constructor with the given name.
    * This is a linear search through the constructors and their selectors, so

diff --git a/src/api/java/jni/datatype.cpp b/src/api/java/jni/datatype.cpp
index e6ba593f692220ecbd0803e07333f05fe6207a56..4af77bb4a0670aa57cfca8c75e159e95010409fa 100644 (file)
--- a/src/api/java/jni/datatype.cpp
+++ b/src/api/java/jni/datatype.cpp
@@ -66,24 +66,6 @@ Java_io_github_cvc5_Datatype_getConstructor__JLjava_lang_String_2(
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 }
 
-/*
- * Class:     io_github_cvc5_Datatype
- * Method:    getConstructorTerm
- * Signature: (JLjava/lang/String;)J
- */
-JNIEXPORT jlong JNICALL Java_io_github_cvc5_Datatype_getConstructorTerm(
-    JNIEnv* env, jobject, jlong pointer, jstring jName)
-{
-  CVC5_JAVA_API_TRY_CATCH_BEGIN;
-  Datatype* current = (Datatype*)pointer;
-  const char* s = env->GetStringUTFChars(jName, nullptr);
-  std::string cName(s);
-  Term* retPointer = new Term(current->getConstructorTerm(cName));
-  env->ReleaseStringUTFChars(jName, s);
-  return ((jlong)retPointer);
-  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
-}
-
 /*
  * Class:     io_github_cvc5_Datatype
  * Method:    getName

diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index bfde85399fe9cbdd234d937fb9775a1d302c48d8..b823816caadf33a2305d63a2ec395416e0a00e2a 100644 (file)
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -58,7 +58,6 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5":
         DatatypeConstructor operator[](size_t idx) except +
         DatatypeConstructor operator[](const string& name) except +
         DatatypeConstructor getConstructor(const string& name) except +
-        Term getConstructorTerm(const string& name) except +
         DatatypeSelector getSelector(const string& name) except +
         string getName() except +
         size_t getNumConstructors() except +

diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 62b45de7397360e179f8154f232f0741202599df..524f067ce089995c655d4827643c83b3cb6d2375 100644 (file)
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -120,16 +120,6 @@ cdef class Datatype:
         dc.cdc = self.cd.getConstructor(name.encode())
         return dc
 
-    def getConstructorTerm(self, str name):
-        """
-            :param name: The name of the constructor.
-            :return: The term representing the datatype constructor with the
-                     given name.
-        """
-        cdef Term term = Term(self.solver)
-        term.cterm = self.cd.getConstructorTerm(name.encode())
-        return term
-
     def getSelector(self, str name):
         """
             :param name: The name of the selector..

diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index 204d270a0d3dbccb298b4e7c5b141a6ca295e239..3cec83f816add70ffe2c14dce05d2f5ff2dc9bf5 100644 (file)
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -854,26 +854,23 @@ TEST_F(TestApiBlackSolver, mkTermFromOp)
   Datatype list = listSort.getDatatype();
 
   // list datatype constructor and selector operator terms
-  Term consTerm1 = list.getConstructorTerm("cons");
-  Term consTerm2 = list.getConstructor("cons").getConstructorTerm();
-  Term nilTerm1 = list.getConstructorTerm("nil");
-  Term nilTerm2 = list.getConstructor("nil").getConstructorTerm();
+  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();
 
   // mkTerm(Op op, Term term) const
-  ASSERT_NO_THROW(d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilTerm1}));
-  ASSERT_NO_THROW(d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilTerm2}));
-  ASSERT_THROW(d_solver.mkTerm(APPLY_SELECTOR, {nilTerm1}), CVC5ApiException);
-  ASSERT_THROW(d_solver.mkTerm(APPLY_SELECTOR, {consTerm1}), CVC5ApiException);
-  ASSERT_THROW(d_solver.mkTerm(APPLY_CONSTRUCTOR, {consTerm2}),
+  ASSERT_NO_THROW(d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilTerm}));
+  ASSERT_THROW(d_solver.mkTerm(APPLY_SELECTOR, {nilTerm}), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkTerm(APPLY_SELECTOR, {consTerm}), CVC5ApiException);
+  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(opterm1), CVC5ApiException);
-  ASSERT_THROW(slv.mkTerm(APPLY_CONSTRUCTOR, {nilTerm1}), CVC5ApiException);
+  ASSERT_THROW(slv.mkTerm(APPLY_CONSTRUCTOR, {nilTerm}), CVC5ApiException);
 
   // mkTerm(Op op, Term child) const
   ASSERT_NO_THROW(d_solver.mkTerm(opterm1, {a}));
@@ -883,16 +880,16 @@ TEST_F(TestApiBlackSolver, mkTermFromOp)
   ASSERT_THROW(d_solver.mkTerm(opterm2, {a}), CVC5ApiException);
   ASSERT_THROW(d_solver.mkTerm(opterm1, {Term()}), CVC5ApiException);
   ASSERT_THROW(
-      d_solver.mkTerm(APPLY_CONSTRUCTOR, {consTerm1, d_solver.mkInteger(0)}),
+      d_solver.mkTerm(APPLY_CONSTRUCTOR, {consTerm, d_solver.mkInteger(0)}),
       CVC5ApiException);
   ASSERT_THROW(slv.mkTerm(opterm1, {a}), CVC5ApiException);
 
   // mkTerm(Op op, Term child1, Term child2) const
   ASSERT_NO_THROW(
       d_solver.mkTerm(APPLY_CONSTRUCTOR,
-                      {consTerm1,
+                      {consTerm,
                        d_solver.mkInteger(0),
-                       d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilTerm1})}));
+                       d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilTerm})}));
   ASSERT_THROW(
       d_solver.mkTerm(opterm2, {d_solver.mkInteger(1), d_solver.mkInteger(2)}),
       CVC5ApiException);
@@ -902,9 +899,9 @@ TEST_F(TestApiBlackSolver, mkTermFromOp)
   ASSERT_THROW(d_solver.mkTerm(opterm2, {Term(), d_solver.mkInteger(1)}),
                CVC5ApiException);
   ASSERT_THROW(slv.mkTerm(APPLY_CONSTRUCTOR,
-                          {consTerm1,
+                          {consTerm,
                            d_solver.mkInteger(0),
-                           d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilTerm1})}),
+                           d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilTerm})}),
                CVC5ApiException);
 
   // mkTerm(Op op, Term child1, Term child2, Term child3) const
@@ -1505,8 +1502,8 @@ TEST_F(TestApiBlackSolver, getOp)
   Sort consListSort = d_solver.mkDatatypeSort(consListSpec);
   Datatype consList = consListSort.getDatatype();
 
-  Term consTerm = consList.getConstructorTerm("cons");
-  Term nilTerm = consList.getConstructorTerm("nil");
+  Term consTerm = consList.getConstructor("cons").getConstructorTerm();
+  Term nilTerm = consList.getConstructor("nil").getConstructorTerm();
   Term headTerm = consList["cons"].getSelectorTerm("head");
 
   Term listnil = d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilTerm});
@@ -2369,12 +2366,12 @@ TEST_F(TestApiBlackSolver, simplify)
   ASSERT_EQ(i1, d_solver.simplify(i3));
 
   Datatype consList = consListSort.getDatatype();
-  Term dt1 =
-      d_solver.mkTerm(APPLY_CONSTRUCTOR,
-                      {consList.getConstructorTerm("cons"),
-                       d_solver.mkInteger(0),
-                       d_solver.mkTerm(APPLY_CONSTRUCTOR,
-                                       {consList.getConstructorTerm("nil")})});
+  Term dt1 = d_solver.mkTerm(
+      APPLY_CONSTRUCTOR,
+      {consList.getConstructor("cons").getConstructorTerm(),
+       d_solver.mkInteger(0),
+       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});
@@ -2934,9 +2931,9 @@ TEST_F(TestApiBlackSolver, proj_issue373)
 
   Term t452 = d_solver.mkVar(s1, "_x281");
   Term bvl = d_solver.mkTerm(d_solver.mkOp(VARIABLE_LIST), {t452});
-  Term acons =
-      d_solver.mkTerm(d_solver.mkOp(APPLY_CONSTRUCTOR),
-                      {s4.getDatatype().getConstructorTerm("_x115"), t452});
+  Term acons = d_solver.mkTerm(
+      d_solver.mkOp(APPLY_CONSTRUCTOR),
+      {s4.getDatatype().getConstructor("_x115").getConstructorTerm(), t452});
   // type exception
   ASSERT_THROW(
       d_solver.mkTerm(d_solver.mkOp(APPLY_CONSTRUCTOR), {bvl, acons, t452}),
@@ -2977,7 +2974,8 @@ TEST_F(TestApiBlackSolver, proj_issue378)
   Sort s7 = d_solver.mkDatatypeSort(dtdecl);
   Sort s9 = s7.instantiate({s2});
   Term t1507 = d_solver.mkTerm(
-      APPLY_CONSTRUCTOR, {s9.getDatatype().getConstructorTerm("_x184"), t7});
+      APPLY_CONSTRUCTOR,
+      {s9.getDatatype().getConstructor("_x184").getConstructorTerm(), t7});
   ASSERT_NO_THROW(d_solver.mkTerm(
       APPLY_UPDATER,
       {s9.getDatatype().getConstructor("_x186").getSelectorTerm("_x185"),

diff --git a/test/unit/api/cpp/solver_white.cpp b/test/unit/api/cpp/solver_white.cpp
index 7699b9ae216fa40e7ae9762de3bfb6fd9b38cbd5..037f686b0426c766d3bbd2757528c5af6ee5786b 100644 (file)
--- a/test/unit/api/cpp/solver_white.cpp
+++ b/test/unit/api/cpp/solver_white.cpp
@@ -36,8 +36,8 @@ TEST_F(TestApiWhiteSolver, getOp)
   Sort consListSort = d_solver.mkDatatypeSort(consListSpec);
   Datatype consList = consListSort.getDatatype();
 
-  Term nilTerm = consList.getConstructorTerm("nil");
-  Term consTerm = consList.getConstructorTerm("cons");
+  Term nilTerm = consList.getConstructor("nil").getConstructorTerm();
+  Term consTerm = consList.getConstructor("cons").getConstructorTerm();
   Term headTerm = consList["cons"].getSelectorTerm("head");
 
   Term listnil = d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilTerm});

diff --git a/test/unit/api/cpp/term_black.cpp b/test/unit/api/cpp/term_black.cpp
index 45f53183bb4df4a6738b1c1296ad4c1d23e56d3b..82417abe40e04c91f66538c6c30932975e93f442 100644 (file)
--- a/test/unit/api/cpp/term_black.cpp
+++ b/test/unit/api/cpp/term_black.cpp
@@ -188,8 +188,8 @@ TEST_F(TestApiBlackTerm, getOp)
   Term c = d_solver.mkConst(intListSort, "c");
   Datatype list = listSort.getDatatype();
   // list datatype constructor and selector operator terms
-  Term consOpTerm = list.getConstructorTerm("cons");
-  Term nilOpTerm = list.getConstructorTerm("nil");
+  Term consOpTerm = list.getConstructor("cons").getConstructorTerm();
+  Term nilOpTerm = list.getConstructor("nil").getConstructorTerm();
   Term headOpTerm = list["cons"].getSelectorTerm("head");
   Term tailOpTerm = list["cons"].getSelectorTerm("tail");
 

diff --git a/test/unit/api/cpp/term_white.cpp b/test/unit/api/cpp/term_white.cpp
index 74f9baf1b6e9478d1d7a8ff9b841e694a022d6d3..8f79e1bb68b7de5756df74379262b5303ba27017 100644 (file)
--- a/test/unit/api/cpp/term_white.cpp
+++ b/test/unit/api/cpp/term_white.cpp
@@ -63,8 +63,8 @@ TEST_F(TestApiWhiteTerm, getOp)
   Term c = d_solver.mkConst(intListSort, "c");
   Datatype list = listSort.getDatatype();
   // list datatype constructor and selector operator terms
-  Term consOpTerm = list.getConstructorTerm("cons");
-  Term nilOpTerm = list.getConstructorTerm("nil");
+  Term consOpTerm = list.getConstructor("cons").getConstructorTerm();
+  Term nilOpTerm = list.getConstructor("nil").getConstructorTerm();
   Term headOpTerm = list["cons"].getSelectorTerm("head");
   Term tailOpTerm = list["cons"].getSelectorTerm("tail");
 

diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java
index 33ebd2ddb35835a143e7ee05e58bcf1546e1caa0..0f5f80e894ce8cab35f9ac31b090191a372d1483 100644 (file)
--- a/test/unit/api/java/SolverTest.java
+++ b/test/unit/api/java/SolverTest.java
@@ -838,25 +838,22 @@ class SolverTest
     Datatype list = listSort.getDatatype();
 
     // list datatype constructor and selector operator terms
-    Term consTerm1 = list.getConstructorTerm("cons");
-    Term consTerm2 = list.getConstructor("cons").getConstructorTerm();
-    Term nilTerm1 = list.getConstructorTerm("nil");
-    Term nilTerm2 = list.getConstructor("nil").getConstructorTerm();
+    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();
 
     // mkTerm(Op op, Term term) const
-    assertDoesNotThrow(() -> d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm1));
-    assertDoesNotThrow(() -> d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm2));
-    assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(APPLY_SELECTOR, nilTerm1));
-    assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(APPLY_SELECTOR, consTerm1));
-    assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(APPLY_CONSTRUCTOR, consTerm2));
+    assertDoesNotThrow(() -> d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(APPLY_SELECTOR, nilTerm));
+    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(opterm1));
-    assertThrows(CVC5ApiException.class, () -> slv.mkTerm(APPLY_CONSTRUCTOR, nilTerm1));
+    assertThrows(CVC5ApiException.class, () -> slv.mkTerm(APPLY_CONSTRUCTOR, nilTerm));
 
     // mkTerm(Op op, Term child) const
     assertDoesNotThrow(() -> d_solver.mkTerm(opterm1, a));
@@ -866,16 +863,16 @@ class SolverTest
     assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(opterm2, a));
     assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(opterm1, d_solver.getNullTerm()));
     assertThrows(CVC5ApiException.class,
-        () -> d_solver.mkTerm(APPLY_CONSTRUCTOR, consTerm1, d_solver.mkInteger(0)));
+        () -> d_solver.mkTerm(APPLY_CONSTRUCTOR, consTerm, d_solver.mkInteger(0)));
 
     assertThrows(CVC5ApiException.class, () -> slv.mkTerm(opterm1, a));
 
     // mkTerm(Op op, Term child1, Term child2) const
     assertDoesNotThrow(()
                            -> d_solver.mkTerm(APPLY_CONSTRUCTOR,
-                               consTerm1,
+                               consTerm,
                                d_solver.mkInteger(0),
-                               d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm1)));
+                               d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm)));
     assertThrows(CVC5ApiException.class,
         () -> d_solver.mkTerm(opterm2, d_solver.mkInteger(1), d_solver.mkInteger(2)));
 
@@ -889,9 +886,9 @@ class SolverTest
     assertThrows(CVC5ApiException.class,
         ()
             -> slv.mkTerm(APPLY_CONSTRUCTOR,
-                consTerm1,
+                consTerm,
                 d_solver.mkInteger(0),
-                d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm1)));
+                d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm)));
 
     // mkTerm(Op op, Term child1, Term child2, Term child3) const
     assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(opterm1, a, b, a));
@@ -1550,8 +1547,8 @@ class SolverTest
     Sort consListSort = d_solver.mkDatatypeSort(consListSpec);
     Datatype consList = consListSort.getDatatype();
 
-    Term consTerm = consList.getConstructorTerm("cons");
-    Term nilTerm = consList.getConstructorTerm("nil");
+    Term consTerm = consList.getConstructor("cons").getConstructorTerm();
+    Term nilTerm = consList.getConstructor("nil").getConstructorTerm();
     Term headTerm = consList.getConstructor("cons").getSelectorTerm("head");
 
     Term listnil = d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm);
@@ -2423,9 +2420,9 @@ class SolverTest
 
     Datatype consList = consListSort.getDatatype();
     Term dt1 = d_solver.mkTerm(APPLY_CONSTRUCTOR,
-        consList.getConstructorTerm("cons"),
+        consList.getConstructor("cons").getConstructorTerm(),
         d_solver.mkInteger(0),
-        d_solver.mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil")));
+        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);

diff --git a/test/unit/api/java/TermTest.java b/test/unit/api/java/TermTest.java
index 3725a7be09f1c54748555e62feb16c6e4cc998af..239e3262d48dc5c41eb3b2d1ee07bd4f6b34f2a0 100644 (file)
--- a/test/unit/api/java/TermTest.java
+++ b/test/unit/api/java/TermTest.java
@@ -222,8 +222,8 @@ class TermTest
     Term c = d_solver.mkConst(intListSort, "c");
     Datatype list = listSort.getDatatype();
     // list datatype constructor and selector operator terms
-    Term consOpTerm = list.getConstructorTerm("cons");
-    Term nilOpTerm = list.getConstructorTerm("nil");
+    Term consOpTerm = list.getConstructor("cons").getConstructorTerm();
+    Term nilOpTerm = list.getConstructor("nil").getConstructorTerm();
   }
 
   @Test

diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py
index c27cef850de494710f677206f729bc8d0c9840a6..ac8c8b0739779b2fdfb0ba4d0bea017593fd75aa 100644 (file)
--- a/test/unit/api/python/test_solver.py
+++ b/test/unit/api/python/test_solver.py
@@ -817,24 +817,22 @@ def test_mk_term_from_op(solver):
     lis = listSort.getDatatype()
 
     # list datatype constructor and selector operator terms
-    consTerm1 = lis.getConstructorTerm("cons")
-    consTerm2 = lis.getConstructor("cons").getConstructorTerm()
-    nilTerm1 = lis.getConstructorTerm("nil")
-    nilTerm2 = lis.getConstructor("nil").getConstructorTerm()
+    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()
 
     # mkTerm(Op op, Term term) const
-    solver.mkTerm(Kind.APPLY_CONSTRUCTOR, nilTerm1)
-    solver.mkTerm(Kind.APPLY_CONSTRUCTOR, nilTerm2)
+    solver.mkTerm(Kind.APPLY_CONSTRUCTOR, nilTerm)
+    solver.mkTerm(Kind.APPLY_CONSTRUCTOR, nilTerm)
     with pytest.raises(RuntimeError):
-        solver.mkTerm(Kind.APPLY_SELECTOR, nilTerm1)
+        solver.mkTerm(Kind.APPLY_SELECTOR, nilTerm)
     with pytest.raises(RuntimeError):
-        solver.mkTerm(Kind.APPLY_SELECTOR, consTerm1)
+        solver.mkTerm(Kind.APPLY_SELECTOR, consTerm)
     with pytest.raises(RuntimeError):
-        solver.mkTerm(Kind.APPLY_CONSTRUCTOR, consTerm2)
+        solver.mkTerm(Kind.APPLY_CONSTRUCTOR, consTerm)
     with pytest.raises(RuntimeError):
         solver.mkTerm(opterm1)
     with pytest.raises(RuntimeError):
@@ -842,7 +840,7 @@ def test_mk_term_from_op(solver):
     with pytest.raises(RuntimeError):
         solver.mkTerm(opterm1)
     with pytest.raises(RuntimeError):
-        slv.mkTerm(Kind.APPLY_CONSTRUCTOR, nilTerm1)
+        slv.mkTerm(Kind.APPLY_CONSTRUCTOR, nilTerm)
 
     # mkTerm(Op op, Term child) const
     solver.mkTerm(opterm1, a)
@@ -854,13 +852,13 @@ def test_mk_term_from_op(solver):
     with pytest.raises(RuntimeError):
         solver.mkTerm(opterm1, cvc5.Term(solver))
     with pytest.raises(RuntimeError):
-        solver.mkTerm(Kind.APPLY_CONSTRUCTOR, consTerm1, solver.mkInteger(0))
+        solver.mkTerm(Kind.APPLY_CONSTRUCTOR, consTerm, solver.mkInteger(0))
     with pytest.raises(RuntimeError):
         slv.mkTerm(opterm1, a)
 
     # mkTerm(Op op, Term child1, Term child2) const
-    solver.mkTerm(Kind.APPLY_CONSTRUCTOR, consTerm1, solver.mkInteger(0),
-                  solver.mkTerm(Kind.APPLY_CONSTRUCTOR, nilTerm1))
+    solver.mkTerm(Kind.APPLY_CONSTRUCTOR, consTerm, solver.mkInteger(0),
+                  solver.mkTerm(Kind.APPLY_CONSTRUCTOR, nilTerm))
     with pytest.raises(RuntimeError):
         solver.mkTerm(opterm2, solver.mkInteger(1), solver.mkInteger(2))
     with pytest.raises(RuntimeError):
@@ -871,9 +869,9 @@ def test_mk_term_from_op(solver):
         solver.mkTerm(opterm2, cvc5.Term(solver), solver.mkInteger(1))
     with pytest.raises(RuntimeError):
         slv.mkTerm(Kind.APPLY_CONSTRUCTOR,\
-                        consTerm1,\
+                        consTerm,\
                         solver.mkInteger(0),\
-                        solver.mkTerm(Kind.APPLY_CONSTRUCTOR, nilTerm1))
+                        solver.mkTerm(Kind.APPLY_CONSTRUCTOR, nilTerm))
 
     # mkTerm(Op op, Term child1, Term child2, Term child3) const
     with pytest.raises(RuntimeError):
@@ -1151,8 +1149,8 @@ def test_get_op(solver):
     consListSort = solver.mkDatatypeSort(consListSpec)
     consList = consListSort.getDatatype()
 
-    consTerm = consList.getConstructorTerm("cons")
-    nilTerm = consList.getConstructorTerm("nil")
+    consTerm = consList.getConstructor("cons").getConstructorTerm()
+    nilTerm = consList.getConstructor("nil").getConstructorTerm()
     headTerm = consList["cons"].getSelectorTerm("head")
 
     listnil = solver.mkTerm(Kind.APPLY_CONSTRUCTOR, nilTerm)
@@ -1716,14 +1714,15 @@ def test_simplify(solver):
     assert i1 == solver.simplify(i3)
 
     consList = consListSort.getDatatype()
-    dt1 = solver.mkTerm(\
-        Kind.APPLY_CONSTRUCTOR,\
-        consList.getConstructorTerm("cons"),\
-        solver.mkInteger(0),\
+    dt1 = solver.mkTerm(
+        Kind.APPLY_CONSTRUCTOR,
+        consList.getConstructor("cons").getConstructorTerm(),
+        solver.mkInteger(0),
         solver.mkTerm(
-            Kind.APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil")))
+            Kind.APPLY_CONSTRUCTOR,
+            consList.getConstructor("nil").getConstructorTerm()))
     solver.simplify(dt1)
-    dt2 = solver.mkTerm(\
+    dt2 = solver.mkTerm(
       Kind.APPLY_SELECTOR, consList["cons"].getSelectorTerm("head"), dt1)
     solver.simplify(dt2)
 

diff --git a/test/unit/api/python/test_term.py b/test/unit/api/python/test_term.py
index 5cac4b89fc595d702f4951f154d6ea6e14ce06e0..5af769267179e8f6150ee72102506ef9e63b81cf 100644 (file)
--- a/test/unit/api/python/test_term.py
+++ b/test/unit/api/python/test_term.py
@@ -187,8 +187,8 @@ def test_get_op(solver):
     c = solver.mkConst(intListSort, "c")
     list1 = listSort.getDatatype()
     # list datatype constructor and selector operator terms
-    consOpTerm = list1.getConstructorTerm("cons")
-    nilOpTerm = list1.getConstructorTerm("nil")
+    consOpTerm = list1.getConstructor("cons").getConstructorTerm()
+    nilOpTerm = list1.getConstructor("nil").getConstructorTerm()
     headOpTerm = list1["cons"].getSelectorTerm("head")
     tailOpTerm = list1["cons"].getSelectorTerm("tail")