GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/bound_counts.h Lines: 83 97 85.6 %
Date: 2021-03-22 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
37808848
  BoundCounts() : d_lowerBoundCount(0), d_upperBoundCount(0) {}
36
152049132
  BoundCounts(uint32_t lbs, uint32_t ubs)
37
152049132
  : d_lowerBoundCount(lbs), d_upperBoundCount(ubs) {}
38
39
56507169
  bool operator==(BoundCounts bc) const {
40
56507169
    return d_lowerBoundCount == bc.d_lowerBoundCount
41
56507169
      && d_upperBoundCount == bc.d_upperBoundCount;
42
  }
43
3970877
  bool operator!=(BoundCounts bc) const {
44
3970877
    return  d_lowerBoundCount != bc.d_lowerBoundCount
45
3970877
      || 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
209453879
  inline bool isZero() const{ return d_lowerBoundCount == 0 && d_upperBoundCount == 0; }
54
16215538
  inline uint32_t lowerBoundCount() const{
55
16215538
    return d_lowerBoundCount;
56
  }
57
16049227
  inline uint32_t upperBoundCount() const{
58
16049227
    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
762100
  inline BoundCounts& operator+=(BoundCounts bc) {
74
762100
    d_upperBoundCount += bc.d_upperBoundCount;
75
762100
    d_lowerBoundCount += bc.d_lowerBoundCount;
76
762100
    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
980346
  inline BoundCounts multiplyBySgn(int sgn) const{
93
980346
    if(sgn > 0){
94
329194
      return *this;
95
651152
    }else if(sgn == 0){
96
      return BoundCounts(0,0);
97
    }else{
98
651152
      return BoundCounts(d_upperBoundCount, d_lowerBoundCount);
99
    }
100
  }
101
102
45031825
  inline void addInChange(int sgn, BoundCounts before, BoundCounts after){
103
45031825
    if(before == after){
104
3041405
      return;
105
41990420
    }else if(sgn < 0){
106
23315516
      Assert(d_upperBoundCount >= before.d_lowerBoundCount);
107
23315516
      Assert(d_lowerBoundCount >= before.d_upperBoundCount);
108
23315516
      d_upperBoundCount += after.d_lowerBoundCount - before.d_lowerBoundCount;
109
23315516
      d_lowerBoundCount += after.d_upperBoundCount - before.d_upperBoundCount;
110
18674904
    }else if(sgn > 0){
111
18674904
      Assert(d_upperBoundCount >= before.d_upperBoundCount);
112
18674904
      Assert(d_lowerBoundCount >= before.d_lowerBoundCount);
113
18674904
      d_upperBoundCount += after.d_upperBoundCount - before.d_upperBoundCount;
114
18674904
      d_lowerBoundCount += after.d_lowerBoundCount - before.d_lowerBoundCount;
115
    }
116
  }
117
118
101588013
  inline void addInSgn(BoundCounts bc, int before, int after){
119
101588013
    Assert(before != after);
120
101588013
    Assert(!bc.isZero());
121
122
101588013
    if(before < 0){
123
25980948
      d_upperBoundCount -= bc.d_lowerBoundCount;
124
25980948
      d_lowerBoundCount -= bc.d_upperBoundCount;
125
75607065
    }else if(before > 0){
126
25908200
      d_upperBoundCount -= bc.d_upperBoundCount;
127
25908200
      d_lowerBoundCount -= bc.d_lowerBoundCount;
128
    }
129
101588013
    if(after < 0){
130
30118975
      d_upperBoundCount += bc.d_lowerBoundCount;
131
30118975
      d_lowerBoundCount += bc.d_upperBoundCount;
132
71469038
    }else if(after > 0){
133
27238980
      d_upperBoundCount += bc.d_upperBoundCount;
134
27238980
      d_lowerBoundCount += bc.d_lowerBoundCount;
135
    }
136
101588013
  }
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
18904424
  BoundsInfo() : d_atBounds(), d_hasBounds() {}
155
72218286
  BoundsInfo(BoundCounts atBounds, BoundCounts hasBounds)
156
72218286
    : d_atBounds(atBounds), d_hasBounds(hasBounds) {}
157
158
895219
  BoundCounts atBounds() const { return d_atBounds; }
159
8617674
  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
381050
  inline BoundsInfo& operator+=(const BoundsInfo& bc) {
174
381050
    d_atBounds += bc.d_atBounds;
175
381050
    d_hasBounds += bc.d_hasBounds;
176
381050
    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
490173
  inline BoundsInfo multiplyBySgn(int sgn) const{
184
490173
    return BoundsInfo(d_atBounds.multiplyBySgn(sgn), d_hasBounds.multiplyBySgn(sgn));
185
  }
186
187
9179966
  bool operator==(const BoundsInfo& other) const{
188
9179966
    return d_atBounds == other.d_atBounds && d_hasBounds == other.d_hasBounds;
189
  }
190
9179966
  bool operator!=(const BoundsInfo& other) const{
191
9179966
    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
20913117
  void addInChange(int sgn, const BoundsInfo& before, const BoundsInfo& after){
198
20913117
    addInAtBoundChange(sgn, before.d_atBounds, after.d_atBounds);
199
20913117
    addInHasBoundChange(sgn, before.d_hasBounds, after.d_hasBounds);
200
20913117
  }
201
24118708
  void addInAtBoundChange(int sgn, BoundCounts before, BoundCounts after){
202
24118708
    d_atBounds.addInChange(sgn, before, after);
203
24118708
  }
204
20913117
  void addInHasBoundChange(int sgn, BoundCounts before, BoundCounts after){
205
20913117
    d_hasBounds.addInChange(sgn, before, after);
206
20913117
  }
207
208
53932933
  inline void addInSgn(const BoundsInfo& bc, int before, int after){
209
53932933
    if(!bc.d_atBounds.isZero()){ d_atBounds.addInSgn(bc.d_atBounds, before, after);}
210
53932933
    if(!bc.d_hasBounds.isZero()){ d_hasBounds.addInSgn(bc.d_hasBounds, before, after);}
211
53932933
  }
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
2811558
class BoundUpdateCallback {
227
public:
228
2811558
  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 */