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
12
#include "
enumerating_loop_acceleration.h
"
13
14
#include "
accelerator.h
"
15
16
bool
enumerating_loop_accelerationt::accelerate
(
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"
;
29
namespacet
ns(
symbol_table
);
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
}
enumerating_loop_accelerationt::symbol_table
symbol_tablet & symbol_table
Definition:
enumerating_loop_acceleration.h:66
polynomial_acceleratort::accelerate
bool accelerate(patht &loop, path_acceleratort &accelerator)
Definition:
polynomial_accelerator.cpp:37
enumerating_loop_accelerationt::path_enumerator
std::unique_ptr< path_enumeratort > path_enumerator
Definition:
enumerating_loop_acceleration.h:75
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition:
namespace.h:90
enumerating_loop_accelerationt::polynomial_accelerator
polynomial_acceleratort polynomial_accelerator
Definition:
enumerating_loop_acceleration.h:72
path_acceleratort::path
patht path
Definition:
accelerator.h:62
path_acceleratort
Definition:
accelerator.h:26
enumerating_loop_accelerationt::path_limit
int path_limit
Definition:
enumerating_loop_acceleration.h:73
patht
std::list< path_nodet > patht
Definition:
path.h:44
accelerator.h
enumerating_loop_acceleration.h
enumerating_loop_accelerationt::accelerate
bool accelerate(path_acceleratort &accelerator)
Definition:
enumerating_loop_acceleration.cpp:16
src
goto-instrument
accelerate
enumerating_loop_acceleration.cpp
Generated by
1.8.17