GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/util/result.h Lines: 14 14 100.0 %
Date: 2021-03-22 Branches: 9 12 75.0 %

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