CBMC
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 
6 #include <solvers/smt2_incremental/ast/smt_responses.h> // IWYU pragma: keep
7 #include <solvers/smt2_incremental/response_or_error.h>
8 
9 [[nodiscard]] response_or_errort<smt_responset> validate_smt_response(
10  const irept &parse_tree,
11  const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table);
12 
13 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_RESPONSE_VALIDATION_H
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:360
response_or_errort
Holds either a valid parsed response or response sub-tree of type.
Definition: response_or_error.h:17
response_or_error.h
validate_smt_response
response_or_errort< smt_responset > validate_smt_response(const irept &parse_tree, const std::unordered_map< irep_idt, smt_identifier_termt > &identifier_table)
Definition: smt_response_validation.cpp:356
smt_responses.h