api: Rename get(Selector|Constructor)Term() to getTerm(). (#8537)

diff --git a/docs/theories/datatypes.rst b/docs/theories/datatypes.rst
index d78c13e0a3202257c10777d8589a8b1804808aad..4106e31fed92a0796ddf453aa200cec7eb251252 100644 (file)
--- a/docs/theories/datatypes.rst
+++ b/docs/theories/datatypes.rst
@@ -207,7 +207,7 @@ a `cvc5::Solver solver` object.
 |                    |                                        |                                                                                                                                 |
 |                    |                                        | ``Datatype dt = s.getDatatype();``                                                                                              |
 |                    |                                        |                                                                                                                                 |
-|                    |                                        | ``Term ci = dt[i].getConstructorTerm();``                                                                                       |
+|                    |                                        | ``Term ci = dt[i].getTerm();``                                                                                                  |
 |                    |                                        |                                                                                                                                 |
 |                    |                                        | ``Term r = solver.mkTerm(Kind::APPLY_CONSTRUCTOR, {ci, <Term_1>, ..., <Term_n>});``                                             |
 +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
@@ -215,7 +215,7 @@ a `cvc5::Solver solver` object.
 |                    |                                        |                                                                                                                                 |
 |                    |                                        | ``Datatype dt = s.getDatatype();``                                                                                              |
 |                    |                                        |                                                                                                                                 |
-|                    |                                        | ``Term sij = dt[i].getSelector(j).getSelectorTerm();``                                                                          |
+|                    |                                        | ``Term sij = dt[i].getSelector(j).getTerm();``                                                                                  |
 |                    |                                        |                                                                                                                                 |
 |                    |                                        | ``Term r = solver.mkTerm(Kind::APPLY_SELECTOR, {sij, t});``                                                                     |
 +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
@@ -249,7 +249,7 @@ a `cvc5::Solver solver` object.
 |                    |                                        |                                                                                                                                 |
 |                    |                                        | ``Datatype dt = s.getDatatype();``                                                                                              |
 |                    |                                        |                                                                                                                                 |
-|                    |                                        | ``Term c = dt[0].getConstructorTerm();``                                                                                        |
+|                    |                                        | ``Term c = dt[0].getTerm();``                                                                                                   |
 |                    |                                        |                                                                                                                                 |
 |                    |                                        | ``Term r = solver.mkTerm(Kind::APPLY_CONSTRUCTOR, {c, <Term_1>, ..., <Term_n>});``                                              |
 +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
@@ -257,7 +257,7 @@ a `cvc5::Solver solver` object.
 |                    |                                        |                                                                                                                                 |
 |                    |                                        | ``Datatype dt = s.getDatatype();``                                                                                              |
 |                    |                                        |                                                                                                                                 |
-|                    |                                        | ``Term sel = dt[0].getSelector(i).getSelectorTerm();``                                                                          |
+|                    |                                        | ``Term sel = dt[0].getSelector(i).getTerm();``                                                                                  |
 |                    |                                        |                                                                                                                                 |
 |                    |                                        | ``Term r = solver.mkTerm(Kind::APPLY_SELECTOR, {sel, t});``                                                                     |
 +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
@@ -291,7 +291,7 @@ a `cvc5::Solver solver` object.
 |                    |                                        |                                                                                                                                 |
 |                    |                                        | ``Datatype dt = s.getDatatype();``                                                                                              |
 |                    |                                        |                                                                                                                                 |
-|                    |                                        | ``Term c = dt[0].getConstructorTerm();``                                                                                        |
+|                    |                                        | ``Term c = dt[0].getTerm();``                                                                                                   |
 |                    |                                        |                                                                                                                                 |
 |                    |                                        | ``Term r = solver.mkTerm(Kind::APPLY_CONSTRUCTOR, {c, <Term_1>, ..., <Term_n>});``                                              |
 +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+

diff --git a/examples/api/cpp/datatypes.cpp b/examples/api/cpp/datatypes.cpp
index 75e4a97d1256ec906b961d31319b06c4870acd41..bbdaa7e0f53261d6ef884fede78b7ac4564fe669 100644 (file)
--- a/examples/api/cpp/datatypes.cpp
+++ b/examples/api/cpp/datatypes.cpp
@@ -35,29 +35,25 @@ void test(Solver& slv, Sort& consListSort)
   // which is equivalent to consList["cons"].getConstructor().  Note that
   // "nil" is a constructor too, so it needs to be applied with
   // APPLY_CONSTRUCTOR, even though it has no arguments.
-  Term t = slv.mkTerm(
-      APPLY_CONSTRUCTOR,
-      {consList.getConstructor("cons").getConstructorTerm(),
-       slv.mkInteger(0),
-       slv.mkTerm(APPLY_CONSTRUCTOR,
-                  {consList.getConstructor("nil").getConstructorTerm()})});
+  Term t = slv.mkTerm(APPLY_CONSTRUCTOR,
+                      {consList.getConstructor("cons").getTerm(),
+                       slv.mkInteger(0),
+                       slv.mkTerm(APPLY_CONSTRUCTOR,
+                                  {consList.getConstructor("nil").getTerm()})});
 
   std::cout << "t is " << t << std::endl
             << "sort of cons is "
-            << consList.getConstructor("cons").getConstructorTerm().getSort()
-            << std::endl
+            << consList.getConstructor("cons").getTerm().getSort() << std::endl
             << "sort of nil is "
-            << consList.getConstructor("nil").getConstructorTerm().getSort()
-            << std::endl;
+            << consList.getConstructor("nil").getTerm().getSort() << std::endl;
 
   // t2 = head(cons 0 nil), and of course this can be evaluated
   //
   // 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(APPLY_SELECTOR,
-                 {consList["cons"].getSelector("head").getSelectorTerm(), t});
+  Term t2 = slv.mkTerm(APPLY_SELECTOR,
+                       {consList["cons"].getSelector("head").getTerm(), t});
 
   std::cout << "t2 is " << t2 << std::endl
             << "simplify(t2) is " << slv.simplify(t2) << std::endl
@@ -133,14 +129,13 @@ void test(Solver& slv, Sort& consListSort)
   std::cout << "term " << a << " is of sort " << a.getSort() << std::endl;
 
   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 "
-      << paramConsList.getConstructor("cons").getConstructorTerm().getSort()
-      << std::endl
-      << std::endl;
+      APPLY_SELECTOR, {paramConsList["cons"].getSelector("head").getTerm(), a});
+  std::cout << "head_a is " << head_a << " of sort " << head_a.getSort()
+            << std::endl
+            << "sort of cons is "
+            << paramConsList.getConstructor("cons").getTerm().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 0f70ce0dcf6bdea0dd1855bec7ba82af3e934f36..03c80c0a0818a01da2e5b1251cb27d7911774629 100644 (file)
--- a/examples/api/java/Datatypes.java
+++ b/examples/api/java/Datatypes.java
@@ -35,22 +35,21 @@ 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.getConstructor("cons").getConstructorTerm(),
+        consList.getConstructor("cons").getTerm(),
         slv.mkInteger(0),
-        slv.mkTerm(Kind.APPLY_CONSTRUCTOR, consList.getConstructor("nil").getConstructorTerm()));
+        slv.mkTerm(Kind.APPLY_CONSTRUCTOR, consList.getConstructor("nil").getTerm()));
 
     System.out.println("t is " + t + "\n"
-        + "sort of cons is " + consList.getConstructor("cons").getConstructorTerm().getSort() + "\n"
-        + "sort of nil is " + consList.getConstructor("nil").getConstructorTerm().getSort());
+        + "sort of cons is " + consList.getConstructor("cons").getTerm().getSort() + "\n"
+        + "sort of nil is " + consList.getConstructor("nil").getTerm().getSort());
 
     // t2 = head(cons 0 nil), and of course this can be evaluated
     //
     // 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").getSelector("head").getSelectorTerm(),
-        t);
+    Term t2 = slv.mkTerm(
+        Kind.APPLY_SELECTOR, consList.getConstructor("cons").getSelector("head").getTerm(), t);
 
     System.out.println("t2 is " + t2 + "\n"
         + "simplify(t2) is " + slv.simplify(t2) + "\n");
@@ -124,12 +123,10 @@ 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").getSelector("head").getSelectorTerm(),
-        a);
+    Term head_a = slv.mkTerm(
+        Kind.APPLY_SELECTOR, paramConsList.getConstructor("cons").getSelector("head").getTerm(), 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");
+        + "sort of cons is " + paramConsList.getConstructor("cons").getTerm().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/java/Statistics.java b/examples/api/java/Statistics.java
index da1bbeb8c76a27fe3723449567214e64156bffe4..fc7015e04a1a0cdbf0f96cee70b278b3f38b1375 100644 (file)
--- a/examples/api/java/Statistics.java
+++ b/examples/api/java/Statistics.java
@@ -202,7 +202,7 @@ public class Statistics
     // (assert (forall ((x Person)) (not (set.member (mkTuple x x) ancestor))))
     Term var = solver.mkVar(personSort, "x");
     DatatypeConstructor constructor = tupleArity2.getDatatype().getConstructor(0);
-    Term xxTuple = solver.mkTerm(APPLY_CONSTRUCTOR, constructor.getConstructorTerm(), var, var);
+    Term xxTuple = solver.mkTerm(APPLY_CONSTRUCTOR, constructor.getTerm(), var, var);
     Term member = solver.mkTerm(SET_MEMBER, xxTuple, ancestor);
     Term notMember = solver.mkTerm(NOT, member);
 

diff --git a/examples/api/python/datatypes.py b/examples/api/python/datatypes.py
index 39642297cafd9ba598967ca9125062cd281f7738..24226d44353d421cc1128ffa0147328a50077a41 100644 (file)
--- a/examples/api/python/datatypes.py
+++ b/examples/api/python/datatypes.py
@@ -36,16 +36,16 @@ def test(slv, consListSort):
 
     t = slv.mkTerm(
             Kind.APPLY_CONSTRUCTOR,
-            consList.getConstructor("cons").getConstructorTerm(),
+            consList.getConstructor("cons").getTerm(),
             slv.mkInteger(0),
             slv.mkTerm(
                 Kind.APPLY_CONSTRUCTOR,
-                consList.getConstructor("nil").getConstructorTerm()))
+                consList.getConstructor("nil").getTerm()))
 
     print("t is {}\nsort of cons is {}\n sort of nil is {}".format(
         t,
-        consList.getConstructor("cons").getConstructorTerm().getSort(),
-        consList.getConstructor("nil").getConstructorTerm().getSort()))
+        consList.getConstructor("cons").getTerm().getSort(),
+        consList.getConstructor("nil").getTerm().getSort()))
 
     # t2 = head(cons 0 nil), and of course this can be evaluated
     #
@@ -55,7 +55,7 @@ def test(slv, consListSort):
 
     t2 = slv.mkTerm(
             Kind.APPLY_SELECTOR,
-            consList["cons"].getSelector("head").getSelectorTerm(),
+            consList["cons"].getSelector("head").getTerm(),
             t)
 
     print("t2 is {}\nsimplify(t2) is {}\n\n".format(t2, slv.simplify(t2)))
@@ -102,11 +102,11 @@ def test(slv, consListSort):
 
     head_a = slv.mkTerm(
             Kind.APPLY_SELECTOR,
-            paramConsList["cons"].getSelector("head").getSelectorTerm(),
+            paramConsList["cons"].getSelector("head").getTerm(),
             a)
     print("head_a is {} of sort {}".format(head_a, head_a.getSort()))
     print("sort of cons is",
-          paramConsList.getConstructor("cons").getConstructorTerm().getSort())
+          paramConsList.getConstructor("cons").getTerm().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 26da68abca26f3e94b3eb813e7890b0a1560fc8d..2da46514e94b4f7cb3c6eba3bb134fe701a86e63 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -3593,7 +3593,7 @@ std::string DatatypeSelector::getName() const
   CVC5_API_TRY_CATCH_END;
 }
 
-Term DatatypeSelector::getSelectorTerm() const
+Term DatatypeSelector::getTerm() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK_NOT_NULL;
@@ -3682,7 +3682,7 @@ std::string DatatypeConstructor::getName() const
   CVC5_API_TRY_CATCH_END;
 }
 
-Term DatatypeConstructor::getConstructorTerm() const
+Term DatatypeConstructor::getTerm() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK_NOT_NULL;
@@ -6124,7 +6124,7 @@ Term Solver::mkTuple(const std::vector<Sort>& sorts,
   Sort s = mkTupleSortHelper(sorts);
   Datatype dt = s.getDatatype();
   internal::NodeBuilder nb(extToIntKind(APPLY_CONSTRUCTOR));
-  nb << *dt[0].getConstructorTerm().d_node;
+  nb << *dt[0].getTerm().d_node;
   nb.append(args);
   internal::Node res = nb.constructNode();
   (void)res.getType(true); /* kick off type checking */

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 7bf71accdb19d89e601f9bcd32d0bdb21b8d62d2..78bad1eeec215e5a30d4d2f6c666127d030ec405 100644 (file)
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -2017,7 +2017,7 @@ class CVC5_EXPORT DatatypeSelector
    * Get the selector operator of this datatype selector.
    * @return the selector term
    */
-  Term getSelectorTerm() const;
+  Term getTerm() const;
 
   /**
    * Get the updater operator of this datatype selector.
@@ -2092,7 +2092,7 @@ class CVC5_EXPORT DatatypeConstructor
    * Get the constructor operator of this datatype constructor.
    * @return the constructor term
    */
-  Term getConstructorTerm() const;
+  Term getTerm() const;
 
   /**
    * Get the constructor operator of this datatype constructor whose return

diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h
index 1d5c2da90c25d062163c56ff8b4cf157e9d1c97b..7d405891a61f057e2cb226ab8d73eaed29bd7713 100644 (file)
--- a/src/api/cpp/cvc5_kind.h
+++ b/src/api/cpp/cvc5_kind.h
@@ -2533,7 +2533,7 @@ enum Kind : int32_t
    *
    * - Arity: ``n > 0``
    *
-   *   - ``1:`` DatatypeConstructor Term (see DatatypeConstructor::getConstructorTerm() const)
+   *   - ``1:`` DatatypeConstructor Term (see DatatypeConstructor::getTerm() const)
    *   - ``2..n:`` Terms of the Sorts of the selectors of the constructor (the arguments to the constructor)
    *
    * - Create Term of this Kind with:
@@ -2555,7 +2555,7 @@ enum Kind : int32_t
    *
    * - Arity: ``2``
    *
-   *   - ``1:`` DatatypeSelector Term (see DatatypeSelector::getSelectorTerm() const)
+   *   - ``1:`` DatatypeSelector Term (see DatatypeSelector::getTerm() 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 e3e482feef4c7cbc0fb132f903aca0a92d44399d..94a838d9570f8ec3b8387a4dd2418cbdf4d92d87 100644 (file)
--- a/src/api/java/io/github/cvc5/DatatypeConstructor.java
+++ b/src/api/java/io/github/cvc5/DatatypeConstructor.java
@@ -50,13 +50,13 @@ public class DatatypeConstructor extends AbstractPointer implements Iterable<Dat
    * Get the constructor operator of this datatype constructor.
    * @return the constructor term
    */
-  public Term getConstructorTerm()
+  public Term getTerm()
   {
-    long termPointer = getConstructorTerm(pointer);
+    long termPointer = getTerm(pointer);
     return new Term(solver, termPointer);
   }
 
-  private native long getConstructorTerm(long pointer);
+  private native long getTerm(long pointer);
 
   /**
    * Get the constructor operator of this datatype constructor whose return

diff --git a/src/api/java/io/github/cvc5/DatatypeSelector.java b/src/api/java/io/github/cvc5/DatatypeSelector.java
index 4978143c9d72a585c45b51bd3bb0106672d79a3e..325b0b1d083f383ec0344e3f2656c5608dee4860 100644 (file)
--- a/src/api/java/io/github/cvc5/DatatypeSelector.java
+++ b/src/api/java/io/github/cvc5/DatatypeSelector.java
@@ -47,13 +47,13 @@ public class DatatypeSelector extends AbstractPointer
    * Get the selector operator of this datatype selector.
    * @return the selector term
    */
-  public Term getSelectorTerm()
+  public Term getTerm()
   {
-    long termPointer = getSelectorTerm(pointer);
+    long termPointer = getTerm(pointer);
     return new Term(solver, termPointer);
   }
 
-  private native long getSelectorTerm(long pointer);
+  private native long getTerm(long pointer);
 
   /**
    * Get the upater operator of this datatype selector.

diff --git a/src/api/java/jni/datatype_constructor.cpp b/src/api/java/jni/datatype_constructor.cpp
index 1631674fe8092c7b425b9750662bba35841730b9..2f6645d0c4e470bc1e72030cd3998ccd891df852 100644 (file)
--- a/src/api/java/jni/datatype_constructor.cpp
+++ b/src/api/java/jni/datatype_constructor.cpp
@@ -48,17 +48,15 @@ JNIEXPORT jstring JNICALL Java_io_github_cvc5_DatatypeConstructor_getName(
 
 /*
  * Class:     io_github_cvc5_DatatypeConstructor
- * Method:    getConstructorTerm
+ * Method:    getTerm
  * Signature: (J)J
  */
-JNIEXPORT jlong JNICALL
-Java_io_github_cvc5_DatatypeConstructor_getConstructorTerm(JNIEnv* env,
-                                                               jobject,
-                                                               jlong pointer)
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_DatatypeConstructor_getTerm(
+    JNIEnv* env, jobject, jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   DatatypeConstructor* current = (DatatypeConstructor*)pointer;
-  Term* retPointer = new Term(current->getConstructorTerm());
+  Term* retPointer = new Term(current->getTerm());
   return (jlong)retPointer;
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 }

diff --git a/src/api/java/jni/datatype_selector.cpp b/src/api/java/jni/datatype_selector.cpp
index d75263b5092601f5996174e50aeded2bf2fdd289..a5f20cb1ae2052f00257ead9f80e383119d92963 100644 (file)
--- a/src/api/java/jni/datatype_selector.cpp
+++ b/src/api/java/jni/datatype_selector.cpp
@@ -46,17 +46,15 @@ JNIEXPORT jstring JNICALL Java_io_github_cvc5_DatatypeSelector_getName(
 
 /*
  * Class:     io_github_cvc5_DatatypeSelector
- * Method:    getSelectorTerm
+ * Method:    getTerm
  * Signature: (J)J
  */
-JNIEXPORT jlong JNICALL
-Java_io_github_cvc5_DatatypeSelector_getSelectorTerm(JNIEnv* env,
-                                                         jobject,
-                                                         jlong pointer)
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_DatatypeSelector_getTerm(
+    JNIEnv* env, jobject, jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   DatatypeSelector* current = (DatatypeSelector*)pointer;
-  Term* retPointer = new Term(current->getSelectorTerm());
+  Term* retPointer = new Term(current->getTerm());
   return (jlong)retPointer;
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 }

diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index 65bb821f9edbf6682d5952e723aacf509a22a06a..c4fb71c5cb13008cce7abdd8a6ecc9d0ed320678 100644 (file)
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -85,7 +85,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5":
         DatatypeSelector operator[](size_t idx) except +
         DatatypeSelector operator[](const string& name) except +
         string getName() except +
-        Term getConstructorTerm() except +
+        Term getTerm() except +
         Term getInstantiatedConstructorTerm(const Sort& retSort) except +
         Term getTesterTerm() except +
         size_t getNumSelectors() except +
@@ -122,7 +122,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5":
     cdef cppclass DatatypeSelector:
         DatatypeSelector() except +
         string getName() except +
-        Term getSelectorTerm() except +
+        Term getTerm() except +
         Term getUpdaterTerm() except +
         Sort getCodomainSort() except +
         bint isNull() except +

diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 8fc4904e7dcf15c676289d08e931ec4788bb183f..f43888edd313726fdfac1651f06eea31341a48dc 100644 (file)
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -256,12 +256,12 @@ cdef class DatatypeConstructor:
         """
         return self.cdc.getName().decode()
 
-    def getConstructorTerm(self):
+    def getTerm(self):
         """
             :return: The constructor operator as a term.
         """
         cdef Term term = Term(self.solver)
-        term.cterm = self.cdc.getConstructorTerm()
+        term.cterm = self.cdc.getTerm()
         return term
 
     def getInstantiatedConstructorTerm(self, Sort retSort):
@@ -491,12 +491,12 @@ cdef class DatatypeSelector:
         """
         return self.cds.getName().decode()
 
-    def getSelectorTerm(self):
+    def getTerm(self):
         """
             :return: The selector opeartor of this datatype selector as a term.
         """
         cdef Term term = Term(self.solver)
-        term.cterm = self.cds.getSelectorTerm()
+        term.cterm = self.cds.getTerm()
         return term
 
     def getUpdaterTerm(self):

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 59bc680908bc5588d236df96a3878ea7507ecdd1..5e82012dddaa3fbc1dd5925035b083fab3847d51 100644 (file)
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -388,7 +388,7 @@ std::vector<cvc5::Sort> Parser::bindMutualDatatypeTypes(
       for (size_t j = 0, ncons = dt.getNumConstructors(); j < ncons; j++)
       {
         const cvc5::DatatypeConstructor& ctor = dt[j];
-        cvc5::Term constructor = ctor.getConstructorTerm();
+        cvc5::Term constructor = ctor.getTerm();
         Trace("parser-idt") << "+ define " << constructor << std::endl;
         string constructorName = ctor.getName();
         if(consNames.find(constructorName)==consNames.end()) {
@@ -414,7 +414,7 @@ std::vector<cvc5::Sort> Parser::bindMutualDatatypeTypes(
         for (size_t k = 0, nargs = ctor.getNumSelectors(); k < nargs; k++)
         {
           const cvc5::DatatypeSelector& sel = ctor[k];
-          cvc5::Term selector = sel.getSelectorTerm();
+          cvc5::Term selector = sel.getTerm();
           Trace("parser-idt") << "+++ define " << selector << std::endl;
           string selectorName = sel.getName();
           if(selNames.find(selectorName)==selNames.end()) {

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index bf610ae86683244b8ea98770e30050bd0b6eb1cb..63cc3af4e24a206ed63ad654777ce4e0613e7dc8 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1101,8 +1101,8 @@ cvc5::Term Smt2::applyParseOp(ParseOp& p, std::vector<cvc5::Term>& args)
     cvc5::Term ret;
     if (p.d_kind == cvc5::APPLY_SELECTOR)
     {
-      ret = d_solver->mkTerm(cvc5::APPLY_SELECTOR,
-                             {dt[0][n].getSelectorTerm(), args[0]});
+      ret =
+          d_solver->mkTerm(cvc5::APPLY_SELECTOR, {dt[0][n].getTerm(), args[0]});
     }
     else
     {

diff --git a/test/unit/api/cpp/datatype_api_black.cpp b/test/unit/api/cpp/datatype_api_black.cpp
index f4831b9a0e4b43ca293ff0dd8e19e5db82d76570..ad0c567010fd83c3ad4c746cca7c8984a6fef59f 100644 (file)
--- a/test/unit/api/cpp/datatype_api_black.cpp
+++ b/test/unit/api/cpp/datatype_api_black.cpp
@@ -36,8 +36,8 @@ TEST_F(TestApiBlackDatatype, mkDatatypeSort)
   DatatypeConstructor consConstr = d[0];
   DatatypeConstructor nilConstr = d[1];
   ASSERT_THROW(d[2], CVC5ApiException);
-  ASSERT_NO_THROW(consConstr.getConstructorTerm());
-  ASSERT_NO_THROW(nilConstr.getConstructorTerm());
+  ASSERT_NO_THROW(consConstr.getTerm());
+  ASSERT_NO_THROW(nilConstr.getTerm());
 }
 
 TEST_F(TestApiBlackDatatype, isNull)
@@ -206,7 +206,7 @@ TEST_F(TestApiBlackDatatype, datatypeStructs)
   ASSERT_TRUE(dt.isWellFounded());
   // get constructor
   DatatypeConstructor dcons = dt[0];
-  Term consTerm = dcons.getConstructorTerm();
+  Term consTerm = dcons.getTerm();
   ASSERT_EQ(dcons.getNumSelectors(), 2);
 
   // create datatype sort to test
@@ -588,7 +588,7 @@ TEST_F(TestApiBlackDatatype, datatypeSpecializedCons)
   Term testConsTerm;
   // get the specialized constructor term for list[Int]
   ASSERT_NO_THROW(testConsTerm = nilc.getInstantiatedConstructorTerm(listInt));
-  ASSERT_NE(testConsTerm, nilc.getConstructorTerm());
+  ASSERT_NE(testConsTerm, nilc.getTerm());
   // error to get the specialized constructor term for Int
   ASSERT_THROW(nilc.getInstantiatedConstructorTerm(isort), CVC5ApiException);
 }

diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index 7461a879eeeffd8dbc78d8b53d6425c4fb33b937..17812748badbf80f9fd559197236aba76297152c 100644 (file)
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -227,7 +227,7 @@ TEST_F(TestApiBlackSolver, mkDatatypeSorts)
   Term t1 = d_solver.mkConst(isort1, "t");
   Term t0 = d_solver.mkTerm(
       APPLY_SELECTOR,
-      {t1.getSort().getDatatype().getSelector("s1").getSelectorTerm(), t1});
+      {t1.getSort().getDatatype().getSelector("s1").getTerm(), t1});
   ASSERT_EQ(dt_sorts[0].instantiate({d_solver.getBooleanSort()}), t0.getSort());
 
   /* Note: More tests are in datatype_api_black. */
@@ -852,10 +852,10 @@ TEST_F(TestApiBlackSolver, mkTermFromOp)
   Datatype list = listSort.getDatatype();
 
   // list datatype constructor and selector operator terms
-  Term consTerm = list.getConstructor("cons").getConstructorTerm();
-  Term nilTerm = list.getConstructor("nil").getConstructorTerm();
-  Term headTerm = list["cons"].getSelector("head").getSelectorTerm();
-  Term tailTerm = list["cons"]["tail"].getSelectorTerm();
+  Term consTerm = list.getConstructor("cons").getTerm();
+  Term nilTerm = list.getConstructor("nil").getTerm();
+  Term headTerm = list["cons"].getSelector("head").getTerm();
+  Term tailTerm = list["cons"]["tail"].getTerm();
 
   // mkTerm(Op op, Term term) const
   ASSERT_NO_THROW(d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilTerm}));
@@ -1498,9 +1498,9 @@ TEST_F(TestApiBlackSolver, getOp)
   Sort consListSort = d_solver.mkDatatypeSort(consListSpec);
   Datatype consList = consListSort.getDatatype();
 
-  Term consTerm = consList.getConstructor("cons").getConstructorTerm();
-  Term nilTerm = consList.getConstructor("nil").getConstructorTerm();
-  Term headTerm = consList["cons"].getSelector("head").getSelectorTerm();
+  Term consTerm = consList.getConstructor("cons").getTerm();
+  Term nilTerm = consList.getConstructor("nil").getTerm();
+  Term headTerm = consList["cons"].getSelector("head").getTerm();
 
   Term listnil = d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilTerm});
   Term listcons1 = d_solver.mkTerm(APPLY_CONSTRUCTOR,
@@ -2364,14 +2364,13 @@ TEST_F(TestApiBlackSolver, simplify)
   Datatype consList = consListSort.getDatatype();
   Term dt1 = d_solver.mkTerm(
       APPLY_CONSTRUCTOR,
-      {consList.getConstructor("cons").getConstructorTerm(),
+      {consList.getConstructor("cons").getTerm(),
        d_solver.mkInteger(0),
        d_solver.mkTerm(APPLY_CONSTRUCTOR,
-                       {consList.getConstructor("nil").getConstructorTerm()})});
+                       {consList.getConstructor("nil").getTerm()})});
   ASSERT_NO_THROW(d_solver.simplify(dt1));
   Term dt2 = d_solver.mkTerm(
-      APPLY_SELECTOR,
-      {consList["cons"].getSelector("head").getSelectorTerm(), dt1});
+      APPLY_SELECTOR, {consList["cons"].getSelector("head").getTerm(), dt1});
   ASSERT_NO_THROW(d_solver.simplify(dt2));
 
   Term b1 = d_solver.mkVar(bvSort, "b1");
@@ -2853,7 +2852,7 @@ TEST_F(TestApiBlackSolver, tupleProject)
 
   for (size_t i = 0; i < indices.size(); i++)
   {
-    Term selectorTerm = constructor[indices[i]].getSelectorTerm();
+    Term selectorTerm = constructor[indices[i]].getTerm();
     Term selectedTerm = d_solver.mkTerm(APPLY_SELECTOR, {selectorTerm, tuple});
     Term simplifiedTerm = d_solver.simplify(selectedTerm);
     ASSERT_EQ(elements[indices[i]], simplifiedTerm);
@@ -2930,7 +2929,7 @@ TEST_F(TestApiBlackSolver, proj_issue373)
   Term bvl = d_solver.mkTerm(d_solver.mkOp(VARIABLE_LIST), {t452});
   Term acons = d_solver.mkTerm(
       d_solver.mkOp(APPLY_CONSTRUCTOR),
-      {s4.getDatatype().getConstructor("_x115").getConstructorTerm(), t452});
+      {s4.getDatatype().getConstructor("_x115").getTerm(), t452});
   // type exception
   ASSERT_THROW(
       d_solver.mkTerm(d_solver.mkOp(APPLY_CONSTRUCTOR), {bvl, acons, t452}),
@@ -2970,16 +2969,14 @@ TEST_F(TestApiBlackSolver, proj_issue378)
   dtdecl.addConstructor(cdecl);
   Sort s7 = d_solver.mkDatatypeSort(dtdecl);
   Sort s9 = s7.instantiate({s2});
-  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")
-                                       .getSelector("_x185")
-                                       .getSelectorTerm(),
-                                   t1507,
-                                   t7}));
+  Term t1507 =
+      d_solver.mkTerm(APPLY_CONSTRUCTOR,
+                      {s9.getDatatype().getConstructor("_x184").getTerm(), t7});
+  ASSERT_NO_THROW(d_solver.mkTerm(
+      APPLY_UPDATER,
+      {s9.getDatatype().getConstructor("_x186").getSelector("_x185").getTerm(),
+       t1507,
+       t7}));
 }
 
 TEST_F(TestApiBlackSolver, proj_issue379)
@@ -3072,7 +3069,7 @@ TEST_F(TestApiBlackSolver, proj_issue382)
   Term t82 = d_solver.mkTerm(MATCH, {t13, t53, t53, t53, t81});
   Term t325 = d_solver.mkTerm(
       APPLY_SELECTOR,
-      {t82.getSort().getDatatype().getSelector("_x19").getSelectorTerm(), t82});
+      {t82.getSort().getDatatype().getSelector("_x19").getTerm(), t82});
   ASSERT_NO_THROW(d_solver.simplify(t325));
 }
 
@@ -3347,7 +3344,7 @@ TEST_F(TestApiBlackSolver, projIssue431)
                  .getDatatype()
                  .getConstructor("_cons64")
                  .getSelector("_sel62")
-                 .getSelectorTerm();
+                 .getTerm();
   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 ab2b878311d7b0f16cd34ab992ec917b705ded8b..3cc89434b5edd77790ea6daf3189671f6f5117b5 100644 (file)
--- a/test/unit/api/cpp/solver_white.cpp
+++ b/test/unit/api/cpp/solver_white.cpp
@@ -36,9 +36,9 @@ TEST_F(TestApiWhiteSolver, getOp)
   Sort consListSort = d_solver.mkDatatypeSort(consListSpec);
   Datatype consList = consListSort.getDatatype();
 
-  Term nilTerm = consList.getConstructor("nil").getConstructorTerm();
-  Term consTerm = consList.getConstructor("cons").getConstructorTerm();
-  Term headTerm = consList["cons"].getSelector("head").getSelectorTerm();
+  Term nilTerm = consList.getConstructor("nil").getTerm();
+  Term consTerm = consList.getConstructor("cons").getTerm();
+  Term headTerm = consList["cons"].getSelector("head").getTerm();
 
   Term listnil = d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilTerm});
   Term listcons1 = d_solver.mkTerm(APPLY_CONSTRUCTOR,

diff --git a/test/unit/api/cpp/sort_black.cpp b/test/unit/api/cpp/sort_black.cpp
index ccbe23f9b7fc148a5702ee24ceb681e25ec86031..8a716faec49cecdeb3c7cbd18dd74e896990fcc8 100644 (file)
--- a/test/unit/api/cpp/sort_black.cpp
+++ b/test/unit/api/cpp/sort_black.cpp
@@ -146,7 +146,7 @@ TEST_F(TestApiBlackSort, isConstructor)
 {
   Sort dt_sort = create_datatype_sort();
   Datatype dt = dt_sort.getDatatype();
-  Sort cons_sort = dt[0].getConstructorTerm().getSort();
+  Sort cons_sort = dt[0].getTerm().getSort();
   ASSERT_TRUE(cons_sort.isDatatypeConstructor());
   ASSERT_NO_THROW(Sort().isDatatypeConstructor());
 }
@@ -155,7 +155,7 @@ TEST_F(TestApiBlackSort, isSelector)
 {
   Sort dt_sort = create_datatype_sort();
   Datatype dt = dt_sort.getDatatype();
-  Sort cons_sort = dt[0][1].getSelectorTerm().getSort();
+  Sort cons_sort = dt[0][1].getTerm().getSort();
   ASSERT_TRUE(cons_sort.isDatatypeSelector());
   ASSERT_NO_THROW(Sort().isDatatypeSelector());
 }
@@ -277,7 +277,7 @@ TEST_F(TestApiBlackSort, datatypeSorts)
 
   // get constructor
   DatatypeConstructor dcons = dt[0];
-  Term consTerm = dcons.getConstructorTerm();
+  Term consTerm = dcons.getTerm();
   Sort consSort = consTerm.getSort();
   ASSERT_TRUE(consSort.isDatatypeConstructor());
   ASSERT_FALSE(consSort.isDatatypeTester());
@@ -299,7 +299,7 @@ TEST_F(TestApiBlackSort, datatypeSorts)
 
   // get selector
   DatatypeSelector dselTail = dcons[1];
-  Term tailTerm = dselTail.getSelectorTerm();
+  Term tailTerm = dselTail.getTerm();
   ASSERT_TRUE(tailTerm.getSort().isDatatypeSelector());
   ASSERT_EQ(tailTerm.getSort().getDatatypeSelectorDomainSort(), dtypeSort);
   ASSERT_EQ(tailTerm.getSort().getDatatypeSelectorCodomainSort(), dtypeSort);

diff --git a/test/unit/api/cpp/term_black.cpp b/test/unit/api/cpp/term_black.cpp
index c1034cf1d0cb43477273854c6fa08d6b2ce69f71..ec4743037cb3abe596bbb3c58156e88b513cc541 100644 (file)
--- a/test/unit/api/cpp/term_black.cpp
+++ b/test/unit/api/cpp/term_black.cpp
@@ -188,10 +188,10 @@ 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.getConstructor("cons").getConstructorTerm();
-  Term nilOpTerm = list.getConstructor("nil").getConstructorTerm();
-  Term headOpTerm = list["cons"].getSelector("head").getSelectorTerm();
-  Term tailOpTerm = list["cons"].getSelector("tail").getSelectorTerm();
+  Term consOpTerm = list.getConstructor("cons").getTerm();
+  Term nilOpTerm = list.getConstructor("nil").getTerm();
+  Term headOpTerm = list["cons"].getSelector("head").getTerm();
+  Term tailOpTerm = list["cons"].getSelector("tail").getTerm();
 
   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 470dd4db80ef261d687bf254a80f31099ee00e62..86d6b976ed4567fc436a52fc3667b38fcd58c4bf 100644 (file)
--- a/test/unit/api/cpp/term_white.cpp
+++ b/test/unit/api/cpp/term_white.cpp
@@ -63,10 +63,10 @@ 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.getConstructor("cons").getConstructorTerm();
-  Term nilOpTerm = list.getConstructor("nil").getConstructorTerm();
-  Term headOpTerm = list["cons"].getSelector("head").getSelectorTerm();
-  Term tailOpTerm = list["cons"].getSelector("tail").getSelectorTerm();
+  Term consOpTerm = list.getConstructor("cons").getTerm();
+  Term nilOpTerm = list.getConstructor("nil").getTerm();
+  Term headOpTerm = list["cons"].getSelector("head").getTerm();
+  Term tailOpTerm = list["cons"].getSelector("tail").getTerm();
 
   Term nilTerm = d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilOpTerm});
   Term consTerm = d_solver.mkTerm(APPLY_CONSTRUCTOR,

diff --git a/test/unit/api/java/DatatypeTest.java b/test/unit/api/java/DatatypeTest.java
index bc13ab634b7cdd8f730d7c1702424fe12805307c..557db2f9b48d8a3eb04cac3c50040b1be5e6ad70 100644 (file)
--- a/test/unit/api/java/DatatypeTest.java
+++ b/test/unit/api/java/DatatypeTest.java
@@ -54,8 +54,8 @@ class DatatypeTest
     DatatypeConstructor consConstr = d.getConstructor(0);
     DatatypeConstructor nilConstr = d.getConstructor(1);
     assertThrows(CVC5ApiException.class, () -> d.getConstructor(2));
-    assertDoesNotThrow(() -> consConstr.getConstructorTerm());
-    assertDoesNotThrow(() -> nilConstr.getConstructorTerm());
+    assertDoesNotThrow(() -> consConstr.getTerm());
+    assertDoesNotThrow(() -> nilConstr.getTerm());
   }
 
   @Test
@@ -200,7 +200,7 @@ class DatatypeTest
     assertTrue(dt.isWellFounded());
     // get constructor
     DatatypeConstructor dcons = dt.getConstructor(0);
-    Term consTerm = dcons.getConstructorTerm();
+    Term consTerm = dcons.getTerm();
     assertEquals(dcons.getNumSelectors(), 2);
 
     // create datatype sort to test
@@ -592,7 +592,7 @@ class DatatypeTest
     // get the specialized constructor term for list[Int]
     assertDoesNotThrow(() -> atomicTerm.set(nilc.getInstantiatedConstructorTerm(listInt)));
     Term testConsTerm = atomicTerm.get();
-    assertNotEquals(testConsTerm, nilc.getConstructorTerm());
+    assertNotEquals(testConsTerm, nilc.getTerm());
     // error to get the specialized constructor term for Int
     assertThrows(CVC5ApiException.class, () -> nilc.getInstantiatedConstructorTerm(isort));
   }

diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java
index 0865d604571918858c4cb22d02580132241745d2..bd21caeb98cf7d13228002d35bd6443231759113 100644 (file)
--- a/test/unit/api/java/SolverTest.java
+++ b/test/unit/api/java/SolverTest.java
@@ -215,7 +215,7 @@ class SolverTest
     Sort isort1 = dt_sorts[1].instantiate(new Sort[] {d_solver.getBooleanSort()});
     Term t1 = d_solver.mkConst(isort1, "t");
     Term t0 = d_solver.mkTerm(APPLY_SELECTOR,
-        t1.getSort().getDatatype().getConstructor("c1").getSelector("s1").getSelectorTerm(),
+        t1.getSort().getDatatype().getConstructor("c1").getSelector("s1").getTerm(),
         t1);
     assertEquals(dt_sorts[0].instantiate(new Sort[] {d_solver.getBooleanSort()}), t0.getSort());
 
@@ -834,10 +834,10 @@ class SolverTest
     Datatype list = listSort.getDatatype();
 
     // list datatype constructor and selector operator terms
-    Term consTerm = list.getConstructor("cons").getConstructorTerm();
-    Term nilTerm = list.getConstructor("nil").getConstructorTerm();
-    Term headTerm = list.getConstructor("cons").getSelector("head").getSelectorTerm();
-    Term tailTerm = list.getConstructor("cons").getSelector("tail").getSelectorTerm();
+    Term consTerm = list.getConstructor("cons").getTerm();
+    Term nilTerm = list.getConstructor("nil").getTerm();
+    Term headTerm = list.getConstructor("cons").getSelector("head").getTerm();
+    Term tailTerm = list.getConstructor("cons").getSelector("tail").getTerm();
 
     // mkTerm(Op op, Term term) const
     assertDoesNotThrow(() -> d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm));
@@ -1541,9 +1541,9 @@ class SolverTest
     Sort consListSort = d_solver.mkDatatypeSort(consListSpec);
     Datatype consList = consListSort.getDatatype();
 
-    Term consTerm = consList.getConstructor("cons").getConstructorTerm();
-    Term nilTerm = consList.getConstructor("nil").getConstructorTerm();
-    Term headTerm = consList.getConstructor("cons").getSelector("head").getSelectorTerm();
+    Term consTerm = consList.getConstructor("cons").getTerm();
+    Term nilTerm = consList.getConstructor("nil").getTerm();
+    Term headTerm = consList.getConstructor("cons").getSelector("head").getTerm();
 
     Term listnil = d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm);
     Term listcons1 = d_solver.mkTerm(APPLY_CONSTRUCTOR, consTerm, d_solver.mkInteger(1), listnil);
@@ -2414,12 +2414,12 @@ class SolverTest
 
     Datatype consList = consListSort.getDatatype();
     Term dt1 = d_solver.mkTerm(APPLY_CONSTRUCTOR,
-        consList.getConstructor("cons").getConstructorTerm(),
+        consList.getConstructor("cons").getTerm(),
         d_solver.mkInteger(0),
-        d_solver.mkTerm(APPLY_CONSTRUCTOR, consList.getConstructor("nil").getConstructorTerm()));
+        d_solver.mkTerm(APPLY_CONSTRUCTOR, consList.getConstructor("nil").getTerm()));
     assertDoesNotThrow(() -> d_solver.simplify(dt1));
     Term dt2 = d_solver.mkTerm(
-        APPLY_SELECTOR, consList.getConstructor("cons").getSelector("head").getSelectorTerm(), dt1);
+        APPLY_SELECTOR, consList.getConstructor("cons").getSelector("head").getTerm(), dt1);
     assertDoesNotThrow(() -> d_solver.simplify(dt2));
 
     Term b1 = d_solver.mkVar(bvSort, "b1");
@@ -2939,7 +2939,7 @@ class SolverTest
 
     for (int i = 0; i < indices.length; i++)
     {
-      Term selectorTerm = constructor.getSelector(indices[i]).getSelectorTerm();
+      Term selectorTerm = constructor.getSelector(indices[i]).getTerm();
       Term selectedTerm = d_solver.mkTerm(APPLY_SELECTOR, selectorTerm, tuple);
       Term simplifiedTerm = d_solver.simplify(selectedTerm);
       assertEquals(elements[indices[i]], simplifiedTerm);

diff --git a/test/unit/api/java/SortTest.java b/test/unit/api/java/SortTest.java
index bc3376ab7fb6f1b8d0f0e6d541ce88378a9ff9db..1396b27c7f264f18962e04b0b456256d113adae7 100644 (file)
--- a/test/unit/api/java/SortTest.java
+++ b/test/unit/api/java/SortTest.java
@@ -165,7 +165,7 @@ class SortTest
   {
     Sort dt_sort = create_datatype_sort();
     Datatype dt = dt_sort.getDatatype();
-    Sort cons_sort = dt.getConstructor(0).getConstructorTerm().getSort();
+    Sort cons_sort = dt.getConstructor(0).getTerm().getSort();
     assertTrue(cons_sort.isDatatypeConstructor());
     assertDoesNotThrow(() -> d_solver.getNullSort().isDatatypeConstructor());
   }
@@ -175,7 +175,7 @@ class SortTest
   {
     Sort dt_sort = create_datatype_sort();
     Datatype dt = dt_sort.getDatatype();
-    Sort cons_sort = dt.getConstructor(0).getSelector(1).getSelectorTerm().getSort();
+    Sort cons_sort = dt.getConstructor(0).getSelector(1).getTerm().getSort();
     assertTrue(cons_sort.isDatatypeSelector());
     assertDoesNotThrow(() -> d_solver.getNullSort().isDatatypeSelector());
   }
@@ -294,7 +294,7 @@ class SortTest
 
     // get constructor
     DatatypeConstructor dcons = dt.getConstructor(0);
-    Term consTerm = dcons.getConstructorTerm();
+    Term consTerm = dcons.getTerm();
     Sort consSort = consTerm.getSort();
     assertTrue(consSort.isDatatypeConstructor());
     assertFalse(consSort.isDatatypeTester());
@@ -316,7 +316,7 @@ class SortTest
 
     // get selector
     DatatypeSelector dselTail = dcons.getSelector(1);
-    Term tailTerm = dselTail.getSelectorTerm();
+    Term tailTerm = dselTail.getTerm();
     assertTrue(tailTerm.getSort().isDatatypeSelector());
     assertEquals(tailTerm.getSort().getDatatypeSelectorDomainSort(), dtypeSort);
     assertEquals(tailTerm.getSort().getDatatypeSelectorCodomainSort(), dtypeSort);

diff --git a/test/unit/api/java/TermTest.java b/test/unit/api/java/TermTest.java
index 3ecddb82c35869a2c8fb8ef5058ab7702c6b6c6f..c8ee81f0a7e35d00c03b8e897ed79b31cc8859e4 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.getConstructor("cons").getConstructorTerm();
-    Term nilOpTerm = list.getConstructor("nil").getConstructorTerm();
+    Term consOpTerm = list.getConstructor("cons").getTerm();
+    Term nilOpTerm = list.getConstructor("nil").getTerm();
   }
 
   @Test

diff --git a/test/unit/api/python/test_datatype_api.py b/test/unit/api/python/test_datatype_api.py
index df448574166b87208d95f589806a8fa6159731cd..09d5ce05eacb146265895bb5c715314c1ce19d89 100644 (file)
--- a/test/unit/api/python/test_datatype_api.py
+++ b/test/unit/api/python/test_datatype_api.py
@@ -39,8 +39,8 @@ def test_mk_datatype_sort(solver):
     nilConstr = d[1]
     with pytest.raises(RuntimeError):
         d[2]
-    consConstr.getConstructorTerm()
-    nilConstr.getConstructorTerm()
+    consConstr.getTerm()
+    nilConstr.getTerm()
 
 def test_is_null(solver):
   # creating empty (null) objects.
@@ -203,7 +203,7 @@ def test_datatype_structs(solver):
     assert dt.isWellFounded()
     # get constructor
     dcons = dt[0]
-    consTerm = dcons.getConstructorTerm()
+    consTerm = dcons.getTerm()
     assert dcons.getNumSelectors() == 2
 
     # create datatype sort to test
@@ -558,7 +558,7 @@ def test_datatype_specialized_cons(solver):
     testConsTerm = Term(solver)
     # get the specialized constructor term for list[Int]
     testConsTerm = nilc.getInstantiatedConstructorTerm(listInt)
-    assert testConsTerm != nilc.getConstructorTerm()
+    assert testConsTerm != nilc.getTerm()
     # error to get the specialized constructor term for Int
     with pytest.raises(RuntimeError):
         nilc.getInstantiatedConstructorTerm(isort)

diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py
index fb09cdee24dfb74d6a383cac3f98801d64ab66a2..53821e1740a7a11b2fd0af08d1ad12270ce9ad93 100644 (file)
--- a/test/unit/api/python/test_solver.py
+++ b/test/unit/api/python/test_solver.py
@@ -177,7 +177,7 @@ def test_mk_datatype_sorts(solver):
     t1 = solver.mkConst(isort1, "t")
     t0 = solver.mkTerm(
         Kind.APPLY_SELECTOR,
-        t1.getSort().getDatatype().getSelector("s1").getSelectorTerm(),
+        t1.getSort().getDatatype().getSelector("s1").getTerm(),
         t1)
     assert dt_sorts[0].instantiate({solver.getBooleanSort()}) == t0.getSort()
 
@@ -827,10 +827,10 @@ def test_mk_term_from_op(solver):
     lis = listSort.getDatatype()
 
     # list datatype constructor and selector operator terms
-    consTerm = lis.getConstructor("cons").getConstructorTerm()
-    nilTerm = lis.getConstructor("nil").getConstructorTerm()
-    headTerm = lis["cons"].getSelector("head").getSelectorTerm()
-    tailTerm = lis["cons"]["tail"].getSelectorTerm()
+    consTerm = lis.getConstructor("cons").getTerm()
+    nilTerm = lis.getConstructor("nil").getTerm()
+    headTerm = lis["cons"].getSelector("head").getTerm()
+    tailTerm = lis["cons"]["tail"].getTerm()
 
     # mkTerm(Op op, Term term) const
     solver.mkTerm(Kind.APPLY_CONSTRUCTOR, nilTerm)
@@ -1157,9 +1157,9 @@ def test_get_op(solver):
     consListSort = solver.mkDatatypeSort(consListSpec)
     consList = consListSort.getDatatype()
 
-    consTerm = consList.getConstructor("cons").getConstructorTerm()
-    nilTerm = consList.getConstructor("nil").getConstructorTerm()
-    headTerm = consList["cons"].getSelector("head").getSelectorTerm()
+    consTerm = consList.getConstructor("cons").getTerm()
+    nilTerm = consList.getConstructor("nil").getTerm()
+    headTerm = consList["cons"].getSelector("head").getTerm()
 
     listnil = solver.mkTerm(Kind.APPLY_CONSTRUCTOR, nilTerm)
     listcons1 = solver.mkTerm(Kind.APPLY_CONSTRUCTOR, consTerm,
@@ -1724,15 +1724,15 @@ def test_simplify(solver):
     consList = consListSort.getDatatype()
     dt1 = solver.mkTerm(
         Kind.APPLY_CONSTRUCTOR,
-        consList.getConstructor("cons").getConstructorTerm(),
+        consList.getConstructor("cons").getTerm(),
         solver.mkInteger(0),
         solver.mkTerm(
             Kind.APPLY_CONSTRUCTOR,
-            consList.getConstructor("nil").getConstructorTerm()))
+            consList.getConstructor("nil").getTerm()))
     solver.simplify(dt1)
     dt2 = solver.mkTerm(
       Kind.APPLY_SELECTOR,
-      consList["cons"].getSelector("head").getSelectorTerm(),
+      consList["cons"].getSelector("head").getTerm(),
       dt1)
     solver.simplify(dt2)
 
@@ -2589,7 +2589,7 @@ def test_tuple_project(solver):
 
     for i in indices:
 
-        selectorTerm = constructor[i].getSelectorTerm()
+        selectorTerm = constructor[i].getTerm()
         selectedTerm = solver.mkTerm(Kind.APPLY_SELECTOR, selectorTerm, tuple)
         simplifiedTerm = solver.simplify(selectedTerm)
         assert elements[i] == simplifiedTerm

diff --git a/test/unit/api/python/test_sort.py b/test/unit/api/python/test_sort.py
index c6168d17ff41874fd7f7bdb113e4854f80fe611e..77800d69eebbe0585bd01ae0c076e1d70a4aa803 100644 (file)
--- a/test/unit/api/python/test_sort.py
+++ b/test/unit/api/python/test_sort.py
@@ -136,7 +136,7 @@ def test_is_datatype(solver):
 def test_is_constructor(solver):
     dt_sort = create_datatype_sort(solver)
     dt = dt_sort.getDatatype()
-    cons_sort = dt[0].getConstructorTerm().getSort()
+    cons_sort = dt[0].getTerm().getSort()
     assert cons_sort.isDatatypeConstructor()
     Sort(solver).isDatatypeConstructor()
 
@@ -146,7 +146,7 @@ def test_is_selector(solver):
     dt = dt_sort.getDatatype()
     dt0 = dt[0]
     dt01 = dt0[1]
-    cons_sort = dt01.getSelectorTerm().getSort()
+    cons_sort = dt01.getTerm().getSort()
     assert cons_sort.isDatatypeSelector()
     Sort(solver).isDatatypeSelector()
 
@@ -250,7 +250,7 @@ def test_datatype_sorts(solver):
 
     # get constructor
     dcons = dt[0]
-    consTerm = dcons.getConstructorTerm()
+    consTerm = dcons.getTerm()
     consSort = consTerm.getSort()
     assert consSort.isDatatypeConstructor()
     assert not consSort.isDatatypeTester()
@@ -275,7 +275,7 @@ def test_datatype_sorts(solver):
 
     # get selector
     dselTail = dcons[1]
-    tailTerm = dselTail.getSelectorTerm()
+    tailTerm = dselTail.getTerm()
     assert tailTerm.getSort().isDatatypeSelector()
     assert tailTerm.getSort().getDatatypeSelectorDomainSort() == dtypeSort
     assert tailTerm.getSort().getDatatypeSelectorCodomainSort() == dtypeSort

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