1 /********************* */ 2 /*! \file result.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Morgan Deters, Tim King 6 ** This file is part of the CVC4 project. 7 ** Copyright (c) 2009-2019 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.\endverbatim 11 ** 12 ** \brief Encapsulation of the result of a query. 13 ** 14 ** Encapsulation of the result of a query. 15 **/ 16 17 #include "cvc4_public.h" 18 19 #ifndef __CVC4__RESULT_H 20 #define __CVC4__RESULT_H 21 22 #include <iostream> 23 #include <string> 24 25 #include "base/exception.h" 26 #include "options/language.h" 27 28 namespace CVC4 { 29 30 class Result; 31 32 std::ostream& operator<<(std::ostream& out, const Result& r) CVC4_PUBLIC; 33 34 /** 35 * Three-valued SMT result, with optional explanation. 36 */ 37 class CVC4_PUBLIC Result { 38 public: 39 enum Sat { UNSAT = 0, SAT = 1, SAT_UNKNOWN = 2 }; 40 41 enum Validity { INVALID = 0, VALID = 1, VALIDITY_UNKNOWN = 2 }; 42 43 enum Type { TYPE_SAT, TYPE_VALIDITY, TYPE_NONE }; 44 45 enum UnknownExplanation { 46 REQUIRES_FULL_CHECK, 47 INCOMPLETE, 48 TIMEOUT, 49 RESOURCEOUT, 50 MEMOUT, 51 INTERRUPTED, 52 NO_STATUS, 53 UNSUPPORTED, 54 OTHER, 55 UNKNOWN_REASON 56 }; 57 58 private: 59 enum Sat d_sat; 60 enum Validity d_validity; 61 enum Type d_which; 62 enum UnknownExplanation d_unknownExplanation; 63 std::string d_inputName; 64 65 public: 66 Result(); 67 68 Result(enum Sat s, std::string inputName = ""); 69 70 Result(enum Validity v, std::string inputName = ""); 71 72 Result(enum Sat s, enum UnknownExplanation unknownExplanation, 73 std::string inputName = ""); 74 75 Result(enum Validity v, enum UnknownExplanation unknownExplanation, 76 std::string inputName = ""); 77 78 Result(const std::string& s, std::string inputName = ""); 79 Result(const Result & r,std::string inputName)80 Result(const Result& r, std::string inputName) { 81 *this = r; 82 d_inputName = inputName; 83 } 84 isSat()85 enum Sat isSat() const { return d_which == TYPE_SAT ? d_sat : SAT_UNKNOWN; } 86 isValid()87 enum Validity isValid() const { 88 return d_which == TYPE_VALIDITY ? d_validity : VALIDITY_UNKNOWN; 89 } 90 isUnknown()91 bool isUnknown() const { 92 return isSat() == SAT_UNKNOWN && isValid() == VALIDITY_UNKNOWN; 93 } 94 getType()95 Type getType() const { return d_which; } 96 isNull()97 bool isNull() const { return d_which == TYPE_NONE; } 98 99 enum UnknownExplanation whyUnknown() const; 100 101 bool operator==(const Result& r) const; 102 inline bool operator!=(const Result& r) const; 103 Result asSatisfiabilityResult() const; 104 Result asValidityResult() const; 105 106 std::string toString() const; 107 getInputName()108 std::string getInputName() const { return d_inputName; } 109 110 /** 111 * Write a Result out to a stream in this language. 112 */ 113 void toStream(std::ostream& out, OutputLanguage language) const; 114 115 /** 116 * This is mostly the same the default 117 * If getType() == Result::TYPE_SAT && isSat() == Result::SAT_UNKNOWN, 118 * 119 */ 120 void toStreamSmt2(std::ostream& out) const; 121 122 /** 123 * Write a Result out to a stream in the Tptp format 124 */ 125 void toStreamTptp(std::ostream& out) const; 126 127 /** 128 * Write a Result out to a stream. 129 * 130 * The default implementation writes a reasonable string in lowercase 131 * for sat, unsat, valid, invalid, or unknown results. This behavior 132 * is overridable by each Printer, since sometimes an output language 133 * has a particular preference for how results should appear. 134 */ 135 void toStreamDefault(std::ostream& out) const; 136 }; /* class Result */ 137 138 inline bool Result::operator!=(const Result& r) const { return !(*this == r); } 139 140 std::ostream& operator<<(std::ostream& out, enum Result::Sat s) CVC4_PUBLIC; 141 std::ostream& operator<<(std::ostream& out, 142 enum Result::Validity v) CVC4_PUBLIC; 143 std::ostream& operator<<(std::ostream& out, 144 enum Result::UnknownExplanation e) CVC4_PUBLIC; 145 146 bool operator==(enum Result::Sat s, const Result& r) CVC4_PUBLIC; 147 bool operator==(enum Result::Validity v, const Result& r) CVC4_PUBLIC; 148 149 bool operator!=(enum Result::Sat s, const Result& r) CVC4_PUBLIC; 150 bool operator!=(enum Result::Validity v, const Result& r) CVC4_PUBLIC; 151 152 } /* CVC4 namespace */ 153 154 #endif /* __CVC4__RESULT_H */ 155