CBMC
smt_is_dynamic_object.h
Go to the documentation of this file.
1 // Author: Diffblue Ltd.
2 
3 #ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_IS_DYNAMIC_OBJECT_H
4 #define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_IS_DYNAMIC_OBJECT_H
5 
6 #include <solvers/smt2_incremental/ast/smt_commands.h>
7 #include <solvers/smt2_incremental/ast/smt_terms.h>
8 
14 struct smt_is_dynamic_objectt final
15 {
16  smt_is_dynamic_objectt();
20  smt_declare_function_commandt declaration;
22  using make_applicationt =
23  smt_function_application_termt::factoryt<smt_command_functiont>;
24  make_applicationt make_application;
27  smt_commandt
28  make_definition(std::size_t unique_id, bool is_dynamic_object) const;
29 };
30 
31 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_IS_DYNAMIC_OBJECT_H
smt_commandt
Definition: smt_commands.h:15
smt_declare_function_commandt
Definition: smt_commands.h:51
smt_function_application_termt::factoryt< smt_command_functiont >
smt_commands.h
smt_terms.h
smt_is_dynamic_objectt
Specifics of how the dynamic object status lookup is implemented in SMT terms.
Definition: smt_is_dynamic_object.h:15
smt_is_dynamic_objectt::make_application
make_applicationt make_application
Definition: smt_is_dynamic_object.h:24
smt_is_dynamic_objectt::smt_is_dynamic_objectt
smt_is_dynamic_objectt()
Definition: smt_is_dynamic_object.cpp:17
smt_is_dynamic_objectt::declaration
smt_declare_function_commandt declaration
The command for declaring the is_dynamic_object function.
Definition: smt_is_dynamic_object.h:20
smt_is_dynamic_objectt::make_definition
smt_commandt make_definition(std::size_t unique_id, bool is_dynamic_object) const
Makes the command to define the resulting is_dynamic_object status for calls to the is_dynamic_object...
Definition: smt_is_dynamic_object.cpp:23