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 module maintains the relationship between a Tableau and
11 : : * PartialModel.
12 : : *
13 : : * This shares with the theory a Tableau, and a PartialModel that:
14 : : * - satisfies the equalities in the Tableau, and
15 : : * - the assignment for the non-basic variables satisfies their bounds.
16 : : * This maintains the relationship needed by the SimplexDecisionProcedure.
17 : : *
18 : : * In the language of Simplex for DPLL(T), this provides:
19 : : * - update()
20 : : * - pivotAndUpdate()
21 : : *
22 : : * This class also provides utility functions that require
23 : : * using both the Tableau and PartialModel.
24 : : */
25 : :
26 : : #include "cvc5_private.h"
27 : :
28 : : #pragma once
29 : :
30 : : #include "options/arith_options.h"
31 : : #include "theory/arith/delta_rational.h"
32 : : #include "theory/arith/linear/arithvar.h"
33 : : #include "theory/arith/linear/constraint_forward.h"
34 : : #include "theory/arith/linear/partial_model.h"
35 : : #include "theory/arith/linear/simplex_update.h"
36 : : #include "theory/arith/linear/tableau.h"
37 : : #include "util/statistics_stats.h"
38 : :
39 : : namespace cvc5::internal {
40 : : namespace theory {
41 : : namespace arith::linear {
42 : :
43 : : struct Border
44 : : {
45 : : // The constraint for the border
46 : : ConstraintP d_bound;
47 : :
48 : : // The change to the nonbasic to reach the border
49 : : DeltaRational d_diff;
50 : :
51 : : // Is reach this value fixing the constraint
52 : : // or is going past this value hurting the constraint
53 : : bool d_areFixing;
54 : :
55 : : // Entry into the tableau
56 : : const Tableau::Entry* d_entry;
57 : :
58 : : // Was this an upper bound or a lower bound?
59 : : bool d_upperbound;
60 : :
61 : : Border() : d_bound(NullConstraint) // ignore the other values
62 : : {
63 : : }
64 : :
65 : 265885 : Border(ConstraintP l,
66 : : const DeltaRational& diff,
67 : : bool areFixing,
68 : : const Tableau::Entry* en,
69 : : bool ub)
70 : 265885 : : d_bound(l),
71 : 265885 : d_diff(diff),
72 : 265885 : d_areFixing(areFixing),
73 : 265885 : d_entry(en),
74 : 265885 : d_upperbound(ub)
75 : : {
76 : 265885 : }
77 : :
78 : : Border(ConstraintP l, const DeltaRational& diff, bool areFixing, bool ub)
79 : : : d_bound(l),
80 : : d_diff(diff),
81 : : d_areFixing(areFixing),
82 : : d_entry(nullptr),
83 : : d_upperbound(ub)
84 : : {
85 : : }
86 : 273681 : bool operator<(const Border& other) const { return d_diff < other.d_diff; }
87 : :
88 : : /** d_lim is the nonbasic variable's own bound. */
89 : 331003 : bool ownBorder() const { return d_entry == nullptr; }
90 : :
91 : 67904 : bool isZero() const { return d_diff.sgn() == 0; }
92 : 67904 : static bool nonZero(const Border& b) { return !b.isZero(); }
93 : :
94 : 95554 : const Rational& getCoefficient() const
95 : : {
96 [ - + ][ - + ]: 95554 : Assert(!ownBorder());
[ - - ]
97 : 95554 : return d_entry->getCoefficient();
98 : : }
99 : : void output(std::ostream& out) const;
100 : : };
101 : :
102 : 0 : inline std::ostream& operator<<(std::ostream& out, const Border& b)
103 : : {
104 : 0 : b.output(out);
105 : 0 : return out;
106 : : }
107 : :
108 : : typedef std::vector<Border> BorderVec;
109 : :
110 : : class BorderHeap
111 : : {
112 : : const int d_dir;
113 : :
114 : : class BorderHeapCmp
115 : : {
116 : : private:
117 : : int d_nbDirection;
118 : :
119 : : public:
120 : 102426 : BorderHeapCmp(int dir) : d_nbDirection(dir) {}
121 : 273681 : bool operator()(const Border& a, const Border& b) const
122 : : {
123 [ + + ]: 273681 : if (d_nbDirection > 0)
124 : : {
125 : : // if nb is increasing,
126 : : // this needs to act like a max
127 : : // in order to have a min heap
128 : 142857 : return b < a;
129 : : }
130 : : else
131 : : {
132 : : // if nb is decreasing,
133 : : // this needs to act like a min
134 : : // in order to have a max heap
135 : 130824 : return a < b;
136 : : }
137 : : }
138 : : };
139 : : const BorderHeapCmp d_cmp;
140 : :
141 : : BorderVec d_vec;
142 : :
143 : : BorderVec::iterator d_begin;
144 : :
145 : : /**
146 : : * Once this is initialized the top of the heap will always
147 : : * be at d_end - 1
148 : : */
149 : : BorderVec::iterator d_end;
150 : :
151 : : int d_possibleFixes;
152 : : int d_numZeroes;
153 : :
154 : : public:
155 : 102426 : BorderHeap(int dir)
156 : 102426 : : d_dir(dir), d_cmp(dir), d_possibleFixes(0), d_numZeroes(0)
157 : : {
158 : 102426 : }
159 : :
160 : 265885 : void push_back(const Border& b)
161 : : {
162 : 265885 : d_vec.push_back(b);
163 [ + + ]: 265885 : if (b.d_areFixing)
164 : : {
165 : 45861 : d_possibleFixes++;
166 : : }
167 [ + + ]: 265885 : if (b.d_diff.sgn() == 0)
168 : : {
169 : 96980 : d_numZeroes++;
170 : : }
171 : 265885 : }
172 : :
173 : 45060 : int numZeroes() const { return d_numZeroes; }
174 : 56644 : int possibleFixes() const { return d_possibleFixes; }
175 : 44236 : int direction() const { return d_dir; }
176 : :
177 : 28379 : void make_heap()
178 : : {
179 : 28379 : d_begin = d_vec.begin();
180 : 28379 : d_end = d_vec.end();
181 : 28379 : std::make_heap(d_begin, d_end, d_cmp);
182 : 28379 : }
183 : :
184 : 6976 : void dropNonZeroes()
185 : : {
186 : 6976 : d_vec.erase(std::remove_if(d_vec.begin(), d_vec.end(), &Border::nonZero),
187 : 6976 : d_vec.end());
188 : 6976 : }
189 : :
190 : 112222 : const Border& top() const
191 : : {
192 [ - + ][ - + ]: 112222 : Assert(more());
[ - - ]
193 : 112222 : return *d_begin;
194 : : }
195 : 96365 : void pop_heap()
196 : : {
197 [ - + ][ - + ]: 96365 : Assert(more());
[ - - ]
198 : :
199 : 96365 : std::pop_heap(d_begin, d_end, d_cmp);
200 : 96365 : --d_end;
201 : 96365 : }
202 : :
203 : 85035 : BorderVec::const_iterator end() const
204 : : {
205 : 85035 : return BorderVec::const_iterator(d_end);
206 : : }
207 : 18732 : BorderVec::const_iterator begin() const
208 : : {
209 : 18732 : return BorderVec::const_iterator(d_begin);
210 : : }
211 : :
212 : 437098 : inline bool more() const { return d_begin != d_end; }
213 : :
214 : 113342 : inline bool empty() const { return d_vec.empty(); }
215 : :
216 : 56698 : void clear()
217 : : {
218 : 56698 : d_possibleFixes = 0;
219 : 56698 : d_numZeroes = 0;
220 : 56698 : d_vec.clear();
221 : 56698 : }
222 : : };
223 : :
224 : : class LinearEqualityModule
225 : : {
226 : : public:
227 : : typedef ArithVar (LinearEqualityModule::*VarPreferenceFunction)(
228 : : ArithVar, ArithVar) const;
229 : :
230 : : typedef bool (LinearEqualityModule::*UpdatePreferenceFunction)(
231 : : const UpdateInfo&, const UpdateInfo&) const;
232 : :
233 : : private:
234 : : /**
235 : : * Manages information about the assignment and upper and lower bounds on the
236 : : * variables.
237 : : */
238 : : ArithVariables& d_variables;
239 : :
240 : : /** Reference to the Tableau to operate upon. */
241 : : Tableau& d_tableau;
242 : :
243 : : /** Called whenever the value of a basic variable is updated. */
244 : : BasicVarModelUpdateCallBack d_basicVariableUpdates;
245 : :
246 : : BorderHeap d_increasing;
247 : : BorderHeap d_decreasing;
248 : : std::optional<DeltaRational> d_upperBoundDifference;
249 : : std::optional<DeltaRational> d_lowerBoundDifference;
250 : :
251 : : Rational d_one;
252 : : Rational d_negOne;
253 : :
254 : : public:
255 : : /**
256 : : * Initializes a LinearEqualityModule with a partial model, a tableau,
257 : : * and a callback function for when basic variables update their values.
258 : : */
259 : : LinearEqualityModule(StatisticsRegistry& sr,
260 : : ArithVariables& vars,
261 : : Tableau& t,
262 : : BoundInfoMap& boundTracking,
263 : : BasicVarModelUpdateCallBack f);
264 : :
265 : : /**
266 : : * Updates the assignment of a nonbasic variable x_i to v.
267 : : * Also updates the assignment of basic variables accordingly.
268 : : */
269 : 305442 : void update(ArithVar x_i, const DeltaRational& v)
270 : : {
271 [ + + ]: 305442 : if (d_areTracking)
272 : : {
273 : 6 : updateTracked(x_i, v);
274 : : }
275 : : else
276 : : {
277 : 305436 : updateUntracked(x_i, v);
278 : : }
279 : 305442 : }
280 : :
281 : : /** Specialization of update if the module is not tracking yet (for Assert*).
282 : : */
283 : : void updateUntracked(ArithVar x_i, const DeltaRational& v);
284 : :
285 : : /** Specialization of update if the module is not tracking yet (for Simplex).
286 : : */
287 : : void updateTracked(ArithVar x_i, const DeltaRational& v);
288 : :
289 : : /**
290 : : * Updates the value of a basic variable x_i to v,
291 : : * and then pivots x_i with the nonbasic variable in its row x_j.
292 : : * Updates the assignment of the other basic variables accordingly.
293 : : */
294 : : void pivotAndUpdate(ArithVar x_i, ArithVar x_j, const DeltaRational& v);
295 : :
296 : 204852 : ArithVariables& getVariables() const { return d_variables; }
297 : 6457310 : Tableau& getTableau() const { return d_tableau; }
298 : :
299 : : /**
300 : : * Updates every non-basic to reflect the assignment in many.
301 : : * For use with ApproximateSimplex.
302 : : */
303 : : void updateMany(const DenseMap<DeltaRational>& many);
304 : : void forceNewBasis(const DenseSet& newBasis);
305 : : void applySolution(const DenseSet& newBasis,
306 : : const DenseMap<DeltaRational>& newValues);
307 : :
308 : : /**
309 : : * Returns a pointer to the first Tableau entry on the row ridx that does not
310 : : * have an either a lower bound/upper bound for proving a bound on skip.
311 : : * The variable skip is always excluded. Returns NULL if there is no such
312 : : * element.
313 : : *
314 : : * If skip == ARITHVAR_SENTINEL, this is equivalent to considering the whole
315 : : * row.
316 : : */
317 : : const Tableau::Entry* rowLacksBound(RowIndex ridx,
318 : : bool upperBound,
319 : : ArithVar skip);
320 : :
321 : : void startTrackingBoundCounts();
322 : : void stopTrackingBoundCounts();
323 : :
324 : : void includeBoundUpdate(ArithVar nb, const BoundsInfo& prev);
325 : :
326 : : uint32_t updateProduct(const UpdateInfo& inf) const;
327 : :
328 : 14549 : inline bool minNonBasicVarOrder(const UpdateInfo& a,
329 : : const UpdateInfo& b) const
330 : : {
331 : 14549 : return a.nonbasic() >= b.nonbasic();
332 : : }
333 : :
334 : : /**
335 : : * Prefer the update that touch the fewest entries in the matrix.
336 : : *
337 : : * The intuition is that this operation will be cheaper.
338 : : * This strongly biases the system towards updates instead of pivots.
339 : : */
340 : 54128 : inline bool minProduct(const UpdateInfo& a, const UpdateInfo& b) const
341 : : {
342 : 54128 : uint32_t aprod = updateProduct(a);
343 : 54128 : uint32_t bprod = updateProduct(b);
344 : :
345 [ + + ]: 54128 : if (aprod == bprod)
346 : : {
347 : 14549 : return minNonBasicVarOrder(a, b);
348 : : }
349 : : else
350 : : {
351 : 39579 : return aprod > bprod;
352 : : }
353 : : }
354 : 54716 : inline bool constrainedMin(const UpdateInfo& a, const UpdateInfo& b) const
355 : : {
356 [ + + ][ + + ]: 54716 : if (a.describesPivot() && b.describesPivot())
[ + + ]
357 : : {
358 : 53226 : bool aAtBounds = basicsAtBounds(a);
359 : 53226 : bool bAtBounds = basicsAtBounds(b);
360 [ + + ]: 53226 : if (aAtBounds != bAtBounds)
361 : : {
362 : 588 : return bAtBounds;
363 : : }
364 : : }
365 : 54128 : return minProduct(a, b);
366 : : }
367 : :
368 : : /**
369 : : * If both a and b are pivots, prefer the pivot with the leaving variables
370 : : * that has equal bounds. The intuition is that such variables will be less
371 : : * likely to lead to future problems.
372 : : */
373 : 71518 : inline bool preferFrozen(const UpdateInfo& a, const UpdateInfo& b) const
374 : : {
375 [ + + ][ + + ]: 71518 : if (a.describesPivot() && b.describesPivot())
[ + + ]
376 : : {
377 : 70028 : bool aFrozen = d_variables.boundsAreEqual(a.leaving());
378 : 70028 : bool bFrozen = d_variables.boundsAreEqual(b.leaving());
379 : :
380 [ + + ]: 70028 : if (aFrozen != bFrozen)
381 : : {
382 : 16802 : return bFrozen;
383 : : }
384 : : }
385 : 54716 : return constrainedMin(a, b);
386 : : }
387 : :
388 : : /**
389 : : * Prefer pivots with entering variables that do not have bounds.
390 : : * The intuition is that such variables will be less likely to lead to future
391 : : * problems.
392 : : */
393 : 73141 : bool preferNeitherBound(const UpdateInfo& a, const UpdateInfo& b) const
394 : : {
395 : 73141 : if (d_variables.hasEitherBound(a.nonbasic())
396 [ + + ]: 73141 : == d_variables.hasEitherBound(b.nonbasic()))
397 : : {
398 : 71518 : return preferFrozen(a, b);
399 : : }
400 : : else
401 : : {
402 : 1623 : return d_variables.hasEitherBound(a.nonbasic());
403 : : }
404 : : }
405 : :
406 : 0 : bool modifiedBlands(const UpdateInfo& a, const UpdateInfo& b) const
407 : : {
408 : 0 : Assert(a.focusDirection() == 0 && b.focusDirection() == 0);
409 : 0 : Assert(a.describesPivot());
410 : 0 : Assert(b.describesPivot());
411 [ - - ]: 0 : if (a.nonbasic() == b.nonbasic())
412 : : {
413 : 0 : bool aIsZero = a.nonbasicDelta().sgn() == 0;
414 : 0 : bool bIsZero = b.nonbasicDelta().sgn() == 0;
415 : :
416 [ - - ][ - - ]: 0 : if ((aIsZero || bIsZero) && (!aIsZero || !bIsZero))
[ - - ][ - - ]
417 : : {
418 : 0 : return bIsZero;
419 : : }
420 : : else
421 : : {
422 : 0 : return a.leaving() >= b.leaving();
423 : : }
424 : : }
425 : : else
426 : : {
427 : 0 : return a.nonbasic() > b.nonbasic();
428 : : }
429 : : }
430 : :
431 : : template <bool heuristic>
432 : 88384 : bool preferWitness(const UpdateInfo& a, const UpdateInfo& b) const
433 : : {
434 : 88384 : WitnessImprovement aImp = a.getWitness(!heuristic);
435 : 88384 : WitnessImprovement bImp = b.getWitness(!heuristic);
436 : :
437 [ + + ]: 88384 : if (aImp == bImp)
438 : : {
439 [ - + ][ + - ]: 77623 : switch (aImp)
[ + - ][ - - ]
440 : : {
441 : 0 : case ConflictFound: return preferNeitherBound(a, b);
442 : 37370 : case ErrorDropped:
443 [ + + ]: 37370 : if (a.errorsChange() == b.errorsChange())
444 : : {
445 : 32888 : return preferNeitherBound(a, b);
446 : : }
447 : : else
448 : : {
449 : 4482 : return a.errorsChange() > b.errorsChange();
450 : : }
451 : 8008 : case FocusImproved: return preferNeitherBound(a, b);
452 : 0 : case BlandsDegenerate:
453 : 0 : Assert(a.describesPivot());
454 : 0 : Assert(b.describesPivot());
455 : 0 : Assert(a.focusDirection() == 0 && b.focusDirection() == 0);
456 : 0 : return modifiedBlands(a, b);
457 : 32245 : case HeuristicDegenerate:
458 [ - + ][ - + ]: 32245 : Assert(a.describesPivot());
[ - - ]
459 [ - + ][ - + ]: 32245 : Assert(b.describesPivot());
[ - - ]
460 [ + - ][ + - ]: 32245 : Assert(a.focusDirection() == 0 && b.focusDirection() == 0);
[ - + ][ - + ]
[ - - ]
461 : 32245 : return preferNeitherBound(a, b);
462 : 0 : case AntiProductive: return minNonBasicVarOrder(a, b);
463 : : // Not valid responses
464 : 0 : case Degenerate:
465 : 0 : case FocusShrank: Unreachable();
466 : : }
467 : 0 : Unreachable();
468 : : }
469 : : else
470 : : {
471 : 10761 : return aImp > bImp;
472 : : }
473 : : }
474 : :
475 : : private:
476 : : /**
477 : : * This maps each row index to its relevant bounds info.
478 : : * This tracks the count for how many variables on a row have bounds
479 : : * and how many are assigned at their bounds.
480 : : */
481 : : BoundInfoMap& d_btracking;
482 : : bool d_areTracking;
483 : :
484 : : public:
485 : : /**
486 : : * The constraint on a basic variable b is implied by the constraints
487 : : * on its row. This is a wrapper for propagateRow().
488 : : */
489 : : void propagateBasicFromRow(NodeManager* nm,
490 : : ConstraintP c,
491 : : bool produceProofs);
492 : :
493 : : /**
494 : : * Let v be the variable for the constraint c.
495 : : * Exports either the explanation of an upperbound or a lower bound
496 : : * of v using the other variables in the row.
497 : : *
498 : : * If farkas != RationalVectorPSentinel, this function additionally
499 : : * stores the farkas coefficients of the constraints stored in into.
500 : : * Position 0 is the coefficient of v.
501 : : * Position i > 0, corresponds to the order of the other constraints.
502 : : */
503 : : void propagateRow(ConstraintCPVec& into,
504 : : RowIndex ridx,
505 : : bool rowUp,
506 : : ConstraintP c,
507 : : RationalVectorP farkas);
508 : :
509 : : /**
510 : : * Computes the value of a basic variable using the assignments
511 : : * of the values of the variables in the basic variable's row tableau.
512 : : * This can compute the value using either:
513 : : * - the the current assignment (useSafe=false) or
514 : : * - the safe assignment (useSafe = true).
515 : : */
516 : : DeltaRational computeRowValue(ArithVar x, bool useSafe) const;
517 : :
518 : : /**
519 : : * A PreferenceFunction takes a const ref to the SimplexDecisionProcedure,
520 : : * and 2 ArithVar variables and returns one of the ArithVar variables
521 : : * potentially using the internals of the SimplexDecisionProcedure.
522 : : */
523 : :
524 : : ArithVar noPreference(ArithVar x, CVC5_UNUSED ArithVar y) const { return x; }
525 : :
526 : : /**
527 : : * minVarOrder is a PreferenceFunction for selecting the smaller of the 2
528 : : * ArithVars. This PreferenceFunction is used during the VarOrder stage of
529 : : * findModel.
530 : : */
531 : : ArithVar minVarOrder(ArithVar x, ArithVar y) const;
532 : :
533 : : /**
534 : : * minColLength is a PreferenceFunction for selecting the variable with the
535 : : * smaller row count in the tableau.
536 : : *
537 : : * This is a heuristic rule and should not be used during the VarOrder
538 : : * stage of findModel.
539 : : */
540 : : ArithVar minColLength(ArithVar x, ArithVar y) const;
541 : :
542 : : /**
543 : : * minRowLength is a PreferenceFunction for selecting the variable with the
544 : : * smaller row count in the tableau.
545 : : *
546 : : * This is a heuristic rule and should not be used during the VarOrder
547 : : * stage of findModel.
548 : : */
549 : : ArithVar minRowLength(ArithVar x, ArithVar y) const;
550 : :
551 : : /**
552 : : * minBoundAndRowCount is a PreferenceFunction for preferring a variable
553 : : * without an asserted bound over variables with an asserted bound.
554 : : * If both have bounds or both do not have bounds,
555 : : * the rule falls back to minRowCount(...).
556 : : *
557 : : * This is a heuristic rule and should not be used during the VarOrder
558 : : * stage of findModel.
559 : : */
560 : : ArithVar minBoundAndColLength(ArithVar x, ArithVar y) const;
561 : :
562 : : template <bool above>
563 : 5380195 : inline bool isAcceptableSlack(int sgn, ArithVar nonbasic) const
564 : : {
565 [ + + ]: 715957 : return (above && sgn < 0 && d_variables.strictlyBelowUpperBound(nonbasic))
566 [ + + ]: 1251872 : || (above && sgn > 0
567 [ + + ]: 893389 : && d_variables.strictlyAboveLowerBound(nonbasic))
568 : : || (!above && sgn > 0
569 [ + + ]: 1264495 : && d_variables.strictlyBelowUpperBound(nonbasic))
570 [ + + ][ + + ]: 10760390 : || (!above && sgn < 0
571 [ + + ]: 7886549 : && d_variables.strictlyAboveLowerBound(nonbasic));
572 : : }
573 : :
574 : : /**
575 : : * Given the basic variable x_i,
576 : : * this function finds the smallest nonbasic variable x_j in the row of x_i
577 : : * in the tableau that can "take up the slack" to let x_i satisfy its bounds.
578 : : * This returns ARITHVAR_SENTINEL if none exists.
579 : : *
580 : : * More formally one of the following conditions must be satisfied:
581 : : * - lowerBound && a_ij < 0 && assignment(x_j) < upperbound(x_j)
582 : : * - lowerBound && a_ij > 0 && assignment(x_j) > lowerbound(x_j)
583 : : * - !lowerBound && a_ij > 0 && assignment(x_j) < upperbound(x_j)
584 : : * - !lowerBound && a_ij < 0 && assignment(x_j) > lowerbound(x_j)
585 : : *
586 : : */
587 : : template <bool lowerBound>
588 : : ArithVar selectSlack(ArithVar x_i, VarPreferenceFunction pf) const;
589 : 165629 : ArithVar selectSlackLowerBound(ArithVar x_i, VarPreferenceFunction pf) const
590 : : {
591 : 165629 : return selectSlack<true>(x_i, pf);
592 : : }
593 : 164945 : ArithVar selectSlackUpperBound(ArithVar x_i, VarPreferenceFunction pf) const
594 : : {
595 : 164945 : return selectSlack<false>(x_i, pf);
596 : : }
597 : :
598 : : const Tableau::Entry* selectSlackEntry(ArithVar x_i, bool above) const;
599 : :
600 : 90933630 : inline bool rowIndexIsTracked(RowIndex ridx) const
601 : : {
602 : 90933630 : return d_btracking.isKey(ridx);
603 : : }
604 : 12272014 : inline bool basicIsTracked(ArithVar v) const
605 : : {
606 : 12272014 : return rowIndexIsTracked(d_tableau.basicToRowIndex(v));
607 : : }
608 : : void trackRowIndex(RowIndex ridx);
609 : 4096 : void stopTrackingRowIndex(RowIndex ridx)
610 : : {
611 [ - + ][ - + ]: 4096 : Assert(rowIndexIsTracked(ridx));
[ - - ]
612 : 4096 : d_btracking.remove(ridx);
613 : 4096 : }
614 : :
615 : : /**
616 : : * If the pivot described in u were performed,
617 : : * then the row would qualify as being either at the minimum/maximum
618 : : * to the non-basics being at their bounds.
619 : : * The minimum/maximum is determined by the direction the non-basic is
620 : : * changing.
621 : : */
622 : : bool basicsAtBounds(const UpdateInfo& u) const;
623 : :
624 : : private:
625 : : /**
626 : : * Recomputes the bound info for a row using either the information
627 : : * in the bounds queue or the current information.
628 : : * O(row length of ridx)
629 : : */
630 : : BoundsInfo computeRowBoundInfo(RowIndex ridx, bool inQueue) const;
631 : :
632 : : public:
633 : : /** Debug only routine. */
634 : : BoundCounts debugBasicAtBoundCount(ArithVar x_i) const;
635 : :
636 : : /** Track the effect of the change of coefficient for bound counting. */
637 : : void trackingCoefficientChange(RowIndex ridx,
638 : : ArithVar nb,
639 : : int oldSgn,
640 : : int currSgn);
641 : :
642 : : /** Track the effect of multiplying a row by a sign for bound counting. */
643 : : void trackingMultiplyRow(RowIndex ridx, int sgn);
644 : :
645 : : /** Count for how many on a row have *an* upper/lower bounds. */
646 : 18764392 : BoundCounts hasBoundCount(RowIndex ri) const
647 : : {
648 [ - + ][ - + ]: 18764392 : Assert(d_variables.boundsQueueEmpty());
[ - - ]
649 : 18764392 : return d_btracking[ri].hasBounds();
650 : : }
651 : :
652 : : /**
653 : : * Are there any non-basics on x_i's row that are not at
654 : : * their respective lower bounds (mod sgns).
655 : : * O(1) time due to the atBound() count.
656 : : */
657 : : bool nonbasicsAtLowerBounds(ArithVar x_i) const;
658 : :
659 : : /**
660 : : * Are there any non-basics on x_i's row that are not at
661 : : * their respective upper bounds (mod sgns).
662 : : * O(1) time due to the atBound() count.
663 : : */
664 : : bool nonbasicsAtUpperBounds(ArithVar x_i) const;
665 : :
666 : : private:
667 : : class TrackingCallback : public CoefficientChangeCallback
668 : : {
669 : : private:
670 : : LinearEqualityModule* d_linEq;
671 : :
672 : : public:
673 : 51213 : TrackingCallback(LinearEqualityModule* le) : d_linEq(le) {}
674 : 71484607 : void update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn) override
675 : : {
676 : 71484607 : d_linEq->trackingCoefficientChange(ridx, nb, oldSgn, currSgn);
677 : 71484607 : }
678 : 338353 : void multiplyRow(RowIndex ridx, int sgn) override
679 : : {
680 : 338353 : d_linEq->trackingMultiplyRow(ridx, sgn);
681 : 338353 : }
682 : 6252458 : bool canUseRow(RowIndex ridx) const override
683 : : {
684 : 6252458 : ArithVar basic = d_linEq->getTableau().rowIndexToBasic(ridx);
685 : 6252458 : return d_linEq->basicIsTracked(basic);
686 : : }
687 : : } d_trackCallback;
688 : :
689 : : /**
690 : : * Selects the constraint for the variable v on the row for basic
691 : : * with the weakest possible constraint that is consistent with the surplus
692 : : * surplus.
693 : : */
694 : : ConstraintP weakestExplanation(bool aboveUpper,
695 : : DeltaRational& surplus,
696 : : ArithVar v,
697 : : const Rational& coeff,
698 : : bool& anyWeakening,
699 : : ArithVar basic) const;
700 : :
701 : : public:
702 : : /**
703 : : * Constructs a minimally weak conflict for the basic variable basicVar.
704 : : *
705 : : * Returns a constraint that is now in conflict.
706 : : */
707 : : ConstraintCP minimallyWeakConflict(NodeManager* nm,
708 : : bool aboveUpper,
709 : : ArithVar basicVar,
710 : : FarkasConflictBuilder& rc) const;
711 : :
712 : : /**
713 : : * Given a basic variable that is know to have a conflict on it,
714 : : * construct and return a conflict.
715 : : * Follows section 4.2 in the CAV06 paper.
716 : : */
717 : 50419 : inline ConstraintCP generateConflictAboveUpperBound(
718 : : NodeManager* nm, ArithVar conflictVar, FarkasConflictBuilder& rc) const
719 : : {
720 : 50419 : return minimallyWeakConflict(nm, true, conflictVar, rc);
721 : : }
722 : :
723 : 52456 : inline ConstraintCP generateConflictBelowLowerBound(
724 : : NodeManager* nm, ArithVar conflictVar, FarkasConflictBuilder& rc) const
725 : : {
726 : 52456 : return minimallyWeakConflict(nm, false, conflictVar, rc);
727 : : }
728 : :
729 : : /**
730 : : * Computes the sum of the upper/lower bound of row.
731 : : * The variable skip is not included in the sum.
732 : : */
733 : : DeltaRational computeRowBound(RowIndex ridx, bool rowUb, ArithVar skip) const;
734 : :
735 : : public:
736 : : void substitutePlusTimesConstant(ArithVar to,
737 : : ArithVar from,
738 : : const Rational& mult);
739 : : void directlyAddToCoefficient(ArithVar row,
740 : : ArithVar col,
741 : : const Rational& mult);
742 : :
743 : : /**
744 : : * Checks to make sure the assignment is consistent with the tableau.
745 : : * This code is for debugging.
746 : : */
747 : : void debugCheckTableau();
748 : :
749 : : void debugCheckTracking();
750 : :
751 : : /** Debugging information for a pivot. */
752 : : void debugPivot(ArithVar x_i, ArithVar x_j);
753 : :
754 : : ArithVar minBy(const ArithVarVec& vec, VarPreferenceFunction pf) const;
755 : :
756 : : /**
757 : : * Returns true if there would be a conflict on this row after a pivot
758 : : * and update using its basic variable and one of the non-basic variables on
759 : : * the row.
760 : : */
761 : : bool willBeInConflictAfterPivot(const Tableau::Entry& entry,
762 : : const DeltaRational& nbDiff,
763 : : bool bToUB) const;
764 : : UpdateInfo mkConflictUpdate(const Tableau::Entry& entry, bool ub) const;
765 : :
766 : : /**
767 : : * Looks more an update for fcSimplex on the nonbasic variable nb with the
768 : : * focus coefficient.
769 : : */
770 : : UpdateInfo speculativeUpdate(ArithVar nb,
771 : : const Rational& focusCoeff,
772 : : UpdatePreferenceFunction pref);
773 : :
774 : : private:
775 : : /**
776 : : * Examines the effects of pivoting the entries column variable
777 : : * with the row's basic variable and setting the variable s.t.
778 : : * the basic variable is equal to one of its bounds.
779 : : *
780 : : * If ub, then the basic variable will be equal its upper bound.
781 : : * If not ub,then the basic variable will be equal its lower bound.
782 : : *
783 : : * Returns iff this row will be in conflict after the pivot.
784 : : *
785 : : * If this is false, add the bound to the relevant heap.
786 : : * If the bound is +/-infinity, this is ignored.
787 : :
788 : : *
789 : : * Returns true if this would be a conflict.
790 : : * If it returns false, this
791 : : */
792 : : bool accumulateBorder(const Tableau::Entry& entry, bool ub);
793 : :
794 : : void handleBorders(UpdateInfo& selected,
795 : : ArithVar nb,
796 : : const Rational& focusCoeff,
797 : : BorderHeap& heap,
798 : : int minimumFixes,
799 : : UpdatePreferenceFunction pref);
800 : : void pop_block(BorderHeap& heap,
801 : : int& brokenInBlock,
802 : : int& fixesRemaining,
803 : : int& negErrorChange);
804 : : void clearSpeculative();
805 : : Rational updateCoefficient(BorderVec::const_iterator startBlock,
806 : : BorderVec::const_iterator endBlock);
807 : :
808 : : private:
809 : : /** These fields are designed to be accessible to TheoryArith methods. */
810 : : class Statistics
811 : : {
812 : : public:
813 : : IntStat d_statPivots, d_statUpdates;
814 : : TimerStat d_pivotTime;
815 : : TimerStat d_adjTime;
816 : :
817 : : IntStat d_weakeningAttempts, d_weakeningSuccesses, d_weakenings;
818 : : TimerStat d_weakenTime;
819 : : TimerStat d_forceTime;
820 : :
821 : : Statistics(StatisticsRegistry& sr);
822 : : };
823 : : mutable Statistics d_statistics;
824 : :
825 : : }; /* class LinearEqualityModule */
826 : :
827 : : struct Cand
828 : : {
829 : : ArithVar d_nb;
830 : : uint32_t d_penalty;
831 : : int d_sgn;
832 : : const Rational* d_coeff;
833 : :
834 : 28481 : Cand(ArithVar nb, uint32_t penalty, int s, const Rational* c)
835 : 28481 : : d_nb(nb), d_penalty(penalty), d_sgn(s), d_coeff(c)
836 : : {
837 : 28481 : }
838 : : };
839 : :
840 : : class CompPenaltyColLength
841 : : {
842 : : private:
843 : : LinearEqualityModule* d_mod;
844 : : const bool d_havePenalties;
845 : :
846 : : public:
847 : 7971 : CompPenaltyColLength(LinearEqualityModule* mod, bool havePenalties)
848 : 7971 : : d_mod(mod), d_havePenalties(havePenalties)
849 : : {
850 : 7971 : }
851 : :
852 : 57309 : bool operator()(const Cand& x, const Cand& y) const
853 : : {
854 [ - + ][ - - ]: 57309 : if (x.d_penalty == y.d_penalty || !d_havePenalties)
855 : : {
856 : 57309 : return x.d_nb == d_mod->minBoundAndColLength(x.d_nb, y.d_nb);
857 : : }
858 : : else
859 : : {
860 : 0 : return x.d_penalty < y.d_penalty;
861 : : }
862 : : }
863 : : };
864 : :
865 : : class UpdateTrackingCallback : public BoundUpdateCallback
866 : : {
867 : : private:
868 : : LinearEqualityModule* d_mod;
869 : :
870 : : public:
871 : 5317136 : UpdateTrackingCallback(LinearEqualityModule* mod) : d_mod(mod) {}
872 : 9134319 : void operator()(ArithVar v, const BoundsInfo& bi) override
873 : : {
874 : 9134319 : d_mod->includeBoundUpdate(v, bi);
875 : 9134319 : }
876 : : };
877 : :
878 : : } // namespace arith::linear
879 : : } // namespace theory
880 : : } // namespace cvc5::internal
|
