CBMC
subsumed.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_SUBSUMED_H
13 #define CPROVER_GOTO_INSTRUMENT_ACCELERATE_SUBSUMED_H
14 
15 #include "path.h"
16 
17 #include <list>
18 
20 {
21 public:
22  explicit subsumed_patht(patht &_subsumed)
23  {
24  patht::iterator it = subsumed.begin();
25  subsumed.insert(it, _subsumed.begin(), _subsumed.end());
26  }
27 
31 };
32 
33 typedef std::list<subsumed_patht> subsumed_pathst;
34 
35 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_SUBSUMED_H
patht residue
Definition: subsumed.h:30
patht subsumed
Definition: subsumed.h:28
subsumed_patht(patht &_subsumed)
Definition: subsumed.h:22
patht accelerator
Definition: subsumed.h:29
Loop Acceleration.
std::list< path_nodet > patht
Definition: path.h:44
std::list< subsumed_patht > subsumed_pathst
Definition: subsumed.h:33