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