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 <util/nodiscard.h>
7 
8 #include <solvers/smt2_incremental/response_or_error.h>
9 #include <solvers/smt2_incremental/smt_responses.h>
10 
11 NODISCARD response_or_errort<smt_responset> validate_smt_response(
12  const irept &parse_tree,
13  const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table);
14 
15 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_RESPONSE_VALIDATION_H
response_or_errort
Holds either a valid parsed response or response sub-tree of type.
Definition: response_or_error.h:16
NODISCARD
#define NODISCARD
Definition: nodiscard.h:22
response_or_error.h
nodiscard.h
smt_responses.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:352
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:359