Add internal synth result class (#8352)

This is in preparation for refactoring the return values of several API methods.

diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index c8940ae944c7162b8430023c25c6e3f52cdac86b..b1319d8eac2694df9d6e018390f98e4b6c56d706 100644 (file)
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -76,6 +76,8 @@ libcvc5_add_sources(
   statistics_value.h
   string.cpp
   string.h
+  synth_result.cpp
+  synth_result.h
   uninterpreted_sort_value.cpp
   uninterpreted_sort_value.h
   utility.cpp

diff --git a/src/util/result.h b/src/util/result.h
index 949d10e93a46897646baf6e819b1f4d49eeb09a4..8bcddb9d2336fb611dd752fa285116e03b4aa4a9 100644 (file)
--- a/src/util/result.h
+++ b/src/util/result.h
@@ -15,8 +15,8 @@
 
 #include "cvc5_public.h"
 
-#ifndef CVC5__RESULT_H
-#define CVC5__RESULT_H
+#ifndef CVC5__UTIL__RESULT_H
+#define CVC5__UTIL__RESULT_H
 
 #include <iosfwd>
 #include <string>

diff --git a/src/util/synth_result.cpp b/src/util/synth_result.cpp
new file mode 100644 (file)
index 0000000..862dec3
--- /dev/null
+++ b/src/util/synth_result.cpp
@@ -0,0 +1,73 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Encapsulation of the result of a synthesis query.
+ */
+#include "util/synth_result.h"
+
+#include <sstream>
+#include "base/check.h"
+
+using namespace std;
+
+namespace cvc5 {
+
+SynthResult::SynthResult()
+    : d_status(NONE), d_unknownExplanation(Result::UNKNOWN_REASON)
+{
+}
+
+SynthResult::SynthResult(Status s,
+                         Result::UnknownExplanation unknownExplanation)
+    : d_status(s), d_unknownExplanation(unknownExplanation)
+{
+}
+
+SynthResult::Status SynthResult::getStatus() const { return d_status; }
+
+Result::UnknownExplanation SynthResult::getUnknownExplanation() const
+{
+  return d_unknownExplanation;
+}
+
+std::string SynthResult::toString() const
+{
+  std::stringstream ss;
+  ss << "(" << d_status;
+  if (d_unknownExplanation != Result::UNKNOWN_REASON)
+  {
+    ss << " :unknown-explanation " << d_unknownExplanation;
+  }
+  ss << ")";
+  return ss.str();
+}
+
+std::ostream& operator<<(std::ostream& out, const SynthResult& r)
+{
+  out << r.toString();
+  return out;
+}
+
+ostream& operator<<(ostream& out, SynthResult::Status s)
+{
+  switch (s)
+  {
+    case SynthResult::NONE: out << "NONE"; break;
+    case SynthResult::SOLUTION: out << "SOLUTION"; break;
+    case SynthResult::NO_SOLUTION: out << "NO_SOLUTION"; break;
+    case SynthResult::UNKNOWN: out << "UNKNOWN"; break;
+    default: Unhandled() << s;
+  }
+  return out;
+}
+
+}  // namespace cvc5

diff --git a/src/util/synth_result.h b/src/util/synth_result.h
new file mode 100644 (file)
index 0000000..164028a
--- /dev/null
+++ b/src/util/synth_result.h
@@ -0,0 +1,77 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Encapsulation of the result of a synthesis query.
+ */
+
+#include "cvc5_public.h"
+
+#ifndef CVC5__EXPR__SYNTH_RESULT_H
+#define CVC5__EXPR__SYNTH_RESULT_H
+
+#include <iosfwd>
+#include <string>
+
+#include "util/result.h"
+
+namespace cvc5 {
+
+/**
+ * A result for a synthesis query. This can be used for synthesis, abduction,
+ * interpolation, and quantifier elimination.
+ */
+class SynthResult
+{
+ public:
+  enum Status
+  {
+    // the status has not been set
+    NONE,
+    // the synthesis query was successful, i.e. there is a solution
+    SOLUTION,
+    // the synthesis query resulted in failure, i.e. there is no solution
+    NO_SOLUTION,
+    // the synthesis query is unknown, i.e. it is not known whether there is a
+    // solution.
+    UNKNOWN
+  };
+
+ public:
+  /** Default constructor */
+  SynthResult();
+  /** Constructor when the solution is not successful */
+  SynthResult(
+      Status s,
+      Result::UnknownExplanation unknownExplanation = Result::UNKNOWN_REASON);
+
+  /** Get the status */
+  Status getStatus() const;
+
+  /** Get the unknown explanation */
+  Result::UnknownExplanation getUnknownExplanation() const;
+
+  /** Get the string representation */
+  std::string toString() const;
+
+ private:
+  /** The status */
+  Status d_status;
+  /** The unknown explanation */
+  Result::UnknownExplanation d_unknownExplanation;
+};
+
+std::ostream& operator<<(std::ostream& out, const SynthResult& r);
+std::ostream& operator<<(std::ostream& out, SynthResult::Status s);
+
+}  // namespace cvc5
+
+#endif /* CVC5__RESULT_H */