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