cprover
Loading...
Searching...
No Matches
response_or_error.h
Go to the documentation of this file.
1// Author: Diffblue Ltd.
2
3#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_RESPONSE_OR_ERROR_H
4#define CPROVER_SOLVERS_SMT2_INCREMENTAL_RESPONSE_OR_ERROR_H
5
6#include <util/invariant.h>
7#include <util/optional.h>
8
9#include <string>
10#include <vector>
11
15template <class smtt>
17{
18public:
19 explicit response_or_errort(smtt smt) : smt{std::move(smt)}
20 {
21 }
22
23 explicit response_or_errort(std::string message)
24 : messages{std::move(message)}
25 {
26 }
27
28 explicit response_or_errort(std::vector<std::string> messages)
29 : messages{std::move(messages)}
30 {
31 }
32
35 const smtt *get_if_valid() const
36 {
38 smt.has_value() == messages.empty(),
39 "The response_or_errort class must be in the valid state or error state, "
40 "exclusively.");
41 return smt.has_value() ? &smt.value() : nullptr;
42 }
43
46 const std::vector<std::string> *get_if_error() const
47 {
49 smt.has_value() == messages.empty(),
50 "The response_or_errort class must be in the valid state or error state, "
51 "exclusively.");
52 return smt.has_value() ? nullptr : &messages;
53 }
54
55private:
56 // The below two fields could be a single `std::variant` field, if there was
57 // an implementation of it available in the cbmc repository. However at the
58 // time of writing we are targeting C++11, `std::variant` was introduced in
59 // C++17 and we have no backported version.
61 std::vector<std::string> messages;
62};
63
64#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_RESPONSE_OR_ERROR_H
Holds either a valid parsed response or response sub-tree of type.
const std::vector< std::string > * get_if_error() const
Gets the error messages if the response is invalid, or returns nullptr otherwise.
response_or_errort(std::string message)
std::vector< std::string > messages
optionalt< smtt > smt
const smtt * get_if_valid() const
Gets the smt response if the response is valid, or returns nullptr otherwise.
response_or_errort(std::vector< std::string > messages)
STL namespace.
nonstd::optional< T > optionalt
Definition optional.h:35
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423