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
|
#if ! defined _Rel_map_h
#define _Rel_map_h 1
#include <omega/pres_gen.h>
#include <omega/pres_var.h>
namespace omega {
//
// Mapping for relations
// When a relation operation needs to re-arrange the variables,
// it describes the re-arragement with a mapping, and then calls
// align to re-arrange them.
//
// In a mapping, map_in (map_out/map_set) gives the new type and
// position of each of the old input (output/set) variables.
// For variables being mapped to Input, Output, or Set variables,
// the position is the new position in the tuple.
// For variables being mapped to Exists_Var, Forall_Var, or
// Wildcard_Var, the positions can be used to map multiple
// variables to the same quantified variable, by providing
// the same position. Each variable with a negative position
// is given a unique quantified variable that is NOT listed
// in the seen_exists_ids list.
// I'm not sure what the positions mean for Global_Vars - perhaps
// they are ignored?
//
// Currently, align seems to support only mapping to Set, Input,
// Output, and Exists vars.
//
class Mapping {
public:
inline Mapping(int no_in, int no_out): n_input(no_in), n_output(no_out) {}
inline Mapping(int no_set): n_input(no_set), n_output(0){}
inline Mapping(const Mapping &m): n_input(m.n_input), n_output(m.n_output) {
int i;
for(i=1; i<=n_input; i++) map_in_kind[i] = m.map_in_kind[i];
for(i=1; i<=n_input; i++) map_in_pos[i] = m.map_in_pos[i];
for(i=1; i<=n_output;i++) map_out_kind[i] = m.map_out_kind[i];
for(i=1; i<=n_output;i++) map_out_pos[i] = m.map_out_pos[i];
}
inline void set_map (Var_Kind in_kind, int pos, Var_Kind type, int map) {
if(in_kind==Input_Var)
set_map_in(pos,type,map);
else if(in_kind==Set_Var)
set_map_in(pos,type,map);
else if(in_kind==Output_Var)
set_map_out(pos,type,map);
else
assert(0);
}
inline void set_map_in (int pos, Var_Kind type, int map) {
assert(pos>=1 && pos<=n_input);
map_in_kind[pos] = type;
map_in_pos[pos] = map;
}
inline void set_map_set (int pos, Var_Kind type, int map) {
assert(pos>=1 && pos<=n_input);
map_in_kind[pos] = type;
map_in_pos[pos] = map;
}
inline void set_map_out(int pos, Var_Kind type, int map) {
assert(pos>=1 && pos<=n_output);
map_out_kind[pos] = type;
map_out_pos[pos] = map;
}
inline Var_Kind get_map_in_kind(int pos) const {
assert(pos>=1 && pos<=n_input);
return map_in_kind[pos];
}
inline int get_map_in_pos(int pos) const {
assert(pos>=1 && pos<=n_input);
return map_in_pos[pos];
}
inline Var_Kind get_map_out_kind(int pos) const {
assert(pos>=1 && pos<=n_output);
return map_out_kind[pos];
}
inline int get_map_out_pos(int pos) const {
assert(pos>=1 && pos<=n_output);
return map_out_pos[pos];
}
inline int n_in() const { return n_input; }
inline int n_out() const { return n_output; }
// If a tuple as a whole becomes the new Input or Output tuple,
// return the Tuple of they will become (Input, Output)
// Return Unknown_Tuple otherwise
inline Argument_Tuple get_tuple_fate(Argument_Tuple t, int prefix = -1) const {
return t== Input_Tuple ? get_input_fate(prefix) :
(t==Output_Tuple ? get_output_fate(prefix) : Unknown_Tuple); }
inline Argument_Tuple get_set_fate(int prefix = -1) const {
return get_input_fate(prefix); }
inline Argument_Tuple get_input_fate(int prefix = -1) const {
if (prefix < 0) prefix = n_input;
assert(n_input >= prefix);
if (n_input < prefix)
return Unknown_Tuple;
Var_Kind vf = map_in_kind[1];
for (int i = 1; i<=prefix; i++)
if (map_in_pos[i]!=i || map_in_kind[i]!=vf)
return Unknown_Tuple;
return vf == Input_Var ? Input_Tuple
: vf == Set_Var ? Set_Tuple
: vf == Output_Var ? Output_Tuple
: Unknown_Tuple;
}
inline Argument_Tuple get_output_fate(int prefix = -1) const {
if (prefix < 0) prefix = n_output;
assert(n_output >= prefix);
if (n_output < 1)
return Unknown_Tuple;
Var_Kind vf = map_out_kind[1];
for (int i = 1; i<=prefix; i++)
if (map_out_pos[i]!=i || map_out_kind[i]!=vf)
return Unknown_Tuple;
return vf == Input_Var ? Input_Tuple
: vf == Set_Var ? Set_Tuple
: vf == Output_Var ? Output_Tuple
: Unknown_Tuple;
}
inline static Mapping Identity(int inp, int outp) {
Mapping m(inp, outp); int i;
for(i=1; i<=m.n_input; i++) m.set_map(Input_Var, i, Input_Var, i);
for(i=1; i<=m.n_output;i++) m.set_map(Output_Var, i, Output_Var, i);
return m;
}
inline static Mapping Identity(int setvars) {
Mapping m(setvars); int i;
for(i=1; i<=setvars; i++) m.set_map(Set_Var, i, Set_Var, i);
return m;
}
private:
int n_input;
int n_output;
Var_Kind map_in_kind[maxVars];
int map_in_pos[maxVars];
Var_Kind map_out_kind[maxVars];
int map_out_pos[maxVars];
};
} // namespace
#endif
|
