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

1 files changed, 5 insertions, 5 deletions

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.