Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * This implements the LinearEqualityModule.
11 : : */
12 : : #include "theory/arith/linear/linear_equality.h"
13 : :
14 : : #include "base/output.h"
15 : : #include "theory/arith/linear/constraint.h"
16 : : #include "util/statistics_registry.h"
17 : :
18 : : using namespace std;
19 : :
20 : : namespace cvc5::internal {
21 : : namespace theory {
22 : : namespace arith::linear {
23 : :
24 : : /* Explicitly instatiate these functions. */
25 : :
26 : : template ArithVar LinearEqualityModule::selectSlack<true>(
27 : : ArithVar x_i, VarPreferenceFunction pf) const;
28 : : template ArithVar LinearEqualityModule::selectSlack<false>(
29 : : ArithVar x_i, VarPreferenceFunction pf) const;
30 : :
31 : : template bool LinearEqualityModule::preferWitness<true>(
32 : : const UpdateInfo& a, const UpdateInfo& b) const;
33 : : template bool LinearEqualityModule::preferWitness<false>(
34 : : const UpdateInfo& a, const UpdateInfo& b) const;
35 : :
36 : 0 : void Border::output(std::ostream& out) const
37 : : {
38 : : out << "{Border"
39 : 0 : << ", " << d_bound->getVariable() << ", " << d_bound->getValue() << ", "
40 : 0 : << d_diff << ", " << d_areFixing << ", " << d_upperbound;
41 [ - - ]: 0 : if (ownBorder())
42 : : {
43 : 0 : out << ", ownBorder";
44 : : }
45 : : else
46 : : {
47 : 0 : out << ", " << d_entry->getCoefficient();
48 : : }
49 : 0 : out << ", " << d_bound << "}";
50 : 0 : }
51 : :
52 : 51016 : LinearEqualityModule::LinearEqualityModule(StatisticsRegistry& sr,
53 : : ArithVariables& vars,
54 : : Tableau& t,
55 : : BoundInfoMap& boundsTracking,
56 : 51016 : BasicVarModelUpdateCallBack f)
57 : 51016 : : d_variables(vars),
58 : 51016 : d_tableau(t),
59 : 51016 : d_basicVariableUpdates(f),
60 : 51016 : d_increasing(1),
61 : 51016 : d_decreasing(-1),
62 : 51016 : d_upperBoundDifference(),
63 : 51016 : d_lowerBoundDifference(),
64 : 51016 : d_one(1),
65 : 51016 : d_negOne(-1),
66 : 51016 : d_btracking(boundsTracking),
67 : 51016 : d_areTracking(false),
68 : 51016 : d_trackCallback(this),
69 : 51016 : d_statistics(sr)
70 : : {
71 : 51016 : }
72 : :
73 : 51016 : LinearEqualityModule::Statistics::Statistics(StatisticsRegistry& sr)
74 : 51016 : : d_statPivots(sr.registerInt("theory::arith::pivots")),
75 : 51016 : d_statUpdates(sr.registerInt("theory::arith::updates")),
76 : 51016 : d_pivotTime(sr.registerTimer("theory::arith::pivotTime")),
77 : 51016 : d_adjTime(sr.registerTimer("theory::arith::adjTime")),
78 : 51016 : d_weakeningAttempts(sr.registerInt("theory::arith::weakening::attempts")),
79 : 51016 : d_weakeningSuccesses(sr.registerInt("theory::arith::weakening::success")),
80 : 51016 : d_weakenings(sr.registerInt("theory::arith::weakening::total")),
81 : 51016 : d_weakenTime(sr.registerTimer("theory::arith::weakening::time")),
82 : 51016 : d_forceTime(sr.registerTimer("theory::arith::forcing::time"))
83 : : {
84 : 51016 : }
85 : :
86 : 9026703 : void LinearEqualityModule::includeBoundUpdate(ArithVar v,
87 : : const BoundsInfo& prev)
88 : : {
89 [ - + ][ - + ]: 9026703 : Assert(!d_areTracking);
[ - - ]
90 : :
91 : 9026703 : BoundsInfo curr = d_variables.boundsInfo(v);
92 : :
93 [ - + ][ - + ]: 9026703 : Assert(prev != curr);
[ - - ]
94 : 9026703 : Tableau::ColIterator basicIter = d_tableau.colIterator(v);
95 [ + + ]: 54242429 : for (; !basicIter.atEnd(); ++basicIter)
96 : : {
97 : 45215726 : const Tableau::Entry& entry = *basicIter;
98 [ - + ][ - + ]: 45215726 : Assert(entry.getColVar() == v);
[ - - ]
99 : 45215726 : int a_ijSgn = entry.getCoefficient().sgn();
100 : :
101 : 45215726 : RowIndex ridx = entry.getRowIndex();
102 : 45215726 : BoundsInfo& counts = d_btracking.get(ridx);
103 [ + - ]: 90431452 : Trace("includeBoundUpdate")
104 : 45215726 : << d_tableau.rowIndexToBasic(ridx) << " " << counts << " to ";
105 : 45215726 : counts.addInChange(a_ijSgn, prev, curr);
106 [ + - ]: 45215726 : Trace("includeBoundUpdate") << counts << " " << a_ijSgn << std::endl;
107 : : }
108 : 9026703 : }
109 : :
110 : 0 : void LinearEqualityModule::updateMany(const DenseMap<DeltaRational>& many)
111 : : {
112 : 0 : for (DenseMap<DeltaRational>::const_iterator i = many.begin(),
113 : 0 : i_end = many.end();
114 [ - - ]: 0 : i != i_end;
115 : 0 : ++i)
116 : : {
117 : 0 : ArithVar nb = *i;
118 [ - - ]: 0 : if (!d_tableau.isBasic(nb))
119 : : {
120 : 0 : Assert(!d_tableau.isBasic(nb));
121 : 0 : const DeltaRational& newValue = many[nb];
122 [ - - ]: 0 : if (newValue != d_variables.getAssignment(nb))
123 : : {
124 [ - - ]: 0 : Trace("arith::updateMany")
125 : 0 : << "updateMany:" << nb << " " << d_variables.getAssignment(nb)
126 : 0 : << " to " << newValue << endl;
127 : 0 : update(nb, newValue);
128 : : }
129 : : }
130 : : }
131 : 0 : }
132 : :
133 : 0 : void LinearEqualityModule::applySolution(
134 : : const DenseSet& newBasis, const DenseMap<DeltaRational>& newValues)
135 : : {
136 : 0 : forceNewBasis(newBasis);
137 : 0 : updateMany(newValues);
138 : 0 : }
139 : :
140 : 0 : void LinearEqualityModule::forceNewBasis(const DenseSet& newBasis)
141 : : {
142 : 0 : TimerStat::CodeTimer codeTimer(d_statistics.d_forceTime);
143 : 0 : DenseSet needsToBeAdded;
144 : 0 : for (DenseSet::const_iterator i = newBasis.begin(), i_end = newBasis.end();
145 [ - - ]: 0 : i != i_end;
146 : 0 : ++i)
147 : : {
148 : 0 : ArithVar b = *i;
149 [ - - ]: 0 : if (!d_tableau.isBasic(b))
150 : : {
151 : 0 : needsToBeAdded.add(b);
152 : : }
153 : : }
154 : :
155 [ - - ]: 0 : while (!needsToBeAdded.empty())
156 : : {
157 : 0 : ArithVar toRemove = ARITHVAR_SENTINEL;
158 : 0 : ArithVar toAdd = ARITHVAR_SENTINEL;
159 : 0 : DenseSet::const_iterator i = needsToBeAdded.begin(),
160 : 0 : i_end = needsToBeAdded.end();
161 [ - - ][ - - ]: 0 : for (; toAdd == ARITHVAR_SENTINEL && i != i_end; ++i)
[ - - ]
162 : : {
163 : 0 : ArithVar v = *i;
164 : :
165 : 0 : Tableau::ColIterator colIter = d_tableau.colIterator(v);
166 [ - - ]: 0 : for (; !colIter.atEnd(); ++colIter)
167 : : {
168 : 0 : const Tableau::Entry& entry = *colIter;
169 : 0 : Assert(entry.getColVar() == v);
170 : 0 : ArithVar b = d_tableau.rowIndexToBasic(entry.getRowIndex());
171 [ - - ]: 0 : if (!newBasis.isMember(b))
172 : : {
173 : 0 : toAdd = v;
174 : 0 : if (toRemove == ARITHVAR_SENTINEL
175 : 0 : || d_tableau.basicRowLength(toRemove)
176 [ - - ]: 0 : > d_tableau.basicRowLength(b))
177 : : {
178 : 0 : toRemove = b;
179 : : }
180 : : }
181 : : }
182 : : }
183 : 0 : Assert(toRemove != ARITHVAR_SENTINEL);
184 : 0 : Assert(toAdd != ARITHVAR_SENTINEL);
185 : :
186 [ - - ]: 0 : Trace("arith::forceNewBasis") << toRemove << " " << toAdd << endl;
187 : 0 : d_tableau.pivot(toRemove, toAdd, d_trackCallback);
188 : 0 : d_basicVariableUpdates(toAdd);
189 : :
190 [ - - ]: 0 : Trace("arith::forceNewBasis") << needsToBeAdded.size() << "to go" << endl;
191 : 0 : needsToBeAdded.remove(toAdd);
192 : : }
193 : 0 : }
194 : :
195 : 305673 : void LinearEqualityModule::updateUntracked(ArithVar x_i, const DeltaRational& v)
196 : : {
197 [ - + ][ - + ]: 305673 : Assert(!d_tableau.isBasic(x_i));
[ - - ]
198 [ - + ][ - + ]: 305673 : Assert(!d_areTracking);
[ - - ]
199 : 305673 : const DeltaRational& assignment_x_i = d_variables.getAssignment(x_i);
200 : 305673 : ++(d_statistics.d_statUpdates);
201 : :
202 [ + - ]: 611346 : Trace("arith") << "update " << x_i << ": " << assignment_x_i << "|-> " << v
203 : 305673 : << endl;
204 : 305673 : DeltaRational diff = v - assignment_x_i;
205 : :
206 : 305673 : Tableau::ColIterator colIter = d_tableau.colIterator(x_i);
207 [ + + ]: 3314178 : for (; !colIter.atEnd(); ++colIter)
208 : : {
209 : 3008505 : const Tableau::Entry& entry = *colIter;
210 [ - + ][ - + ]: 3008505 : Assert(entry.getColVar() == x_i);
[ - - ]
211 : :
212 : 3008505 : ArithVar x_j = d_tableau.rowIndexToBasic(entry.getRowIndex());
213 : 3008505 : const Rational& a_ji = entry.getCoefficient();
214 : :
215 : 3008505 : const DeltaRational& assignment = d_variables.getAssignment(x_j);
216 : 3008505 : DeltaRational nAssignment = assignment + (diff * a_ji);
217 : 3008505 : d_variables.setAssignment(x_j, nAssignment);
218 : :
219 : 3008505 : d_basicVariableUpdates(x_j);
220 : 3008505 : }
221 : :
222 : 305673 : d_variables.setAssignment(x_i, v);
223 : :
224 [ - + ]: 305673 : if (TraceIsOn("paranoid:check_tableau"))
225 : : {
226 : 0 : debugCheckTableau();
227 : : }
228 : 305673 : }
229 : :
230 : 341437 : void LinearEqualityModule::updateTracked(ArithVar x_i, const DeltaRational& v)
231 : : {
232 : 341437 : TimerStat::CodeTimer codeTimer(d_statistics.d_adjTime);
233 : :
234 [ - + ][ - + ]: 341437 : Assert(!d_tableau.isBasic(x_i));
[ - - ]
235 [ - + ][ - + ]: 341437 : Assert(d_areTracking);
[ - - ]
236 : :
237 : 341437 : ++(d_statistics.d_statUpdates);
238 : :
239 : 341437 : DeltaRational diff = v - d_variables.getAssignment(x_i);
240 [ + - ]: 682874 : Trace("arith") << "update " << x_i << ": " << d_variables.getAssignment(x_i)
241 : 341437 : << "|-> " << v << endl;
242 : :
243 : 341437 : BoundCounts before = d_variables.atBoundCounts(x_i);
244 : 341437 : d_variables.setAssignment(x_i, v);
245 : 341437 : BoundCounts after = d_variables.atBoundCounts(x_i);
246 : :
247 : 341437 : bool anyChange = before != after;
248 : :
249 : 341437 : Tableau::ColIterator colIter = d_tableau.colIterator(x_i);
250 [ + + ]: 6960642 : for (; !colIter.atEnd(); ++colIter)
251 : : {
252 : 6619205 : const Tableau::Entry& entry = *colIter;
253 [ - + ][ - + ]: 6619205 : Assert(entry.getColVar() == x_i);
[ - - ]
254 : :
255 : 6619205 : RowIndex ridx = entry.getRowIndex();
256 : 6619205 : ArithVar x_j = d_tableau.rowIndexToBasic(ridx);
257 : 6619205 : const Rational& a_ji = entry.getCoefficient();
258 : :
259 : 6619205 : const DeltaRational& assignment = d_variables.getAssignment(x_j);
260 : 6619205 : DeltaRational nAssignment = assignment + (diff * a_ji);
261 [ + - ]: 13238410 : Trace("update") << x_j << " " << a_ji << assignment << " -> " << nAssignment
262 : 6619205 : << endl;
263 : 6619205 : BoundCounts xjBefore = d_variables.atBoundCounts(x_j);
264 : 6619205 : d_variables.setAssignment(x_j, nAssignment);
265 : 6619205 : BoundCounts xjAfter = d_variables.atBoundCounts(x_j);
266 : :
267 [ - + ][ - + ]: 6619205 : Assert(rowIndexIsTracked(ridx));
[ - - ]
268 : 6619205 : BoundsInfo& next_bc_k = d_btracking.get(ridx);
269 [ + + ]: 6619205 : if (anyChange)
270 : : {
271 : 4561076 : next_bc_k.addInAtBoundChange(a_ji.sgn(), before, after);
272 : : }
273 [ + + ]: 6619205 : if (xjBefore != xjAfter)
274 : : {
275 : 816702 : next_bc_k.addInAtBoundChange(-1, xjBefore, xjAfter);
276 : : }
277 : :
278 : 6619205 : d_basicVariableUpdates(x_j);
279 : 6619205 : }
280 : :
281 [ - + ]: 341437 : if (TraceIsOn("paranoid:check_tableau"))
282 : : {
283 : 0 : debugCheckTableau();
284 : : }
285 : 341437 : }
286 : :
287 : 341292 : void LinearEqualityModule::pivotAndUpdate(ArithVar x_i,
288 : : ArithVar x_j,
289 : : const DeltaRational& x_i_value)
290 : : {
291 [ - + ][ - + ]: 341292 : Assert(x_i != x_j);
[ - - ]
292 : :
293 : 341292 : TimerStat::CodeTimer codeTimer(d_statistics.d_pivotTime);
294 : :
295 [ - + ]: 341292 : if (TraceIsOn("arith::tracking::pre"))
296 : : {
297 [ - - ]: 0 : Trace("arith::tracking") << "pre update" << endl;
298 : 0 : debugCheckTracking();
299 : : }
300 : :
301 [ - + ]: 341292 : if (TraceIsOn("arith::simplex:row"))
302 : : {
303 : 0 : debugPivot(x_i, x_j);
304 : : }
305 : :
306 : 341292 : RowIndex ridx = d_tableau.basicToRowIndex(x_i);
307 : 341292 : const Tableau::Entry& entry_ij = d_tableau.findEntry(ridx, x_j);
308 [ - + ][ - + ]: 341292 : Assert(!entry_ij.blank());
[ - - ]
309 : :
310 : 341292 : const Rational& a_ij = entry_ij.getCoefficient();
311 : 341292 : const DeltaRational& betaX_i = d_variables.getAssignment(x_i);
312 : 341292 : DeltaRational theta = (x_i_value - betaX_i) / a_ij;
313 : 341292 : DeltaRational x_j_value = d_variables.getAssignment(x_j) + theta;
314 : :
315 : 341292 : updateTracked(x_j, x_j_value);
316 : :
317 [ - + ]: 341292 : if (TraceIsOn("arith::tracking::mid"))
318 : : {
319 [ - - ]: 0 : Trace("arith::tracking") << "postupdate prepivot" << endl;
320 : 0 : debugCheckTracking();
321 : : }
322 : :
323 : : // Pivots
324 : 341292 : ++(d_statistics.d_statPivots);
325 : :
326 : 341292 : d_tableau.pivot(x_i, x_j, d_trackCallback);
327 : :
328 [ - + ]: 341292 : if (TraceIsOn("arith::tracking::post"))
329 : : {
330 [ - - ]: 0 : Trace("arith::tracking") << "postpivot" << endl;
331 : 0 : debugCheckTracking();
332 : : }
333 : :
334 : 341292 : d_basicVariableUpdates(x_j);
335 : :
336 [ - + ]: 341292 : if (TraceIsOn("matrix"))
337 : : {
338 : 0 : d_tableau.printMatrix();
339 : : }
340 : 341292 : }
341 : :
342 : 108256 : uint32_t LinearEqualityModule::updateProduct(const UpdateInfo& inf) const
343 : : {
344 : 108256 : uint32_t colLen = d_tableau.getColLength(inf.nonbasic());
345 [ + + ]: 108256 : if (inf.describesPivot())
346 : : {
347 [ - + ][ - + ]: 106696 : Assert(inf.leaving() != inf.nonbasic());
[ - - ]
348 : 106696 : return colLen + d_tableau.basicRowLength(inf.leaving());
349 : : }
350 : : else
351 : : {
352 : 1560 : return colLen;
353 : : }
354 : : }
355 : :
356 : 0 : void LinearEqualityModule::debugCheckTracking()
357 : : {
358 : 0 : Tableau::BasicIterator basicIter = d_tableau.beginBasic(),
359 : 0 : endIter = d_tableau.endBasic();
360 [ - - ]: 0 : for (; basicIter != endIter; ++basicIter)
361 : : {
362 : 0 : ArithVar basic = *basicIter;
363 [ - - ]: 0 : Trace("arith::tracking") << "arith::tracking row basic: " << basic << endl;
364 : :
365 : 0 : for (Tableau::RowIterator iter = d_tableau.basicRowIterator(basic);
366 : 0 : !iter.atEnd() && TraceIsOn("arith::tracking");
367 : 0 : ++iter)
368 : : {
369 : 0 : const Tableau::Entry& entry = *iter;
370 : :
371 : 0 : ArithVar var = entry.getColVar();
372 : 0 : const Rational& coeff = entry.getCoefficient();
373 : 0 : DeltaRational beta = d_variables.getAssignment(var);
374 [ - - ]: 0 : Trace("arith::tracking")
375 : 0 : << var << " " << d_variables.boundsInfo(var) << " " << beta << coeff;
376 [ - - ]: 0 : if (d_variables.hasLowerBound(var))
377 : : {
378 [ - - ]: 0 : Trace("arith::tracking")
379 : 0 : << "(lb " << d_variables.getLowerBound(var) << ")";
380 : : }
381 [ - - ]: 0 : if (d_variables.hasUpperBound(var))
382 : : {
383 [ - - ]: 0 : Trace("arith::tracking")
384 : 0 : << "(up " << d_variables.getUpperBound(var) << ")";
385 : : }
386 [ - - ]: 0 : Trace("arith::tracking") << endl;
387 : 0 : }
388 [ - - ]: 0 : Trace("arith::tracking") << "end row" << endl;
389 : :
390 [ - - ]: 0 : if (basicIsTracked(basic))
391 : : {
392 : 0 : RowIndex ridx = d_tableau.basicToRowIndex(basic);
393 : 0 : BoundsInfo computed = computeRowBoundInfo(ridx, false);
394 [ - - ]: 0 : Trace("arith::tracking") << "computed " << computed << " tracking "
395 : 0 : << d_btracking[ridx] << endl;
396 : 0 : Assert(computed == d_btracking[ridx]);
397 : : }
398 : : }
399 : 0 : }
400 : :
401 : 0 : void LinearEqualityModule::debugPivot(ArithVar x_i, ArithVar x_j)
402 : : {
403 [ - - ]: 0 : Trace("arith::pivot") << "debugPivot(" << x_i << "|->" << x_j << ")" << endl;
404 : :
405 : 0 : for (Tableau::RowIterator iter = d_tableau.basicRowIterator(x_i);
406 [ - - ]: 0 : !iter.atEnd();
407 : 0 : ++iter)
408 : : {
409 : 0 : const Tableau::Entry& entry = *iter;
410 : :
411 : 0 : ArithVar var = entry.getColVar();
412 : 0 : const Rational& coeff = entry.getCoefficient();
413 : 0 : DeltaRational beta = d_variables.getAssignment(var);
414 [ - - ]: 0 : Trace("arith::pivot") << var << beta << coeff;
415 [ - - ]: 0 : if (d_variables.hasLowerBound(var))
416 : : {
417 [ - - ]: 0 : Trace("arith::pivot") << "(lb " << d_variables.getLowerBound(var) << ")";
418 : : }
419 [ - - ]: 0 : if (d_variables.hasUpperBound(var))
420 : : {
421 [ - - ]: 0 : Trace("arith::pivot") << "(up " << d_variables.getUpperBound(var) << ")";
422 : : }
423 [ - - ]: 0 : Trace("arith::pivot") << endl;
424 : 0 : }
425 [ - - ]: 0 : Trace("arith::pivot") << "end row" << endl;
426 : 0 : }
427 : :
428 : : /**
429 : : * This check is quite expensive.
430 : : * It should be wrapped in a TraceIsOn() guard.
431 : : * if(TraceIsOn("paranoid:check_tableau")){
432 : : * checkTableau();
433 : : * }
434 : : */
435 : 0 : void LinearEqualityModule::debugCheckTableau()
436 : : {
437 : 0 : Tableau::BasicIterator basicIter = d_tableau.beginBasic(),
438 : 0 : endIter = d_tableau.endBasic();
439 [ - - ]: 0 : for (; basicIter != endIter; ++basicIter)
440 : : {
441 : 0 : ArithVar basic = *basicIter;
442 : 0 : DeltaRational sum;
443 [ - - ]: 0 : Trace("paranoid:check_tableau") << "starting row" << basic << endl;
444 : 0 : Tableau::RowIterator nonbasicIter = d_tableau.basicRowIterator(basic);
445 [ - - ]: 0 : for (; !nonbasicIter.atEnd(); ++nonbasicIter)
446 : : {
447 : 0 : const Tableau::Entry& entry = *nonbasicIter;
448 : 0 : ArithVar nonbasic = entry.getColVar();
449 [ - - ]: 0 : if (basic == nonbasic) continue;
450 : :
451 : 0 : const Rational& coeff = entry.getCoefficient();
452 : 0 : DeltaRational beta = d_variables.getAssignment(nonbasic);
453 [ - - ]: 0 : Trace("paranoid:check_tableau") << nonbasic << beta << coeff << endl;
454 : 0 : sum = sum + (beta * coeff);
455 : 0 : }
456 : 0 : DeltaRational shouldBe = d_variables.getAssignment(basic);
457 [ - - ]: 0 : Trace("paranoid:check_tableau")
458 : 0 : << "ending row" << sum << "," << shouldBe << endl;
459 : :
460 : 0 : Assert(sum == shouldBe);
461 : 0 : }
462 : 0 : }
463 : :
464 : 813028 : DeltaRational LinearEqualityModule::computeRowBound(RowIndex ridx,
465 : : bool rowUb,
466 : : ArithVar skip) const
467 : : {
468 : 1626056 : DeltaRational sum(0, 0);
469 [ + + ]: 5426419 : for (Tableau::RowIterator i = d_tableau.ridRowIterator(ridx); !i.atEnd(); ++i)
470 : : {
471 : 4613391 : const Tableau::Entry& entry = (*i);
472 : 4613391 : ArithVar v = entry.getColVar();
473 [ + + ]: 4613391 : if (v == skip)
474 : : {
475 : 600763 : continue;
476 : : }
477 : :
478 : 4012628 : const Rational& coeff = entry.getCoefficient();
479 : 4012628 : bool vUb = (rowUb == (coeff.sgn() > 0));
480 : :
481 : : const DeltaRational& bound =
482 [ + + ]: 4012628 : vUb ? d_variables.getUpperBound(v) : d_variables.getLowerBound(v);
483 : :
484 : 4012628 : DeltaRational diff = bound * coeff;
485 : 4012628 : sum = sum + diff;
486 : 4012628 : }
487 : 813028 : return sum;
488 : 0 : }
489 : :
490 : : /**
491 : : * Computes the value of a basic variable using the current assignment.
492 : : */
493 : 398398 : DeltaRational LinearEqualityModule::computeRowValue(ArithVar x,
494 : : bool useSafe) const
495 : : {
496 [ - + ][ - + ]: 398398 : Assert(d_tableau.isBasic(x));
[ - - ]
497 : 398398 : DeltaRational sum(0);
498 : :
499 [ + + ]: 2378714 : for (Tableau::RowIterator i = d_tableau.basicRowIterator(x); !i.atEnd(); ++i)
500 : : {
501 : 1980316 : const Tableau::Entry& entry = (*i);
502 : 1980316 : ArithVar nonbasic = entry.getColVar();
503 [ + + ]: 1980316 : if (nonbasic == x) continue;
504 : 1581918 : const Rational& coeff = entry.getCoefficient();
505 : :
506 : : const DeltaRational& assignment =
507 : 1581918 : d_variables.getAssignment(nonbasic, useSafe);
508 : 1581918 : sum = sum + (assignment * coeff);
509 : : }
510 : 398398 : return sum;
511 : 0 : }
512 : :
513 : 7945179 : const Tableau::Entry* LinearEqualityModule::rowLacksBound(RowIndex ridx,
514 : : bool rowUb,
515 : : ArithVar skip)
516 : : {
517 : 7945179 : Tableau::RowIterator iter = d_tableau.ridRowIterator(ridx);
518 [ + + ]: 42228659 : for (; !iter.atEnd(); ++iter)
519 : : {
520 : 42228051 : const Tableau::Entry& entry = *iter;
521 : :
522 : 42228051 : ArithVar var = entry.getColVar();
523 [ + + ]: 42228051 : if (var == skip)
524 : : {
525 : 906 : continue;
526 : : }
527 : :
528 : 42227145 : int sgn = entry.getCoefficient().sgn();
529 : 42227145 : bool selectUb = (rowUb == (sgn > 0));
530 [ + + ]: 42227145 : bool hasBound = selectUb ? d_variables.hasUpperBound(var)
531 : 20832814 : : d_variables.hasLowerBound(var);
532 [ + + ]: 42227145 : if (!hasBound)
533 : : {
534 : 7944571 : return &entry;
535 : : }
536 : : }
537 : 608 : return nullptr;
538 : : }
539 : :
540 : 106 : void LinearEqualityModule::propagateBasicFromRow(NodeManager* nm,
541 : : ConstraintP c,
542 : : bool produceProofs)
543 : : {
544 [ - + ][ - + ]: 106 : Assert(c != NullConstraint);
[ - - ]
545 [ + + ][ + - ]: 106 : Assert(c->isUpperBound() || c->isLowerBound());
[ - + ][ - + ]
[ - - ]
546 [ - + ][ - + ]: 106 : Assert(!c->assertedToTheTheory());
[ - - ]
547 [ - + ][ - + ]: 106 : Assert(!c->hasProof());
[ - - ]
548 : :
549 : 106 : bool upperBound = c->isUpperBound();
550 : 106 : ArithVar basic = c->getVariable();
551 : 106 : RowIndex ridx = d_tableau.basicToRowIndex(basic);
552 : :
553 : 106 : ConstraintCPVec bounds;
554 [ - + ]: 106 : RationalVectorP coeffs = produceProofs ? new RationalVector() : nullptr;
555 : 106 : propagateRow(bounds, ridx, upperBound, c, coeffs);
556 : 106 : c->impliedByFarkas(nm, bounds, coeffs, false);
557 : 106 : c->tryToPropagate();
558 : :
559 [ - + ]: 106 : if (coeffs != RationalVectorPSentinel)
560 : : {
561 [ - - ]: 0 : delete coeffs;
562 : : }
563 : 106 : }
564 : :
565 : : /* An explanation of the farkas coefficients.
566 : : *
567 : : * We are proving c using the other variables on the row.
568 : : * The proof is in terms of the other constraints and the negation of c, ~c.
569 : : *
570 : : * A row has the form:
571 : : * sum a_i * x_i = 0
572 : : * or
573 : : * sx + sum r y + sum q z = 0
574 : : * where r > 0 and q < 0.
575 : : *
576 : : * If rowUp, we are proving c
577 : : * g = sum r u_y + sum q l_z
578 : : * and c is entailed by -sx <= g
579 : : * If !rowUp, we are proving c
580 : : * g = sum r l_y + sum q u_z
581 : : * and c is entailed by -sx >= g
582 : : *
583 : : * | s | c | ~c | u_i | l_i
584 : : * if rowUp | s > 0 | x >= -g/s | x < -g/s | a_i > 0 | a_i < 0
585 : : * if rowUp | s < 0 | x <= -g/s | x > -g/s | a_i > 0 | a_i < 0
586 : : * if !rowUp | s > 0 | x <= -g/s | x > -g/s | a_i < 0 | a_i > 0
587 : : * if !rowUp | s < 0 | x >= -g/s | x < -g/s | a_i < 0 | a_i > 0
588 : : *
589 : : *
590 : : * Thus we treat !rowUp as multiplying the row by -1 and rowUp as 1
591 : : * for the entire row.
592 : : */
593 : 232985 : void LinearEqualityModule::propagateRow(ConstraintCPVec& into,
594 : : RowIndex ridx,
595 : : bool rowUp,
596 : : ConstraintP c,
597 : : RationalVectorP farkas)
598 : : {
599 [ - + ][ - + ]: 232985 : Assert(!c->assertedToTheTheory());
[ - - ]
600 [ - + ][ - + ]: 232985 : Assert(c->canBePropagated());
[ - - ]
601 [ - + ][ - + ]: 232985 : Assert(!c->hasProof());
[ - - ]
602 : :
603 [ + + ]: 232985 : if (farkas != RationalVectorPSentinel)
604 : : {
605 [ - + ][ - + ]: 157701 : Assert(farkas->empty());
[ - - ]
606 : 157701 : farkas->push_back(Rational(0));
607 : : }
608 : :
609 : 232985 : ArithVar v = c->getVariable();
610 [ + - ]: 465970 : Trace("arith::propagateRow")
611 : 0 : << "LinearEqualityModule::propagateRow(" << ridx << ", " << rowUp << ", "
612 : 232985 : << v << ") start" << endl;
613 : :
614 [ + + ]: 232985 : const Rational& multiple = rowUp ? d_one : d_negOne;
615 : :
616 [ + - ]: 232985 : Trace("arith::propagateRow") << "multiple: " << multiple << endl;
617 : :
618 : 232985 : Tableau::RowIterator iter = d_tableau.ridRowIterator(ridx);
619 [ + + ]: 1844219 : for (; !iter.atEnd(); ++iter)
620 : : {
621 : 1611234 : const Tableau::Entry& entry = *iter;
622 : 1611234 : ArithVar nonbasic = entry.getColVar();
623 : 1611234 : const Rational& a_ij = entry.getCoefficient();
624 : 1611234 : int sgn = a_ij.sgn();
625 [ - + ][ - + ]: 1611234 : Assert(sgn != 0);
[ - - ]
626 [ + + ]: 1611234 : bool selectUb = rowUp ? (sgn > 0) : (sgn < 0);
627 : :
628 [ + + ][ + + ]: 1611234 : Assert(nonbasic != v || (rowUp && a_ij.sgn() > 0 && c->isLowerBound())
[ + + ][ + + ]
[ + - ][ + + ]
[ + + ][ + + ]
[ + - ][ + + ]
[ + - ][ + + ]
[ + + ][ + - ]
[ + + ][ + + ]
[ + - ][ + + ]
[ + + ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ - + ][ - + ]
[ - - ]
629 : : || (rowUp && a_ij.sgn() < 0 && c->isUpperBound())
630 : : || (!rowUp && a_ij.sgn() > 0 && c->isUpperBound())
631 : : || (!rowUp && a_ij.sgn() < 0 && c->isLowerBound()));
632 : :
633 [ - + ]: 1611234 : if (TraceIsOn("arith::propagateRow"))
634 : : {
635 [ - - ]: 0 : if (nonbasic == v)
636 : : {
637 [ - - ]: 0 : Trace("arith::propagateRow")
638 : 0 : << "(target) " << rowUp << " " << a_ij.sgn() << " "
639 : 0 : << c->isLowerBound() << " " << c->isUpperBound() << endl;
640 : :
641 [ - - ]: 0 : Trace("arith::propagateRow") << "(target) ";
642 : : }
643 [ - - ]: 0 : Trace("arith::propagateRow")
644 : 0 : << "propagateRow " << a_ij << " * " << nonbasic;
645 : : }
646 : :
647 [ + + ]: 1611234 : if (nonbasic == v)
648 : : {
649 [ + + ]: 232985 : if (farkas != RationalVectorPSentinel)
650 : : {
651 [ - + ][ - + ]: 157701 : Assert(farkas->front().isZero());
[ - - ]
652 : 157701 : Rational multAij = multiple * a_ij;
653 [ + - ]: 157701 : Trace("arith::propagateRow") << "(" << multAij << ") ";
654 : 157701 : farkas->front() = multAij;
655 : 157701 : }
656 : :
657 [ + - ]: 232985 : Trace("arith::propagateRow") << c << endl;
658 : : }
659 : : else
660 : : {
661 : : ConstraintCP bound = selectUb
662 : 647567 : ? d_variables.getUpperBoundConstraint(nonbasic)
663 [ + + ]: 1378249 : : d_variables.getLowerBoundConstraint(nonbasic);
664 : :
665 [ + + ]: 1378249 : if (farkas != RationalVectorPSentinel)
666 : : {
667 : 937118 : Rational multAij = multiple * a_ij;
668 [ + - ]: 937118 : Trace("arith::propagateRow") << "(" << multAij << ") ";
669 : 937118 : farkas->push_back(multAij);
670 : 937118 : }
671 [ - + ][ - + ]: 1378249 : Assert(bound != NullConstraint);
[ - - ]
672 [ + - ]: 1378249 : Trace("arith::propagateRow") << bound << endl;
673 : 1378249 : into.push_back(bound);
674 : : }
675 : : }
676 [ + - ]: 465970 : Trace("arith::propagateRow")
677 : 0 : << "LinearEqualityModule::propagateRow(" << ridx << ", " << rowUp << ", "
678 : 232985 : << v << ") done" << endl;
679 : 232985 : }
680 : :
681 : 1158800 : ConstraintP LinearEqualityModule::weakestExplanation(bool aboveUpper,
682 : : DeltaRational& surplus,
683 : : ArithVar v,
684 : : const Rational& coeff,
685 : : bool& anyWeakening,
686 : : ArithVar basic) const
687 : : {
688 : 1158800 : int sgn = coeff.sgn();
689 [ + + ]: 1158800 : bool ub = aboveUpper ? (sgn < 0) : (sgn > 0);
690 : :
691 [ + + ]: 1158800 : ConstraintP c = ub ? d_variables.getUpperBoundConstraint(v)
692 : 1158800 : : d_variables.getLowerBoundConstraint(v);
693 : :
694 : : bool weakened;
695 [ + + ]: 1339023 : do
696 : : {
697 : 1339023 : const DeltaRational& bound = c->getValue();
698 : :
699 : 1339023 : weakened = false;
700 : :
701 [ + + ]: 1339023 : ConstraintP weaker = ub ? c->getStrictlyWeakerUpperBound(true, true)
702 : 793222 : : c->getStrictlyWeakerLowerBound(true, true);
703 : :
704 [ + + ]: 1339023 : if (weaker != NullConstraint)
705 : : {
706 : 356114 : const DeltaRational& weakerBound = weaker->getValue();
707 : :
708 : : DeltaRational diff =
709 [ + + ]: 356114 : aboveUpper ? bound - weakerBound : weakerBound - bound;
710 : : // if var == basic,
711 : : // if aboveUpper, weakerBound > bound, multiply by -1
712 : : // if !aboveUpper, weakerBound < bound, multiply by -1
713 : 356114 : diff = diff * coeff;
714 [ + + ]: 356114 : if (surplus > diff)
715 : : {
716 : 180223 : ++d_statistics.d_weakenings;
717 : 180223 : weakened = true;
718 : 180223 : anyWeakening = true;
719 : 180223 : surplus = surplus - diff;
720 : :
721 [ + - ]: 180223 : Trace("arith::weak") << "found:" << endl;
722 [ + + ]: 180223 : if (v == basic)
723 : : {
724 [ + - ]: 17705 : Trace("arith::weak") << " basic: ";
725 : : }
726 [ + - ]: 360446 : Trace("arith::weak") << " " << surplus << " " << diff << endl
727 : 0 : << " " << bound << c << endl
728 : 180223 : << " " << weakerBound << weaker << endl;
729 : :
730 [ - + ][ - + ]: 180223 : Assert(diff.sgn() > 0);
[ - - ]
731 : 180223 : c = weaker;
732 : : }
733 : 356114 : }
734 : : } while (weakened);
735 : :
736 : 1158800 : return c;
737 : : }
738 : :
739 : : /* An explanation of the farkas coefficients.
740 : : *
741 : : * We are proving a conflict on the basic variable x_b.
742 : : * If aboveUpper, then the conflict is with the constraint c : x_b <= u_b.
743 : : * If !aboveUpper, then the conflict is with the constraint c : x_b >= l_b.
744 : : *
745 : : * A row has the form:
746 : : * -x_b sum a_i * x_i = 0
747 : : * or
748 : : * -x_b + sum r y + sum q z = 0,
749 : : * x_b = sum r y + sum q z
750 : : * where r > 0 and q < 0.
751 : : *
752 : : *
753 : : * If !aboveUp, we are proving ~c: x_b < l_b
754 : : * g = sum r u_y + sum q l_z
755 : : * x_b <= g < l_b
756 : : * and ~c is entailed by x_b <= g
757 : : *
758 : : * If aboveUp, we are proving ~c : x_b > u_b
759 : : * g = sum r l_y + sum q u_z
760 : : * x_b >= g > u_b
761 : : * and ~c is entailed by x_b >= g
762 : : *
763 : : *
764 : : * | s | c | ~c | u_i | l_i
765 : : * if !aboveUp | s > 0 | x >= -g/s | x < -g/s | a_i > 0 | a_i < 0
766 : : * if !aboveUp | s < 0 | x <= -g/s | x > -g/s | a_i > 0 | a_i < 0
767 : : * if aboveUp | s > 0 | x <= -g/s | x > -g/s | a_i < 0 | a_i > 0
768 : : * if aboveUp | s < 0 | x >= -g/s | x < -g/s | a_i < 0 | a_i > 0
769 : : *
770 : : * Thus we treat aboveUp as multiplying the row by -1 and !aboveUp as 1
771 : : * for the entire row.
772 : : */
773 : 104031 : ConstraintCP LinearEqualityModule::minimallyWeakConflict(
774 : : NodeManager* nm,
775 : : bool aboveUpper,
776 : : ArithVar basicVar,
777 : : FarkasConflictBuilder& fcs) const
778 : : {
779 [ - + ][ - + ]: 104031 : Assert(!fcs.underConstruction());
[ - - ]
780 : 104031 : TimerStat::CodeTimer codeTimer(d_statistics.d_weakenTime);
781 : :
782 [ + - ]: 208062 : Trace("arith::weak") << "LinearEqualityModule::minimallyWeakConflict("
783 : 0 : << aboveUpper << ", " << basicVar << ", ...) start"
784 : 104031 : << endl;
785 : :
786 [ + + ]: 104031 : const Rational& adjustSgn = aboveUpper ? d_negOne : d_one;
787 : 104031 : const DeltaRational& assignment = d_variables.getAssignment(basicVar);
788 : 104031 : DeltaRational surplus;
789 [ + + ]: 104031 : if (aboveUpper)
790 : : {
791 [ - + ][ - + ]: 50328 : Assert(d_variables.hasUpperBound(basicVar));
[ - - ]
792 [ - + ][ - + ]: 50328 : Assert(assignment > d_variables.getUpperBound(basicVar));
[ - - ]
793 : 50328 : surplus = assignment - d_variables.getUpperBound(basicVar);
794 : : }
795 : : else
796 : : {
797 [ - + ][ - + ]: 53703 : Assert(d_variables.hasLowerBound(basicVar));
[ - - ]
798 [ - + ][ - + ]: 53703 : Assert(assignment < d_variables.getLowerBound(basicVar));
[ - - ]
799 : 53703 : surplus = d_variables.getLowerBound(basicVar) - assignment;
800 : : }
801 : :
802 : 104031 : bool anyWeakenings = false;
803 : 104031 : for (Tableau::RowIterator i = d_tableau.basicRowIterator(basicVar);
804 [ + + ]: 1262831 : !i.atEnd();
805 : 1158800 : ++i)
806 : : {
807 : 1158800 : const Tableau::Entry& entry = *i;
808 : 1158800 : ArithVar v = entry.getColVar();
809 : 1158800 : const Rational& coeff = entry.getCoefficient();
810 : 1158800 : bool weakening = false;
811 : : ConstraintP c =
812 : 1158800 : weakestExplanation(aboveUpper, surplus, v, coeff, weakening, basicVar);
813 [ + - ]: 2317600 : Trace("arith::weak") << "weak : " << weakening << " "
814 : 1158800 : << c->assertedToTheTheory() << " "
815 : 1158800 : << d_variables.getAssignment(v) << " " << c << endl;
816 [ + + ][ + + ]: 1158800 : anyWeakenings = anyWeakenings || weakening;
817 : :
818 : 1158800 : fcs.addConstraint(c, coeff, adjustSgn);
819 [ + + ]: 1158800 : if (basicVar == v)
820 : : {
821 [ - + ][ - + ]: 104031 : Assert(!c->negationHasProof());
[ - - ]
822 : 104031 : fcs.makeLastConsequent();
823 : : }
824 : : }
825 [ - + ][ - + ]: 104031 : Assert(fcs.consequentIsSet());
[ - - ]
826 : :
827 : 104031 : ConstraintCP conflicted = fcs.commitConflict(nm);
828 : :
829 : 104031 : ++d_statistics.d_weakeningAttempts;
830 [ + + ]: 104031 : if (anyWeakenings)
831 : : {
832 : 81577 : ++d_statistics.d_weakeningSuccesses;
833 : : }
834 [ + - ]: 208062 : Trace("arith::weak") << "LinearEqualityModule::minimallyWeakConflict("
835 : 0 : << aboveUpper << ", " << basicVar << ", ...) done"
836 : 104031 : << endl;
837 : 104031 : return conflicted;
838 : 104031 : }
839 : :
840 : 154058 : ArithVar LinearEqualityModule::minVarOrder(ArithVar x, ArithVar y) const
841 : : {
842 [ - + ][ - + ]: 154058 : Assert(x != ARITHVAR_SENTINEL);
[ - - ]
843 [ - + ][ - + ]: 154058 : Assert(y != ARITHVAR_SENTINEL);
[ - - ]
844 [ + + ]: 154058 : if (x <= y)
845 : : {
846 : 90144 : return x;
847 : : }
848 : : else
849 : : {
850 : 63914 : return y;
851 : : }
852 : : }
853 : :
854 : 983055 : ArithVar LinearEqualityModule::minColLength(ArithVar x, ArithVar y) const
855 : : {
856 [ - + ][ - + ]: 983055 : Assert(x != ARITHVAR_SENTINEL);
[ - - ]
857 [ - + ][ - + ]: 983055 : Assert(y != ARITHVAR_SENTINEL);
[ - - ]
858 [ - + ][ - + ]: 983055 : Assert(!d_tableau.isBasic(x));
[ - - ]
859 [ - + ][ - + ]: 983055 : Assert(!d_tableau.isBasic(y));
[ - - ]
860 : 983055 : uint32_t xLen = d_tableau.getColLength(x);
861 : 983055 : uint32_t yLen = d_tableau.getColLength(y);
862 [ + + ]: 983055 : if (xLen > yLen)
863 : : {
864 : 180908 : return y;
865 : : }
866 [ + + ]: 802147 : else if (xLen == yLen)
867 : : {
868 : 152736 : return minVarOrder(x, y);
869 : : }
870 : : else
871 : : {
872 : 649411 : return x;
873 : : }
874 : : }
875 : :
876 : 0 : ArithVar LinearEqualityModule::minRowLength(ArithVar x, ArithVar y) const
877 : : {
878 : 0 : Assert(x != ARITHVAR_SENTINEL);
879 : 0 : Assert(y != ARITHVAR_SENTINEL);
880 : 0 : Assert(d_tableau.isBasic(x));
881 : 0 : Assert(d_tableau.isBasic(y));
882 : 0 : uint32_t xLen = d_tableau.basicRowLength(x);
883 : 0 : uint32_t yLen = d_tableau.basicRowLength(y);
884 [ - - ]: 0 : if (xLen > yLen)
885 : : {
886 : 0 : return y;
887 : : }
888 [ - - ]: 0 : else if (xLen == yLen)
889 : : {
890 : 0 : return minVarOrder(x, y);
891 : : }
892 : : else
893 : : {
894 : 0 : return x;
895 : : }
896 : : }
897 : :
898 : 1061906 : ArithVar LinearEqualityModule::minBoundAndColLength(ArithVar x,
899 : : ArithVar y) const
900 : : {
901 [ - + ][ - + ]: 1061906 : Assert(x != ARITHVAR_SENTINEL);
[ - - ]
902 [ - + ][ - + ]: 1061906 : Assert(y != ARITHVAR_SENTINEL);
[ - - ]
903 [ - + ][ - + ]: 1061906 : Assert(!d_tableau.isBasic(x));
[ - - ]
904 [ - + ][ - + ]: 1061906 : Assert(!d_tableau.isBasic(y));
[ - - ]
905 [ + + ][ + + ]: 1061906 : if (d_variables.hasEitherBound(x) && !d_variables.hasEitherBound(y))
[ + + ]
906 : : {
907 : 33173 : return y;
908 : : }
909 [ + + ][ + + ]: 1028733 : else if (!d_variables.hasEitherBound(x) && d_variables.hasEitherBound(y))
[ + + ]
910 : : {
911 : 45678 : return x;
912 : : }
913 : : else
914 : : {
915 : 983055 : return minColLength(x, y);
916 : : }
917 : : }
918 : :
919 : : template <bool above>
920 : 333513 : ArithVar LinearEqualityModule::selectSlack(ArithVar x_i,
921 : : VarPreferenceFunction pref) const
922 : : {
923 : 333513 : ArithVar slack = ARITHVAR_SENTINEL;
924 : :
925 : 333513 : for (Tableau::RowIterator iter = d_tableau.basicRowIterator(x_i);
926 [ + + ]: 6082196 : !iter.atEnd();
927 : 5748683 : ++iter)
928 : : {
929 : 5748683 : const Tableau::Entry& entry = *iter;
930 : 5748683 : ArithVar nonbasic = entry.getColVar();
931 [ + + ]: 5748683 : if (nonbasic == x_i) continue;
932 : :
933 : 5415170 : const Rational& a_ij = entry.getCoefficient();
934 : 5415170 : int sgn = a_ij.sgn();
935 [ + + ]: 5415170 : if (isAcceptableSlack<above>(sgn, nonbasic))
936 : : {
937 : : // If one of the above conditions is met, we have found an acceptable
938 : : // nonbasic variable to pivot x_i with. We can now choose which one we
939 : : // prefer the most.
940 [ + + ]: 2345351 : slack = (slack == ARITHVAR_SENTINEL) ? nonbasic
941 [ - + ]: 1005919 : : (this->*pref)(slack, nonbasic);
942 : : }
943 : : }
944 : :
945 : 333513 : return slack;
946 : : }
947 : :
948 : 0 : const Tableau::Entry* LinearEqualityModule::selectSlackEntry(ArithVar x_i,
949 : : bool above) const
950 : : {
951 : 0 : for (Tableau::RowIterator iter = d_tableau.basicRowIterator(x_i);
952 [ - - ]: 0 : !iter.atEnd();
953 : 0 : ++iter)
954 : : {
955 : 0 : const Tableau::Entry& entry = *iter;
956 : 0 : ArithVar nonbasic = entry.getColVar();
957 [ - - ]: 0 : if (nonbasic == x_i) continue;
958 : :
959 : 0 : const Rational& a_ij = entry.getCoefficient();
960 : 0 : int sgn = a_ij.sgn();
961 : 0 : if (above && isAcceptableSlack<true>(sgn, nonbasic))
962 : : {
963 : : // If one of the above conditions is met, we have found an acceptable
964 : : // nonbasic variable to pivot x_i with. We can now choose which one we
965 : : // prefer the most.
966 : 0 : return &entry;
967 : : }
968 : 0 : else if (!above && isAcceptableSlack<false>(sgn, nonbasic))
969 : : {
970 : 0 : return &entry;
971 : : }
972 : : }
973 : :
974 : 0 : return nullptr;
975 : : }
976 : :
977 : 3258671 : void LinearEqualityModule::startTrackingBoundCounts()
978 : : {
979 [ - + ][ - + ]: 3258671 : Assert(!d_areTracking);
[ - - ]
980 : 3258671 : d_areTracking = true;
981 [ - + ]: 3258671 : if (TraceIsOn("arith::tracking"))
982 : : {
983 : 0 : debugCheckTracking();
984 : : }
985 [ - + ][ - + ]: 3258671 : Assert(d_areTracking);
[ - - ]
986 : 3258671 : }
987 : :
988 : 3258671 : void LinearEqualityModule::stopTrackingBoundCounts()
989 : : {
990 [ - + ][ - + ]: 3258671 : Assert(d_areTracking);
[ - - ]
991 : 3258671 : d_areTracking = false;
992 [ - + ]: 3258671 : if (TraceIsOn("arith::tracking"))
993 : : {
994 : 0 : debugCheckTracking();
995 : : }
996 [ - + ][ - + ]: 3258671 : Assert(!d_areTracking);
[ - - ]
997 : 3258671 : }
998 : :
999 : 201247 : void LinearEqualityModule::trackRowIndex(RowIndex ridx)
1000 : : {
1001 [ - + ][ - + ]: 201247 : Assert(!rowIndexIsTracked(ridx));
[ - - ]
1002 : 201247 : BoundsInfo bi = computeRowBoundInfo(ridx, true);
1003 : 201247 : d_btracking.set(ridx, bi);
1004 : 201247 : }
1005 : :
1006 : 201247 : BoundsInfo LinearEqualityModule::computeRowBoundInfo(RowIndex ridx,
1007 : : bool inQueue) const
1008 : : {
1009 : 201247 : BoundsInfo bi;
1010 : :
1011 : 201247 : Tableau::RowIterator iter = d_tableau.ridRowIterator(ridx);
1012 [ + + ]: 1219310 : for (; !iter.atEnd(); ++iter)
1013 : : {
1014 : 1018063 : const Tableau::Entry& entry = *iter;
1015 : 1018063 : ArithVar v = entry.getColVar();
1016 : 1018063 : const Rational& a_ij = entry.getCoefficient();
1017 : 1018063 : bi += (d_variables.selectBoundsInfo(v, inQueue)).multiplyBySgn(a_ij.sgn());
1018 : : }
1019 : 201247 : return bi;
1020 : : }
1021 : :
1022 : 0 : BoundCounts LinearEqualityModule::debugBasicAtBoundCount(ArithVar x_i) const
1023 : : {
1024 : 0 : return d_btracking[d_tableau.basicToRowIndex(x_i)].atBounds();
1025 : : }
1026 : :
1027 : : /**
1028 : : * If the pivot described in u were performed,
1029 : : * then the row would qualify as being either at the minimum/maximum
1030 : : * to the non-basics being at their bounds.
1031 : : * The minimum/maximum is determined by the direction the non-basic is changing.
1032 : : */
1033 : 106452 : bool LinearEqualityModule::basicsAtBounds(const UpdateInfo& u) const
1034 : : {
1035 [ - + ][ - + ]: 106452 : Assert(u.describesPivot());
[ - - ]
1036 : :
1037 : 106452 : ArithVar nonbasic = u.nonbasic();
1038 : 106452 : ArithVar basic = u.leaving();
1039 [ - + ][ - + ]: 106452 : Assert(basicIsTracked(basic));
[ - - ]
1040 : 106452 : int coeffSgn = u.getCoefficient().sgn();
1041 : 106452 : int nbdir = u.nonbasicDirection();
1042 : :
1043 : 106452 : ConstraintP c = u.limiting();
1044 [ + + ][ + + ]: 106452 : int toUB = (c->getType() == UpperBound || c->getType() == Equality) ? 1 : 0;
1045 [ + + ][ + + ]: 106452 : int toLB = (c->getType() == LowerBound || c->getType() == Equality) ? 1 : 0;
1046 : :
1047 : 106452 : RowIndex ridx = d_tableau.basicToRowIndex(basic);
1048 : :
1049 : 106452 : BoundCounts bcs = d_btracking[ridx].atBounds();
1050 : : // x = c*n + \sum d*m
1051 : : // 0 = -x + c*n + \sum d*m
1052 : : // n = 1/c * x + -1/c * (\sum d*m)
1053 : : BoundCounts nonb =
1054 : 106452 : bcs - d_variables.atBoundCounts(nonbasic).multiplyBySgn(coeffSgn);
1055 : 212904 : nonb.addInChange(
1056 : 106452 : -1, d_variables.atBoundCounts(basic), BoundCounts(toLB, toUB));
1057 : 106452 : nonb = nonb.multiplyBySgn(-coeffSgn);
1058 : :
1059 : 106452 : uint32_t length = d_tableau.basicRowLength(basic);
1060 [ + - ]: 212904 : Trace("basicsAtBounds") << "bcs " << bcs << "nonb " << nonb << "length "
1061 : 106452 : << length << endl;
1062 : : // nonb has nb excluded.
1063 [ + + ]: 106452 : if (nbdir < 0)
1064 : : {
1065 : 51312 : return nonb.lowerBoundCount() + 1 == length;
1066 : : }
1067 : : else
1068 : : {
1069 [ - + ][ - + ]: 55140 : Assert(nbdir > 0);
[ - - ]
1070 : 55140 : return nonb.upperBoundCount() + 1 == length;
1071 : : }
1072 : : }
1073 : :
1074 : 681358 : bool LinearEqualityModule::nonbasicsAtLowerBounds(ArithVar basic) const
1075 : : {
1076 [ - + ][ - + ]: 681358 : Assert(basicIsTracked(basic));
[ - - ]
1077 : 681358 : RowIndex ridx = d_tableau.basicToRowIndex(basic);
1078 : :
1079 : 681358 : BoundCounts bcs = d_btracking[ridx].atBounds();
1080 : 681358 : uint32_t length = d_tableau.basicRowLength(basic);
1081 : :
1082 : : // return true if excluding the basic is every element is at its "lowerbound"
1083 : : // The psuedo code is:
1084 : : // bcs -= basic.count(basic, basic's sgn)
1085 : : // return bcs.lowerBoundCount() + 1 == length
1086 : : // As basic's sign is always -1, we can pull out the pieces of the count:
1087 : : // bcs.lowerBoundCount() - basic.atUpperBoundInd() + 1 == length
1088 : : // basic.atUpperBoundInd() is either 0 or 1
1089 : 681358 : uint32_t lbc = bcs.lowerBoundCount();
1090 : : return (lbc == length)
1091 [ + - ][ + + ]: 882670 : || (lbc + 1 == length
1092 [ + - ]: 882670 : && d_variables.cmpAssignmentUpperBound(basic) != 0);
1093 : : }
1094 : :
1095 : 699669 : bool LinearEqualityModule::nonbasicsAtUpperBounds(ArithVar basic) const
1096 : : {
1097 [ - + ][ - + ]: 699669 : Assert(basicIsTracked(basic));
[ - - ]
1098 : 699669 : RowIndex ridx = d_tableau.basicToRowIndex(basic);
1099 : 699669 : BoundCounts bcs = d_btracking[ridx].atBounds();
1100 : 699669 : uint32_t length = d_tableau.basicRowLength(basic);
1101 : 699669 : uint32_t ubc = bcs.upperBoundCount();
1102 : : // See the comment for nonbasicsAtLowerBounds()
1103 : :
1104 : : return (ubc == length)
1105 [ + - ][ + + ]: 914481 : || (ubc + 1 == length
1106 [ + - ]: 914481 : && d_variables.cmpAssignmentLowerBound(basic) != 0);
1107 : : }
1108 : :
1109 : 341292 : void LinearEqualityModule::trackingMultiplyRow(RowIndex ridx, int sgn)
1110 : : {
1111 [ - + ][ - + ]: 341292 : Assert(rowIndexIsTracked(ridx));
[ - - ]
1112 [ - + ][ - + ]: 341292 : Assert(sgn != 0);
[ - - ]
1113 [ + + ]: 341292 : if (sgn < 0)
1114 : : {
1115 : 186764 : BoundsInfo& bi = d_btracking.get(ridx);
1116 : 186764 : bi = bi.multiplyBySgn(sgn);
1117 : : }
1118 : 341292 : }
1119 : :
1120 : 71710684 : void LinearEqualityModule::trackingCoefficientChange(RowIndex ridx,
1121 : : ArithVar nb,
1122 : : int oldSgn,
1123 : : int currSgn)
1124 : : {
1125 [ - + ][ - + ]: 71710684 : Assert(oldSgn != currSgn);
[ - - ]
1126 : 71710684 : BoundsInfo nb_inf = d_variables.boundsInfo(nb);
1127 : :
1128 [ - + ][ - + ]: 71710684 : Assert(rowIndexIsTracked(ridx));
[ - - ]
1129 : :
1130 : 71710684 : BoundsInfo& row_bi = d_btracking.get(ridx);
1131 : 71710684 : row_bi.addInSgn(nb_inf, oldSgn, currSgn);
1132 : 71710684 : }
1133 : :
1134 : 0 : ArithVar LinearEqualityModule::minBy(const ArithVarVec& vec,
1135 : : VarPreferenceFunction pf) const
1136 : : {
1137 [ - - ]: 0 : if (vec.empty())
1138 : : {
1139 : 0 : return ARITHVAR_SENTINEL;
1140 : : }
1141 : : else
1142 : : {
1143 : 0 : ArithVar sel = vec.front();
1144 : 0 : ArithVarVec::const_iterator i = vec.begin() + 1;
1145 : 0 : ArithVarVec::const_iterator i_end = vec.end();
1146 [ - - ]: 0 : for (; i != i_end; ++i)
1147 : : {
1148 [ - - ]: 0 : sel = (this->*pf)(sel, *i);
1149 : : }
1150 : 0 : return sel;
1151 : : }
1152 : : }
1153 : :
1154 : 2190489 : bool LinearEqualityModule::accumulateBorder(const Tableau::Entry& entry,
1155 : : bool ub)
1156 : : {
1157 : 2190489 : ArithVar currBasic = d_tableau.rowIndexToBasic(entry.getRowIndex());
1158 : :
1159 [ - + ][ - + ]: 2190489 : Assert(basicIsTracked(currBasic));
[ - - ]
1160 : :
1161 [ + + ]: 2190489 : ConstraintP bound = ub ? d_variables.getUpperBoundConstraint(currBasic)
1162 : 1095237 : : d_variables.getLowerBoundConstraint(currBasic);
1163 : :
1164 [ + + ]: 2190489 : if (bound == NullConstraint)
1165 : : {
1166 : 1937551 : return false;
1167 : : }
1168 [ - + ][ - + ]: 252938 : Assert(bound != NullConstraint);
[ - - ]
1169 : :
1170 : 252938 : const Rational& coeff = entry.getCoefficient();
1171 : :
1172 : 252938 : const DeltaRational& assignment = d_variables.getAssignment(currBasic);
1173 : 252938 : DeltaRational toBound = bound->getValue() - assignment;
1174 : 252938 : DeltaRational nbDiff = toBound / coeff;
1175 : :
1176 : : // if ub
1177 : : // if toUB >= 0
1178 : : // then ub >= currBasic
1179 : : // if sgn > 0,
1180 : : // then diff >= 0, so nb must increase for G
1181 : : // else diff <= 0, so nb must decrease for G
1182 : : // else ub < currBasic
1183 : : // if sgn > 0,
1184 : : // then diff < 0, so nb must decrease for G
1185 : : // else diff > 0, so nb must increase for G
1186 : :
1187 : 252938 : int diffSgn = nbDiff.sgn();
1188 : :
1189 [ + + ][ + + ]: 252938 : if (diffSgn != 0 && willBeInConflictAfterPivot(entry, nbDiff, ub))
[ + + ]
1190 : : {
1191 : 27 : return true;
1192 : : }
1193 : : else
1194 : : {
1195 [ + + ]: 252911 : bool areFixing = ub ? (toBound.sgn() < 0) : (toBound.sgn() > 0);
1196 : 252911 : Border border(bound, nbDiff, areFixing, &entry, ub);
1197 : : bool increasing =
1198 [ + + ][ + + ]: 252911 : (diffSgn > 0) || (diffSgn == 0 && ((coeff.sgn() > 0) == ub));
[ + + ]
1199 : :
1200 : : // assume diffSgn == 0
1201 : : // if coeff > 0,
1202 : : // if ub, inc
1203 : : // else, dec
1204 : : // else coeff < 0
1205 : : // if ub, dec
1206 : : // else, inc
1207 : :
1208 [ + + ]: 252911 : if (increasing)
1209 : : {
1210 [ + - ]: 128732 : Trace("handleBorders") << "push back increasing " << border << endl;
1211 : 128732 : d_increasing.push_back(border);
1212 : : }
1213 : : else
1214 : : {
1215 [ + - ]: 124179 : Trace("handleBorders") << "push back decreasing " << border << endl;
1216 : 124179 : d_decreasing.push_back(border);
1217 : : }
1218 : 252911 : return false;
1219 : 252911 : }
1220 : 252938 : }
1221 : :
1222 : 167528 : bool LinearEqualityModule::willBeInConflictAfterPivot(
1223 : : const Tableau::Entry& entry, const DeltaRational& nbDiff, bool bToUB) const
1224 : : {
1225 : 167528 : int nbSgn = nbDiff.sgn();
1226 [ - + ][ - + ]: 167528 : Assert(nbSgn != 0);
[ - - ]
1227 : :
1228 [ + + ]: 167528 : if (nbSgn > 0)
1229 : : {
1230 [ + + ][ + + ]: 87619 : if (!d_upperBoundDifference || nbDiff <= *d_upperBoundDifference)
[ + + ]
1231 : : {
1232 : 69367 : return false;
1233 : : }
1234 : : }
1235 : : else
1236 : : {
1237 [ + + ][ + + ]: 79909 : if (!d_lowerBoundDifference || nbDiff >= *d_lowerBoundDifference)
[ + + ]
1238 : : {
1239 : 62665 : return false;
1240 : : }
1241 : : }
1242 : :
1243 : : // Assume past this point, nb will be in error if this pivot is done
1244 : 35496 : ArithVar nb = entry.getColVar();
1245 : 35496 : RowIndex ridx = entry.getRowIndex();
1246 : 35496 : ArithVar basic = d_tableau.rowIndexToBasic(ridx);
1247 [ - + ][ - + ]: 35496 : Assert(rowIndexIsTracked(ridx));
[ - - ]
1248 : 35496 : int coeffSgn = entry.getCoefficient().sgn();
1249 : :
1250 : : // if bToUB, then basic is going to be set to its upperbound
1251 : : // if not bToUB, then basic is going to be set to its lowerbound
1252 : :
1253 : : // Different steps of solving for this:
1254 : : // 1) y = a * x + \sum b * z
1255 : : // 2) -a * x = -y + \sum b * z
1256 : : // 3) x = (-1/a) * ( -y + \sum b * z)
1257 : :
1258 : 35496 : BoundCounts bc = d_btracking[ridx].atBounds();
1259 : :
1260 : : // 1) y = a * x + \sum b * z
1261 : : // Get bc(\sum b * z)
1262 : : BoundCounts sumOnly =
1263 : 35496 : bc - d_variables.atBoundCounts(nb).multiplyBySgn(coeffSgn);
1264 : :
1265 : : // y's bounds in the proposed model
1266 [ + + ][ + + ]: 35496 : int yWillBeAtUb = (bToUB || d_variables.boundsAreEqual(basic)) ? 1 : 0;
1267 [ + + ][ + + ]: 35496 : int yWillBeAtLb = (!bToUB || d_variables.boundsAreEqual(basic)) ? 1 : 0;
1268 : 35496 : BoundCounts ysBounds(yWillBeAtLb, yWillBeAtUb);
1269 : :
1270 : : // 2) -a * x = -y + \sum b * z
1271 : : // Get bc(-y + \sum b * z)
1272 : 35496 : sumOnly.addInChange(-1, d_variables.atBoundCounts(basic), ysBounds);
1273 : :
1274 : : // 3) x = (-1/a) * ( -y + \sum b * z)
1275 : : // Get bc((-1/a) * ( -y + \sum b * z))
1276 : 35496 : BoundCounts xsBoundsAfterPivot = sumOnly.multiplyBySgn(-coeffSgn);
1277 : :
1278 : 35496 : uint32_t length = d_tableau.basicRowLength(basic);
1279 [ + + ]: 35496 : if (nbSgn > 0)
1280 : : {
1281 : : // Only check for the upper bound being violated
1282 : 18252 : return xsBoundsAfterPivot.lowerBoundCount() + 1 == length;
1283 : : }
1284 : : else
1285 : : {
1286 : : // Only check for the lower bound being violated
1287 : 17244 : return xsBoundsAfterPivot.upperBoundCount() + 1 == length;
1288 : : }
1289 : : }
1290 : :
1291 : 27 : UpdateInfo LinearEqualityModule::mkConflictUpdate(const Tableau::Entry& entry,
1292 : : bool ub) const
1293 : : {
1294 : 27 : ArithVar currBasic = d_tableau.rowIndexToBasic(entry.getRowIndex());
1295 : 27 : ArithVar nb = entry.getColVar();
1296 : :
1297 [ + + ]: 27 : ConstraintP bound = ub ? d_variables.getUpperBoundConstraint(currBasic)
1298 : 12 : : d_variables.getLowerBoundConstraint(currBasic);
1299 : :
1300 : 27 : const Rational& coeff = entry.getCoefficient();
1301 : 27 : const DeltaRational& assignment = d_variables.getAssignment(currBasic);
1302 : 27 : DeltaRational toBound = bound->getValue() - assignment;
1303 : 27 : DeltaRational nbDiff = toBound / coeff;
1304 : :
1305 : 54 : return UpdateInfo::conflict(nb, nbDiff, coeff, bound);
1306 : 27 : }
1307 : :
1308 : 28349 : UpdateInfo LinearEqualityModule::speculativeUpdate(
1309 : : ArithVar nb, const Rational& focusCoeff, UpdatePreferenceFunction pref)
1310 : : {
1311 [ - + ][ - + ]: 28349 : Assert(d_increasing.empty());
[ - - ]
1312 [ - + ][ - + ]: 28349 : Assert(d_decreasing.empty());
[ - - ]
1313 [ - + ][ - + ]: 28349 : Assert(!d_lowerBoundDifference);
[ - - ]
1314 [ - + ][ - + ]: 28349 : Assert(!d_upperBoundDifference);
[ - - ]
1315 : :
1316 : 28349 : int focusCoeffSgn = focusCoeff.sgn();
1317 : :
1318 [ + - ]: 28349 : Trace("speculativeUpdate") << "speculativeUpdate" << endl;
1319 [ + - ]: 28349 : Trace("speculativeUpdate") << "nb " << nb << endl;
1320 [ + - ]: 28349 : Trace("speculativeUpdate") << "focusCoeff " << focusCoeff << endl;
1321 : :
1322 [ + + ]: 28349 : if (d_variables.hasUpperBound(nb))
1323 : : {
1324 : 5886 : ConstraintP ub = d_variables.getUpperBoundConstraint(nb);
1325 : 5886 : d_upperBoundDifference = ub->getValue() - d_variables.getAssignment(nb);
1326 : 5886 : Border border(ub, *d_upperBoundDifference, false, nullptr, true);
1327 [ + - ]: 5886 : Trace("handleBorders") << "push back increasing " << border << endl;
1328 : 5886 : d_increasing.push_back(border);
1329 : 5886 : }
1330 [ + + ]: 28349 : if (d_variables.hasLowerBound(nb))
1331 : : {
1332 : 7088 : ConstraintP lb = d_variables.getLowerBoundConstraint(nb);
1333 : 7088 : d_lowerBoundDifference = lb->getValue() - d_variables.getAssignment(nb);
1334 : 7088 : Border border(lb, *d_lowerBoundDifference, false, nullptr, false);
1335 [ + - ]: 7088 : Trace("handleBorders") << "push back decreasing " << border << endl;
1336 : 7088 : d_decreasing.push_back(border);
1337 : 7088 : }
1338 : :
1339 : 28349 : Tableau::ColIterator colIter = d_tableau.colIterator(nb);
1340 [ + + ]: 1123574 : for (; !colIter.atEnd(); ++colIter)
1341 : : {
1342 : 1095252 : const Tableau::Entry& entry = *colIter;
1343 [ - + ][ - + ]: 1095252 : Assert(entry.getColVar() == nb);
[ - - ]
1344 : :
1345 [ + + ]: 1095252 : if (accumulateBorder(entry, true))
1346 : : {
1347 : 15 : clearSpeculative();
1348 : 15 : return mkConflictUpdate(entry, true);
1349 : : }
1350 [ + + ]: 1095237 : if (accumulateBorder(entry, false))
1351 : : {
1352 : 12 : clearSpeculative();
1353 : 12 : return mkConflictUpdate(entry, false);
1354 : : }
1355 : : }
1356 : :
1357 : 28322 : UpdateInfo selected;
1358 [ + + ]: 28322 : BorderHeap& withSgn = focusCoeffSgn > 0 ? d_increasing : d_decreasing;
1359 [ + + ]: 28322 : BorderHeap& againstSgn = focusCoeffSgn > 0 ? d_decreasing : d_increasing;
1360 : :
1361 : 28322 : handleBorders(selected, nb, focusCoeff, withSgn, 0, pref);
1362 : 28322 : int m = 1 - selected.errorsChangeSafe(0);
1363 : 28322 : handleBorders(selected, nb, focusCoeff, againstSgn, m, pref);
1364 : :
1365 : 28322 : clearSpeculative();
1366 : 28322 : return selected;
1367 : 28322 : }
1368 : :
1369 : 28349 : void LinearEqualityModule::clearSpeculative()
1370 : : {
1371 : : // clear everything away
1372 : 28349 : d_increasing.clear();
1373 : 28349 : d_decreasing.clear();
1374 : 28349 : d_lowerBoundDifference.reset();
1375 : 28349 : d_upperBoundDifference.reset();
1376 : 28349 : }
1377 : :
1378 : 56644 : void LinearEqualityModule::handleBorders(UpdateInfo& selected,
1379 : : ArithVar nb,
1380 : : const Rational& focusCoeff,
1381 : : BorderHeap& heap,
1382 : : int minimumFixes,
1383 : : UpdatePreferenceFunction pref)
1384 : : {
1385 [ - + ][ - + ]: 56644 : Assert(minimumFixes >= 0);
[ - - ]
1386 : :
1387 : : // The values popped off of the heap
1388 : : // should be popped with the values closest to 0
1389 : : // being first and larger in absolute value last
1390 : :
1391 : 56644 : int fixesRemaining = heap.possibleFixes();
1392 : :
1393 [ + - ]: 113288 : Trace("handleBorders") << "handleBorders "
1394 : 0 : << "nb " << nb << "fc " << focusCoeff << "h.e "
1395 : 0 : << heap.empty() << "h.dir " << heap.direction()
1396 : 0 : << "h.rem " << fixesRemaining << "h.0s "
1397 : 56644 : << heap.numZeroes() << "min " << minimumFixes << endl;
1398 : :
1399 [ + + ]: 56644 : if (heap.empty())
1400 : : {
1401 : : // if the heap is empty, return
1402 : 28265 : return;
1403 : : }
1404 : :
1405 : 45060 : bool zeroesWillDominate = fixesRemaining - heap.numZeroes() < minimumFixes;
1406 : :
1407 : : // can the number of fixes ever exceed the minimum?
1408 : : // no more than the number of possible fixes can be fixed in total
1409 : : // nothing can be fixed before the zeroes are taken care of
1410 [ + + ][ + + ]: 45060 : if (minimumFixes > 0 && zeroesWillDominate)
1411 : : {
1412 : 16681 : return;
1413 : : }
1414 : :
1415 : 28379 : int negErrorChange = 0;
1416 : 28379 : int nbDir = heap.direction();
1417 : :
1418 : : // points at the beginning of the heap
1419 [ + + ]: 28379 : if (zeroesWillDominate)
1420 : : {
1421 : 6976 : heap.dropNonZeroes();
1422 : : }
1423 : 28379 : heap.make_heap();
1424 : :
1425 : : // pretend like the previous block had a value of zero.
1426 : : // The block that actually has a value of 0 must handle this.
1427 : 28379 : const DeltaRational zero(0);
1428 : 28379 : const DeltaRational* prevBlockValue = &zero;
1429 : :
1430 : : /** The coefficient changes as the value crosses border. */
1431 : 28379 : Rational effectiveCoefficient = focusCoeff;
1432 : :
1433 : : /* Keeps track of the change to the value of the focus function.*/
1434 : 28379 : DeltaRational totalFocusChange(0);
1435 : :
1436 : 28379 : const int focusCoeffSgn = focusCoeff.sgn();
1437 : :
1438 : 62968 : while (heap.more()
1439 [ + + ][ + + ]: 73327 : && (fixesRemaining + negErrorChange > minimumFixes
[ + + ]
1440 [ + + ]: 10359 : || (fixesRemaining + negErrorChange == minimumFixes
1441 [ + + ]: 7140 : && effectiveCoefficient.sgn() == focusCoeffSgn)))
1442 : : {
1443 : : // There are more elements &&
1444 : : // we can either fix at least 1 more variable in the error function
1445 : : // or we can improve the error function
1446 : :
1447 : 34589 : int brokenInBlock = 0;
1448 : 34589 : BorderVec::const_iterator endBlock = heap.end();
1449 : :
1450 : 34589 : pop_block(heap, brokenInBlock, fixesRemaining, negErrorChange);
1451 : :
1452 : : // if endVec == beginVec, block starts there
1453 : : // other wise, block starts at endVec
1454 : : BorderVec::const_iterator startBlock =
1455 [ + + ]: 34589 : heap.more() ? heap.end() : heap.begin();
1456 : :
1457 : 34589 : const DeltaRational& blockValue = (*startBlock).d_diff;
1458 : :
1459 : : // if decreasing
1460 : : // blockValue < prevBlockValue
1461 : : // diff.sgn() = -1
1462 : 34589 : DeltaRational diff = blockValue - (*prevBlockValue);
1463 : 34589 : DeltaRational blockChangeToFocus = diff * effectiveCoefficient;
1464 : 34589 : totalFocusChange += blockChangeToFocus;
1465 : :
1466 [ + - ]: 69178 : Trace("handleBorders") << "blockValue " << (blockValue) << "diff " << diff
1467 : 0 : << "blockChangeToFocus " << totalFocusChange
1468 : 0 : << "blockChangeToFocus " << totalFocusChange
1469 : 0 : << "negErrorChange " << negErrorChange
1470 : 0 : << "brokenInBlock " << brokenInBlock
1471 : 34589 : << "fixesRemaining " << fixesRemaining << endl;
1472 : :
1473 : 34589 : int currFocusChangeSgn = totalFocusChange.sgn();
1474 [ + + ]: 130954 : for (BorderVec::const_iterator i = startBlock; i != endBlock; ++i)
1475 : : {
1476 : 96365 : const Border& b = *i;
1477 : :
1478 [ + - ]: 96365 : Trace("handleBorders") << b << endl;
1479 : :
1480 : 96365 : bool makesImprovement =
1481 [ + + ][ + + ]: 96365 : negErrorChange > 0 || (negErrorChange == 0 && currFocusChangeSgn > 0);
[ + + ]
1482 : :
1483 [ + + ]: 96365 : if (!makesImprovement)
1484 : : {
1485 [ + + ][ + + ]: 42809 : if (b.ownBorder() || minimumFixes > 0)
[ + + ]
1486 : : {
1487 : 90 : continue;
1488 : : }
1489 : : }
1490 : :
1491 : 96275 : UpdateInfo proposal(nb, nbDir);
1492 [ + + ]: 96275 : if (b.ownBorder())
1493 : : {
1494 : 721 : proposal.witnessedUpdate(
1495 : 721 : b.d_diff, b.d_bound, -negErrorChange, currFocusChangeSgn);
1496 : : }
1497 : : else
1498 : : {
1499 : 95554 : proposal.update(b.d_diff,
1500 : : b.getCoefficient(),
1501 : 95554 : b.d_bound,
1502 : : -negErrorChange,
1503 : : currFocusChangeSgn);
1504 : : }
1505 : :
1506 [ + + ][ - + ]: 96275 : if (selected.unbounded() || (this->*pref)(selected, proposal))
[ + + ][ + + ]
1507 : : {
1508 : 57715 : selected = proposal;
1509 : : }
1510 : 96275 : }
1511 : :
1512 : 34589 : effectiveCoefficient += updateCoefficient(startBlock, endBlock);
1513 : 34589 : prevBlockValue = &blockValue;
1514 : 34589 : negErrorChange -= brokenInBlock;
1515 : 34589 : }
1516 : 28379 : }
1517 : :
1518 : 34589 : Rational LinearEqualityModule::updateCoefficient(
1519 : : BorderVec::const_iterator startBlock, BorderVec::const_iterator endBlock)
1520 : : {
1521 : : // update coefficient
1522 : 34589 : Rational changeToCoefficient(0);
1523 [ + + ]: 130954 : for (BorderVec::const_iterator i = startBlock; i != endBlock; ++i)
1524 : : {
1525 : 96365 : const Border& curr = *i;
1526 [ + + ]: 96365 : if (curr.ownBorder())
1527 : : { // breaking its own bound
1528 [ + + ]: 776 : if (curr.d_upperbound)
1529 : : {
1530 : 604 : changeToCoefficient -= 1;
1531 : : }
1532 : : else
1533 : : {
1534 : 172 : changeToCoefficient += 1;
1535 : : }
1536 : : }
1537 : : else
1538 : : {
1539 : 95589 : const Rational& coeff = curr.d_entry->getCoefficient();
1540 [ + + ]: 95589 : if (curr.d_areFixing)
1541 : : {
1542 [ + + ]: 24280 : if (curr.d_upperbound)
1543 : : { // fixing an upper bound
1544 : 11107 : changeToCoefficient += coeff;
1545 : : }
1546 : : else
1547 : : { // fixing a lower bound
1548 : 13173 : changeToCoefficient -= coeff;
1549 : : }
1550 : : }
1551 : : else
1552 : : {
1553 [ + + ]: 71309 : if (curr.d_upperbound)
1554 : : { // breaking an upper bound
1555 : 29614 : changeToCoefficient -= coeff;
1556 : : }
1557 : : else
1558 : : {
1559 : : // breaking a lower bound
1560 : 41695 : changeToCoefficient += coeff;
1561 : : }
1562 : : }
1563 : : }
1564 : : }
1565 : 34589 : return changeToCoefficient;
1566 : 0 : }
1567 : :
1568 : 34589 : void LinearEqualityModule::pop_block(BorderHeap& heap,
1569 : : int& brokenInBlock,
1570 : : int& fixesRemaining,
1571 : : int& negErrorChange)
1572 : : {
1573 [ - + ][ - + ]: 34589 : Assert(heap.more());
[ - - ]
1574 : :
1575 [ + + ]: 34589 : if (heap.top().d_areFixing)
1576 : : {
1577 : 11965 : fixesRemaining--;
1578 : 11965 : negErrorChange++;
1579 : : }
1580 : : else
1581 : : {
1582 : 22624 : brokenInBlock++;
1583 : : }
1584 : 34589 : heap.pop_heap();
1585 : 34589 : const DeltaRational& blockValue = (*heap.end()).d_diff;
1586 : :
1587 [ + + ]: 96365 : while (heap.more())
1588 : : {
1589 : 77633 : const Border& top = heap.top();
1590 [ + + ]: 77633 : if (blockValue == top.d_diff)
1591 : : {
1592 : : // belongs to the block
1593 [ + + ]: 61776 : if (top.d_areFixing)
1594 : : {
1595 : 12315 : fixesRemaining--;
1596 : 12315 : negErrorChange++;
1597 : : }
1598 : : else
1599 : : {
1600 : 49461 : brokenInBlock++;
1601 : : }
1602 : 61776 : heap.pop_heap();
1603 : : }
1604 : : else
1605 : : {
1606 : : // does not belong to the block
1607 [ + + ][ - + ]: 15857 : Assert((heap.direction() > 0) ? (blockValue < top.d_diff)
[ - + ][ - - ]
1608 : : : (blockValue > top.d_diff));
1609 : 15857 : break;
1610 : : }
1611 : : }
1612 : 34589 : }
1613 : :
1614 : 5039 : void LinearEqualityModule::substitutePlusTimesConstant(ArithVar to,
1615 : : ArithVar from,
1616 : : const Rational& mult)
1617 : : {
1618 : 5039 : d_tableau.substitutePlusTimesConstant(to, from, mult, d_trackCallback);
1619 : 5039 : }
1620 : 4541 : void LinearEqualityModule::directlyAddToCoefficient(ArithVar row,
1621 : : ArithVar col,
1622 : : const Rational& mult)
1623 : : {
1624 : 4541 : d_tableau.directlyAddToCoefficient(row, col, mult, d_trackCallback);
1625 : 4541 : }
1626 : :
1627 : : } // namespace arith::linear
1628 : : } // namespace theory
1629 : : } // namespace cvc5::internal
|
