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
|
#if ! defined _pres_cnstr_h
#define _pres_cnstr_h 1
#include <omega/pres_var.h>
#include <vector>
namespace omega {
//
// Constraint handles
//
void copy_constraint(Constraint_Handle H, const Constraint_Handle initial);
class Constraint_Handle {
public:
Constraint_Handle() {}
virtual ~Constraint_Handle() {}
void update_coef(Variable_ID, coef_t delta);
void update_const(coef_t delta);
coef_t get_coef(Variable_ID v) const;
coef_t get_const() const;
bool has_wildcards() const;
int max_tuple_pos() const;
int min_tuple_pos() const;
bool is_const(Variable_ID v);
bool is_const_except_for_global(Variable_ID v);
virtual std::string print_to_string() const;
virtual std::string print_term_to_string() const;
Variable_ID get_local(const Global_Var_ID G);
Variable_ID get_local(const Global_Var_ID G, Argument_Tuple of);
// not sure that the second one can be used in a meaningful
// way if the conjunct is in multiple relations
void finalize();
void multiply(int multiplier);
Rel_Body *relation() const;
protected:
Conjunct *c;
eqn **eqns;
int e;
friend class Constr_Vars_Iter;
friend class Constraint_Iterator;
Constraint_Handle(Conjunct *, eqn **, int);
#if defined PROTECTED_DOESNT_WORK
friend class EQ_Handle;
friend class GEQ_Handle;
#endif
void update_coef_during_simplify(Variable_ID, coef_t delta);
void update_const_during_simplify(coef_t delta);
coef_t get_const_during_simplify() const;
coef_t get_coef_during_simplify(Variable_ID v) const;
public:
friend class Conjunct; // assert_leading_info updates coef's
// as does move_UFS_to_input
friend class DNF; // and DNF::make_level_carried_to
friend void copy_constraint(Constraint_Handle H,
const Constraint_Handle initial);
// copy_constraint does updates and gets at c and e
};
class GEQ_Handle : public Constraint_Handle {
public:
inline GEQ_Handle() {}
virtual std::string print_to_string() const;
virtual std::string print_term_to_string() const;
bool operator==(const Constraint_Handle &that);
void negate();
private:
friend class Conjunct;
friend class GEQ_Iterator;
GEQ_Handle(Conjunct *, int);
};
class EQ_Handle : public Constraint_Handle {
public:
inline EQ_Handle() {}
virtual std::string print_to_string() const;
virtual std::string print_term_to_string() const;
bool operator==(const Constraint_Handle &that);
private:
friend class Conjunct;
friend class EQ_Iterator;
EQ_Handle(Conjunct *, int);
};
//
// Conjuct iterators -- for querying resulting DNF.
//
class Constraint_Iterator : public Generator<Constraint_Handle> {
public:
Constraint_Iterator(Conjunct *);
int live() const;
void operator++(int);
void operator++();
Constraint_Handle operator* ();
Constraint_Handle operator* () const;
private:
Conjunct *c;
int current,last;
eqn **eqns;
};
class EQ_Iterator : public Generator<EQ_Handle> {
public:
EQ_Iterator(Conjunct *);
int live() const;
void operator++(int);
void operator++();
EQ_Handle operator* ();
EQ_Handle operator* () const;
private:
Conjunct *c;
int current, last;
};
class GEQ_Iterator : public Generator<GEQ_Handle> {
public:
GEQ_Iterator(Conjunct *);
int live() const;
void operator++(int);
void operator++();
GEQ_Handle operator* ();
GEQ_Handle operator* () const;
private:
Conjunct *c;
int current, last;
};
//
// Variables of constraint iterator.
//
struct Variable_Info {
Variable_ID var;
coef_t coef;
Variable_Info(Variable_ID _var, coef_t _coef)
{ var = _var; coef = _coef; }
};
class Constr_Vars_Iter : public Generator<Variable_Info> {
public:
Constr_Vars_Iter(const Constraint_Handle &ch, bool _wild_only = false);
int live() const;
void operator++(int);
void operator++();
Variable_Info operator*() const;
Variable_ID curr_var() const;
coef_t curr_coef() const;
private:
eqn **eqns;
int e;
Problem *prob;
Variable_ID_Tuple &vars;
bool wild_only;
int current;
};
} // namespace
#endif
|
