src/theory/arith/partial_model.cpp

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