GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/partial_model.cpp Lines: 320 406 78.8 %
Date: 2021-05-24 Branches: 294 874 33.6 %

Line Exec Source
1
/******************************************************************************
2
 * Top contributors (to current version):
3
 *   Tim King
4
 *
5
 * This file is part of the cvc5 project.
6
 *
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.
11
 * ****************************************************************************
12
 *
13
 * [[ Add one-line brief description here ]]
14
 *
15
 * [[ Add lengthier description here ]]
16
 * \todo document this file
17
 */
18
19
#include "base/output.h"
20
#include "theory/arith/constraint.h"
21
#include "theory/arith/normal_form.h"
22
#include "theory/arith/partial_model.h"
23
24
using namespace std;
25
26
namespace cvc5 {
27
namespace theory {
28
namespace arith {
29
30
9459
ArithVariables::ArithVariables(context::Context* c, DeltaComputeCallback deltaComputingFunc)
31
 : d_vars(),
32
   d_safeAssignment(),
33
   d_numberOfVariables(0),
34
   d_pool(),
35
   d_released(),
36
   d_nodeToArithVarMap(),
37
   d_boundsQueue(),
38
   d_enqueueingBoundCounts(true),
39
18918
   d_lbRevertHistory(c, true, LowerBoundCleanUp(this)),
40
18918
   d_ubRevertHistory(c, true, UpperBoundCleanUp(this)),
41
   d_deltaIsSafe(false),
42
   d_delta(-1,1),
43
47295
   d_deltaComputingFunc(deltaComputingFunc)
44
9459
{ }
45
46
140774259
ArithVar ArithVariables::getNumberOfVariables() const {
47
140774259
  return d_numberOfVariables;
48
}
49
50
51
10217343
bool ArithVariables::hasArithVar(TNode x) const {
52
10217343
  return d_nodeToArithVarMap.find(x) != d_nodeToArithVarMap.end();
53
}
54
55
115423840
bool ArithVariables::hasNode(ArithVar a) const {
56
115423840
  return d_vars.isKey(a);
57
}
58
59
3166298
ArithVar ArithVariables::asArithVar(TNode x) const{
60
3166298
  Assert(hasArithVar(x));
61
3166298
  Assert((d_nodeToArithVarMap.find(x))->second <= ARITHVAR_SENTINEL);
62
3166298
  return (d_nodeToArithVarMap.find(x))->second;
63
}
64
65
112389351
Node ArithVariables::asNode(ArithVar a) const{
66
112389351
  Assert(hasNode(a));
67
112389351
  return d_vars[a].d_node;
68
}
69
70
ArithVariables::var_iterator::var_iterator()
71
  : d_vars(NULL)
72
  , d_wrapped()
73
{}
74
75
2589822
ArithVariables::var_iterator::var_iterator(const VarInfoVec* vars, VarInfoVec::const_iterator ci)
76
2589822
  : d_vars(vars), d_wrapped(ci)
77
{
78
2589822
  nextInitialized();
79
2589822
}
80
81
10531684
ArithVariables::var_iterator& ArithVariables::var_iterator::operator++(){
82
10531684
  ++d_wrapped;
83
10531684
  nextInitialized();
84
10531684
  return *this;
85
}
86
bool ArithVariables::var_iterator::operator==(const ArithVariables::var_iterator& other) const{
87
  return d_wrapped == other.d_wrapped;
88
}
89
11826595
bool ArithVariables::var_iterator::operator!=(const ArithVariables::var_iterator& other) const{
90
11826595
  return d_wrapped != other.d_wrapped;
91
}
92
10531684
ArithVar ArithVariables::var_iterator::operator*() const{
93
10531684
  return *d_wrapped;
94
}
95
96
13121506
void ArithVariables::var_iterator::nextInitialized(){
97
13121506
  VarInfoVec::const_iterator end = d_vars->end();
98
24900561
  while(d_wrapped != end &&
99
11779055
        !((*d_vars)[*d_wrapped].initialized())){
100
    ++d_wrapped;
101
  }
102
13121506
}
103
104
1294911
ArithVariables::var_iterator ArithVariables::var_begin() const {
105
1294911
  return var_iterator(&d_vars, d_vars.begin());
106
}
107
108
1294911
ArithVariables::var_iterator ArithVariables::var_end() const {
109
1294911
  return var_iterator(&d_vars, d_vars.end());
110
}
111
461484176
bool ArithVariables::isInteger(ArithVar x) const {
112
461484176
  return d_vars[x].d_type >= ArithType::Integer;
113
}
114
115
/** Is the assignment to x integral? */
116
107612635
bool ArithVariables::integralAssignment(ArithVar x) const {
117
107612635
  return getAssignment(x).isIntegral();
118
}
119
280110769
bool ArithVariables::isAuxiliary(ArithVar x) const {
120
280110769
  return d_vars[x].d_auxiliary;
121
}
122
123
445906553
bool ArithVariables::isIntegerInput(ArithVar x) const {
124
445906553
  return isInteger(x) && !isAuxiliary(x);
125
}
126
127
295826
ArithVariables::VarInfo::VarInfo()
128
    : d_var(ARITHVAR_SENTINEL),
129
      d_assignment(0),
130
      d_lb(NullConstraint),
131
      d_ub(NullConstraint),
132
      d_cmpAssignmentLB(1),
133
      d_cmpAssignmentUB(-1),
134
      d_pushCount(0),
135
      d_type(ArithType::Unset),
136
      d_node(Node::null()),
137
295826
      d_auxiliary(false) {}
138
139
24765471
bool ArithVariables::VarInfo::initialized() const {
140
24765471
  return d_var != ARITHVAR_SENTINEL;
141
}
142
143
147913
void ArithVariables::VarInfo::initialize(ArithVar v, Node n, bool aux){
144
147913
  Assert(!initialized());
145
147913
  Assert(d_lb == NullConstraint);
146
147913
  Assert(d_ub == NullConstraint);
147
147913
  Assert(d_cmpAssignmentLB > 0);
148
147913
  Assert(d_cmpAssignmentUB < 0);
149
147913
  d_var = v;
150
147913
  d_node = n;
151
147913
  d_auxiliary = aux;
152
153
147913
  if(d_auxiliary){
154
    //The type computation is not quite accurate for Rationals that are
155
    //integral.
156
    //We'll use the isIntegral check from the polynomial package instead.
157
169380
    Polynomial p = Polynomial::parsePolynomial(n);
158
84690
    d_type = p.isIntegral() ? ArithType::Integer : ArithType::Real;
159
  }else{
160
63223
    d_type = n.getType().isInteger() ? ArithType::Integer : ArithType::Real;
161
  }
162
163
147913
  Assert(initialized());
164
147913
}
165
166
void ArithVariables::VarInfo::uninitialize(){
167
  d_var = ARITHVAR_SENTINEL;
168
  d_node = Node::null();
169
}
170
171
5752214
bool ArithVariables::VarInfo::setAssignment(const DeltaRational& a, BoundsInfo& prev){
172
5752214
  Assert(initialized());
173
5752214
  d_assignment = a;
174
6961647
  int cmpUB = (d_ub == NullConstraint) ? -1 :
175
6961647
    d_assignment.cmp(d_ub->getValue());
176
177
7227660
  int cmpLB = (d_lb == NullConstraint) ? 1 :
178
7227660
    d_assignment.cmp(d_lb->getValue());
179
180
6313957
  bool lbChanged = cmpLB != d_cmpAssignmentLB &&
181
290740
    (cmpLB == 0 || d_cmpAssignmentLB == 0);
182
6228403
  bool ubChanged = cmpUB != d_cmpAssignmentUB &&
183
217060
    (cmpUB == 0 || d_cmpAssignmentUB == 0);
184
185
5752214
  if(lbChanged || ubChanged){
186
819373
    prev = boundsInfo();
187
  }
188
189
5752214
  d_cmpAssignmentUB = cmpUB;
190
5752214
  d_cmpAssignmentLB = cmpLB;
191
5752214
  return lbChanged || ubChanged;
192
}
193
194
void ArithVariables::releaseArithVar(ArithVar v){
195
  VarInfo& vi = d_vars.get(v);
196
197
  size_t removed CVC5_UNUSED = d_nodeToArithVarMap.erase(vi.d_node);
198
  Assert(removed == 1);
199
200
  vi.uninitialize();
201
202
  if(d_safeAssignment.isKey(v)){
203
    d_safeAssignment.remove(v);
204
  }
205
  if(vi.canBeReclaimed()){
206
    d_pool.push_back(v);
207
  }else{
208
    d_released.push_back(v);
209
  }
210
}
211
212
3378252
bool ArithVariables::VarInfo::setUpperBound(ConstraintP ub, BoundsInfo& prev){
213
3378252
  Assert(initialized());
214
3378252
  bool wasNull = d_ub == NullConstraint;
215
3378252
  bool isNull = ub == NullConstraint;
216
217
3378252
  int cmpUB = isNull ? -1 : d_assignment.cmp(ub->getValue());
218
6968912
  bool ubChanged = (wasNull != isNull) ||
219
618051
    (cmpUB != d_cmpAssignmentUB && (cmpUB == 0 || d_cmpAssignmentUB == 0));
220
3378252
  if(ubChanged){
221
3194160
    prev = boundsInfo();
222
  }
223
3378252
  d_ub = ub;
224
3378252
  d_cmpAssignmentUB = cmpUB;
225
3378252
  return ubChanged;
226
}
227
228
3560124
bool ArithVariables::VarInfo::setLowerBound(ConstraintP lb, BoundsInfo& prev){
229
3560124
  Assert(initialized());
230
3560124
  bool wasNull = d_lb == NullConstraint;
231
3560124
  bool isNull = lb == NullConstraint;
232
233
3560124
  int cmpLB = isNull ? 1 : d_assignment.cmp(lb->getValue());
234
235
7429784
  bool lbChanged = (wasNull != isNull) ||
236
1004429
    (cmpLB != d_cmpAssignmentLB && (cmpLB == 0 || d_cmpAssignmentLB == 0));
237
3560124
  if(lbChanged){
238
3183276
    prev = boundsInfo();
239
  }
240
3560124
  d_lb = lb;
241
3560124
  d_cmpAssignmentLB = cmpLB;
242
3560124
  return lbChanged;
243
}
244
245
75918802
BoundCounts ArithVariables::VarInfo::atBoundCounts() const {
246
75918802
  uint32_t lbIndc = (d_cmpAssignmentLB == 0) ? 1 : 0;
247
75918802
  uint32_t ubIndc = (d_cmpAssignmentUB == 0) ? 1 : 0;
248
75918802
  return BoundCounts(lbIndc, ubIndc);
249
}
250
251
68110876
BoundCounts ArithVariables::VarInfo::hasBoundCounts() const {
252
68110876
  uint32_t lbIndc = (d_lb != NullConstraint) ? 1 : 0;
253
68110876
  uint32_t ubIndc = (d_ub != NullConstraint) ? 1 : 0;
254
68110876
  return BoundCounts(lbIndc, ubIndc);
255
}
256
257
68110876
BoundsInfo ArithVariables::VarInfo::boundsInfo() const{
258
68110876
  return BoundsInfo(atBoundCounts(), hasBoundCounts());
259
}
260
261
bool ArithVariables::VarInfo::canBeReclaimed() const{
262
  return d_pushCount == 0;
263
}
264
265
bool ArithVariables::canBeReleased(ArithVar v) const{
266
  return d_vars[v].canBeReclaimed();
267
}
268
269
147913
void ArithVariables::attemptToReclaimReleased(){
270
147913
  size_t readPos = 0, writePos = 0, N = d_released.size();
271
147913
  for(; readPos < N; ++readPos){
272
    ArithVar v = d_released[readPos];
273
    if(canBeReleased(v)){
274
      d_pool.push_back(v);
275
    }else{
276
      d_released[writePos] = v;
277
      writePos++;
278
    }
279
  }
280
147913
  d_released.resize(writePos);
281
147913
}
282
283
147913
ArithVar ArithVariables::allocateVariable(){
284
147913
  if(d_pool.empty()){
285
147913
    attemptToReclaimReleased();
286
  }
287
147913
  bool reclaim = !d_pool.empty();
288
289
  ArithVar varX;
290
147913
  if(reclaim){
291
    varX = d_pool.back();
292
    d_pool.pop_back();
293
  }else{
294
147913
    varX = d_numberOfVariables;
295
147913
    ++d_numberOfVariables;
296
  }
297
147913
  d_vars.set(varX, VarInfo());
298
147913
  return varX;
299
}
300
301
302
16298
const Rational& ArithVariables::getDelta(){
303
16298
  if(!d_deltaIsSafe){
304
23782
    Rational nextDelta = d_deltaComputingFunc();
305
11891
    setDelta(nextDelta);
306
  }
307
16298
  Assert(d_deltaIsSafe);
308
16298
  return d_delta;
309
}
310
311
60157
bool ArithVariables::boundsAreEqual(ArithVar x) const{
312
60157
  if(hasLowerBound(x) && hasUpperBound(x)){
313
51303
    return getUpperBound(x) == getLowerBound(x);
314
  }else{
315
8854
    return false;
316
  }
317
}
318
319
320
std::pair<ConstraintP, ConstraintP> ArithVariables::explainEqualBounds(ArithVar x) const{
321
  Assert(boundsAreEqual(x));
322
323
  ConstraintP lb = getLowerBoundConstraint(x);
324
  ConstraintP ub = getUpperBoundConstraint(x);
325
  if(lb->isEquality()){
326
    return make_pair(lb, NullConstraint);
327
  }else if(ub->isEquality()){
328
    return make_pair(ub, NullConstraint);
329
  }else{
330
    return make_pair(lb, ub);
331
  }
332
}
333
334
5667524
void ArithVariables::setAssignment(ArithVar x, const DeltaRational& r){
335
11335048
  Debug("partial_model") << "pm: updating the assignment to" << x
336
5667524
                         << " now " << r <<endl;
337
5667524
  VarInfo& vi = d_vars.get(x);
338
5667524
  if(!d_safeAssignment.isKey(x)){
339
3215647
    d_safeAssignment.set(x, vi.d_assignment);
340
  }
341
5667524
  invalidateDelta();
342
343
5667524
  BoundsInfo prev;
344
5667524
  if(vi.setAssignment(r, prev)){
345
819373
    addToBoundQueue(x, prev);
346
  }
347
5667524
}
348
349
84690
void ArithVariables::setAssignment(ArithVar x, const DeltaRational& safe, const DeltaRational& r){
350
169380
  Debug("partial_model") << "pm: updating the assignment to" << x
351
84690
                         << " now " << r <<endl;
352
84690
  if(safe == r){
353
84383
    if(d_safeAssignment.isKey(x)){
354
      d_safeAssignment.remove(x);
355
    }
356
  }else{
357
307
    d_safeAssignment.set(x, safe);
358
  }
359
360
84690
  invalidateDelta();
361
84690
  VarInfo& vi = d_vars.get(x);
362
84690
  BoundsInfo prev;
363
84690
  if(vi.setAssignment(r, prev)){
364
    addToBoundQueue(x, prev);
365
  }
366
84690
}
367
368
147913
void ArithVariables::initialize(ArithVar x, Node n, bool aux){
369
147913
  VarInfo& vi = d_vars.get(x);
370
147913
  vi.initialize(x, n, aux);
371
147913
  d_nodeToArithVarMap[n] = x;
372
147913
}
373
374
147913
ArithVar ArithVariables::allocate(Node n, bool aux){
375
147913
  ArithVar v = allocateVariable();
376
147913
  initialize(v, n, aux);
377
147913
  return v;
378
}
379
380
// void ArithVariables::initialize(ArithVar x, const DeltaRational& r){
381
//   Assert(x == d_mapSize);
382
//   Assert(equalSizes());
383
//   ++d_mapSize;
384
385
//   // Is worth mentioning that this is not strictly necessary, but this maintains the internal invariant
386
//   // that when d_assignment is set this gets set.
387
//   invalidateDelta();
388
//   d_assignment.push_back( r );
389
390
//   d_boundRel.push_back(BetweenBounds);
391
392
//   d_ubc.push_back(NullConstraint);
393
//   d_lbc.push_back(NullConstraint);
394
// }
395
396
/** Must know that the bound exists both calling this! */
397
4231864
const DeltaRational& ArithVariables::getUpperBound(ArithVar x) const {
398
4231864
  Assert(inMaps(x));
399
4231864
  Assert(hasUpperBound(x));
400
401
4231864
  return getUpperBoundConstraint(x)->getValue();
402
}
403
404
4425885
const DeltaRational& ArithVariables::getLowerBound(ArithVar x) const {
405
4425885
  Assert(inMaps(x));
406
4425885
  Assert(hasLowerBound(x));
407
408
4425885
  return getLowerBoundConstraint(x)->getValue();
409
}
410
411
const DeltaRational& ArithVariables::getSafeAssignment(ArithVar x) const{
412
  Assert(inMaps(x));
413
  if(d_safeAssignment.isKey(x)){
414
    return d_safeAssignment[x];
415
  }else{
416
    return d_vars[x].d_assignment;
417
  }
418
}
419
420
590932
const DeltaRational& ArithVariables::getAssignment(ArithVar x, bool safe) const{
421
590932
  Assert(inMaps(x));
422
590932
  if(safe && d_safeAssignment.isKey(x)){
423
341
    return d_safeAssignment[x];
424
  }else{
425
590591
    return d_vars[x].d_assignment;
426
  }
427
}
428
429
125077817
const DeltaRational& ArithVariables::getAssignment(ArithVar x) const{
430
125077817
  Assert(inMaps(x));
431
125077817
  return d_vars[x].d_assignment;
432
}
433
434
435
1780062
void ArithVariables::setLowerBoundConstraint(ConstraintP c){
436
1780062
  AssertArgument(c != NullConstraint, "Cannot set a lower bound to NullConstraint.");
437
1780062
  AssertArgument(c->isEquality() || c->isLowerBound(),
438
                 "Constraint type must be set to an equality or UpperBound.");
439
1780062
  ArithVar x = c->getVariable();
440
1780062
  Debug("partial_model") << "setLowerBoundConstraint(" << x << ":" << c << ")" << endl;
441
1780062
  Assert(inMaps(x));
442
1780062
  Assert(greaterThanLowerBound(x, c->getValue()));
443
444
1780062
  invalidateDelta();
445
1780062
  VarInfo& vi = d_vars.get(x);
446
1780062
  pushLowerBound(vi);
447
1780062
  BoundsInfo prev;
448
1780062
  if(vi.setLowerBound(c, prev)){
449
1592773
    addToBoundQueue(x, prev);
450
  }
451
1780062
}
452
453
1689126
void ArithVariables::setUpperBoundConstraint(ConstraintP c){
454
1689126
  AssertArgument(c != NullConstraint, "Cannot set a upper bound to NullConstraint.");
455
1689126
  AssertArgument(c->isEquality() || c->isUpperBound(),
456
                 "Constraint type must be set to an equality or UpperBound.");
457
458
1689126
  ArithVar x = c->getVariable();
459
1689126
  Debug("partial_model") << "setUpperBoundConstraint(" << x << ":" << c << ")" << endl;
460
1689126
  Assert(inMaps(x));
461
1689126
  Assert(lessThanUpperBound(x, c->getValue()));
462
463
1689126
  invalidateDelta();
464
1689126
  VarInfo& vi = d_vars.get(x);
465
1689126
  pushUpperBound(vi);
466
1689126
  BoundsInfo prev;
467
1689126
  if(vi.setUpperBound(c, prev)){
468
1597474
    addToBoundQueue(x, prev);
469
  }
470
1689126
}
471
472
6412779
int ArithVariables::cmpToLowerBound(ArithVar x, const DeltaRational& c) const{
473
6412779
  if(!hasLowerBound(x)){
474
    // l = -\intfy
475
    // ? c < -\infty |-  _|_
476
4179542
    return 1;
477
  }else{
478
2233237
    return c.cmp(getLowerBound(x));
479
  }
480
}
481
482
5921380
int ArithVariables::cmpToUpperBound(ArithVar x, const DeltaRational& c) const{
483
5921380
  if(!hasUpperBound(x)){
484
    //u = \intfy
485
    // ? c > \infty |-  _|_
486
4067826
    return -1;
487
  }else{
488
1853554
    return c.cmp(getUpperBound(x));
489
  }
490
}
491
492
bool ArithVariables::equalsLowerBound(ArithVar x, const DeltaRational& c){
493
  if(!hasLowerBound(x)){
494
    return false;
495
  }else{
496
    return c == getLowerBound(x);
497
  }
498
}
499
bool ArithVariables::equalsUpperBound(ArithVar x, const DeltaRational& c){
500
  if(!hasUpperBound(x)){
501
    return false;
502
  }else{
503
    return c == getUpperBound(x);
504
  }
505
}
506
507
2528711
bool ArithVariables::hasEitherBound(ArithVar x) const{
508
2528711
  return hasLowerBound(x) || hasUpperBound(x);
509
}
510
511
1610467
bool ArithVariables::strictlyBelowUpperBound(ArithVar x) const{
512
1610467
  return d_vars[x].d_cmpAssignmentUB < 0;
513
}
514
515
3033194
bool ArithVariables::strictlyAboveLowerBound(ArithVar x) const{
516
3033194
  return d_vars[x].d_cmpAssignmentLB > 0;
517
}
518
519
14637034
bool ArithVariables::assignmentIsConsistent(ArithVar x) const{
520
  return
521
28387229
    d_vars[x].d_cmpAssignmentLB >= 0 &&
522
28387229
    d_vars[x].d_cmpAssignmentUB <= 0;
523
}
524
525
526
1377850
void ArithVariables::clearSafeAssignments(bool revert){
527
528
1377850
  if(revert && !d_safeAssignment.empty()){
529
    invalidateDelta();
530
  }
531
532
7809758
  while(!d_safeAssignment.empty()){
533
3215954
    ArithVar atBack = d_safeAssignment.back();
534
3215954
    if(revert){
535
      VarInfo& vi = d_vars.get(atBack);
536
      BoundsInfo prev;
537
      if(vi.setAssignment(d_safeAssignment[atBack], prev)){
538
        addToBoundQueue(atBack, prev);
539
      }
540
    }
541
3215954
    d_safeAssignment.pop_back();
542
  }
543
1377850
}
544
545
49477
void ArithVariables::revertAssignmentChanges(){
546
49477
  clearSafeAssignments(true);
547
49477
}
548
1328373
void ArithVariables::commitAssignmentChanges(){
549
1328373
  clearSafeAssignments(false);
550
1328373
}
551
552
827988
bool ArithVariables::lowerBoundIsZero(ArithVar x){
553
827988
  return hasLowerBound(x) && getLowerBound(x).sgn() == 0;
554
}
555
556
884613
bool ArithVariables::upperBoundIsZero(ArithVar x){
557
884613
  return hasUpperBound(x) && getUpperBound(x).sgn() == 0;
558
}
559
560
void ArithVariables::printEntireModel(std::ostream& out) const{
561
  out << "---Printing Model ---" << std::endl;
562
  for(var_iterator i = var_begin(), iend = var_end(); i != iend; ++i){
563
    printModel(*i, out);
564
  }
565
  out << "---Done Model ---" << std::endl;
566
}
567
568
void ArithVariables::printModel(ArithVar x, std::ostream& out) const{
569
  out << "model" << x << ": "
570
      << asNode(x) << " "
571
      << getAssignment(x) << " ";
572
  if(!hasLowerBound(x)){
573
    out << "no lb ";
574
  }else{
575
    out << getLowerBound(x) << " ";
576
    out << getLowerBoundConstraint(x) << " ";
577
  }
578
  if(!hasUpperBound(x)){
579
    out << "no ub ";
580
  }else{
581
    out << getUpperBound(x) << " ";
582
    out << getUpperBoundConstraint(x) << " ";
583
  }
584
585
  if(isInteger(x) && !integralAssignment(x)){
586
    out << "(not an integer)" << endl;
587
  }
588
  out << endl;
589
}
590
591
void ArithVariables::printModel(ArithVar x) const{
592
  printModel(x,  Debug("model"));
593
}
594
595
1689126
void ArithVariables::pushUpperBound(VarInfo& vi){
596
1689126
  ++vi.d_pushCount;
597
5158314
  d_ubRevertHistory.push_back(make_pair(vi.d_var, vi.d_ub));
598
1689126
}
599
1780062
void ArithVariables::pushLowerBound(VarInfo& vi){
600
1780062
  ++vi.d_pushCount;
601
1780062
  d_lbRevertHistory.push_back(make_pair(vi.d_var, vi.d_lb));
602
1780062
}
603
604
1689126
void ArithVariables::popUpperBound(AVCPair* c){
605
1689126
  ArithVar x = c->first;
606
1689126
  VarInfo& vi = d_vars.get(x);
607
1689126
  BoundsInfo prev;
608
1689126
  if(vi.setUpperBound(c->second, prev)){
609
1596686
    addToBoundQueue(x, prev);
610
  }
611
1689126
  --vi.d_pushCount;
612
1689126
}
613
614
1780062
void ArithVariables::popLowerBound(AVCPair* c){
615
1780062
  ArithVar x = c->first;
616
1780062
  VarInfo& vi = d_vars.get(x);
617
1780062
  BoundsInfo prev;
618
1780062
  if(vi.setLowerBound(c->second, prev)){
619
1590503
    addToBoundQueue(x, prev);
620
  }
621
1780062
  --vi.d_pushCount;
622
1780062
}
623
624
7196809
void ArithVariables::addToBoundQueue(ArithVar v, const BoundsInfo& prev){
625
7196809
  if(d_enqueueingBoundCounts && !d_boundsQueue.isKey(v)){
626
4113040
    d_boundsQueue.set(v, prev);
627
  }
628
7196809
}
629
630
380156
BoundsInfo ArithVariables::selectBoundsInfo(ArithVar v, bool old) const {
631
380156
  if(old && d_boundsQueue.isKey(v)){
632
13477
    return d_boundsQueue[v];
633
  }else{
634
366679
    return boundsInfo(v);
635
  }
636
}
637
638
13810010
bool ArithVariables::boundsQueueEmpty() const {
639
13810010
  return d_boundsQueue.empty();
640
}
641
642
6062519
void ArithVariables::processBoundsQueue(BoundUpdateCallback& changed){
643
10096312
  while(!boundsQueueEmpty()){
644
4033793
    ArithVar v = d_boundsQueue.back();
645
4033793
    BoundsInfo prev = d_boundsQueue[v];
646
4033793
    d_boundsQueue.pop_back();
647
4033793
    BoundsInfo curr = boundsInfo(v);
648
4033793
    if(prev != curr){
649
3846305
      changed(v, prev);
650
    }
651
  }
652
2028726
}
653
654
9444380
void ArithVariables::invalidateDelta() {
655
9444380
  d_deltaIsSafe = false;
656
9444380
}
657
658
11891
void ArithVariables::setDelta(const Rational& d){
659
11891
  d_delta = d;
660
11891
  d_deltaIsSafe = true;
661
11891
}
662
663
1267778
void ArithVariables::startQueueingBoundCounts(){
664
1267778
  d_enqueueingBoundCounts = true;
665
1267778
}
666
1267778
void ArithVariables::stopQueueingBoundCounts(){
667
1267778
  d_enqueueingBoundCounts = false;
668
1267778
}
669
670
137795686
bool ArithVariables::inMaps(ArithVar x) const{
671
137795686
  return x < getNumberOfVariables();
672
}
673
674
9459
ArithVariables::LowerBoundCleanUp::LowerBoundCleanUp(ArithVariables* pm)
675
9459
  : d_pm(pm)
676
9459
{}
677
1780062
void ArithVariables::LowerBoundCleanUp::operator()(AVCPair* p){
678
1780062
  d_pm->popLowerBound(p);
679
1780062
}
680
681
9459
ArithVariables::UpperBoundCleanUp::UpperBoundCleanUp(ArithVariables* pm)
682
9459
  : d_pm(pm)
683
9459
{}
684
1689126
void ArithVariables::UpperBoundCleanUp::operator()(AVCPair* p){
685
1689126
  d_pm->popUpperBound(p);
686
1689126
}
687
688
}  // namespace arith
689
}  // namespace theory
690
28191
}  // namespace cvc5