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, 210 insertions, 176 deletions

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