src/theory/arith/bound_counts.h

   1 /*********************                                                        */
   2 /*! \file bound_counts.h
   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 #include "cvc4_private.h"
  19 #pragma once
  20
  21 #include <stdint.h>
  22 #include "theory/arith/arithvar.h"
  23 #include "util/cvc4_assert.h"
  24 #include "util/dense_map.h"
  25
  26 namespace CVC4 {
  27 namespace theory {
  28 namespace arith {
  29
  30 class BoundCounts {
  31 private:
  32   uint32_t d_lowerBoundCount;
  33   uint32_t d_upperBoundCount;
  34
  35 public:
  36   BoundCounts() : d_lowerBoundCount(0), d_upperBoundCount(0) {}
  37   BoundCounts(uint32_t lbs, uint32_t ubs)
  38   : d_lowerBoundCount(lbs), d_upperBoundCount(ubs) {}
  39
  40   bool operator==(BoundCounts bc) const {
  41     return d_lowerBoundCount == bc.d_lowerBoundCount
  42       && d_upperBoundCount == bc.d_upperBoundCount;
  43   }
  44   bool operator!=(BoundCounts bc) const {
  45     return  d_lowerBoundCount != bc.d_lowerBoundCount
  46       || d_upperBoundCount != bc.d_upperBoundCount;
  47   }
  48   /** This is not a total order! */
  49   bool operator>=(BoundCounts bc) const {
  50     return d_lowerBoundCount >= bc.d_lowerBoundCount &&
  51       d_upperBoundCount >= bc.d_upperBoundCount;
  52   }
  53
  54   inline bool isZero() const{ return d_lowerBoundCount == 0 && d_upperBoundCount == 0; }
  55   inline uint32_t lowerBoundCount() const{
  56     return d_lowerBoundCount;
  57   }
  58   inline uint32_t upperBoundCount() const{
  59     return d_upperBoundCount;
  60   }
  61
  62   inline BoundCounts operator+(BoundCounts bc) const{
  63     return BoundCounts(d_lowerBoundCount + bc.d_lowerBoundCount,
  64                        d_upperBoundCount + bc.d_upperBoundCount);
  65   }
  66
  67   inline BoundCounts operator-(BoundCounts bc) const {
  68     Assert( *this >= bc );
  69     return BoundCounts(d_lowerBoundCount - bc.d_lowerBoundCount,
  70                        d_upperBoundCount - bc.d_upperBoundCount);
  71   }
  72
  73
  74   inline BoundCounts& operator+=(BoundCounts bc) {
  75     d_upperBoundCount += bc.d_upperBoundCount;
  76     d_lowerBoundCount += bc.d_lowerBoundCount;
  77     return *this;
  78   }
  79
  80   inline BoundCounts& operator-=(BoundCounts bc) {
  81     Assert(d_lowerBoundCount >= bc.d_lowerBoundCount);
  82     Assert(d_upperBoundCount >= bc.d_upperBoundCount);
  83     d_upperBoundCount -= bc.d_upperBoundCount;
  84     d_lowerBoundCount -= bc.d_lowerBoundCount;
  85
  86     return *this;
  87   }
  88
  89   /** Based on the sign coefficient a variable is multiplied by,
  90    * the effects the bound counts either has no effect (sgn == 0),
  91    * the lower bounds and upper bounds flip (sgn < 0), or nothing (sgn >0).
  92    */
  93   inline BoundCounts multiplyBySgn(int sgn) const{
  94     if(sgn > 0){
  95       return *this;
  96     }else if(sgn == 0){
  97       return BoundCounts(0,0);
  98     }else{
  99       return BoundCounts(d_upperBoundCount, d_lowerBoundCount);
 100     }
 101   }
 102
 103   inline void addInChange(int sgn, BoundCounts before, BoundCounts after){
 104     if(before == after){
 105       return;
 106     }else if(sgn < 0){
 107       Assert(d_upperBoundCount >= before.d_lowerBoundCount);
 108       Assert(d_lowerBoundCount >= before.d_upperBoundCount);
 109       d_upperBoundCount += after.d_lowerBoundCount - before.d_lowerBoundCount;
 110       d_lowerBoundCount += after.d_upperBoundCount - before.d_upperBoundCount;
 111     }else if(sgn > 0){
 112       Assert(d_upperBoundCount >= before.d_upperBoundCount);
 113       Assert(d_lowerBoundCount >= before.d_lowerBoundCount);
 114       d_upperBoundCount += after.d_upperBoundCount - before.d_upperBoundCount;
 115       d_lowerBoundCount += after.d_lowerBoundCount - before.d_lowerBoundCount;
 116     }
 117   }
 118
 119   inline void addInSgn(BoundCounts bc, int before, int after){
 120     Assert(before != after);
 121     Assert(!bc.isZero());
 122
 123     if(before < 0){
 124       d_upperBoundCount -= bc.d_lowerBoundCount;
 125       d_lowerBoundCount -= bc.d_upperBoundCount;
 126     }else if(before > 0){
 127       d_upperBoundCount -= bc.d_upperBoundCount;
 128       d_lowerBoundCount -= bc.d_lowerBoundCount;
 129     }
 130     if(after < 0){
 131       d_upperBoundCount += bc.d_lowerBoundCount;
 132       d_lowerBoundCount += bc.d_upperBoundCount;
 133     }else if(after > 0){
 134       d_upperBoundCount += bc.d_upperBoundCount;
 135       d_lowerBoundCount += bc.d_lowerBoundCount;
 136     }
 137   }
 138 };
 139
 140 class BoundsInfo {
 141 private:
 142
 143   /**
 144    * x = \sum_{a < 0} a_i i + \sum_{b > 0} b_j j
 145    *
 146    * AtUpperBound = {assignment(i) = lb(i)} \cup {assignment(j) = ub(j)}
 147    * AtLowerBound = {assignment(i) = ub(i)} \cup {assignment(j) = lb(j)}
 148    */
 149   BoundCounts d_atBounds;
 150
 151   /** This is for counting how many upper and lower bounds a row has. */
 152   BoundCounts d_hasBounds;
 153
 154 public:
 155   BoundsInfo() : d_atBounds(), d_hasBounds() {}
 156   BoundsInfo(BoundCounts atBounds, BoundCounts hasBounds)
 157     : d_atBounds(atBounds), d_hasBounds(hasBounds) {}
 158
 159   BoundCounts atBounds() const { return d_atBounds; }
 160   BoundCounts hasBounds() const { return d_hasBounds; }
 161
 162   /** This corresponds to adding in another variable to the row. */
 163   inline BoundsInfo operator+(const BoundsInfo& bc) const{
 164     return BoundsInfo(d_atBounds + bc.d_atBounds,
 165                       d_hasBounds + bc.d_hasBounds);
 166   }
 167   /** This corresponds to removing a variable from the row. */
 168   inline BoundsInfo operator-(const BoundsInfo& bc) const {
 169     Assert(*this >= bc);
 170     return BoundsInfo(d_atBounds - bc.d_atBounds,
 171                       d_hasBounds - bc.d_hasBounds);
 172   }
 173
 174   inline BoundsInfo& operator+=(const BoundsInfo& bc) {
 175     d_atBounds += bc.d_atBounds;
 176     d_hasBounds += bc.d_hasBounds;
 177     return (*this);
 178   }
 179
 180   /** Based on the sign coefficient a variable is multiplied by,
 181    * the effects the bound counts either has no effect (sgn == 0),
 182    * the lower bounds and upper bounds flip (sgn < 0), or nothing (sgn >0).
 183    */
 184   inline BoundsInfo multiplyBySgn(int sgn) const{
 185     return BoundsInfo(d_atBounds.multiplyBySgn(sgn), d_hasBounds.multiplyBySgn(sgn));
 186   }
 187
 188   bool operator==(const BoundsInfo& other) const{
 189     return d_atBounds == other.d_atBounds && d_hasBounds == other.d_hasBounds;
 190   }
 191   bool operator!=(const BoundsInfo& other) const{
 192     return !(*this == other);
 193   }
 194   /** This is not a total order! */
 195   bool operator>=(const BoundsInfo& other) const{
 196     return d_atBounds >= other.d_atBounds && d_hasBounds >= other.d_hasBounds;
 197   }
 198   void addInChange(int sgn, const BoundsInfo& before, const BoundsInfo& after){
 199     addInAtBoundChange(sgn, before.d_atBounds, after.d_atBounds);
 200     addInHasBoundChange(sgn, before.d_hasBounds, after.d_hasBounds);
 201   }
 202   void addInAtBoundChange(int sgn, BoundCounts before, BoundCounts after){
 203     d_atBounds.addInChange(sgn, before, after);
 204   }
 205   void addInHasBoundChange(int sgn, BoundCounts before, BoundCounts after){
 206     d_hasBounds.addInChange(sgn, before, after);
 207   }
 208
 209   inline void addInSgn(const BoundsInfo& bc, int before, int after){
 210     if(!bc.d_atBounds.isZero()){ d_atBounds.addInSgn(bc.d_atBounds, before, after);}
 211     if(!bc.d_hasBounds.isZero()){ d_hasBounds.addInSgn(bc.d_hasBounds, before, after);}
 212   }
 213 };
 214
 215 /** This is intended to map each row to its relevant bound information. */
 216 typedef DenseMap<BoundsInfo> BoundInfoMap;
 217
 218 inline std::ostream& operator<<(std::ostream& os, const BoundCounts& bc){
 219   os << "[bc " << bc.lowerBoundCount() << ", " << bc.upperBoundCount() << "]";
 220   return os;
 221 }
 222
 223 inline std::ostream& operator<<(std::ostream& os, const BoundsInfo& inf){
 224   os << "[bi : @ " << inf.atBounds() << ", " << inf.hasBounds() << "]";
 225   return os;
 226 }
 227 class BoundUpdateCallback {
 228 public:
 229   virtual void operator()(ArithVar v, const BoundsInfo&  up) = 0;
 230 };
 231
 232 }/* CVC4::theory::arith namespace */
 233 }/* CVC4::theory namespace */
 234 }/* CVC4 namespace */