cprover
Loading...
Searching...
No Matches
state_encoding.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: State Encoding
4
5
Author: Daniel Kroening, dkr@amazon.com
6
7
\*******************************************************************/
8
11
12
#ifndef CPROVER_CPROVER_STATE_ENCODING_H
13
#define CPROVER_CPROVER_STATE_ENCODING_H
14
15
#include <
util/irep.h
>
16
#include <
util/optional.h
>
17
18
#include "
solver.h
"
19
20
#include <iosfwd>
21
22
class
goto_modelt
;
23
24
enum class
state_encoding_formatt
25
{
26
ASCII
,
27
SMT2
28
};
29
30
void
state_encoding
(
31
const
goto_modelt
&,
32
state_encoding_formatt
,
33
bool
program_is_inlined
,
34
optionalt<irep_idt>
contract
,
35
std::ostream &out);
36
37
solver_resultt
state_encoding_solver
(
38
const
goto_modelt
&,
39
bool
program_is_inlined
,
40
optionalt<irep_idt>
contract
,
41
const
solver_optionst
&);
42
43
void
variable_encoding
(
44
const
goto_modelt
&,
45
state_encoding_formatt
,
46
std::ostream &out);
47
48
#endif
// CPROVER_CPROVER_STATE_ENCODING_H
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition
ai.h:563
goto_modelt
Definition
goto_model.h:27
solver_optionst
Definition
solver.h:28
irep.h
optional.h
solver.h
Equality Propagation.
solver_resultt
solver_resultt
Definition
solver.h:21
state_encoding_formatt
state_encoding_formatt
Definition
state_encoding.h:25
state_encoding_formatt::SMT2
@ SMT2
state_encoding_formatt::ASCII
@ ASCII
variable_encoding
void variable_encoding(const goto_modelt &, state_encoding_formatt, std::ostream &out)
Definition
state_encoding.cpp:1204
state_encoding_solver
solver_resultt state_encoding_solver(const goto_modelt &, bool program_is_inlined, optionalt< irep_idt > contract, const solver_optionst &)
Definition
state_encoding.cpp:1236
state_encoding
void state_encoding(const goto_modelt &, state_encoding_formatt, bool program_is_inlined, optionalt< irep_idt > contract, std::ostream &out)
Definition
state_encoding.cpp:1178
cprover
state_encoding.h
Generated by
1.10.0