1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
|
/********************* */
/*! \file recursion_breaker.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 project.
** Copyright (c) 2009-2013 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
** \brief A utility class to help with detecting recursion in a
** computation
**
** A utility class to help with detecting recursion in a computation.
** A breadcrumb trail is left, and a function can query the breaker
** to see if recursion has occurred. For example:
**
** @code
** int foo(int x) {
** RecursionBreaker<int> breaker("foo", x);
** if(breaker.isRecursion()) {
** ++d_count;
** return 0;
** }
** int xfactor = x * x;
** if(x > 0) {
** xfactor = -xfactor;
** }
** int y = foo(11 * x + xfactor);
** int z = y < 0 ? y : x * y;
** cout << "x == " << x << ", y == " << y << " ==> " << z << endl;
** return z;
** }
** @endcode
**
** Recursion occurs after a while in this example, and the recursion
** is broken by the RecursionBreaker.
**
** RecursionBreaker is really just a thread-local set of "what has
** been seen." The above example is trivial, easily fixed by
** allocating such a set at the base of the recursion, and passing a
** reference to it to each invocation. But other cases of
** nontrivial, mutual recursion exist that aren't so easily broken,
** and that's what the RecursionBreaker is for. See
** Datatype::getCardinality(), for example. A Datatype's cardinality
** depends on the cardinalities of the types it references---but
** these, in turn can reference the original datatype in a cyclic
** fashion. Where that happens, we need to break the recursion.
**
** Several RecursionBreakers can be used at once; each is identified
** by the string tag in its constructor. If a single function is
** involved in the detection of recursion, a good choice is to use
** __FUNCTION__:
**
** RecursionBreaker<Foo*>(__FUNCTION__, this) breaker;
**
** Of course, if you're using GNU, you might prefer
** __PRETTY_FUNCTION__, since it's robust to overloading, namespaces,
** and containing classes. But neither is a good choice if two
** functions need to access the same RecursionBreaker mechanism.
**
** For non-primitive datatypes, it might be a good idea to use a
** pointer type to instantiate RecursionBreaker<>, for example with
** RecursionBreaker<Foo*>.
**/
#include "cvc4_private.h"
#ifndef __CVC4__RECURSION_BREAKER_H
#define __CVC4__RECURSION_BREAKER_H
#include <string>
#include <map>
#include <ext/hash_set>
#include "util/hash.h"
#include "util/tls.h"
#include "util/cvc4_assert.h"
namespace CVC4 {
template <class T, class Hasher = std::hash<T> >
class RecursionBreaker {
typedef std::hash_set<T, Hasher> Set;
typedef std::map<std::string, Set> Map;
static CVC4_THREADLOCAL(Map*) s_maps;
std::string d_tag;
const T d_item;
bool d_firstToTag;
bool d_recursion;
public:
/** Mark that item has been seen for tag. */
RecursionBreaker(std::string tag, const T& item) :
d_tag(tag),
d_item(item) {
if(s_maps == NULL) {
s_maps = new Map();
}
d_firstToTag = s_maps->find(tag) == s_maps->end();
Set& set = (*s_maps)[tag];
d_recursion = (set.find(item) != set.end());
Assert(!d_recursion || !d_firstToTag);
if(!d_recursion) {
set.insert(item);
}
}
/** Clean up the seen trail. */
~RecursionBreaker() {
Assert(s_maps->find(d_tag) != s_maps->end());
if(!d_recursion) {
(*s_maps)[d_tag].erase(d_item);
}
if(d_firstToTag) {
Assert((*s_maps)[d_tag].empty());
s_maps->erase(d_tag);
Assert(s_maps->find(d_tag) == s_maps->end());
}
}
/** Return true iff recursion has been detected. */
bool isRecursion() const throw() {
return d_recursion;
}
};/* class RecursionBreaker<T> */
template <class T, class Hasher>
CVC4_THREADLOCAL(typename RecursionBreaker<T, Hasher>::Map*) RecursionBreaker<T, Hasher>::s_maps;
}/* CVC4 namespace */
#endif /* __CVC4__RECURSION_BREAKER_H */
|
