Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Tim King, Clark Barrett
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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.
11 : : * ****************************************************************************
12 : : *
13 : : * [[ Add one-line brief description here ]]
14 : : *
15 : : * [[ Add lengthier description here ]]
16 : : * \todo document this file
17 : : */
18 : :
19 : : #include "cvc5_private.h"
20 : : #pragma once
21 : :
22 : : #include "base/check.h"
23 : : #include "theory/arith/linear/arithvar.h"
24 : : #include "util/dense_map.h"
25 : :
26 : : namespace cvc5::internal {
27 : : namespace theory {
28 : : namespace arith::linear {
29 : :
30 : : class BoundCounts {
31 : : private:
32 : : uint32_t d_lowerBoundCount;
33 : : uint32_t d_upperBoundCount;
34 : :
35 : : public:
36 : 74610280 : BoundCounts() : d_lowerBoundCount(0), d_upperBoundCount(0) {}
37 : 262508320 : BoundCounts(uint32_t lbs, uint32_t ubs)
38 : 262508320 : : d_lowerBoundCount(lbs), d_upperBoundCount(ubs) {}
39 : :
40 : 120173629 : bool operator==(BoundCounts bc) const {
41 : 120173629 : return d_lowerBoundCount == bc.d_lowerBoundCount
42 [ + + ][ + + ]: 120173629 : && d_upperBoundCount == bc.d_upperBoundCount;
43 : : }
44 : 7103312 : bool operator!=(BoundCounts bc) const {
45 : 7103312 : return d_lowerBoundCount != bc.d_lowerBoundCount
46 [ + + ][ + + ]: 7103312 : || d_upperBoundCount != bc.d_upperBoundCount;
47 : : }
48 : : /** This is not a total order! */
49 : 124970 : bool operator>=(BoundCounts bc) const {
50 [ + - ]: 249940 : return d_lowerBoundCount >= bc.d_lowerBoundCount &&
51 [ + - ]: 249940 : d_upperBoundCount >= bc.d_upperBoundCount;
52 : : }
53 : :
54 [ + + ][ + + ]: 335110098 : inline bool isZero() const{ return d_lowerBoundCount == 0 && d_upperBoundCount == 0; }
55 : 35514779 : inline uint32_t lowerBoundCount() const{
56 : 35514779 : return d_lowerBoundCount;
57 : : }
58 : 35177263 : inline uint32_t upperBoundCount() const{
59 : 35177263 : return d_upperBoundCount;
60 : : }
61 : :
62 : : inline BoundCounts operator+(BoundCounts bc) const{
63 : : return BoundCounts(d_lowerBoundCount + bc.d_lowerBoundCount,
64 : : d_upperBoundCount + bc.d_upperBoundCount);
65 : : }
66 : :
67 : 124970 : inline BoundCounts operator-(BoundCounts bc) const {
68 [ - + ][ - + ]: 124970 : Assert(*this >= bc);
[ - - ]
69 : 249940 : return BoundCounts(d_lowerBoundCount - bc.d_lowerBoundCount,
70 : 124970 : d_upperBoundCount - bc.d_upperBoundCount);
71 : : }
72 : :
73 : :
74 : 1966858 : inline BoundCounts& operator+=(BoundCounts bc) {
75 : 1966858 : d_upperBoundCount += bc.d_upperBoundCount;
76 : 1966858 : d_lowerBoundCount += bc.d_lowerBoundCount;
77 : 1966858 : return *this;
78 : : }
79 : :
80 : : inline BoundCounts& operator-=(BoundCounts bc) {
81 : : Assert(d_lowerBoundCount >= bc.d_lowerBoundCount);
82 : : Assert(d_upperBoundCount >= bc.d_upperBoundCount);
83 : : d_upperBoundCount -= bc.d_upperBoundCount;
84 : : d_lowerBoundCount -= bc.d_lowerBoundCount;
85 : :
86 : : return *this;
87 : : }
88 : :
89 : : /** Based on the sign coefficient a variable is multiplied by,
90 : : * the effects the bound counts either has no effect (sgn == 0),
91 : : * the lower bounds and upper bounds flip (sgn < 0), or nothing (sgn >0).
92 : : */
93 : 2624214 : inline BoundCounts multiplyBySgn(int sgn) const{
94 [ + + ]: 2624214 : if(sgn > 0){
95 : 984034 : return *this;
96 [ - + ]: 1640180 : }else if(sgn == 0){
97 : 0 : return BoundCounts(0,0);
98 : : }else{
99 : 1640180 : return BoundCounts(d_upperBoundCount, d_lowerBoundCount);
100 : : }
101 : : }
102 : :
103 : 96734815 : inline void addInChange(int sgn, BoundCounts before, BoundCounts after){
104 [ + + ]: 96734815 : if(before == after){
105 : 6515223 : return;
106 [ + + ]: 90219592 : }else if(sgn < 0){
107 [ - + ][ - + ]: 50080447 : Assert(d_upperBoundCount >= before.d_lowerBoundCount);
[ - - ]
108 [ - + ][ - + ]: 50080447 : Assert(d_lowerBoundCount >= before.d_upperBoundCount);
[ - - ]
109 : 50080447 : d_upperBoundCount += after.d_lowerBoundCount - before.d_lowerBoundCount;
110 : 50080447 : d_lowerBoundCount += after.d_upperBoundCount - before.d_upperBoundCount;
111 [ + - ]: 40139145 : }else if(sgn > 0){
112 [ - + ][ - + ]: 40139145 : Assert(d_upperBoundCount >= before.d_upperBoundCount);
[ - - ]
113 [ - + ][ - + ]: 40139145 : Assert(d_lowerBoundCount >= before.d_lowerBoundCount);
[ - - ]
114 : 40139145 : d_upperBoundCount += after.d_upperBoundCount - before.d_upperBoundCount;
115 : 40139145 : d_lowerBoundCount += after.d_lowerBoundCount - before.d_lowerBoundCount;
116 : : }
117 : : }
118 : :
119 : 161530398 : inline void addInSgn(BoundCounts bc, int before, int after){
120 [ - + ][ - + ]: 161530398 : Assert(before != after);
[ - - ]
121 [ - + ][ - + ]: 161530398 : Assert(!bc.isZero());
[ - - ]
122 : :
123 [ + + ]: 161530398 : if(before < 0){
124 : 40155140 : d_upperBoundCount -= bc.d_lowerBoundCount;
125 : 40155140 : d_lowerBoundCount -= bc.d_upperBoundCount;
126 [ + + ]: 121375258 : }else if(before > 0){
127 : 41086476 : d_upperBoundCount -= bc.d_upperBoundCount;
128 : 41086476 : d_lowerBoundCount -= bc.d_lowerBoundCount;
129 : : }
130 [ + + ]: 161530398 : if(after < 0){
131 : 47472615 : d_upperBoundCount += bc.d_lowerBoundCount;
132 : 47472615 : d_lowerBoundCount += bc.d_upperBoundCount;
133 [ + + ]: 114057783 : }else if(after > 0){
134 : 43610928 : d_upperBoundCount += bc.d_upperBoundCount;
135 : 43610928 : d_lowerBoundCount += bc.d_lowerBoundCount;
136 : : }
137 : 161530398 : }
138 : : };
139 : :
140 : : class BoundsInfo {
141 : : private:
142 : :
143 : : /**
144 : : * x = \sum_{a < 0} a_i i + \sum_{b > 0} b_j j
145 : : *
146 : : * AtUpperBound = {assignment(i) = lb(i)} \cup {assignment(j) = ub(j)}
147 : : * AtLowerBound = {assignment(i) = ub(i)} \cup {assignment(j) = lb(j)}
148 : : */
149 : : BoundCounts d_atBounds;
150 : :
151 : : /** This is for counting how many upper and lower bounds a row has. */
152 : : BoundCounts d_hasBounds;
153 : :
154 : : public:
155 : 37305140 : BoundsInfo() : d_atBounds(), d_hasBounds() {}
156 : 124267955 : BoundsInfo(BoundCounts atBounds, BoundCounts hasBounds)
157 : 124267955 : : d_atBounds(atBounds), d_hasBounds(hasBounds) {}
158 : :
159 : 1558416 : BoundCounts atBounds() const { return d_atBounds; }
160 : 18669269 : BoundCounts hasBounds() const { return d_hasBounds; }
161 : :
162 : : /** This corresponds to adding in another variable to the row. */
163 : : inline BoundsInfo operator+(const BoundsInfo& bc) const{
164 : : return BoundsInfo(d_atBounds + bc.d_atBounds,
165 : : d_hasBounds + bc.d_hasBounds);
166 : : }
167 : : /** This corresponds to removing a variable from the row. */
168 : : inline BoundsInfo operator-(const BoundsInfo& bc) const {
169 : : Assert(*this >= bc);
170 : : return BoundsInfo(d_atBounds - bc.d_atBounds,
171 : : d_hasBounds - bc.d_hasBounds);
172 : : }
173 : :
174 : 983429 : inline BoundsInfo& operator+=(const BoundsInfo& bc) {
175 : 983429 : d_atBounds += bc.d_atBounds;
176 : 983429 : d_hasBounds += bc.d_hasBounds;
177 : 983429 : return (*this);
178 : : }
179 : :
180 : : /** Based on the sign coefficient a variable is multiplied by,
181 : : * the effects the bound counts either has no effect (sgn == 0),
182 : : * the lower bounds and upper bounds flip (sgn < 0), or nothing (sgn >0).
183 : : */
184 : 1187137 : inline BoundsInfo multiplyBySgn(int sgn) const{
185 : 1187137 : return BoundsInfo(d_atBounds.multiplyBySgn(sgn), d_hasBounds.multiplyBySgn(sgn));
186 : : }
187 : :
188 : 18545821 : bool operator==(const BoundsInfo& other) const{
189 [ + + ][ + + ]: 18545821 : return d_atBounds == other.d_atBounds && d_hasBounds == other.d_hasBounds;
190 : : }
191 : 18545821 : bool operator!=(const BoundsInfo& other) const{
192 : 18545821 : return !(*this == other);
193 : : }
194 : : /** This is not a total order! */
195 : : bool operator>=(const BoundsInfo& other) const{
196 : : return d_atBounds >= other.d_atBounds && d_hasBounds >= other.d_hasBounds;
197 : : }
198 : 45527534 : void addInChange(int sgn, const BoundsInfo& before, const BoundsInfo& after){
199 : 45527534 : addInAtBoundChange(sgn, before.d_atBounds, after.d_atBounds);
200 : 45527534 : addInHasBoundChange(sgn, before.d_hasBounds, after.d_hasBounds);
201 : 45527534 : }
202 : 51082311 : void addInAtBoundChange(int sgn, BoundCounts before, BoundCounts after){
203 : 51082311 : d_atBounds.addInChange(sgn, before, after);
204 : 51082311 : }
205 : 45527534 : void addInHasBoundChange(int sgn, BoundCounts before, BoundCounts after){
206 : 45527534 : d_hasBounds.addInChange(sgn, before, after);
207 : 45527534 : }
208 : :
209 : 86789850 : inline void addInSgn(const BoundsInfo& bc, int before, int after){
210 [ + + ]: 86789850 : if(!bc.d_atBounds.isZero()){ d_atBounds.addInSgn(bc.d_atBounds, before, after);}
211 [ + + ]: 86789850 : if(!bc.d_hasBounds.isZero()){ d_hasBounds.addInSgn(bc.d_hasBounds, before, after);}
212 : 86789850 : }
213 : : };
214 : :
215 : : /** This is intended to map each row to its relevant bound information. */
216 : : typedef DenseMap<BoundsInfo> BoundInfoMap;
217 : :
218 : 0 : inline std::ostream& operator<<(std::ostream& os, const BoundCounts& bc){
219 : 0 : os << "[bc " << bc.lowerBoundCount() << ", " << bc.upperBoundCount() << "]";
220 : 0 : return os;
221 : : }
222 : :
223 : 0 : inline std::ostream& operator<<(std::ostream& os, const BoundsInfo& inf){
224 : 0 : os << "[bi : @ " << inf.atBounds() << ", " << inf.hasBounds() << "]";
225 : 0 : return os;
226 : : }
227 : : class BoundUpdateCallback {
228 : : public:
229 : 5117697 : virtual ~BoundUpdateCallback() {}
230 : : virtual void operator()(ArithVar v, const BoundsInfo& up) = 0;
231 : : };
232 : :
233 : : } // namespace arith
234 : : } // namespace theory
235 : : } // namespace cvc5::internal
|
