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

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