GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/partial_model.cpp Lines: 320 406 78.8 %
Date: 2021-03-22 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
8995
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
17990
   d_lbRevertHistory(c, true, LowerBoundCleanUp(this)),
39
17990
   d_ubRevertHistory(c, true, UpperBoundCleanUp(this)),
40
   d_deltaIsSafe(false),
41
   d_delta(-1,1),
42
44975
   d_deltaComputingFunc(deltaComputingFunc)
43
8995
{ }
44
45
243231438
ArithVar ArithVariables::getNumberOfVariables() const {
46
243231438
  return d_numberOfVariables;
47
}
48
49
50
13017160
bool ArithVariables::hasArithVar(TNode x) const {
51
13017160
  return d_nodeToArithVarMap.find(x) != d_nodeToArithVarMap.end();
52
}
53
54
4858429
bool ArithVariables::hasNode(ArithVar a) const {
55
4858429
  return d_vars.isKey(a);
56
}
57
58
3829591
ArithVar ArithVariables::asArithVar(TNode x) const{
59
3829591
  Assert(hasArithVar(x));
60
3829591
  Assert((d_nodeToArithVarMap.find(x))->second <= ARITHVAR_SENTINEL);
61
3829591
  return (d_nodeToArithVarMap.find(x))->second;
62
}
63
64
3082813
Node ArithVariables::asNode(ArithVar a) const{
65
3082813
  Assert(hasNode(a));
66
3082813
  return d_vars[a].d_node;
67
}
68
69
ArithVariables::var_iterator::var_iterator()
70
  : d_vars(NULL)
71
  , d_wrapped()
72
{}
73
74
3607308
ArithVariables::var_iterator::var_iterator(const VarInfoVec* vars, VarInfoVec::const_iterator ci)
75
3607308
  : d_vars(vars), d_wrapped(ci)
76
{
77
3607308
  nextInitialized();
78
3607308
}
79
80
10816222
ArithVariables::var_iterator& ArithVariables::var_iterator::operator++(){
81
10816222
  ++d_wrapped;
82
10816222
  nextInitialized();
83
10816222
  return *this;
84
}
85
bool ArithVariables::var_iterator::operator==(const ArithVariables::var_iterator& other) const{
86
  return d_wrapped == other.d_wrapped;
87
}
88
12619876
bool ArithVariables::var_iterator::operator!=(const ArithVariables::var_iterator& other) const{
89
12619876
  return d_wrapped != other.d_wrapped;
90
}
91
10816222
ArithVar ArithVariables::var_iterator::operator*() const{
92
10816222
  return *d_wrapped;
93
}
94
95
14423530
void ArithVariables::var_iterator::nextInitialized(){
96
14423530
  VarInfoVec::const_iterator end = d_vars->end();
97
26994593
  while(d_wrapped != end &&
98
12571063
        !((*d_vars)[*d_wrapped].initialized())){
99
    ++d_wrapped;
100
  }
101
14423530
}
102
103
1803654
ArithVariables::var_iterator ArithVariables::var_begin() const {
104
1803654
  return var_iterator(&d_vars, d_vars.begin());
105
}
106
107
1803654
ArithVariables::var_iterator ArithVariables::var_end() const {
108
1803654
  return var_iterator(&d_vars, d_vars.end());
109
}
110
699011224
bool ArithVariables::isInteger(ArithVar x) const {
111
699011224
  return d_vars[x].d_type >= ArithType::Integer;
112
}
113
114
/** Is the assignment to x integral? */
115
204530074
bool ArithVariables::integralAssignment(ArithVar x) const {
116
204530074
  return getAssignment(x).isIntegral();
117
}
118
519161050
bool ArithVariables::isAuxiliary(ArithVar x) const {
119
519161050
  return d_vars[x].d_auxiliary;
120
}
121
122
680263101
bool ArithVariables::isIntegerInput(ArithVar x) const {
123
680263101
  return isInteger(x) && !isAuxiliary(x);
124
}
125
126
292736
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
292736
      d_auxiliary(false) {}
137
138
26774176
bool ArithVariables::VarInfo::initialized() const {
139
26774176
  return d_var != ARITHVAR_SENTINEL;
140
}
141
142
146368
void ArithVariables::VarInfo::initialize(ArithVar v, Node n, bool aux){
143
146368
  Assert(!initialized());
144
146368
  Assert(d_lb == NullConstraint);
145
146368
  Assert(d_ub == NullConstraint);
146
146368
  Assert(d_cmpAssignmentLB > 0);
147
146368
  Assert(d_cmpAssignmentUB < 0);
148
146368
  d_var = v;
149
146368
  d_node = n;
150
146368
  d_auxiliary = aux;
151
152
146368
  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
165058
    Polynomial p = Polynomial::parsePolynomial(n);
157
82529
    d_type = p.isIntegral() ? ArithType::Integer : ArithType::Real;
158
  }else{
159
63839
    d_type = n.getType().isInteger() ? ArithType::Integer : ArithType::Real;
160
  }
161
162
146368
  Assert(initialized());
163
146368
}
164
165
void ArithVariables::VarInfo::uninitialize(){
166
  d_var = ARITHVAR_SENTINEL;
167
  d_node = Node::null();
168
}
169
170
5860999
bool ArithVariables::VarInfo::setAssignment(const DeltaRational& a, BoundsInfo& prev){
171
5860999
  Assert(initialized());
172
5860999
  d_assignment = a;
173
7104006
  int cmpUB = (d_ub == NullConstraint) ? -1 :
174
7104006
    d_assignment.cmp(d_ub->getValue());
175
176
7453391
  int cmpLB = (d_lb == NullConstraint) ? 1 :
177
7453391
    d_assignment.cmp(d_lb->getValue());
178
179
6475558
  bool lbChanged = cmpLB != d_cmpAssignmentLB &&
180
304810
    (cmpLB == 0 || d_cmpAssignmentLB == 0);
181
6360757
  bool ubChanged = cmpUB != d_cmpAssignmentUB &&
182
217170
    (cmpUB == 0 || d_cmpAssignmentUB == 0);
183
184
5860999
  if(lbChanged || ubChanged){
185
872389
    prev = boundsInfo();
186
  }
187
188
5860999
  d_cmpAssignmentUB = cmpUB;
189
5860999
  d_cmpAssignmentLB = cmpLB;
190
5860999
  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
3988278
bool ArithVariables::VarInfo::setUpperBound(ConstraintP ub, BoundsInfo& prev){
212
3988278
  Assert(initialized());
213
3988278
  bool wasNull = d_ub == NullConstraint;
214
3988278
  bool isNull = ub == NullConstraint;
215
216
3988278
  int cmpUB = isNull ? -1 : d_assignment.cmp(ub->getValue());
217
8227325
  bool ubChanged = (wasNull != isNull) ||
218
707909
    (cmpUB != d_cmpAssignmentUB && (cmpUB == 0 || d_cmpAssignmentUB == 0));
219
3988278
  if(ubChanged){
220
3789493
    prev = boundsInfo();
221
  }
222
3988278
  d_ub = ub;
223
3988278
  d_cmpAssignmentUB = cmpUB;
224
3988278
  return ubChanged;
225
}
226
227
4061100
bool ArithVariables::VarInfo::setLowerBound(ConstraintP lb, BoundsInfo& prev){
228
4061100
  Assert(initialized());
229
4061100
  bool wasNull = d_lb == NullConstraint;
230
4061100
  bool isNull = lb == NullConstraint;
231
232
4061100
  int cmpLB = isNull ? 1 : d_assignment.cmp(lb->getValue());
233
234
8471686
  bool lbChanged = (wasNull != isNull) ||
235
1184475
    (cmpLB != d_cmpAssignmentLB && (cmpLB == 0 || d_cmpAssignmentLB == 0));
236
4061100
  if(lbChanged){
237
3583174
    prev = boundsInfo();
238
  }
239
4061100
  d_lb = lb;
240
4061100
  d_cmpAssignmentLB = cmpLB;
241
4061100
  return lbChanged;
242
}
243
244
79669867
BoundCounts ArithVariables::VarInfo::atBoundCounts() const {
245
79669867
  uint32_t lbIndc = (d_cmpAssignmentLB == 0) ? 1 : 0;
246
79669867
  uint32_t ubIndc = (d_cmpAssignmentUB == 0) ? 1 : 0;
247
79669867
  return BoundCounts(lbIndc, ubIndc);
248
}
249
250
71728113
BoundCounts ArithVariables::VarInfo::hasBoundCounts() const {
251
71728113
  uint32_t lbIndc = (d_lb != NullConstraint) ? 1 : 0;
252
71728113
  uint32_t ubIndc = (d_ub != NullConstraint) ? 1 : 0;
253
71728113
  return BoundCounts(lbIndc, ubIndc);
254
}
255
256
71728113
BoundsInfo ArithVariables::VarInfo::boundsInfo() const{
257
71728113
  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
146368
void ArithVariables::attemptToReclaimReleased(){
269
146368
  size_t readPos = 0, writePos = 0, N = d_released.size();
270
146368
  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
146368
  d_released.resize(writePos);
280
146368
}
281
282
146368
ArithVar ArithVariables::allocateVariable(){
283
146368
  if(d_pool.empty()){
284
146368
    attemptToReclaimReleased();
285
  }
286
146368
  bool reclaim = !d_pool.empty();
287
288
  ArithVar varX;
289
146368
  if(reclaim){
290
    varX = d_pool.back();
291
    d_pool.pop_back();
292
  }else{
293
146368
    varX = d_numberOfVariables;
294
146368
    ++d_numberOfVariables;
295
  }
296
146368
  d_vars.set(varX, VarInfo());
297
146368
  return varX;
298
}
299
300
301
22555
const Rational& ArithVariables::getDelta(){
302
22555
  if(!d_deltaIsSafe){
303
31258
    Rational nextDelta = d_deltaComputingFunc();
304
15629
    setDelta(nextDelta);
305
  }
306
22555
  Assert(d_deltaIsSafe);
307
22555
  return d_delta;
308
}
309
310
51228
bool ArithVariables::boundsAreEqual(ArithVar x) const{
311
51228
  if(hasLowerBound(x) && hasUpperBound(x)){
312
43430
    return getUpperBound(x) == getLowerBound(x);
313
  }else{
314
7798
    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
5778470
void ArithVariables::setAssignment(ArithVar x, const DeltaRational& r){
334
11556940
  Debug("partial_model") << "pm: updating the assignment to" << x
335
5778470
                         << " now " << r <<endl;
336
5778470
  VarInfo& vi = d_vars.get(x);
337
5778470
  if(!d_safeAssignment.isKey(x)){
338
3296723
    d_safeAssignment.set(x, vi.d_assignment);
339
  }
340
5778470
  invalidateDelta();
341
342
5778470
  BoundsInfo prev;
343
5778470
  if(vi.setAssignment(r, prev)){
344
872389
    addToBoundQueue(x, prev);
345
  }
346
5778470
}
347
348
82529
void ArithVariables::setAssignment(ArithVar x, const DeltaRational& safe, const DeltaRational& r){
349
165058
  Debug("partial_model") << "pm: updating the assignment to" << x
350
82529
                         << " now " << r <<endl;
351
82529
  if(safe == r){
352
82098
    if(d_safeAssignment.isKey(x)){
353
      d_safeAssignment.remove(x);
354
    }
355
  }else{
356
431
    d_safeAssignment.set(x, safe);
357
  }
358
359
82529
  invalidateDelta();
360
82529
  VarInfo& vi = d_vars.get(x);
361
82529
  BoundsInfo prev;
362
82529
  if(vi.setAssignment(r, prev)){
363
    addToBoundQueue(x, prev);
364
  }
365
82529
}
366
367
146368
void ArithVariables::initialize(ArithVar x, Node n, bool aux){
368
146368
  VarInfo& vi = d_vars.get(x);
369
146368
  vi.initialize(x, n, aux);
370
146368
  d_nodeToArithVarMap[n] = x;
371
146368
}
372
373
146368
ArithVar ArithVariables::allocate(Node n, bool aux){
374
146368
  ArithVar v = allocateVariable();
375
146368
  initialize(v, n, aux);
376
146368
  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
4657580
const DeltaRational& ArithVariables::getUpperBound(ArithVar x) const {
397
4657580
  Assert(inMaps(x));
398
4657580
  Assert(hasUpperBound(x));
399
400
4657580
  return getUpperBoundConstraint(x)->getValue();
401
}
402
403
5020214
const DeltaRational& ArithVariables::getLowerBound(ArithVar x) const {
404
5020214
  Assert(inMaps(x));
405
5020214
  Assert(hasLowerBound(x));
406
407
5020214
  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
597042
const DeltaRational& ArithVariables::getAssignment(ArithVar x, bool safe) const{
420
597042
  Assert(inMaps(x));
421
597042
  if(safe && d_safeAssignment.isKey(x)){
422
487
    return d_safeAssignment[x];
423
  }else{
424
596555
    return d_vars[x].d_assignment;
425
  }
426
}
427
428
224930934
const DeltaRational& ArithVariables::getAssignment(ArithVar x) const{
429
224930934
  Assert(inMaps(x));
430
224930934
  return d_vars[x].d_assignment;
431
}
432
433
434
2030550
void ArithVariables::setLowerBoundConstraint(ConstraintP c){
435
2030550
  AssertArgument(c != NullConstraint, "Cannot set a lower bound to NullConstraint.");
436
2030550
  AssertArgument(c->isEquality() || c->isLowerBound(),
437
                 "Constraint type must be set to an equality or UpperBound.");
438
2030550
  ArithVar x = c->getVariable();
439
2030550
  Debug("partial_model") << "setLowerBoundConstraint(" << x << ":" << c << ")" << endl;
440
2030550
  Assert(inMaps(x));
441
2030550
  Assert(greaterThanLowerBound(x, c->getValue()));
442
443
2030550
  invalidateDelta();
444
2030550
  VarInfo& vi = d_vars.get(x);
445
2030550
  pushLowerBound(vi);
446
2030550
  BoundsInfo prev;
447
2030550
  if(vi.setLowerBound(c, prev)){
448
1794423
    addToBoundQueue(x, prev);
449
  }
450
2030550
}
451
452
1994139
void ArithVariables::setUpperBoundConstraint(ConstraintP c){
453
1994139
  AssertArgument(c != NullConstraint, "Cannot set a upper bound to NullConstraint.");
454
1994139
  AssertArgument(c->isEquality() || c->isUpperBound(),
455
                 "Constraint type must be set to an equality or UpperBound.");
456
457
1994139
  ArithVar x = c->getVariable();
458
1994139
  Debug("partial_model") << "setUpperBoundConstraint(" << x << ":" << c << ")" << endl;
459
1994139
  Assert(inMaps(x));
460
1994139
  Assert(lessThanUpperBound(x, c->getValue()));
461
462
1994139
  invalidateDelta();
463
1994139
  VarInfo& vi = d_vars.get(x);
464
1994139
  pushUpperBound(vi);
465
1994139
  BoundsInfo prev;
466
1994139
  if(vi.setUpperBound(c, prev)){
467
1895293
    addToBoundQueue(x, prev);
468
  }
469
1994139
}
470
471
7367407
int ArithVariables::cmpToLowerBound(ArithVar x, const DeltaRational& c) const{
472
7367407
  if(!hasLowerBound(x)){
473
    // l = -\intfy
474
    // ? c < -\infty |-  _|_
475
4679064
    return 1;
476
  }else{
477
2688343
    return c.cmp(getLowerBound(x));
478
  }
479
}
480
481
7015440
int ArithVariables::cmpToUpperBound(ArithVar x, const DeltaRational& c) const{
482
7015440
  if(!hasUpperBound(x)){
483
    //u = \intfy
484
    // ? c > \infty |-  _|_
485
4768692
    return -1;
486
  }else{
487
2246748
    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
2508165
bool ArithVariables::hasEitherBound(ArithVar x) const{
507
2508165
  return hasLowerBound(x) || hasUpperBound(x);
508
}
509
510
1607725
bool ArithVariables::strictlyBelowUpperBound(ArithVar x) const{
511
1607725
  return d_vars[x].d_cmpAssignmentUB < 0;
512
}
513
514
3043058
bool ArithVariables::strictlyAboveLowerBound(ArithVar x) const{
515
3043058
  return d_vars[x].d_cmpAssignmentLB > 0;
516
}
517
518
15250796
bool ArithVariables::assignmentIsConsistent(ArithVar x) const{
519
  return
520
29583160
    d_vars[x].d_cmpAssignmentLB >= 0 &&
521
29583160
    d_vars[x].d_cmpAssignmentUB <= 0;
522
}
523
524
525
1907188
void ArithVariables::clearSafeAssignments(bool revert){
526
527
1907188
  if(revert && !d_safeAssignment.empty()){
528
    invalidateDelta();
529
  }
530
531
8501496
  while(!d_safeAssignment.empty()){
532
3297154
    ArithVar atBack = d_safeAssignment.back();
533
3297154
    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
3297154
    d_safeAssignment.pop_back();
541
  }
542
1907188
}
543
544
64107
void ArithVariables::revertAssignmentChanges(){
545
64107
  clearSafeAssignments(true);
546
64107
}
547
1843081
void ArithVariables::commitAssignmentChanges(){
548
1843081
  clearSafeAssignments(false);
549
1843081
}
550
551
847207
bool ArithVariables::lowerBoundIsZero(ArithVar x){
552
847207
  return hasLowerBound(x) && getLowerBound(x).sgn() == 0;
553
}
554
555
891398
bool ArithVariables::upperBoundIsZero(ArithVar x){
556
891398
  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
1994139
void ArithVariables::pushUpperBound(VarInfo& vi){
595
1994139
  ++vi.d_pushCount;
596
6018828
  d_ubRevertHistory.push_back(make_pair(vi.d_var, vi.d_ub));
597
1994139
}
598
2030550
void ArithVariables::pushLowerBound(VarInfo& vi){
599
2030550
  ++vi.d_pushCount;
600
2030550
  d_lbRevertHistory.push_back(make_pair(vi.d_var, vi.d_lb));
601
2030550
}
602
603
1994139
void ArithVariables::popUpperBound(AVCPair* c){
604
1994139
  ArithVar x = c->first;
605
1994139
  VarInfo& vi = d_vars.get(x);
606
1994139
  BoundsInfo prev;
607
1994139
  if(vi.setUpperBound(c->second, prev)){
608
1894200
    addToBoundQueue(x, prev);
609
  }
610
1994139
  --vi.d_pushCount;
611
1994139
}
612
613
2030550
void ArithVariables::popLowerBound(AVCPair* c){
614
2030550
  ArithVar x = c->first;
615
2030550
  VarInfo& vi = d_vars.get(x);
616
2030550
  BoundsInfo prev;
617
2030550
  if(vi.setLowerBound(c->second, prev)){
618
1788751
    addToBoundQueue(x, prev);
619
  }
620
2030550
  --vi.d_pushCount;
621
2030550
}
622
623
8245056
void ArithVariables::addToBoundQueue(ArithVar v, const BoundsInfo& prev){
624
8245056
  if(d_enqueueingBoundCounts && !d_boundsQueue.isKey(v)){
625
4770891
    d_boundsQueue.set(v, prev);
626
  }
627
8245056
}
628
629
381050
BoundsInfo ArithVariables::selectBoundsInfo(ArithVar v, bool old) const {
630
381050
  if(old && d_boundsQueue.isKey(v)){
631
10892
    return d_boundsQueue[v];
632
  }else{
633
370158
    return boundsInfo(v);
634
  }
635
}
636
637
16115988
bool ArithVariables::boundsQueueEmpty() const {
638
16115988
  return d_boundsQueue.empty();
639
}
640
641
7498314
void ArithVariables::processBoundsQueue(BoundUpdateCallback& changed){
642
12185070
  while(!boundsQueueEmpty()){
643
4686756
    ArithVar v = d_boundsQueue.back();
644
4686756
    BoundsInfo prev = d_boundsQueue[v];
645
4686756
    d_boundsQueue.pop_back();
646
4686756
    BoundsInfo curr = boundsInfo(v);
647
4686756
    if(prev != curr){
648
4493210
      changed(v, prev);
649
    }
650
  }
651
2811558
}
652
653
10178556
void ArithVariables::invalidateDelta() {
654
10178556
  d_deltaIsSafe = false;
655
10178556
}
656
657
15629
void ArithVariables::setDelta(const Rational& d){
658
15629
  d_delta = d;
659
15629
  d_deltaIsSafe = true;
660
15629
}
661
662
1769324
void ArithVariables::startQueueingBoundCounts(){
663
1769324
  d_enqueueingBoundCounts = true;
664
1769324
}
665
1769324
void ArithVariables::stopQueueingBoundCounts(){
666
1769324
  d_enqueueingBoundCounts = false;
667
1769324
}
668
669
239230459
bool ArithVariables::inMaps(ArithVar x) const{
670
239230459
  return x < getNumberOfVariables();
671
}
672
673
8995
ArithVariables::LowerBoundCleanUp::LowerBoundCleanUp(ArithVariables* pm)
674
8995
  : d_pm(pm)
675
8995
{}
676
2030550
void ArithVariables::LowerBoundCleanUp::operator()(AVCPair* p){
677
2030550
  d_pm->popLowerBound(p);
678
2030550
}
679
680
8995
ArithVariables::UpperBoundCleanUp::UpperBoundCleanUp(ArithVariables* pm)
681
8995
  : d_pm(pm)
682
8995
{}
683
1994139
void ArithVariables::UpperBoundCleanUp::operator()(AVCPair* p){
684
1994139
  d_pm->popUpperBound(p);
685
1994139
}
686
687
}/* CVC4::theory::arith namespace */
688
}/* CVC4::theory namespace */
689
26676
}/* CVC4 namespace */