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

* Treat uninterpreted functions as a child in Term iteration

* Remove unnecessary const_iterator constructor

* Add parameter comments to const_iterator constructor

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

* Switch pos member variable from int to uint32_t

* Add comment about how UFs are treated in iteration

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

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

* Remove unnecessary function checkMkOpTerm

* Update mkOpTerm comments to not use _OP Kinds

* Update examples to use new mkTerm

* First pass on fixing unit test

* Override kind for Constructor and Selector Terms

* More fixes to unit tests

* Updates to parser

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

* Remove *_OP kinds from public API

* Add hasOpTerm and getOpTerm methods to Term

* Add test for UF iteration

* Add unit test for getOpTerm

* Move OpTerm implementation above Term implemenation to match header file

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

* Fix mkTerm in datatypes-new.cpp example

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

* Rename: OpTerm->Op in API

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

* Add case for APPLY_TESTER

* operator term -> operator

* Update src/api/cvc4cpp.h

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

* Comment comment suggestion

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

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

* Undo sed mistake for OpTerm replacement

* Add 'd_' prefix to member vars

* Fix comment and remove old commented-out code

* Formatting

* Revert "Formatting"

This reverts commit d1d5fc1fb71496daeba668e97cad84c213200ba9.

* More fixes for sed mistakes

* Minor formatting

* Undo changes in CVC parser

* Add isIndexed and prefix with d_

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

3 files changed, 15 insertions, 19 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;