cprover
scratch_program.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Loop Acceleration
4 
5 Author: Matt Lewis
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_INSTRUMENT_ACCELERATE_SCRATCH_PROGRAM_H
13 #define CPROVER_GOTO_INSTRUMENT_ACCELERATE_SCRATCH_PROGRAM_H
14 
15 #include <string>
16 
17 #include <util/symbol_table.h>
18 
21 
22 #include <goto-symex/goto_symex.h>
24 
25 #include <solvers/smt2/smt2_dec.h>
26 
28 #include <solvers/sat/satcheck.h>
29 
30 #include "path.h"
31 
33 {
34 public:
35  explicit scratch_programt(symbol_tablet &_symbol_table):
37  symbol_table(_symbol_table),
39  equation(ns),
41  satcheck(new satcheckt),
43  z3(ns, "accelerate", "", "", smt2_dect::solvert::Z3),
44  checker(&z3) // checker(&satchecker)
45  {
46  }
47 
49  {
50  delete satcheck;
51  }
52 
54  void append(goto_programt &program);
55  void append_path(patht &path);
56  void append_loop(goto_programt &program, goto_programt::targett loop_header);
57 
58  targett assign(const exprt &lhs, const exprt &rhs);
59  targett assume(const exprt &guard);
60 
61  bool check_sat(bool do_slice);
62 
63  bool check_sat()
64  {
65  return check_sat(true);
66  }
67 
68  exprt eval(const exprt &e);
69 
70  void fix_types();
71 
73 
74 protected:
78  const namespacet ns;
81 
86 };
87 
88 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_SCRATCH_PROGRAM_H
const namespacet ns
Generate Equation using Symbolic Execution.
targett assign(const exprt &lhs, const exprt &rhs)
instructionst instructions
The list of instructions in the goto program.
Goto Programs with Functions.
symbol_tablet & symbol_table
scratch_programt(symbol_tablet &_symbol_table)
Decision procedure interface for various SMT 2.x solvers.
Definition: smt2_dec.h:35
goto_functionst functions
targett assume(const exprt &guard)
exprt eval(const exprt &e)
Symbolic Execution.
void append_loop(goto_programt &program, goto_programt::targett loop_header)
void append(goto_programt::instructionst &instructions)
std::list< path_nodet > patht
Definition: path.h:45
The symbol table.
Definition: symbol_table.h:52
TO_BE_DOCUMENTED.
Definition: namespace.h:62
Symbol table.
TO_BE_DOCUMENTED.
Definition: prop.h:22
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
Loop Acceleration.
The main class for the forward symbolic simulator.
Definition: goto_symex.h:41
symex_target_equationt equation
void append_path(patht &path)
prop_convt * checker
Base class for all expressions.
Definition: expr.h:46
goto_symex_statet symex_state
goto_symext symex
bv_pointerst satchecker
Concrete Goto Program.