blob: 79c1d76290dcb695edc2cd6fc26043b7968ab681 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
|
/********************* */
/*! \file cvc4cpp.cpp
** \verbatim
** Top contributors (to current version):
** Aina Niemetz
** This file is part of the CVC4 project.
** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
** \brief The CVC4 C++ API.
**
** The CVC4 C++ API.
**/
#include "api/cvc4cpp.h"
#include "util/result.h"
#include <sstream>
namespace CVC4 {
namespace api {
/* -------------------------------------------------------------------------- */
/* Result */
/* -------------------------------------------------------------------------- */
Result::Result(const CVC4::Result& r) : d_result(new CVC4::Result(r)) {}
bool Result::isSat(void) const
{
return d_result->getType() == CVC4::Result::TYPE_SAT
&& d_result->isSat() == CVC4::Result::SAT;
}
bool Result::isUnsat(void) const
{
return d_result->getType() == CVC4::Result::TYPE_SAT
&& d_result->isSat() == CVC4::Result::UNSAT;
}
bool Result::isSatUnknown(void) const
{
return d_result->getType() == CVC4::Result::TYPE_SAT
&& d_result->isSat() == CVC4::Result::SAT_UNKNOWN;
}
bool Result::isValid(void) const
{
return d_result->getType() == CVC4::Result::TYPE_VALIDITY
&& d_result->isValid() == CVC4::Result::VALID;
}
bool Result::isInvalid(void) const
{
return d_result->getType() == CVC4::Result::TYPE_VALIDITY
&& d_result->isValid() == CVC4::Result::INVALID;
}
bool Result::isValidUnknown(void) const
{
return d_result->getType() == CVC4::Result::TYPE_VALIDITY
&& d_result->isValid() == CVC4::Result::VALIDITY_UNKNOWN;
}
bool Result::operator==(const Result& r) const
{
return *d_result == *r.d_result;
}
bool Result::operator!=(const Result& r) const
{
return *d_result != *r.d_result;
}
std::string Result::getUnknownExplanation(void) const
{
std::stringstream ss;
ss << d_result->whyUnknown();
return ss.str();
}
std::string Result::toString(void) const { return d_result->toString(); }
std::ostream& operator<<(std::ostream& out, const Result& r)
{
out << r.toString();
return out;
}
} // namespace api
} // namespace CVC4
|
