Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * This file is part of the cvc5 project.
       3                 :            :  *
       4                 :            :  * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
       5                 :            :  * in the top-level source directory and their institutional affiliations.
       6                 :            :  * All rights reserved.  See the file COPYING in the top-level source
       7                 :            :  * directory for licensing information.
       8                 :            :  * ****************************************************************************
       9                 :            :  *
      10                 :            :  * Encapsulation of the result of a query.
      11                 :            :  */
      12                 :            : #include "util/result.h"
      13                 :            : 
      14                 :            : #include <algorithm>
      15                 :            : #include <cctype>
      16                 :            : #include <iostream>
      17                 :            : #include <sstream>
      18                 :            : #include <string>
      19                 :            : 
      20                 :            : #include "base/check.h"
      21                 :            : #include "options/io_utils.h"
      22                 :            : 
      23                 :            : using namespace std;
      24                 :            : 
      25                 :            : namespace cvc5::internal {
      26                 :            : 
      27                 :     908552 : Result::Result()
      28                 :     908552 :     : d_status(NONE),
      29                 :     908552 :       d_unknownExplanation(UnknownExplanation::UNKNOWN_REASON),
      30                 :     908552 :       d_inputName("")
      31                 :            : {
      32                 :     908552 : }
      33                 :            : 
      34                 :      53018 : Result::Result(Status s, std::string inputName)
      35                 :      53018 :     : d_status(s),
      36                 :      53018 :       d_unknownExplanation(UnknownExplanation::UNKNOWN_REASON),
      37                 :      53018 :       d_inputName(inputName)
      38                 :            : {
      39 [ -  + ][ -  + ]:      53018 :   Assert(s != UNKNOWN)
                 [ -  - ]
      40                 :          0 :       << "Must provide a reason for satisfiability being unknown";
      41                 :      53018 : }
      42                 :            : 
      43                 :      10873 : Result::Result(Status s,
      44                 :            :                UnknownExplanation unknownExplanation,
      45                 :      10873 :                std::string inputName)
      46                 :      10873 :     : d_status(s),
      47                 :      10873 :       d_unknownExplanation(unknownExplanation),
      48                 :      10873 :       d_inputName(inputName)
      49                 :            : {
      50 [ -  + ][ -  + ]:      10873 :   Assert(s == UNKNOWN) << "improper use of unknown-result constructor";
                 [ -  - ]
      51                 :      10873 : }
      52                 :            : 
      53                 :       8072 : Result::Result(const std::string& instr, std::string inputName)
      54                 :       8072 :     : d_status(NONE),
      55                 :       8072 :       d_unknownExplanation(UnknownExplanation::UNKNOWN_REASON),
      56                 :       8072 :       d_inputName(inputName)
      57                 :            : {
      58                 :       8072 :   std::string s = instr;
      59                 :       8072 :   transform(s.begin(), s.end(), s.begin(), ::tolower);
      60 [ +  + ][ -  + ]:       8072 :   if (s == "sat" || s == "satisfiable")
                 [ +  + ]
      61                 :            :   {
      62                 :       2128 :     d_status = SAT;
      63                 :            :   }
      64 [ +  + ][ -  + ]:       5944 :   else if (s == "unsat" || s == "unsatisfiable")
                 [ +  + ]
      65                 :            :   {
      66                 :       5875 :     d_status = UNSAT;
      67                 :            :   }
      68         [ -  + ]:         69 :   else if (s == "incomplete")
      69                 :            :   {
      70                 :          0 :     d_status = UNKNOWN;
      71                 :          0 :     d_unknownExplanation = UnknownExplanation::INCOMPLETE;
      72                 :            :   }
      73         [ -  + ]:         69 :   else if (s == "timeout")
      74                 :            :   {
      75                 :          0 :     d_status = UNKNOWN;
      76                 :          0 :     d_unknownExplanation = UnknownExplanation::TIMEOUT;
      77                 :            :   }
      78         [ -  + ]:         69 :   else if (s == "resourceout")
      79                 :            :   {
      80                 :          0 :     d_status = UNKNOWN;
      81                 :          0 :     d_unknownExplanation = UnknownExplanation::RESOURCEOUT;
      82                 :            :   }
      83         [ -  + ]:         69 :   else if (s == "memout")
      84                 :            :   {
      85                 :          0 :     d_status = UNKNOWN;
      86                 :          0 :     d_unknownExplanation = UnknownExplanation::MEMOUT;
      87                 :            :   }
      88         [ -  + ]:         69 :   else if (s == "interrupted")
      89                 :            :   {
      90                 :          0 :     d_status = UNKNOWN;
      91                 :          0 :     d_unknownExplanation = UnknownExplanation::INTERRUPTED;
      92                 :            :   }
      93 [ +  - ][ +  - ]:         69 :   else if (s.size() >= 7 && s.compare(0, 7, "unknown") == 0)
                 [ +  - ]
      94                 :            :   {
      95                 :         69 :     d_status = UNKNOWN;
      96                 :            :   }
      97                 :            :   else
      98                 :            :   {
      99                 :          0 :     IllegalArgument(s,
     100                 :            :                     "expected satisfiability/entailment result, "
     101                 :            :                     "instead got `%s'",
     102                 :            :                     s.c_str());
     103                 :            :   }
     104                 :       8072 : }
     105                 :            : 
     106                 :        978 : UnknownExplanation Result::getUnknownExplanation() const
     107                 :            : {
     108 [ -  + ][ -  + ]:        978 :   Assert(isUnknown()) << "This result is not unknown, so the reason for "
                 [ -  - ]
     109                 :          0 :                          "being unknown cannot be inquired of it";
     110                 :        978 :   return d_unknownExplanation;
     111                 :            : }
     112                 :            : 
     113                 :      17420 : bool Result::operator==(const Result& r) const
     114                 :            : {
     115                 :      17420 :   return d_status == r.d_status
     116 [ +  + ][ -  + ]:      17420 :          && (d_status != UNKNOWN
     117         [ -  - ]:      17420 :              || d_unknownExplanation == r.d_unknownExplanation);
     118                 :            : }
     119                 :            : 
     120                 :      16369 : bool Result::operator!=(const Result& r) const { return !(*this == r); }
     121                 :            : 
     122                 :      20525 : string Result::toString() const
     123                 :            : {
     124                 :      20525 :   stringstream ss;
     125                 :      20525 :   ss << *this;
     126                 :      41050 :   return ss.str();
     127                 :      20525 : }
     128                 :            : 
     129                 :          0 : ostream& operator<<(ostream& out, enum Result::Status s)
     130                 :            : {
     131 [ -  - ][ -  - ]:          0 :   switch (s)
                    [ - ]
     132                 :            :   {
     133                 :          0 :     case Result::NONE: out << "NONE"; break;
     134                 :          0 :     case Result::UNSAT: out << "UNSAT"; break;
     135                 :          0 :     case Result::SAT: out << "SAT"; break;
     136                 :          0 :     case Result::UNKNOWN: out << "UNKNOWN"; break;
     137                 :          0 :     default: Unhandled() << s;
     138                 :            :   }
     139                 :          0 :   return out;
     140                 :            : }
     141                 :            : 
     142                 :      22789 : ostream& operator<<(ostream& out, const Result& r)
     143                 :            : {
     144                 :      22789 :   Language language = options::ioutils::getOutputLanguage(out);
     145         [ +  + ]:      22789 :   switch (language)
     146                 :            :   {
     147                 :          1 :     case Language::LANG_SYGUS_V2: r.toStreamSmt2(out); break;
     148                 :      22788 :     default:
     149         [ +  + ]:      22788 :       if (language::isLangSmt2(language))
     150                 :            :       {
     151                 :      22756 :         r.toStreamSmt2(out);
     152                 :            :       }
     153                 :            :       else
     154                 :            :       {
     155                 :         32 :         r.toStreamDefault(out);
     156                 :            :       }
     157                 :            :   };
     158                 :      22789 :   return out;
     159                 :            : }
     160                 :            : 
     161                 :      22669 : void Result::toStreamDefault(std::ostream& out) const
     162                 :            : {
     163 [ +  + ][ +  + ]:      22669 :   switch (d_status)
                    [ - ]
     164                 :            :   {
     165                 :          2 :     case Result::NONE: out << "none"; break;
     166                 :      14746 :     case Result::UNSAT: out << "unsat"; break;
     167                 :       7920 :     case Result::SAT: out << "sat"; break;
     168                 :          1 :     case Result::UNKNOWN:
     169                 :          1 :       out << "unknown";
     170         [ +  - ]:          1 :       if (getUnknownExplanation() != UnknownExplanation::UNKNOWN_REASON)
     171                 :            :       {
     172                 :          1 :         out << " (" << getUnknownExplanation() << ")";
     173                 :            :       }
     174                 :          1 :       break;
     175                 :          0 :     default: out << "???"; break;
     176                 :            :   }
     177                 :      22669 : }
     178                 :            : 
     179                 :      22757 : void Result::toStreamSmt2(ostream& out) const
     180                 :            : {
     181         [ +  + ]:      22757 :   if (d_status == Result::UNKNOWN)
     182                 :            :   {
     183                 :            :     // to avoid printing the reason
     184                 :        120 :     out << "unknown";
     185                 :        120 :     return;
     186                 :            :   }
     187                 :      22637 :   toStreamDefault(out);
     188                 :            : }
     189                 :            : 
     190                 :            : }  // namespace cvc5::internal