From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Wed, 4 Jul 2018 08:31:02 +0000 (-0700)
Subject: New C++ API: Implementation of OpTerm. (#2132)
X-Git-Tag: cvc5-1.0.0~4918
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9eb2c735f8c34d4980b37e337e711a629f997834;p=cvc5.git

New C++ API: Implementation of OpTerm. (#2132)
---

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 80af4199b..703c298d3 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -1023,5 +1023,74 @@ size_t TermHashFunction::operator()(const Term& t) const
   return ExprHashFunction()(*t.d_expr);
 }
 
+/* -------------------------------------------------------------------------- */
+/* OpTerm                                                                     */
+/* -------------------------------------------------------------------------- */
+
+OpTerm::OpTerm() : d_expr(new CVC4::Expr())
+{
+}
+
+OpTerm::OpTerm(const CVC4::Expr& e) : d_expr(new CVC4::Expr(e))
+{
+}
+
+OpTerm::~OpTerm()
+{
+}
+
+OpTerm& OpTerm::operator=(const OpTerm& t)
+{
+  // CHECK: expr managers must match
+  if (this != &t)
+  {
+    *d_expr = *t.d_expr;
+  }
+  return *this;
+}
+
+bool OpTerm::operator==(const OpTerm& t) const
+{
+  // CHECK: expr managers must match
+  return *d_expr == *t.d_expr;
+}
+
+bool OpTerm::operator!=(const OpTerm& t) const
+{
+  // CHECK: expr managers must match
+  return *d_expr != *t.d_expr;
+}
+
+Kind OpTerm::getKind() const
+{
+  return intToExtKind(d_expr->getKind());
+}
+
+Sort OpTerm::getSort() const
+{
+  return Sort(d_expr->getType());
+}
+
+bool OpTerm::isNull() const
+{
+  return d_expr->isNull();
+}
+
+std::string OpTerm::toString() const
+{
+  return d_expr->toString();
+}
+
+std::ostream& operator<< (std::ostream& out, const OpTerm& t)
+{
+  out << t.toString();
+  return out;
+}
+
+size_t OpTermHashFunction::operator()(const OpTerm& t) const
+{
+  return ExprHashFunction()(*t.d_expr);
+}
+
 }  // namespace api
 }  // namespace CVC4