diff options
author | Tim King <taking@cs.nyu.edu> | 2013-04-30 00:46:14 -0400 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2013-04-30 00:46:14 -0400 |
commit | 2b9e032cc93a96dccab8757326645da82b5866e5 (patch) | |
tree | 3d579a615f0d3acbf7edadc7cf81a237c4888f43 /src/theory/arith/bound_counts.h | |
parent | 9098391fe334d829ec4101f190b8f1fa21c30752 (diff) |
Adding has bound counts and tracking for rows.
Diffstat (limited to 'src/theory/arith/bound_counts.h')
-rw-r--r-- | src/theory/arith/bound_counts.h | 232 |
1 files changed, 161 insertions, 71 deletions
diff --git a/src/theory/arith/bound_counts.h b/src/theory/arith/bound_counts.h index 954cc056a..d82fff3eb 100644 --- a/src/theory/arith/bound_counts.h +++ b/src/theory/arith/bound_counts.h @@ -10,62 +10,92 @@ namespace CVC4 { namespace theory { namespace arith { -/** - * x = \sum_{a < 0} a_i i + \sum_{b > 0} b_j j - * - * AtUpperBound = {assignment(i) = lb(i)} \cup {assignment(j) = ub(j)} - * AtLowerBound = {assignment(i) = ub(i)} \cup {assignment(j) = lb(j)} - */ class BoundCounts { private: - uint32_t d_atLowerBounds; - uint32_t d_atUpperBounds; + uint32_t d_lowerBoundCount; + uint32_t d_upperBoundCount; public: - BoundCounts() : d_atLowerBounds(0), d_atUpperBounds(0) {} + BoundCounts() : d_lowerBoundCount(0), d_upperBoundCount(0) {} BoundCounts(uint32_t lbs, uint32_t ubs) - : d_atLowerBounds(lbs), d_atUpperBounds(ubs) {} + : d_lowerBoundCount(lbs), d_upperBoundCount(ubs) {} bool operator==(BoundCounts bc) const { - return d_atLowerBounds == bc.d_atLowerBounds - && d_atUpperBounds == bc.d_atUpperBounds; + return d_lowerBoundCount == bc.d_lowerBoundCount + && d_upperBoundCount == bc.d_upperBoundCount; } bool operator!=(BoundCounts bc) const { - return d_atLowerBounds != bc.d_atLowerBounds - || d_atUpperBounds != bc.d_atUpperBounds; + return d_lowerBoundCount != bc.d_lowerBoundCount + || d_upperBoundCount != bc.d_upperBoundCount; } - inline bool isZero() const{ return d_atLowerBounds == 0 && d_atUpperBounds == 0; } - inline uint32_t atLowerBounds() const{ - return d_atLowerBounds; + /** This is not a total order! */ + bool operator>=(BoundCounts bc) const { + return d_lowerBoundCount >= bc.d_lowerBoundCount && + d_upperBoundCount >= bc.d_upperBoundCount; } - inline uint32_t atUpperBounds() const{ - return d_atUpperBounds; + + inline bool isZero() const{ return d_lowerBoundCount == 0 && d_upperBoundCount == 0; } + inline uint32_t lowerBoundCount() const{ + return d_lowerBoundCount; + } + inline uint32_t upperBoundCount() const{ + return d_upperBoundCount; } inline BoundCounts operator+(BoundCounts bc) const{ - return BoundCounts(d_atLowerBounds + bc.d_atLowerBounds, - d_atUpperBounds + bc.d_atUpperBounds); + return BoundCounts(d_lowerBoundCount + bc.d_lowerBoundCount, + d_upperBoundCount + bc.d_upperBoundCount); } inline BoundCounts operator-(BoundCounts bc) const { - Assert(d_atLowerBounds >= bc.d_atLowerBounds); - Assert(d_atUpperBounds >= bc.d_atUpperBounds); - return BoundCounts(d_atLowerBounds - bc.d_atLowerBounds, - d_atUpperBounds - bc.d_atUpperBounds); + Assert( *this >= bc ); + return BoundCounts(d_lowerBoundCount - bc.d_lowerBoundCount, + d_upperBoundCount - bc.d_upperBoundCount); + } + + + inline BoundCounts& operator+=(BoundCounts bc) { + d_upperBoundCount += bc.d_upperBoundCount; + d_lowerBoundCount += bc.d_lowerBoundCount; + return *this; + } + + inline BoundCounts& operator-=(BoundCounts bc) { + Assert(d_lowerBoundCount >= bc.d_lowerBoundCount); + Assert(d_upperBoundCount >= bc.d_upperBoundCount); + d_upperBoundCount -= bc.d_upperBoundCount; + d_lowerBoundCount -= bc.d_lowerBoundCount; + + return *this; + } + + /** Based on the sign coefficient a variable is multiplied by, + * the effects the bound counts either has no effect (sgn == 0), + * the lower bounds and upper bounds flip (sgn < 0), or nothing (sgn >0). + */ + inline BoundCounts multiplyBySgn(int sgn) const{ + if(sgn > 0){ + return *this; + }else if(sgn == 0){ + return BoundCounts(0,0); + }else{ + return BoundCounts(d_upperBoundCount, d_lowerBoundCount); + } } inline void addInChange(int sgn, BoundCounts before, BoundCounts after){ - Assert(before != after); - if(sgn < 0){ - Assert(d_atUpperBounds >= before.d_atLowerBounds); - Assert(d_atLowerBounds >= before.d_atUpperBounds); - d_atUpperBounds += after.d_atLowerBounds - before.d_atLowerBounds; - d_atLowerBounds += after.d_atUpperBounds - before.d_atUpperBounds; + if(before == after){ + return; + }else if(sgn < 0){ + Assert(d_upperBoundCount >= before.d_lowerBoundCount); + Assert(d_lowerBoundCount >= before.d_upperBoundCount); + d_upperBoundCount += after.d_lowerBoundCount - before.d_lowerBoundCount; + d_lowerBoundCount += after.d_upperBoundCount - before.d_upperBoundCount; }else if(sgn > 0){ - Assert(d_atUpperBounds >= before.d_atUpperBounds); - Assert(d_atLowerBounds >= before.d_atLowerBounds); - d_atUpperBounds += after.d_atUpperBounds - before.d_atUpperBounds; - d_atLowerBounds += after.d_atLowerBounds - before.d_atLowerBounds; + Assert(d_upperBoundCount >= before.d_upperBoundCount); + Assert(d_lowerBoundCount >= before.d_lowerBoundCount); + d_upperBoundCount += after.d_upperBoundCount - before.d_upperBoundCount; + d_lowerBoundCount += after.d_lowerBoundCount - before.d_lowerBoundCount; } } @@ -74,69 +104,129 @@ public: Assert(!bc.isZero()); if(before < 0){ - d_atUpperBounds -= bc.d_atLowerBounds; - d_atLowerBounds -= bc.d_atUpperBounds; + d_upperBoundCount -= bc.d_lowerBoundCount; + d_lowerBoundCount -= bc.d_upperBoundCount; }else if(before > 0){ - d_atUpperBounds -= bc.d_atUpperBounds; - d_atLowerBounds -= bc.d_atLowerBounds; + d_upperBoundCount -= bc.d_upperBoundCount; + d_lowerBoundCount -= bc.d_lowerBoundCount; } if(after < 0){ - d_atUpperBounds += bc.d_atLowerBounds; - d_atLowerBounds += bc.d_atUpperBounds; + d_upperBoundCount += bc.d_lowerBoundCount; + d_lowerBoundCount += bc.d_upperBoundCount; }else if(after > 0){ - d_atUpperBounds += bc.d_atUpperBounds; - d_atLowerBounds += bc.d_atLowerBounds; + d_upperBoundCount += bc.d_upperBoundCount; + d_lowerBoundCount += bc.d_lowerBoundCount; } } +}; - inline BoundCounts& operator+=(BoundCounts bc) { - d_atUpperBounds += bc.d_atUpperBounds; - d_atLowerBounds += bc.d_atLowerBounds; - return *this; +class BoundsInfo { +private: + + /** + * x = \sum_{a < 0} a_i i + \sum_{b > 0} b_j j + * + * AtUpperBound = {assignment(i) = lb(i)} \cup {assignment(j) = ub(j)} + * AtLowerBound = {assignment(i) = ub(i)} \cup {assignment(j) = lb(j)} + */ + BoundCounts d_atBounds; + + /** This is for counting how many upper and lower bounds a row has. */ + BoundCounts d_hasBounds; + +public: + BoundsInfo() : d_atBounds(), d_hasBounds() {} + BoundsInfo(BoundCounts atBounds, BoundCounts hasBounds) + : d_atBounds(atBounds), d_hasBounds(hasBounds) {} + + BoundCounts atBounds() const { return d_atBounds; } + BoundCounts hasBounds() const { return d_hasBounds; } + + /** This corresponds to adding in another variable to the row. */ + inline BoundsInfo operator+(const BoundsInfo& bc) const{ + return BoundsInfo(d_atBounds + bc.d_atBounds, + d_hasBounds + bc.d_hasBounds); + } + /** This corresponds to removing a variable from the row. */ + inline BoundsInfo operator-(const BoundsInfo& bc) const { + Assert(*this >= bc); + return BoundsInfo(d_atBounds - bc.d_atBounds, + d_hasBounds - bc.d_hasBounds); } - inline BoundCounts& operator-=(BoundCounts bc) { - Assert(d_atLowerBounds >= bc.d_atLowerBounds); - Assert(d_atUpperBounds >= bc.d_atUpperBounds); - d_atUpperBounds -= bc.d_atUpperBounds; - d_atLowerBounds -= bc.d_atLowerBounds; + inline BoundsInfo& operator+=(const BoundsInfo& bc) { + d_atBounds += bc.d_atBounds; + d_hasBounds += bc.d_hasBounds; + return (*this); + } - return *this; + /** Based on the sign coefficient a variable is multiplied by, + * the effects the bound counts either has no effect (sgn == 0), + * the lower bounds and upper bounds flip (sgn < 0), or nothing (sgn >0). + */ + inline BoundsInfo multiplyBySgn(int sgn) const{ + return BoundsInfo(d_atBounds.multiplyBySgn(sgn), d_hasBounds.multiplyBySgn(sgn)); } - inline BoundCounts multiplyBySgn(int sgn) const{ - if(sgn > 0){ - return *this; - }else if(sgn == 0){ - return BoundCounts(0,0); - }else{ - return BoundCounts(d_atUpperBounds, d_atLowerBounds); - } + bool operator==(const BoundsInfo& other) const{ + return d_atBounds == other.d_atBounds && d_hasBounds == other.d_hasBounds; + } + bool operator!=(const BoundsInfo& other) const{ + return !(*this == other); + } + /** This is not a total order! */ + bool operator>=(const BoundsInfo& other) const{ + return d_atBounds >= other.d_atBounds && d_hasBounds >= other.d_hasBounds; + } + void addInChange(int sgn, const BoundsInfo& before, const BoundsInfo& after){ + addInAtBoundChange(sgn, before.d_atBounds, after.d_atBounds); + addInHasBoundChange(sgn, before.d_hasBounds, after.d_hasBounds); + } + void addInAtBoundChange(int sgn, BoundCounts before, BoundCounts after){ + d_atBounds.addInChange(sgn, before, after); + } + void addInHasBoundChange(int sgn, BoundCounts before, BoundCounts after){ + d_hasBounds.addInChange(sgn, before, after); + } + + inline void addInSgn(const BoundsInfo& bc, int before, int after){ + if(!bc.d_atBounds.isZero()){ d_atBounds.addInSgn(bc.d_atBounds, before, after);} + if(!bc.d_hasBounds.isZero()){ d_hasBounds.addInSgn(bc.d_hasBounds, before, after);} } }; -typedef DenseMap<BoundCounts> BoundCountingVector; +/** This is intended to map each row to its relevant bound information. */ +typedef DenseMap<BoundsInfo> BoundInfoMap; + +class Tableau; class BoundCountingLookup { private: - BoundCountingVector* d_bc; + BoundInfoMap* d_bc; + Tableau* d_tab; public: - BoundCountingLookup(BoundCountingVector* bc) : d_bc(bc) {} - BoundCounts boundCounts(ArithVar v) const { - Assert(d_bc->isKey(v)); - return (*d_bc)[v]; + BoundCountingLookup(BoundInfoMap* bc, Tableau* tab) : d_bc(bc), d_tab(tab) {} + const BoundsInfo& boundsInfo(ArithVar basic) const; + BoundCounts atBounds(ArithVar basic) const{ + return boundsInfo(basic).atBounds(); + } + BoundCounts hasBounds(ArithVar basic) const { + return boundsInfo(basic).hasBounds(); } }; inline std::ostream& operator<<(std::ostream& os, const BoundCounts& bc){ - os << "[bc " << bc.atLowerBounds() << ", " - << bc.atUpperBounds() << "]"; + os << "[bc " << bc.lowerBoundCount() << ", " << bc.upperBoundCount() << "]"; return os; } -class BoundCountsCallback { +inline std::ostream& operator<<(std::ostream& os, const BoundsInfo& inf){ + os << "[bi : @ " << inf.atBounds() << ", " << inf.hasBounds() << "]"; + return os; +} +class BoundUpdateCallback { public: - virtual void operator()(ArithVar v, BoundCounts bc) = 0; + virtual void operator()(ArithVar v, const BoundsInfo& up) = 0; }; }/* CVC4::theory::arith namespace */ |