CBMC
enumerating_loop_acceleration.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Loop Acceleration
4 
5 Author: Matt Lewis
6 
7 \*******************************************************************/
8 
11 
13 
14 #include "accelerator.h"
15 
17  path_acceleratort &accelerator)
18 {
19  patht path;
20  int enumerated = 0;
21 
22  // Note: we use enumerated!=path_limit rather than
23  // enumerated < path_limit so that passing in path_limit=-1 causes
24  // us to enumerate all the paths (or at least 2^31 of them...)
25  while(path_enumerator->next(path) && enumerated++!=path_limit)
26  {
27 #ifdef DEBUG
28  std::cout << "Found a path...\n";
30 
31  for(patht::iterator it = path.begin();
32  it!=path.end();
33  ++it)
34  {
35  it->loc->output(std::cout);
36  }
37 #endif
38 
39  if(polynomial_accelerator.accelerate(path, accelerator))
40  {
41  // We accelerated this path successfully -- return it.
42 #ifdef DEBUG
43  std::cout << "Accelerated it\n";
44 #endif
45 
46  accelerator.path.swap(path);
47  return true;
48  }
49 
50  path.clear();
51  }
52 
53  // No more paths, or we hit the enumeration limit.
54 #ifdef DEBUG
55  std::cout << "No more paths to accelerate!\n";
56 #endif
57 
58  return false;
59 }
Loop Acceleration.
std::unique_ptr< path_enumeratort > path_enumerator
bool accelerate(path_acceleratort &accelerator)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
bool accelerate(patht &loop, path_acceleratort &accelerator)
std::list< path_nodet > patht
Definition: path.h:44