1 /********************* */
2 /*! \file bound_counts.h
4 ** Original author: Tim King
5 ** Major contributors: none
6 ** Minor contributors (to current version): Morgan Deters
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2013 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief [[ Add one-line brief description here ]]
14 ** [[ Add lengthier description here ]]
15 ** \todo document this file
18 #include "cvc4_private.h"
22 #include "theory/arith/arithvar.h"
23 #include "util/cvc4_assert.h"
24 #include "util/dense_map.h"
32 uint32_t d_lowerBoundCount
;
33 uint32_t d_upperBoundCount
;
36 BoundCounts() : d_lowerBoundCount(0), d_upperBoundCount(0) {}
37 BoundCounts(uint32_t lbs
, uint32_t ubs
)
38 : d_lowerBoundCount(lbs
), d_upperBoundCount(ubs
) {}
40 bool operator==(BoundCounts bc
) const {
41 return d_lowerBoundCount
== bc
.d_lowerBoundCount
42 && d_upperBoundCount
== bc
.d_upperBoundCount
;
44 bool operator!=(BoundCounts bc
) const {
45 return d_lowerBoundCount
!= bc
.d_lowerBoundCount
46 || d_upperBoundCount
!= bc
.d_upperBoundCount
;
48 /** This is not a total order! */
49 bool operator>=(BoundCounts bc
) const {
50 return d_lowerBoundCount
>= bc
.d_lowerBoundCount
&&
51 d_upperBoundCount
>= bc
.d_upperBoundCount
;
54 inline bool isZero() const{ return d_lowerBoundCount
== 0 && d_upperBoundCount
== 0; }
55 inline uint32_t lowerBoundCount() const{
56 return d_lowerBoundCount
;
58 inline uint32_t upperBoundCount() const{
59 return d_upperBoundCount
;
62 inline BoundCounts
operator+(BoundCounts bc
) const{
63 return BoundCounts(d_lowerBoundCount
+ bc
.d_lowerBoundCount
,
64 d_upperBoundCount
+ bc
.d_upperBoundCount
);
67 inline BoundCounts
operator-(BoundCounts bc
) const {
68 Assert( *this >= bc
);
69 return BoundCounts(d_lowerBoundCount
- bc
.d_lowerBoundCount
,
70 d_upperBoundCount
- bc
.d_upperBoundCount
);
74 inline BoundCounts
& operator+=(BoundCounts bc
) {
75 d_upperBoundCount
+= bc
.d_upperBoundCount
;
76 d_lowerBoundCount
+= bc
.d_lowerBoundCount
;
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
;
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).
93 inline BoundCounts
multiplyBySgn(int sgn
) const{
97 return BoundCounts(0,0);
99 return BoundCounts(d_upperBoundCount
, d_lowerBoundCount
);
103 inline void addInChange(int sgn
, BoundCounts before
, BoundCounts after
){
107 Assert(d_upperBoundCount
>= before
.d_lowerBoundCount
);
108 Assert(d_lowerBoundCount
>= before
.d_upperBoundCount
);
109 d_upperBoundCount
+= after
.d_lowerBoundCount
- before
.d_lowerBoundCount
;
110 d_lowerBoundCount
+= after
.d_upperBoundCount
- before
.d_upperBoundCount
;
112 Assert(d_upperBoundCount
>= before
.d_upperBoundCount
);
113 Assert(d_lowerBoundCount
>= before
.d_lowerBoundCount
);
114 d_upperBoundCount
+= after
.d_upperBoundCount
- before
.d_upperBoundCount
;
115 d_lowerBoundCount
+= after
.d_lowerBoundCount
- before
.d_lowerBoundCount
;
119 inline void addInSgn(BoundCounts bc
, int before
, int after
){
120 Assert(before
!= after
);
121 Assert(!bc
.isZero());
124 d_upperBoundCount
-= bc
.d_lowerBoundCount
;
125 d_lowerBoundCount
-= bc
.d_upperBoundCount
;
126 }else if(before
> 0){
127 d_upperBoundCount
-= bc
.d_upperBoundCount
;
128 d_lowerBoundCount
-= bc
.d_lowerBoundCount
;
131 d_upperBoundCount
+= bc
.d_lowerBoundCount
;
132 d_lowerBoundCount
+= bc
.d_upperBoundCount
;
134 d_upperBoundCount
+= bc
.d_upperBoundCount
;
135 d_lowerBoundCount
+= bc
.d_lowerBoundCount
;
144 * x = \sum_{a < 0} a_i i + \sum_{b > 0} b_j j
146 * AtUpperBound = {assignment(i) = lb(i)} \cup {assignment(j) = ub(j)}
147 * AtLowerBound = {assignment(i) = ub(i)} \cup {assignment(j) = lb(j)}
149 BoundCounts d_atBounds
;
151 /** This is for counting how many upper and lower bounds a row has. */
152 BoundCounts d_hasBounds
;
155 BoundsInfo() : d_atBounds(), d_hasBounds() {}
156 BoundsInfo(BoundCounts atBounds
, BoundCounts hasBounds
)
157 : d_atBounds(atBounds
), d_hasBounds(hasBounds
) {}
159 BoundCounts
atBounds() const { return d_atBounds
; }
160 BoundCounts
hasBounds() const { return d_hasBounds
; }
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
);
167 /** This corresponds to removing a variable from the row. */
168 inline BoundsInfo
operator-(const BoundsInfo
& bc
) const {
170 return BoundsInfo(d_atBounds
- bc
.d_atBounds
,
171 d_hasBounds
- bc
.d_hasBounds
);
174 inline BoundsInfo
& operator+=(const BoundsInfo
& bc
) {
175 d_atBounds
+= bc
.d_atBounds
;
176 d_hasBounds
+= bc
.d_hasBounds
;
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).
184 inline BoundsInfo
multiplyBySgn(int sgn
) const{
185 return BoundsInfo(d_atBounds
.multiplyBySgn(sgn
), d_hasBounds
.multiplyBySgn(sgn
));
188 bool operator==(const BoundsInfo
& other
) const{
189 return d_atBounds
== other
.d_atBounds
&& d_hasBounds
== other
.d_hasBounds
;
191 bool operator!=(const BoundsInfo
& other
) const{
192 return !(*this == other
);
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
;
198 void addInChange(int sgn
, const BoundsInfo
& before
, const BoundsInfo
& after
){
199 addInAtBoundChange(sgn
, before
.d_atBounds
, after
.d_atBounds
);
200 addInHasBoundChange(sgn
, before
.d_hasBounds
, after
.d_hasBounds
);
202 void addInAtBoundChange(int sgn
, BoundCounts before
, BoundCounts after
){
203 d_atBounds
.addInChange(sgn
, before
, after
);
205 void addInHasBoundChange(int sgn
, BoundCounts before
, BoundCounts after
){
206 d_hasBounds
.addInChange(sgn
, before
, after
);
209 inline void addInSgn(const BoundsInfo
& bc
, int before
, int after
){
210 if(!bc
.d_atBounds
.isZero()){ d_atBounds
.addInSgn(bc
.d_atBounds
, before
, after
);}
211 if(!bc
.d_hasBounds
.isZero()){ d_hasBounds
.addInSgn(bc
.d_hasBounds
, before
, after
);}
215 /** This is intended to map each row to its relevant bound information. */
216 typedef DenseMap
<BoundsInfo
> BoundInfoMap
;
218 inline std::ostream
& operator<<(std::ostream
& os
, const BoundCounts
& bc
){
219 os
<< "[bc " << bc
.lowerBoundCount() << ", " << bc
.upperBoundCount() << "]";
223 inline std::ostream
& operator<<(std::ostream
& os
, const BoundsInfo
& inf
){
224 os
<< "[bi : @ " << inf
.atBounds() << ", " << inf
.hasBounds() << "]";
227 class BoundUpdateCallback
{
229 virtual void operator()(ArithVar v
, const BoundsInfo
& up
) = 0;
232 }/* CVC4::theory::arith namespace */
233 }/* CVC4::theory namespace */
234 }/* CVC4 namespace */