GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/bound_counts.h Lines: 83 97 85.6 %
Date: 2021-03-23 Branches: 48 162 29.6 %

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