cprover
Loading...
Searching...
No Matches
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
17template <class smtt>
19{
20public:
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
32private:
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
42validate_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)