From 021e7ebaf808f4496609685cccab4eae8eb04d38 Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Thu, 28 Jun 2018 17:54:33 -0700
Subject: [PATCH] New C++ API: Implementation of Result. (#2112)

---
 src/Makefile.am       |  3 ++
 src/api/cvc4cpp.cpp   | 94 +++++++++++++++++++++++++++++++++++++++++++
 src/api/cvc4cppkind.h |  5 ++-
 3 files changed, 100 insertions(+), 2 deletions(-)
 create mode 100644 src/api/cvc4cpp.cpp

diff --git a/src/Makefile.am b/src/Makefile.am
index b60cede21..2ddc905e0 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -35,6 +35,9 @@ nodist_EXTRA_libcvc4_la_SOURCES = dummy.cpp
 libcvc4_la_SOURCES = \
 	git_versioninfo.cpp \
 	svn_versioninfo.cpp \
+	api/cvc4cpp.h \
+	api/cvc4cppkind.h \
+	api/cvc4cpp.cpp \
 	context/backtrackable.h \
 	context/cddense_set.h \
 	context/cdhashmap.h \
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
new file mode 100644
index 000000000..79c1d7629
--- /dev/null
+++ b/src/api/cvc4cpp.cpp
@@ -0,0 +1,94 @@
+/*********************                                                        */
+/*! \file cvc4cpp.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The CVC4 C++ API.
+ **
+ ** The CVC4 C++ API.
+ **/
+
+#include "api/cvc4cpp.h"
+
+#include "util/result.h"
+
+#include <sstream>
+
+namespace CVC4 {
+namespace api {
+
+/* -------------------------------------------------------------------------- */
+/* Result                                                                     */
+/* -------------------------------------------------------------------------- */
+
+Result::Result(const CVC4::Result& r) : d_result(new CVC4::Result(r)) {}
+
+bool Result::isSat(void) const
+{
+  return d_result->getType() == CVC4::Result::TYPE_SAT
+         && d_result->isSat() == CVC4::Result::SAT;
+}
+
+bool Result::isUnsat(void) const
+{
+  return d_result->getType() == CVC4::Result::TYPE_SAT
+         && d_result->isSat() == CVC4::Result::UNSAT;
+}
+
+bool Result::isSatUnknown(void) const
+{
+  return d_result->getType() == CVC4::Result::TYPE_SAT
+         && d_result->isSat() == CVC4::Result::SAT_UNKNOWN;
+}
+
+bool Result::isValid(void) const
+{
+  return d_result->getType() == CVC4::Result::TYPE_VALIDITY
+         && d_result->isValid() == CVC4::Result::VALID;
+}
+
+bool Result::isInvalid(void) const
+{
+  return d_result->getType() == CVC4::Result::TYPE_VALIDITY
+         && d_result->isValid() == CVC4::Result::INVALID;
+}
+
+bool Result::isValidUnknown(void) const
+{
+  return d_result->getType() == CVC4::Result::TYPE_VALIDITY
+         && d_result->isValid() == CVC4::Result::VALIDITY_UNKNOWN;
+}
+
+bool Result::operator==(const Result& r) const
+{
+  return *d_result == *r.d_result;
+}
+
+bool Result::operator!=(const Result& r) const
+{
+  return *d_result != *r.d_result;
+}
+
+std::string Result::getUnknownExplanation(void) const
+{
+  std::stringstream ss;
+  ss << d_result->whyUnknown();
+  return ss.str();
+}
+
+std::string Result::toString(void) const { return d_result->toString(); }
+
+std::ostream& operator<<(std::ostream& out, const Result& r)
+{
+  out << r.toString();
+  return out;
+}
+
+}  // namespace api
+}  // namespace CVC4
diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h
index afa1e29f9..0b5f0ad06 100644
--- a/src/api/cvc4cppkind.h
+++ b/src/api/cvc4cppkind.h
@@ -1,7 +1,8 @@
 /*********************                                                        */
-/*! \file cvc4cpp.h
+/*! \file cvc4cppkind.h
  ** \verbatim
- ** Top authors (to current version): Aina Niemetz
+ ** Top contributors (to current version):
+ **   Aina Niemetz
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
-- 
2.30.2