Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * [[ Add one-line brief description here ]]
11 : : *
12 : : * [[ Add lengthier description here ]]
13 : : * \todo document this file
14 : : */
15 : :
16 : : #include "cvc5_private.h"
17 : : #pragma once
18 : :
19 : : #include "base/check.h"
20 : : #include "theory/arith/linear/arithvar.h"
21 : : #include "util/dense_map.h"
22 : :
23 : : namespace cvc5::internal {
24 : : namespace theory {
25 : : namespace arith::linear {
26 : :
27 : : class BoundCounts
28 : : {
29 : : private:
30 : : uint32_t d_lowerBoundCount;
31 : : uint32_t d_upperBoundCount;
32 : :
33 : : public:
34 : 73944314 : BoundCounts() : d_lowerBoundCount(0), d_upperBoundCount(0) {}
35 : 231754010 : BoundCounts(uint32_t lbs, uint32_t ubs)
36 : 231754010 : : d_lowerBoundCount(lbs), d_upperBoundCount(ubs)
37 : : {
38 : 231754010 : }
39 : :
40 : 119120455 : bool operator==(BoundCounts bc) const
41 : : {
42 : 119120455 : return d_lowerBoundCount == bc.d_lowerBoundCount
43 [ + + ][ + + ]: 119120455 : && d_upperBoundCount == bc.d_upperBoundCount;
44 : : }
45 : 6960550 : bool operator!=(BoundCounts bc) const
46 : : {
47 : 6960550 : return d_lowerBoundCount != bc.d_lowerBoundCount
48 [ + + ][ + + ]: 6960550 : || d_upperBoundCount != bc.d_upperBoundCount;
49 : : }
50 : : /** This is not a total order! */
51 : 141948 : bool operator>=(BoundCounts bc) const
52 : : {
53 : 141948 : return d_lowerBoundCount >= bc.d_lowerBoundCount
54 [ + - ][ + - ]: 141948 : && d_upperBoundCount >= bc.d_upperBoundCount;
55 : : }
56 : :
57 : 275001124 : inline bool isZero() const
58 : : {
59 [ + + ][ + + ]: 275001124 : return d_lowerBoundCount == 0 && d_upperBoundCount == 0;
60 : : }
61 : 35604250 : inline uint32_t lowerBoundCount() const { return d_lowerBoundCount; }
62 : 35287605 : inline uint32_t upperBoundCount() const { return d_upperBoundCount; }
63 : :
64 : : inline BoundCounts operator+(BoundCounts bc) const
65 : : {
66 : : return BoundCounts(d_lowerBoundCount + bc.d_lowerBoundCount,
67 : : d_upperBoundCount + bc.d_upperBoundCount);
68 : : }
69 : :
70 : 141948 : inline BoundCounts operator-(BoundCounts bc) const
71 : : {
72 [ - + ][ - + ]: 141948 : Assert(*this >= bc);
[ - - ]
73 : 283896 : return BoundCounts(d_lowerBoundCount - bc.d_lowerBoundCount,
74 : 141948 : d_upperBoundCount - bc.d_upperBoundCount);
75 : : }
76 : :
77 : 2036620 : inline BoundCounts& operator+=(BoundCounts bc)
78 : : {
79 : 2036620 : d_upperBoundCount += bc.d_upperBoundCount;
80 : 2036620 : d_lowerBoundCount += bc.d_lowerBoundCount;
81 : 2036620 : return *this;
82 : : }
83 : :
84 : : inline BoundCounts& operator-=(BoundCounts bc)
85 : : {
86 : : Assert(d_lowerBoundCount >= bc.d_lowerBoundCount);
87 : : Assert(d_upperBoundCount >= bc.d_upperBoundCount);
88 : : d_upperBoundCount -= bc.d_upperBoundCount;
89 : : d_lowerBoundCount -= bc.d_lowerBoundCount;
90 : :
91 : : return *this;
92 : : }
93 : :
94 : : /** Based on the sign coefficient a variable is multiplied by,
95 : : * the effects the bound counts either has no effect (sgn == 0),
96 : : * the lower bounds and upper bounds flip (sgn < 0), or nothing (sgn >0).
97 : : */
98 : 2694036 : inline BoundCounts multiplyBySgn(int sgn) const
99 : : {
100 [ + + ]: 2694036 : if (sgn > 0)
101 : : {
102 : 1034556 : return *this;
103 : : }
104 [ - + ]: 1659480 : else if (sgn == 0)
105 : : {
106 : 0 : return BoundCounts(0, 0);
107 : : }
108 : : else
109 : : {
110 : 1659480 : return BoundCounts(d_upperBoundCount, d_lowerBoundCount);
111 : : }
112 : : }
113 : :
114 : 95946069 : inline void addInChange(int sgn, BoundCounts before, BoundCounts after)
115 : : {
116 [ + + ]: 95946069 : if (before == after)
117 : : {
118 : 6358786 : return;
119 : : }
120 [ + + ]: 89587283 : else if (sgn < 0)
121 : : {
122 [ - + ][ - + ]: 49117999 : Assert(d_upperBoundCount >= before.d_lowerBoundCount);
[ - - ]
123 [ - + ][ - + ]: 49117999 : Assert(d_lowerBoundCount >= before.d_upperBoundCount);
[ - - ]
124 : 49117999 : d_upperBoundCount += after.d_lowerBoundCount - before.d_lowerBoundCount;
125 : 49117999 : d_lowerBoundCount += after.d_upperBoundCount - before.d_upperBoundCount;
126 : : }
127 [ + - ]: 40469284 : else if (sgn > 0)
128 : : {
129 [ - + ][ - + ]: 40469284 : Assert(d_upperBoundCount >= before.d_upperBoundCount);
[ - - ]
130 [ - + ][ - + ]: 40469284 : Assert(d_lowerBoundCount >= before.d_lowerBoundCount);
[ - - ]
131 : 40469284 : d_upperBoundCount += after.d_upperBoundCount - before.d_upperBoundCount;
132 : 40469284 : d_lowerBoundCount += after.d_lowerBoundCount - before.d_lowerBoundCount;
133 : : }
134 : : }
135 : :
136 : 131580104 : inline void addInSgn(BoundCounts bc, int before, int after)
137 : : {
138 [ - + ][ - + ]: 131580104 : Assert(before != after);
[ - - ]
139 [ - + ][ - + ]: 131580104 : Assert(!bc.isZero());
[ - - ]
140 : :
141 [ + + ]: 131580104 : if (before < 0)
142 : : {
143 : 32787167 : d_upperBoundCount -= bc.d_lowerBoundCount;
144 : 32787167 : d_lowerBoundCount -= bc.d_upperBoundCount;
145 : : }
146 [ + + ]: 98792937 : else if (before > 0)
147 : : {
148 : 32955144 : d_upperBoundCount -= bc.d_upperBoundCount;
149 : 32955144 : d_lowerBoundCount -= bc.d_lowerBoundCount;
150 : : }
151 [ + + ]: 131580104 : if (after < 0)
152 : : {
153 : 39058516 : d_upperBoundCount += bc.d_lowerBoundCount;
154 : 39058516 : d_lowerBoundCount += bc.d_upperBoundCount;
155 : : }
156 [ + + ]: 92521588 : else if (after > 0)
157 : : {
158 : 36418476 : d_upperBoundCount += bc.d_upperBoundCount;
159 : 36418476 : d_lowerBoundCount += bc.d_lowerBoundCount;
160 : : }
161 : 131580104 : }
162 : : };
163 : :
164 : : class BoundsInfo
165 : : {
166 : : private:
167 : : /**
168 : : * x = \sum_{a < 0} a_i i + \sum_{b > 0} b_j j
169 : : *
170 : : * AtUpperBound = {assignment(i) = lb(i)} \cup {assignment(j) = ub(j)}
171 : : * AtLowerBound = {assignment(i) = ub(i)} \cup {assignment(j) = lb(j)}
172 : : */
173 : : BoundCounts d_atBounds;
174 : :
175 : : /** This is for counting how many upper and lower bounds a row has. */
176 : : BoundCounts d_hasBounds;
177 : :
178 : : public:
179 : 36972157 : BoundsInfo() : d_atBounds(), d_hasBounds() {}
180 : 109007889 : BoundsInfo(BoundCounts atBounds, BoundCounts hasBounds)
181 : 109007889 : : d_atBounds(atBounds), d_hasBounds(hasBounds)
182 : : {
183 : 109007889 : }
184 : :
185 : 1545645 : BoundCounts atBounds() const { return d_atBounds; }
186 : 18723461 : BoundCounts hasBounds() const { return d_hasBounds; }
187 : :
188 : : /** This corresponds to adding in another variable to the row. */
189 : : inline BoundsInfo operator+(const BoundsInfo& bc) const
190 : : {
191 : : return BoundsInfo(d_atBounds + bc.d_atBounds, d_hasBounds + bc.d_hasBounds);
192 : : }
193 : : /** This corresponds to removing a variable from the row. */
194 : : inline BoundsInfo operator-(const BoundsInfo& bc) const
195 : : {
196 : : Assert(*this >= bc);
197 : : return BoundsInfo(d_atBounds - bc.d_atBounds, d_hasBounds - bc.d_hasBounds);
198 : : }
199 : :
200 : 1018310 : inline BoundsInfo& operator+=(const BoundsInfo& bc)
201 : : {
202 : 1018310 : d_atBounds += bc.d_atBounds;
203 : 1018310 : d_hasBounds += bc.d_hasBounds;
204 : 1018310 : return (*this);
205 : : }
206 : :
207 : : /** Based on the sign coefficient a variable is multiplied by,
208 : : * the effects the bound counts either has no effect (sgn == 0),
209 : : * the lower bounds and upper bounds flip (sgn < 0), or nothing (sgn >0).
210 : : */
211 : 1205070 : inline BoundsInfo multiplyBySgn(int sgn) const
212 : : {
213 : 1205070 : return BoundsInfo(d_atBounds.multiplyBySgn(sgn),
214 : 1205070 : d_hasBounds.multiplyBySgn(sgn));
215 : : }
216 : :
217 : 18399882 : bool operator==(const BoundsInfo& other) const
218 : : {
219 [ + + ][ + + ]: 18399882 : return d_atBounds == other.d_atBounds && d_hasBounds == other.d_hasBounds;
220 : : }
221 : 18399882 : bool operator!=(const BoundsInfo& other) const { return !(*this == other); }
222 : : /** This is not a total order! */
223 : : bool operator>=(const BoundsInfo& other) const
224 : : {
225 : : return d_atBounds >= other.d_atBounds && d_hasBounds >= other.d_hasBounds;
226 : : }
227 : 45213182 : void addInChange(int sgn, const BoundsInfo& before, const BoundsInfo& after)
228 : : {
229 : 45213182 : addInAtBoundChange(sgn, before.d_atBounds, after.d_atBounds);
230 : 45213182 : addInHasBoundChange(sgn, before.d_hasBounds, after.d_hasBounds);
231 : 45213182 : }
232 : 50590939 : void addInAtBoundChange(int sgn, BoundCounts before, BoundCounts after)
233 : : {
234 : 50590939 : d_atBounds.addInChange(sgn, before, after);
235 : 50590939 : }
236 : 45213182 : void addInHasBoundChange(int sgn, BoundCounts before, BoundCounts after)
237 : : {
238 : 45213182 : d_hasBounds.addInChange(sgn, before, after);
239 : 45213182 : }
240 : :
241 : 71710510 : inline void addInSgn(const BoundsInfo& bc, int before, int after)
242 : : {
243 [ + + ]: 71710510 : if (!bc.d_atBounds.isZero())
244 : : {
245 : 63401971 : d_atBounds.addInSgn(bc.d_atBounds, before, after);
246 : : }
247 [ + + ]: 71710510 : if (!bc.d_hasBounds.isZero())
248 : : {
249 : 68178133 : d_hasBounds.addInSgn(bc.d_hasBounds, before, after);
250 : : }
251 : 71710510 : }
252 : : };
253 : :
254 : : /** This is intended to map each row to its relevant bound information. */
255 : : typedef DenseMap<BoundsInfo> BoundInfoMap;
256 : :
257 : 0 : inline std::ostream& operator<<(std::ostream& os, const BoundCounts& bc)
258 : : {
259 : 0 : os << "[bc " << bc.lowerBoundCount() << ", " << bc.upperBoundCount() << "]";
260 : 0 : return os;
261 : : }
262 : :
263 : 0 : inline std::ostream& operator<<(std::ostream& os, const BoundsInfo& inf)
264 : : {
265 : 0 : os << "[bi : @ " << inf.atBounds() << ", " << inf.hasBounds() << "]";
266 : 0 : return os;
267 : : }
268 : : class BoundUpdateCallback
269 : : {
270 : : public:
271 : 5194534 : virtual ~BoundUpdateCallback() {}
272 : : virtual void operator()(ArithVar v, const BoundsInfo& up) = 0;
273 : : };
274 : :
275 : : } // namespace arith::linear
276 : : } // namespace theory
277 : : } // namespace cvc5::internal
|
