1 /*++
2 Copyright (c) 2006 Microsoft Corporation
3
4 Module Name:
5
6 linear_equation.cpp
7
8 Abstract:
9
10 Basic infrastructure for managing linear equations of the form:
11
12 a_1 * x_1 + ... + a_n * x_n = 0
13
14 Author:
15
16 Leonardo de Moura (leonardo) 2011-06-28
17
18 Revision History:
19
20 --*/
21 #include "tactic/arith/linear_equation.h"
22
23 /**
24 \brief Return the position of variable x_i in the linear equation.
25 Return UINT_MAX, if the variable is not in the linear_equation.
26 */
pos(unsigned x_i) const27 unsigned linear_equation::pos(unsigned x_i) const {
28 int low = 0;
29 int high = m_size - 1;
30 while (true) {
31 int mid = low + ((high - low) / 2);
32 var x_mid = m_xs[mid];
33 if (x_i > x_mid) {
34 low = mid + 1;
35 if (low > high)
36 return UINT_MAX;
37 }
38 else if (x_i < x_mid) {
39 high = mid - 1;
40 if (low > high)
41 return UINT_MAX;
42 }
43 else {
44 return mid;
45 }
46 }
47 }
48
display(std::ostream & out,linear_equation const & eq) const49 void linear_equation_manager::display(std::ostream & out, linear_equation const & eq) const {
50 unsigned sz = eq.m_size;
51 for (unsigned i = 0; i < sz; i++) {
52 if (i > 0)
53 out << " + ";
54 out << m.to_string(eq.m_as[i]) << "*x" << eq.m_xs[i];
55 }
56 out << " = 0";
57 }
58
mk(unsigned sz,mpq * as,var * xs,bool normalized)59 linear_equation * linear_equation_manager::mk(unsigned sz, mpq * as, var * xs, bool normalized) {
60 SASSERT(sz > 1);
61
62 // compute lcm of the denominators
63 mpz l;
64 mpz r;
65 m.set(l, as[0].denominator());
66 for (unsigned i = 1; i < sz; i++) {
67 m.set(r, as[i].denominator());
68 m.lcm(r, l, l);
69 }
70
71 TRACE("linear_equation_mk", tout << "lcm: " << m.to_string(l) << "\n";);
72
73 // copy l * as to m_int_buffer.
74 m_int_buffer.reset();
75 for (unsigned i = 0; i < sz; i++) {
76 TRACE("linear_equation_mk", tout << "before as[" << i << "]: " << m.to_string(as[i]) << "\n";);
77 m.mul(l, as[i], as[i]);
78 TRACE("linear_equation_mk", tout << "after as[" << i << "]: " << m.to_string(as[i]) << "\n";);
79 SASSERT(m.is_int(as[i]));
80 m_int_buffer.push_back(as[i].numerator());
81 }
82
83 linear_equation * new_eq = mk(sz, m_int_buffer.data(), xs, normalized);
84
85 m.del(r);
86 m.del(l);
87
88 return new_eq;
89 }
90
mk_core(unsigned sz,mpz * as,var * xs)91 linear_equation * linear_equation_manager::mk_core(unsigned sz, mpz * as, var * xs) {
92 SASSERT(sz > 0);
93 DEBUG_CODE({
94 for (unsigned i = 1; i < sz; i++) {
95 SASSERT(xs[i-1] < xs[i]);
96 }
97 });
98
99 TRACE("linear_equation_bug", for (unsigned i = 0; i < sz; i++) tout << m.to_string(as[i]) << "*x" << xs[i] << " "; tout << "\n";);
100
101 mpz g;
102 m.set(g, as[0]);
103 for (unsigned i = 1; i < sz; i++) {
104 if (m.is_one(g))
105 break;
106 if (m.is_neg(as[i])) {
107 m.neg(as[i]);
108 m.gcd(g, as[i], g);
109 m.neg(as[i]);
110 }
111 else {
112 m.gcd(g, as[i], g);
113 }
114 }
115 if (!m.is_one(g)) {
116 for (unsigned i = 0; i < sz; i++) {
117 m.div(as[i], g, as[i]);
118 }
119 }
120
121 TRACE("linear_equation_bug",
122 tout << "g: " << m.to_string(g) << "\n";
123 for (unsigned i = 0; i < sz; i++) tout << m.to_string(as[i]) << "*x" << xs[i] << " "; tout << "\n";);
124
125 m.del(g);
126
127 unsigned obj_sz = linear_equation::get_obj_size(sz);
128 void * mem = m_allocator.allocate(obj_sz);
129 linear_equation * new_eq = new (mem) linear_equation();
130 mpz * new_as = reinterpret_cast<mpz*>(reinterpret_cast<char*>(new_eq) + sizeof(linear_equation));
131 double * new_app_as = reinterpret_cast<double*>(reinterpret_cast<char*>(new_as) + sz * sizeof(mpz));
132 var * new_xs = reinterpret_cast<var *>(reinterpret_cast<char*>(new_app_as) + sz * sizeof(double));
133 for (unsigned i = 0; i < sz; i++) {
134 new (new_as + i) mpz();
135 m.set(new_as[i], as[i]);
136 new_app_as[i] = m.get_double(as[i]);
137 var x_i = xs[i];
138 new_xs[i] = x_i;
139 }
140 new_eq->m_size = sz;
141 new_eq->m_as = new_as;
142 new_eq->m_approx_as = new_app_as;
143 new_eq->m_xs = new_xs;
144 return new_eq;
145 }
146
mk(unsigned sz,mpz * as,var * xs,bool normalized)147 linear_equation * linear_equation_manager::mk(unsigned sz, mpz * as, var * xs, bool normalized) {
148 if (!normalized) {
149 for (unsigned i = 0; i < sz; i++) {
150 var x = xs[i];
151 m_mark.reserve(x+1, false);
152 m_val_buffer.reserve(x+1);
153
154 if (m_mark[x]) {
155 m.add(m_val_buffer[x], as[i], m_val_buffer[x]);
156 }
157 else {
158 m.set(m_val_buffer[x], as[i]);
159 m_mark[x] = true;
160 }
161 }
162
163 unsigned j = 0;
164 for (unsigned i = 0; i < sz; i++) {
165 var x = xs[i];
166 if (m_mark[x]) {
167 if (!m.is_zero(m_val_buffer[x])) {
168 xs[j] = xs[i];
169 m.set(as[j], m_val_buffer[x]);
170 j++;
171 }
172 m_mark[x] = false;
173 }
174 }
175 sz = j;
176 if (sz <= 1)
177 return nullptr;
178 }
179 else {
180 DEBUG_CODE({
181 for (unsigned i = 0; i < sz; i++) {
182 var x = xs[i];
183 m_mark.reserve(x+1, false);
184 SASSERT(!m_mark[x]);
185 m_mark[x] = true;
186 }
187 for (unsigned i = 0; i < sz; i++) {
188 var x = xs[i];
189 m_mark[x] = false;
190 }
191 });
192 }
193
194 for (unsigned i = 0; i < sz; i++) {
195 var x = xs[i];
196 m_val_buffer.reserve(x+1);
197 m.swap(m_val_buffer[x], as[i]);
198 }
199 std::sort(xs, xs+sz);
200 for (unsigned i = 0; i < sz; i++) {
201 var x = xs[i];
202 m.swap(as[i], m_val_buffer[x]);
203 }
204
205 return mk_core(sz, as, xs);
206 }
207
mk(mpz const & b1,linear_equation const & eq1,mpz const & b2,linear_equation const & eq2)208 linear_equation * linear_equation_manager::mk(mpz const & b1, linear_equation const & eq1, mpz const & b2, linear_equation const & eq2) {
209 SASSERT(!m.is_zero(b1));
210 SASSERT(!m.is_zero(b2));
211 mpz tmp, new_a;
212 m_int_buffer.reset();
213 m_var_buffer.reset();
214 unsigned sz1 = eq1.size();
215 unsigned sz2 = eq2.size();
216 unsigned i1 = 0;
217 unsigned i2 = 0;
218 while (true) {
219 if (i1 == sz1) {
220 // copy remaining entries from eq2
221 while (i2 < sz2) {
222 m_int_buffer.push_back(eq2.a(i2));
223 m.mul(m_int_buffer.back(), b2, m_int_buffer.back());
224 m_var_buffer.push_back(eq2.x(i2));
225 i2++;
226 }
227 break;
228 }
229 if (i2 == sz2) {
230 // copy remaining entries from eq1
231 while (i1 < sz1) {
232 m_int_buffer.push_back(eq1.a(i1));
233 m.mul(m_int_buffer.back(), b1, m_int_buffer.back());
234 m_var_buffer.push_back(eq1.x(i1));
235 i1++;
236 }
237 break;
238 }
239 var x1 = eq1.x(i1);
240 var x2 = eq2.x(i2);
241 if (x1 < x2) {
242 m_int_buffer.push_back(eq1.a(i1));
243 m.mul(m_int_buffer.back(), b1, m_int_buffer.back());
244 m_var_buffer.push_back(eq1.x(i1));
245 i1++;
246 }
247 else if (x1 > x2) {
248 m_int_buffer.push_back(eq2.a(i2));
249 m.mul(m_int_buffer.back(), b2, m_int_buffer.back());
250 m_var_buffer.push_back(eq2.x(i2));
251 i2++;
252 }
253 else {
254 m.mul(eq1.a(i1), b1, tmp);
255 m.addmul(tmp, b2, eq2.a(i2), new_a);
256 if (!m.is_zero(new_a)) {
257 m_int_buffer.push_back(new_a);
258 m_var_buffer.push_back(eq1.x(i1));
259 }
260 i1++;
261 i2++;
262 }
263 }
264 m.del(tmp);
265 m.del(new_a);
266 SASSERT(m_int_buffer.size() == m_var_buffer.size());
267 if (m_int_buffer.empty())
268 return nullptr;
269 return mk_core(m_int_buffer.size(), m_int_buffer.data(), m_var_buffer.data());
270 }
271
del(linear_equation * eq)272 void linear_equation_manager::del(linear_equation * eq) {
273 for (unsigned i = 0; i < eq->m_size; i++) {
274 m.del(eq->m_as[i]);
275 }
276 unsigned obj_sz = linear_equation::get_obj_size(eq->m_size);
277 m_allocator.deallocate(obj_sz, eq);
278 }
279
280