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

15 files changed, 1172 insertions, 1018 deletions

diff --git a/examples/api/bitvectors-new.cpp b/examples/api/bitvectors-new.cpp
index 58912a1bb..4578da733 100644
--- a/examples/api/bitvectors-new.cpp
+++ b/examples/api/bitvectors-new.cpp
@@ -114,8 +114,8 @@ int main()
   cout << " CVC4: " << slv.checkValidAssuming(v) << endl;
 
   // Assert that a is odd
-  OpTerm extract_op = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 0, 0);
-  Term lsb_of_a = slv.mkTerm(BITVECTOR_EXTRACT, extract_op, a);
+  Op extract_op = slv.mkOp(BITVECTOR_EXTRACT, 0, 0);
+  Term lsb_of_a = slv.mkTerm(extract_op, a);
   cout << "Sort of " << lsb_of_a << " is " << lsb_of_a.getSort() << endl;
   Term a_odd = slv.mkTerm(EQUAL, lsb_of_a, slv.mkBitVector(1u, 1u));
   cout << "Assert " << a_odd << endl;
diff --git a/examples/api/datatypes-new.cpp b/examples/api/datatypes-new.cpp
index efbd33645..9ff05ac0d 100644
--- a/examples/api/datatypes-new.cpp
+++ b/examples/api/datatypes-new.cpp
@@ -36,11 +36,9 @@ 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.getConstructorTerm("cons"),
-      slv.mkReal(0),
-      slv.mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil")));
+  Term t = slv.mkTerm(consList.getConstructorTerm("cons"),
+                      slv.mkReal(0),
+                      slv.mkTerm(consList.getConstructorTerm("nil")));
 
   std::cout << "t is " << t << std::endl
             << "sort of cons is "
@@ -53,8 +51,7 @@ void test(Solver& slv, Sort& consListSort)
   // 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"].getSelectorTerm("head"), t);
+  Term t2 = slv.mkTerm(consList["cons"].getSelectorTerm("head"), t);
 
   std::cout << "t2 is " << t2 << std::endl
             << "simplify(t2) is " << slv.simplify(t2) << std::endl
@@ -118,8 +115,7 @@ void test(Solver& slv, Sort& consListSort)
   Term a = slv.mkConst(paramConsIntListSort, "a");
   std::cout << "term " << a << " is of sort " << a.getSort() << std::endl;
 
-  Term head_a = slv.mkTerm(
-      APPLY_SELECTOR, paramConsList["cons"].getSelectorTerm("head"), a);
+  Term head_a = slv.mkTerm(paramConsList["cons"].getSelectorTerm("head"), a);
   std::cout << "head_a is " << head_a << " of sort " << head_a.getSort()
             << std::endl
             << "sort of cons is "
diff --git a/examples/api/extract-new.cpp b/examples/api/extract-new.cpp
index 0cb885b2c..0f0f8243a 100644
--- a/examples/api/extract-new.cpp
+++ b/examples/api/extract-new.cpp
@@ -30,17 +30,17 @@ int main()
 
   Term x = slv.mkConst(bitvector32, "a");
 
-  OpTerm ext_31_1 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 1);
-  Term x_31_1 = slv.mkTerm(BITVECTOR_EXTRACT, ext_31_1, x);
+  Op ext_31_1 = slv.mkOp(BITVECTOR_EXTRACT, 31, 1);
+  Term x_31_1 = slv.mkTerm(ext_31_1, x);
 
-  OpTerm ext_30_0 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 30, 0);
-  Term x_30_0 = slv.mkTerm(BITVECTOR_EXTRACT, ext_30_0, x);
+  Op ext_30_0 = slv.mkOp(BITVECTOR_EXTRACT, 30, 0);
+  Term x_30_0 = slv.mkTerm(ext_30_0, x);
 
-  OpTerm ext_31_31 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 31);
-  Term x_31_31 = slv.mkTerm(BITVECTOR_EXTRACT, ext_31_31, x);
+  Op ext_31_31 = slv.mkOp(BITVECTOR_EXTRACT, 31, 31);
+  Term x_31_31 = slv.mkTerm(ext_31_31, x);
 
-  OpTerm ext_0_0 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 0, 0);
-  Term x_0_0 = slv.mkTerm(BITVECTOR_EXTRACT, ext_0_0, x);
+  Op ext_0_0 = slv.mkOp(BITVECTOR_EXTRACT, 0, 0);
+  Term x_0_0 = slv.mkTerm(ext_0_0, x);
 
   Term eq = slv.mkTerm(EQUAL, x_31_1, x_30_0);
   cout << " Asserting: " << eq << endl;
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 4bb772e9d..4fd3c4276 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -77,7 +77,6 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{
     {LAMBDA, CVC4::Kind::LAMBDA},
     {CHOICE, CVC4::Kind::CHOICE},
     {CHAIN, CVC4::Kind::CHAIN},
-    {CHAIN_OP, CVC4::Kind::CHAIN_OP},
     /* Boolean ------------------------------------------------------------- */
     {CONST_BOOLEAN, CVC4::Kind::CONST_BOOLEAN},
     {NOT, CVC4::Kind::NOT},
@@ -118,7 +117,6 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{
     {ARCSECANT, CVC4::Kind::ARCSECANT},
     {ARCCOTANGENT, CVC4::Kind::ARCCOTANGENT},
     {SQRT, CVC4::Kind::SQRT},
-    {DIVISIBLE_OP, CVC4::Kind::DIVISIBLE_OP},
     {CONST_RATIONAL, CVC4::Kind::CONST_RATIONAL},
     {LT, CVC4::Kind::LT},
     {LEQ, CVC4::Kind::LEQ},
@@ -166,19 +164,12 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{
     {BITVECTOR_ITE, CVC4::Kind::BITVECTOR_ITE},
     {BITVECTOR_REDOR, CVC4::Kind::BITVECTOR_REDOR},
     {BITVECTOR_REDAND, CVC4::Kind::BITVECTOR_REDAND},
-    {BITVECTOR_EXTRACT_OP, CVC4::Kind::BITVECTOR_EXTRACT_OP},
-    {BITVECTOR_REPEAT_OP, CVC4::Kind::BITVECTOR_REPEAT_OP},
-    {BITVECTOR_ZERO_EXTEND_OP, CVC4::Kind::BITVECTOR_ZERO_EXTEND_OP},
-    {BITVECTOR_SIGN_EXTEND_OP, CVC4::Kind::BITVECTOR_SIGN_EXTEND_OP},
-    {BITVECTOR_ROTATE_LEFT_OP, CVC4::Kind::BITVECTOR_ROTATE_LEFT_OP},
-    {BITVECTOR_ROTATE_RIGHT_OP, CVC4::Kind::BITVECTOR_ROTATE_RIGHT_OP},
     {BITVECTOR_EXTRACT, CVC4::Kind::BITVECTOR_EXTRACT},
     {BITVECTOR_REPEAT, CVC4::Kind::BITVECTOR_REPEAT},
     {BITVECTOR_ZERO_EXTEND, CVC4::Kind::BITVECTOR_ZERO_EXTEND},
     {BITVECTOR_SIGN_EXTEND, CVC4::Kind::BITVECTOR_SIGN_EXTEND},
     {BITVECTOR_ROTATE_LEFT, CVC4::Kind::BITVECTOR_ROTATE_LEFT},
     {BITVECTOR_ROTATE_RIGHT, CVC4::Kind::BITVECTOR_ROTATE_RIGHT},
-    {INT_TO_BITVECTOR_OP, CVC4::Kind::INT_TO_BITVECTOR_OP},
     {INT_TO_BITVECTOR, CVC4::Kind::INT_TO_BITVECTOR},
     {BITVECTOR_TO_NAT, CVC4::Kind::BITVECTOR_TO_NAT},
     /* FP ------------------------------------------------------------------ */
@@ -209,34 +200,17 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{
     {FLOATINGPOINT_ISNAN, CVC4::Kind::FLOATINGPOINT_ISNAN},
     {FLOATINGPOINT_ISNEG, CVC4::Kind::FLOATINGPOINT_ISNEG},
     {FLOATINGPOINT_ISPOS, CVC4::Kind::FLOATINGPOINT_ISPOS},
-    {FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP,
-     CVC4::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP},
-    {FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
-     CVC4::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR},
-    {FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP,
-     CVC4::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP},
     {FLOATINGPOINT_TO_FP_FLOATINGPOINT,
      CVC4::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT},
-    {FLOATINGPOINT_TO_FP_REAL_OP, CVC4::Kind::FLOATINGPOINT_TO_FP_REAL_OP},
     {FLOATINGPOINT_TO_FP_REAL, CVC4::Kind::FLOATINGPOINT_TO_FP_REAL},
-    {FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP,
-     CVC4::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP},
     {FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
      CVC4::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR},
-    {FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP,
-     CVC4::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP},
     {FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
      CVC4::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR},
-    {FLOATINGPOINT_TO_FP_GENERIC_OP,
-     CVC4::Kind::FLOATINGPOINT_TO_FP_GENERIC_OP},
     {FLOATINGPOINT_TO_FP_GENERIC, CVC4::Kind::FLOATINGPOINT_TO_FP_GENERIC},
-    {FLOATINGPOINT_TO_UBV_OP, CVC4::Kind::FLOATINGPOINT_TO_UBV_OP},
     {FLOATINGPOINT_TO_UBV, CVC4::Kind::FLOATINGPOINT_TO_UBV},
-    {FLOATINGPOINT_TO_UBV_TOTAL_OP, CVC4::Kind::FLOATINGPOINT_TO_UBV_TOTAL_OP},
     {FLOATINGPOINT_TO_UBV_TOTAL, CVC4::Kind::FLOATINGPOINT_TO_UBV_TOTAL},
-    {FLOATINGPOINT_TO_SBV_OP, CVC4::Kind::FLOATINGPOINT_TO_SBV_OP},
     {FLOATINGPOINT_TO_SBV, CVC4::Kind::FLOATINGPOINT_TO_SBV},
-    {FLOATINGPOINT_TO_SBV_TOTAL_OP, CVC4::Kind::FLOATINGPOINT_TO_SBV_TOTAL_OP},
     {FLOATINGPOINT_TO_SBV_TOTAL, CVC4::Kind::FLOATINGPOINT_TO_SBV_TOTAL},
     {FLOATINGPOINT_TO_REAL, CVC4::Kind::FLOATINGPOINT_TO_REAL},
     {FLOATINGPOINT_TO_REAL_TOTAL, CVC4::Kind::FLOATINGPOINT_TO_REAL_TOTAL},
@@ -249,9 +223,7 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{
     {APPLY_CONSTRUCTOR, CVC4::Kind::APPLY_CONSTRUCTOR},
     {APPLY_SELECTOR_TOTAL, CVC4::Kind::APPLY_SELECTOR_TOTAL},
     {APPLY_TESTER, CVC4::Kind::APPLY_TESTER},
-    {TUPLE_UPDATE_OP, CVC4::Kind::TUPLE_UPDATE_OP},
     {TUPLE_UPDATE, CVC4::Kind::TUPLE_UPDATE},
-    {RECORD_UPDATE_OP, CVC4::Kind::RECORD_UPDATE_OP},
     {RECORD_UPDATE, CVC4::Kind::RECORD_UPDATE},
     /* Separation Logic ---------------------------------------------------- */
     {SEP_NIL, CVC4::Kind::SEP_NIL},
@@ -323,7 +295,7 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction>
         {CVC4::Kind::LAMBDA, LAMBDA},
         {CVC4::Kind::CHOICE, CHOICE},
         {CVC4::Kind::CHAIN, CHAIN},
-        {CVC4::Kind::CHAIN_OP, CHAIN_OP},
+        {CVC4::Kind::CHAIN_OP, CHAIN},
         /* Boolean --------------------------------------------------------- */
         {CVC4::Kind::CONST_BOOLEAN, CONST_BOOLEAN},
         {CVC4::Kind::NOT, NOT},
@@ -364,7 +336,7 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction>
         {CVC4::Kind::ARCSECANT, ARCSECANT},
         {CVC4::Kind::ARCCOTANGENT, ARCCOTANGENT},
         {CVC4::Kind::SQRT, SQRT},
-        {CVC4::Kind::DIVISIBLE_OP, DIVISIBLE_OP},
+        {CVC4::Kind::DIVISIBLE_OP, DIVISIBLE},
         {CVC4::Kind::CONST_RATIONAL, CONST_RATIONAL},
         {CVC4::Kind::LT, LT},
         {CVC4::Kind::LEQ, LEQ},
@@ -412,19 +384,19 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction>
         {CVC4::Kind::BITVECTOR_ITE, BITVECTOR_ITE},
         {CVC4::Kind::BITVECTOR_REDOR, BITVECTOR_REDOR},
         {CVC4::Kind::BITVECTOR_REDAND, BITVECTOR_REDAND},
-        {CVC4::Kind::BITVECTOR_EXTRACT_OP, BITVECTOR_EXTRACT_OP},
-        {CVC4::Kind::BITVECTOR_REPEAT_OP, BITVECTOR_REPEAT_OP},
-        {CVC4::Kind::BITVECTOR_ZERO_EXTEND_OP, BITVECTOR_ZERO_EXTEND_OP},
-        {CVC4::Kind::BITVECTOR_SIGN_EXTEND_OP, BITVECTOR_SIGN_EXTEND_OP},
-        {CVC4::Kind::BITVECTOR_ROTATE_LEFT_OP, BITVECTOR_ROTATE_LEFT_OP},
-        {CVC4::Kind::BITVECTOR_ROTATE_RIGHT_OP, BITVECTOR_ROTATE_RIGHT_OP},
+        {CVC4::Kind::BITVECTOR_EXTRACT_OP, BITVECTOR_EXTRACT},
+        {CVC4::Kind::BITVECTOR_REPEAT_OP, BITVECTOR_REPEAT},
+        {CVC4::Kind::BITVECTOR_ZERO_EXTEND_OP, BITVECTOR_ZERO_EXTEND},
+        {CVC4::Kind::BITVECTOR_SIGN_EXTEND_OP, BITVECTOR_SIGN_EXTEND},
+        {CVC4::Kind::BITVECTOR_ROTATE_LEFT_OP, BITVECTOR_ROTATE_LEFT},
+        {CVC4::Kind::BITVECTOR_ROTATE_RIGHT_OP, BITVECTOR_ROTATE_RIGHT},
         {CVC4::Kind::BITVECTOR_EXTRACT, BITVECTOR_EXTRACT},
         {CVC4::Kind::BITVECTOR_REPEAT, BITVECTOR_REPEAT},
         {CVC4::Kind::BITVECTOR_ZERO_EXTEND, BITVECTOR_ZERO_EXTEND},
         {CVC4::Kind::BITVECTOR_SIGN_EXTEND, BITVECTOR_SIGN_EXTEND},
         {CVC4::Kind::BITVECTOR_ROTATE_LEFT, BITVECTOR_ROTATE_LEFT},
         {CVC4::Kind::BITVECTOR_ROTATE_RIGHT, BITVECTOR_ROTATE_RIGHT},
-        {CVC4::Kind::INT_TO_BITVECTOR_OP, INT_TO_BITVECTOR_OP},
+        {CVC4::Kind::INT_TO_BITVECTOR_OP, INT_TO_BITVECTOR},
         {CVC4::Kind::INT_TO_BITVECTOR, INT_TO_BITVECTOR},
         {CVC4::Kind::BITVECTOR_TO_NAT, BITVECTOR_TO_NAT},
         /* FP -------------------------------------------------------------- */
@@ -456,35 +428,33 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction>
         {CVC4::Kind::FLOATINGPOINT_ISNEG, FLOATINGPOINT_ISNEG},
         {CVC4::Kind::FLOATINGPOINT_ISPOS, FLOATINGPOINT_ISPOS},
         {CVC4::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP,
-         FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP},
+         FLOATINGPOINT_TO_FP_IEEE_BITVECTOR},
         {CVC4::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
          FLOATINGPOINT_TO_FP_IEEE_BITVECTOR},
         {CVC4::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP,
-         FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP},
+         FLOATINGPOINT_TO_FP_FLOATINGPOINT},
         {CVC4::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT,
          FLOATINGPOINT_TO_FP_FLOATINGPOINT},
-        {CVC4::Kind::FLOATINGPOINT_TO_FP_REAL_OP, FLOATINGPOINT_TO_FP_REAL_OP},
+        {CVC4::Kind::FLOATINGPOINT_TO_FP_REAL_OP, FLOATINGPOINT_TO_FP_REAL},
         {CVC4::Kind::FLOATINGPOINT_TO_FP_REAL, FLOATINGPOINT_TO_FP_REAL},
         {CVC4::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP,
-         FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP},
+         FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR},
         {CVC4::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
          FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR},
         {CVC4::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP,
-         FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP},
+         FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR},
         {CVC4::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
          FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR},
         {CVC4::Kind::FLOATINGPOINT_TO_FP_GENERIC_OP,
-         FLOATINGPOINT_TO_FP_GENERIC_OP},
+         FLOATINGPOINT_TO_FP_GENERIC},
         {CVC4::Kind::FLOATINGPOINT_TO_FP_GENERIC, FLOATINGPOINT_TO_FP_GENERIC},
-        {CVC4::Kind::FLOATINGPOINT_TO_UBV_OP, FLOATINGPOINT_TO_UBV_OP},
+        {CVC4::Kind::FLOATINGPOINT_TO_UBV_OP, FLOATINGPOINT_TO_UBV},
         {CVC4::Kind::FLOATINGPOINT_TO_UBV, FLOATINGPOINT_TO_UBV},
-        {CVC4::Kind::FLOATINGPOINT_TO_UBV_TOTAL_OP,
-         FLOATINGPOINT_TO_UBV_TOTAL_OP},
+        {CVC4::Kind::FLOATINGPOINT_TO_UBV_TOTAL_OP, FLOATINGPOINT_TO_UBV_TOTAL},
         {CVC4::Kind::FLOATINGPOINT_TO_UBV_TOTAL, FLOATINGPOINT_TO_UBV_TOTAL},
-        {CVC4::Kind::FLOATINGPOINT_TO_SBV_OP, FLOATINGPOINT_TO_SBV_OP},
+        {CVC4::Kind::FLOATINGPOINT_TO_SBV_OP, FLOATINGPOINT_TO_SBV},
         {CVC4::Kind::FLOATINGPOINT_TO_SBV, FLOATINGPOINT_TO_SBV},
-        {CVC4::Kind::FLOATINGPOINT_TO_SBV_TOTAL_OP,
-         FLOATINGPOINT_TO_SBV_TOTAL_OP},
+        {CVC4::Kind::FLOATINGPOINT_TO_SBV_TOTAL_OP, FLOATINGPOINT_TO_SBV_TOTAL},
         {CVC4::Kind::FLOATINGPOINT_TO_SBV_TOTAL, FLOATINGPOINT_TO_SBV_TOTAL},
         {CVC4::Kind::FLOATINGPOINT_TO_REAL, FLOATINGPOINT_TO_REAL},
         {CVC4::Kind::FLOATINGPOINT_TO_REAL_TOTAL, FLOATINGPOINT_TO_REAL_TOTAL},
@@ -497,9 +467,9 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction>
         {CVC4::Kind::APPLY_CONSTRUCTOR, APPLY_CONSTRUCTOR},
         {CVC4::Kind::APPLY_SELECTOR_TOTAL, APPLY_SELECTOR_TOTAL},
         {CVC4::Kind::APPLY_TESTER, APPLY_TESTER},
-        {CVC4::Kind::TUPLE_UPDATE_OP, TUPLE_UPDATE_OP},
+        {CVC4::Kind::TUPLE_UPDATE_OP, TUPLE_UPDATE},
         {CVC4::Kind::TUPLE_UPDATE, TUPLE_UPDATE},
-        {CVC4::Kind::RECORD_UPDATE_OP, RECORD_UPDATE_OP},
+        {CVC4::Kind::RECORD_UPDATE_OP, RECORD_UPDATE},
         {CVC4::Kind::RECORD_UPDATE, RECORD_UPDATE},
         /* Separation Logic ------------------------------------------------ */
         {CVC4::Kind::SEP_NIL, SEP_NIL},
@@ -1023,6 +993,240 @@ size_t SortHashFunction::operator()(const Sort& s) const
 }
 
 /* -------------------------------------------------------------------------- */
+/* Op                                                                     */
+/* -------------------------------------------------------------------------- */
+
+Op::Op() : d_kind(NULL_EXPR), d_expr(new CVC4::Expr()) {}
+
+Op::Op(const Kind k) : d_kind(k), d_expr(new CVC4::Expr()) {}
+
+Op::Op(const Kind k, const CVC4::Expr& e) : d_kind(k), d_expr(new CVC4::Expr(e))
+{
+}
+
+Op::~Op() {}
+
+/* Helpers                                                                    */
+/* -------------------------------------------------------------------------- */
+
+/* Split out to avoid nested API calls (problematic with API tracing).        */
+/* .......................................................................... */
+
+bool Op::isIndexedHelper() const { return !d_expr->isNull(); }
+
+/* Public methods                                                             */
+bool Op::operator==(const Op& t) const
+{
+  if (d_expr->isNull() || t.d_expr->isNull())
+  {
+    return false;
+  }
+  return (d_kind == t.d_kind) && (*d_expr == *t.d_expr);
+}
+
+bool Op::operator!=(const Op& t) const { return !(*this == t); }
+
+Kind Op::getKind() const
+{
+  CVC4_API_CHECK(d_kind != NULL_EXPR) << "Expecting a non-null Kind";
+  return d_kind;
+}
+
+Sort Op::getSort() const
+{
+  CVC4_API_CHECK_NOT_NULL;
+  return Sort(d_expr->getType());
+}
+
+bool Op::isNull() const { return (d_expr->isNull() && (d_kind == NULL_EXPR)); }
+
+bool Op::isIndexed() const { return isIndexedHelper(); }
+
+template <>
+std::string Op::getIndices() const
+{
+  CVC4_API_CHECK_NOT_NULL;
+  CVC4_API_CHECK(!d_expr->isNull())
+      << "Expecting a non-null internal expression. This Op is not indexed.";
+
+  std::string i;
+  Kind k = intToExtKind(d_expr->getKind());
+
+  if (k == DIVISIBLE)
+  {
+    // DIVISIBLE returns a string index to support
+    // arbitrary precision integers
+    CVC4::Integer _int = d_expr->getConst<Divisible>().k;
+    i = _int.toString();
+  }
+  else if (k == RECORD_UPDATE)
+  {
+    i = d_expr->getConst<RecordUpdate>().getField();
+  }
+  else
+  {
+    CVC4_API_CHECK(false) << "Can't get string index from"
+                          << " kind " << kindToString(k);
+  }
+
+  return i;
+}
+
+template <>
+Kind Op::getIndices() const
+{
+  CVC4_API_CHECK_NOT_NULL;
+  CVC4_API_CHECK(!d_expr->isNull())
+      << "Expecting a non-null internal expression. This Op is not indexed.";
+  Kind kind = intToExtKind(d_expr->getKind());
+  CVC4_API_KIND_CHECK_EXPECTED(kind == CHAIN, kind) << "CHAIN";
+  return intToExtKind(d_expr->getConst<Chain>().getOperator());
+}
+
+template <>
+uint32_t Op::getIndices() const
+{
+  CVC4_API_CHECK_NOT_NULL;
+  CVC4_API_CHECK(!d_expr->isNull())
+      << "Expecting a non-null internal expression. This Op is not indexed.";
+
+  uint32_t i = 0;
+  Kind k = intToExtKind(d_expr->getKind());
+  switch (k)
+  {
+    case BITVECTOR_REPEAT:
+      i = d_expr->getConst<BitVectorRepeat>().repeatAmount;
+      break;
+    case BITVECTOR_ZERO_EXTEND:
+      i = d_expr->getConst<BitVectorZeroExtend>().zeroExtendAmount;
+      break;
+    case BITVECTOR_SIGN_EXTEND:
+      i = d_expr->getConst<BitVectorSignExtend>().signExtendAmount;
+      break;
+    case BITVECTOR_ROTATE_LEFT:
+      i = d_expr->getConst<BitVectorRotateLeft>().rotateLeftAmount;
+      break;
+    case BITVECTOR_ROTATE_RIGHT:
+      i = d_expr->getConst<BitVectorRotateRight>().rotateRightAmount;
+      break;
+    case INT_TO_BITVECTOR: i = d_expr->getConst<IntToBitVector>().size; break;
+    case FLOATINGPOINT_TO_UBV:
+      i = d_expr->getConst<FloatingPointToUBV>().bvs.size;
+      break;
+    case FLOATINGPOINT_TO_UBV_TOTAL:
+      i = d_expr->getConst<FloatingPointToUBVTotal>().bvs.size;
+      break;
+    case FLOATINGPOINT_TO_SBV:
+      i = d_expr->getConst<FloatingPointToSBV>().bvs.size;
+      break;
+    case FLOATINGPOINT_TO_SBV_TOTAL:
+      i = d_expr->getConst<FloatingPointToSBVTotal>().bvs.size;
+      break;
+    case TUPLE_UPDATE: i = d_expr->getConst<TupleUpdate>().getIndex(); break;
+    default:
+      CVC4ApiExceptionStream().ostream() << "Can't get uint32_t index from"
+                                         << " kind " << kindToString(k);
+  }
+  return i;
+}
+
+template <>
+std::pair<uint32_t, uint32_t> Op::getIndices() const
+{
+  CVC4_API_CHECK_NOT_NULL;
+  CVC4_API_CHECK(!d_expr->isNull())
+      << "Expecting a non-null internal expression. This Op is not indexed.";
+
+  std::pair<uint32_t, uint32_t> indices;
+  Kind k = intToExtKind(d_expr->getKind());
+
+  // using if/else instead of case statement because want local variables
+  if (k == BITVECTOR_EXTRACT)
+  {
+    CVC4::BitVectorExtract ext = d_expr->getConst<BitVectorExtract>();
+    indices = std::make_pair(ext.high, ext.low);
+  }
+  else if (k == FLOATINGPOINT_TO_FP_IEEE_BITVECTOR)
+  {
+    CVC4::FloatingPointToFPIEEEBitVector ext =
+        d_expr->getConst<FloatingPointToFPIEEEBitVector>();
+    indices = std::make_pair(ext.t.exponent(), ext.t.significand());
+  }
+  else if (k == FLOATINGPOINT_TO_FP_FLOATINGPOINT)
+  {
+    CVC4::FloatingPointToFPFloatingPoint ext =
+        d_expr->getConst<FloatingPointToFPFloatingPoint>();
+    indices = std::make_pair(ext.t.exponent(), ext.t.significand());
+  }
+  else if (k == FLOATINGPOINT_TO_FP_REAL)
+  {
+    CVC4::FloatingPointToFPReal ext = d_expr->getConst<FloatingPointToFPReal>();
+    indices = std::make_pair(ext.t.exponent(), ext.t.significand());
+  }
+  else if (k == FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR)
+  {
+    CVC4::FloatingPointToFPSignedBitVector ext =
+        d_expr->getConst<FloatingPointToFPSignedBitVector>();
+    indices = std::make_pair(ext.t.exponent(), ext.t.significand());
+  }
+  else if (k == FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR)
+  {
+    CVC4::FloatingPointToFPUnsignedBitVector ext =
+        d_expr->getConst<FloatingPointToFPUnsignedBitVector>();
+    indices = std::make_pair(ext.t.exponent(), ext.t.significand());
+  }
+  else if (k == FLOATINGPOINT_TO_FP_GENERIC)
+  {
+    CVC4::FloatingPointToFPGeneric ext =
+        d_expr->getConst<FloatingPointToFPGeneric>();
+    indices = std::make_pair(ext.t.exponent(), ext.t.significand());
+  }
+  else
+  {
+    CVC4_API_CHECK(false) << "Can't get pair<uint32_t, uint32_t> indices from"
+                          << " kind " << kindToString(k);
+  }
+  return indices;
+}
+
+std::string Op::toString() const
+{
+  CVC4_API_CHECK_NOT_NULL;
+  if (d_expr->isNull())
+  {
+    return kindToString(d_kind);
+  }
+  else
+  {
+    CVC4_API_CHECK(!d_expr->isNull())
+        << "Expecting a non-null internal expression";
+    return d_expr->toString();
+  }
+}
+
+// !!! This is only temporarily available until the parser is fully migrated
+// to the new API. !!!
+CVC4::Expr Op::getExpr(void) const { return *d_expr; }
+
+std::ostream& operator<<(std::ostream& out, const Op& t)
+{
+  out << t.toString();
+  return out;
+}
+
+size_t OpHashFunction::operator()(const Op& t) const
+{
+  if (t.isIndexedHelper())
+  {
+    return ExprHashFunction()(*t.d_expr);
+  }
+  else
+  {
+    return KindHashFunction()(t.d_kind);
+  }
+}
+
+/* -------------------------------------------------------------------------- */
 /* Term                                                                       */
 /* -------------------------------------------------------------------------- */
 
@@ -1054,6 +1258,39 @@ Sort Term::getSort() const
   return Sort(d_expr->getType());
 }
 
+bool Term::hasOp() const
+{
+  CVC4_API_CHECK_NOT_NULL;
+  return d_expr->hasOperator();
+}
+
+Op Term::getOp() const
+{
+  CVC4_API_CHECK_NOT_NULL;
+  CVC4_API_CHECK(d_expr->hasOperator())
+      << "Expecting Term to have an Op when calling getOp()";
+  CVC4::Expr op = d_expr->getOperator();
+  CVC4::Type t = op.getType();
+
+  // special cases for Datatype operators
+  if (t.isSelector())
+  {
+    return Op(APPLY_SELECTOR, op);
+  }
+  else if (t.isConstructor())
+  {
+    return Op(APPLY_CONSTRUCTOR, op);
+  }
+  else if (t.isTester())
+  {
+    return Op(APPLY_TESTER, op);
+  }
+  else
+  {
+    return Op(intToExtKind(op.getKind()), op);
+  }
+}
+
 bool Term::isNull() const { return d_expr->isNull(); }
 
 bool Term::isParameterized() const
@@ -1176,41 +1413,38 @@ Term Term::iteTerm(const Term& then_t, const Term& else_t) const
 
 std::string Term::toString() const { return d_expr->toString(); }
 
-Term::const_iterator::const_iterator() : d_iterator(nullptr) {}
+Term::const_iterator::const_iterator() : d_orig_expr(nullptr), d_pos(0) {}
 
-Term::const_iterator::const_iterator(void* it) : d_iterator(it) {}
+Term::const_iterator::const_iterator(const std::shared_ptr<CVC4::Expr>& e,
+                                     uint32_t p)
+    : d_orig_expr(e), d_pos(p)
+{
+}
 
 Term::const_iterator::const_iterator(const const_iterator& it)
-    : d_iterator(nullptr)
+    : d_orig_expr(nullptr)
 {
-  if (it.d_iterator != nullptr)
+  if (it.d_orig_expr != nullptr)
   {
-    d_iterator = new CVC4::Expr::const_iterator(
-        *static_cast<CVC4::Expr::const_iterator*>(it.d_iterator));
+    d_orig_expr = it.d_orig_expr;
+    d_pos = it.d_pos;
   }
 }
 
 Term::const_iterator& Term::const_iterator::operator=(const const_iterator& it)
 {
-  delete static_cast<CVC4::Expr::const_iterator*>(d_iterator);
-  d_iterator = new CVC4::Expr::const_iterator(
-      *static_cast<CVC4::Expr::const_iterator*>(it.d_iterator));
+  d_orig_expr = it.d_orig_expr;
+  d_pos = it.d_pos;
   return *this;
 }
 
-Term::const_iterator::~const_iterator()
-{
-  delete static_cast<CVC4::Expr::const_iterator*>(d_iterator);
-}
-
 bool Term::const_iterator::operator==(const const_iterator& it) const
 {
-  if (d_iterator == nullptr || it.d_iterator == nullptr)
+  if (d_orig_expr == nullptr || it.d_orig_expr == nullptr)
   {
     return false;
   }
-  return *static_cast<CVC4::Expr::const_iterator*>(d_iterator)
-         == *static_cast<CVC4::Expr::const_iterator*>(it.d_iterator);
+  return (*d_orig_expr == *it.d_orig_expr) && (d_pos == it.d_pos);
 }
 
 bool Term::const_iterator::operator!=(const const_iterator& it) const
@@ -1220,33 +1454,53 @@ bool Term::const_iterator::operator!=(const const_iterator& it) const
 
 Term::const_iterator& Term::const_iterator::operator++()
 {
-  Assert(d_iterator != nullptr);
-  ++*static_cast<CVC4::Expr::const_iterator*>(d_iterator);
+  Assert(d_orig_expr != nullptr);
+  ++d_pos;
   return *this;
 }
 
 Term::const_iterator Term::const_iterator::operator++(int)
 {
-  Assert(d_iterator != nullptr);
+  Assert(d_orig_expr != nullptr);
   const_iterator it = *this;
-  ++*static_cast<CVC4::Expr::const_iterator*>(d_iterator);
+  ++d_pos;
   return it;
 }
 
 Term Term::const_iterator::operator*() const
 {
-  Assert(d_iterator != nullptr);
-  return Term(**static_cast<CVC4::Expr::const_iterator*>(d_iterator));
+  Assert(d_orig_expr != nullptr);
+  if (!d_pos && (d_orig_expr->getKind() == CVC4::Kind::APPLY_UF))
+  {
+    return Term(d_orig_expr->getOperator());
+  }
+  else
+  {
+    uint32_t idx = d_pos;
+    if (d_orig_expr->getKind() == CVC4::Kind::APPLY_UF)
+    {
+      Assert(idx > 0);
+      --idx;
+    }
+    Assert(idx >= 0);
+    return Term((*d_orig_expr)[idx]);
+  }
 }
 
 Term::const_iterator Term::begin() const
 {
-  return Term::const_iterator(new CVC4::Expr::const_iterator(d_expr->begin()));
+  return Term::const_iterator(d_expr, 0);
 }
 
 Term::const_iterator Term::end() const
 {
-  return Term::const_iterator(new CVC4::Expr::const_iterator(d_expr->end()));
+  int endpos = d_expr->getNumChildren();
+  if (d_expr->getKind() == CVC4::Kind::APPLY_UF)
+  {
+    // one more child if this is a UF application (count the UF as a child)
+    ++endpos;
+  }
+  return Term::const_iterator(d_expr, endpos);
 }
 
 // !!! This is only temporarily available until the parser is fully migrated
@@ -1300,188 +1554,6 @@ size_t TermHashFunction::operator()(const Term& t) const
   return ExprHashFunction()(*t.d_expr);
 }
 
-/* -------------------------------------------------------------------------- */
-/* OpTerm                                                                     */
-/* -------------------------------------------------------------------------- */
-
-OpTerm::OpTerm() : d_expr(new CVC4::Expr()) {}
-
-OpTerm::OpTerm(const CVC4::Expr& e) : d_expr(new CVC4::Expr(e)) {}
-
-OpTerm::~OpTerm() {}
-
-bool OpTerm::operator==(const OpTerm& t) const { return *d_expr == *t.d_expr; }
-
-bool OpTerm::operator!=(const OpTerm& t) const { return *d_expr != *t.d_expr; }
-
-Kind OpTerm::getKind() const
-{
-  CVC4_API_CHECK_NOT_NULL;
-  return intToExtKind(d_expr->getKind());
-}
-
-Sort OpTerm::getSort() const
-{
-  CVC4_API_CHECK_NOT_NULL;
-  return Sort(d_expr->getType());
-}
-
-bool OpTerm::isNull() const { return d_expr->isNull(); }
-
-template <>
-std::string OpTerm::getIndices() const
-{
-  CVC4_API_CHECK_NOT_NULL;
-  std::string i;
-  Kind k = intToExtKind(d_expr->getKind());
-
-  if (k == DIVISIBLE_OP)
-  {
-    // DIVISIBLE_OP returns a string index to support
-    // arbitrary precision integers
-    CVC4::Integer _int = d_expr->getConst<Divisible>().k;
-    i = _int.toString();
-  }
-  else if (k == RECORD_UPDATE_OP)
-  {
-    i = d_expr->getConst<RecordUpdate>().getField();
-  }
-  else
-  {
-    CVC4_API_CHECK(false) << "Can't get string index from"
-                          << " kind " << kindToString(k);
-  }
-
-  return i;
-}
-
-template <>
-Kind OpTerm::getIndices() const
-{
-  CVC4_API_CHECK_NOT_NULL;
-  Kind kind = intToExtKind(d_expr->getKind());
-  CVC4_API_KIND_CHECK_EXPECTED(kind == CHAIN_OP, kind) << "CHAIN_OP";
-  return intToExtKind(d_expr->getConst<Chain>().getOperator());
-}
-
-template <>
-uint32_t OpTerm::getIndices() const
-{
-  CVC4_API_CHECK_NOT_NULL;
-  uint32_t i = 0;
-  Kind k = intToExtKind(d_expr->getKind());
-  switch (k)
-  {
-    case BITVECTOR_REPEAT_OP:
-      i = d_expr->getConst<BitVectorRepeat>().repeatAmount;
-      break;
-    case BITVECTOR_ZERO_EXTEND_OP:
-      i = d_expr->getConst<BitVectorZeroExtend>().zeroExtendAmount;
-      break;
-    case BITVECTOR_SIGN_EXTEND_OP:
-      i = d_expr->getConst<BitVectorSignExtend>().signExtendAmount;
-      break;
-    case BITVECTOR_ROTATE_LEFT_OP:
-      i = d_expr->getConst<BitVectorRotateLeft>().rotateLeftAmount;
-      break;
-    case BITVECTOR_ROTATE_RIGHT_OP:
-      i = d_expr->getConst<BitVectorRotateRight>().rotateRightAmount;
-      break;
-    case INT_TO_BITVECTOR_OP:
-      i = d_expr->getConst<IntToBitVector>().size;
-      break;
-    case FLOATINGPOINT_TO_UBV_OP:
-      i = d_expr->getConst<FloatingPointToUBV>().bvs.size;
-      break;
-    case FLOATINGPOINT_TO_UBV_TOTAL_OP:
-      i = d_expr->getConst<FloatingPointToUBVTotal>().bvs.size;
-      break;
-    case FLOATINGPOINT_TO_SBV_OP:
-      i = d_expr->getConst<FloatingPointToSBV>().bvs.size;
-      break;
-    case FLOATINGPOINT_TO_SBV_TOTAL_OP:
-      i = d_expr->getConst<FloatingPointToSBVTotal>().bvs.size;
-      break;
-    case TUPLE_UPDATE_OP: i = d_expr->getConst<TupleUpdate>().getIndex(); break;
-    default:
-      CVC4ApiExceptionStream().ostream() << "Can't get uint32_t index from"
-                                         << " kind " << kindToString(k);
-  }
-  return i;
-}
-
-template <>
-std::pair<uint32_t, uint32_t> OpTerm::getIndices() const
-{
-  CVC4_API_CHECK_NOT_NULL;
-  std::pair<uint32_t, uint32_t> indices;
-  Kind k = intToExtKind(d_expr->getKind());
-
-  // using if/else instead of case statement because want local variables
-  if (k == BITVECTOR_EXTRACT_OP)
-  {
-    CVC4::BitVectorExtract ext = d_expr->getConst<BitVectorExtract>();
-    indices = std::make_pair(ext.high, ext.low);
-  }
-  else if (k == FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP)
-  {
-    CVC4::FloatingPointToFPIEEEBitVector ext =
-        d_expr->getConst<FloatingPointToFPIEEEBitVector>();
-    indices = std::make_pair(ext.t.exponent(), ext.t.significand());
-  }
-  else if (k == FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP)
-  {
-    CVC4::FloatingPointToFPFloatingPoint ext =
-        d_expr->getConst<FloatingPointToFPFloatingPoint>();
-    indices = std::make_pair(ext.t.exponent(), ext.t.significand());
-  }
-  else if (k == FLOATINGPOINT_TO_FP_REAL_OP)
-  {
-    CVC4::FloatingPointToFPReal ext = d_expr->getConst<FloatingPointToFPReal>();
-    indices = std::make_pair(ext.t.exponent(), ext.t.significand());
-  }
-  else if (k == FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP)
-  {
-    CVC4::FloatingPointToFPSignedBitVector ext =
-        d_expr->getConst<FloatingPointToFPSignedBitVector>();
-    indices = std::make_pair(ext.t.exponent(), ext.t.significand());
-  }
-  else if (k == FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP)
-  {
-    CVC4::FloatingPointToFPUnsignedBitVector ext =
-        d_expr->getConst<FloatingPointToFPUnsignedBitVector>();
-    indices = std::make_pair(ext.t.exponent(), ext.t.significand());
-  }
-  else if (k == FLOATINGPOINT_TO_FP_GENERIC_OP)
-  {
-    CVC4::FloatingPointToFPGeneric ext =
-        d_expr->getConst<FloatingPointToFPGeneric>();
-    indices = std::make_pair(ext.t.exponent(), ext.t.significand());
-  }
-  else
-  {
-    CVC4_API_CHECK(false) << "Can't get pair<uint32_t, uint32_t> indices from"
-                          << " kind " << kindToString(k);
-  }
-  return indices;
-}
-
-std::string OpTerm::toString() const { return d_expr->toString(); }
-
-// !!! This is only temporarily available until the parser is fully migrated
-// to the new API. !!!
-CVC4::Expr OpTerm::getExpr(void) const { return *d_expr; }
-
-std::ostream& operator<<(std::ostream& out, const OpTerm& t)
-{
-  out << t.toString();
-  return out;
-}
-
-size_t OpTermHashFunction::operator()(const OpTerm& t) const
-{
-  return ExprHashFunction()(*t.d_expr);
-}
 
 /* -------------------------------------------------------------------------- */
 /* Datatypes                                                                  */
@@ -1635,10 +1707,11 @@ DatatypeSelector::~DatatypeSelector() {}
 
 bool DatatypeSelector::isResolved() const { return d_stor->isResolved(); }
 
-OpTerm DatatypeSelector::getSelectorTerm() const
+Op DatatypeSelector::getSelectorTerm() const
 {
   CVC4_API_CHECK(isResolved()) << "Expected resolved datatype selector.";
-  return d_stor->getSelector();
+  CVC4::Expr sel = d_stor->getSelector();
+  return Op(APPLY_SELECTOR, sel);
 }
 
 std::string DatatypeSelector::toString() const
@@ -1675,10 +1748,11 @@ DatatypeConstructor::~DatatypeConstructor() {}
 
 bool DatatypeConstructor::isResolved() const { return d_ctor->isResolved(); }
 
-OpTerm DatatypeConstructor::getConstructorTerm() const
+Op DatatypeConstructor::getConstructorTerm() const
 {
   CVC4_API_CHECK(isResolved()) << "Expected resolved datatype constructor.";
-  return OpTerm(d_ctor->getConstructor());
+  CVC4::Expr ctor = d_ctor->getConstructor();
+  return Op(APPLY_CONSTRUCTOR, ctor);
 }
 
 DatatypeSelector DatatypeConstructor::operator[](const std::string& name) const
@@ -1695,11 +1769,12 @@ DatatypeSelector DatatypeConstructor::getSelector(const std::string& name) const
   return (*d_ctor)[name];
 }
 
-OpTerm DatatypeConstructor::getSelectorTerm(const std::string& name) const
+Op DatatypeConstructor::getSelectorTerm(const std::string& name) const
 {
   // CHECK: cons with name exists?
   // CHECK: is resolved?
-  return d_ctor->getSelector(name);
+  CVC4::Expr sel = d_ctor->getSelector(name);
+  return Op(APPLY_SELECTOR, sel);
 }
 
 DatatypeConstructor::const_iterator DatatypeConstructor::begin() const
@@ -1824,11 +1899,12 @@ DatatypeConstructor Datatype::getConstructor(const std::string& name) const
   return (*d_dtype)[name];
 }
 
-OpTerm Datatype::getConstructorTerm(const std::string& name) const
+Op Datatype::getConstructorTerm(const std::string& name) const
 {
   // CHECK: cons with name exists?
   // CHECK: is resolved?
-  return d_dtype->getConstructor(name);
+  CVC4::Expr ctor = d_dtype->getConstructor(name);
+  return Op(APPLY_CONSTRUCTOR, ctor);
 }
 
 size_t Datatype::getNumConstructors() const
@@ -2032,6 +2108,31 @@ Term Solver::mkBVFromStrHelper(uint32_t size,
   return mkValHelper<CVC4::BitVector>(CVC4::BitVector(size, val));
 }
 
+Term Solver::mkTermFromKind(Kind kind) const
+{
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4_API_KIND_CHECK_EXPECTED(
+      kind == PI || kind == REGEXP_EMPTY || kind == REGEXP_SIGMA, kind)
+      << "PI or REGEXP_EMPTY or REGEXP_SIGMA";
+
+  Term res;
+  if (kind == REGEXP_EMPTY || kind == REGEXP_SIGMA)
+  {
+    CVC4::Kind k = extToIntKind(kind);
+    Assert(isDefinedIntKind(k));
+    res = d_exprMgr->mkExpr(k, std::vector<Expr>());
+  }
+  else
+  {
+    Assert(kind == PI);
+    res = d_exprMgr->mkNullaryOperator(d_exprMgr->realType(), CVC4::kind::PI);
+  }
+  (void)res.d_expr->getType(true); /* kick off type checking */
+  return res;
+
+  CVC4_API_SOLVER_TRY_CATCH_END;
+}
+
 /* Helpers for converting vectors.                                            */
 /* .......................................................................... */
 
@@ -2079,36 +2180,6 @@ void Solver::checkMkTerm(Kind kind, uint32_t nchildren) const
       << " children (the one under construction has " << nchildren << ")";
 }
 
-void Solver::checkMkOpTerm(Kind kind, OpTerm opTerm, uint32_t nchildren) const
-{
-  Assert(isDefinedIntKind(extToIntKind(kind)));
-  const CVC4::Kind int_kind = extToIntKind(kind);
-  const CVC4::Kind int_op_kind = opTerm.d_expr->getKind();
-  const CVC4::Kind int_op_to_kind =
-      NodeManager::operatorToKind(opTerm.d_expr->getNode());
-  CVC4_API_ARG_CHECK_EXPECTED(
-      int_kind == int_op_to_kind
-          || (kind == APPLY_CONSTRUCTOR
-              && int_op_to_kind == CVC4::Kind::UNDEFINED_KIND)
-          || (kind == APPLY_SELECTOR
-              && int_op_to_kind == CVC4::Kind::UNDEFINED_KIND)
-          || (kind == APPLY_UF && int_op_to_kind == CVC4::Kind::UNDEFINED_KIND),
-      kind)
-      << "kind that matches kind associated with given operator term";
-  CVC4_API_ARG_CHECK_EXPECTED(
-      int_op_kind == CVC4::kind::BUILTIN
-          || CVC4::kind::metaKindOf(int_kind) == kind::metakind::PARAMETERIZED,
-      opTerm)
-      << "This term constructor is for parameterized kinds only";
-  uint32_t min_arity = ExprManager::minArity(int_kind);
-  uint32_t max_arity = ExprManager::maxArity(int_kind);
-  CVC4_API_KIND_CHECK_EXPECTED(nchildren >= min_arity && nchildren <= max_arity,
-                               kind)
-      << "Terms with kind " << kindToString(kind) << " must have at least "
-      << min_arity << " children and at most " << max_arity
-      << " children (the one under construction has " << nchildren << ")";
-}
-
 /* Sorts Handling                                                             */
 /* -------------------------------------------------------------------------- */
 
@@ -2758,25 +2829,7 @@ Term Solver::mkVar(Sort sort, const std::string& symbol) const
 Term Solver::mkTerm(Kind kind) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  CVC4_API_KIND_CHECK_EXPECTED(
-      kind == PI || kind == REGEXP_EMPTY || kind == REGEXP_SIGMA, kind)
-      << "PI or REGEXP_EMPTY or REGEXP_SIGMA";
-
-  Term res;
-  if (kind == REGEXP_EMPTY || kind == REGEXP_SIGMA)
-  {
-    CVC4::Kind k = extToIntKind(kind);
-    Assert(isDefinedIntKind(k));
-    res = d_exprMgr->mkExpr(k, std::vector<Expr>());
-  }
-  else
-  {
-    Assert(kind == PI);
-    res = d_exprMgr->mkNullaryOperator(d_exprMgr->realType(), CVC4::kind::PI);
-  }
-  (void)res.d_expr->getType(true); /* kick off type checking */
-  return res;
-
+  return mkTermFromKind(kind);
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
@@ -2849,69 +2902,99 @@ Term Solver::mkTerm(Kind kind, const std::vector<Term>& children) const
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
-Term Solver::mkTerm(Kind kind, OpTerm opTerm) const
+Term Solver::mkTerm(Op op) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  checkMkOpTerm(kind, opTerm, 0);
 
-  const CVC4::Kind int_kind = extToIntKind(kind);
-  Term res = d_exprMgr->mkExpr(int_kind, *opTerm.d_expr);
+  Term res;
+  if (op.isIndexedHelper())
+  {
+    const CVC4::Kind int_kind = extToIntKind(op.d_kind);
+    res = d_exprMgr->mkExpr(int_kind, *op.d_expr);
+  }
+  else
+  {
+    res = mkTermFromKind(op.d_kind);
+  }
+
   (void)res.d_expr->getType(true); /* kick off type checking */
   return res;
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
-Term Solver::mkTerm(Kind kind, OpTerm opTerm, Term child) const
+Term Solver::mkTerm(Op op, Term child) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(!child.isNull(), child) << "non-null term";
-  checkMkOpTerm(kind, opTerm, 1);
 
-  const CVC4::Kind int_kind = extToIntKind(kind);
-  Term res = d_exprMgr->mkExpr(int_kind, *opTerm.d_expr, *child.d_expr);
+  const CVC4::Kind int_kind = extToIntKind(op.d_kind);
+  Term res;
+  if (op.isIndexedHelper())
+  {
+    res = d_exprMgr->mkExpr(int_kind, *op.d_expr, *child.d_expr);
+  }
+  else
+  {
+    res = d_exprMgr->mkExpr(int_kind, *child.d_expr);
+  }
+
   (void)res.d_expr->getType(true); /* kick off type checking */
   return res;
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
-Term Solver::mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2) const
+Term Solver::mkTerm(Op op, Term child1, Term child2) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term";
   CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term";
-  checkMkOpTerm(kind, opTerm, 2);
 
-  const CVC4::Kind int_kind = extToIntKind(kind);
-  Term res = d_exprMgr->mkExpr(
-      int_kind, *opTerm.d_expr, *child1.d_expr, *child2.d_expr);
+  const CVC4::Kind int_kind = extToIntKind(op.d_kind);
+  Term res;
+  if (op.isIndexedHelper())
+  {
+    res =
+        d_exprMgr->mkExpr(int_kind, *op.d_expr, *child1.d_expr, *child2.d_expr);
+  }
+  else
+  {
+    res = d_exprMgr->mkExpr(int_kind, *child1.d_expr, *child2.d_expr);
+  }
+
   (void)res.d_expr->getType(true); /* kick off type checking */
   return res;
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
-Term Solver::mkTerm(
-    Kind kind, OpTerm opTerm, Term child1, Term child2, Term child3) const
+Term Solver::mkTerm(Op op, Term child1, Term child2, Term child3) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term";
   CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term";
   CVC4_API_ARG_CHECK_EXPECTED(!child3.isNull(), child3) << "non-null term";
-  checkMkOpTerm(kind, opTerm, 3);
 
-  const CVC4::Kind int_kind = extToIntKind(kind);
-  Term res = d_exprMgr->mkExpr(
-      int_kind, *opTerm.d_expr, *child1.d_expr, *child2.d_expr, *child3.d_expr);
+  const CVC4::Kind int_kind = extToIntKind(op.d_kind);
+  Term res;
+  if (op.isIndexedHelper())
+  {
+    res = d_exprMgr->mkExpr(
+        int_kind, *op.d_expr, *child1.d_expr, *child2.d_expr, *child3.d_expr);
+  }
+  else
+  {
+    res = d_exprMgr->mkExpr(
+        int_kind, *child1.d_expr, *child2.d_expr, *child3.d_expr);
+  }
+
   (void)res.d_expr->getType(true); /* kick off type checking */
   return res;
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
-Term Solver::mkTerm(Kind kind,
-                    OpTerm opTerm,
-                    const std::vector<Term>& children) const
+Term Solver::mkTerm(Op op, const std::vector<Term>& children) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   for (size_t i = 0, size = children.size(); i < size; ++i)
@@ -2920,11 +3003,19 @@ Term Solver::mkTerm(Kind kind,
         !children[i].isNull(), "parameter term", children[i], i)
         << "non-null term";
   }
-  checkMkOpTerm(kind, opTerm, children.size());
 
-  const CVC4::Kind int_kind = extToIntKind(kind);
+  const CVC4::Kind int_kind = extToIntKind(op.d_kind);
   std::vector<Expr> echildren = termVectorToExprs(children);
-  Term res = d_exprMgr->mkExpr(int_kind, *opTerm.d_expr, echildren);
+  Term res;
+  if (op.isIndexedHelper())
+  {
+    res = d_exprMgr->mkExpr(int_kind, *op.d_expr, echildren);
+  }
+  else
+  {
+    res = d_exprMgr->mkExpr(int_kind, echildren);
+  }
+
   (void)res.d_expr->getType(true); /* kick off type checking */
   return res;
 
@@ -2954,30 +3045,33 @@ Term Solver::mkTuple(const std::vector<Sort>& sorts,
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
-/* Create operator terms                                                      */
+/* Create operators                                                           */
 /* -------------------------------------------------------------------------- */
 
-OpTerm Solver::mkOpTerm(Kind kind, Kind k) const
+Op Solver::mkOp(Kind kind, Kind k) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  CVC4_API_KIND_CHECK_EXPECTED(kind == CHAIN_OP, kind) << "CHAIN_OP";
+  CVC4_API_KIND_CHECK_EXPECTED(kind == CHAIN, kind) << "CHAIN";
 
-  return *mkValHelper<CVC4::Chain>(CVC4::Chain(extToIntKind(k))).d_expr.get();
+  return Op(
+      kind,
+      *mkValHelper<CVC4::Chain>(CVC4::Chain(extToIntKind(k))).d_expr.get());
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
-OpTerm Solver::mkOpTerm(Kind kind, const std::string& arg) const
+Op Solver::mkOp(Kind kind, const std::string& arg) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  CVC4_API_KIND_CHECK_EXPECTED(
-      (kind == RECORD_UPDATE_OP) || (kind == DIVISIBLE_OP), kind)
-      << "RECORD_UPDATE_OP or DIVISIBLE_OP";
-  OpTerm res;
-  if (kind == RECORD_UPDATE_OP)
+  CVC4_API_KIND_CHECK_EXPECTED((kind == RECORD_UPDATE) || (kind == DIVISIBLE),
+                               kind)
+      << "RECORD_UPDATE or DIVISIBLE";
+  Op res;
+  if (kind == RECORD_UPDATE)
   {
-    res =
-        *mkValHelper<CVC4::RecordUpdate>(CVC4::RecordUpdate(arg)).d_expr.get();
+    res = Op(
+        kind,
+        *mkValHelper<CVC4::RecordUpdate>(CVC4::RecordUpdate(arg)).d_expr.get());
   }
   else
   {
@@ -2986,76 +3080,90 @@ OpTerm Solver::mkOpTerm(Kind kind, const std::string& arg) const
      * as invalid. */
     CVC4_API_ARG_CHECK_EXPECTED(arg != ".", arg)
         << "a string representing an integer, real or rational value.";
-    res = *mkValHelper<CVC4::Divisible>(CVC4::Divisible(CVC4::Integer(arg)))
-               .d_expr.get();
+    res = Op(kind,
+             *mkValHelper<CVC4::Divisible>(CVC4::Divisible(CVC4::Integer(arg)))
+                  .d_expr.get());
   }
   return res;
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
-OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg) const
+Op Solver::mkOp(Kind kind, uint32_t arg) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_KIND_CHECK(kind);
 
-  OpTerm res;
+  Op res;
   switch (kind)
   {
-    case DIVISIBLE_OP:
-      res = *mkValHelper<CVC4::Divisible>(CVC4::Divisible(arg)).d_expr.get();
+    case DIVISIBLE:
+      res =
+          Op(kind,
+             *mkValHelper<CVC4::Divisible>(CVC4::Divisible(arg)).d_expr.get());
       break;
-    case BITVECTOR_REPEAT_OP:
-      res = *mkValHelper<CVC4::BitVectorRepeat>(CVC4::BitVectorRepeat(arg))
-                 .d_expr.get();
+    case BITVECTOR_REPEAT:
+      res = Op(kind,
+               *mkValHelper<CVC4::BitVectorRepeat>(CVC4::BitVectorRepeat(arg))
+                    .d_expr.get());
       break;
-    case BITVECTOR_ZERO_EXTEND_OP:
-      res = *mkValHelper<CVC4::BitVectorZeroExtend>(
-                 CVC4::BitVectorZeroExtend(arg))
-                 .d_expr.get();
+    case BITVECTOR_ZERO_EXTEND:
+      res = Op(kind,
+               *mkValHelper<CVC4::BitVectorZeroExtend>(
+                    CVC4::BitVectorZeroExtend(arg))
+                    .d_expr.get());
       break;
-    case BITVECTOR_SIGN_EXTEND_OP:
-      res = *mkValHelper<CVC4::BitVectorSignExtend>(
-                 CVC4::BitVectorSignExtend(arg))
-                 .d_expr.get();
+    case BITVECTOR_SIGN_EXTEND:
+      res = Op(kind,
+               *mkValHelper<CVC4::BitVectorSignExtend>(
+                    CVC4::BitVectorSignExtend(arg))
+                    .d_expr.get());
       break;
-    case BITVECTOR_ROTATE_LEFT_OP:
-      res = *mkValHelper<CVC4::BitVectorRotateLeft>(
-                 CVC4::BitVectorRotateLeft(arg))
-                 .d_expr.get();
+    case BITVECTOR_ROTATE_LEFT:
+      res = Op(kind,
+               *mkValHelper<CVC4::BitVectorRotateLeft>(
+                    CVC4::BitVectorRotateLeft(arg))
+                    .d_expr.get());
       break;
-    case BITVECTOR_ROTATE_RIGHT_OP:
-      res = *mkValHelper<CVC4::BitVectorRotateRight>(
-                 CVC4::BitVectorRotateRight(arg))
-                 .d_expr.get();
+    case BITVECTOR_ROTATE_RIGHT:
+      res = Op(kind,
+               *mkValHelper<CVC4::BitVectorRotateRight>(
+                    CVC4::BitVectorRotateRight(arg))
+                    .d_expr.get());
       break;
-    case INT_TO_BITVECTOR_OP:
-      res = *mkValHelper<CVC4::IntToBitVector>(CVC4::IntToBitVector(arg))
-                 .d_expr.get();
+    case INT_TO_BITVECTOR:
+      res = Op(kind,
+               *mkValHelper<CVC4::IntToBitVector>(CVC4::IntToBitVector(arg))
+                    .d_expr.get());
       break;
-    case FLOATINGPOINT_TO_UBV_OP:
-      res =
+    case FLOATINGPOINT_TO_UBV:
+      res = Op(
+          kind,
           *mkValHelper<CVC4::FloatingPointToUBV>(CVC4::FloatingPointToUBV(arg))
-               .d_expr.get();
+               .d_expr.get());
       break;
-    case FLOATINGPOINT_TO_UBV_TOTAL_OP:
-      res = *mkValHelper<CVC4::FloatingPointToUBVTotal>(
-                 CVC4::FloatingPointToUBVTotal(arg))
-                 .d_expr.get();
+    case FLOATINGPOINT_TO_UBV_TOTAL:
+      res = Op(kind,
+               *mkValHelper<CVC4::FloatingPointToUBVTotal>(
+                    CVC4::FloatingPointToUBVTotal(arg))
+                    .d_expr.get());
       break;
-    case FLOATINGPOINT_TO_SBV_OP:
-      res =
+    case FLOATINGPOINT_TO_SBV:
+      res = Op(
+          kind,
           *mkValHelper<CVC4::FloatingPointToSBV>(CVC4::FloatingPointToSBV(arg))
-               .d_expr.get();
+               .d_expr.get());
       break;
-    case FLOATINGPOINT_TO_SBV_TOTAL_OP:
-      res = *mkValHelper<CVC4::FloatingPointToSBVTotal>(
-                 CVC4::FloatingPointToSBVTotal(arg))
-                 .d_expr.get();
+    case FLOATINGPOINT_TO_SBV_TOTAL:
+      res = Op(kind,
+               *mkValHelper<CVC4::FloatingPointToSBVTotal>(
+                    CVC4::FloatingPointToSBVTotal(arg))
+                    .d_expr.get());
       break;
-    case TUPLE_UPDATE_OP:
-      res =
-          *mkValHelper<CVC4::TupleUpdate>(CVC4::TupleUpdate(arg)).d_expr.get();
+    case TUPLE_UPDATE:
+      res = Op(
+          kind,
+          *mkValHelper<CVC4::TupleUpdate>(CVC4::TupleUpdate(arg)).d_expr.get());
       break;
     default:
       CVC4_API_KIND_CHECK_EXPECTED(false, kind)
@@ -3067,48 +3175,55 @@ OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg) const
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
-OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg1, uint32_t arg2) const
+Op Solver::mkOp(Kind kind, uint32_t arg1, uint32_t arg2) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_KIND_CHECK(kind);
 
-  OpTerm res;
+  Op res;
   switch (kind)
   {
-    case BITVECTOR_EXTRACT_OP:
-      res = *mkValHelper<CVC4::BitVectorExtract>(
-                 CVC4::BitVectorExtract(arg1, arg2))
-                 .d_expr.get();
+    case BITVECTOR_EXTRACT:
+      res = Op(kind,
+               *mkValHelper<CVC4::BitVectorExtract>(
+                    CVC4::BitVectorExtract(arg1, arg2))
+                    .d_expr.get());
       break;
-    case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP:
-      res = *mkValHelper<CVC4::FloatingPointToFPIEEEBitVector>(
-                 CVC4::FloatingPointToFPIEEEBitVector(arg1, arg2))
-                 .d_expr.get();
+    case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR:
+      res = Op(kind,
+               *mkValHelper<CVC4::FloatingPointToFPIEEEBitVector>(
+                    CVC4::FloatingPointToFPIEEEBitVector(arg1, arg2))
+                    .d_expr.get());
       break;
-    case FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP:
-      res = *mkValHelper<CVC4::FloatingPointToFPFloatingPoint>(
-                 CVC4::FloatingPointToFPFloatingPoint(arg1, arg2))
-                 .d_expr.get();
+    case FLOATINGPOINT_TO_FP_FLOATINGPOINT:
+      res = Op(kind,
+               *mkValHelper<CVC4::FloatingPointToFPFloatingPoint>(
+                    CVC4::FloatingPointToFPFloatingPoint(arg1, arg2))
+                    .d_expr.get());
       break;
-    case FLOATINGPOINT_TO_FP_REAL_OP:
-      res = *mkValHelper<CVC4::FloatingPointToFPReal>(
-                 CVC4::FloatingPointToFPReal(arg1, arg2))
-                 .d_expr.get();
+    case FLOATINGPOINT_TO_FP_REAL:
+      res = Op(kind,
+               *mkValHelper<CVC4::FloatingPointToFPReal>(
+                    CVC4::FloatingPointToFPReal(arg1, arg2))
+                    .d_expr.get());
       break;
-    case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP:
-      res = *mkValHelper<CVC4::FloatingPointToFPSignedBitVector>(
-                 CVC4::FloatingPointToFPSignedBitVector(arg1, arg2))
-                 .d_expr.get();
+    case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR:
+      res = Op(kind,
+               *mkValHelper<CVC4::FloatingPointToFPSignedBitVector>(
+                    CVC4::FloatingPointToFPSignedBitVector(arg1, arg2))
+                    .d_expr.get());
       break;
-    case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP:
-      res = *mkValHelper<CVC4::FloatingPointToFPUnsignedBitVector>(
-                 CVC4::FloatingPointToFPUnsignedBitVector(arg1, arg2))
-                 .d_expr.get();
+    case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR:
+      res = Op(kind,
+               *mkValHelper<CVC4::FloatingPointToFPUnsignedBitVector>(
+                    CVC4::FloatingPointToFPUnsignedBitVector(arg1, arg2))
+                    .d_expr.get());
       break;
-    case FLOATINGPOINT_TO_FP_GENERIC_OP:
-      res = *mkValHelper<CVC4::FloatingPointToFPGeneric>(
-                 CVC4::FloatingPointToFPGeneric(arg1, arg2))
-                 .d_expr.get();
+    case FLOATINGPOINT_TO_FP_GENERIC:
+      res = Op(kind,
+               *mkValHelper<CVC4::FloatingPointToFPGeneric>(
+                    CVC4::FloatingPointToFPGeneric(arg1, arg2))
+                    .d_expr.get());
       break;
     default:
       CVC4_API_KIND_CHECK_EXPECTED(false, kind)
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index ad923f866..d73fbfdbd 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -177,7 +177,7 @@ class CVC4_PUBLIC Sort
   friend class DatatypeConstructorDecl;
   friend class DatatypeDecl;
   friend class DatatypeSelectorDecl;
-  friend class OpTerm;
+  friend class Op;
   friend class Solver;
   friend struct SortHashFunction;
   friend class Term;
@@ -524,6 +524,130 @@ struct CVC4_PUBLIC SortHashFunction
 };
 
 /* -------------------------------------------------------------------------- */
+/* Op                                                                     */
+/* -------------------------------------------------------------------------- */
+
+/**
+ * A CVC4 operator.
+ * An operator is a term that represents certain operators, instantiated
+ * with its required parameters, e.g., a term of kind BITVECTOR_EXTRACT.
+ */
+class CVC4_PUBLIC Op
+{
+  friend class Solver;
+  friend struct OpHashFunction;
+
+ public:
+  /**
+   * Constructor.
+   */
+  Op();
+
+  // !!! This constructor is only temporarily public until the parser is fully
+  // migrated to the new API. !!!
+  /**
+   * Constructor for a single kind (non-indexed operator).
+   * @param k the kind of this Op
+   */
+  Op(const Kind k);
+
+  // !!! This constructor is only temporarily public until the parser is fully
+  // migrated to the new API. !!!
+  /**
+   * Constructor.
+   * @param k the kind of this Op
+   * @param e the internal expression that is to be wrapped by this term
+   * @return the Term
+   */
+  Op(const Kind k, const CVC4::Expr& e);
+
+  /**
+   * Destructor.
+   */
+  ~Op();
+
+  /**
+   * Syntactic equality operator.
+   * Return true if both operators are syntactically identical.
+   * Both operators must belong to the same solver object.
+   * @param t the operator to compare to for equality
+   * @return true if the operators are equal
+   */
+  bool operator==(const Op& t) const;
+
+  /**
+   * Syntactic disequality operator.
+   * Return true if both operators differ syntactically.
+   * Both terms must belong to the same solver object.
+   * @param t the operator to compare to for disequality
+   * @return true if operators are disequal
+   */
+  bool operator!=(const Op& t) const;
+
+  /**
+   * @return the kind of this operator
+   */
+  Kind getKind() const;
+
+  /**
+   * @return the sort of this operator
+   */
+  Sort getSort() const;
+
+  /**
+   * @return true if this operator is a null term
+   */
+  bool isNull() const;
+
+  /**
+   * @return true iff this operator is indexed
+   */
+  bool isIndexed() const;
+
+  /**
+   * Get the indices used to create this Op.
+   * Supports the following template arguments:
+   *   - string
+   *   - Kind
+   *   - uint32_t
+   *   - pair<uint32_t, uint32_t>
+   * Check the Op Kind with getKind() to determine which argument to use.
+   * @return the indices used to create this Op
+   */
+  template <typename T>
+  T getIndices() const;
+
+  /**
+   * @return a string representation of this operator
+   */
+  std::string toString() const;
+
+  // !!! This is only temporarily available until the parser is fully migrated
+  // to the new API. !!!
+  CVC4::Expr getExpr(void) const;
+
+ private:
+  /* The kind of this operator. */
+  Kind d_kind;
+
+  /**
+   * The internal expression wrapped by this operator.
+   * This is a shared_ptr rather than a unique_ptr to avoid overhead due to
+   * memory allocation (CVC4::Expr is already ref counted, so this could be
+   * a unique_ptr instead).
+   */
+  std::shared_ptr<CVC4::Expr> d_expr;
+
+  /**
+   * Note: An indexed operator has a non-null internal expr, d_expr
+   * Note 2: We use a helper method to avoid having API functions call
+   *         other API functions (we need to call this internally)
+   * @return true iff this Op is indexed
+   */
+  bool isIndexedHelper() const;
+};
+
+/* -------------------------------------------------------------------------- */
 /* Term                                                                       */
 /* -------------------------------------------------------------------------- */
 
@@ -591,6 +715,17 @@ class CVC4_PUBLIC Term
   Sort getSort() const;
 
   /**
+   * @return true iff this term has an operator
+   */
+  bool hasOp() const;
+
+  /**
+   * @return the Op used to create this term
+   * Note: This is safe to call when hasOp() returns true.
+   */
+  Op getOp() const;
+
+  /**
    * @return true if this Term is a null term
    */
   bool isNull() const;
@@ -668,6 +803,9 @@ class CVC4_PUBLIC Term
 
   /**
    * Iterator for the children of a Term.
+   * Note: This treats uninterpreted functions as Term just like any other term
+   *       for example, the term f(x, y) will have Kind APPLY_UF and three
+   *       children: f, x, and y
    */
   class const_iterator : public std::iterator<std::input_iterator_tag, Term>
   {
@@ -675,19 +813,21 @@ class CVC4_PUBLIC Term
 
    public:
     /**
-     * Constructor.
+     * Null Constructor.
      */
     const_iterator();
 
     /**
-     * Copy constructor.
+     * Constructor
+     * @param e a shared pointer to the expression that we're iterating over
+     * @param p the position of the iterator (e.g. which child it's on)
      */
-    const_iterator(const const_iterator& it);
+    const_iterator(const std::shared_ptr<CVC4::Expr>& e, uint32_t p);
 
     /**
-     * Destructor.
+     * Copy constructor.
      */
-    ~const_iterator();
+    const_iterator(const const_iterator& it);
 
     /**
      * Assignment operator.
@@ -729,10 +869,10 @@ class CVC4_PUBLIC Term
     Term operator*() const;
 
    private:
-    /* The internal expression iterator wrapped by this iterator. */
-    void* d_iterator;
-    /* Constructor. */
-    explicit const_iterator(void*);
+    /* The original expression to be iteratoed over */
+    std::shared_ptr<CVC4::Expr> d_orig_expr;
+    /* Keeps track of the iteration position */
+    uint32_t d_pos;
   };
 
   /**
@@ -827,119 +967,20 @@ std::ostream& operator<<(std::ostream& out,
                          const std::unordered_map<Term, V, TermHashFunction>&
                              unordered_map) CVC4_PUBLIC;
 
-/* -------------------------------------------------------------------------- */
-/* OpTerm                                                                     */
-/* -------------------------------------------------------------------------- */
-
-/**
- * A CVC4 operator term.
- * An operator term is a term that represents certain operators, instantiated
- * with its required parameters, e.g., a term of kind BITVECTOR_EXTRACT.
- */
-class CVC4_PUBLIC OpTerm
-{
-  friend class Solver;
-  friend struct OpTermHashFunction;
-
- public:
-  /**
-   * Constructor.
-   */
-  OpTerm();
-
-  // !!! This constructor is only temporarily public until the parser is fully
-  // migrated to the new API. !!!
-  /**
-   * Constructor.
-   * @param e the internal expression that is to be wrapped by this term
-   * @return the Term
-   */
-  OpTerm(const CVC4::Expr& e);
-
-  /**
-   * Destructor.
-   */
-  ~OpTerm();
-
-  /**
-   * Syntactic equality operator.
-   * Return true if both operator terms are syntactically identical.
-   * Both operator terms must belong to the same solver object.
-   * @param t the operator term to compare to for equality
-   * @return true if the operator terms are equal
-   */
-  bool operator==(const OpTerm& t) const;
-
-  /**
-   * Syntactic disequality operator.
-   * Return true if both operator terms differ syntactically.
-   * Both terms must belong to the same solver object.
-   * @param t the operator term to compare to for disequality
-   * @return true if operator terms are disequal
-   */
-  bool operator!=(const OpTerm& t) const;
-
-  /**
-   * @return the kind of this operator term
-   */
-  Kind getKind() const;
-
-  /**
-   * @return the sort of this operator term
-   */
-  Sort getSort() const;
-
-  /**
-   * @return true if this operator term is a null term
-   */
-  bool isNull() const;
-
-  /**
-   * Get the indices used to create this OpTerm.
-   * Supports the following template arguments:
-   *   - string
-   *   - Kind
-   *   - uint32_t
-   *   - pair<uint32_t, uint32_t>
-   * Check the OpTerm Kind with getKind() to determine which argument to use.
-   * @return the indices used to create this OpTerm
-   */
-  template <typename T>
-  T getIndices() const;
-
-  /**
-   * @return a string representation of this operator term
-   */
-  std::string toString() const;
-
-  // !!! This is only temporarily available until the parser is fully migrated
-  // to the new API. !!!
-  CVC4::Expr getExpr(void) const;
-
- private:
-  /**
-   * The internal expression wrapped by this operator term.
-   * This is a shared_ptr rather than a unique_ptr to avoid overhead due to
-   * memory allocation (CVC4::Expr is already ref counted, so this could be
-   * a unique_ptr instead).
-   */
-  std::shared_ptr<CVC4::Expr> d_expr;
-};
-
 /**
- * Serialize an operator term to given stream.
+ * Serialize an operator to given stream.
  * @param out the output stream
- * @param t the operator term to be serialized to the given output stream
+ * @param t the operator to be serialized to the given output stream
  * @return the output stream
  */
-std::ostream& operator<<(std::ostream& out, const OpTerm& t) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& out, const Op& t) CVC4_PUBLIC;
 
 /**
- * Hash function for OpTerms.
+ * Hash function for Ops.
  */
-struct CVC4_PUBLIC OpTermHashFunction
+struct CVC4_PUBLIC OpHashFunction
 {
-  size_t operator()(const OpTerm& t) const;
+  size_t operator()(const Op& t) const;
 };
 
 /* -------------------------------------------------------------------------- */
@@ -1143,7 +1184,7 @@ class CVC4_PUBLIC DatatypeSelector
    * Get the selector operator of this datatype selector.
    * @return the selector operator
    */
-  OpTerm getSelectorTerm() const;
+  Op getSelectorTerm() const;
 
   /**
    * @return a string representation of this datatype selector
@@ -1200,7 +1241,7 @@ class CVC4_PUBLIC DatatypeConstructor
    * Get the constructor operator of this datatype constructor.
    * @return the constructor operator
    */
-  OpTerm getConstructorTerm() const;
+  Op getConstructorTerm() const;
 
   /**
    * Get the datatype selector with the given name.
@@ -1219,7 +1260,7 @@ class CVC4_PUBLIC DatatypeConstructor
    * @param name the name of the datatype selector
    * @return a term representing the datatype selector with the given name
    */
-  OpTerm getSelectorTerm(const std::string& name) const;
+  Op getSelectorTerm(const std::string& name) const;
 
   /**
    * @return a string representation of this datatype constructor
@@ -1366,7 +1407,7 @@ class CVC4_PUBLIC Datatype
    * similarly-named constructors, the
    * first is returned.
    */
-  OpTerm getConstructorTerm(const std::string& name) const;
+  Op getConstructorTerm(const std::string& name) const;
 
   /** Get the number of constructors for this Datatype. */
   size_t getNumConstructors() const;
@@ -1773,59 +1814,52 @@ class CVC4_PUBLIC Solver
   Term mkTerm(Kind kind, const std::vector<Term>& children) const;
 
   /**
-   * Create nullary term of given kind from a given operator term.
-   * Create operator terms with mkOpTerm().
-   * @param kind the kind of the term
-   * @param the operator term
+   * Create nullary term of given kind from a given operator.
+   * Create operators with mkOp().
+   * @param the operator
    * @return the Term
    */
-  Term mkTerm(Kind kind, OpTerm opTerm) const;
+  Term mkTerm(Op op) const;
 
   /**
-   * Create unary term of given kind from a given operator term.
-   * Create operator terms with mkOpTerm().
-   * @param kind the kind of the term
-   * @param the operator term
+   * Create unary term of given kind from a given operator.
+   * Create operators with mkOp().
+   * @param the operator
    * @child the child of the term
    * @return the Term
    */
-  Term mkTerm(Kind kind, OpTerm opTerm, Term child) const;
+  Term mkTerm(Op op, Term child) const;
 
   /**
-   * Create binary term of given kind from a given operator term.
-   * @param kind the kind of the term
-   * Create operator terms with mkOpTerm().
-   * @param the operator term
+   * Create binary term of given kind from a given operator.
+   * Create operators with mkOp().
+   * @param the operator
    * @child1 the first child of the term
    * @child2 the second child of the term
    * @return the Term
    */
-  Term mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2) const;
+  Term mkTerm(Op op, Term child1, Term child2) const;
 
   /**
-   * Create ternary term of given kind from a given operator term.
-   * Create operator terms with mkOpTerm().
-   * @param kind the kind of the term
-   * @param the operator term
+   * Create ternary term of given kind from a given operator.
+   * Create operators with mkOp().
+   * @param the operator
    * @child1 the first child of the term
    * @child2 the second child of the term
    * @child3 the third child of the term
    * @return the Term
    */
-  Term mkTerm(
-      Kind kind, OpTerm opTerm, Term child1, Term child2, Term child3) const;
+  Term mkTerm(Op op, Term child1, Term child2, Term child3) const;
 
   /**
-   * Create n-ary term of given kind from a given operator term.
-   * Create operator terms with mkOpTerm().
+   * Create n-ary term of given kind from a given operator.
+   * Create operators with mkOp().
    * @param kind the kind of the term
-   * @param the operator term
+   * @param the operator
    * @children the children of the term
    * @return the Term
    */
-  Term mkTerm(Kind kind,
-              OpTerm opTerm,
-              const std::vector<Term>& children) const;
+  Term mkTerm(Op op, const std::vector<Term>& children) const;
 
   /**
    * Create a tuple term. Terms are automatically converted if sorts are
@@ -1842,59 +1876,59 @@ class CVC4_PUBLIC Solver
   /* .................................................................... */
 
   /**
-   * Create operator term of kind:
-   *   - CHAIN_OP
+   * Create operator of kind:
+   *   - CHAIN
    * See enum Kind for a description of the parameters.
    * @param kind the kind of the operator
    * @param k the kind argument to this operator
    */
-  OpTerm mkOpTerm(Kind kind, Kind k) const;
+  Op mkOp(Kind kind, Kind k) const;
 
   /**
    * Create operator of kind:
-   *   - RECORD_UPDATE_OP
-   *   - DIVISIBLE_OP (to support arbitrary precision integers)
+   *   - RECORD_UPDATE
+   *   - DIVISIBLE (to support arbitrary precision integers)
    * See enum Kind for a description of the parameters.
    * @param kind the kind of the operator
    * @param arg the string argument to this operator
    */
-  OpTerm mkOpTerm(Kind kind, const std::string& arg) const;
+  Op mkOp(Kind kind, const std::string& arg) const;
 
   /**
    * Create operator of kind:
-   *   - DIVISIBLE_OP
-   *   - BITVECTOR_REPEAT_OP
-   *   - BITVECTOR_ZERO_EXTEND_OP
-   *   - BITVECTOR_SIGN_EXTEND_OP
-   *   - BITVECTOR_ROTATE_LEFT_OP
-   *   - BITVECTOR_ROTATE_RIGHT_OP
-   *   - INT_TO_BITVECTOR_OP
-   *   - FLOATINGPOINT_TO_UBV_OP
-   *   - FLOATINGPOINT_TO_UBV_TOTAL_OP
-   *   - FLOATINGPOINT_TO_SBV_OP
-   *   - FLOATINGPOINT_TO_SBV_TOTAL_OP
-   *   - TUPLE_UPDATE_OP
+   *   - DIVISIBLE
+   *   - BITVECTOR_REPEAT
+   *   - BITVECTOR_ZERO_EXTEND
+   *   - BITVECTOR_SIGN_EXTEND
+   *   - BITVECTOR_ROTATE_LEFT
+   *   - BITVECTOR_ROTATE_RIGHT
+   *   - INT_TO_BITVECTOR
+   *   - FLOATINGPOINT_TO_UBV
+   *   - FLOATINGPOINT_TO_UBV_TOTAL
+   *   - FLOATINGPOINT_TO_SBV
+   *   - FLOATINGPOINT_TO_SBV_TOTAL
+   *   - TUPLE_UPDATE
    * See enum Kind for a description of the parameters.
    * @param kind the kind of the operator
    * @param arg the uint32_t argument to this operator
    */
-  OpTerm mkOpTerm(Kind kind, uint32_t arg) const;
+  Op mkOp(Kind kind, uint32_t arg) const;
 
   /**
    * Create operator of Kind:
-   *   - BITVECTOR_EXTRACT_OP
-   *   - FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP
-   *   - FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP
-   *   - FLOATINGPOINT_TO_FP_REAL_OP
-   *   - FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP
-   *   - FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP
-   *   - FLOATINGPOINT_TO_FP_GENERIC_OP
+   *   - BITVECTOR_EXTRACT
+   *   - FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
+   *   - FLOATINGPOINT_TO_FP_FLOATINGPOINT
+   *   - FLOATINGPOINT_TO_FP_REAL
+   *   - FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
+   *   - FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
+   *   - FLOATINGPOINT_TO_FP_GENERIC
    * See enum Kind for a description of the parameters.
    * @param kind the kind of the operator
    * @param arg1 the first uint32_t argument to this operator
    * @param arg2 the second uint32_t argument to this operator
    */
-  OpTerm mkOpTerm(Kind kind, uint32_t arg1, uint32_t arg2) const;
+  Op mkOp(Kind kind, uint32_t arg1, uint32_t arg2) const;
 
   /* .................................................................... */
   /* Create Constants                                                     */
@@ -2537,9 +2571,7 @@ class CVC4_PUBLIC Solver
   std::vector<Type> sortVectorToTypes(const std::vector<Sort>& vector) const;
   /* Helper to convert a vector of sorts to internal types. */
   std::vector<Expr> termVectorToExprs(const std::vector<Term>& vector) const;
-  /* Helper to check for API misuse in mkTerm functions. */
-  void checkMkOpTerm(Kind kind, OpTerm opTerm, uint32_t nchildren) const;
-  /* Helper to check for API misuse in mkOpTerm functions. */
+  /* Helper to check for API misuse in mkOp functions. */
   void checkMkTerm(Kind kind, uint32_t nchildren) const;
   /* Helper for mk-functions that call d_exprMgr->mkConst(). */
   template <typename T>
@@ -2555,6 +2587,8 @@ class CVC4_PUBLIC Solver
   Term mkBVFromIntHelper(uint32_t size, uint64_t val) const;
   /* Helper for setLogic. */
   void setLogicHelper(const std::string& logic) const;
+  /* Helper for mkTerm functions that create Term from a Kind */
+  Term mkTermFromKind(Kind kind) const;
 
   /**
    * Helper function that ensures that a given term is of sort real (as opposed
diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h
index 1f2a36676..bb2700706 100644
--- a/src/api/cvc4cppkind.h
+++ b/src/api/cvc4cppkind.h
@@ -143,26 +143,24 @@ enum CVC4_PUBLIC Kind : int32_t
    */
   CHOICE,
   /**
-   * Chained operation.
+   * Chained operator.
+   * Parameters: 1
+   *   -[1]: Kind of the binary operation
+   * Create with:
+   *   mkOp(Kind opkind, Kind kind)
+
+   * Apply chained operation.
    * Parameters: n > 1
-   *   -[1]: Term of kind CHAIN_OP (represents a binary op)
+   *   -[1]: Op of kind CHAIN (represents a binary op)
    *   -[2]..[n]: Arguments to that operator
    * Create with:
-   *   mkTerm(Kind kind, Term child1, Term child2)
-   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
-   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   *   mkTerm(Op op, Term child1, Term child2)
+   *   mkTerm(Op op, Term child1, Term child2, Term child3)
+   *   mkTerm(Op op, const std::vector<Term>& children)
    * Turned into a conjunction of binary applications of the operator on
    * adjoining parameters.
    */
   CHAIN,
-  /**
-   * Chained operator.
-   * Parameters: 1
-   *   -[1]: Kind of the binary operation
-   * Create with:
-   *   mkOpTerm(Kind opkind, Kind kind)
-   */
-  CHAIN_OP,
 
   /* Boolean --------------------------------------------------------------- */
 
@@ -382,16 +380,6 @@ enum CVC4_PUBLIC Kind : int32_t
    */
   ABS,
   /**
-   * Divisibility-by-k predicate.
-   * Parameters: 2
-   *   -[1]: DIVISIBLE_OP Term
-   *   -[2]: Integer Term
-   * Create with:
-   *   mkTerm(Kind kind, Term child1, Term child2)
-   *   mkTerm(Kind kind, const std::vector<Term>& children)
-   */
-  DIVISIBLE,
-  /**
    * Arithmetic power.
    * Parameters: 2
    *   -[1]..[2]: Terms of sort Integer, Real
@@ -517,9 +505,17 @@ enum CVC4_PUBLIC Kind : int32_t
    * Parameter: 1
    *   -[1]: The k to divide by (sort Integer)
    * Create with:
-   *   mkOpTerm(Kind kind, uint32_t param)
+   *   mkOp(Kind kind, uint32_t param)
+   *
+   * Apply divisibility-by-k predicate.
+   * Parameters: 2
+   *   -[1]: Op of kind DIVISIBLE
+   *   -[2]: Integer Term
+   * Create with:
+   *   mkTerm(Op op, Term child1, Term child2)
+   *   mkTerm(Op op, const std::vector<Term>& children)
    */
-  DIVISIBLE_OP,
+  DIVISIBLE,
   /**
    * Multiple-precision rational constant.
    * Parameters:
@@ -973,9 +969,6 @@ enum CVC4_PUBLIC Kind : int32_t
   /* term to be treated as a variable. used for eager bit-blasting Ackermann
    * expansion of bvurem (internal-only symbol) */
   BITVECTOR_ACKERMANIZE_UREM,
-  /* operator for the bit-vector boolean bit extract.
-   * One parameter, parameter is the index of the bit to extract */
-  BITVECTOR_BITOF_OP,
 #endif
   /**
    * Operator for bit-vector extract (from index 'high' to 'low').
@@ -983,125 +976,115 @@ enum CVC4_PUBLIC Kind : int32_t
    *   -[1]: The 'high' index
    *   -[2]: The 'low' index
    * Create with:
-   *   mkOpTerm(Kind kind, uint32_t param, uint32_t param)
+   *   mkOp(Kind kind, uint32_t param, uint32_t param)
+   *
+   * Apply bit-vector extract.
+   * Parameters: 2
+   *   -[1]: Op of kind BITVECTOR_EXTRACT
+   *   -[2]: Term of bit-vector sort
+   * Create with:
+   *   mkTerm(Op op, Term child)
+   *   mkTerm(Op op, const std::vector<Term>& children)
    */
-  BITVECTOR_EXTRACT_OP,
+  BITVECTOR_EXTRACT,
   /**
    * Operator for bit-vector repeat.
    * Parameter 1:
    *   -[1]: Number of times to repeat a given bit-vector
    * Create with:
-   *   mkOpTerm(Kind kind, uint32_t param).
+   *   mkOp(Kind kind, uint32_t param).
+   *
+   * Apply bit-vector repeat.
+   * Parameters: 2
+   *   -[1]: Op of kind BITVECTOR_REPEAT
+   *   -[2]: Term of bit-vector sort
+   * Create with:
+   *   mkTerm(Op op, Term child)
+   *   mkTerm(Op op, const std::vector<Term>& children)
    */
-  BITVECTOR_REPEAT_OP,
+  BITVECTOR_REPEAT,
   /**
    * Operator for bit-vector zero-extend.
    * Parameter 1:
    *   -[1]: Number of bits by which a given bit-vector is to be extended
    * Create with:
-   *   mkOpTerm(Kind kind, uint32_t param).
+   *   mkOp(Kind kind, uint32_t param).
+   *
+   * Apply bit-vector zero-extend.
+   * Parameters: 2
+   *   -[1]: Op of kind BITVECTOR_ZERO_EXTEND
+   *   -[2]: Term of bit-vector sort
+   * Create with:
+   *   mkTerm(Op op, Term child)
+   *   mkTerm(Op op, const std::vector<Term>& children)
    */
-  BITVECTOR_ZERO_EXTEND_OP,
+  BITVECTOR_ZERO_EXTEND,
   /**
    * Operator for bit-vector sign-extend.
    * Parameter 1:
    *   -[1]: Number of bits by which a given bit-vector is to be extended
    * Create with:
-   *   mkOpTerm(Kind kind, uint32_t param).
-   */
-  BITVECTOR_SIGN_EXTEND_OP,
-  /**
-   * Operator for bit-vector rotate left.
-   * Parameter 1:
-   *   -[1]: Number of bits by which a given bit-vector is to be rotated
+   *   mkOp(Kind kind, uint32_t param).
+   *
+   * Apply bit-vector sign-extend.
+   * Parameters: 2
+   *   -[1]: Op of kind BITVECTOR_SIGN_EXTEND
+   *   -[2]: Term of bit-vector sort
    * Create with:
-   *   mkOpTerm(Kind kind, uint32_t param).
+   *   mkTerm(Op op, Term child)
+   *   mkTerm(Op op, const std::vector<Term>& children)
    */
-  BITVECTOR_ROTATE_LEFT_OP,
+  BITVECTOR_SIGN_EXTEND,
   /**
-   * Operator for bit-vector rotate right.
+   * Operator for bit-vector rotate left.
    * Parameter 1:
    *   -[1]: Number of bits by which a given bit-vector is to be rotated
    * Create with:
-   *   mkOpTerm(Kind kind, uint32_t param).
-   */
-  BITVECTOR_ROTATE_RIGHT_OP,
-#if 0
-  /* bit-vector boolean bit extract.
-   * first parameter is a BITVECTOR_BITOF_OP, second is a bit-vector term */
-  BITVECTOR_BITOF,
-#endif
-  /* Bit-vector extract.
-   * Parameters: 2
-   *   -[1]: BITVECTOR_EXTRACT_OP Term
-   *   -[2]: Term of bit-vector sort
-   * Create with:
-   *   mkTerm(Term opTerm, Term child)
-   *   mkTerm(Term opTerm, const std::vector<Term>& children)
-   */
-  BITVECTOR_EXTRACT,
-  /* Bit-vector repeat.
-   * Parameters: 2
-   *   -[1]: BITVECTOR_REPEAT_OP Term
-   *   -[2]: Term of bit-vector sort
-   * Create with:
-   *   mkTerm(Term opTerm, Term child)
-   *   mkTerm(Term opTerm, const std::vector<Term>& children)
-   */
-  BITVECTOR_REPEAT,
-  /* Bit-vector zero-extend.
-   * Parameters: 2
-   *   -[1]: BITVECTOR_ZERO_EXTEND_OP Term
-   *   -[2]: Term of bit-vector sort
-   * Create with:
-   *   mkTerm(Term opTerm, Term child)
-   *   mkTerm(Term opTerm, const std::vector<Term>& children)
-   */
-  BITVECTOR_ZERO_EXTEND,
-  /* Bit-vector sign-extend.
-   * Parameters: 2
-   *   -[1]: BITVECTOR_SIGN_EXTEND_OP Term
-   *   -[2]: Term of bit-vector sort
-   * Create with:
-   *   mkTerm(Term opTerm, Term child)
-   *   mkTerm(Term opTerm, const std::vector<Term>& children)
-   */
-  BITVECTOR_SIGN_EXTEND,
-  /* Bit-vector rotate left.
+   *   mkOp(Kind kind, uint32_t param).
+   *
+   * Apply bit-vector rotate left.
    * Parameters: 2
-   *   -[1]: BITVECTOR_ROTATE_LEFT_OP Term
+   *   -[1]: Op of kind BITVECTOR_ROTATE_LEFT
    *   -[2]: Term of bit-vector sort
    * Create with:
-   *   mkTerm(Term opTerm, Term child)
-   *   mkTerm(Term opTerm, const std::vector<Term>& children)
+   *   mkTerm(Op op, Term child)
+   *   mkTerm(Op op, const std::vector<Term>& children)
    */
   BITVECTOR_ROTATE_LEFT,
   /**
-   * Bit-vector rotate right.
+   * Operator for bit-vector rotate right.
+   * Parameter 1:
+   *   -[1]: Number of bits by which a given bit-vector is to be rotated
+   * Create with:
+   *   mkOp(Kind kind, uint32_t param).
+   *
+   * Apply bit-vector rotate right.
    * Parameters: 2
-   *   -[1]: BITVECTOR_ROTATE_RIGHT_OP Term
+   *   -[1]: Op of kind BITVECTOR_ROTATE_RIGHT
    *   -[2]: Term of bit-vector sort
    * Create with:
-   *   mkTerm(Term opTerm, Term child)
-   *   mkTerm(Term opTerm, const std::vector<Term>& children)
+   *   mkTerm(Op op, Term child)
+   *   mkTerm(Op op, const std::vector<Term>& children)
    */
   BITVECTOR_ROTATE_RIGHT,
+#if 0
+  /* bit-vector boolean bit extract. */
+  BITVECTOR_BITOF,
+#endif
   /**
    * Operator for the conversion from Integer to bit-vector.
    * Parameter: 1
    *   -[1]: Size of the bit-vector to convert to
    * Create with:
-   *   mkOpTerm(Kind kind, uint32_t param).
-   */
-  INT_TO_BITVECTOR_OP,
-  /**
-   * Integer conversion to bit-vector.
+   *   mkOp(Kind kind, uint32_t param).
+   *
+   * Apply integer conversion to bit-vector.
    * Parameters: 2
-   *   -[1]: INT_TO_BITVECTOR_OP Term
+   *   -[1]: Op of kind INT_TO_BITVECTOR
    *   -[2]: Integer term
    * Create with:
-   *   mkTerm(Kind kind, Term child1, Term child2)
-   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   *   mkTerm(Op op, Term child)
+   *   mkTerm(Op op, const std::vector<Term>& children)
    */
   INT_TO_BITVECTOR,
   /**
@@ -1371,17 +1354,15 @@ enum CVC4_PUBLIC Kind : int32_t
    *   -[1]: Exponent size
    *   -[2]: Significand size
    * Create with:
-   *   mkOpTerm(Kind kind, uint32_t param1, uint32_t param2)
-   */
-  FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP,
-  /**
+   *   mkOp(Kind kind, uint32_t param1, uint32_t param2)
+   *
    * Conversion from an IEEE-754 bit vector to floating-point.
    * Parameters: 2
-   *   -[1]: FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP Term
+   *   -[1]: Op of kind FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
    *   -[2]: Term of sort FloatingPoint
    * Create with:
-   *   mkTerm(Term opTerm, Term child)
-   *   mkTerm(Term opTerm, const std::vector<Term>& children)
+   *   mkTerm(Op op, Term child)
+   *   mkTerm(Op op, const std::vector<Term>& children)
    */
   FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
   /**
@@ -1390,17 +1371,15 @@ enum CVC4_PUBLIC Kind : int32_t
    *   -[1]: Exponent size
    *   -[2]: Significand size
    * Create with:
-   *   mkOpTerm(Kind kind, uint32_t param1, uint32_t param2)
-   */
-  FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP,
-  /**
+   *   mkOp(Kind kind, uint32_t param1, uint32_t param2)
+   *
    * Conversion between floating-point sorts.
    * Parameters: 2
-   *   -[1]: FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP Term
+   *   -[1]: Op of kind FLOATINGPOINT_TO_FP_FLOATINGPOINT
    *   -[2]: Term of sort FloatingPoint
    * Create with:
-   *   mkTerm(Term opTerm, Term child)
-   *   mkTerm(Term opTerm, const std::vector<Term>& children)
+   *   mkTerm(Op op, Term child)
+   *   mkTerm(Op op, const std::vector<Term>& children)
    */
   FLOATINGPOINT_TO_FP_FLOATINGPOINT,
   /**
@@ -1409,17 +1388,15 @@ enum CVC4_PUBLIC Kind : int32_t
    *   -[1]: Exponent size
    *   -[2]: Significand size
    * Create with:
-   *   mkOpTerm(Kind kind, uint32_t param1, uint32_t param2)
-   */
-  FLOATINGPOINT_TO_FP_REAL_OP,
-  /**
+   *   mkOp(Kind kind, uint32_t param1, uint32_t param2)
+   *
    * Conversion from a real to floating-point.
    * Parameters: 2
-   *   -[1]: FLOATINGPOINT_TO_FP_REAL_OP Term
+   *   -[1]: Op of kind FLOATINGPOINT_TO_FP_REAL
    *   -[2]: Term of sort FloatingPoint
    * Create with:
-   *   mkTerm(Term opTerm, Term child)
-   *   mkTerm(Term opTerm, const std::vector<Term>& children)
+   *   mkTerm(Op op, Term child)
+   *   mkTerm(Op op, const std::vector<Term>& children)
    */
   FLOATINGPOINT_TO_FP_REAL,
   /*
@@ -1428,17 +1405,15 @@ enum CVC4_PUBLIC Kind : int32_t
    *   -[1]: Exponent size
    *   -[2]: Significand size
    * Create with:
-   *   mkOpTerm(Kind kind, uint32_t param1, uint32_t param2)
-   */
-  FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP,
-  /**
+   *   mkOp(Kind kind, uint32_t param1, uint32_t param2)
+   *
    * Conversion from a signed bit vector to floating-point.
    * Parameters: 2
-   *   -[1]: FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP Term
+   *   -[1]: Op of kind FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
    *   -[2]: Term of sort FloatingPoint
    * Create with:
-   *   mkTerm(Term opTerm, Term child)
-   *   mkTerm(Term opTerm, const std::vector<Term>& children)
+   *   mkTerm(Op op, Term child)
+   *   mkTerm(Op op, const std::vector<Term>& children)
    */
   FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
   /**
@@ -1447,17 +1422,15 @@ enum CVC4_PUBLIC Kind : int32_t
    *   -[1]: Exponent size
    *   -[2]: Significand size
    * Create with:
-   *   mkOpTerm(Kind kind, uint32_t param1, uint32_t param2)
-   */
-  FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP,
-  /**
-   * Operator for converting an unsigned bit vector to floating-point.
+   *   mkOp(Kind kind, uint32_t param1, uint32_t param2)
+   *
+   * Converting an unsigned bit vector to floating-point.
    * Parameters: 2
-   *   -[1]: FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP Term
+   *   -[1]: Op of kind FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
    *   -[2]: Term of sort FloatingPoint
    * Create with:
-   *   mkTerm(Term opTerm, Term child)
-   *   mkTerm(Term opTerm, const std::vector<Term>& children)
+   *   mkTerm(Op op, Term child)
+   *   mkTerm(Op op, const std::vector<Term>& children)
    */
   FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
   /**
@@ -1466,17 +1439,15 @@ enum CVC4_PUBLIC Kind : int32_t
    *   -[1]: exponent size
    *   -[2]: Significand size
    * Create with:
-   *   mkOpTerm(Kind kind, uint32_t param1, uint32_t param2)
-   */
-  FLOATINGPOINT_TO_FP_GENERIC_OP,
-  /**
+   *   mkOp(Kind kind, uint32_t param1, uint32_t param2)
+   *
    * Generic conversion to floating-point, used in parsing only.
    * Parameters: 2
-   *   -[1]: FLOATINGPOINT_TO_FP_GENERIC_OP Term
+   *   -[1]: Op of kind FLOATINGPOINT_TO_FP_GENERIC
    *   -[2]: Term of sort FloatingPoint
    * Create with:
-   *   mkTerm(Term opTerm, Term child)
-   *   mkTerm(Term opTerm, const std::vector<Term>& children)
+   *   mkTerm(Op op, Term child)
+   *   mkTerm(Op op, const std::vector<Term>& children)
    */
   FLOATINGPOINT_TO_FP_GENERIC,
   /**
@@ -1484,17 +1455,15 @@ enum CVC4_PUBLIC Kind : int32_t
    * Parameters: 1
    *   -[1]: Size of the bit-vector to convert to
    * Create with:
-   *   mkOpTerm(Kind kind, uint32_t param)
-   */
-  FLOATINGPOINT_TO_UBV_OP,
-  /**
+   *   mkOp(Kind kind, uint32_t param)
+   *
    * Conversion from a floating-point value to an unsigned bit vector.
    * Parameters: 2
-   *   -[1]: FLOATINGPOINT_TO_FP_TO_UBV_OP Term
+   *   -[1]: Op of kind FLOATINGPOINT_TO_FP_TO_UBV
    *   -[2]: Term of sort FloatingPoint
    * Create with:
-   *   mkTerm(Term opTerm, Term child)
-   *   mkTerm(Term opTerm, const std::vector<Term>& children)
+   *   mkTerm(Op op, Term child)
+   *   mkTerm(Op op, const std::vector<Term>& children)
    */
   FLOATINGPOINT_TO_UBV,
   /**
@@ -1502,18 +1471,16 @@ enum CVC4_PUBLIC Kind : int32_t
    * Parameters: 1
    *   -[1]: Size of the bit-vector to convert to
    * Create with:
-   *   mkOpTerm(Kind kind, uint32_t param)
-   */
-  FLOATINGPOINT_TO_UBV_TOTAL_OP,
-  /**
+   *   mkOp(Kind kind, uint32_t param)
+   *
    * Conversion from  a floating-point value to an unsigned bit vector
    * (defined for all inputs).
    * Parameters: 2
-   *   -[1]: FLOATINGPOINT_TO_FP_TO_UBV_TOTAL_OP Term
+   *   -[1]: Op of kind FLOATINGPOINT_TO_FP_TO_UBV_TOTAL
    *   -[2]: Term of sort FloatingPoint
    * Create with:
-   *   mkTerm(Term opTerm, Term child)
-   *   mkTerm(Term opTerm, const std::vector<Term>& children)
+   *   mkTerm(Op op, Term child)
+   *   mkTerm(Op op, const std::vector<Term>& children)
    */
   FLOATINGPOINT_TO_UBV_TOTAL,
   /**
@@ -1521,17 +1488,15 @@ enum CVC4_PUBLIC Kind : int32_t
    * Parameters: 1
    *   -[1]: Size of the bit-vector to convert to
    * Create with:
-   *   mkOpTerm(Kind kind, uint32_t param)
-   */
-  FLOATINGPOINT_TO_SBV_OP,
-  /**
+   *   mkOp(Kind kind, uint32_t param)
+   *
    * Conversion from a floating-point value to a signed bit vector.
    * Parameters: 2
-   *   -[1]: FLOATINGPOINT_TO_FP_TO_SBV_OP Term
+   *   -[1]: Op of kind FLOATINGPOINT_TO_FP_TO_SBV
    *   -[2]: Term of sort FloatingPoint
    * Create with:
-   *   mkTerm(Term opTerm, Term child)
-   *   mkTerm(Term opTerm, const std::vector<Term>& children)
+   *   mkTerm(Op op, Term child)
+   *   mkTerm(Op op, const std::vector<Term>& children)
    */
   FLOATINGPOINT_TO_SBV,
   /**
@@ -1539,18 +1504,16 @@ enum CVC4_PUBLIC Kind : int32_t
    * Parameters: 1
    *   -[1]: Size of the bit-vector to convert to
    * Create with:
-   *   mkOpTerm(Kind kind, uint32_t param)
-   */
-  FLOATINGPOINT_TO_SBV_TOTAL_OP,
-  /**
+   *   mkOp(Kind kind, uint32_t param)
+   *
    * Conversion from a floating-point value to a signed bit vector
    * (defined for all inputs).
    * Parameters: 2
-   *   -[1]: FLOATINGPOINT_TO_FP_TO_SBV_TOTAL_OP Term
+   *   -[1]: Op of kind FLOATINGPOINT_TO_FP_TO_SBV_TOTAL
    *   -[2]: Term of sort FloatingPoint
    * Create with:
-   *   mkTerm(Term opTerm, Term child)
-   *   mkTerm(Term opTerm, const std::vector<Term>& children)
+   *   mkTerm(Op op, Term child)
+   *   mkTerm(Op op, const std::vector<Term>& children)
    */
   FLOATINGPOINT_TO_SBV_TOTAL,
   /**
@@ -1578,8 +1541,8 @@ enum CVC4_PUBLIC Kind : int32_t
    *   -[1]: Term of array sort
    *   -[2]: Selection index
    * Create with:
-   *   mkTerm(Term opTerm, Term child1, Term child2)
-   *   mkTerm(Term opTerm, const std::vector<Term>& children)
+   *   mkTerm(Op op, Term child1, Term child2)
+   *   mkTerm(Op op, const std::vector<Term>& children)
    */
   SELECT,
   /**
@@ -1589,8 +1552,8 @@ enum CVC4_PUBLIC Kind : int32_t
    *   -[2]: Store index
    *   -[3]: Term to store at the index
    * Create with:
-   *   mkTerm(Term opTerm, Term child1, Term child2, Term child3)
-   *   mkTerm(Term opTerm, const std::vector<Term>& children)
+   *   mkTerm(Op op, Term child1, Term child2, Term child3)
+   *   mkTerm(Op op, const std::vector<Term>& children)
    */
   STORE,
   /**
@@ -1599,8 +1562,8 @@ enum CVC4_PUBLIC Kind : int32_t
    *   -[1]: Array sort
    *   -[2]: Term representing a constant
    * Create with:
-   *   mkTerm(Term opTerm, Term child1, Term child2)
-   *   mkTerm(Term opTerm, const std::vector<Term>& children)
+   *   mkTerm(Op op, Term child1, Term child2)
+   *   mkTerm(Op op, const std::vector<Term>& children)
    *
    * Note: We currently support the creation of constant arrays, but under some
    * conditions when there is a chain of equalities connecting two constant
@@ -1623,32 +1586,32 @@ enum CVC4_PUBLIC Kind : int32_t
   /**
    * Constructor application.
    * Paramters: n > 0
-   *   -[1]: Constructor (operator term)
+   *   -[1]: Constructor (operator)
    *   -[2]..[n]: Parameters to the constructor
    * Create with:
-   *   mkTerm(Kind kind, OpTerm opTerm)
-   *   mkTerm(Kind kind, OpTerm opTerm, Term child)
-   *   mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2)
-   *   mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2, Term child3)
-   *   mkTerm(Kind kind, OpTerm opTerm, const std::vector<Term>& children)
+   *   mkTerm(Kind kind, Op op)
+   *   mkTerm(Kind kind, Op op, Term child)
+   *   mkTerm(Kind kind, Op op, Term child1, Term child2)
+   *   mkTerm(Kind kind, Op op, Term child1, Term child2, Term child3)
+   *   mkTerm(Kind kind, Op op, const std::vector<Term>& children)
    */
   APPLY_CONSTRUCTOR,
   /**
    * Datatype selector application.
    * Parameters: 1
-   *   -[1]: Selector (operator term)
+   *   -[1]: Selector (operator)
    *   -[2]: Datatype term (undefined if mis-applied)
    * Create with:
-   *   mkTerm(Kind kind, OpTerm opTerm, Term child)
+   *   mkTerm(Kind kind, Op op, Term child)
    */
   APPLY_SELECTOR,
   /**
    * Datatype selector application.
    * Parameters: 1
-   *   -[1]: Selector (operator term)
+   *   -[1]: Selector (operator)
    *   -[2]: Datatype term (defined rigidly if mis-applied)
    * Create with:
-   *   mkTerm(Kind kind, OpTerm opTerm, Term child)
+   *   mkTerm(Kind kind, Op op, Term child)
    */
   APPLY_SELECTOR_TOTAL,
   /**
@@ -1674,18 +1637,16 @@ enum CVC4_PUBLIC Kind : int32_t
    * Parameters: 1
    *   -[1]: Index of the tuple to be updated
    * Create with:
-   *   mkOpTerm(Kind kind, uint32_t param)
-   */
-  TUPLE_UPDATE_OP,
-  /**
-   * Tuple update.
+   *   mkOp(Kind kind, uint32_t param)
+   *
+   * Apply tuple update.
    * Parameters: 3
-   *   -[1]: TUPLE_UPDATE_OP (which references an index)
+   *   -[1]: Op of kind TUPLE_UPDATE (which references an index)
    *   -[2]: Tuple
    *   -[3]: Element to store in the tuple at the given index
    * Create with:
-   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
-   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   *   mkTerm(Op op, Term child1, Term child2)
+   *   mkTerm(Op op, const std::vector<Term>& children)
    */
   TUPLE_UPDATE,
   /**
@@ -1693,18 +1654,16 @@ enum CVC4_PUBLIC Kind : int32_t
    * Parameters: 1
    *   -[1]: Name of the field to be updated
    * Create with:
-   *   mkOpTerm(Kind kind, const std::string& param)
-   */
-  RECORD_UPDATE_OP,
-  /**
+   *   mkOp(Kind kind, const std::string& param)
+   *
    * Record update.
    * Parameters: 3
-   *   -[1]: RECORD_UPDATE_OP Term (which references a field)
+   *   -[1]: Op of kind RECORD_UPDATE (which references a field)
    *   -[2]: Record term to update
    *   -[3]: Element to store in the record in the given field
    * Create with:
-   *   mkTerm(Kind kind, Term child1, Term child2)
-   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   *   mkTerm(Op op, Term child1, Term child2)
+   *   mkTerm(Op op,, const std::vector<Term>& children)
    */
   RECORD_UPDATE,
 #if 0
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 6dc29b8fe..c7e70495e 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -123,23 +123,18 @@ void Smt2::addBitvectorOperators() {
   addOperator(kind::BITVECTOR_TO_NAT, "bv2nat");
 
   addIndexedOperator(
-      kind::BITVECTOR_EXTRACT, api::BITVECTOR_EXTRACT_OP, "extract");
+      kind::BITVECTOR_EXTRACT, api::BITVECTOR_EXTRACT, "extract");
+  addIndexedOperator(kind::BITVECTOR_REPEAT, api::BITVECTOR_REPEAT, "repeat");
   addIndexedOperator(
-      kind::BITVECTOR_REPEAT, api::BITVECTOR_REPEAT_OP, "repeat");
-  addIndexedOperator(kind::BITVECTOR_ZERO_EXTEND,
-                     api::BITVECTOR_ZERO_EXTEND_OP,
-                     "zero_extend");
-  addIndexedOperator(kind::BITVECTOR_SIGN_EXTEND,
-                     api::BITVECTOR_SIGN_EXTEND_OP,
-                     "sign_extend");
-  addIndexedOperator(kind::BITVECTOR_ROTATE_LEFT,
-                     api::BITVECTOR_ROTATE_LEFT_OP,
-                     "rotate_left");
+      kind::BITVECTOR_ZERO_EXTEND, api::BITVECTOR_ZERO_EXTEND, "zero_extend");
+  addIndexedOperator(
+      kind::BITVECTOR_SIGN_EXTEND, api::BITVECTOR_SIGN_EXTEND, "sign_extend");
+  addIndexedOperator(
+      kind::BITVECTOR_ROTATE_LEFT, api::BITVECTOR_ROTATE_LEFT, "rotate_left");
   addIndexedOperator(kind::BITVECTOR_ROTATE_RIGHT,
-                     api::BITVECTOR_ROTATE_RIGHT_OP,
+                     api::BITVECTOR_ROTATE_RIGHT,
                      "rotate_right");
-  addIndexedOperator(
-      kind::INT_TO_BITVECTOR, api::INT_TO_BITVECTOR_OP, "int2bv");
+  addIndexedOperator(kind::INT_TO_BITVECTOR, api::INT_TO_BITVECTOR, "int2bv");
 }
 
 void Smt2::addDatatypesOperators()
@@ -234,29 +229,29 @@ void Smt2::addFloatingPointOperators() {
   addOperator(kind::FLOATINGPOINT_TO_REAL, "fp.to_real");
 
   addIndexedOperator(kind::FLOATINGPOINT_TO_FP_GENERIC,
-                     api::FLOATINGPOINT_TO_FP_GENERIC_OP,
+                     api::FLOATINGPOINT_TO_FP_GENERIC,
                      "to_fp");
   addIndexedOperator(kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
-                     api::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP,
+                     api::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
                      "to_fp_unsigned");
   addIndexedOperator(
-      kind::FLOATINGPOINT_TO_UBV, api::FLOATINGPOINT_TO_UBV_OP, "fp.to_ubv");
+      kind::FLOATINGPOINT_TO_UBV, api::FLOATINGPOINT_TO_UBV, "fp.to_ubv");
   addIndexedOperator(
-      kind::FLOATINGPOINT_TO_SBV, api::FLOATINGPOINT_TO_SBV_OP, "fp.to_sbv");
+      kind::FLOATINGPOINT_TO_SBV, api::FLOATINGPOINT_TO_SBV, "fp.to_sbv");
 
   if (!strictModeEnabled())
   {
     addIndexedOperator(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
-                       api::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP,
+                       api::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
                        "to_fp_bv");
     addIndexedOperator(kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT,
-                       api::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP,
+                       api::FLOATINGPOINT_TO_FP_FLOATINGPOINT,
                        "to_fp_fp");
     addIndexedOperator(kind::FLOATINGPOINT_TO_FP_REAL,
-                       api::FLOATINGPOINT_TO_FP_REAL_OP,
+                       api::FLOATINGPOINT_TO_FP_REAL,
                        "to_fp_real");
     addIndexedOperator(kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
-                       api::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP,
+                       api::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
                        "to_fp_signed");
   }
 }
@@ -311,7 +306,7 @@ void Smt2::addTheory(Theory theory) {
     addOperator(kind::INTS_DIVISION, "div");
     addOperator(kind::INTS_MODULUS, "mod");
     addOperator(kind::ABS, "abs");
-    addIndexedOperator(kind::DIVISIBLE, api::DIVISIBLE_OP, "divisible");
+    addIndexedOperator(kind::DIVISIBLE, api::DIVISIBLE, "divisible");
     break;
 
   case THEORY_REALS:
@@ -549,8 +544,8 @@ api::Term Smt2::mkIndexedConstant(const std::string& name,
   return api::Term();
 }
 
-api::OpTerm Smt2::mkIndexedOp(const std::string& name,
-                              const std::vector<uint64_t>& numerals)
+api::Op Smt2::mkIndexedOp(const std::string& name,
+                          const std::vector<uint64_t>& numerals)
 {
   const auto& kIt = d_indexedOpKindMap.find(name);
   if (kIt != d_indexedOpKindMap.end())
@@ -558,16 +553,16 @@ api::OpTerm Smt2::mkIndexedOp(const std::string& name,
     api::Kind k = (*kIt).second;
     if (numerals.size() == 1)
     {
-      return d_solver->mkOpTerm(k, numerals[0]);
+      return d_solver->mkOp(k, numerals[0]);
     }
     else if (numerals.size() == 2)
     {
-      return d_solver->mkOpTerm(k, numerals[0], numerals[1]);
+      return d_solver->mkOp(k, numerals[0], numerals[1]);
     }
   }
 
   parseError(std::string("Unknown indexed function `") + name + "'");
-  return api::OpTerm();
+  return api::Op();
 }
 
 Expr Smt2::mkDefineFunRec(
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index ec7e2071a..215f565cd 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -75,7 +75,7 @@ class Smt2 : public Parser
   std::unordered_map<std::string, Kind> operatorKindMap;
   /**
    * Maps indexed symbols to the kind of the operator (e.g. "extract" to
-   * BITVECTOR_EXTRACT_OP).
+   * BITVECTOR_EXTRACT).
    */
   std::unordered_map<std::string, api::Kind> d_indexedOpKindMap;
   std::pair<Expr, std::string> d_lastNamedTerm;
@@ -106,7 +106,7 @@ class Smt2 : public Parser
    *              BITVECTOR_EXTRACT). NOTE: this is an internal kind for now
    *              because that is what we use to create expressions. Eventually
    *              it will be an api::Kind.
-   * @param opKind The kind of the operator term (e.g. BITVECTOR_EXTRACT_OP)
+   * @param opKind The kind of the operator term (e.g. BITVECTOR_EXTRACT)
    * @param name The name of the symbol (e.g. "extract")
    */
   void addIndexedOperator(Kind tKind,
@@ -141,8 +141,8 @@ class Smt2 : public Parser
    * @return The operator term corresponding to the indexed operator or a parse
    *         error if the name is not valid.
    */
-  api::OpTerm mkIndexedOp(const std::string& name,
-                          const std::vector<uint64_t>& numerals);
+  api::Op mkIndexedOp(const std::string& name,
+                      const std::vector<uint64_t>& numerals);
 
   /**
    * Returns the expression that name should be interpreted as.
@@ -214,7 +214,7 @@ class Smt2 : public Parser
                                              const std::vector<Expr>& guards,
                                              const std::vector<Expr>& heads,
                                              Expr body);
-                                             
+
   /**
    * Class for creating instances of `SynthFunCommand`s. Creating an instance
    * of this class pushes the scope, destroying it pops the scope.
diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp
index 4b5873e80..87c7fa2ce 100644
--- a/src/preprocessing/passes/ackermann.cpp
+++ b/src/preprocessing/passes/ackermann.cpp
@@ -35,8 +35,7 @@ namespace passes {
 
 /* -------------------------------------------------------------------------- */
 
-namespace
-{
+namespace {
 
 void addLemmaForPair(TNode args1,
                      TNode args2,
@@ -219,7 +218,6 @@ PreprocessingPassResult Ackermann::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
-
 /* -------------------------------------------------------------------------- */
 
 }  // namespace passes
diff --git a/src/preprocessing/passes/ackermann.h b/src/preprocessing/passes/ackermann.h
index 8f27cab25..410dde8b9 100644
--- a/src/preprocessing/passes/ackermann.h
+++ b/src/preprocessing/passes/ackermann.h
@@ -55,8 +55,8 @@ class Ackermann : public PreprocessingPass
    *   occurring in the input formula, add the following lemma:
    *     (x_1 = y_1 /\ ... /\ x_n = y_n) => f_X = f_Y
    */
-   PreprocessingPassResult applyInternal(
-       AssertionPipeline* assertionsToPreprocess) override;
+  PreprocessingPassResult applyInternal(
+      AssertionPipeline* assertionsToPreprocess) override;
 
  private:
   /* Map each function to a set of terms associated with it */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index eb10f580a..c47506510 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2283,9 +2283,10 @@ void SmtEngine::setDefaults() {
           << endl;
       setOption("incremental", SExpr("false"));
     }
-    if (d_logic > LogicInfo("QF_AUFBVLRA")) {
-        throw OptionException(
-            "Proofs are only supported for sub-logics of QF_AUFBVLIA."); 
+    if (d_logic > LogicInfo("QF_AUFBVLRA"))
+    {
+      throw OptionException(
+          "Proofs are only supported for sub-logics of QF_AUFBVLIA.");
     }
     if (options::bitvectorAlgebraicSolver())
     {
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 13ab03b45..a1264c612 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -746,7 +746,9 @@ RewriteResponse ArithRewriter::rewriteIntsDivModTotal(TNode t, bool pre){
                    ? nm->mkNode(kind::UMINUS, nn)
                    : nn;
     return RewriteResponse(REWRITE_AGAIN, ret);
-  }else if(dIsConstant && n.getKind() == kind::CONST_RATIONAL){
+  }
+  else if (dIsConstant && n.getKind() == kind::CONST_RATIONAL)
+  {
     Assert(d.getConst<Rational>().isIntegral());
     Assert(n.getConst<Rational>().isIntegral());
     Assert(!d.getConst<Rational>().isZero());
@@ -759,7 +761,9 @@ RewriteResponse ArithRewriter::rewriteIntsDivModTotal(TNode t, bool pre){
 
     Node resultNode = mkRationalNode(Rational(result));
     return RewriteResponse(REWRITE_DONE, resultNode);
-  }else{
+  }
+  else
+  {
     return RewriteResponse(REWRITE_DONE, t);
   }
 }
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));