summaryrefslogtreecommitdiff
path: root/src/theory/arith/bound_counts.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith/bound_counts.h')
-rw-r--r--src/theory/arith/bound_counts.h232
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback