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
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
|
/********************* */
/*! \file trans_closure.h
** \verbatim
** Original author: barrett
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
** \brief The transitive closure module
**
** The transitive closure module.
**/
#ifndef __CVC4__UTIL__TRANSITIVE_CLOSURE_H
#define __CVC4__UTIL__TRANSITIVE_CLOSURE_H
#include "context/context.h"
#include "expr/node.h"
#include <map>
#include "context/cdlist.h"
#include "context/cdmap.h"
#include "context/cdo.h"
namespace CVC4 {
/*
* Implements context-dependent variable-sized boolean vector
*/
class CDBV :public context::ContextObj {
uint64_t d_data;
CDBV* d_next;
CDBV(const CDBV& cdbv) : ContextObj(cdbv), d_data(cdbv.d_data), d_next(cdbv.d_next) {}
/**
* operator= for CDBV is private to ensure CDBV object is not copied.
*/
CDBV& operator=(const CDBV& cdbv);
protected:
context::ContextObj* save(context::ContextMemoryManager* pCMM) {
return new(pCMM) CDBV(*this);
}
void restore(context::ContextObj* pContextObj) {
d_data = ((CDBV*) pContextObj)->d_data;
}
uint64_t data() { return d_data; }
CDBV* next() { return d_next; }
public:
CDBV(context::Context* context) :
ContextObj(context), d_data(0), d_next(NULL)
{}
~CDBV() {
if (d_next != NULL) {
d_next->deleteSelf();
}
destroy();
}
bool read(unsigned index) {
if (index < 64) return (d_data & (uint64_t(1) << index)) != 0;
else if (d_next == NULL) return false;
else return d_next->read(index - 64);
}
void write(unsigned index) {
if (index < 64) {
uint64_t mask = uint64_t(1) << index;
if ((d_data & mask) != 0) return;
makeCurrent();
d_data = d_data | mask;
}
else if (d_next != NULL) {
d_next->write(index - 64);
}
else {
makeCurrent();
d_next = new(true) CDBV(getContext());
d_next->write(index - 64);
}
}
void merge(CDBV* pcdbv) {
d_data = d_data | pcdbv->data();
if (d_next != NULL && pcdbv->next() != NULL) {
d_next->merge(pcdbv->next());
}
}
};
/**
* Transitive closure module for CVC4.
*
*/
class TransitiveClosure {
context::Context* d_context;
std::vector<CDBV* > adjMatrix;
public:
TransitiveClosure(context::Context* context) : d_context(context) {}
virtual ~TransitiveClosure();
/* Add an edge from node i to node j. Return false if successful, true if this edge would create a cycle */
bool addEdge(unsigned i, unsigned j);
/** whether node i is connected to node j */
bool isConnected(unsigned i, unsigned j);
void debugPrintMatrix();
};
/**
* Transitive closure module for nodes in CVC4.
*
*/
class TransitiveClosureNode : public TransitiveClosure{
context::CDO< unsigned > d_counter;
context::CDMap< Node, unsigned, NodeHashFunction > nodeMap;
//for debugging
context::CDList< std::pair< Node, Node > > currEdges;
public:
TransitiveClosureNode(context::Context* context) :
TransitiveClosure(context), d_counter( context, 0 ), nodeMap( context ), currEdges(context) {}
~TransitiveClosureNode(){}
/** get id for node */
unsigned getId( Node i );
/** Add an edge from node i to node j. Return false if successful, true if this edge would create a cycle */
bool addEdgeNode(Node i, Node j) {
currEdges.push_back( std::pair< Node, Node >( i, j ) );
return addEdge( getId( i ), getId( j ) );
}
/** whether node i is connected to node j */
bool isConnectedNode(Node i, Node j) {
return isConnected( getId( i ), getId( j ) );
}
void debugPrint();
};
}/* CVC4 namespace */
#endif /* __CVC4__UTIL__TRANSITIVE_CLOSURE_H */
|
