OpTerm Refactor: Allow retrieving OpTerm used to create Term in public C++ API (#3355)

* Treat uninterpreted functions as a child in Term iteration

* Remove unnecessary const_iterator constructor

* Add parameter comments to const_iterator constructor

* Use operator[] instead of storing a vector of Expr children

* Switch pos member variable from int to uint32_t

* Add comment about how UFs are treated in iteration

* Allow OpTerm to contain a single Kind, update OpTerm construction

* Update mkTerm to use only an OpTerm (and not also a Kind)

* Remove unnecessary function checkMkOpTerm

* Update mkOpTerm comments to not use _OP Kinds

* Update examples to use new mkTerm

* First pass on fixing unit test

* Override kind for Constructor and Selector Terms

* More fixes to unit tests

* Updates to parser

* Remove old assert (for Kind, OpTerm pattern which was removed)

* Remove *_OP kinds from public API

* Add hasOpTerm and getOpTerm methods to Term

* Add test for UF iteration

* Add unit test for getOpTerm

* Move OpTerm implementation above Term implemenation to match header file

Moved in header because Term::getOpTerm() returns an OpTerm and the compiler complains
if OpTerm is not defined earlier. Simply moving the declaration is easier/cleaner than
forward declaring within the same file that it's declared.

* Fix mkTerm in datatypes-new.cpp example

* Use helper function for creating term from Kind to avoid nested API calls

* Rename: OpTerm->Op in API

* Update OpTerm->Op in examples/tests/parser

* Add case for APPLY_TESTER

* operator term -> operator

* Update src/api/cvc4cpp.h

Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com>

* Comment comment suggestion

Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com>

* Add not-null checks and implement Op from a single Kind constructor

* Undo sed mistake for OpTerm replacement

* Add 'd_' prefix to member vars

* Fix comment and remove old commented-out code

* Formatting

* Revert "Formatting"

This reverts commit d1d5fc1fb71496daeba668e97cad84c213200ba9.

* More fixes for sed mistakes

* Minor formatting

* Undo changes in CVC parser

* Add isIndexed and prefix with d_

* Create helper function for isIndexed to avoid calling API functions in other API functions

3 files changed, 199 insertions, 147 deletions

diff --git a/test/unit/api/opterm_black.h b/test/unit/api/opterm_black.h
index 150cebcbf..0dd7587ff 100644
--- a/test/unit/api/opterm_black.h
+++ b/test/unit/api/opterm_black.h
@@ -18,7 +18,7 @@
 
 using namespace CVC4::api;
 
-class OpTermBlack : public CxxTest::TestSuite
+class OpBlack : public CxxTest::TestSuite
 {
  public:
   void setUp() override {}
@@ -27,6 +27,7 @@ class OpTermBlack : public CxxTest::TestSuite
   void testGetKind();
   void testGetSort();
   void testIsNull();
+  void testOpTermFromKind();
   void testGetIndicesString();
   void testGetIndicesKind();
   void testGetIndicesUint();
@@ -36,168 +37,173 @@ class OpTermBlack : public CxxTest::TestSuite
   Solver d_solver;
 };
 
-void OpTermBlack::testGetKind()
+void OpBlack::testGetKind()
 {
-  OpTerm x;
+  Op x;
   TS_ASSERT_THROWS(x.getSort(), CVC4ApiException&);
-  x = d_solver.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 1);
+  x = d_solver.mkOp(BITVECTOR_EXTRACT, 31, 1);
   TS_ASSERT_THROWS_NOTHING(x.getKind());
 }
 
-void OpTermBlack::testGetSort()
+void OpBlack::testGetSort()
 {
-  OpTerm x;
+  Op x;
   TS_ASSERT_THROWS(x.getSort(), CVC4ApiException&);
-  x = d_solver.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 1);
+  x = d_solver.mkOp(BITVECTOR_EXTRACT, 31, 1);
   TS_ASSERT_THROWS_NOTHING(x.getSort());
 }
 
-void OpTermBlack::testIsNull()
+void OpBlack::testIsNull()
 {
-  OpTerm x;
+  Op x;
   TS_ASSERT(x.isNull());
-  x = d_solver.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 1);
+  x = d_solver.mkOp(BITVECTOR_EXTRACT, 31, 1);
   TS_ASSERT(!x.isNull());
 }
 
-void OpTermBlack::testGetIndicesString()
+void OpBlack::testOpTermFromKind()
 {
-  OpTerm x;
+  Op plus(PLUS);
+  TS_ASSERT(!plus.isIndexed());
+  TS_ASSERT_THROWS(plus.getIndices<uint32_t>(), CVC4ApiException&);
+}
+
+void OpBlack::testGetIndicesString()
+{
+  Op x;
   TS_ASSERT_THROWS(x.getIndices<std::string>(), CVC4ApiException&);
 
-  OpTerm divisible_ot = d_solver.mkOpTerm(DIVISIBLE_OP, 4);
+  Op divisible_ot = d_solver.mkOp(DIVISIBLE, 4);
+  TS_ASSERT(divisible_ot.isIndexed());
   std::string divisible_idx = divisible_ot.getIndices<std::string>();
   TS_ASSERT(divisible_idx == "4");
 
-  OpTerm record_update_ot = d_solver.mkOpTerm(RECORD_UPDATE_OP, "test");
+  Op record_update_ot = d_solver.mkOp(RECORD_UPDATE, "test");
   std::string record_update_idx = record_update_ot.getIndices<std::string>();
   TS_ASSERT(record_update_idx == "test");
   TS_ASSERT_THROWS(record_update_ot.getIndices<uint32_t>(), CVC4ApiException&);
 }
 
-void OpTermBlack::testGetIndicesKind()
+void OpBlack::testGetIndicesKind()
 {
-  OpTerm chain_ot = d_solver.mkOpTerm(CHAIN_OP, AND);
+  Op chain_ot = d_solver.mkOp(CHAIN, AND);
+  TS_ASSERT(chain_ot.isIndexed());
   Kind chain_idx = chain_ot.getIndices<Kind>();
   TS_ASSERT(chain_idx == AND);
 }
 
-void OpTermBlack::testGetIndicesUint()
+void OpBlack::testGetIndicesUint()
 {
-  OpTerm bitvector_repeat_ot = d_solver.mkOpTerm(BITVECTOR_REPEAT_OP, 5);
+  Op bitvector_repeat_ot = d_solver.mkOp(BITVECTOR_REPEAT, 5);
+  TS_ASSERT(bitvector_repeat_ot.isIndexed());
   uint32_t bitvector_repeat_idx = bitvector_repeat_ot.getIndices<uint32_t>();
   TS_ASSERT(bitvector_repeat_idx == 5);
   TS_ASSERT_THROWS(
       (bitvector_repeat_ot.getIndices<std::pair<uint32_t, uint32_t>>()),
       CVC4ApiException&);
 
-  OpTerm bitvector_zero_extend_ot =
-      d_solver.mkOpTerm(BITVECTOR_ZERO_EXTEND_OP, 6);
+  Op bitvector_zero_extend_ot = d_solver.mkOp(BITVECTOR_ZERO_EXTEND, 6);
   uint32_t bitvector_zero_extend_idx =
       bitvector_zero_extend_ot.getIndices<uint32_t>();
   TS_ASSERT(bitvector_zero_extend_idx == 6);
 
-  OpTerm bitvector_sign_extend_ot =
-      d_solver.mkOpTerm(BITVECTOR_SIGN_EXTEND_OP, 7);
+  Op bitvector_sign_extend_ot = d_solver.mkOp(BITVECTOR_SIGN_EXTEND, 7);
   uint32_t bitvector_sign_extend_idx =
       bitvector_sign_extend_ot.getIndices<uint32_t>();
   TS_ASSERT(bitvector_sign_extend_idx == 7);
 
-  OpTerm bitvector_rotate_left_ot =
-      d_solver.mkOpTerm(BITVECTOR_ROTATE_LEFT_OP, 8);
+  Op bitvector_rotate_left_ot = d_solver.mkOp(BITVECTOR_ROTATE_LEFT, 8);
   uint32_t bitvector_rotate_left_idx =
       bitvector_rotate_left_ot.getIndices<uint32_t>();
   TS_ASSERT(bitvector_rotate_left_idx == 8);
 
-  OpTerm bitvector_rotate_right_ot =
-      d_solver.mkOpTerm(BITVECTOR_ROTATE_RIGHT_OP, 9);
+  Op bitvector_rotate_right_ot = d_solver.mkOp(BITVECTOR_ROTATE_RIGHT, 9);
   uint32_t bitvector_rotate_right_idx =
       bitvector_rotate_right_ot.getIndices<uint32_t>();
   TS_ASSERT(bitvector_rotate_right_idx == 9);
 
-  OpTerm int_to_bitvector_ot = d_solver.mkOpTerm(INT_TO_BITVECTOR_OP, 10);
+  Op int_to_bitvector_ot = d_solver.mkOp(INT_TO_BITVECTOR, 10);
   uint32_t int_to_bitvector_idx = int_to_bitvector_ot.getIndices<uint32_t>();
   TS_ASSERT(int_to_bitvector_idx == 10);
 
-  OpTerm floatingpoint_to_ubv_ot =
-      d_solver.mkOpTerm(FLOATINGPOINT_TO_UBV_OP, 11);
+  Op floatingpoint_to_ubv_ot = d_solver.mkOp(FLOATINGPOINT_TO_UBV, 11);
   uint32_t floatingpoint_to_ubv_idx =
       floatingpoint_to_ubv_ot.getIndices<uint32_t>();
   TS_ASSERT(floatingpoint_to_ubv_idx == 11);
 
-  OpTerm floatingpoint_to_ubv_total_ot =
-      d_solver.mkOpTerm(FLOATINGPOINT_TO_UBV_TOTAL_OP, 12);
+  Op floatingpoint_to_ubv_total_ot =
+      d_solver.mkOp(FLOATINGPOINT_TO_UBV_TOTAL, 12);
   uint32_t floatingpoint_to_ubv_total_idx =
       floatingpoint_to_ubv_total_ot.getIndices<uint32_t>();
   TS_ASSERT(floatingpoint_to_ubv_total_idx == 12);
 
-  OpTerm floatingpoint_to_sbv_ot =
-      d_solver.mkOpTerm(FLOATINGPOINT_TO_SBV_OP, 13);
+  Op floatingpoint_to_sbv_ot = d_solver.mkOp(FLOATINGPOINT_TO_SBV, 13);
   uint32_t floatingpoint_to_sbv_idx =
       floatingpoint_to_sbv_ot.getIndices<uint32_t>();
   TS_ASSERT(floatingpoint_to_sbv_idx == 13);
 
-  OpTerm floatingpoint_to_sbv_total_ot =
-      d_solver.mkOpTerm(FLOATINGPOINT_TO_SBV_TOTAL_OP, 14);
+  Op floatingpoint_to_sbv_total_ot =
+      d_solver.mkOp(FLOATINGPOINT_TO_SBV_TOTAL, 14);
   uint32_t floatingpoint_to_sbv_total_idx =
       floatingpoint_to_sbv_total_ot.getIndices<uint32_t>();
   TS_ASSERT(floatingpoint_to_sbv_total_idx == 14);
 
-  OpTerm tuple_update_ot = d_solver.mkOpTerm(TUPLE_UPDATE_OP, 5);
+  Op tuple_update_ot = d_solver.mkOp(TUPLE_UPDATE, 5);
   uint32_t tuple_update_idx = tuple_update_ot.getIndices<uint32_t>();
   TS_ASSERT(tuple_update_idx == 5);
   TS_ASSERT_THROWS(tuple_update_ot.getIndices<std::string>(),
                    CVC4ApiException&);
 }
 
-void OpTermBlack::testGetIndicesPairUint()
+void OpBlack::testGetIndicesPairUint()
 {
-  OpTerm bitvector_extract_ot = d_solver.mkOpTerm(BITVECTOR_EXTRACT_OP, 4, 0);
+  Op bitvector_extract_ot = d_solver.mkOp(BITVECTOR_EXTRACT, 4, 0);
+  TS_ASSERT(bitvector_extract_ot.isIndexed());
   std::pair<uint32_t, uint32_t> bitvector_extract_indices =
       bitvector_extract_ot.getIndices<std::pair<uint32_t, uint32_t>>();
   TS_ASSERT((bitvector_extract_indices == std::pair<uint32_t, uint32_t>{4, 0}));
 
-  OpTerm floatingpoint_to_fp_ieee_bitvector_ot =
-      d_solver.mkOpTerm(FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP, 4, 25);
+  Op floatingpoint_to_fp_ieee_bitvector_ot =
+      d_solver.mkOp(FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, 4, 25);
   std::pair<uint32_t, uint32_t> floatingpoint_to_fp_ieee_bitvector_indices =
       floatingpoint_to_fp_ieee_bitvector_ot
           .getIndices<std::pair<uint32_t, uint32_t>>();
   TS_ASSERT((floatingpoint_to_fp_ieee_bitvector_indices
              == std::pair<uint32_t, uint32_t>{4, 25}));
 
-  OpTerm floatingpoint_to_fp_floatingpoint_ot =
-      d_solver.mkOpTerm(FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP, 4, 25);
+  Op floatingpoint_to_fp_floatingpoint_ot =
+      d_solver.mkOp(FLOATINGPOINT_TO_FP_FLOATINGPOINT, 4, 25);
   std::pair<uint32_t, uint32_t> floatingpoint_to_fp_floatingpoint_indices =
       floatingpoint_to_fp_floatingpoint_ot
           .getIndices<std::pair<uint32_t, uint32_t>>();
   TS_ASSERT((floatingpoint_to_fp_floatingpoint_indices
              == std::pair<uint32_t, uint32_t>{4, 25}));
 
-  OpTerm floatingpoint_to_fp_real_ot =
-      d_solver.mkOpTerm(FLOATINGPOINT_TO_FP_REAL_OP, 4, 25);
+  Op floatingpoint_to_fp_real_ot =
+      d_solver.mkOp(FLOATINGPOINT_TO_FP_REAL, 4, 25);
   std::pair<uint32_t, uint32_t> floatingpoint_to_fp_real_indices =
       floatingpoint_to_fp_real_ot.getIndices<std::pair<uint32_t, uint32_t>>();
   TS_ASSERT((floatingpoint_to_fp_real_indices
              == std::pair<uint32_t, uint32_t>{4, 25}));
 
-  OpTerm floatingpoint_to_fp_signed_bitvector_ot =
-      d_solver.mkOpTerm(FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP, 4, 25);
+  Op floatingpoint_to_fp_signed_bitvector_ot =
+      d_solver.mkOp(FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, 4, 25);
   std::pair<uint32_t, uint32_t> floatingpoint_to_fp_signed_bitvector_indices =
       floatingpoint_to_fp_signed_bitvector_ot
           .getIndices<std::pair<uint32_t, uint32_t>>();
   TS_ASSERT((floatingpoint_to_fp_signed_bitvector_indices
              == std::pair<uint32_t, uint32_t>{4, 25}));
 
-  OpTerm floatingpoint_to_fp_unsigned_bitvector_ot =
-      d_solver.mkOpTerm(FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP, 4, 25);
+  Op floatingpoint_to_fp_unsigned_bitvector_ot =
+      d_solver.mkOp(FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, 4, 25);
   std::pair<uint32_t, uint32_t> floatingpoint_to_fp_unsigned_bitvector_indices =
       floatingpoint_to_fp_unsigned_bitvector_ot
           .getIndices<std::pair<uint32_t, uint32_t>>();
   TS_ASSERT((floatingpoint_to_fp_unsigned_bitvector_indices
              == std::pair<uint32_t, uint32_t>{4, 25}));
 
-  OpTerm floatingpoint_to_fp_generic_ot =
-      d_solver.mkOpTerm(FLOATINGPOINT_TO_FP_GENERIC_OP, 4, 25);
+  Op floatingpoint_to_fp_generic_ot =
+      d_solver.mkOp(FLOATINGPOINT_TO_FP_GENERIC, 4, 25);
   std::pair<uint32_t, uint32_t> floatingpoint_to_fp_generic_indices =
       floatingpoint_to_fp_generic_ot
           .getIndices<std::pair<uint32_t, uint32_t>>();
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 374a3ff2a..92313ac3c 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -40,7 +40,7 @@ class SolverBlack : public CxxTest::TestSuite
   void testMkFloatingPointSort();
   void testMkDatatypeSort();
   void testMkFunctionSort();
-  void testMkOpTerm();
+  void testMkOp();
   void testMkParamSort();
   void testMkPredicateSort();
   void testMkRecordSort();
@@ -70,7 +70,7 @@ class SolverBlack : public CxxTest::TestSuite
   void testMkSepNil();
   void testMkString();
   void testMkTerm();
-  void testMkTermFromOpTerm();
+  void testMkTermFromOp();
   void testMkTrue();
   void testMkTuple();
   void testMkUninterpretedConst();
@@ -85,6 +85,9 @@ class SolverBlack : public CxxTest::TestSuite
   void testDefineFunRec();
   void testDefineFunsRec();
 
+  void testUFIteration();
+  void testGetOp();
+
   void testPush1();
   void testPush2();
   void testPop1();
@@ -453,29 +456,27 @@ void SolverBlack::testMkPosZero()
   }
 }
 
-void SolverBlack::testMkOpTerm()
+void SolverBlack::testMkOp()
 {
-  // mkOpTerm(Kind kind, Kind k)
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkOpTerm(CHAIN_OP, EQUAL));
-  TS_ASSERT_THROWS(d_solver->mkOpTerm(BITVECTOR_EXTRACT_OP, EQUAL),
-                   CVC4ApiException&);
+  // mkOp(Kind kind, Kind k)
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkOp(CHAIN, EQUAL));
+  TS_ASSERT_THROWS(d_solver->mkOp(BITVECTOR_EXTRACT, EQUAL), CVC4ApiException&);
 
-  // mkOpTerm(Kind kind, const std::string& arg)
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkOpTerm(RECORD_UPDATE_OP, "asdf"));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkOpTerm(DIVISIBLE_OP, "2147483648"));
-  TS_ASSERT_THROWS(d_solver->mkOpTerm(BITVECTOR_EXTRACT_OP, "asdf"),
+  // mkOp(Kind kind, const std::string& arg)
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkOp(RECORD_UPDATE, "asdf"));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkOp(DIVISIBLE, "2147483648"));
+  TS_ASSERT_THROWS(d_solver->mkOp(BITVECTOR_EXTRACT, "asdf"),
                    CVC4ApiException&);
 
-  // mkOpTerm(Kind kind, uint32_t arg)
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkOpTerm(DIVISIBLE_OP, 1));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkOpTerm(BITVECTOR_ROTATE_LEFT_OP, 1));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkOpTerm(BITVECTOR_ROTATE_RIGHT_OP, 1));
-  TS_ASSERT_THROWS(d_solver->mkOpTerm(BITVECTOR_EXTRACT_OP, 1),
-                   CVC4ApiException&);
+  // mkOp(Kind kind, uint32_t arg)
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkOp(DIVISIBLE, 1));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkOp(BITVECTOR_ROTATE_LEFT, 1));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkOp(BITVECTOR_ROTATE_RIGHT, 1));
+  TS_ASSERT_THROWS(d_solver->mkOp(BITVECTOR_EXTRACT, 1), CVC4ApiException&);
 
-  // mkOpTerm(Kind kind, uint32_t arg1, uint32_t arg2)
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkOpTerm(BITVECTOR_EXTRACT_OP, 1, 1));
-  TS_ASSERT_THROWS(d_solver->mkOpTerm(DIVISIBLE_OP, 1, 2), CVC4ApiException&);
+  // mkOp(Kind kind, uint32_t arg1, uint32_t arg2)
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkOp(BITVECTOR_EXTRACT, 1, 1));
+  TS_ASSERT_THROWS(d_solver->mkOp(DIVISIBLE, 1, 2), CVC4ApiException&);
 }
 
 void SolverBlack::testMkPi() { TS_ASSERT_THROWS_NOTHING(d_solver->mkPi()); }
@@ -611,7 +612,7 @@ void SolverBlack::testMkTerm()
   TS_ASSERT_THROWS(d_solver->mkTerm(DISTINCT, v6), CVC4ApiException&);
 }
 
-void SolverBlack::testMkTermFromOpTerm()
+void SolverBlack::testMkTermFromOp()
 {
   Sort bv32 = d_solver->mkBitVectorSort(32);
   Term a = d_solver->mkConst(bv32, "a");
@@ -620,9 +621,9 @@ void SolverBlack::testMkTermFromOpTerm()
   std::vector<Term> v2 = {d_solver->mkReal(1), Term()};
   std::vector<Term> v3 = {};
   // simple operator terms
-  OpTerm opterm1 = d_solver->mkOpTerm(BITVECTOR_EXTRACT_OP, 2, 1);
-  OpTerm opterm2 = d_solver->mkOpTerm(DIVISIBLE_OP, 1);
-  OpTerm opterm3 = d_solver->mkOpTerm(CHAIN_OP, EQUAL);
+  Op opterm1 = d_solver->mkOp(BITVECTOR_EXTRACT, 2, 1);
+  Op opterm2 = d_solver->mkOp(DIVISIBLE, 1);
+  Op opterm3 = d_solver->mkOp(CHAIN, EQUAL);
   // list datatype
 
   Sort sort = d_solver->mkParamSort("T");
@@ -641,80 +642,60 @@ void SolverBlack::testMkTermFromOpTerm()
   Term c = d_solver->mkConst(intListSort, "c");
   Datatype list = listSort.getDatatype();
   // list datatype constructor and selector operator terms
-  OpTerm consTerm1 = list.getConstructorTerm("cons");
-  OpTerm consTerm2 = list.getConstructor("cons").getConstructorTerm();
-  OpTerm nilTerm1 = list.getConstructorTerm("nil");
-  OpTerm nilTerm2 = list.getConstructor("nil").getConstructorTerm();
-  OpTerm headTerm1 = list["cons"].getSelectorTerm("head");
-  OpTerm headTerm2 = list["cons"].getSelector("head").getSelectorTerm();
-  OpTerm tailTerm1 = list["cons"].getSelectorTerm("tail");
-  OpTerm tailTerm2 = list["cons"]["tail"].getSelectorTerm();
-
-  // mkTerm(Kind kind, OpTerm opTerm) const
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm1));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm2));
-  TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm1),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm2),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_CONSTRUCTOR, opterm1),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_SELECTOR, headTerm1),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_SELECTOR, tailTerm2),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkTerm(BITVECTOR_EXTRACT, opterm1),
+  Op consTerm1 = list.getConstructorTerm("cons");
+  Op consTerm2 = list.getConstructor("cons").getConstructorTerm();
+  Op nilTerm1 = list.getConstructorTerm("nil");
+  Op nilTerm2 = list.getConstructor("nil").getConstructorTerm();
+  Op headTerm1 = list["cons"].getSelectorTerm("head");
+  Op headTerm2 = list["cons"].getSelector("head").getSelectorTerm();
+  Op tailTerm1 = list["cons"].getSelectorTerm("tail");
+  Op tailTerm2 = list["cons"]["tail"].getSelectorTerm();
+
+  // mkTerm(Kind kind, Op op) const
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(nilTerm1));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(nilTerm2));
+  TS_ASSERT_THROWS(d_solver->mkTerm(consTerm1), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkTerm(consTerm2), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkTerm(opterm1), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkTerm(headTerm1), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkTerm(tailTerm2), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkTerm(opterm1), CVC4ApiException&);
+
+  // mkTerm(Kind kind, Op op, Term child) const
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm1, a));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm2, d_solver->mkReal(1)));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(headTerm1, c));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(tailTerm2, c));
+  TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, a), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, Term()), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkTerm(consTerm1, d_solver->mkReal(0)),
                    CVC4ApiException&);
 
-  // mkTerm(Kind kind, OpTerm opTerm, Term child) const
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(BITVECTOR_EXTRACT, opterm1, a));
+  // mkTerm(Kind kind, Op op, Term child1, Term child2) const
   TS_ASSERT_THROWS_NOTHING(
-      d_solver->mkTerm(DIVISIBLE, opterm2, d_solver->mkReal(1)));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_SELECTOR, headTerm1, c));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_SELECTOR, tailTerm2, c));
-  TS_ASSERT_THROWS(d_solver->mkTerm(DIVISIBLE, opterm1, a), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkTerm(DIVISIBLE, opterm2, a), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkTerm(BITVECTOR_EXTRACT, opterm1, Term()),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(
-      d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm1, d_solver->mkReal(0)),
-      CVC4ApiException&);
-
-  // mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2) const
+      d_solver->mkTerm(opterm3, d_solver->mkReal(1), d_solver->mkReal(2)));
   TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(
-      CHAIN, opterm3, d_solver->mkReal(1), d_solver->mkReal(2)));
-  TS_ASSERT_THROWS_NOTHING(
-      d_solver->mkTerm(APPLY_CONSTRUCTOR,
-                       consTerm1,
-                       d_solver->mkReal(0),
-                       d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm1)));
-  TS_ASSERT_THROWS(d_solver->mkTerm(BITVECTOR_EXTRACT, opterm1, a, b),
+      consTerm1, d_solver->mkReal(0), d_solver->mkTerm(nilTerm1)));
+  TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, a, b), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkTerm(opterm3, d_solver->mkReal(1), Term()),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkTerm(opterm3, Term(), d_solver->mkReal(1)),
                    CVC4ApiException&);
-  TS_ASSERT_THROWS(
-      d_solver->mkTerm(CHAIN, opterm3, d_solver->mkReal(1), Term()),
-      CVC4ApiException&);
-  TS_ASSERT_THROWS(
-      d_solver->mkTerm(CHAIN, opterm3, Term(), d_solver->mkReal(1)),
-      CVC4ApiException&);
 
-  // mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2, Term child3)
+  // mkTerm(Kind kind, Op op, Term child1, Term child2, Term child3)
   // const
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(CHAIN,
-                                            opterm3,
-                                            d_solver->mkReal(1),
-                                            d_solver->mkReal(1),
-                                            d_solver->mkReal(2)));
-  TS_ASSERT_THROWS(d_solver->mkTerm(BITVECTOR_EXTRACT, opterm1, a, b, a),
-                   CVC4ApiException&);
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(
+      opterm3, d_solver->mkReal(1), d_solver->mkReal(1), d_solver->mkReal(2)));
+  TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, a, b, a), CVC4ApiException&);
   TS_ASSERT_THROWS(
       d_solver->mkTerm(
-          CHAIN, opterm3, d_solver->mkReal(1), d_solver->mkReal(1), Term()),
+          opterm3, d_solver->mkReal(1), d_solver->mkReal(1), Term()),
       CVC4ApiException&);
 
-  // mkTerm(OpTerm opTerm, const std::vector<Term>& children) const
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(CHAIN, opterm3, v1));
-  TS_ASSERT_THROWS(d_solver->mkTerm(CHAIN, opterm3, v2), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkTerm(CHAIN, opterm3, v3), CVC4ApiException&);
+  // mkTerm(Op op, const std::vector<Term>& children) const
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm3, v1));
+  TS_ASSERT_THROWS(d_solver->mkTerm(opterm3, v2), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkTerm(opterm3, v3), CVC4ApiException&);
 }
 
 void SolverBlack::testMkTrue()
@@ -916,6 +897,73 @@ void SolverBlack::testDefineFunsRec()
       CVC4ApiException&);
 }
 
+void SolverBlack::testUFIteration()
+{
+  Sort intSort = d_solver->getIntegerSort();
+  Sort funSort = d_solver->mkFunctionSort({intSort, intSort}, intSort);
+  Term x = d_solver->mkConst(intSort, "x");
+  Term y = d_solver->mkConst(intSort, "y");
+  Term f = d_solver->mkConst(funSort, "f");
+  Term fxy = d_solver->mkTerm(APPLY_UF, f, x, y);
+
+  // Expecting the uninterpreted function to be one of the children
+  Term expected_children[3] = {f, x, y};
+  uint32_t idx = 0;
+  for (auto c : fxy)
+  {
+    TS_ASSERT(idx < 3);
+    TS_ASSERT(c == expected_children[idx]);
+    idx++;
+  }
+}
+
+void SolverBlack::testGetOp()
+{
+  Sort bv32 = d_solver->mkBitVectorSort(32);
+  Term a = d_solver->mkConst(bv32, "a");
+  Op ext = d_solver->mkOp(BITVECTOR_EXTRACT, 2, 1);
+  Term exta = d_solver->mkTerm(ext, a);
+
+  TS_ASSERT(!a.hasOp());
+  TS_ASSERT_THROWS(a.getOp(), CVC4ApiException&);
+  TS_ASSERT(exta.hasOp());
+  TS_ASSERT_EQUALS(exta.getOp(), ext);
+
+  // Test Datatypes -- more complicated
+  DatatypeDecl consListSpec("list");
+  DatatypeConstructorDecl cons("cons");
+  DatatypeSelectorDecl head("head", d_solver->getIntegerSort());
+  DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort());
+  cons.addSelector(head);
+  cons.addSelector(tail);
+  consListSpec.addConstructor(cons);
+  DatatypeConstructorDecl nil("nil");
+  consListSpec.addConstructor(nil);
+  Sort consListSort = d_solver->mkDatatypeSort(consListSpec);
+  Datatype consList = consListSort.getDatatype();
+
+  Op consTerm = consList.getConstructorTerm("cons");
+  Op nilTerm = consList.getConstructorTerm("nil");
+  Op headTerm = consList["cons"].getSelectorTerm("head");
+
+  TS_ASSERT(consTerm.getKind() == APPLY_CONSTRUCTOR);
+  TS_ASSERT(nilTerm.getKind() == APPLY_CONSTRUCTOR);
+  TS_ASSERT(headTerm.getKind() == APPLY_SELECTOR);
+
+  Term listnil = d_solver->mkTerm(nilTerm);
+  Term listcons1 = d_solver->mkTerm(consTerm, d_solver->mkReal(1), listnil);
+  Term listhead = d_solver->mkTerm(headTerm, listcons1);
+
+  TS_ASSERT(listnil.hasOp());
+  TS_ASSERT_EQUALS(listnil.getOp(), nilTerm);
+
+  TS_ASSERT(listcons1.hasOp());
+  TS_ASSERT_EQUALS(listcons1.getOp(), consTerm);
+
+  TS_ASSERT(listhead.hasOp());
+  TS_ASSERT_EQUALS(listhead.getOp(), headTerm);
+}
+
 void SolverBlack::testPush1()
 {
   d_solver->setOption("incremental", "true");
@@ -1026,14 +1074,12 @@ void SolverBlack::testSimplify()
   TS_ASSERT(i1 == d_solver->simplify(i3));
 
   Datatype consList = consListSort.getDatatype();
-  Term dt1 = d_solver->mkTerm(
-      APPLY_CONSTRUCTOR,
-      consList.getConstructorTerm("cons"),
-      d_solver->mkReal(0),
-      d_solver->mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil")));
+  Term dt1 =
+      d_solver->mkTerm(consList.getConstructorTerm("cons"),
+                       d_solver->mkReal(0),
+                       d_solver->mkTerm(consList.getConstructorTerm("nil")));
   TS_ASSERT_THROWS_NOTHING(d_solver->simplify(dt1));
-  Term dt2 = d_solver->mkTerm(
-      APPLY_SELECTOR, consList["cons"].getSelectorTerm("head"), dt1);
+  Term dt2 = d_solver->mkTerm(consList["cons"].getSelectorTerm("head"), dt1);
   TS_ASSERT_THROWS_NOTHING(d_solver->simplify(dt2));
 
   Term b1 = d_solver->mkVar(bvSort, "b1");
diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h
index c5300dbfe..0d5400f5f 100644
--- a/test/unit/api/term_black.h
+++ b/test/unit/api/term_black.h
@@ -207,7 +207,7 @@ void TermBlack::testAndTerm()
 
   Term b = d_solver.mkTrue();
   TS_ASSERT_THROWS(Term().andTerm(b), CVC4ApiException&);
-  TS_ASSERT_THROWS(b.andTerm(Term()), CVC4ApiException&);  
+  TS_ASSERT_THROWS(b.andTerm(Term()), CVC4ApiException&);
   TS_ASSERT_THROWS_NOTHING(b.andTerm(b));
   Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
   TS_ASSERT_THROWS(x.andTerm(b), CVC4ApiException&);
@@ -471,7 +471,7 @@ void TermBlack::testImpTerm()
 
   Term b = d_solver.mkTrue();
   TS_ASSERT_THROWS(Term().impTerm(b), CVC4ApiException&);
-  TS_ASSERT_THROWS(b.impTerm(Term()), CVC4ApiException&);  
+  TS_ASSERT_THROWS(b.impTerm(Term()), CVC4ApiException&);
   TS_ASSERT_THROWS_NOTHING(b.impTerm(b));
   Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
   TS_ASSERT_THROWS(x.impTerm(b), CVC4ApiException&);
@@ -538,7 +538,7 @@ void TermBlack::testIteTerm()
   Term b = d_solver.mkTrue();
   TS_ASSERT_THROWS(Term().iteTerm(b, b), CVC4ApiException&);
   TS_ASSERT_THROWS(b.iteTerm(Term(), b), CVC4ApiException&);
-  TS_ASSERT_THROWS(b.iteTerm(b, Term()), CVC4ApiException&);    
+  TS_ASSERT_THROWS(b.iteTerm(b, Term()), CVC4ApiException&);
   TS_ASSERT_THROWS_NOTHING(b.iteTerm(b, b));
   Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
   TS_ASSERT_THROWS_NOTHING(b.iteTerm(x, x));