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