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>(ArithVar x_i, VarPreferenceFunction pf) const;
27 : : template ArithVar LinearEqualityModule::selectSlack<false>(ArithVar x_i, VarPreferenceFunction pf) const;
28 : :
29 : : template bool LinearEqualityModule::preferWitness<true>(const UpdateInfo& a, const UpdateInfo& b) const;
30 : : template bool LinearEqualityModule::preferWitness<false>(const UpdateInfo& a, const UpdateInfo& b) const;
31 : :
32 : :
33 : 0 : void Border::output(std::ostream& out) const{
34 : : out << "{Border"
35 : 0 : << ", " << d_bound->getVariable()
36 : 0 : << ", " << d_bound->getValue()
37 : 0 : << ", " << d_diff
38 : 0 : << ", " << d_areFixing
39 : 0 : << ", " << d_upperbound;
40 [ - - ]: 0 : if(ownBorder()){
41 : 0 : out << ", ownBorder";
42 : : }else{
43 : 0 : out << ", " << d_entry->getCoefficient();
44 : : }
45 : 0 : out << ", " << d_bound
46 : 0 : << "}";
47 : 0 : }
48 : :
49 : 49981 : LinearEqualityModule::LinearEqualityModule(StatisticsRegistry& sr,
50 : : ArithVariables& vars,
51 : : Tableau& t,
52 : : BoundInfoMap& boundsTracking,
53 : 49981 : BasicVarModelUpdateCallBack f)
54 : 49981 : : d_variables(vars),
55 : 49981 : d_tableau(t),
56 : 49981 : d_basicVariableUpdates(f),
57 : 49981 : d_increasing(1),
58 : 49981 : d_decreasing(-1),
59 : 49981 : d_upperBoundDifference(),
60 : 49981 : d_lowerBoundDifference(),
61 : 49981 : d_one(1),
62 : 49981 : d_negOne(-1),
63 : 49981 : d_btracking(boundsTracking),
64 : 49981 : d_areTracking(false),
65 : 49981 : d_trackCallback(this),
66 : 49981 : d_statistics(sr)
67 : 49981 : {}
68 : :
69 : 49981 : LinearEqualityModule::Statistics::Statistics(StatisticsRegistry& sr)
70 : 49981 : : d_statPivots(sr.registerInt("theory::arith::pivots")),
71 : 49981 : d_statUpdates(sr.registerInt("theory::arith::updates")),
72 : 49981 : d_pivotTime(sr.registerTimer("theory::arith::pivotTime")),
73 : 49981 : d_adjTime(sr.registerTimer("theory::arith::adjTime")),
74 : 49981 : d_weakeningAttempts(sr.registerInt("theory::arith::weakening::attempts")),
75 : 49981 : d_weakeningSuccesses(sr.registerInt("theory::arith::weakening::success")),
76 : 49981 : d_weakenings(sr.registerInt("theory::arith::weakening::total")),
77 : 49981 : d_weakenTime(sr.registerTimer("theory::arith::weakening::time")),
78 : 49981 : d_forceTime(sr.registerTimer("theory::arith::forcing::time"))
79 : : {
80 : 49981 : }
81 : :
82 : 9246350 : void LinearEqualityModule::includeBoundUpdate(ArithVar v, const BoundsInfo& prev){
83 [ - + ][ - + ]: 9246350 : Assert(!d_areTracking);
[ - - ]
84 : :
85 : 9246350 : BoundsInfo curr = d_variables.boundsInfo(v);
86 : :
87 [ - + ][ - + ]: 9246350 : Assert(prev != curr);
[ - - ]
88 : 9246350 : Tableau::ColIterator basicIter = d_tableau.colIterator(v);
89 [ + + ]: 56465840 : for(; !basicIter.atEnd(); ++basicIter){
90 : 47219490 : const Tableau::Entry& entry = *basicIter;
91 [ - + ][ - + ]: 47219490 : Assert(entry.getColVar() == v);
[ - - ]
92 : 47219490 : int a_ijSgn = entry.getCoefficient().sgn();
93 : :
94 : 47219490 : RowIndex ridx = entry.getRowIndex();
95 : 47219490 : BoundsInfo& counts = d_btracking.get(ridx);
96 [ + - ]: 47219490 : Trace("includeBoundUpdate") << d_tableau.rowIndexToBasic(ridx) << " " << counts << " to " ;
97 : 47219490 : counts.addInChange(a_ijSgn, prev, curr);
98 [ + - ]: 47219490 : Trace("includeBoundUpdate") << counts << " " << a_ijSgn << std::endl;
99 : : }
100 : 9246350 : }
101 : :
102 : 0 : void LinearEqualityModule::updateMany(const DenseMap<DeltaRational>& many){
103 [ - - ]: 0 : for(DenseMap<DeltaRational>::const_iterator i = many.begin(), i_end = many.end(); i != i_end; ++i){
104 : 0 : ArithVar nb = *i;
105 [ - - ]: 0 : if(!d_tableau.isBasic(nb)){
106 : 0 : Assert(!d_tableau.isBasic(nb));
107 : 0 : const DeltaRational& newValue = many[nb];
108 [ - - ]: 0 : if(newValue != d_variables.getAssignment(nb)){
109 [ - - ]: 0 : Trace("arith::updateMany")
110 : 0 : << "updateMany:" << nb << " "
111 : 0 : << d_variables.getAssignment(nb) << " to "<< newValue << endl;
112 : 0 : update(nb, newValue);
113 : : }
114 : : }
115 : : }
116 : 0 : }
117 : :
118 : :
119 : :
120 : :
121 : 0 : void LinearEqualityModule::applySolution(const DenseSet& newBasis, const DenseMap<DeltaRational>& newValues){
122 : 0 : forceNewBasis(newBasis);
123 : 0 : updateMany(newValues);
124 : 0 : }
125 : :
126 : 0 : void LinearEqualityModule::forceNewBasis(const DenseSet& newBasis){
127 : 0 : TimerStat::CodeTimer codeTimer(d_statistics.d_forceTime);
128 : 0 : cout << "force begin" << endl;
129 : 0 : DenseSet needsToBeAdded;
130 [ - - ]: 0 : for(DenseSet::const_iterator i = newBasis.begin(), i_end = newBasis.end(); i != i_end; ++i){
131 : 0 : ArithVar b = *i;
132 [ - - ]: 0 : if(!d_tableau.isBasic(b)){
133 : 0 : needsToBeAdded.add(b);
134 : : }
135 : : }
136 : :
137 [ - - ]: 0 : while(!needsToBeAdded.empty()){
138 : 0 : ArithVar toRemove = ARITHVAR_SENTINEL;
139 : 0 : ArithVar toAdd = ARITHVAR_SENTINEL;
140 : 0 : DenseSet::const_iterator i = needsToBeAdded.begin(), i_end = needsToBeAdded.end();
141 [ - - ][ - - ]: 0 : for(; toAdd == ARITHVAR_SENTINEL && i != i_end; ++i){
[ - - ]
142 : 0 : ArithVar v = *i;
143 : :
144 : 0 : Tableau::ColIterator colIter = d_tableau.colIterator(v);
145 [ - - ]: 0 : for(; !colIter.atEnd(); ++colIter){
146 : 0 : const Tableau::Entry& entry = *colIter;
147 : 0 : Assert(entry.getColVar() == v);
148 : 0 : ArithVar b = d_tableau.rowIndexToBasic(entry.getRowIndex());
149 [ - - ]: 0 : if(!newBasis.isMember(b)){
150 : 0 : toAdd = v;
151 [ - - ][ - - ]: 0 : if(toRemove == ARITHVAR_SENTINEL ||
152 [ - - ]: 0 : d_tableau.basicRowLength(toRemove) > d_tableau.basicRowLength(b)){
153 : 0 : toRemove = b;
154 : : }
155 : : }
156 : : }
157 : : }
158 : 0 : Assert(toRemove != ARITHVAR_SENTINEL);
159 : 0 : Assert(toAdd != ARITHVAR_SENTINEL);
160 : :
161 [ - - ]: 0 : Trace("arith::forceNewBasis") << toRemove << " " << toAdd << endl;
162 : 0 : d_tableau.pivot(toRemove, toAdd, d_trackCallback);
163 : 0 : d_basicVariableUpdates(toAdd);
164 : :
165 [ - - ]: 0 : Trace("arith::forceNewBasis") << needsToBeAdded.size() << "to go" << endl;
166 : 0 : needsToBeAdded.remove(toAdd);
167 : : }
168 : 0 : }
169 : :
170 : 311760 : void LinearEqualityModule::updateUntracked(ArithVar x_i, const DeltaRational& v){
171 [ - + ][ - + ]: 311760 : Assert(!d_tableau.isBasic(x_i));
[ - - ]
172 [ - + ][ - + ]: 311760 : Assert(!d_areTracking);
[ - - ]
173 : 311760 : const DeltaRational& assignment_x_i = d_variables.getAssignment(x_i);
174 : 311760 : ++(d_statistics.d_statUpdates);
175 : :
176 : :
177 [ + - ]: 623520 : Trace("arith") <<"update " << x_i << ": "
178 : 311760 : << assignment_x_i << "|-> " << v << endl;
179 : 311760 : DeltaRational diff = v - assignment_x_i;
180 : :
181 : 311760 : Tableau::ColIterator colIter = d_tableau.colIterator(x_i);
182 [ + + ]: 3457834 : for(; !colIter.atEnd(); ++colIter){
183 : 3146074 : const Tableau::Entry& entry = *colIter;
184 [ - + ][ - + ]: 3146074 : Assert(entry.getColVar() == x_i);
[ - - ]
185 : :
186 : 3146074 : ArithVar x_j = d_tableau.rowIndexToBasic(entry.getRowIndex());
187 : 3146074 : const Rational& a_ji = entry.getCoefficient();
188 : :
189 : 3146074 : const DeltaRational& assignment = d_variables.getAssignment(x_j);
190 : 3146074 : DeltaRational nAssignment = assignment+(diff * a_ji);
191 : 3146074 : d_variables.setAssignment(x_j, nAssignment);
192 : :
193 : 3146074 : d_basicVariableUpdates(x_j);
194 : 3146074 : }
195 : :
196 : 311760 : d_variables.setAssignment(x_i, v);
197 : :
198 [ - + ]: 311760 : if(TraceIsOn("paranoid:check_tableau")){ debugCheckTableau(); }
199 : 311760 : }
200 : :
201 : 364608 : void LinearEqualityModule::updateTracked(ArithVar x_i, const DeltaRational& v){
202 : 364608 : TimerStat::CodeTimer codeTimer(d_statistics.d_adjTime);
203 : :
204 [ - + ][ - + ]: 364608 : Assert(!d_tableau.isBasic(x_i));
[ - - ]
205 [ - + ][ - + ]: 364608 : Assert(d_areTracking);
[ - - ]
206 : :
207 : 364608 : ++(d_statistics.d_statUpdates);
208 : :
209 : 364608 : DeltaRational diff = v - d_variables.getAssignment(x_i);
210 [ + - ]: 729216 : Trace("arith") <<"update " << x_i << ": "
211 : 364608 : << d_variables.getAssignment(x_i) << "|-> " << v << endl;
212 : :
213 : :
214 : 364608 : BoundCounts before = d_variables.atBoundCounts(x_i);
215 : 364608 : d_variables.setAssignment(x_i, v);
216 : 364608 : BoundCounts after = d_variables.atBoundCounts(x_i);
217 : :
218 : 364608 : bool anyChange = before != after;
219 : :
220 : 364608 : Tableau::ColIterator colIter = d_tableau.colIterator(x_i);
221 [ + + ]: 7216115 : for(; !colIter.atEnd(); ++colIter){
222 : 6851507 : const Tableau::Entry& entry = *colIter;
223 [ - + ][ - + ]: 6851507 : Assert(entry.getColVar() == x_i);
[ - - ]
224 : :
225 : 6851507 : RowIndex ridx = entry.getRowIndex();
226 : 6851507 : ArithVar x_j = d_tableau.rowIndexToBasic(ridx);
227 : 6851507 : const Rational& a_ji = entry.getCoefficient();
228 : :
229 : 6851507 : const DeltaRational& assignment = d_variables.getAssignment(x_j);
230 : 6851507 : DeltaRational nAssignment = assignment+(diff * a_ji);
231 [ + - ]: 6851507 : Trace("update") << x_j << " " << a_ji << assignment << " -> " << nAssignment << endl;
232 : 6851507 : BoundCounts xjBefore = d_variables.atBoundCounts(x_j);
233 : 6851507 : d_variables.setAssignment(x_j, nAssignment);
234 : 6851507 : BoundCounts xjAfter = d_variables.atBoundCounts(x_j);
235 : :
236 [ - + ][ - + ]: 6851507 : Assert(rowIndexIsTracked(ridx));
[ - - ]
237 : 6851507 : BoundsInfo& next_bc_k = d_btracking.get(ridx);
238 [ + + ]: 6851507 : if(anyChange){
239 : 4763064 : next_bc_k.addInAtBoundChange(a_ji.sgn(), before, after);
240 : : }
241 [ + + ]: 6851507 : if(xjBefore != xjAfter){
242 : 862032 : next_bc_k.addInAtBoundChange(-1, xjBefore, xjAfter);
243 : : }
244 : :
245 : 6851507 : d_basicVariableUpdates(x_j);
246 : 6851507 : }
247 : :
248 [ - + ]: 364608 : if(TraceIsOn("paranoid:check_tableau")){ debugCheckTableau(); }
249 : 364608 : }
250 : :
251 : 364468 : void LinearEqualityModule::pivotAndUpdate(ArithVar x_i, ArithVar x_j, const DeltaRational& x_i_value){
252 [ - + ][ - + ]: 364468 : Assert(x_i != x_j);
[ - - ]
253 : :
254 : 364468 : TimerStat::CodeTimer codeTimer(d_statistics.d_pivotTime);
255 : :
256 [ - + ]: 364468 : if(TraceIsOn("arith::tracking::pre")){
257 [ - - ]: 0 : Trace("arith::tracking") << "pre update" << endl;
258 : 0 : debugCheckTracking();
259 : : }
260 : :
261 [ - + ]: 364468 : if(TraceIsOn("arith::simplex:row")){ debugPivot(x_i, x_j); }
262 : :
263 : 364468 : RowIndex ridx = d_tableau.basicToRowIndex(x_i);
264 : 364468 : const Tableau::Entry& entry_ij = d_tableau.findEntry(ridx, x_j);
265 [ - + ][ - + ]: 364468 : Assert(!entry_ij.blank());
[ - - ]
266 : :
267 : 364468 : const Rational& a_ij = entry_ij.getCoefficient();
268 : 364468 : const DeltaRational& betaX_i = d_variables.getAssignment(x_i);
269 : 364468 : DeltaRational theta = (x_i_value - betaX_i)/a_ij;
270 : 364468 : DeltaRational x_j_value = d_variables.getAssignment(x_j) + theta;
271 : :
272 : 364468 : updateTracked(x_j, x_j_value);
273 : :
274 [ - + ]: 364468 : if(TraceIsOn("arith::tracking::mid")){
275 [ - - ]: 0 : Trace("arith::tracking") << "postupdate prepivot" << endl;
276 : 0 : debugCheckTracking();
277 : : }
278 : :
279 : : // Pivots
280 : 364468 : ++(d_statistics.d_statPivots);
281 : :
282 : 364468 : d_tableau.pivot(x_i, x_j, d_trackCallback);
283 : :
284 [ - + ]: 364468 : if(TraceIsOn("arith::tracking::post")){
285 [ - - ]: 0 : Trace("arith::tracking") << "postpivot" << endl;
286 : 0 : debugCheckTracking();
287 : : }
288 : :
289 : 364468 : d_basicVariableUpdates(x_j);
290 : :
291 [ - + ]: 364468 : if(TraceIsOn("matrix")){
292 : 0 : d_tableau.printMatrix();
293 : : }
294 : 364468 : }
295 : :
296 : 90190 : uint32_t LinearEqualityModule::updateProduct(const UpdateInfo& inf) const {
297 : 90190 : uint32_t colLen = d_tableau.getColLength(inf.nonbasic());
298 [ + + ]: 90190 : if(inf.describesPivot()){
299 [ - + ][ - + ]: 87950 : Assert(inf.leaving() != inf.nonbasic());
[ - - ]
300 : 87950 : return colLen + d_tableau.basicRowLength(inf.leaving());
301 : : }else{
302 : 2240 : return colLen;
303 : : }
304 : : }
305 : :
306 : 0 : void LinearEqualityModule::debugCheckTracking(){
307 : 0 : Tableau::BasicIterator basicIter = d_tableau.beginBasic(),
308 : 0 : endIter = d_tableau.endBasic();
309 [ - - ]: 0 : for(; basicIter != endIter; ++basicIter){
310 : 0 : ArithVar basic = *basicIter;
311 [ - - ]: 0 : Trace("arith::tracking") << "arith::tracking row basic: " << basic << endl;
312 : :
313 : 0 : for(Tableau::RowIterator iter = d_tableau.basicRowIterator(basic); !iter.atEnd() && TraceIsOn("arith::tracking"); ++iter){
314 : 0 : const Tableau::Entry& entry = *iter;
315 : :
316 : 0 : ArithVar var = entry.getColVar();
317 : 0 : const Rational& coeff = entry.getCoefficient();
318 : 0 : DeltaRational beta = d_variables.getAssignment(var);
319 [ - - ]: 0 : Trace("arith::tracking") << var << " " << d_variables.boundsInfo(var)
320 : 0 : << " " << beta << coeff;
321 [ - - ]: 0 : if(d_variables.hasLowerBound(var)){
322 [ - - ]: 0 : Trace("arith::tracking") << "(lb " << d_variables.getLowerBound(var) << ")";
323 : : }
324 [ - - ]: 0 : if(d_variables.hasUpperBound(var)){
325 [ - - ]: 0 : Trace("arith::tracking") << "(up " << d_variables.getUpperBound(var) << ")";
326 : : }
327 [ - - ]: 0 : Trace("arith::tracking") << endl;
328 : 0 : }
329 [ - - ]: 0 : Trace("arith::tracking") << "end row"<< endl;
330 : :
331 [ - - ]: 0 : if(basicIsTracked(basic)){
332 : 0 : RowIndex ridx = d_tableau.basicToRowIndex(basic);
333 : 0 : BoundsInfo computed = computeRowBoundInfo(ridx, false);
334 [ - - ]: 0 : Trace("arith::tracking")
335 : 0 : << "computed " << computed
336 : 0 : << " tracking " << d_btracking[ridx] << endl;
337 : 0 : Assert(computed == d_btracking[ridx]);
338 : : }
339 : : }
340 : 0 : }
341 : :
342 : 0 : void LinearEqualityModule::debugPivot(ArithVar x_i, ArithVar x_j){
343 [ - - ]: 0 : Trace("arith::pivot") << "debugPivot("<< x_i <<"|->"<< x_j << ")" << endl;
344 : :
345 [ - - ]: 0 : for(Tableau::RowIterator iter = d_tableau.basicRowIterator(x_i); !iter.atEnd(); ++iter){
346 : 0 : const Tableau::Entry& entry = *iter;
347 : :
348 : 0 : ArithVar var = entry.getColVar();
349 : 0 : const Rational& coeff = entry.getCoefficient();
350 : 0 : DeltaRational beta = d_variables.getAssignment(var);
351 [ - - ]: 0 : Trace("arith::pivot") << var << beta << coeff;
352 [ - - ]: 0 : if(d_variables.hasLowerBound(var)){
353 [ - - ]: 0 : Trace("arith::pivot") << "(lb " << d_variables.getLowerBound(var) << ")";
354 : : }
355 [ - - ]: 0 : if(d_variables.hasUpperBound(var)){
356 [ - - ]: 0 : Trace("arith::pivot") << "(up " << d_variables.getUpperBound(var) << ")";
357 : : }
358 [ - - ]: 0 : Trace("arith::pivot") << endl;
359 : 0 : }
360 [ - - ]: 0 : Trace("arith::pivot") << "end row"<< endl;
361 : 0 : }
362 : :
363 : : /**
364 : : * This check is quite expensive.
365 : : * It should be wrapped in a TraceIsOn() guard.
366 : : * if(TraceIsOn("paranoid:check_tableau")){
367 : : * checkTableau();
368 : : * }
369 : : */
370 : 0 : void LinearEqualityModule::debugCheckTableau(){
371 : 0 : Tableau::BasicIterator basicIter = d_tableau.beginBasic(),
372 : 0 : endIter = d_tableau.endBasic();
373 [ - - ]: 0 : for(; basicIter != endIter; ++basicIter){
374 : 0 : ArithVar basic = *basicIter;
375 : 0 : DeltaRational sum;
376 [ - - ]: 0 : Trace("paranoid:check_tableau") << "starting row" << basic << endl;
377 : 0 : Tableau::RowIterator nonbasicIter = d_tableau.basicRowIterator(basic);
378 [ - - ]: 0 : for(; !nonbasicIter.atEnd(); ++nonbasicIter){
379 : 0 : const Tableau::Entry& entry = *nonbasicIter;
380 : 0 : ArithVar nonbasic = entry.getColVar();
381 [ - - ]: 0 : if(basic == nonbasic) continue;
382 : :
383 : 0 : const Rational& coeff = entry.getCoefficient();
384 : 0 : DeltaRational beta = d_variables.getAssignment(nonbasic);
385 [ - - ]: 0 : Trace("paranoid:check_tableau") << nonbasic << beta << coeff<<endl;
386 : 0 : sum = sum + (beta*coeff);
387 : 0 : }
388 : 0 : DeltaRational shouldBe = d_variables.getAssignment(basic);
389 [ - - ]: 0 : Trace("paranoid:check_tableau") << "ending row" << sum
390 : 0 : << "," << shouldBe << endl;
391 : :
392 : 0 : Assert(sum == shouldBe);
393 : 0 : }
394 : 0 : }
395 : :
396 : 820176 : DeltaRational LinearEqualityModule::computeRowBound(RowIndex ridx, bool rowUb, ArithVar skip) const {
397 : 1640352 : DeltaRational sum(0,0);
398 [ + + ]: 5312192 : for(Tableau::RowIterator i = d_tableau.ridRowIterator(ridx); !i.atEnd(); ++i){
399 : 4492016 : const Tableau::Entry& entry = (*i);
400 : 4492016 : ArithVar v = entry.getColVar();
401 [ + + ]: 4492016 : if(v == skip){ continue; }
402 : :
403 : 3892838 : const Rational& coeff = entry.getCoefficient();
404 : 3892838 : bool vUb = (rowUb == (coeff.sgn() > 0));
405 : :
406 [ + + ]: 3892838 : const DeltaRational& bound = vUb ?
407 : 1939339 : d_variables.getUpperBound(v):
408 : 1953499 : d_variables.getLowerBound(v);
409 : :
410 : 3892838 : DeltaRational diff = bound * coeff;
411 : 3892838 : sum = sum + diff;
412 : 3892838 : }
413 : 820176 : return sum;
414 : 0 : }
415 : :
416 : : /**
417 : : * Computes the value of a basic variable using the current assignment.
418 : : */
419 : 396233 : DeltaRational LinearEqualityModule::computeRowValue(ArithVar x, bool useSafe) const{
420 [ - + ][ - + ]: 396233 : Assert(d_tableau.isBasic(x));
[ - - ]
421 : 396233 : DeltaRational sum(0);
422 : :
423 [ + + ]: 2351650 : for(Tableau::RowIterator i = d_tableau.basicRowIterator(x); !i.atEnd(); ++i){
424 : 1955417 : const Tableau::Entry& entry = (*i);
425 : 1955417 : ArithVar nonbasic = entry.getColVar();
426 [ + + ]: 1955417 : if(nonbasic == x) continue;
427 : 1559184 : const Rational& coeff = entry.getCoefficient();
428 : :
429 : 1559184 : const DeltaRational& assignment = d_variables.getAssignment(nonbasic, useSafe);
430 : 1559184 : sum = sum + (assignment * coeff);
431 : : }
432 : 396233 : return sum;
433 : 0 : }
434 : :
435 : 8107063 : const Tableau::Entry* LinearEqualityModule::rowLacksBound(RowIndex ridx, bool rowUb, ArithVar skip){
436 : 8107063 : Tableau::RowIterator iter = d_tableau.ridRowIterator(ridx);
437 [ + + ]: 43027502 : for(; !iter.atEnd(); ++iter){
438 : 43026894 : const Tableau::Entry& entry = *iter;
439 : :
440 : 43026894 : ArithVar var = entry.getColVar();
441 [ + + ]: 43026894 : if(var == skip) { continue; }
442 : :
443 : 43025988 : int sgn = entry.getCoefficient().sgn();
444 : 43025988 : bool selectUb = (rowUb == (sgn > 0));
445 [ + + ]: 43025988 : bool hasBound = selectUb ?
446 : 21722556 : d_variables.hasUpperBound(var):
447 : 21303432 : d_variables.hasLowerBound(var);
448 [ + + ]: 43025988 : if(!hasBound){
449 : 8106455 : return &entry;
450 : : }
451 : : }
452 : 608 : return NULL;
453 : : }
454 : :
455 : 106 : void LinearEqualityModule::propagateBasicFromRow(NodeManager* nm,
456 : : ConstraintP c,
457 : : bool produceProofs)
458 : : {
459 [ - + ][ - + ]: 106 : Assert(c != NullConstraint);
[ - - ]
460 [ + + ][ + - ]: 106 : Assert(c->isUpperBound() || c->isLowerBound());
[ - + ][ - + ]
[ - - ]
461 [ - + ][ - + ]: 106 : Assert(!c->assertedToTheTheory());
[ - - ]
462 [ - + ][ - + ]: 106 : Assert(!c->hasProof());
[ - - ]
463 : :
464 : 106 : bool upperBound = c->isUpperBound();
465 : 106 : ArithVar basic = c->getVariable();
466 : 106 : RowIndex ridx = d_tableau.basicToRowIndex(basic);
467 : :
468 : 106 : ConstraintCPVec bounds;
469 [ - + ]: 106 : RationalVectorP coeffs = produceProofs ? new RationalVector() : nullptr;
470 : 106 : propagateRow(bounds, ridx, upperBound, c, coeffs);
471 : 106 : c->impliedByFarkas(nm, bounds, coeffs, false);
472 : 106 : c->tryToPropagate();
473 : :
474 [ - + ][ - - ]: 106 : if(coeffs != RationalVectorPSentinel) { delete coeffs; }
475 : 106 : }
476 : :
477 : : /* An explanation of the farkas coefficients.
478 : : *
479 : : * We are proving c using the other variables on the row.
480 : : * The proof is in terms of the other constraints and the negation of c, ~c.
481 : : *
482 : : * A row has the form:
483 : : * sum a_i * x_i = 0
484 : : * or
485 : : * sx + sum r y + sum q z = 0
486 : : * where r > 0 and q < 0.
487 : : *
488 : : * If rowUp, we are proving c
489 : : * g = sum r u_y + sum q l_z
490 : : * and c is entailed by -sx <= g
491 : : * If !rowUp, we are proving c
492 : : * g = sum r l_y + sum q u_z
493 : : * and c is entailed by -sx >= g
494 : : *
495 : : * | s | c | ~c | u_i | l_i
496 : : * if rowUp | s > 0 | x >= -g/s | x < -g/s | a_i > 0 | a_i < 0
497 : : * if rowUp | s < 0 | x <= -g/s | x > -g/s | a_i > 0 | a_i < 0
498 : : * if !rowUp | s > 0 | x <= -g/s | x > -g/s | a_i < 0 | a_i > 0
499 : : * if !rowUp | s < 0 | x >= -g/s | x < -g/s | a_i < 0 | a_i > 0
500 : : *
501 : : *
502 : : * Thus we treat !rowUp as multiplying the row by -1 and rowUp as 1
503 : : * for the entire row.
504 : : */
505 : 238536 : void LinearEqualityModule::propagateRow(ConstraintCPVec& into, RowIndex ridx, bool rowUp, ConstraintP c, RationalVectorP farkas){
506 [ - + ][ - + ]: 238536 : Assert(!c->assertedToTheTheory());
[ - - ]
507 [ - + ][ - + ]: 238536 : Assert(c->canBePropagated());
[ - - ]
508 [ - + ][ - + ]: 238536 : Assert(!c->hasProof());
[ - - ]
509 : :
510 [ + + ]: 238536 : if(farkas != RationalVectorPSentinel){
511 [ - + ][ - + ]: 163063 : Assert(farkas->empty());
[ - - ]
512 : 163063 : farkas->push_back(Rational(0));
513 : : }
514 : :
515 : 238536 : ArithVar v = c->getVariable();
516 [ + - ]: 477072 : Trace("arith::propagateRow") << "LinearEqualityModule::propagateRow("
517 : 238536 : << ridx << ", " << rowUp << ", " << v << ") start" << endl;
518 : :
519 [ + + ]: 238536 : const Rational& multiple = rowUp ? d_one : d_negOne;
520 : :
521 [ + - ]: 238536 : Trace("arith::propagateRow") << "multiple: " << multiple << endl;
522 : :
523 : 238536 : Tableau::RowIterator iter = d_tableau.ridRowIterator(ridx);
524 [ + + ]: 1913683 : for(; !iter.atEnd(); ++iter){
525 : 1675147 : const Tableau::Entry& entry = *iter;
526 : 1675147 : ArithVar nonbasic = entry.getColVar();
527 : 1675147 : const Rational& a_ij = entry.getCoefficient();
528 : 1675147 : int sgn = a_ij.sgn();
529 [ - + ][ - + ]: 1675147 : Assert(sgn != 0);
[ - - ]
530 [ + + ]: 1675147 : bool selectUb = rowUp ? (sgn > 0) : (sgn < 0);
531 : :
532 [ + + ][ + + ]: 1675147 : Assert(nonbasic != v || (rowUp && a_ij.sgn() > 0 && c->isLowerBound())
[ + + ][ + + ]
[ + - ][ + + ]
[ + + ][ + + ]
[ + - ][ + + ]
[ + - ][ + + ]
[ + + ][ + - ]
[ + + ][ + + ]
[ + - ][ + + ]
[ + + ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ - + ][ - + ]
[ - - ]
533 : : || (rowUp && a_ij.sgn() < 0 && c->isUpperBound())
534 : : || (!rowUp && a_ij.sgn() > 0 && c->isUpperBound())
535 : : || (!rowUp && a_ij.sgn() < 0 && c->isLowerBound()));
536 : :
537 [ - + ]: 1675147 : if(TraceIsOn("arith::propagateRow")){
538 [ - - ]: 0 : if(nonbasic == v){
539 [ - - ]: 0 : Trace("arith::propagateRow") << "(target) "
540 : 0 : << rowUp << " "
541 : 0 : << a_ij.sgn() << " "
542 : 0 : << c->isLowerBound() << " "
543 : 0 : << c->isUpperBound() << endl;
544 : :
545 [ - - ]: 0 : Trace("arith::propagateRow") << "(target) ";
546 : : }
547 [ - - ]: 0 : Trace("arith::propagateRow") << "propagateRow " << a_ij << " * " << nonbasic ;
548 : : }
549 : :
550 [ + + ]: 1675147 : if(nonbasic == v){
551 [ + + ]: 238536 : if(farkas != RationalVectorPSentinel){
552 [ - + ][ - + ]: 163063 : Assert(farkas->front().isZero());
[ - - ]
553 : 163063 : Rational multAij = multiple * a_ij;
554 [ + - ]: 163063 : Trace("arith::propagateRow") << "(" << multAij << ") ";
555 : 163063 : farkas->front() = multAij;
556 : 163063 : }
557 : :
558 [ + - ]: 238536 : Trace("arith::propagateRow") << c << endl;
559 : : }else{
560 : :
561 : : ConstraintCP bound = selectUb
562 : 664419 : ? d_variables.getUpperBoundConstraint(nonbasic)
563 [ + + ]: 1436611 : : d_variables.getLowerBoundConstraint(nonbasic);
564 : :
565 [ + + ]: 1436611 : if(farkas != RationalVectorPSentinel){
566 : 967880 : Rational multAij = multiple * a_ij;
567 [ + - ]: 967880 : Trace("arith::propagateRow") << "(" << multAij << ") ";
568 : 967880 : farkas->push_back(multAij);
569 : 967880 : }
570 [ - + ][ - + ]: 1436611 : Assert(bound != NullConstraint);
[ - - ]
571 [ + - ]: 1436611 : Trace("arith::propagateRow") << bound << endl;
572 : 1436611 : into.push_back(bound);
573 : : }
574 : : }
575 [ + - ]: 477072 : Trace("arith::propagateRow") << "LinearEqualityModule::propagateRow("
576 : 238536 : << ridx << ", " << rowUp << ", " << v << ") done" << endl;
577 : :
578 : 238536 : }
579 : :
580 : 1287170 : ConstraintP LinearEqualityModule::weakestExplanation(bool aboveUpper, DeltaRational& surplus, ArithVar v, const Rational& coeff, bool& anyWeakening, ArithVar basic) const {
581 : :
582 : 1287170 : int sgn = coeff.sgn();
583 [ + + ]: 1287170 : bool ub = aboveUpper?(sgn < 0) : (sgn > 0);
584 : :
585 [ + + ]: 1287170 : ConstraintP c = ub ?
586 : 433974 : d_variables.getUpperBoundConstraint(v) :
587 : 1287170 : d_variables.getLowerBoundConstraint(v);
588 : :
589 : : bool weakened;
590 [ + + ]: 1459978 : do{
591 : 1459978 : const DeltaRational& bound = c->getValue();
592 : :
593 : 1459978 : weakened = false;
594 : :
595 [ + + ]: 1459978 : ConstraintP weaker = ub?
596 : 546289 : c->getStrictlyWeakerUpperBound(true, true):
597 : 913689 : c->getStrictlyWeakerLowerBound(true, true);
598 : :
599 [ + + ]: 1459978 : if(weaker != NullConstraint){
600 : 354797 : const DeltaRational& weakerBound = weaker->getValue();
601 : :
602 [ + + ]: 354797 : DeltaRational diff = aboveUpper ? bound - weakerBound : weakerBound - bound;
603 : : //if var == basic,
604 : : // if aboveUpper, weakerBound > bound, multiply by -1
605 : : // if !aboveUpper, weakerBound < bound, multiply by -1
606 : 354797 : diff = diff * coeff;
607 [ + + ]: 354797 : if(surplus > diff){
608 : 172808 : ++d_statistics.d_weakenings;
609 : 172808 : weakened = true;
610 : 172808 : anyWeakening = true;
611 : 172808 : surplus = surplus - diff;
612 : :
613 [ + - ]: 172808 : Trace("arith::weak") << "found:" << endl;
614 [ + + ]: 172808 : if(v == basic){
615 [ + - ]: 18454 : Trace("arith::weak") << " basic: ";
616 : : }
617 [ + - ]: 345616 : Trace("arith::weak") << " " << surplus << " "<< diff << endl
618 : 0 : << " " << bound << c << endl
619 : 172808 : << " " << weakerBound << weaker << endl;
620 : :
621 [ - + ][ - + ]: 172808 : Assert(diff.sgn() > 0);
[ - - ]
622 : 172808 : c = weaker;
623 : : }
624 : 354797 : }
625 : : }while(weakened);
626 : :
627 : 1287170 : return c;
628 : : }
629 : :
630 : : /* An explanation of the farkas coefficients.
631 : : *
632 : : * We are proving a conflict on the basic variable x_b.
633 : : * If aboveUpper, then the conflict is with the constraint c : x_b <= u_b.
634 : : * If !aboveUpper, then the conflict is with the constraint c : x_b >= l_b.
635 : : *
636 : : * A row has the form:
637 : : * -x_b sum a_i * x_i = 0
638 : : * or
639 : : * -x_b + sum r y + sum q z = 0,
640 : : * x_b = sum r y + sum q z
641 : : * where r > 0 and q < 0.
642 : : *
643 : : *
644 : : * If !aboveUp, we are proving ~c: x_b < l_b
645 : : * g = sum r u_y + sum q l_z
646 : : * x_b <= g < l_b
647 : : * and ~c is entailed by x_b <= g
648 : : *
649 : : * If aboveUp, we are proving ~c : x_b > u_b
650 : : * g = sum r l_y + sum q u_z
651 : : * x_b >= g > u_b
652 : : * and ~c is entailed by x_b >= g
653 : : *
654 : : *
655 : : * | s | c | ~c | u_i | l_i
656 : : * if !aboveUp | s > 0 | x >= -g/s | x < -g/s | a_i > 0 | a_i < 0
657 : : * if !aboveUp | s < 0 | x <= -g/s | x > -g/s | a_i > 0 | a_i < 0
658 : : * if aboveUp | s > 0 | x <= -g/s | x > -g/s | a_i < 0 | a_i > 0
659 : : * if aboveUp | s < 0 | x >= -g/s | x < -g/s | a_i < 0 | a_i > 0
660 : : *
661 : : * Thus we treat aboveUp as multiplying the row by -1 and !aboveUp as 1
662 : : * for the entire row.
663 : : */
664 : 103498 : ConstraintCP LinearEqualityModule::minimallyWeakConflict(
665 : : NodeManager* nm,
666 : : bool aboveUpper,
667 : : ArithVar basicVar,
668 : : FarkasConflictBuilder& fcs) const
669 : : {
670 [ - + ][ - + ]: 103498 : Assert(!fcs.underConstruction());
[ - - ]
671 : 103498 : TimerStat::CodeTimer codeTimer(d_statistics.d_weakenTime);
672 : :
673 [ + - ]: 206996 : Trace("arith::weak") << "LinearEqualityModule::minimallyWeakConflict("
674 : 103498 : << aboveUpper <<", "<< basicVar << ", ...) start" << endl;
675 : :
676 [ + + ]: 103498 : const Rational& adjustSgn = aboveUpper ? d_negOne : d_one;
677 : 103498 : const DeltaRational& assignment = d_variables.getAssignment(basicVar);
678 : 103498 : DeltaRational surplus;
679 [ + + ]: 103498 : if(aboveUpper){
680 [ - + ][ - + ]: 49852 : Assert(d_variables.hasUpperBound(basicVar));
[ - - ]
681 [ - + ][ - + ]: 49852 : Assert(assignment > d_variables.getUpperBound(basicVar));
[ - - ]
682 : 49852 : surplus = assignment - d_variables.getUpperBound(basicVar);
683 : : }else{
684 [ - + ][ - + ]: 53646 : Assert(d_variables.hasLowerBound(basicVar));
[ - - ]
685 [ - + ][ - + ]: 53646 : Assert(assignment < d_variables.getLowerBound(basicVar));
[ - - ]
686 : 53646 : surplus = d_variables.getLowerBound(basicVar) - assignment;
687 : : }
688 : :
689 : 103498 : bool anyWeakenings = false;
690 [ + + ]: 1390668 : for(Tableau::RowIterator i = d_tableau.basicRowIterator(basicVar); !i.atEnd(); ++i){
691 : 1287170 : const Tableau::Entry& entry = *i;
692 : 1287170 : ArithVar v = entry.getColVar();
693 : 1287170 : const Rational& coeff = entry.getCoefficient();
694 : 1287170 : bool weakening = false;
695 : 1287170 : ConstraintP c = weakestExplanation(aboveUpper, surplus, v, coeff, weakening, basicVar);
696 [ + - ]: 2574340 : Trace("arith::weak") << "weak : " << weakening << " "
697 : 1287170 : << c->assertedToTheTheory() << " "
698 : 0 : << d_variables.getAssignment(v) << " "
699 : 1287170 : << c << endl;
700 [ + + ][ + + ]: 1287170 : anyWeakenings = anyWeakenings || weakening;
701 : :
702 : 1287170 : fcs.addConstraint(c, coeff, adjustSgn);
703 [ + + ]: 1287170 : if(basicVar == v){
704 [ - + ][ - + ]: 103498 : Assert(!c->negationHasProof());
[ - - ]
705 : 103498 : fcs.makeLastConsequent();
706 : : }
707 : : }
708 [ - + ][ - + ]: 103498 : Assert(fcs.consequentIsSet());
[ - - ]
709 : :
710 : 103498 : ConstraintCP conflicted = fcs.commitConflict(nm);
711 : :
712 : 103498 : ++d_statistics.d_weakeningAttempts;
713 [ + + ]: 103498 : if(anyWeakenings){
714 : 79715 : ++d_statistics.d_weakeningSuccesses;
715 : : }
716 [ + - ]: 206996 : Trace("arith::weak") << "LinearEqualityModule::minimallyWeakConflict("
717 : 103498 : << aboveUpper <<", "<< basicVar << ", ...) done" << endl;
718 : 103498 : return conflicted;
719 : 103498 : }
720 : :
721 : 219954 : ArithVar LinearEqualityModule::minVarOrder(ArithVar x, ArithVar y) const {
722 [ - + ][ - + ]: 219954 : Assert(x != ARITHVAR_SENTINEL);
[ - - ]
723 [ - + ][ - + ]: 219954 : Assert(y != ARITHVAR_SENTINEL);
[ - - ]
724 [ + + ]: 219954 : if(x <= y){
725 : 130860 : return x;
726 : : } else {
727 : 89094 : return y;
728 : : }
729 : : }
730 : :
731 : 1337448 : ArithVar LinearEqualityModule::minColLength(ArithVar x, ArithVar y) const {
732 [ - + ][ - + ]: 1337448 : Assert(x != ARITHVAR_SENTINEL);
[ - - ]
733 [ - + ][ - + ]: 1337448 : Assert(y != ARITHVAR_SENTINEL);
[ - - ]
734 [ - + ][ - + ]: 1337448 : Assert(!d_tableau.isBasic(x));
[ - - ]
735 [ - + ][ - + ]: 1337448 : Assert(!d_tableau.isBasic(y));
[ - - ]
736 : 1337448 : uint32_t xLen = d_tableau.getColLength(x);
737 : 1337448 : uint32_t yLen = d_tableau.getColLength(y);
738 [ + + ]: 1337448 : if( xLen > yLen){
739 : 214338 : return y;
740 [ + + ]: 1123110 : } else if( xLen== yLen ){
741 : 218596 : return minVarOrder(x,y);
742 : : }else{
743 : 904514 : return x;
744 : : }
745 : : }
746 : :
747 : 0 : ArithVar LinearEqualityModule::minRowLength(ArithVar x, ArithVar y) const {
748 : 0 : Assert(x != ARITHVAR_SENTINEL);
749 : 0 : Assert(y != ARITHVAR_SENTINEL);
750 : 0 : Assert(d_tableau.isBasic(x));
751 : 0 : Assert(d_tableau.isBasic(y));
752 : 0 : uint32_t xLen = d_tableau.basicRowLength(x);
753 : 0 : uint32_t yLen = d_tableau.basicRowLength(y);
754 [ - - ]: 0 : if( xLen > yLen){
755 : 0 : return y;
756 [ - - ]: 0 : } else if( xLen== yLen ){
757 : 0 : return minVarOrder(x,y);
758 : : }else{
759 : 0 : return x;
760 : : }
761 : : }
762 : :
763 : 1420543 : ArithVar LinearEqualityModule::minBoundAndColLength(ArithVar x, ArithVar y) const{
764 [ - + ][ - + ]: 1420543 : Assert(x != ARITHVAR_SENTINEL);
[ - - ]
765 [ - + ][ - + ]: 1420543 : Assert(y != ARITHVAR_SENTINEL);
[ - - ]
766 [ - + ][ - + ]: 1420543 : Assert(!d_tableau.isBasic(x));
[ - - ]
767 [ - + ][ - + ]: 1420543 : Assert(!d_tableau.isBasic(y));
[ - - ]
768 [ + + ][ + + ]: 1420543 : if(d_variables.hasEitherBound(x) && !d_variables.hasEitherBound(y)){
[ + + ]
769 : 33116 : return y;
770 [ + + ][ + + ]: 1387427 : }else if(!d_variables.hasEitherBound(x) && d_variables.hasEitherBound(y)){
[ + + ]
771 : 49979 : return x;
772 : : }else {
773 : 1337448 : return minColLength(x, y);
774 : : }
775 : : }
776 : :
777 : : template <bool above>
778 : 357192 : ArithVar LinearEqualityModule::selectSlack(ArithVar x_i, VarPreferenceFunction pref) const{
779 : 357192 : ArithVar slack = ARITHVAR_SENTINEL;
780 : :
781 [ + + ]: 8020985 : for(Tableau::RowIterator iter = d_tableau.basicRowIterator(x_i); !iter.atEnd(); ++iter){
782 : 7663793 : const Tableau::Entry& entry = *iter;
783 : 7663793 : ArithVar nonbasic = entry.getColVar();
784 [ + + ]: 7663793 : if(nonbasic == x_i) continue;
785 : :
786 : 7306601 : const Rational& a_ij = entry.getCoefficient();
787 : 7306601 : int sgn = a_ij.sgn();
788 [ + + ]: 7306601 : if(isAcceptableSlack<above>(sgn, nonbasic)){
789 : : //If one of the above conditions is met, we have found an acceptable
790 : : //nonbasic variable to pivot x_i with. We can now choose which one we
791 : : //prefer the most.
792 [ + + ][ - + ]: 1727035 : slack = (slack == ARITHVAR_SENTINEL) ? nonbasic : (this->*pref)(slack, nonbasic);
793 : : }
794 : : }
795 : :
796 : 357192 : return slack;
797 : : }
798 : :
799 : 0 : const Tableau::Entry* LinearEqualityModule::selectSlackEntry(ArithVar x_i, bool above) const{
800 [ - - ]: 0 : for(Tableau::RowIterator iter = d_tableau.basicRowIterator(x_i); !iter.atEnd(); ++iter){
801 : 0 : const Tableau::Entry& entry = *iter;
802 : 0 : ArithVar nonbasic = entry.getColVar();
803 [ - - ]: 0 : if(nonbasic == x_i) continue;
804 : :
805 : 0 : const Rational& a_ij = entry.getCoefficient();
806 : 0 : int sgn = a_ij.sgn();
807 : 0 : if(above && isAcceptableSlack<true>(sgn, nonbasic)){
808 : : //If one of the above conditions is met, we have found an acceptable
809 : : //nonbasic variable to pivot x_i with. We can now choose which one we
810 : : //prefer the most.
811 : 0 : return &entry;
812 : 0 : }else if(!above && isAcceptableSlack<false>(sgn, nonbasic)){
813 : 0 : return &entry;
814 : : }
815 : : }
816 : :
817 : 0 : return NULL;
818 : : }
819 : :
820 : 3259788 : void LinearEqualityModule::startTrackingBoundCounts(){
821 [ - + ][ - + ]: 3259788 : Assert(!d_areTracking);
[ - - ]
822 : 3259788 : d_areTracking = true;
823 [ - + ]: 3259788 : if(TraceIsOn("arith::tracking")){
824 : 0 : debugCheckTracking();
825 : : }
826 [ - + ][ - + ]: 3259788 : Assert(d_areTracking);
[ - - ]
827 : 3259788 : }
828 : :
829 : 3259788 : void LinearEqualityModule::stopTrackingBoundCounts(){
830 [ - + ][ - + ]: 3259788 : Assert(d_areTracking);
[ - - ]
831 : 3259788 : d_areTracking = false;
832 [ - + ]: 3259788 : if(TraceIsOn("arith::tracking")){
833 : 0 : debugCheckTracking();
834 : : }
835 [ - + ][ - + ]: 3259788 : Assert(!d_areTracking);
[ - - ]
836 : 3259788 : }
837 : :
838 : :
839 : 200088 : void LinearEqualityModule::trackRowIndex(RowIndex ridx){
840 [ - + ][ - + ]: 200088 : Assert(!rowIndexIsTracked(ridx));
[ - - ]
841 : 200088 : BoundsInfo bi = computeRowBoundInfo(ridx, true);
842 : 200088 : d_btracking.set(ridx, bi);
843 : 200088 : }
844 : :
845 : 200088 : BoundsInfo LinearEqualityModule::computeRowBoundInfo(RowIndex ridx, bool inQueue) const{
846 : 200088 : BoundsInfo bi;
847 : :
848 : 200088 : Tableau::RowIterator iter = d_tableau.ridRowIterator(ridx);
849 [ + + ]: 1204362 : for(; !iter.atEnd(); ++iter){
850 : 1004274 : const Tableau::Entry& entry = *iter;
851 : 1004274 : ArithVar v = entry.getColVar();
852 : 1004274 : const Rational& a_ij = entry.getCoefficient();
853 : 1004274 : bi += (d_variables.selectBoundsInfo(v, inQueue)).multiplyBySgn(a_ij.sgn());
854 : : }
855 : 200088 : return bi;
856 : : }
857 : :
858 : 0 : BoundCounts LinearEqualityModule::debugBasicAtBoundCount(ArithVar x_i) const {
859 : 0 : return d_btracking[d_tableau.basicToRowIndex(x_i)].atBounds();
860 : : }
861 : :
862 : : /**
863 : : * If the pivot described in u were performed,
864 : : * then the row would qualify as being either at the minimum/maximum
865 : : * to the non-basics being at their bounds.
866 : : * The minimum/maximum is determined by the direction the non-basic is changing.
867 : : */
868 : 87236 : bool LinearEqualityModule::basicsAtBounds(const UpdateInfo& u) const {
869 [ - + ][ - + ]: 87236 : Assert(u.describesPivot());
[ - - ]
870 : :
871 : 87236 : ArithVar nonbasic = u.nonbasic();
872 : 87236 : ArithVar basic = u.leaving();
873 [ - + ][ - + ]: 87236 : Assert(basicIsTracked(basic));
[ - - ]
874 : 87236 : int coeffSgn = u.getCoefficient().sgn();
875 : 87236 : int nbdir = u.nonbasicDirection();
876 : :
877 : 87236 : ConstraintP c = u.limiting();
878 [ + + ]: 145259 : int toUB = (c->getType() == UpperBound ||
879 [ + + ]: 145259 : c->getType() == Equality) ? 1 : 0;
880 [ + + ]: 122963 : int toLB = (c->getType() == LowerBound ||
881 [ + + ]: 122963 : c->getType() == Equality) ? 1 : 0;
882 : :
883 : 87236 : RowIndex ridx = d_tableau.basicToRowIndex(basic);
884 : :
885 : 87236 : BoundCounts bcs = d_btracking[ridx].atBounds();
886 : : // x = c*n + \sum d*m
887 : : // 0 = -x + c*n + \sum d*m
888 : : // n = 1/c * x + -1/c * (\sum d*m)
889 : 87236 : BoundCounts nonb = bcs - d_variables.atBoundCounts(nonbasic).multiplyBySgn(coeffSgn);
890 : 87236 : nonb.addInChange(-1, d_variables.atBoundCounts(basic), BoundCounts(toLB, toUB));
891 : 87236 : nonb = nonb.multiplyBySgn(-coeffSgn);
892 : :
893 : 87236 : uint32_t length = d_tableau.basicRowLength(basic);
894 [ + - ]: 174472 : Trace("basicsAtBounds")
895 : 0 : << "bcs " << bcs
896 : 0 : << "nonb " << nonb
897 : 87236 : << "length " << length << endl;
898 : : // nonb has nb excluded.
899 [ + + ]: 87236 : if(nbdir < 0){
900 : 44684 : return nonb.lowerBoundCount() + 1 == length;
901 : : }else{
902 [ - + ][ - + ]: 42552 : Assert(nbdir > 0);
[ - - ]
903 : 42552 : return nonb.upperBoundCount() + 1 == length;
904 : : }
905 : : }
906 : :
907 : 702777 : bool LinearEqualityModule::nonbasicsAtLowerBounds(ArithVar basic) const {
908 [ - + ][ - + ]: 702777 : Assert(basicIsTracked(basic));
[ - - ]
909 : 702777 : RowIndex ridx = d_tableau.basicToRowIndex(basic);
910 : :
911 : 702777 : BoundCounts bcs = d_btracking[ridx].atBounds();
912 : 702777 : uint32_t length = d_tableau.basicRowLength(basic);
913 : :
914 : : // return true if excluding the basic is every element is at its "lowerbound"
915 : : // The psuedo code is:
916 : : // bcs -= basic.count(basic, basic's sgn)
917 : : // return bcs.lowerBoundCount() + 1 == length
918 : : // As basic's sign is always -1, we can pull out the pieces of the count:
919 : : // bcs.lowerBoundCount() - basic.atUpperBoundInd() + 1 == length
920 : : // basic.atUpperBoundInd() is either 0 or 1
921 : 702777 : uint32_t lbc = bcs.lowerBoundCount();
922 [ + - ]: 1405554 : return (lbc == length) ||
923 [ + + ][ + - ]: 1405554 : (lbc + 1 == length && d_variables.cmpAssignmentUpperBound(basic) != 0);
924 : : }
925 : :
926 : 729246 : bool LinearEqualityModule::nonbasicsAtUpperBounds(ArithVar basic) const {
927 [ - + ][ - + ]: 729246 : Assert(basicIsTracked(basic));
[ - - ]
928 : 729246 : RowIndex ridx = d_tableau.basicToRowIndex(basic);
929 : 729246 : BoundCounts bcs = d_btracking[ridx].atBounds();
930 : 729246 : uint32_t length = d_tableau.basicRowLength(basic);
931 : 729246 : uint32_t ubc = bcs.upperBoundCount();
932 : : // See the comment for nonbasicsAtLowerBounds()
933 : :
934 [ + - ]: 1458492 : return (ubc == length) ||
935 [ + + ][ + - ]: 1458492 : (ubc + 1 == length && d_variables.cmpAssignmentLowerBound(basic) != 0);
936 : : }
937 : :
938 : 364468 : void LinearEqualityModule::trackingMultiplyRow(RowIndex ridx, int sgn) {
939 [ - + ][ - + ]: 364468 : Assert(rowIndexIsTracked(ridx));
[ - - ]
940 [ - + ][ - + ]: 364468 : Assert(sgn != 0);
[ - - ]
941 [ + + ]: 364468 : if(sgn < 0){
942 : 205138 : BoundsInfo& bi = d_btracking.get(ridx);
943 : 205138 : bi = bi.multiplyBySgn(sgn);
944 : : }
945 : 364468 : }
946 : :
947 : 87719333 : void LinearEqualityModule::trackingCoefficientChange(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn){
948 [ - + ][ - + ]: 87719333 : Assert(oldSgn != currSgn);
[ - - ]
949 : 87719333 : BoundsInfo nb_inf = d_variables.boundsInfo(nb);
950 : :
951 [ - + ][ - + ]: 87719333 : Assert(rowIndexIsTracked(ridx));
[ - - ]
952 : :
953 : 87719333 : BoundsInfo& row_bi = d_btracking.get(ridx);
954 : 87719333 : row_bi.addInSgn(nb_inf, oldSgn, currSgn);
955 : 87719333 : }
956 : :
957 : 0 : ArithVar LinearEqualityModule::minBy(const ArithVarVec& vec, VarPreferenceFunction pf) const{
958 [ - - ]: 0 : if(vec.empty()) {
959 : 0 : return ARITHVAR_SENTINEL;
960 : : }else {
961 : 0 : ArithVar sel = vec.front();
962 : 0 : ArithVarVec::const_iterator i = vec.begin() + 1;
963 : 0 : ArithVarVec::const_iterator i_end = vec.end();
964 [ - - ]: 0 : for(; i != i_end; ++i){
965 [ - - ]: 0 : sel = (this->*pf)(sel, *i);
966 : : }
967 : 0 : return sel;
968 : : }
969 : : }
970 : :
971 : 1976401 : bool LinearEqualityModule::accumulateBorder(const Tableau::Entry& entry, bool ub){
972 : 1976401 : ArithVar currBasic = d_tableau.rowIndexToBasic(entry.getRowIndex());
973 : :
974 [ - + ][ - + ]: 1976401 : Assert(basicIsTracked(currBasic));
[ - - ]
975 : :
976 [ + + ]: 1976401 : ConstraintP bound = ub ?
977 : 988218 : d_variables.getUpperBoundConstraint(currBasic):
978 : 988183 : d_variables.getLowerBoundConstraint(currBasic);
979 : :
980 [ + + ]: 1976401 : if(bound == NullConstraint){ return false; }
981 [ - + ][ - + ]: 231277 : Assert(bound != NullConstraint);
[ - - ]
982 : :
983 : 231277 : const Rational& coeff = entry.getCoefficient();
984 : :
985 : 231277 : const DeltaRational& assignment = d_variables.getAssignment(currBasic);
986 : 231277 : DeltaRational toBound = bound->getValue() - assignment;
987 : 231277 : DeltaRational nbDiff = toBound/coeff;
988 : :
989 : : // if ub
990 : : // if toUB >= 0
991 : : // then ub >= currBasic
992 : : // if sgn > 0,
993 : : // then diff >= 0, so nb must increase for G
994 : : // else diff <= 0, so nb must decrease for G
995 : : // else ub < currBasic
996 : : // if sgn > 0,
997 : : // then diff < 0, so nb must decrease for G
998 : : // else diff > 0, so nb must increase for G
999 : :
1000 : 231277 : int diffSgn = nbDiff.sgn();
1001 : :
1002 [ + + ][ + + ]: 231277 : if(diffSgn != 0 && willBeInConflictAfterPivot(entry, nbDiff, ub)){
[ + + ]
1003 : 67 : return true;
1004 : : }else{
1005 [ + + ]: 231210 : bool areFixing = ub ? (toBound.sgn() < 0 ) : (toBound.sgn() > 0);
1006 : 231210 : Border border(bound, nbDiff, areFixing, &entry, ub);
1007 : : bool increasing =
1008 [ + + ][ + + ]: 300228 : (diffSgn > 0) ||
1009 [ + + ]: 69018 : (diffSgn == 0 && ((coeff.sgn() > 0) == ub));
1010 : :
1011 : : // assume diffSgn == 0
1012 : : // if coeff > 0,
1013 : : // if ub, inc
1014 : : // else, dec
1015 : : // else coeff < 0
1016 : : // if ub, dec
1017 : : // else, inc
1018 : :
1019 [ + + ]: 231210 : if(increasing){
1020 [ + - ]: 113535 : Trace("handleBorders") << "push back increasing " << border << endl;
1021 : 113535 : d_increasing.push_back(border);
1022 : : }else{
1023 [ + - ]: 117675 : Trace("handleBorders") << "push back decreasing " << border << endl;
1024 : 117675 : d_decreasing.push_back(border);
1025 : : }
1026 : 231210 : return false;
1027 : 231210 : }
1028 : 231277 : }
1029 : :
1030 : 162259 : bool LinearEqualityModule::willBeInConflictAfterPivot(const Tableau::Entry& entry, const DeltaRational& nbDiff, bool bToUB) const{
1031 : 162259 : int nbSgn = nbDiff.sgn();
1032 [ - + ][ - + ]: 162259 : Assert(nbSgn != 0);
[ - - ]
1033 : :
1034 [ + + ]: 162259 : if(nbSgn > 0){
1035 [ + + ][ + + ]: 81174 : if (!d_upperBoundDifference || nbDiff <= *d_upperBoundDifference)
[ + + ]
1036 : : {
1037 : 63727 : return false;
1038 : : }
1039 : : }else{
1040 [ + + ][ + + ]: 81085 : if (!d_lowerBoundDifference || nbDiff >= *d_lowerBoundDifference)
[ + + ]
1041 : : {
1042 : 60798 : return false;
1043 : : }
1044 : : }
1045 : :
1046 : : // Assume past this point, nb will be in error if this pivot is done
1047 : 37734 : ArithVar nb = entry.getColVar();
1048 : 37734 : RowIndex ridx = entry.getRowIndex();
1049 : 37734 : ArithVar basic = d_tableau.rowIndexToBasic(ridx);
1050 [ - + ][ - + ]: 37734 : Assert(rowIndexIsTracked(ridx));
[ - - ]
1051 : 37734 : int coeffSgn = entry.getCoefficient().sgn();
1052 : :
1053 : :
1054 : : // if bToUB, then basic is going to be set to its upperbound
1055 : : // if not bToUB, then basic is going to be set to its lowerbound
1056 : :
1057 : : // Different steps of solving for this:
1058 : : // 1) y = a * x + \sum b * z
1059 : : // 2) -a * x = -y + \sum b * z
1060 : : // 3) x = (-1/a) * ( -y + \sum b * z)
1061 : :
1062 : 37734 : BoundCounts bc = d_btracking[ridx].atBounds();
1063 : :
1064 : : // 1) y = a * x + \sum b * z
1065 : : // Get bc(\sum b * z)
1066 : 37734 : BoundCounts sumOnly = bc - d_variables.atBoundCounts(nb).multiplyBySgn(coeffSgn);
1067 : :
1068 : : // y's bounds in the proposed model
1069 [ + + ][ + + ]: 37734 : int yWillBeAtUb = (bToUB || d_variables.boundsAreEqual(basic)) ? 1 : 0;
1070 [ + + ][ + + ]: 37734 : int yWillBeAtLb = (!bToUB || d_variables.boundsAreEqual(basic)) ? 1 : 0;
1071 : 37734 : BoundCounts ysBounds(yWillBeAtLb, yWillBeAtUb);
1072 : :
1073 : : // 2) -a * x = -y + \sum b * z
1074 : : // Get bc(-y + \sum b * z)
1075 : 37734 : sumOnly.addInChange(-1, d_variables.atBoundCounts(basic), ysBounds);
1076 : :
1077 : : // 3) x = (-1/a) * ( -y + \sum b * z)
1078 : : // Get bc((-1/a) * ( -y + \sum b * z))
1079 : 37734 : BoundCounts xsBoundsAfterPivot = sumOnly.multiplyBySgn(-coeffSgn);
1080 : :
1081 : 37734 : uint32_t length = d_tableau.basicRowLength(basic);
1082 [ + + ]: 37734 : if(nbSgn > 0){
1083 : : // Only check for the upper bound being violated
1084 : 17447 : return xsBoundsAfterPivot.lowerBoundCount() + 1 == length;
1085 : : }else{
1086 : : // Only check for the lower bound being violated
1087 : 20287 : return xsBoundsAfterPivot.upperBoundCount() + 1 == length;
1088 : : }
1089 : : }
1090 : :
1091 : 67 : UpdateInfo LinearEqualityModule::mkConflictUpdate(const Tableau::Entry& entry, bool ub) const{
1092 : 67 : ArithVar currBasic = d_tableau.rowIndexToBasic(entry.getRowIndex());
1093 : 67 : ArithVar nb = entry.getColVar();
1094 : :
1095 [ + + ]: 67 : ConstraintP bound = ub ?
1096 : 35 : d_variables.getUpperBoundConstraint(currBasic):
1097 : 32 : d_variables.getLowerBoundConstraint(currBasic);
1098 : :
1099 : :
1100 : 67 : const Rational& coeff = entry.getCoefficient();
1101 : 67 : const DeltaRational& assignment = d_variables.getAssignment(currBasic);
1102 : 67 : DeltaRational toBound = bound->getValue() - assignment;
1103 : 67 : DeltaRational nbDiff = toBound/coeff;
1104 : :
1105 : 134 : return UpdateInfo::conflict(nb, nbDiff, coeff, bound);
1106 : 67 : }
1107 : :
1108 : 25935 : UpdateInfo LinearEqualityModule::speculativeUpdate(ArithVar nb, const Rational& focusCoeff, UpdatePreferenceFunction pref){
1109 [ - + ][ - + ]: 25935 : Assert(d_increasing.empty());
[ - - ]
1110 [ - + ][ - + ]: 25935 : Assert(d_decreasing.empty());
[ - - ]
1111 [ - + ][ - + ]: 25935 : Assert(!d_lowerBoundDifference);
[ - - ]
1112 [ - + ][ - + ]: 25935 : Assert(!d_upperBoundDifference);
[ - - ]
1113 : :
1114 : 25935 : int focusCoeffSgn = focusCoeff.sgn();
1115 : :
1116 [ + - ]: 25935 : Trace("speculativeUpdate") << "speculativeUpdate" << endl;
1117 [ + - ]: 25935 : Trace("speculativeUpdate") << "nb " << nb << endl;
1118 [ + - ]: 25935 : Trace("speculativeUpdate") << "focusCoeff " << focusCoeff << endl;
1119 : :
1120 [ + + ]: 25935 : if(d_variables.hasUpperBound(nb)){
1121 : 5395 : ConstraintP ub = d_variables.getUpperBoundConstraint(nb);
1122 : 5395 : d_upperBoundDifference = ub->getValue() - d_variables.getAssignment(nb);
1123 : 5395 : Border border(ub, *d_upperBoundDifference, false, NULL, true);
1124 [ + - ]: 5395 : Trace("handleBorders") << "push back increasing " << border << endl;
1125 : 5395 : d_increasing.push_back(border);
1126 : 5395 : }
1127 [ + + ]: 25935 : if(d_variables.hasLowerBound(nb)){
1128 : 6966 : ConstraintP lb = d_variables.getLowerBoundConstraint(nb);
1129 : 6966 : d_lowerBoundDifference = lb->getValue() - d_variables.getAssignment(nb);
1130 : 6966 : Border border(lb, *d_lowerBoundDifference, false, NULL, false);
1131 [ + - ]: 6966 : Trace("handleBorders") << "push back decreasing " << border << endl;
1132 : 6966 : d_decreasing.push_back(border);
1133 : 6966 : }
1134 : :
1135 : 25935 : Tableau::ColIterator colIter = d_tableau.colIterator(nb);
1136 [ + + ]: 1014086 : for(; !colIter.atEnd(); ++colIter){
1137 : 988218 : const Tableau::Entry& entry = *colIter;
1138 [ - + ][ - + ]: 988218 : Assert(entry.getColVar() == nb);
[ - - ]
1139 : :
1140 [ + + ]: 988218 : if(accumulateBorder(entry, true)){
1141 : 35 : clearSpeculative();
1142 : 35 : return mkConflictUpdate(entry, true);
1143 : : }
1144 [ + + ]: 988183 : if(accumulateBorder(entry, false)){
1145 : 32 : clearSpeculative();
1146 : 32 : return mkConflictUpdate(entry, false);
1147 : : }
1148 : : }
1149 : :
1150 : 25868 : UpdateInfo selected;
1151 [ + + ]: 25868 : BorderHeap& withSgn = focusCoeffSgn > 0 ? d_increasing : d_decreasing;
1152 [ + + ]: 25868 : BorderHeap& againstSgn = focusCoeffSgn > 0 ? d_decreasing : d_increasing;
1153 : :
1154 : 25868 : handleBorders(selected, nb, focusCoeff, withSgn, 0, pref);
1155 : 25868 : int m = 1 - selected.errorsChangeSafe(0);
1156 : 25868 : handleBorders(selected, nb, focusCoeff, againstSgn, m, pref);
1157 : :
1158 : 25868 : clearSpeculative();
1159 : 25868 : return selected;
1160 : 25868 : }
1161 : :
1162 : 25935 : void LinearEqualityModule::clearSpeculative(){
1163 : : // clear everything away
1164 : 25935 : d_increasing.clear();
1165 : 25935 : d_decreasing.clear();
1166 : 25935 : d_lowerBoundDifference.reset();
1167 : 25935 : d_upperBoundDifference.reset();
1168 : 25935 : }
1169 : :
1170 : 51736 : void LinearEqualityModule::handleBorders(UpdateInfo& selected, ArithVar nb, const Rational& focusCoeff, BorderHeap& heap, int minimumFixes, UpdatePreferenceFunction pref){
1171 [ - + ][ - + ]: 51736 : Assert(minimumFixes >= 0);
[ - - ]
1172 : :
1173 : : // The values popped off of the heap
1174 : : // should be popped with the values closest to 0
1175 : : // being first and larger in absolute value last
1176 : :
1177 : :
1178 : 51736 : int fixesRemaining = heap.possibleFixes();
1179 : :
1180 [ + - ]: 103472 : Trace("handleBorders")
1181 : 0 : << "handleBorders "
1182 : 0 : << "nb " << nb
1183 : 0 : << "fc " << focusCoeff
1184 : 0 : << "h.e " << heap.empty()
1185 : 0 : << "h.dir " << heap.direction()
1186 : 0 : << "h.rem " << fixesRemaining
1187 : 51736 : << "h.0s " << heap.numZeroes()
1188 : 0 : << "min " << minimumFixes
1189 : 51736 : << endl;
1190 : :
1191 [ + + ]: 51736 : if(heap.empty()){
1192 : : // if the heap is empty, return
1193 : 25816 : return;
1194 : : }
1195 : :
1196 : 41353 : bool zeroesWillDominate = fixesRemaining - heap.numZeroes() < minimumFixes;
1197 : :
1198 : : // can the number of fixes ever exceed the minimum?
1199 : : // no more than the number of possible fixes can be fixed in total
1200 : : // nothing can be fixed before the zeroes are taken care of
1201 [ + + ][ + + ]: 41353 : if(minimumFixes > 0 && zeroesWillDominate){
1202 : 15433 : return;
1203 : : }
1204 : :
1205 : :
1206 : 25920 : int negErrorChange = 0;
1207 : 25920 : int nbDir = heap.direction();
1208 : :
1209 : : // points at the beginning of the heap
1210 [ + + ]: 25920 : if(zeroesWillDominate){
1211 : 5581 : heap.dropNonZeroes();
1212 : : }
1213 : 25920 : heap.make_heap();
1214 : :
1215 : :
1216 : : // pretend like the previous block had a value of zero.
1217 : : // The block that actually has a value of 0 must handle this.
1218 : 25920 : const DeltaRational zero(0);
1219 : 25920 : const DeltaRational* prevBlockValue = &zero;
1220 : :
1221 : : /** The coefficient changes as the value crosses border. */
1222 : 25920 : Rational effectiveCoefficient = focusCoeff;
1223 : :
1224 : : /* Keeps track of the change to the value of the focus function.*/
1225 : 25920 : DeltaRational totalFocusChange(0);
1226 : :
1227 : 25920 : const int focusCoeffSgn = focusCoeff.sgn();
1228 : :
1229 [ + + ][ + + ]: 99109 : while(heap.more() &&
1230 [ + + ]: 41274 : (fixesRemaining + negErrorChange > minimumFixes ||
1231 [ + + ]: 10111 : (fixesRemaining + negErrorChange == minimumFixes &&
1232 [ + + ]: 6977 : effectiveCoefficient.sgn() == focusCoeffSgn))){
1233 : : // There are more elements &&
1234 : : // we can either fix at least 1 more variable in the error function
1235 : : // or we can improve the error function
1236 : :
1237 : :
1238 : 31915 : int brokenInBlock = 0;
1239 : 31915 : BorderVec::const_iterator endBlock = heap.end();
1240 : :
1241 : 31915 : pop_block(heap, brokenInBlock, fixesRemaining, negErrorChange);
1242 : :
1243 : : // if endVec == beginVec, block starts there
1244 : : // other wise, block starts at endVec
1245 : : BorderVec::const_iterator startBlock
1246 [ + + ]: 31915 : = heap.more() ? heap.end() : heap.begin();
1247 : :
1248 : 31915 : const DeltaRational& blockValue = (*startBlock).d_diff;
1249 : :
1250 : : // if decreasing
1251 : : // blockValue < prevBlockValue
1252 : : // diff.sgn() = -1
1253 : 31915 : DeltaRational diff = blockValue - (*prevBlockValue);
1254 : 31915 : DeltaRational blockChangeToFocus = diff * effectiveCoefficient;
1255 : 31915 : totalFocusChange += blockChangeToFocus;
1256 : :
1257 [ + - ]: 63830 : Trace("handleBorders")
1258 : 0 : << "blockValue " << (blockValue)
1259 : 0 : << "diff " << diff
1260 : 0 : << "blockChangeToFocus " << totalFocusChange
1261 : 0 : << "blockChangeToFocus " << totalFocusChange
1262 : 0 : << "negErrorChange " << negErrorChange
1263 : 0 : << "brokenInBlock " << brokenInBlock
1264 : 0 : << "fixesRemaining " << fixesRemaining
1265 : 31915 : << endl;
1266 : :
1267 : 31915 : int currFocusChangeSgn = totalFocusChange.sgn();
1268 [ + + ]: 114941 : for(BorderVec::const_iterator i = startBlock; i != endBlock; ++i){
1269 : 83026 : const Border& b = *i;
1270 : :
1271 [ + - ]: 83026 : Trace("handleBorders") << b << endl;
1272 : :
1273 [ + + ]: 128826 : bool makesImprovement = negErrorChange > 0 ||
1274 [ + + ][ + + ]: 45800 : (negErrorChange == 0 && currFocusChangeSgn > 0);
1275 : :
1276 [ + + ]: 83026 : if(!makesImprovement){
1277 [ + + ][ + + ]: 34344 : if(b.ownBorder() || minimumFixes > 0){
[ + + ]
1278 : 95 : continue;
1279 : : }
1280 : : }
1281 : :
1282 : 82931 : UpdateInfo proposal(nb, nbDir);
1283 [ + + ]: 82931 : if(b.ownBorder()){
1284 : 946 : proposal.witnessedUpdate(b.d_diff, b.d_bound, -negErrorChange, currFocusChangeSgn);
1285 : : }else{
1286 : 81985 : proposal.update(b.d_diff, b.getCoefficient(), b.d_bound, -negErrorChange, currFocusChangeSgn);
1287 : : }
1288 : :
1289 [ + + ][ - + ]: 82931 : if(selected.unbounded() || (this->*pref)(selected, proposal)){
[ + + ][ + + ]
1290 : 50705 : selected = proposal;
1291 : : }
1292 : 82931 : }
1293 : :
1294 : 31915 : effectiveCoefficient += updateCoefficient(startBlock, endBlock);
1295 : 31915 : prevBlockValue = &blockValue;
1296 : 31915 : negErrorChange -= brokenInBlock;
1297 : 31915 : }
1298 : 25920 : }
1299 : :
1300 : 31915 : Rational LinearEqualityModule::updateCoefficient(BorderVec::const_iterator startBlock, BorderVec::const_iterator endBlock){
1301 : : //update coefficient
1302 : 31915 : Rational changeToCoefficient(0);
1303 [ + + ]: 114941 : for(BorderVec::const_iterator i = startBlock; i != endBlock; ++i){
1304 : 83026 : const Border& curr = *i;
1305 [ + + ]: 83026 : if(curr.ownBorder()){// breaking its own bound
1306 [ + + ]: 991 : if(curr.d_upperbound){
1307 : 504 : changeToCoefficient -= 1;
1308 : : }else{
1309 : 487 : changeToCoefficient += 1;
1310 : : }
1311 : : }else{
1312 : 82035 : const Rational& coeff = curr.d_entry->getCoefficient();
1313 [ + + ]: 82035 : if(curr.d_areFixing){
1314 [ + + ]: 22419 : if(curr.d_upperbound){// fixing an upper bound
1315 : 10508 : changeToCoefficient += coeff;
1316 : : }else{// fixing a lower bound
1317 : 11911 : changeToCoefficient -= coeff;
1318 : : }
1319 : : }else{
1320 [ + + ]: 59616 : if(curr.d_upperbound){// breaking an upper bound
1321 : 25498 : changeToCoefficient -= coeff;
1322 : : }else{
1323 : : // breaking a lower bound
1324 : 34118 : changeToCoefficient += coeff;
1325 : : }
1326 : : }
1327 : : }
1328 : : }
1329 : 31915 : return changeToCoefficient;
1330 : 0 : }
1331 : :
1332 : 31915 : void LinearEqualityModule::pop_block(BorderHeap& heap, int& brokenInBlock, int& fixesRemaining, int& negErrorChange){
1333 [ - + ][ - + ]: 31915 : Assert(heap.more());
[ - - ]
1334 : :
1335 [ + + ]: 31915 : if(heap.top().d_areFixing){
1336 : 11323 : fixesRemaining--;
1337 : 11323 : negErrorChange++;
1338 : : }else{
1339 : 20592 : brokenInBlock++;
1340 : : }
1341 : 31915 : heap.pop_heap();
1342 : 31915 : const DeltaRational& blockValue = (*heap.end()).d_diff;
1343 : :
1344 [ + + ]: 83026 : while(heap.more()){
1345 : 66465 : const Border& top = heap.top();
1346 [ + + ]: 66465 : if(blockValue == top.d_diff){
1347 : : // belongs to the block
1348 [ + + ]: 51111 : if(top.d_areFixing){
1349 : 11096 : fixesRemaining--;
1350 : 11096 : negErrorChange++;
1351 : : }else{
1352 : 40015 : brokenInBlock++;
1353 : : }
1354 : 51111 : heap.pop_heap();
1355 : : }else{
1356 : : // does not belong to the block
1357 [ + + ][ - + ]: 15354 : Assert((heap.direction() > 0) ? (blockValue < top.d_diff)
[ - + ][ - - ]
1358 : : : (blockValue > top.d_diff));
1359 : 15354 : break;
1360 : : }
1361 : : }
1362 : 31915 : }
1363 : :
1364 : 4914 : void LinearEqualityModule::substitutePlusTimesConstant(ArithVar to, ArithVar from, const Rational& mult){
1365 : 4914 : d_tableau.substitutePlusTimesConstant(to, from, mult, d_trackCallback);
1366 : 4914 : }
1367 : 4343 : void LinearEqualityModule::directlyAddToCoefficient(ArithVar row, ArithVar col, const Rational& mult){
1368 : 4343 : d_tableau.directlyAddToCoefficient(row, col, mult, d_trackCallback);
1369 : 4343 : }
1370 : :
1371 : : } // namespace arith
1372 : : } // namespace theory
1373 : : } // namespace cvc5::internal
|
