blob: 56951d5316150b201f4fbed93b571eca202822ad (
plain)
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
|
/********************* */
/*! \file transitive_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"
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 & (unsigned(1) << index)) != 0;
else if (d_next == NULL) return false;
else return d_next->read(index - 64);
}
void write(unsigned index) {
if (index < 64) {
unsigned mask = unsigned(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) {}
~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);
void debugPrintMatrix();
};
}/* CVC4 namespace */
#endif /* __CVC4__UTIL__TRANSITIVE_CLOSURE_H */
|
