CBMC
•All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:364
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