Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Andrew Reynolds, Aina Niemetz, Andres Noetzli
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2025 by the authors listed in the file AUTHORS
       8                 :            :  * in the top-level source directory and their institutional affiliations.
       9                 :            :  * All rights reserved.  See the file COPYING in the top-level source
      10                 :            :  * directory for licensing information.
      11                 :            :  * ****************************************************************************
      12                 :            :  *
      13                 :            :  * Encapsulation of the result of a synthesis query.
      14                 :            :  */
      15                 :            : #include "util/synth_result.h"
      16                 :            : 
      17                 :            : #include <sstream>
      18                 :            : #include "base/check.h"
      19                 :            : 
      20                 :            : using namespace std;
      21                 :            : 
      22                 :            : namespace cvc5::internal {
      23                 :            : 
      24                 :       2131 : SynthResult::SynthResult()
      25                 :       2131 :     : d_status(NONE), d_unknownExplanation(UnknownExplanation::UNKNOWN_REASON)
      26                 :            : {
      27                 :       2131 : }
      28                 :            : 
      29                 :       1181 : SynthResult::SynthResult(Status s, UnknownExplanation unknownExplanation)
      30                 :       1181 :     : d_status(s), d_unknownExplanation(unknownExplanation)
      31                 :            : {
      32                 :       1181 : }
      33                 :            : 
      34                 :       3425 : SynthResult::Status SynthResult::getStatus() const { return d_status; }
      35                 :            : 
      36                 :          0 : UnknownExplanation SynthResult::getUnknownExplanation() const
      37                 :            : {
      38                 :          0 :   return d_unknownExplanation;
      39                 :            : }
      40                 :            : 
      41                 :         45 : bool SynthResult::operator==(const SynthResult& r) const
      42                 :            : {
      43                 :         45 :   return d_status == r.d_status
      44 [ +  + ][ -  + ]:         45 :          && (d_status != UNKNOWN
      45         [ -  - ]:         45 :              || d_unknownExplanation == r.d_unknownExplanation);
      46                 :            : }
      47                 :            : 
      48                 :         11 : bool SynthResult::operator!=(const SynthResult& r) const
      49                 :            : {
      50                 :         11 :   return !(*this == r);
      51                 :            : }
      52                 :            : 
      53                 :        397 : std::string SynthResult::toString() const
      54                 :            : {
      55                 :        794 :   std::stringstream ss;
      56                 :        397 :   ss << "(" << d_status;
      57         [ -  + ]:        397 :   if (d_unknownExplanation != UnknownExplanation::UNKNOWN_REASON)
      58                 :            :   {
      59                 :          0 :     ss << " :unknown-explanation " << d_unknownExplanation;
      60                 :            :   }
      61                 :        397 :   ss << ")";
      62                 :        794 :   return ss.str();
      63                 :            : }
      64                 :            : 
      65                 :          0 : std::ostream& operator<<(std::ostream& out, const SynthResult& r)
      66                 :            : {
      67                 :          0 :   out << r.toString();
      68                 :          0 :   return out;
      69                 :            : }
      70                 :            : 
      71                 :        397 : ostream& operator<<(ostream& out, SynthResult::Status s)
      72                 :            : {
      73 [ +  + ][ +  - ]:        397 :   switch (s)
                    [ - ]
      74                 :            :   {
      75                 :          1 :     case SynthResult::NONE: out << "NONE"; break;
      76                 :        296 :     case SynthResult::SOLUTION: out << "SOLUTION"; break;
      77                 :        100 :     case SynthResult::NO_SOLUTION: out << "NO_SOLUTION"; break;
      78                 :          0 :     case SynthResult::UNKNOWN: out << "UNKNOWN"; break;
      79                 :          0 :     default: Unhandled() << s;
      80                 :            :   }
      81                 :        397 :   return out;
      82                 :            : }
      83                 :            : 
      84                 :            : }  // namespace cvc5::internal