New C++ API: Clean up usage of internal types in Op. (#6045)

This disables the temporarily available internals of Op.

2 files changed, 26 insertions, 44 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index c3490938b..410198920 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -1577,15 +1577,6 @@ std::string Op::toString() const
   }
 }
 
-// !!! This is only temporarily available until the parser is fully migrated
-// to the new API. !!!
-CVC4::Expr Op::getExpr(void) const
-{
-  if (d_node->isNull()) return Expr();
-  NodeManagerScope scope(d_solver->getNodeManager());
-  return d_node->toExpr();
-}
-
 std::ostream& operator<<(std::ostream& out, const Op& t)
 {
   out << t.toString();
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index d503a317e..e52fe2524 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -719,6 +719,7 @@ struct CVC4_PUBLIC SortHashFunction
 class CVC4_PUBLIC Op
 {
   friend class Solver;
+  friend class Term;
   friend struct OpHashFunction;
 
  public:
@@ -727,37 +728,6 @@ class CVC4_PUBLIC Op
    */
   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 slv the associated solver object
-   * @param k the kind of this Op
-   */
-  Op(const Solver* slv, const Kind k);
-
-  // !!! This constructor is only temporarily public until the parser is fully
-  // migrated to the new API. !!!
-  /**
-   * Constructor.
-   * @param slv the associated solver object
-   * @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 Solver* slv, const Kind k, const CVC4::Expr& e);
-
-  // !!! This constructor is only temporarily public until the parser is fully
-  // migrated to the new API. !!!
-  /**
-   * Constructor.
-   * @param slv the associated solver object
-   * @param k the kind of this Op
-   * @param n the internal node that is to be wrapped by this term
-   * @return the Term
-   */
-  Op(const Solver* slv, const Kind k, const CVC4::Node& n);
-
   /**
    * Destructor.
    */
@@ -814,12 +784,33 @@ class CVC4_PUBLIC Op
    */
   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:
   /**
+   * Constructor for a single kind (non-indexed operator).
+   * @param slv the associated solver object
+   * @param k the kind of this Op
+   */
+  Op(const Solver* slv, const Kind k);
+
+  /**
+   * Constructor.
+   * @param slv the associated solver object
+   * @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 Solver* slv, const Kind k, const CVC4::Expr& e);
+
+  /**
+   * Constructor.
+   * @param slv the associated solver object
+   * @param k the kind of this Op
+   * @param n the internal node that is to be wrapped by this term
+   * @return the Term
+   */
+  Op(const Solver* slv, const Kind k, const CVC4::Node& n);
+
+  /**
    * Helper for isNull checks. This prevents calling an API function with
    * CVC4_API_CHECK_NOT_NULL
    */