New C++ API: Implementation of Result. (#2112)

diff --git a/src/Makefile.am b/src/Makefile.am
index b60cede211076be4c492c1e959ec9970f7edece1..2ddc905e01bb8cd99bca4ae0cbaa8dcb1d22d77b 100644 (file)
--- 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 (file)
index 0000000..79c1d76
--- /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 afa1e29f95c2f6f972cf5b72e5d897e800f6e280..0b5f0ad0620925b9e423f69a3d73e4492f27c739 100644 (file)
--- 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.