From c3a9047acfbd610e923dafd4ea6102913dee5644 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 23 Mar 2022 09:13:47 -0500 Subject: [PATCH] Add internal synth result class (#8352) This is in preparation for refactoring the return values of several API methods. --- src/util/CMakeLists.txt | 2 + src/util/result.h | 4 +- src/util/synth_result.cpp | 73 +++++++++++++++++++++++++++++++++++++ src/util/synth_result.h | 77 +++++++++++++++++++++++++++++++++++++++ 4 files changed, 154 insertions(+), 2 deletions(-) create mode 100644 src/util/synth_result.cpp create mode 100644 src/util/synth_result.h diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index c8940ae94..b1319d8ea 100644 --- 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 949d10e93..8bcddb9d2 100644 --- 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 #include diff --git a/src/util/synth_result.cpp b/src/util/synth_result.cpp new file mode 100644 index 000000000..862dec3b4 --- /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 +#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 index 000000000..164028aa6 --- /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 +#include + +#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 */ -- 2.30.2