32 : messages{
std::move(message)}
38 : messages{
std::move(messages)}
46 smt.has_value() == messages.empty(),
47 "The response_or_errort class must be in the valid state or error state, "
49 return smt.has_value() ? &smt.value() :
nullptr;
56 smt.has_value() == messages.empty(),
57 "The response_or_errort class must be in the valid state or error state, "
59 return smt.has_value() ? nullptr : &messages;
65template <
typename argumentt,
typename... argumentst>
67 std::vector<std::string> &collected_messages,
70 if(
const auto messages = argument.get_if_error())
72 collected_messages.insert(
73 collected_messages.end(), messages->cbegin(), messages->end());
78template <
typename argumentt,
typename... argumentst>
80 std::vector<std::string> &collected_messages,
82 argumentst &&... arguments)
92template <
typename... argumentst>
95 std::vector<std::string> collected_messages;
97 return collected_messages;
115 typename smt_to_constructt,
116 typename smt_baset = smt_to_constructt,
117 typename... argumentst>
121 if(!collected_messages.empty())
126 smt_to_constructt{(*arguments.get_if_valid())...}};
138 return parse_tree.
pretty(0, 0);
144 if(!parse_tree.
get_sub().empty())
164 if(parse_tree.
get_sub().empty())
166 if(parse_tree.
get_sub().at(0).id() !=
"error")
170 if(parse_tree.
get_sub().size() == 1)
173 "Error response is missing the error message."}};
175 if(parse_tree.
get_sub().size() > 2)
178 "Error response has multiple error messages - \"" +
181 return validation_propagating<smt_error_responset, smt_responset>(
190 [](
const irept &sub) { return sub.get_sub().size() == 2; });
206 if(!parse_tree.
get_sub().empty())
208 if(parse_tree.
id() == ID_true)
210 if(parse_tree.
id() == ID_false)
217 static const std::regex binary_format{
"#b[01]+"};
218 if(!std::regex_match(text, binary_format))
222 const std::size_t width = text.size() - 2;
228 static const std::regex hex_format{
"#x[0-9A-Za-z]+"};
229 if(!std::regex_match(text, hex_format))
231 const std::string hex{text.begin() + 2, text.end()};
236 const std::size_t width = (text.size() - 2) * 4;
245 const auto value_string =
id2string(parse_tree.
id());
267 const auto &descriptor = pair_parse_tree.
get_sub()[0];
268 const auto &value = pair_parse_tree.
get_sub()[1];
269 return validation_propagating<smt_get_value_responset::valuation_pairt>(
284 if(parse_tree.
get_sub().empty())
288 std::vector<std::string> error_messages;
289 std::vector<smt_get_value_responset::valuation_pairt> valuation_pairs;
290 for(
const auto &pair : parse_tree.
get_sub())
293 if(
const auto error = pair_validation_result.get_if_error())
294 error_messages.insert(error_messages.end(), error->begin(), error->end());
295 if(
const auto valid_pair = pair_validation_result.get_if_valid())
296 valuation_pairs.push_back(*valid_pair);
298 if(!error_messages.empty())
309 if(parse_tree.
id() ==
"sat")
312 if(parse_tree.
id() ==
"unsat")
315 if(parse_tree.
id() ==
"unknown")
319 return *error_response;
320 if(parse_tree.
id() ==
"success")
322 if(parse_tree.
id() ==
"unsupported")
325 return *get_value_response;
There are a large number of kinds of tree structured or tree-like data in CPROVER.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const irep_idt & id() const
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(smtt smt)
const smtt * get_if_valid() const
Gets the smt response if the response is valid, or returns nullptr otherwise.
const std::string & id2string(const irep_idt &d)
const mp_integer string2integer(const std::string &n, unsigned base)
nonstd::optional< T > optionalt
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
static optionalt< smt_termt > valid_smt_binary(const std::string &text)
static std::string print_parse_tree(const irept &parse_tree)
Produces a human-readable representation of the given parse_tree, for use in error messaging.
static optionalt< smt_termt > valid_smt_bit_vector_constant(const irept &parse_tree)
static optionalt< response_or_errort< smt_responset > > valid_smt_error_response(const irept &parse_tree)
static optionalt< smt_termt > valid_smt_hex(const std::string &text)
static bool all_subs_are_pairs(const irept &parse_tree)
static response_or_errort< smt_termt > validate_term(const irept &parse_tree)
static response_or_errort< smt_get_value_responset::valuation_pairt > validate_valuation_pair(const irept &pair_parse_tree)
static response_or_errort< irep_idt > validate_smt_identifier(const irept &parse_tree)
static optionalt< smt_termt > valid_smt_bool(const irept &parse_tree)
static response_or_errort< irep_idt > validate_string_literal(const irept &parse_tree)
std::vector< std::string > collect_messages(argumentst &&... arguments)
Builds a collection of messages composed all messages in the response_or_errort typed arguments in ar...
response_or_errort< smt_baset > validation_propagating(argumentst &&... arguments)
Given a class to construct and a set of arguments to its constructor which may include errors,...
static optionalt< response_or_errort< smt_responset > > valid_smt_get_value_response(const irept &parse_tree)
void collect_messages_impl(std::vector< std::string > &collected_messages, argumentt &&argument)
response_or_errort< smt_responset > validate_smt_response(const irept &parse_tree)
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.