cprover
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 <iostream>
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  goto_program.output_instruction(ns, "OMG", std::cout, *it->loc);
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 }
enumerating_loop_accelerationt::symbol_table
symbol_tablet & symbol_table
Definition: enumerating_loop_acceleration.h:67
polynomial_acceleratort::accelerate
bool accelerate(patht &loop, path_acceleratort &accelerator)
Definition: polynomial_accelerator.cpp:45
enumerating_loop_accelerationt::path_enumerator
std::unique_ptr< path_enumeratort > path_enumerator
Definition: enumerating_loop_acceleration.h:76
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
enumerating_loop_accelerationt::goto_program
goto_programt & goto_program
Definition: enumerating_loop_acceleration.h:69
goto_programt::output_instruction
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
Definition: goto_program.cpp:41
enumerating_loop_accelerationt::polynomial_accelerator
polynomial_acceleratort polynomial_accelerator
Definition: enumerating_loop_acceleration.h:73
path_acceleratort::path
patht path
Definition: accelerator.h:62
path_acceleratort
Definition: accelerator.h:27
enumerating_loop_accelerationt::path_limit
int path_limit
Definition: enumerating_loop_acceleration.h:74
patht
std::list< path_nodet > patht
Definition: path.h:45
enumerating_loop_acceleration.h
Loop Acceleration.
enumerating_loop_accelerationt::accelerate
bool accelerate(path_acceleratort &accelerator)
Definition: enumerating_loop_acceleration.cpp:16