cprover
|
Validation of smt response parse trees to produce either a strongly typed smt_responset representation, or a set of error messages. More...
#include "smt_response_validation.h"
#include <util/arith_tools.h>
#include <util/mp_arith.h>
#include <util/range.h>
#include <solvers/smt2_incremental/theories/smt_array_theory.h>
#include "smt_to_smt2_string.h"
#include <regex>
Go to the source code of this file.
Functions | |
static response_or_errort< smt_termt > | validate_term (const irept &parse_tree, const std::unordered_map< irep_idt, smt_identifier_termt > &identifier_table) |
template<typename argumentt, typename... argumentst> | |
void | collect_error_messages_impl (std::vector< std::string > &collected_error_messages, argumentt &&argument) |
template<typename argumentt, typename... argumentst> | |
void | collect_error_messages_impl (std::vector< std::string > &collected_error_messages, argumentt &&argument, argumentst &&... arguments) |
template<typename... argumentst> | |
std::vector< std::string > | collect_error_messages (argumentst &&... arguments) |
Builds a collection of error messages composed all error messages in the response_or_errort typed arguments in arguments . | |
template<typename smt_to_constructt, typename smt_baset = smt_to_constructt, typename... argumentst> | |
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, either return the collected errors if there are any or construct the class otherwise. | |
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 response_or_errort< irep_idt > | validate_string_literal (const irept &parse_tree) |
static std::optional< response_or_errort< smt_responset > > | valid_smt_error_response (const irept &parse_tree) |
static bool | all_subs_are_pairs (const irept &parse_tree) |
static std::optional< smt_termt > | valid_smt_indexed_bit_vector (const irept &parse_tree) |
Checks for valid bit vector constants of the form (_ bv(value) (width)) for example - (_ bv4 64). | |
static std::optional< smt_termt > | valid_smt_bool (const irept &parse_tree) |
static std::optional< smt_termt > | valid_smt_binary (const std::string &text) |
static std::optional< smt_termt > | valid_smt_hex (const std::string &text) |
static std::optional< smt_termt > | valid_smt_bit_vector_constant (const irept &parse_tree) |
static std::optional< response_or_errort< smt_termt > > | try_select_validation (const irept &parse_tree, const std::unordered_map< irep_idt, smt_identifier_termt > &identifier_table) |
static response_or_errort< smt_get_value_responset::valuation_pairt > | validate_valuation_pair (const irept &pair_parse_tree, const std::unordered_map< irep_idt, smt_identifier_termt > &identifier_table) |
static std::optional< response_or_errort< smt_responset > > | valid_smt_get_value_response (const irept &parse_tree, const std::unordered_map< irep_idt, smt_identifier_termt > &identifier_table) |
response_or_errort< smt_responset > | validate_smt_response (const irept &parse_tree, const std::unordered_map< irep_idt, smt_identifier_termt > &identifier_table) |
Validation of smt response parse trees to produce either a strongly typed smt_responset representation, or a set of error messages.
Functions named with the prefix validate_ require the given parse tree to be a particular kind of sub tree. Functions named with the prefix valid_ are called in places where the exact kind of sub-tree expected is unknown and so the function must determine if the sub-tree is of that type at all, before performing validation of it. These functions will return a response_or_errort in the case where the parse tree is of that type or an empty optional otherwise.
Definition in file smt_response_validation.cpp.
|
static |
Definition at line 155 of file smt_response_validation.cpp.
std::vector< std::string > collect_error_messages | ( | argumentst &&... | arguments | ) |
Builds a collection of error messages composed all error messages in the response_or_errort typed arguments in arguments
.
This is a templated function in order to handle response_or_errort instances which are specialised differently.
Definition at line 63 of file smt_response_validation.cpp.
void collect_error_messages_impl | ( | std::vector< std::string > & | collected_error_messages, |
argumentt && | argument ) |
Definition at line 36 of file smt_response_validation.cpp.
void collect_error_messages_impl | ( | std::vector< std::string > & | collected_error_messages, |
argumentt && | argument, | ||
argumentst &&... | arguments ) |
Definition at line 49 of file smt_response_validation.cpp.
|
static |
Produces a human-readable representation of the given parse_tree
, for use in error messaging.
Definition at line 106 of file smt_response_validation.cpp.
|
static |
Definition at line 243 of file smt_response_validation.cpp.
|
static |
Definition at line 203 of file smt_response_validation.cpp.
Definition at line 229 of file smt_response_validation.cpp.
Definition at line 192 of file smt_response_validation.cpp.
|
static |
Definition at line 129 of file smt_response_validation.cpp.
|
static |
Definition at line 325 of file smt_response_validation.cpp.
|
static |
Definition at line 214 of file smt_response_validation.cpp.
Checks for valid bit vector constants of the form (_ bv(value) (width)) for example - (_ bv4 64).
Definition at line 166 of file smt_response_validation.cpp.
|
nodiscard |
Definition at line 356 of file smt_response_validation.cpp.
|
static |
Definition at line 112 of file smt_response_validation.cpp.
|
static |
Definition at line 267 of file smt_response_validation.cpp.
|
static |
Definition at line 289 of file smt_response_validation.cpp.
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, either return the collected errors if there are any or construct the class otherwise.
smt_to_constructt | The class to construct. |
smt_baset | If the class to construct should be upcast to a base class before being stored in the response_or_errort, then the base class should be supplied in this parameter. If no upcast is required, then this should be left empty. |
argumentst | The pack of argument types matching the constructor of smt_to_constructt. These must each be packed into an instance of response_or_errort. |
Definition at line 88 of file smt_response_validation.cpp.