GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/partial_model.cpp Lines: 320 406 78.8 %
Date: 2021-11-08 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
15275
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
30550
   d_lbRevertHistory(c, true, LowerBoundCleanUp(this)),
40
30550
   d_ubRevertHistory(c, true, UpperBoundCleanUp(this)),
41
   d_deltaIsSafe(false),
42
   d_delta(-1,1),
43
76375
   d_deltaComputingFunc(deltaComputingFunc)
44
15275
{ }
45
46
362271795
ArithVar ArithVariables::getNumberOfVariables() const {
47
362271795
  return d_numberOfVariables;
48
}
49
50
51
10323284
bool ArithVariables::hasArithVar(TNode x) const {
52
10323284
  return d_nodeToArithVarMap.find(x) != d_nodeToArithVarMap.end();
53
}
54
55
311302454
bool ArithVariables::hasNode(ArithVar a) const {
56
311302454
  return d_vars.isKey(a);
57
}
58
59
4320246
ArithVar ArithVariables::asArithVar(TNode x) const{
60
4320246
  Assert(hasArithVar(x));
61
4320246
  Assert((d_nodeToArithVarMap.find(x))->second <= ARITHVAR_SENTINEL);
62
4320246
  return (d_nodeToArithVarMap.find(x))->second;
63
}
64
65
306645922
Node ArithVariables::asNode(ArithVar a) const{
66
306645922
  Assert(hasNode(a));
67
306645922
  return d_vars[a].d_node;
68
}
69
70
ArithVariables::var_iterator::var_iterator()
71
  : d_vars(NULL)
72
  , d_wrapped()
73
{}
74
75
5343396
ArithVariables::var_iterator::var_iterator(const VarInfoVec* vars, VarInfoVec::const_iterator ci)
76
5343396
  : d_vars(vars), d_wrapped(ci)
77
{
78
5343396
  nextInitialized();
79
5343396
}
80
81
27259560
ArithVariables::var_iterator& ArithVariables::var_iterator::operator++(){
82
27259560
  ++d_wrapped;
83
27259560
  nextInitialized();
84
27259560
  return *this;
85
}
86
bool ArithVariables::var_iterator::operator==(const ArithVariables::var_iterator& other) const{
87
  return d_wrapped == other.d_wrapped;
88
}
89
29931258
bool ArithVariables::var_iterator::operator!=(const ArithVariables::var_iterator& other) const{
90
29931258
  return d_wrapped != other.d_wrapped;
91
}
92
27259560
ArithVar ArithVariables::var_iterator::operator*() const{
93
27259560
  return *d_wrapped;
94
}
95
96
32602956
void ArithVariables::var_iterator::nextInitialized(){
97
32602956
  VarInfoVec::const_iterator end = d_vars->end();
98
62353571
  while(d_wrapped != end &&
99
29750615
        !((*d_vars)[*d_wrapped].initialized())){
100
    ++d_wrapped;
101
  }
102
32602956
}
103
104
2671698
ArithVariables::var_iterator ArithVariables::var_begin() const {
105
2671698
  return var_iterator(&d_vars, d_vars.begin());
106
}
107
108
2671698
ArithVariables::var_iterator ArithVariables::var_end() const {
109
2671698
  return var_iterator(&d_vars, d_vars.end());
110
}
111
996920312
bool ArithVariables::isInteger(ArithVar x) const {
112
996920312
  return d_vars[x].d_type >= ArithType::Integer;
113
}
114
115
/** Is the assignment to x integral? */
116
297204875
bool ArithVariables::integralAssignment(ArithVar x) const {
117
297204875
  return getAssignment(x).isIntegral();
118
}
119
818656070
bool ArithVariables::isAuxiliary(ArithVar x) const {
120
818656070
  return d_vars[x].d_auxiliary;
121
}
122
123
971327299
bool ArithVariables::isIntegerInput(ArithVar x) const {
124
971327299
  return isInteger(x) && !isAuxiliary(x);
125
}
126
127
363250
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
363250
      d_auxiliary(false) {}
138
139
49329671
bool ArithVariables::VarInfo::initialized() const {
140
49329671
  return d_var != ARITHVAR_SENTINEL;
141
}
142
143
181625
void ArithVariables::VarInfo::initialize(ArithVar v, Node n, bool aux){
144
181625
  Assert(!initialized());
145
181625
  Assert(d_lb == NullConstraint);
146
181625
  Assert(d_ub == NullConstraint);
147
181625
  Assert(d_cmpAssignmentLB > 0);
148
181625
  Assert(d_cmpAssignmentUB < 0);
149
181625
  d_var = v;
150
181625
  d_node = n;
151
181625
  d_auxiliary = aux;
152
153
181625
  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
205090
    Polynomial p = Polynomial::parsePolynomial(n);
158
102545
    d_type = p.isIntegral() ? ArithType::Integer : ArithType::Real;
159
  }else{
160
79080
    d_type = n.getType().isInteger() ? ArithType::Integer : ArithType::Real;
161
  }
162
163
181625
  Assert(initialized());
164
181625
}
165
166
void ArithVariables::VarInfo::uninitialize(){
167
  d_var = ARITHVAR_SENTINEL;
168
  d_node = Node::null();
169
}
170
171
8633576
bool ArithVariables::VarInfo::setAssignment(const DeltaRational& a, BoundsInfo& prev){
172
8633576
  Assert(initialized());
173
8633576
  d_assignment = a;
174
10341291
  int cmpUB = (d_ub == NullConstraint) ? -1 :
175
10341291
    d_assignment.cmp(d_ub->getValue());
176
177
11559309
  int cmpLB = (d_lb == NullConstraint) ? 1 :
178
11559309
    d_assignment.cmp(d_lb->getValue());
179
180
9423499
  bool lbChanged = cmpLB != d_cmpAssignmentLB &&
181
406626
    (cmpLB == 0 || d_cmpAssignmentLB == 0);
182
9243156
  bool ubChanged = cmpUB != d_cmpAssignmentUB &&
183
267186
    (cmpUB == 0 || d_cmpAssignmentUB == 0);
184
185
8633576
  if(lbChanged || ubChanged){
186
1109391
    prev = boundsInfo();
187
  }
188
189
8633576
  d_cmpAssignmentUB = cmpUB;
190
8633576
  d_cmpAssignmentLB = cmpLB;
191
8633576
  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
5271654
bool ArithVariables::VarInfo::setUpperBound(ConstraintP ub, BoundsInfo& prev){
213
5271654
  Assert(initialized());
214
5271654
  bool wasNull = d_ub == NullConstraint;
215
5271654
  bool isNull = ub == NullConstraint;
216
217
5271654
  int cmpUB = isNull ? -1 : d_assignment.cmp(ub->getValue());
218
10852575
  bool ubChanged = (wasNull != isNull) ||
219
939534
    (cmpUB != d_cmpAssignmentUB && (cmpUB == 0 || d_cmpAssignmentUB == 0));
220
5271654
  if(ubChanged){
221
4959959
    prev = boundsInfo();
222
  }
223
5271654
  d_ub = ub;
224
5271654
  d_cmpAssignmentUB = cmpUB;
225
5271654
  return ubChanged;
226
}
227
228
5310576
bool ArithVariables::VarInfo::setLowerBound(ConstraintP lb, BoundsInfo& prev){
229
5310576
  Assert(initialized());
230
5310576
  bool wasNull = d_lb == NullConstraint;
231
5310576
  bool isNull = lb == NullConstraint;
232
233
5310576
  int cmpLB = isNull ? 1 : d_assignment.cmp(lb->getValue());
234
235
11053451
  bool lbChanged = (wasNull != isNull) ||
236
1544046
    (cmpLB != d_cmpAssignmentLB && (cmpLB == 0 || d_cmpAssignmentLB == 0));
237
5310576
  if(lbChanged){
238
4641023
    prev = boundsInfo();
239
  }
240
5310576
  d_lb = lb;
241
5310576
  d_cmpAssignmentLB = cmpLB;
242
5310576
  return lbChanged;
243
}
244
245
102778597
BoundCounts ArithVariables::VarInfo::atBoundCounts() const {
246
102778597
  uint32_t lbIndc = (d_cmpAssignmentLB == 0) ? 1 : 0;
247
102778597
  uint32_t ubIndc = (d_cmpAssignmentUB == 0) ? 1 : 0;
248
102778597
  return BoundCounts(lbIndc, ubIndc);
249
}
250
251
90751697
BoundCounts ArithVariables::VarInfo::hasBoundCounts() const {
252
90751697
  uint32_t lbIndc = (d_lb != NullConstraint) ? 1 : 0;
253
90751697
  uint32_t ubIndc = (d_ub != NullConstraint) ? 1 : 0;
254
90751697
  return BoundCounts(lbIndc, ubIndc);
255
}
256
257
90751697
BoundsInfo ArithVariables::VarInfo::boundsInfo() const{
258
90751697
  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
181625
void ArithVariables::attemptToReclaimReleased(){
270
181625
  size_t readPos = 0, writePos = 0, N = d_released.size();
271
181625
  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
181625
  d_released.resize(writePos);
281
181625
}
282
283
181625
ArithVar ArithVariables::allocateVariable(){
284
181625
  if(d_pool.empty()){
285
181625
    attemptToReclaimReleased();
286
  }
287
181625
  bool reclaim = !d_pool.empty();
288
289
  ArithVar varX;
290
181625
  if(reclaim){
291
    varX = d_pool.back();
292
    d_pool.pop_back();
293
  }else{
294
181625
    varX = d_numberOfVariables;
295
181625
    ++d_numberOfVariables;
296
  }
297
181625
  d_vars.set(varX, VarInfo());
298
181625
  return varX;
299
}
300
301
302
87403
const Rational& ArithVariables::getDelta(){
303
87403
  if(!d_deltaIsSafe){
304
122324
    Rational nextDelta = d_deltaComputingFunc();
305
61162
    setDelta(nextDelta);
306
  }
307
87403
  Assert(d_deltaIsSafe);
308
87403
  return d_delta;
309
}
310
311
70512
bool ArithVariables::boundsAreEqual(ArithVar x) const{
312
70512
  if(hasLowerBound(x) && hasUpperBound(x)){
313
58519
    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
8531031
void ArithVariables::setAssignment(ArithVar x, const DeltaRational& r){
335
17062062
  Debug("partial_model") << "pm: updating the assignment to" << x
336
8531031
                         << " now " << r <<endl;
337
8531031
  VarInfo& vi = d_vars.get(x);
338
8531031
  if(!d_safeAssignment.isKey(x)){
339
4567134
    d_safeAssignment.set(x, vi.d_assignment);
340
  }
341
8531031
  invalidateDelta();
342
343
8531031
  BoundsInfo prev;
344
8531031
  if(vi.setAssignment(r, prev)){
345
1109391
    addToBoundQueue(x, prev);
346
  }
347
8531031
}
348
349
102545
void ArithVariables::setAssignment(ArithVar x, const DeltaRational& safe, const DeltaRational& r){
350
205090
  Debug("partial_model") << "pm: updating the assignment to" << x
351
102545
                         << " now " << r <<endl;
352
102545
  if(safe == r){
353
102050
    if(d_safeAssignment.isKey(x)){
354
      d_safeAssignment.remove(x);
355
    }
356
  }else{
357
495
    d_safeAssignment.set(x, safe);
358
  }
359
360
102545
  invalidateDelta();
361
102545
  VarInfo& vi = d_vars.get(x);
362
102545
  BoundsInfo prev;
363
102545
  if(vi.setAssignment(r, prev)){
364
    addToBoundQueue(x, prev);
365
  }
366
102545
}
367
368
181625
void ArithVariables::initialize(ArithVar x, Node n, bool aux){
369
181625
  VarInfo& vi = d_vars.get(x);
370
181625
  vi.initialize(x, n, aux);
371
181625
  d_nodeToArithVarMap[n] = x;
372
181625
}
373
374
181625
ArithVar ArithVariables::allocate(Node n, bool aux){
375
181625
  ArithVar v = allocateVariable();
376
181625
  initialize(v, n, aux);
377
181625
  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
8937347
const DeltaRational& ArithVariables::getUpperBound(ArithVar x) const {
398
8937347
  Assert(inMaps(x));
399
8937347
  Assert(hasUpperBound(x));
400
401
8937347
  return getUpperBoundConstraint(x)->getValue();
402
}
403
404
10042519
const DeltaRational& ArithVariables::getLowerBound(ArithVar x) const {
405
10042519
  Assert(inMaps(x));
406
10042519
  Assert(hasLowerBound(x));
407
408
10042519
  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
797868
const DeltaRational& ArithVariables::getAssignment(ArithVar x, bool safe) const{
421
797868
  Assert(inMaps(x));
422
797868
  if(safe && d_safeAssignment.isKey(x)){
423
531
    return d_safeAssignment[x];
424
  }else{
425
797337
    return d_vars[x].d_assignment;
426
  }
427
}
428
429
331561513
const DeltaRational& ArithVariables::getAssignment(ArithVar x) const{
430
331561513
  Assert(inMaps(x));
431
331561513
  return d_vars[x].d_assignment;
432
}
433
434
435
2655288
void ArithVariables::setLowerBoundConstraint(ConstraintP c){
436
2655288
  AssertArgument(c != NullConstraint, "Cannot set a lower bound to NullConstraint.");
437
2655288
  AssertArgument(c->isEquality() || c->isLowerBound(),
438
                 "Constraint type must be set to an equality or UpperBound.");
439
2655288
  ArithVar x = c->getVariable();
440
2655288
  Debug("partial_model") << "setLowerBoundConstraint(" << x << ":" << c << ")" << endl;
441
2655288
  Assert(inMaps(x));
442
2655288
  Assert(greaterThanLowerBound(x, c->getValue()));
443
444
2655288
  invalidateDelta();
445
2655288
  VarInfo& vi = d_vars.get(x);
446
2655288
  pushLowerBound(vi);
447
2655288
  BoundsInfo prev;
448
2655288
  if(vi.setLowerBound(c, prev)){
449
2323180
    addToBoundQueue(x, prev);
450
  }
451
2655288
}
452
453
2635827
void ArithVariables::setUpperBoundConstraint(ConstraintP c){
454
2635827
  AssertArgument(c != NullConstraint, "Cannot set a upper bound to NullConstraint.");
455
2635827
  AssertArgument(c->isEquality() || c->isUpperBound(),
456
                 "Constraint type must be set to an equality or UpperBound.");
457
458
2635827
  ArithVar x = c->getVariable();
459
2635827
  Debug("partial_model") << "setUpperBoundConstraint(" << x << ":" << c << ")" << endl;
460
2635827
  Assert(inMaps(x));
461
2635827
  Assert(lessThanUpperBound(x, c->getValue()));
462
463
2635827
  invalidateDelta();
464
2635827
  VarInfo& vi = d_vars.get(x);
465
2635827
  pushUpperBound(vi);
466
2635827
  BoundsInfo prev;
467
2635827
  if(vi.setUpperBound(c, prev)){
468
2481046
    addToBoundQueue(x, prev);
469
  }
470
2635827
}
471
472
9809326
int ArithVariables::cmpToLowerBound(ArithVar x, const DeltaRational& c) const{
473
9809326
  if(!hasLowerBound(x)){
474
    // l = -\intfy
475
    // ? c < -\infty |-  _|_
476
6373126
    return 1;
477
  }else{
478
3436200
    return c.cmp(getLowerBound(x));
479
  }
480
}
481
482
9408223
int ArithVariables::cmpToUpperBound(ArithVar x, const DeltaRational& c) const{
483
9408223
  if(!hasUpperBound(x)){
484
    //u = \intfy
485
    // ? c > \infty |-  _|_
486
6621477
    return -1;
487
  }else{
488
2786746
    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
2775025
bool ArithVariables::hasEitherBound(ArithVar x) const{
508
2775025
  return hasLowerBound(x) || hasUpperBound(x);
509
}
510
511
1871294
bool ArithVariables::strictlyBelowUpperBound(ArithVar x) const{
512
1871294
  return d_vars[x].d_cmpAssignmentUB < 0;
513
}
514
515
3375840
bool ArithVariables::strictlyAboveLowerBound(ArithVar x) const{
516
3375840
  return d_vars[x].d_cmpAssignmentLB > 0;
517
}
518
519
21918359
bool ArithVariables::assignmentIsConsistent(ArithVar x) const{
520
  return
521
42618124
    d_vars[x].d_cmpAssignmentLB >= 0 &&
522
42618124
    d_vars[x].d_cmpAssignmentUB <= 0;
523
}
524
525
526
2690460
void ArithVariables::clearSafeAssignments(bool revert){
527
528
2690460
  if(revert && !d_safeAssignment.empty()){
529
    invalidateDelta();
530
  }
531
532
11825718
  while(!d_safeAssignment.empty()){
533
4567629
    ArithVar atBack = d_safeAssignment.back();
534
4567629
    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
4567629
    d_safeAssignment.pop_back();
542
  }
543
2690460
}
544
545
75185
void ArithVariables::revertAssignmentChanges(){
546
75185
  clearSafeAssignments(true);
547
75185
}
548
2615275
void ArithVariables::commitAssignmentChanges(){
549
2615275
  clearSafeAssignments(false);
550
2615275
}
551
552
950448
bool ArithVariables::lowerBoundIsZero(ArithVar x){
553
950448
  return hasLowerBound(x) && getLowerBound(x).sgn() == 0;
554
}
555
556
951745
bool ArithVariables::upperBoundIsZero(ArithVar x){
557
951745
  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
2635827
void ArithVariables::pushUpperBound(VarInfo& vi){
596
2635827
  ++vi.d_pushCount;
597
7926942
  d_ubRevertHistory.push_back(make_pair(vi.d_var, vi.d_ub));
598
2635827
}
599
2655288
void ArithVariables::pushLowerBound(VarInfo& vi){
600
2655288
  ++vi.d_pushCount;
601
2655288
  d_lbRevertHistory.push_back(make_pair(vi.d_var, vi.d_lb));
602
2655288
}
603
604
2635827
void ArithVariables::popUpperBound(AVCPair* c){
605
2635827
  ArithVar x = c->first;
606
2635827
  VarInfo& vi = d_vars.get(x);
607
2635827
  BoundsInfo prev;
608
2635827
  if(vi.setUpperBound(c->second, prev)){
609
2478913
    addToBoundQueue(x, prev);
610
  }
611
2635827
  --vi.d_pushCount;
612
2635827
}
613
614
2655288
void ArithVariables::popLowerBound(AVCPair* c){
615
2655288
  ArithVar x = c->first;
616
2655288
  VarInfo& vi = d_vars.get(x);
617
2655288
  BoundsInfo prev;
618
2655288
  if(vi.setLowerBound(c->second, prev)){
619
2317843
    addToBoundQueue(x, prev);
620
  }
621
2655288
  --vi.d_pushCount;
622
2655288
}
623
624
10710373
void ArithVariables::addToBoundQueue(ArithVar v, const BoundsInfo& prev){
625
10710373
  if(d_enqueueingBoundCounts && !d_boundsQueue.isKey(v)){
626
6289150
    d_boundsQueue.set(v, prev);
627
  }
628
10710373
}
629
630
501479
BoundsInfo ArithVariables::selectBoundsInfo(ArithVar v, bool old) const {
631
501479
  if(old && d_boundsQueue.isKey(v)){
632
16270
    return d_boundsQueue[v];
633
  }else{
634
485209
    return boundsInfo(v);
635
  }
636
}
637
638
22210895
bool ArithVariables::boundsQueueEmpty() const {
639
22210895
  return d_boundsQueue.empty();
640
}
641
642
10132564
void ArithVariables::processBoundsQueue(BoundUpdateCallback& changed){
643
16320423
  while(!boundsQueueEmpty()){
644
6187859
    ArithVar v = d_boundsQueue.back();
645
6187859
    BoundsInfo prev = d_boundsQueue[v];
646
6187859
    d_boundsQueue.pop_back();
647
6187859
    BoundsInfo curr = boundsInfo(v);
648
6187859
    if(prev != curr){
649
5964629
      changed(v, prev);
650
    }
651
  }
652
3944705
}
653
654
14352415
void ArithVariables::invalidateDelta() {
655
14352415
  d_deltaIsSafe = false;
656
14352415
}
657
658
61162
void ArithVariables::setDelta(const Rational& d){
659
61162
  d_delta = d;
660
61162
  d_deltaIsSafe = true;
661
61162
}
662
663
2523901
void ArithVariables::startQueueingBoundCounts(){
664
2523901
  d_enqueueingBoundCounts = true;
665
2523901
}
666
2523901
void ArithVariables::stopQueueingBoundCounts(){
667
2523901
  d_enqueueingBoundCounts = false;
668
2523901
}
669
670
356630362
bool ArithVariables::inMaps(ArithVar x) const{
671
356630362
  return x < getNumberOfVariables();
672
}
673
674
15275
ArithVariables::LowerBoundCleanUp::LowerBoundCleanUp(ArithVariables* pm)
675
15275
  : d_pm(pm)
676
15275
{}
677
2655288
void ArithVariables::LowerBoundCleanUp::operator()(AVCPair* p){
678
2655288
  d_pm->popLowerBound(p);
679
2655288
}
680
681
15275
ArithVariables::UpperBoundCleanUp::UpperBoundCleanUp(ArithVariables* pm)
682
15275
  : d_pm(pm)
683
15275
{}
684
2635827
void ArithVariables::UpperBoundCleanUp::operator()(AVCPair* p){
685
2635827
  d_pm->popUpperBound(p);
686
2635827
}
687
688
}  // namespace arith
689
}  // namespace theory
690
31140
}  // namespace cvc5