GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/linear_equality.h Lines: 48 183 26.2 %
Date: 2021-03-22 Branches: 19 454 4.2 %

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