diff options
Diffstat (limited to 'src/api')
-rw-r--r-- | src/api/cvc4cpp.cpp | 9 | ||||
-rw-r--r-- | src/api/cvc4cpp.h | 61 |
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 */ |