From 45a5d525d26dba9ed3f12d888c8b9fb844c8a8ec Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Tue, 3 Jul 2018 09:27:59 -0700
Subject: [PATCH] New C++ API: Implementation of Term. (#2131)

---
 src/api/cvc4cpp.cpp | 224 ++++++++++++++++++++++++++++++++++++++++++++
 src/util/utility.h  |   1 +
 2 files changed, 225 insertions(+)

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 968102f5d..80af4199b 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -16,9 +16,13 @@
 
 #include "api/cvc4cpp.h"
 
+#include "base/cvc4_assert.h"
+#include "expr/expr.h"
+#include "expr/expr_manager.h"
 #include "expr/kind.h"
 #include "expr/type.h"
 #include "util/result.h"
+#include "util/utility.h"
 
 #include <sstream>
 
@@ -92,6 +96,7 @@ std::ostream& operator<<(std::ostream& out, const Result& r)
   return out;
 }
 
+
 /* -------------------------------------------------------------------------- */
 /* Kind                                                                       */
 /* -------------------------------------------------------------------------- */
@@ -623,6 +628,7 @@ std::ostream& operator<<(std::ostream& out, Kind k)
 
 size_t KindHashFunction::operator()(Kind k) const { return k; }
 
+
 /* -------------------------------------------------------------------------- */
 /* Sort                                                                       */
 /* -------------------------------------------------------------------------- */
@@ -799,5 +805,223 @@ size_t SortHashFunction::operator()(const Sort& s) const {
   return TypeHashFunction()(*s.d_type);
 }
 
+
+/* -------------------------------------------------------------------------- */
+/* Term                                                                       */
+/* -------------------------------------------------------------------------- */
+
+Term::Term() : d_expr(new CVC4::Expr())
+{
+}
+
+Term::Term(const CVC4::Expr& e) : d_expr(new CVC4::Expr(e))
+{
+}
+
+Term::~Term()
+{
+}
+
+Term& Term::operator=(const Term& t)
+{
+  // CHECK: expr managers must match
+  if (this != &t)
+  {
+    *d_expr = *t.d_expr;
+  }
+  return *this;
+}
+
+bool Term::operator==(const Term& t) const
+{
+  // CHECK: expr managers must match
+  return *d_expr == *t.d_expr;
+}
+
+bool Term::operator!=(const Term& t) const
+{
+  // CHECK: expr managers must match
+  return *d_expr != *t.d_expr;
+}
+
+Kind Term::getKind() const
+{
+  return intToExtKind(d_expr->getKind());
+}
+
+Sort Term::getSort() const
+{
+  return Sort(d_expr->getType());
+}
+
+bool Term::isNull() const
+{
+  return d_expr->isNull();
+}
+
+Term Term::notTerm() const
+{
+  return d_expr->notExpr();
+}
+
+Term Term::andTerm(const Term& t) const
+{
+  return d_expr->andExpr(*t.d_expr);
+}
+
+Term Term::orTerm(const Term& t) const
+{
+  return d_expr->orExpr(*t.d_expr);
+}
+
+Term Term::xorTerm(const Term& t) const
+{
+  return d_expr->xorExpr(*t.d_expr);
+}
+
+Term Term::iffTerm(const Term& t) const
+{
+  return d_expr->iffExpr(*t.d_expr);
+}
+
+Term Term::impTerm(const Term& t) const
+{
+  return d_expr->impExpr(*t.d_expr);
+}
+
+Term Term::iteTerm(const Term& then_t, const Term& else_t) const
+{
+  return d_expr->iteExpr(*then_t.d_expr, *else_t.d_expr);
+}
+
+std::string Term::toString() const
+{
+  return d_expr->toString();
+}
+
+Term::const_iterator::const_iterator() : d_iterator(nullptr)
+{
+}
+
+Term::const_iterator::const_iterator(void* it) : d_iterator(it)
+{
+}
+
+Term::const_iterator::const_iterator(const const_iterator& it)
+    : d_iterator(nullptr)
+{
+  if (it.d_iterator != nullptr)
+  {
+    d_iterator = new CVC4::Expr::const_iterator(
+        *static_cast<CVC4::Expr::const_iterator*>(it.d_iterator));
+  }
+}
+
+Term::const_iterator& Term::const_iterator::operator=(const const_iterator& it)
+{
+  delete static_cast<CVC4::Expr::const_iterator*>(d_iterator);
+  d_iterator = new CVC4::Expr::const_iterator(
+      *static_cast<CVC4::Expr::const_iterator*>(it.d_iterator));
+  return *this;
+}
+
+Term::const_iterator::~const_iterator()
+{
+  delete static_cast<CVC4::Expr::const_iterator*>(d_iterator);
+}
+
+bool Term::const_iterator::operator==(const const_iterator& it) const
+{
+  if (d_iterator == nullptr || it.d_iterator == nullptr)
+  {
+    return false;
+  }
+  return *static_cast<CVC4::Expr::const_iterator*>(d_iterator)
+         == *static_cast<CVC4::Expr::const_iterator*>(it.d_iterator);
+}
+
+bool Term::const_iterator::operator!=(const const_iterator& it) const
+{
+  return !(*this == it);
+}
+
+Term::const_iterator& Term::const_iterator::operator++()
+{
+  Assert(d_iterator != nullptr);
+  ++*static_cast<CVC4::Expr::const_iterator*>(d_iterator);
+  return *this;
+}
+
+Term::const_iterator Term::const_iterator::operator++(int)
+{
+  Assert(d_iterator != nullptr);
+  const_iterator it = *this;
+  ++*static_cast<CVC4::Expr::const_iterator*>(d_iterator);
+  return it;
+}
+
+Term Term::const_iterator::operator*() const
+{
+  Assert(d_iterator != nullptr);
+  return Term(**static_cast<CVC4::Expr::const_iterator*>(d_iterator));
+}
+
+Term::const_iterator Term::begin() const
+{
+  return Term::const_iterator(new CVC4::Expr::const_iterator(d_expr->begin()));
+}
+
+Term::const_iterator Term::end() const
+{
+  return Term::const_iterator(new CVC4::Expr::const_iterator(d_expr->end()));
+}
+
+std::ostream& operator<< (std::ostream& out, const Term& t)
+{
+  out << t.toString();
+  return out;
+}
+
+std::ostream& operator<<(std::ostream& out, const std::vector<Term>& vector)
+{
+  container_to_stream(out, vector);
+  return out;
+}
+
+std::ostream& operator<<(std::ostream& out, const std::set<Term>& set)
+{
+  container_to_stream(out, set);
+  return out;
+}
+
+std::ostream& operator<<(
+    std::ostream& out,
+    const std::unordered_set<Term, TermHashFunction>& unordered_set)
+{
+  container_to_stream(out, unordered_set);
+  return out;
+}
+
+template <typename V>
+std::ostream& operator<<(std::ostream& out, const std::map<Term, V>& map)
+{
+  container_to_stream(out, map);
+  return out;
+}
+
+template <typename V>
+std::ostream& operator<<(
+    std::ostream& out,
+    const std::unordered_map<Term, V, TermHashFunction>& unordered_map)
+{
+  container_to_stream(out, unordered_map);
+  return out;
+}
+
+size_t TermHashFunction::operator()(const Term& t) const
+{
+  return ExprHashFunction()(*t.d_expr);
+}
+
 }  // namespace api
 }  // namespace CVC4
diff --git a/src/util/utility.h b/src/util/utility.h
index bfe8e66c9..a9a9a29c3 100644
--- a/src/util/utility.h
+++ b/src/util/utility.h
@@ -19,6 +19,7 @@
 #ifndef __CVC4__UTILITY_H
 #define __CVC4__UTILITY_H
 
+#include <algorithm>
 #include <utility>
 #include <functional>
 
-- 
2.30.2