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>
70 if(
const auto messages =
argument.get_if_error())
78template <
typename argumentt,
typename... argumentst>
82 argumentst &&... arguments)
92template <
typename... argumentst>
117 typename... argumentst>
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 - \"" +
190 [](
const irept &sub) { return sub.get_sub().size() == 2; });
206 if(!parse_tree.
get_sub().empty())
222 const std::size_t width = text.size() - 2;
228 static const std::regex
hex_format{
"#x[0-9A-Za-z]+"};
231 const std::string
hex{text.begin() + 2, text.end()};
236 const std::size_t width = (text.size() - 2) * 4;
284 if(parse_tree.
get_sub().empty())
309 if(parse_tree.
id() ==
"sat")
312 if(parse_tree.
id() ==
"unsat")
315 if(parse_tree.
id() ==
"unknown")
320 if(parse_tree.
id() ==
"success")
322 if(parse_tree.
id() ==
"unsupported")
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
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
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)
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'.