src/theory/arith/partial_model.cpp

   1 /*********************                                                        */
   2 /*! \file partial_model.cpp
   3  ** \verbatim
   4  ** Original author: Tim King
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): Morgan Deters
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2013  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** 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
  19 #include "theory/arith/partial_model.h"
  20 #include "util/output.h"
  21 #include "theory/arith/constraint.h"
  22 #include "theory/arith/normal_form.h"
  23
  24 using namespace std;
  25
  26 namespace CVC4 {
  27 namespace theory {
  28 namespace arith {
  29
  30 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_releasedIterator(d_released.begin()),
  37    d_nodeToArithVarMap(),
  38    d_boundsQueue(),
  39    d_enqueueingBoundCounts(true),
  40    d_lbRevertHistory(c, true, LowerBoundCleanUp(this)),
  41    d_ubRevertHistory(c, true, UpperBoundCleanUp(this)),
  42    d_deltaIsSafe(false),
  43    d_delta(-1,1),
  44    d_deltaComputingFunc(deltaComputingFunc)
  45 { }
  46
  47 ArithVariables::VarInfo::VarInfo()
  48   : d_var(ARITHVAR_SENTINEL),
  49     d_assignment(0),
  50     d_lb(NullConstraint),
  51     d_ub(NullConstraint),
  52     d_cmpAssignmentLB(1),
  53     d_cmpAssignmentUB(-1),
  54     d_pushCount(0),
  55     d_node(Node::null()),
  56     d_slack(false)
  57 { }
  58
  59 bool ArithVariables::VarInfo::initialized() const {
  60   return d_var != ARITHVAR_SENTINEL;
  61 }
  62
  63 void ArithVariables::VarInfo::initialize(ArithVar v, Node n, bool slack){
  64   Assert(!initialized());
  65   Assert(d_lb == NullConstraint);
  66   Assert(d_ub == NullConstraint);
  67   Assert(d_cmpAssignmentLB > 0);
  68   Assert(d_cmpAssignmentUB < 0);
  69   d_var = v;
  70   d_node = n;
  71   d_slack = slack;
  72
  73   if(d_slack){
  74     //The type computation is not quite accurate for Rationals that are
  75     //integral.
  76     //We'll use the isIntegral check from the polynomial package instead.
  77     Polynomial p = Polynomial::parsePolynomial(n);
  78     d_type = p.isIntegral() ? ATInteger : ATReal;
  79   }else{
  80     d_type = nodeToArithType(n);
  81   }
  82
  83   Assert(initialized());
  84 }
  85 void ArithVariables::VarInfo::uninitialize(){
  86   d_var = ARITHVAR_SENTINEL;
  87   d_node = Node::null();
  88 }
  89
  90 bool ArithVariables::VarInfo::setAssignment(const DeltaRational& a, BoundsInfo& prev){
  91   Assert(initialized());
  92   d_assignment = a;
  93   int cmpUB = (d_ub == NullConstraint) ? -1 :
  94     d_assignment.cmp(d_ub->getValue());
  95
  96   int cmpLB = (d_lb == NullConstraint) ? 1 :
  97     d_assignment.cmp(d_lb->getValue());
  98
  99   bool lbChanged = cmpLB != d_cmpAssignmentLB &&
 100     (cmpLB == 0 || d_cmpAssignmentLB == 0);
 101   bool ubChanged = cmpUB != d_cmpAssignmentUB &&
 102     (cmpUB == 0 || d_cmpAssignmentUB == 0);
 103
 104   if(lbChanged || ubChanged){
 105     prev = boundsInfo();
 106   }
 107
 108   d_cmpAssignmentUB = cmpUB;
 109   d_cmpAssignmentLB = cmpLB;
 110   return lbChanged || ubChanged;
 111 }
 112
 113 void ArithVariables::releaseArithVar(ArithVar v){
 114   VarInfo& vi = d_vars.get(v);
 115   vi.uninitialize();
 116
 117   if(d_safeAssignment.isKey(v)){
 118     d_safeAssignment.remove(v);
 119   }
 120   if(vi.canBeReclaimed()){
 121     d_pool.push_back(v);
 122   }else{
 123     d_released.push_back(v);
 124   }
 125 }
 126
 127 bool ArithVariables::VarInfo::setUpperBound(Constraint ub, BoundsInfo& prev){
 128   Assert(initialized());
 129   bool wasNull = d_ub == NullConstraint;
 130   bool isNull = ub == NullConstraint;
 131
 132   int cmpUB = isNull ? -1 : d_assignment.cmp(ub->getValue());
 133   bool ubChanged = (wasNull != isNull) ||
 134     (cmpUB != d_cmpAssignmentUB && (cmpUB == 0 || d_cmpAssignmentUB == 0));
 135   if(ubChanged){
 136     prev = boundsInfo();
 137   }
 138   d_ub = ub;
 139   d_cmpAssignmentUB = cmpUB;
 140   return ubChanged;
 141 }
 142
 143 bool ArithVariables::VarInfo::setLowerBound(Constraint lb, BoundsInfo& prev){
 144   Assert(initialized());
 145   bool wasNull = d_lb == NullConstraint;
 146   bool isNull = lb == NullConstraint;
 147
 148   int cmpLB = isNull ? 1 : d_assignment.cmp(lb->getValue());
 149
 150   bool lbChanged = (wasNull != isNull) ||
 151     (cmpLB != d_cmpAssignmentLB && (cmpLB == 0 || d_cmpAssignmentLB == 0));
 152   if(lbChanged){
 153     prev = boundsInfo();
 154   }
 155   d_lb = lb;
 156   d_cmpAssignmentLB = cmpLB;
 157   return lbChanged;
 158 }
 159
 160 BoundCounts ArithVariables::VarInfo::atBoundCounts() const {
 161   uint32_t lbIndc = (d_cmpAssignmentLB == 0) ? 1 : 0;
 162   uint32_t ubIndc = (d_cmpAssignmentUB == 0) ? 1 : 0;
 163   return BoundCounts(lbIndc, ubIndc);
 164 }
 165
 166 BoundCounts ArithVariables::VarInfo::hasBoundCounts() const {
 167   uint32_t lbIndc = (d_lb != NullConstraint) ? 1 : 0;
 168   uint32_t ubIndc = (d_ub != NullConstraint) ? 1 : 0;
 169   return BoundCounts(lbIndc, ubIndc);
 170 }
 171
 172 BoundsInfo ArithVariables::VarInfo::boundsInfo() const{
 173   return BoundsInfo(atBoundCounts(), hasBoundCounts());
 174 }
 175
 176 bool ArithVariables::VarInfo::canBeReclaimed() const{
 177   return d_pushCount == 0;
 178 }
 179
 180 void ArithVariables::attemptToReclaimReleased(){
 181   std::list<ArithVar>::iterator i_end = d_released.end();
 182   for(int iter = 0; iter < 20 && d_releasedIterator != i_end; ++d_releasedIterator){
 183     ArithVar v = *d_releasedIterator;
 184     VarInfo& vi = d_vars.get(v);
 185     if(vi.canBeReclaimed()){
 186       d_pool.push_back(v);
 187       std::list<ArithVar>::iterator curr = d_releasedIterator;
 188       ++d_releasedIterator;
 189       d_released.erase(curr);
 190     }else{
 191       ++d_releasedIterator;
 192     }
 193   }
 194   if(d_releasedIterator == i_end){
 195     d_releasedIterator = d_released.begin();
 196   }
 197 }
 198
 199 ArithVar ArithVariables::allocateVariable(){
 200   if(d_pool.empty()){
 201     attemptToReclaimReleased();
 202   }
 203   bool reclaim = !d_pool.empty();
 204
 205   ArithVar varX;
 206   if(reclaim){
 207     varX = d_pool.back();
 208     d_pool.pop_back();
 209   }else{
 210     varX = d_numberOfVariables;
 211     ++d_numberOfVariables;
 212   }
 213   d_vars.set(varX, VarInfo());
 214   return varX;
 215 }
 216
 217
 218 const Rational& ArithVariables::getDelta(){
 219   if(!d_deltaIsSafe){
 220     Rational nextDelta = d_deltaComputingFunc();
 221     setDelta(nextDelta);
 222   }
 223   Assert(d_deltaIsSafe);
 224   return d_delta;
 225 }
 226
 227 bool ArithVariables::boundsAreEqual(ArithVar x) const{
 228   if(hasLowerBound(x) && hasUpperBound(x)){
 229     return getUpperBound(x) == getLowerBound(x);
 230   }else{
 231     return false;
 232   }
 233 }
 234
 235 void ArithVariables::setAssignment(ArithVar x, const DeltaRational& r){
 236   Debug("partial_model") << "pm: updating the assignment to" << x
 237                          << " now " << r <<endl;
 238   VarInfo& vi = d_vars.get(x);
 239   if(!d_safeAssignment.isKey(x)){
 240     d_safeAssignment.set(x, vi.d_assignment);
 241   }
 242   invalidateDelta();
 243
 244   BoundsInfo prev;
 245   if(vi.setAssignment(r, prev)){
 246     addToBoundQueue(x, prev);
 247   }
 248 }
 249
 250 void ArithVariables::setAssignment(ArithVar x, const DeltaRational& safe, const DeltaRational& r){
 251   Debug("partial_model") << "pm: updating the assignment to" << x
 252                          << " now " << r <<endl;
 253   if(safe == r){
 254     if(d_safeAssignment.isKey(x)){
 255       d_safeAssignment.remove(x);
 256     }
 257   }else{
 258     d_safeAssignment.set(x, safe);
 259   }
 260
 261   invalidateDelta();
 262   VarInfo& vi = d_vars.get(x);
 263   BoundsInfo prev;
 264   if(vi.setAssignment(r, prev)){
 265     addToBoundQueue(x, prev);
 266   }
 267 }
 268
 269 void ArithVariables::initialize(ArithVar x, Node n, bool slack){
 270   VarInfo& vi = d_vars.get(x);
 271   vi.initialize(x, n, slack);
 272   d_nodeToArithVarMap[n] = x;
 273 }
 274
 275 ArithVar ArithVariables::allocate(Node n, bool slack){
 276   ArithVar v = allocateVariable();
 277   initialize(v, n, slack);
 278   return v;
 279 }
 280
 281 // void ArithVariables::initialize(ArithVar x, const DeltaRational& r){
 282 //   Assert(x == d_mapSize);
 283 //   Assert(equalSizes());
 284 //   ++d_mapSize;
 285
 286 //   // Is worth mentioning that this is not strictly necessary, but this maintains the internal invariant
 287 //   // that when d_assignment is set this gets set.
 288 //   invalidateDelta();
 289 //   d_assignment.push_back( r );
 290
 291 //   d_boundRel.push_back(BetweenBounds);
 292
 293 //   d_ubc.push_back(NullConstraint);
 294 //   d_lbc.push_back(NullConstraint);
 295 // }
 296
 297 /** Must know that the bound exists both calling this! */
 298 const DeltaRational& ArithVariables::getUpperBound(ArithVar x) const {
 299   Assert(inMaps(x));
 300   Assert(hasUpperBound(x));
 301
 302   return getUpperBoundConstraint(x)->getValue();
 303 }
 304
 305 const DeltaRational& ArithVariables::getLowerBound(ArithVar x) const {
 306   Assert(inMaps(x));
 307   Assert(hasLowerBound(x));
 308
 309   return getLowerBoundConstraint(x)->getValue();
 310 }
 311
 312 const DeltaRational& ArithVariables::getSafeAssignment(ArithVar x) const{
 313   Assert(inMaps(x));
 314   if(d_safeAssignment.isKey(x)){
 315     return d_safeAssignment[x];
 316   }else{
 317     return d_vars[x].d_assignment;
 318   }
 319 }
 320
 321 const DeltaRational& ArithVariables::getAssignment(ArithVar x, bool safe) const{
 322   Assert(inMaps(x));
 323   if(safe && d_safeAssignment.isKey(x)){
 324     return d_safeAssignment[x];
 325   }else{
 326     return d_vars[x].d_assignment;
 327   }
 328 }
 329
 330 const DeltaRational& ArithVariables::getAssignment(ArithVar x) const{
 331   Assert(inMaps(x));
 332   return d_vars[x].d_assignment;
 333 }
 334
 335
 336 void ArithVariables::setLowerBoundConstraint(Constraint c){
 337   AssertArgument(c != NullConstraint, "Cannot set a lower bound to NullConstraint.");
 338   AssertArgument(c->isEquality() || c->isLowerBound(),
 339                  "Constraint type must be set to an equality or UpperBound.");
 340   ArithVar x = c->getVariable();
 341   Debug("partial_model") << "setLowerBoundConstraint(" << x << ":" << c << ")" << endl;
 342   Assert(inMaps(x));
 343   Assert(greaterThanLowerBound(x, c->getValue()));
 344
 345   invalidateDelta();
 346   VarInfo& vi = d_vars.get(x);
 347   pushLowerBound(vi);
 348   BoundsInfo prev;
 349   if(vi.setLowerBound(c, prev)){
 350     addToBoundQueue(x, prev);
 351   }
 352 }
 353
 354 void ArithVariables::setUpperBoundConstraint(Constraint c){
 355   AssertArgument(c != NullConstraint, "Cannot set a upper bound to NullConstraint.");
 356   AssertArgument(c->isEquality() || c->isUpperBound(),
 357                  "Constraint type must be set to an equality or UpperBound.");
 358
 359   ArithVar x = c->getVariable();
 360   Debug("partial_model") << "setUpperBoundConstraint(" << x << ":" << c << ")" << endl;
 361   Assert(inMaps(x));
 362   Assert(lessThanUpperBound(x, c->getValue()));
 363
 364   invalidateDelta();
 365   VarInfo& vi = d_vars.get(x);
 366   pushUpperBound(vi);
 367   BoundsInfo prev;
 368   if(vi.setUpperBound(c, prev)){
 369     addToBoundQueue(x, prev);
 370   }
 371 }
 372
 373 int ArithVariables::cmpToLowerBound(ArithVar x, const DeltaRational& c) const{
 374   if(!hasLowerBound(x)){
 375     // l = -\intfy
 376     // ? c < -\infty |-  _|_
 377     return 1;
 378   }else{
 379     return c.cmp(getLowerBound(x));
 380   }
 381 }
 382
 383 int ArithVariables::cmpToUpperBound(ArithVar x, const DeltaRational& c) const{
 384   if(!hasUpperBound(x)){
 385     //u = \intfy
 386     // ? c > \infty |-  _|_
 387     return -1;
 388   }else{
 389     return c.cmp(getUpperBound(x));
 390   }
 391 }
 392
 393 bool ArithVariables::equalsLowerBound(ArithVar x, const DeltaRational& c){
 394   if(!hasLowerBound(x)){
 395     return false;
 396   }else{
 397     return c == getLowerBound(x);
 398   }
 399 }
 400 bool ArithVariables::equalsUpperBound(ArithVar x, const DeltaRational& c){
 401   if(!hasUpperBound(x)){
 402     return false;
 403   }else{
 404     return c == getUpperBound(x);
 405   }
 406 }
 407
 408 bool ArithVariables::hasEitherBound(ArithVar x) const{
 409   return hasLowerBound(x) || hasUpperBound(x);
 410 }
 411
 412 bool ArithVariables::strictlyBelowUpperBound(ArithVar x) const{
 413   return d_vars[x].d_cmpAssignmentUB < 0;
 414 }
 415
 416 bool ArithVariables::strictlyAboveLowerBound(ArithVar x) const{
 417   return d_vars[x].d_cmpAssignmentLB > 0;
 418 }
 419
 420 bool ArithVariables::assignmentIsConsistent(ArithVar x) const{
 421   return
 422     d_vars[x].d_cmpAssignmentLB >= 0 &&
 423     d_vars[x].d_cmpAssignmentUB <= 0;
 424 }
 425
 426
 427 void ArithVariables::clearSafeAssignments(bool revert){
 428
 429   if(revert && !d_safeAssignment.empty()){
 430     invalidateDelta();
 431   }
 432
 433   while(!d_safeAssignment.empty()){
 434     ArithVar atBack = d_safeAssignment.back();
 435     if(revert){
 436       VarInfo& vi = d_vars.get(atBack);
 437       BoundsInfo prev;
 438       if(vi.setAssignment(d_safeAssignment[atBack], prev)){
 439         addToBoundQueue(atBack, prev);
 440       }
 441     }
 442     d_safeAssignment.pop_back();
 443   }
 444 }
 445
 446 void ArithVariables::revertAssignmentChanges(){
 447   clearSafeAssignments(true);
 448 }
 449 void ArithVariables::commitAssignmentChanges(){
 450   clearSafeAssignments(false);
 451 }
 452
 453 void ArithVariables::printEntireModel(std::ostream& out) const{
 454   out << "---Printing Model ---" << std::endl;
 455   for(var_iterator i = var_begin(), iend = var_end(); i != iend; ++i){
 456     printModel(*i, out);
 457   }
 458   out << "---Done Model ---" << std::endl;
 459 }
 460
 461 void ArithVariables::printModel(ArithVar x, std::ostream& out) const{
 462   out << "model" << x << ": "
 463       << asNode(x) << " "
 464       << getAssignment(x) << " ";
 465   if(!hasLowerBound(x)){
 466     out << "no lb ";
 467   }else{
 468     out << getLowerBound(x) << " ";
 469     out << getLowerBoundConstraint(x) << " ";
 470   }
 471   if(!hasUpperBound(x)){
 472     out << "no ub ";
 473   }else{
 474     out << getUpperBound(x) << " ";
 475     out << getUpperBoundConstraint(x) << " ";
 476   }
 477   out << endl;
 478 }
 479
 480 void ArithVariables::printModel(ArithVar x) const{
 481   printModel(x,  Debug("model"));
 482 }
 483
 484 void ArithVariables::pushUpperBound(VarInfo& vi){
 485   ++vi.d_pushCount;
 486   d_ubRevertHistory.push_back(make_pair(vi.d_var, vi.d_ub));
 487 }
 488 void ArithVariables::pushLowerBound(VarInfo& vi){
 489   ++vi.d_pushCount;
 490   d_lbRevertHistory.push_back(make_pair(vi.d_var, vi.d_lb));
 491 }
 492
 493 void ArithVariables::popUpperBound(AVCPair* c){
 494   ArithVar x = c->first;
 495   VarInfo& vi = d_vars.get(x);
 496   BoundsInfo prev;
 497   if(vi.setUpperBound(c->second, prev)){
 498     addToBoundQueue(x, prev);
 499   }
 500   --vi.d_pushCount;
 501 }
 502
 503 void ArithVariables::popLowerBound(AVCPair* c){
 504   ArithVar x = c->first;
 505   VarInfo& vi = d_vars.get(x);
 506   BoundsInfo prev;
 507   if(vi.setLowerBound(c->second, prev)){
 508     addToBoundQueue(x, prev);
 509   }
 510   --vi.d_pushCount;
 511 }
 512
 513 void ArithVariables::addToBoundQueue(ArithVar v, const BoundsInfo& prev){
 514   if(d_enqueueingBoundCounts && !d_boundsQueue.isKey(v)){
 515     d_boundsQueue.set(v, prev);
 516   }
 517 }
 518
 519 BoundsInfo ArithVariables::selectBoundsInfo(ArithVar v, bool old) const {
 520   if(old && d_boundsQueue.isKey(v)){
 521     return d_boundsQueue[v];
 522   }else{
 523     return boundsInfo(v);
 524   }
 525 }
 526
 527 bool ArithVariables::boundsQueueEmpty() const {
 528   return d_boundsQueue.empty();
 529 }
 530
 531 void ArithVariables::processBoundsQueue(BoundUpdateCallback& changed){
 532   while(!boundsQueueEmpty()){
 533     ArithVar v = d_boundsQueue.back();
 534     BoundsInfo prev = d_boundsQueue[v];
 535     d_boundsQueue.pop_back();
 536     BoundsInfo curr = boundsInfo(v);
 537     if(prev != curr){
 538       changed(v, prev);
 539     }
 540   }
 541 }
 542
 543 void ArithVariables::LowerBoundCleanUp::operator()(AVCPair* p){
 544   d_pm->popLowerBound(p);
 545 }
 546
 547 void ArithVariables::UpperBoundCleanUp::operator()(AVCPair* p){
 548   d_pm->popUpperBound(p);
 549 }
 550
 551 }/* CVC4::theory::arith namespace */
 552 }/* CVC4::theory namespace */
 553 }/* CVC4 namespace */