GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/partial_model.cpp Lines: 320 406 78.8 %
Date: 2021-11-06 Branches: 294 872 33.7 %

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
15272
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
30544
   d_lbRevertHistory(c, true, LowerBoundCleanUp(this)),
40
30544
   d_ubRevertHistory(c, true, UpperBoundCleanUp(this)),
41
   d_deltaIsSafe(false),
42
   d_delta(-1,1),
43
76360
   d_deltaComputingFunc(deltaComputingFunc)
44
15272
{ }
45
46
395784508
ArithVar ArithVariables::getNumberOfVariables() const {
47
395784508
  return d_numberOfVariables;
48
}
49
50
51
9439636
bool ArithVariables::hasArithVar(TNode x) const {
52
9439636
  return d_nodeToArithVarMap.find(x) != d_nodeToArithVarMap.end();
53
}
54
55
359210098
bool ArithVariables::hasNode(ArithVar a) const {
56
359210098
  return d_vars.isKey(a);
57
}
58
59
4108638
ArithVar ArithVariables::asArithVar(TNode x) const{
60
4108638
  Assert(hasArithVar(x));
61
4108638
  Assert((d_nodeToArithVarMap.find(x))->second <= ARITHVAR_SENTINEL);
62
4108638
  return (d_nodeToArithVarMap.find(x))->second;
63
}
64
65
355692528
Node ArithVariables::asNode(ArithVar a) const{
66
355692528
  Assert(hasNode(a));
67
355692528
  return d_vars[a].d_node;
68
}
69
70
ArithVariables::var_iterator::var_iterator()
71
  : d_vars(NULL)
72
  , d_wrapped()
73
{}
74
75
5057202
ArithVariables::var_iterator::var_iterator(const VarInfoVec* vars, VarInfoVec::const_iterator ci)
76
5057202
  : d_vars(vars), d_wrapped(ci)
77
{
78
5057202
  nextInitialized();
79
5057202
}
80
81
26607907
ArithVariables::var_iterator& ArithVariables::var_iterator::operator++(){
82
26607907
  ++d_wrapped;
83
26607907
  nextInitialized();
84
26607907
  return *this;
85
}
86
bool ArithVariables::var_iterator::operator==(const ArithVariables::var_iterator& other) const{
87
  return d_wrapped == other.d_wrapped;
88
}
89
29136508
bool ArithVariables::var_iterator::operator!=(const ArithVariables::var_iterator& other) const{
90
29136508
  return d_wrapped != other.d_wrapped;
91
}
92
26607907
ArithVar ArithVariables::var_iterator::operator*() const{
93
26607907
  return *d_wrapped;
94
}
95
96
31665109
void ArithVariables::var_iterator::nextInitialized(){
97
31665109
  VarInfoVec::const_iterator end = d_vars->end();
98
60628505
  while(d_wrapped != end &&
99
28963396
        !((*d_vars)[*d_wrapped].initialized())){
100
    ++d_wrapped;
101
  }
102
31665109
}
103
104
2528601
ArithVariables::var_iterator ArithVariables::var_begin() const {
105
2528601
  return var_iterator(&d_vars, d_vars.begin());
106
}
107
108
2528601
ArithVariables::var_iterator ArithVariables::var_end() const {
109
2528601
  return var_iterator(&d_vars, d_vars.end());
110
}
111
1130368471
bool ArithVariables::isInteger(ArithVar x) const {
112
1130368471
  return d_vars[x].d_type >= ArithType::Integer;
113
}
114
115
/** Is the assignment to x integral? */
116
331855944
bool ArithVariables::integralAssignment(ArithVar x) const {
117
331855944
  return getAssignment(x).isIntegral();
118
}
119
951989283
bool ArithVariables::isAuxiliary(ArithVar x) const {
120
951989283
  return d_vars[x].d_auxiliary;
121
}
122
123
1105324329
bool ArithVariables::isIntegerInput(ArithVar x) const {
124
1105324329
  return isInteger(x) && !isAuxiliary(x);
125
}
126
127
365500
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
365500
      d_auxiliary(false) {}
138
139
48265120
bool ArithVariables::VarInfo::initialized() const {
140
48265120
  return d_var != ARITHVAR_SENTINEL;
141
}
142
143
182750
void ArithVariables::VarInfo::initialize(ArithVar v, Node n, bool aux){
144
182750
  Assert(!initialized());
145
182750
  Assert(d_lb == NullConstraint);
146
182750
  Assert(d_ub == NullConstraint);
147
182750
  Assert(d_cmpAssignmentLB > 0);
148
182750
  Assert(d_cmpAssignmentUB < 0);
149
182750
  d_var = v;
150
182750
  d_node = n;
151
182750
  d_auxiliary = aux;
152
153
182750
  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
206514
    Polynomial p = Polynomial::parsePolynomial(n);
158
103257
    d_type = p.isIntegral() ? ArithType::Integer : ArithType::Real;
159
  }else{
160
79493
    d_type = n.getType().isInteger() ? ArithType::Integer : ArithType::Real;
161
  }
162
163
182750
  Assert(initialized());
164
182750
}
165
166
void ArithVariables::VarInfo::uninitialize(){
167
  d_var = ARITHVAR_SENTINEL;
168
  d_node = Node::null();
169
}
170
171
8549670
bool ArithVariables::VarInfo::setAssignment(const DeltaRational& a, BoundsInfo& prev){
172
8549670
  Assert(initialized());
173
8549670
  d_assignment = a;
174
10231753
  int cmpUB = (d_ub == NullConstraint) ? -1 :
175
10231753
    d_assignment.cmp(d_ub->getValue());
176
177
11452545
  int cmpLB = (d_lb == NullConstraint) ? 1 :
178
11452545
    d_assignment.cmp(d_lb->getValue());
179
180
9317208
  bool lbChanged = cmpLB != d_cmpAssignmentLB &&
181
404474
    (cmpLB == 0 || d_cmpAssignmentLB == 0);
182
9140005
  bool ubChanged = cmpUB != d_cmpAssignmentUB &&
183
265386
    (cmpUB == 0 || d_cmpAssignmentUB == 0);
184
185
8549670
  if(lbChanged || ubChanged){
186
1084297
    prev = boundsInfo();
187
  }
188
189
8549670
  d_cmpAssignmentUB = cmpUB;
190
8549670
  d_cmpAssignmentLB = cmpLB;
191
8549670
  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
5152740
bool ArithVariables::VarInfo::setUpperBound(ConstraintP ub, BoundsInfo& prev){
213
5152740
  Assert(initialized());
214
5152740
  bool wasNull = d_ub == NullConstraint;
215
5152740
  bool isNull = ub == NullConstraint;
216
217
5152740
  int cmpUB = isNull ? -1 : d_assignment.cmp(ub->getValue());
218
10595747
  bool ubChanged = (wasNull != isNull) ||
219
904828
    (cmpUB != d_cmpAssignmentUB && (cmpUB == 0 || d_cmpAssignmentUB == 0));
220
5152740
  if(ubChanged){
221
4837717
    prev = boundsInfo();
222
  }
223
5152740
  d_ub = ub;
224
5152740
  d_cmpAssignmentUB = cmpUB;
225
5152740
  return ubChanged;
226
}
227
228
5233814
bool ArithVariables::VarInfo::setLowerBound(ConstraintP lb, BoundsInfo& prev){
229
5233814
  Assert(initialized());
230
5233814
  bool wasNull = d_lb == NullConstraint;
231
5233814
  bool isNull = lb == NullConstraint;
232
233
5233814
  int cmpLB = isNull ? 1 : d_assignment.cmp(lb->getValue());
234
235
10888934
  bool lbChanged = (wasNull != isNull) ||
236
1506741
    (cmpLB != d_cmpAssignmentLB && (cmpLB == 0 || d_cmpAssignmentLB == 0));
237
5233814
  if(lbChanged){
238
4579136
    prev = boundsInfo();
239
  }
240
5233814
  d_lb = lb;
241
5233814
  d_cmpAssignmentLB = cmpLB;
242
5233814
  return lbChanged;
243
}
244
245
102588151
BoundCounts ArithVariables::VarInfo::atBoundCounts() const {
246
102588151
  uint32_t lbIndc = (d_cmpAssignmentLB == 0) ? 1 : 0;
247
102588151
  uint32_t ubIndc = (d_cmpAssignmentUB == 0) ? 1 : 0;
248
102588151
  return BoundCounts(lbIndc, ubIndc);
249
}
250
251
90556551
BoundCounts ArithVariables::VarInfo::hasBoundCounts() const {
252
90556551
  uint32_t lbIndc = (d_lb != NullConstraint) ? 1 : 0;
253
90556551
  uint32_t ubIndc = (d_ub != NullConstraint) ? 1 : 0;
254
90556551
  return BoundCounts(lbIndc, ubIndc);
255
}
256
257
90556551
BoundsInfo ArithVariables::VarInfo::boundsInfo() const{
258
90556551
  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
182750
void ArithVariables::attemptToReclaimReleased(){
270
182750
  size_t readPos = 0, writePos = 0, N = d_released.size();
271
182750
  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
182750
  d_released.resize(writePos);
281
182750
}
282
283
182750
ArithVar ArithVariables::allocateVariable(){
284
182750
  if(d_pool.empty()){
285
182750
    attemptToReclaimReleased();
286
  }
287
182750
  bool reclaim = !d_pool.empty();
288
289
  ArithVar varX;
290
182750
  if(reclaim){
291
    varX = d_pool.back();
292
    d_pool.pop_back();
293
  }else{
294
182750
    varX = d_numberOfVariables;
295
182750
    ++d_numberOfVariables;
296
  }
297
182750
  d_vars.set(varX, VarInfo());
298
182750
  return varX;
299
}
300
301
302
83689
const Rational& ArithVariables::getDelta(){
303
83689
  if(!d_deltaIsSafe){
304
114788
    Rational nextDelta = d_deltaComputingFunc();
305
57394
    setDelta(nextDelta);
306
  }
307
83689
  Assert(d_deltaIsSafe);
308
83689
  return d_delta;
309
}
310
311
69272
bool ArithVariables::boundsAreEqual(ArithVar x) const{
312
69272
  if(hasLowerBound(x) && hasUpperBound(x)){
313
57279
    return getUpperBound(x) == getLowerBound(x);
314
  }else{
315
11993
    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
8446413
void ArithVariables::setAssignment(ArithVar x, const DeltaRational& r){
335
16892826
  Debug("partial_model") << "pm: updating the assignment to" << x
336
8446413
                         << " now " << r <<endl;
337
8446413
  VarInfo& vi = d_vars.get(x);
338
8446413
  if(!d_safeAssignment.isKey(x)){
339
4493552
    d_safeAssignment.set(x, vi.d_assignment);
340
  }
341
8446413
  invalidateDelta();
342
343
8446413
  BoundsInfo prev;
344
8446413
  if(vi.setAssignment(r, prev)){
345
1084297
    addToBoundQueue(x, prev);
346
  }
347
8446413
}
348
349
103257
void ArithVariables::setAssignment(ArithVar x, const DeltaRational& safe, const DeltaRational& r){
350
206514
  Debug("partial_model") << "pm: updating the assignment to" << x
351
103257
                         << " now " << r <<endl;
352
103257
  if(safe == r){
353
102780
    if(d_safeAssignment.isKey(x)){
354
      d_safeAssignment.remove(x);
355
    }
356
  }else{
357
477
    d_safeAssignment.set(x, safe);
358
  }
359
360
103257
  invalidateDelta();
361
103257
  VarInfo& vi = d_vars.get(x);
362
103257
  BoundsInfo prev;
363
103257
  if(vi.setAssignment(r, prev)){
364
    addToBoundQueue(x, prev);
365
  }
366
103257
}
367
368
182750
void ArithVariables::initialize(ArithVar x, Node n, bool aux){
369
182750
  VarInfo& vi = d_vars.get(x);
370
182750
  vi.initialize(x, n, aux);
371
182750
  d_nodeToArithVarMap[n] = x;
372
182750
}
373
374
182750
ArithVar ArithVariables::allocate(Node n, bool aux){
375
182750
  ArithVar v = allocateVariable();
376
182750
  initialize(v, n, aux);
377
182750
  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
8676830
const DeltaRational& ArithVariables::getUpperBound(ArithVar x) const {
398
8676830
  Assert(inMaps(x));
399
8676830
  Assert(hasUpperBound(x));
400
401
8676830
  return getUpperBoundConstraint(x)->getValue();
402
}
403
404
9750146
const DeltaRational& ArithVariables::getLowerBound(ArithVar x) const {
405
9750146
  Assert(inMaps(x));
406
9750146
  Assert(hasLowerBound(x));
407
408
9750146
  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
816208
const DeltaRational& ArithVariables::getAssignment(ArithVar x, bool safe) const{
421
816208
  Assert(inMaps(x));
422
816208
  if(safe && d_safeAssignment.isKey(x)){
423
513
    return d_safeAssignment[x];
424
  }else{
425
815695
    return d_vars[x].d_assignment;
426
  }
427
}
428
429
365986914
const DeltaRational& ArithVariables::getAssignment(ArithVar x) const{
430
365986914
  Assert(inMaps(x));
431
365986914
  return d_vars[x].d_assignment;
432
}
433
434
435
2616907
void ArithVariables::setLowerBoundConstraint(ConstraintP c){
436
2616907
  AssertArgument(c != NullConstraint, "Cannot set a lower bound to NullConstraint.");
437
2616907
  AssertArgument(c->isEquality() || c->isLowerBound(),
438
                 "Constraint type must be set to an equality or UpperBound.");
439
2616907
  ArithVar x = c->getVariable();
440
2616907
  Debug("partial_model") << "setLowerBoundConstraint(" << x << ":" << c << ")" << endl;
441
2616907
  Assert(inMaps(x));
442
2616907
  Assert(greaterThanLowerBound(x, c->getValue()));
443
444
2616907
  invalidateDelta();
445
2616907
  VarInfo& vi = d_vars.get(x);
446
2616907
  pushLowerBound(vi);
447
2616907
  BoundsInfo prev;
448
2616907
  if(vi.setLowerBound(c, prev)){
449
2291909
    addToBoundQueue(x, prev);
450
  }
451
2616907
}
452
453
2576370
void ArithVariables::setUpperBoundConstraint(ConstraintP c){
454
2576370
  AssertArgument(c != NullConstraint, "Cannot set a upper bound to NullConstraint.");
455
2576370
  AssertArgument(c->isEquality() || c->isUpperBound(),
456
                 "Constraint type must be set to an equality or UpperBound.");
457
458
2576370
  ArithVar x = c->getVariable();
459
2576370
  Debug("partial_model") << "setUpperBoundConstraint(" << x << ":" << c << ")" << endl;
460
2576370
  Assert(inMaps(x));
461
2576370
  Assert(lessThanUpperBound(x, c->getValue()));
462
463
2576370
  invalidateDelta();
464
2576370
  VarInfo& vi = d_vars.get(x);
465
2576370
  pushUpperBound(vi);
466
2576370
  BoundsInfo prev;
467
2576370
  if(vi.setUpperBound(c, prev)){
468
2419900
    addToBoundQueue(x, prev);
469
  }
470
2576370
}
471
472
9514383
int ArithVariables::cmpToLowerBound(ArithVar x, const DeltaRational& c) const{
473
9514383
  if(!hasLowerBound(x)){
474
    // l = -\intfy
475
    // ? c < -\infty |-  _|_
476
6321707
    return 1;
477
  }else{
478
3192676
    return c.cmp(getLowerBound(x));
479
  }
480
}
481
482
9090972
int ArithVariables::cmpToUpperBound(ArithVar x, const DeltaRational& c) const{
483
9090972
  if(!hasUpperBound(x)){
484
    //u = \intfy
485
    // ? c > \infty |-  _|_
486
6509738
    return -1;
487
  }else{
488
2581234
    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
2776151
bool ArithVariables::hasEitherBound(ArithVar x) const{
508
2776151
  return hasLowerBound(x) || hasUpperBound(x);
509
}
510
511
1875053
bool ArithVariables::strictlyBelowUpperBound(ArithVar x) const{
512
1875053
  return d_vars[x].d_cmpAssignmentUB < 0;
513
}
514
515
3379549
bool ArithVariables::strictlyAboveLowerBound(ArithVar x) const{
516
3379549
  return d_vars[x].d_cmpAssignmentLB > 0;
517
}
518
519
21651284
bool ArithVariables::assignmentIsConsistent(ArithVar x) const{
520
  return
521
42091054
    d_vars[x].d_cmpAssignmentLB >= 0 &&
522
42091054
    d_vars[x].d_cmpAssignmentUB <= 0;
523
}
524
525
526
2541110
void ArithVariables::clearSafeAssignments(bool revert){
527
528
2541110
  if(revert && !d_safeAssignment.empty()){
529
    invalidateDelta();
530
  }
531
532
11529168
  while(!d_safeAssignment.empty()){
533
4494029
    ArithVar atBack = d_safeAssignment.back();
534
4494029
    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
4494029
    d_safeAssignment.pop_back();
542
  }
543
2541110
}
544
545
67962
void ArithVariables::revertAssignmentChanges(){
546
67962
  clearSafeAssignments(true);
547
67962
}
548
2473148
void ArithVariables::commitAssignmentChanges(){
549
2473148
  clearSafeAssignments(false);
550
2473148
}
551
552
917242
bool ArithVariables::lowerBoundIsZero(ArithVar x){
553
917242
  return hasLowerBound(x) && getLowerBound(x).sgn() == 0;
554
}
555
556
925728
bool ArithVariables::upperBoundIsZero(ArithVar x){
557
925728
  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
2576370
void ArithVariables::pushUpperBound(VarInfo& vi){
596
2576370
  ++vi.d_pushCount;
597
7769647
  d_ubRevertHistory.push_back(make_pair(vi.d_var, vi.d_ub));
598
2576370
}
599
2616907
void ArithVariables::pushLowerBound(VarInfo& vi){
600
2616907
  ++vi.d_pushCount;
601
2616907
  d_lbRevertHistory.push_back(make_pair(vi.d_var, vi.d_lb));
602
2616907
}
603
604
2576370
void ArithVariables::popUpperBound(AVCPair* c){
605
2576370
  ArithVar x = c->first;
606
2576370
  VarInfo& vi = d_vars.get(x);
607
2576370
  BoundsInfo prev;
608
2576370
  if(vi.setUpperBound(c->second, prev)){
609
2417817
    addToBoundQueue(x, prev);
610
  }
611
2576370
  --vi.d_pushCount;
612
2576370
}
613
614
2616907
void ArithVariables::popLowerBound(AVCPair* c){
615
2616907
  ArithVar x = c->first;
616
2616907
  VarInfo& vi = d_vars.get(x);
617
2616907
  BoundsInfo prev;
618
2616907
  if(vi.setLowerBound(c->second, prev)){
619
2287227
    addToBoundQueue(x, prev);
620
  }
621
2616907
  --vi.d_pushCount;
622
2616907
}
623
624
10501150
void ArithVariables::addToBoundQueue(ArithVar v, const BoundsInfo& prev){
625
10501150
  if(d_enqueueingBoundCounts && !d_boundsQueue.isKey(v)){
626
6170950
    d_boundsQueue.set(v, prev);
627
  }
628
10501150
}
629
630
511361
BoundsInfo ArithVariables::selectBoundsInfo(ArithVar v, bool old) const {
631
511361
  if(old && d_boundsQueue.isKey(v)){
632
16244
    return d_boundsQueue[v];
633
  }else{
634
495117
    return boundsInfo(v);
635
  }
636
}
637
638
22083625
bool ArithVariables::boundsQueueEmpty() const {
639
22083625
  return d_boundsQueue.empty();
640
}
641
642
9829813
void ArithVariables::processBoundsQueue(BoundUpdateCallback& changed){
643
15899269
  while(!boundsQueueEmpty()){
644
6069456
    ArithVar v = d_boundsQueue.back();
645
6069456
    BoundsInfo prev = d_boundsQueue[v];
646
6069456
    d_boundsQueue.pop_back();
647
6069456
    BoundsInfo curr = boundsInfo(v);
648
6069456
    if(prev != curr){
649
5854381
      changed(v, prev);
650
    }
651
  }
652
3760357
}
653
654
14171038
void ArithVariables::invalidateDelta() {
655
14171038
  d_deltaIsSafe = false;
656
14171038
}
657
658
57394
void ArithVariables::setDelta(const Rational& d){
659
57394
  d_delta = d;
660
57394
  d_deltaIsSafe = true;
661
57394
}
662
663
2388335
void ArithVariables::startQueueingBoundCounts(){
664
2388335
  d_enqueueingBoundCounts = true;
665
2388335
}
666
2388335
void ArithVariables::stopQueueingBoundCounts(){
667
2388335
  d_enqueueingBoundCounts = false;
668
2388335
}
669
670
390423375
bool ArithVariables::inMaps(ArithVar x) const{
671
390423375
  return x < getNumberOfVariables();
672
}
673
674
15272
ArithVariables::LowerBoundCleanUp::LowerBoundCleanUp(ArithVariables* pm)
675
15272
  : d_pm(pm)
676
15272
{}
677
2616907
void ArithVariables::LowerBoundCleanUp::operator()(AVCPair* p){
678
2616907
  d_pm->popLowerBound(p);
679
2616907
}
680
681
15272
ArithVariables::UpperBoundCleanUp::UpperBoundCleanUp(ArithVariables* pm)
682
15272
  : d_pm(pm)
683
15272
{}
684
2576370
void ArithVariables::UpperBoundCleanUp::operator()(AVCPair* p){
685
2576370
  d_pm->popUpperBound(p);
686
2576370
}
687
688
}  // namespace arith
689
}  // namespace theory
690
31137
}  // namespace cvc5