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 <memory>
16 #include <string>
17 
18 #include <util/make_unique.h>
19 #include <util/message.h>
20 #include <util/symbol_table.h>
21 
24 
25 #include <goto-symex/goto_symex.h>
28 
29 #include <solvers/smt2/smt2_dec.h>
30 
32 #include <solvers/sat/satcheck.h>
33 
34 #include "path.h"
35 
37 {
38 public:
40  : constant_propagation(true),
41  symbol_table(_symbol_table),
44  equation(),
45  path_storage(),
46  options(),
48  satcheck(util_make_unique<satcheckt>()),
50  z3(ns, "accelerate", "", "", smt2_dect::solvert::Z3),
51  checker(&z3) // checker(&satchecker)
52  {
53  // Unconditionally set for performance reasons. This option setting applies
54  // only to this program.
55  options.set_option("simplify", true);
56  }
57 
59  void append(goto_programt &program);
60  void append_path(patht &path);
61  void append_loop(goto_programt &program, goto_programt::targett loop_header);
62 
63  targett assign(const exprt &lhs, const exprt &rhs);
64  targett assume(const exprt &guard);
65 
66  bool check_sat(bool do_slice);
67 
68  bool check_sat()
69  {
70  return check_sat(true);
71  }
72 
73  exprt eval(const exprt &e);
74 
75  void fix_types();
76 
78 
79 protected:
89 
90  std::unique_ptr<propt> satcheck;
94 };
95 
96 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_SCRATCH_PROGRAM_H
symbol_tablet symex_symbol_table
Generate Equation using Symbolic Execution.
targett assign(const exprt &lhs, const exprt &rhs)
Goto Programs with Functions.
symbol_tablet & symbol_table
std::list< instructiont > instructionst
Definition: goto_program.h:395
Decision procedure interface for various SMT 2.x solvers.
Definition: smt2_dec.h:35
goto_functionst functions
instructionst::iterator targett
Definition: goto_program.h:397
FIFO save queue: paths are resumed in the order that they were saved.
Definition: path_storage.h:104
targett assume(const exprt &guard)
exprt eval(const exprt &e)
Symbolic Execution.
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:403
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:19
TO_BE_DOCUMENTED.
Definition: namespace.h:74
Author: Diffblue Ltd.
scratch_programt(symbol_tablet &_symbol_table, message_handlert &mh)
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
Loop Acceleration.
The main class for the forward symbolic simulator.
Definition: goto_symex.h:46
symex_target_equationt equation
std::unique_ptr< propt > satcheck
void append_path(patht &path)
prop_convt * checker
Base class for all expressions.
Definition: expr.h:42
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition: make_unique.h:19
goto_symex_statet symex_state
void set_option(const std::string &option, const bool value)
Definition: options.cpp:24
goto_symext symex
path_fifot path_storage
bv_pointerst satchecker
Storage of symbolic execution paths to resume.
Concrete Goto Program.