cprover
smt_response_validation.h
Go to the documentation of this file.
1 // Author: Diffblue Ltd.
2 
3 #ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_RESPONSE_VALIDATION_H
4 #define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_RESPONSE_VALIDATION_H
5 
7 #include <util/invariant.h>
8 #include <util/nodiscard.h>
9 #include <util/optional.h>
10 
11 #include <string>
12 #include <vector>
13 
17 template <class smtt>
18 class response_or_errort final
19 {
20 public:
21  explicit response_or_errort(smtt smt);
22  explicit response_or_errort(std::string message);
23  explicit response_or_errort(std::vector<std::string> messages);
24 
27  const smtt *get_if_valid() const;
30  const std::vector<std::string> *get_if_error() const;
31 
32 private:
33  // The below two fields could be a single `std::variant` field, if there was
34  // an implementation of it available in the cbmc repository. However at the
35  // time of writing we are targeting C++11, `std::variant` was introduced in
36  // C++17 and we have no backported version.
38  std::vector<std::string> messages;
39 };
40 
42 validate_smt_response(const irept &parse_tree);
43 
44 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_RESPONSE_VALIDATION_H
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:372
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.
std::vector< std::string > messages
const smtt * get_if_valid() const
Gets the smt response if the response is valid, or returns nullptr otherwise.
#define NODISCARD
Definition: nodiscard.h:22
nonstd::optional< T > optionalt
Definition: optional.h:35
NODISCARD response_or_errort< smt_responset > validate_smt_response(const irept &parse_tree)