Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Tim King, Gereon Kremer, Andrew Reynolds
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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 : 252607 : Border(ConstraintP l, const DeltaRational& diff, bool areFixing, const Tableau::Entry* en, bool ub):
68 : 252607 : d_bound(l), d_diff(diff), d_areFixing(areFixing), d_entry(en), d_upperbound(ub)
69 : 252607 : {}
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 : 261291 : bool operator<(const Border& other) const{
75 : 261291 : return d_diff < other.d_diff;
76 : : }
77 : :
78 : : /** d_lim is the nonbasic variable's own bound. */
79 : 293173 : bool ownBorder() const { return d_entry == NULL; }
80 : :
81 : 50473 : bool isZero() const { return d_diff.sgn() == 0; }
82 : 50473 : static bool nonZero(const Border& b) { return !b.isZero(); }
83 : :
84 : 85569 : const Rational& getCoefficient() const {
85 [ - + ][ - + ]: 85569 : Assert(!ownBorder());
[ - - ]
86 : 85569 : 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 : 98528 : BorderHeapCmp(int dir): d_nbDirection(dir){}
106 : 261291 : bool operator()(const Border& a, const Border& b) const{
107 [ + + ]: 261291 : 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 : 137791 : 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 : 123500 : 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 : 98528 : BorderHeap(int dir)
137 : 98528 : : d_dir(dir), d_cmp(dir), d_possibleFixes(0), d_numZeroes(0)
138 : 98528 : {}
139 : :
140 : 252607 : void push_back(const Border& b){
141 : 252607 : d_vec.push_back(b);
142 [ + + ]: 252607 : if(b.d_areFixing){
143 : 43877 : d_possibleFixes++;
144 : : }
145 [ + + ]: 252607 : if(b.d_diff.sgn() == 0){
146 : 76720 : d_numZeroes++;
147 : : }
148 : 252607 : }
149 : :
150 : 44611 : int numZeroes() const { return d_numZeroes; }
151 : 57138 : int possibleFixes() const { return d_possibleFixes; }
152 : 45912 : int direction() const { return d_dir; }
153 : :
154 : 28632 : void make_heap(){
155 : 28632 : d_begin = d_vec.begin();
156 : 28632 : d_end = d_vec.end();
157 : 28632 : std::make_heap(d_begin, d_end, d_cmp);
158 : 28632 : }
159 : :
160 : 5610 : void dropNonZeroes(){
161 : 5610 : d_vec.erase(std::remove_if(d_vec.begin(), d_vec.end(), &Border::nonZero),
162 : 11220 : d_vec.end());
163 : 5610 : }
164 : :
165 : 104090 : const Border& top() const {
166 [ - + ][ - + ]: 104090 : Assert(more());
[ - - ]
167 : 104090 : return *d_begin;
168 : : }
169 : 86810 : void pop_heap(){
170 [ - + ][ - + ]: 86810 : Assert(more());
[ - - ]
171 : :
172 : 86810 : std::pop_heap(d_begin, d_end, d_cmp);
173 : 86810 : --d_end;
174 : 86810 : }
175 : :
176 : 88160 : BorderVec::const_iterator end() const{
177 : 88160 : return BorderVec::const_iterator(d_end);
178 : : }
179 : 18160 : BorderVec::const_iterator begin() const{
180 : 18160 : return BorderVec::const_iterator(d_begin);
181 : : }
182 : :
183 : 412662 : inline bool more() const{ return d_begin != d_end; }
184 : :
185 : 114358 : inline bool empty() const{ return d_vec.empty(); }
186 : :
187 : 57220 : void clear(){
188 : 57220 : d_possibleFixes = 0;
189 : 57220 : d_numZeroes = 0;
190 : 57220 : d_vec.clear();
191 : 57220 : }
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 : 319523 : void update(ArithVar x_i, const DeltaRational& v)
240 : : {
241 [ + + ]: 319523 : if (d_areTracking)
242 : : {
243 : 6 : updateTracked(x_i, v);
244 : : }
245 : : else
246 : : {
247 : 319517 : updateUntracked(x_i, v);
248 : : }
249 : 319523 : }
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 : 197056 : ArithVariables& getVariables() const{ return d_variables; }
266 : 11652100 : 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 : 14704 : inline bool minNonBasicVarOrder(const UpdateInfo& a, const UpdateInfo& b) const{
297 : 14704 : 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 : 46517 : inline bool minProduct(const UpdateInfo& a, const UpdateInfo& b) const{
307 : 46517 : uint32_t aprod = updateProduct(a);
308 : 46517 : uint32_t bprod = updateProduct(b);
309 : :
310 [ + + ]: 46517 : if(aprod == bprod){
311 : 14704 : return minNonBasicVarOrder(a,b);
312 : : }else{
313 : 31813 : return aprod > bprod;
314 : : }
315 : : }
316 : 47248 : inline bool constrainedMin(const UpdateInfo& a, const UpdateInfo& b) const{
317 [ + + ][ + + ]: 47248 : if(a.describesPivot() && b.describesPivot()){
[ + + ]
318 : 45097 : bool aAtBounds = basicsAtBounds(a);
319 : 45097 : bool bAtBounds = basicsAtBounds(b);
320 [ + + ]: 45097 : if(aAtBounds != bAtBounds){
321 : 731 : return bAtBounds;
322 : : }
323 : : }
324 : 46517 : 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 : 60238 : inline bool preferFrozen(const UpdateInfo& a, const UpdateInfo& b) const {
332 [ + + ][ + + ]: 60238 : if(a.describesPivot() && b.describesPivot()){
[ + + ]
333 : 58087 : bool aFrozen = d_variables.boundsAreEqual(a.leaving());
334 : 58087 : bool bFrozen = d_variables.boundsAreEqual(b.leaving());
335 : :
336 [ + + ]: 58087 : if(aFrozen != bFrozen){
337 : 12990 : return bFrozen;
338 : : }
339 : : }
340 : 47248 : 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 : 61931 : bool preferNeitherBound(const UpdateInfo& a, const UpdateInfo& b) const {
348 [ + + ]: 61931 : if(d_variables.hasEitherBound(a.nonbasic()) == d_variables.hasEitherBound(b.nonbasic())){
349 : 60238 : return preferFrozen(a,b);
350 : : }else{
351 : 1693 : 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 : 78188 : bool preferWitness(const UpdateInfo& a, const UpdateInfo& b) const{
375 : 78188 : WitnessImprovement aImp = a.getWitness(!heuristic);
376 : 78188 : WitnessImprovement bImp = b.getWitness(!heuristic);
377 : :
378 [ + + ]: 78188 : if(aImp == bImp){
379 [ - + ][ + - ]: 66359 : switch(aImp){
[ + - ][ - - ]
380 : 0 : case ConflictFound:
381 : 0 : return preferNeitherBound(a,b);
382 : 35625 : case ErrorDropped:
383 [ + + ]: 35625 : if(a.errorsChange() == b.errorsChange()){
384 : 31197 : return preferNeitherBound(a,b);
385 : : }else{
386 : 4428 : return a.errorsChange() > b.errorsChange();
387 : : }
388 : 7658 : case FocusImproved:
389 : 7658 : 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 : 23076 : case HeuristicDegenerate:
396 [ - + ][ - + ]: 23076 : Assert(a.describesPivot());
[ - - ]
397 [ - + ][ - + ]: 23076 : Assert(b.describesPivot());
[ - - ]
398 [ + - ][ + - ]: 46152 : Assert(a.focusDirection() == 0 && b.focusDirection() == 0);
[ - + ][ - - ]
399 : 23076 : 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 : 11829 : 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(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, 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 : 7420770 : inline bool isAcceptableSlack(int sgn, ArithVar nonbasic) const
501 : : {
502 [ + + ]: 940282 : return (above && sgn < 0 && d_variables.strictlyBelowUpperBound(nonbasic))
503 [ + + ][ + + ]: 1625950 : || (above && sgn > 0 && d_variables.strictlyAboveLowerBound(nonbasic))
504 : : || (!above && sgn > 0
505 [ + + ]: 1700270 : && d_variables.strictlyBelowUpperBound(nonbasic))
506 [ + + ][ + + ]: 14841570 : || (!above && sgn < 0
507 [ + + ]: 11027930 : && 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 : 182518 : ArithVar selectSlackLowerBound(ArithVar x_i, VarPreferenceFunction pf) const {
525 : 182518 : return selectSlack<true>(x_i, pf);
526 : : }
527 : 189550 : ArithVar selectSlackUpperBound(ArithVar x_i, VarPreferenceFunction pf) const {
528 : 189550 : return selectSlack<false>(x_i, pf);
529 : : }
530 : :
531 : : const Tableau::Entry* selectSlackEntry(ArithVar x_i, bool above) const;
532 : :
533 : 147645000 : inline bool rowIndexIsTracked(RowIndex ridx) const {
534 : 147645000 : return d_btracking.isKey(ridx);
535 : : }
536 : 19113900 : inline bool basicIsTracked(ArithVar v) const {
537 : 19113900 : return rowIndexIsTracked(d_tableau.basicToRowIndex(v));
538 : : }
539 : : void trackRowIndex(RowIndex ridx);
540 : 4657 : void stopTrackingRowIndex(RowIndex ridx){
541 [ - + ][ - + ]: 4657 : Assert(rowIndexIsTracked(ridx));
[ - - ]
542 : 4657 : d_btracking.remove(ridx);
543 : 4657 : }
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 : 22274800 : BoundCounts hasBoundCount(RowIndex ri) const {
574 [ - + ][ - + ]: 22274800 : Assert(d_variables.boundsQueueEmpty());
[ - - ]
575 : 22274800 : 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 : 49264 : TrackingCallback(LinearEqualityModule* le) : d_linEq(le) {}
598 : 116068000 : void update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn) override
599 : : {
600 : 116068000 : d_linEq->trackingCoefficientChange(ridx, nb, oldSgn, currSgn);
601 : 116068000 : }
602 : 380465 : void multiplyRow(RowIndex ridx, int sgn) override
603 : : {
604 : 380465 : d_linEq->trackingMultiplyRow(ridx, sgn);
605 : 380465 : }
606 : 11455000 : bool canUseRow(RowIndex ridx) const override
607 : : {
608 : 11455000 : ArithVar basic = d_linEq->getTableau().rowIndexToBasic(ridx);
609 : 11455000 : 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(bool aboveUpper, ArithVar basicVar, FarkasConflictBuilder& rc) const;
628 : :
629 : : /**
630 : : * Given a basic variable that is know to have a conflict on it,
631 : : * construct and return a conflict.
632 : : * Follows section 4.2 in the CAV06 paper.
633 : : */
634 : 75288 : inline ConstraintCP generateConflictAboveUpperBound(ArithVar conflictVar, FarkasConflictBuilder& rc) const {
635 : 75288 : return minimallyWeakConflict(true, conflictVar, rc);
636 : : }
637 : :
638 : 74000 : inline ConstraintCP generateConflictBelowLowerBound(ArithVar conflictVar, FarkasConflictBuilder& rc) const {
639 : 74000 : return minimallyWeakConflict(false, conflictVar, rc);
640 : : }
641 : :
642 : : /**
643 : : * Computes the sum of the upper/lower bound of row.
644 : : * The variable skip is not included in the sum.
645 : : */
646 : : DeltaRational computeRowBound(RowIndex ridx, bool rowUb, ArithVar skip) const;
647 : :
648 : : public:
649 : : void substitutePlusTimesConstant(ArithVar to, ArithVar from, const Rational& mult);
650 : : void directlyAddToCoefficient(ArithVar row, ArithVar col, const Rational& mult);
651 : :
652 : :
653 : : /**
654 : : * Checks to make sure the assignment is consistent with the tableau.
655 : : * This code is for debugging.
656 : : */
657 : : void debugCheckTableau();
658 : :
659 : : void debugCheckTracking();
660 : :
661 : : /** Debugging information for a pivot. */
662 : : void debugPivot(ArithVar x_i, ArithVar x_j);
663 : :
664 : : ArithVar minBy(const ArithVarVec& vec, VarPreferenceFunction pf) const;
665 : :
666 : : /**
667 : : * Returns true if there would be a conflict on this row after a pivot
668 : : * and update using its basic variable and one of the non-basic variables on
669 : : * the row.
670 : : */
671 : : bool willBeInConflictAfterPivot(const Tableau::Entry& entry, const DeltaRational& nbDiff, bool bToUB) const;
672 : : UpdateInfo mkConflictUpdate(const Tableau::Entry& entry, bool ub) const;
673 : :
674 : : /**
675 : : * Looks more an update for fcSimplex on the nonbasic variable nb with the focus coefficient.
676 : : */
677 : : UpdateInfo speculativeUpdate(ArithVar nb, const Rational& focusCoeff, UpdatePreferenceFunction pref);
678 : :
679 : : private:
680 : :
681 : : /**
682 : : * Examines the effects of pivoting the entries column variable
683 : : * with the row's basic variable and setting the variable s.t.
684 : : * the basic variable is equal to one of its bounds.
685 : : *
686 : : * If ub, then the basic variable will be equal its upper bound.
687 : : * If not ub,then the basic variable will be equal its lower bound.
688 : : *
689 : : * Returns iff this row will be in conflict after the pivot.
690 : : *
691 : : * If this is false, add the bound to the relevant heap.
692 : : * If the bound is +/-infinity, this is ignored.
693 : :
694 : : *
695 : : * Returns true if this would be a conflict.
696 : : * If it returns false, this
697 : : */
698 : : bool accumulateBorder(const Tableau::Entry& entry, bool ub);
699 : :
700 : : void handleBorders(UpdateInfo& selected, ArithVar nb, const Rational& focusCoeff, BorderHeap& heap, int minimumFixes, UpdatePreferenceFunction pref);
701 : : void pop_block(BorderHeap& heap, int& brokenInBlock, int& fixesRemaining, int& negErrorChange);
702 : : void clearSpeculative();
703 : : Rational updateCoefficient(BorderVec::const_iterator startBlock, BorderVec::const_iterator endBlock);
704 : :
705 : : private:
706 : : /** These fields are designed to be accessible to TheoryArith methods. */
707 : : class Statistics {
708 : : public:
709 : : IntStat d_statPivots, d_statUpdates;
710 : : TimerStat d_pivotTime;
711 : : TimerStat d_adjTime;
712 : :
713 : : IntStat d_weakeningAttempts, d_weakeningSuccesses, d_weakenings;
714 : : TimerStat d_weakenTime;
715 : : TimerStat d_forceTime;
716 : :
717 : : Statistics(StatisticsRegistry& sr);
718 : : };
719 : : mutable Statistics d_statistics;
720 : :
721 : : };/* class LinearEqualityModule */
722 : :
723 : : struct Cand {
724 : : ArithVar d_nb;
725 : : uint32_t d_penalty;
726 : : int d_sgn;
727 : : const Rational* d_coeff;
728 : :
729 : 28840 : Cand(ArithVar nb, uint32_t penalty, int s, const Rational* c) :
730 : 28840 : d_nb(nb), d_penalty(penalty), d_sgn(s), d_coeff(c){}
731 : : };
732 : :
733 : :
734 : : class CompPenaltyColLength {
735 : : private:
736 : : LinearEqualityModule* d_mod;
737 : : const bool d_havePenalties;
738 : :
739 : : public:
740 : 8585 : CompPenaltyColLength(LinearEqualityModule* mod, bool havePenalties)
741 : 8585 : : d_mod(mod), d_havePenalties(havePenalties)
742 : : {
743 : 8585 : }
744 : :
745 : 55393 : bool operator()(const Cand& x, const Cand& y) const {
746 [ - + ][ - - ]: 55393 : if (x.d_penalty == y.d_penalty || !d_havePenalties)
747 : : {
748 : 55393 : return x.d_nb == d_mod->minBoundAndColLength(x.d_nb,y.d_nb);
749 : : }
750 : : else
751 : : {
752 : 0 : return x.d_penalty < y.d_penalty;
753 : : }
754 : : }
755 : : };
756 : :
757 : : class UpdateTrackingCallback : public BoundUpdateCallback {
758 : : private:
759 : : LinearEqualityModule* d_mod;
760 : : public:
761 : 5428420 : UpdateTrackingCallback(LinearEqualityModule* mod): d_mod(mod){}
762 : 9350170 : void operator()(ArithVar v, const BoundsInfo& bi) override
763 : : {
764 : 9350170 : d_mod->includeBoundUpdate(v, bi);
765 : 9350170 : }
766 : : };
767 : :
768 : : } // namespace arith
769 : : } // namespace theory
770 : : } // namespace cvc5::internal
|
