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
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
|
#if ! defined _pres_var_h
#define _pres_var_h 1
#include <omega/pres_gen.h>
#include <map>
namespace omega {
//
// Variable declaration.
// Variables are free or quantified.
// Free variables are classified as input, output and global.
// Quantified variables are classified as forall, exists and wildcard.
// All global variables are functions symbols of (possibly 0) arguments
// Local variables that correspond to >0-ary functions are identified
// as functions of a prefix of the input, output, or both tuples
//
//
// typedef enum {Input_Var, Output_Var, Set_Var,
// Global_Var, Forall_Var, Exists_Var, Wildcard_Var} Var_Kind;
typedef enum {Free_Var, Coef_Var, Bomega_Var} Global_Kind;
// NOW IN PRES_GEN.H, as its used as an argument and can't
// be forward declared:
// typedef enum {Unknown_Tuple = 0, Input_Tuple = 1, Output_Tuple = 2,
// Set_Tuple = Input_Tuple } Argument_Tuple;
// Only Input, Output, and Set can be passed to get_local,
// but the values 0 and 3 are also used internally.
class Var_Decl {
public:
inline Var_Kind kind() { return var_kind; }
int get_position();
Global_Var_ID get_global_var();
Argument_Tuple function_of(); // valid iff kind() == Global_var
Const_String base_name;
void name_variable(char *newname);
// The following should be used with care, as they are only valid
// after setup_names has been used on the relation containing this
// variable.
std::string name();
const char* char_name();
void set_kind(Var_Kind v) { var_kind = v; }
// Operation to allow the remap field to be used for
// union-find operations on variables.
// Be sure to reset the remap fields afterward
void UF_union(Variable_ID v);
Variable_ID UF_owner();
private:
Var_Decl(Const_String name, Var_Kind vkind, int pos);
Var_Decl(Var_Kind vkind, int pos);
Var_Decl(Variable_ID v);
Var_Decl(Const_String name, Global_Var_ID v);
Var_Decl(Const_String name, Global_Var_ID v, Argument_Tuple function_of);
friend class F_Declaration; // creates local variables
friend class Global_Var_Decl; // its constructors create Var_Decls.
friend class Global_Input_Output_Tuple;
friend void copy_var_decls(Variable_ID_Tuple &new_vl, Variable_ID_Tuple &vl);
private:
int instance;
void setup_name();
// these set up the names
friend class Rel_Body;
// friend class F_Declaration; already a friend
private:
Variable_ID remap; // pointer to new copy of this node
// lots of things need to get at "remap" - lots of relation ops,
// and functions that move UFS's around:
// dnf::make_level_carried_to and Conjunct::move_UFS_to_input()
// Also of course Conjunct::remap and push_exists
friend_rel_ops;
friend class DNF;
friend class Conjunct;
// this prints remap to the debugging output
friend void print_var_addrs(std::string &s, Variable_ID v);
friend void reset_remap_field(Variable_ID v);
friend void reset_remap_field(Sequence<Variable_ID> &S);
friend void reset_remap_field(Sequence<Variable_ID> &S, int var_no);
friend void reset_remap_field(Variable_ID_Tuple &S);
friend void reset_remap_field(Variable_ID_Tuple &S, int var_no);
private:
Var_Kind var_kind;
int position; // only for Input_Var, Output_Var
Global_Var_ID global_var; // only for Global_Var
Argument_Tuple of; // only for Global_Var
};
bool rm_variable(Variable_ID_Tuple &vl, Variable_ID v);
void reset_remap_field(Sequence<Variable_ID> &S);
void reset_remap_field(Sequence<Variable_ID> &S, int var_no);
void reset_remap_field(Variable_ID v);
void reset_remap_field(Variable_ID_Tuple &S);
void reset_remap_field(Variable_ID_Tuple &S, int var_no);
class Global_Input_Output_Tuple: public Tuple<Variable_ID> {
public:
Global_Input_Output_Tuple(Var_Kind in_my_kind, int init=-1);
~Global_Input_Output_Tuple();
virtual Variable_ID &operator[](int index);
virtual const Variable_ID &operator[](int index) const;
private:
Var_Kind my_kind;
static const int initial_allocation;
};
extern Global_Input_Output_Tuple input_vars;
extern Global_Input_Output_Tuple output_vars;
// This allows the user to refer to set_vars to query sets, w/o knowing
// they are really inputs.
extern Global_Input_Output_Tuple &set_vars;
Variable_ID input_var(int nth);
Variable_ID output_var(int nth);
Variable_ID set_var(int nth);
//
// Global_Var_ID uniquely identifies global var-s through the whole program.
// Global_Var_Decl is an ADT with the following operations:
// - create global variable,
// - find the arity of the variable, (default = 0, for symbolic consts)
// - get the name of global variable,
// - tell if two variables are the same (if they are the same object)
//
class Global_Var_Decl {
public:
Global_Var_Decl(Const_String baseName);
virtual Const_String base_name() const
{
return loc_rep1.base_name;
}
virtual void set_base_name(Const_String newName)
{
loc_rep1.base_name = newName;
loc_rep2.base_name = newName;
}
virtual int arity() const
{
return 0; // default compatible with old symbolic constant stuff
}
virtual Omega_Var *really_omega_var(); // until we get RTTI in C++
virtual Coef_Var_Decl *really_coef_var(); // until we get RTTI in C++
virtual Global_Kind kind() const;
private:
friend class Rel_Body; // Rel_Body::get_local calls this get_local
Variable_ID get_local()
{
assert(arity() == 0);
return &loc_rep1;
}
Variable_ID get_local(Argument_Tuple of)
{
assert(arity() == 0 || of == Input_Tuple || of == Output_Tuple);
return ((arity() == 0 || of == Input_Tuple) ? &loc_rep1 : &loc_rep2);
}
// local representative, there is just 1 for every 0-ary global variable
Var_Decl loc_rep1; // arity == 0, or arity > 0 and of == In
Var_Decl loc_rep2; // arity > 0 and of == Out
public:
// friend class Rel_Body; // Rel_Body::setup_names sets instance
friend class Var_Decl;
int instance;
};
class Coef_Var_Decl : public Global_Var_Decl {
public:
Coef_Var_Decl(int id, int var);
int stmt() const;
int var() const;
virtual Global_Kind kind() const;
virtual Coef_Var_Decl *really_coef_var(); // until we get RTTI in C++
private:
int i, v;
};
//
// Test subclass for Global_Var: named global variable
//
class Free_Var_Decl : public Global_Var_Decl {
public:
Free_Var_Decl(Const_String name);
Free_Var_Decl(Const_String name, int arity);
int arity() const;
virtual Global_Kind kind() const;
private:
int _arity;
};
/* === implementation functions === */
void copy_var_decls(Variable_ID_Tuple &new_vl, Variable_ID_Tuple &vl);
void free_var_decls(Variable_ID_Tuple &vl);
extern int wildCardInstanceNumber;
} // namespace
#endif
|
