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
|
#include <omega/pres_subs.h>
namespace omega {
Substitutions::Substitutions(Relation &input_R, Conjunct *input_c) {
int i;
r = new Relation(input_R,input_c);
c = r->single_conjunct();
c->reorder_for_print();
c->ordered_elimination(r->global_decls()->length());
int num_subs = c->problem->nSUBs;
subs = new eqn[num_subs];
for(i = 0; i < num_subs; i++)
subs[i] = SUBs[i];
subbed_vars.reallocate(num_subs);
/* Go through and categorize variables as:
1) substituted, 2) not substituted, 3) wildcard
Safevars number of variables were not able to be substituted.
nVars number of total variables, including wildcards.
nSUBs is the number of substitutions.
nSUBs + nVars == the number of variables that went in.
Then reset var and forwardingAddress arrays in the problem,
so that they will correctly refer to the reconstructed
mappedVars. */
Variable_ID_Tuple unsubbed_vars(c->problem->safeVars);
for(i = 1; i <= c->mappedVars.size(); i++)
if(c->mappedVars[i]->kind() != Wildcard_Var) {
int addr = c->problem->forwardingAddress[i];
assert(addr == c->find_column(c->mappedVars[i]) && addr != 0);
if(addr < 0) {
assert(-addr <= subbed_vars.size());
subbed_vars[-addr] = c->mappedVars[i];
}
else {
assert(addr <= unsubbed_vars.size());
unsubbed_vars[addr] = c->mappedVars[i];
}
}
else {
// Here we don't redeclare wildcards, just re-use them.
unsubbed_vars.append(c->mappedVars[i]);
}
assert(unsubbed_vars.size() + subbed_vars.size() == c->mappedVars.size());
c->mappedVars = unsubbed_vars; /* These are the variables that remain */
for(int col = 1; col <= c->problem->nVars; col++) {
c->problem->var[col] = col;
c->problem->forwardingAddress[col] = col;
}
}
Substitutions::~Substitutions() {
delete [] subs;
delete r;
}
bool Substitutions::substituted(Variable_ID v) {
return (subbed_vars.index(v) > 0);
}
Sub_Handle Substitutions::get_sub(Variable_ID v) {
assert(substituted(v) && "No substitution for variable");
return Sub_Handle(this,subbed_vars.index(v)-1,v);
}
bool Substitutions::sub_involves(Variable_ID v, Var_Kind kind) {
assert(substituted(v));
for(Constr_Vars_Iter i = get_sub(v); i; i++)
if ((*i).var->kind() == kind)
return true;
return false;
}
//::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
int Sub_Iterator::live() const {
return current <= last;
}
void Sub_Iterator::operator++() { this->operator++(0); }
void Sub_Iterator::operator++(int) {
current++;
}
Sub_Handle Sub_Iterator::operator*() {
assert(s && current <= last && "Sub_Iterator::operator*: bad call");
return Sub_Handle(s,current,s->subbed_vars[current+1]);
}
Sub_Handle Sub_Iterator::operator*() const {
assert(s && current <= last && "Sub_Iterator::operator*: bad call");
return Sub_Handle(s,current,s->subbed_vars[current+1]);
}
//::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Sub_Handle::Sub_Handle(Substitutions *_s, int _e, Variable_ID _v) :
Constraint_Handle(_s->c,&(_s->subs),_e), v(_v) {}
std::string Sub_Handle::print_to_string() const {
relation()->setup_names();
return v->name() + " = " + this->print_term_to_string();
}
std::string Sub_Handle::print_term_to_string() const {
/* The horrible truth is that print_term_to_string is a member
function of Conjunct, (and then Problem below it) but uses
nothing from there but the names, so you can pass it a pointer to
an equation that isn't even part of the conjunct. */
relation()->setup_names();
return c->print_term_to_string(&((*eqns)[e]));
}
/*
String Sub_Handle::print_to_string() const {
return c->problem->print_EQ_to_string(&((*eqns)[e]));
}
String Sub_Handle::print_term_to_string() const {
return c->print_term_to_string(&(*eqns[e]));
}
*/
} // namespace
|
