Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Tim King, Andres Noetzli, Gereon Kremer
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 "base/output.h"
20 : : #include "theory/arith/linear/constraint.h"
21 : : #include "theory/arith/linear/normal_form.h"
22 : : #include "theory/arith/linear/partial_model.h"
23 : :
24 : : using namespace std;
25 : :
26 : : namespace cvc5::internal {
27 : : namespace theory {
28 : : namespace arith::linear {
29 : :
30 : 50287 : ArithVariables::ArithVariables(context::Context* c,
31 : 50287 : DeltaComputeCallback deltaComputingFunc)
32 : : : d_vars(),
33 : : d_safeAssignment(),
34 : : d_numberOfVariables(0),
35 : : d_pool(),
36 : : d_released(),
37 : : d_nodeToArithVarMap(),
38 : : d_boundsQueue(),
39 : : d_enqueueingBoundCounts(true),
40 : 0 : d_lbRevertHistory(c, true, LowerBoundCleanUp(this)),
41 : 0 : d_ubRevertHistory(c, true, UpperBoundCleanUp(this)),
42 : : d_deltaIsSafe(false),
43 : : d_delta(-1, 1),
44 : 50287 : d_deltaComputingFunc(deltaComputingFunc)
45 : 50287 : { }
46 : :
47 : 79163600 : ArithVar ArithVariables::getNumberOfVariables() const {
48 : 79163600 : return d_numberOfVariables;
49 : : }
50 : :
51 : :
52 : 13070600 : bool ArithVariables::hasArithVar(TNode x) const {
53 : 13070600 : return d_nodeToArithVarMap.find(x) != d_nodeToArithVarMap.end();
54 : : }
55 : :
56 : 31293800 : bool ArithVariables::hasNode(ArithVar a) const {
57 : 31293800 : return d_vars.isKey(a);
58 : : }
59 : :
60 : 5443700 : ArithVar ArithVariables::asArithVar(TNode x) const{
61 [ - + ][ - + ]: 5443700 : Assert(hasArithVar(x));
[ - - ]
62 [ - + ][ - + ]: 5443700 : Assert((d_nodeToArithVarMap.find(x))->second <= ARITHVAR_SENTINEL);
[ - - ]
63 : 5443700 : return (d_nodeToArithVarMap.find(x))->second;
64 : : }
65 : :
66 : 19693800 : Node ArithVariables::asNode(ArithVar a) const{
67 [ - + ][ - + ]: 19693800 : Assert(hasNode(a));
[ - - ]
68 : 19693800 : return d_vars[a].d_node;
69 : : }
70 : :
71 : 0 : ArithVariables::var_iterator::var_iterator()
72 : : : d_vars(NULL)
73 : 0 : , d_wrapped()
74 : 0 : {}
75 : :
76 : 506920 : ArithVariables::var_iterator::var_iterator(const VarInfoVec* vars, VarInfoVec::const_iterator ci)
77 : 506920 : : d_vars(vars), d_wrapped(ci)
78 : : {
79 : 506920 : nextInitialized();
80 : 506920 : }
81 : :
82 : 14342100 : ArithVariables::var_iterator& ArithVariables::var_iterator::operator++(){
83 : 14342100 : ++d_wrapped;
84 : 14342100 : nextInitialized();
85 : 14342100 : return *this;
86 : : }
87 : 0 : bool ArithVariables::var_iterator::operator==(const ArithVariables::var_iterator& other) const{
88 : 0 : return d_wrapped == other.d_wrapped;
89 : : }
90 : 14595600 : bool ArithVariables::var_iterator::operator!=(const ArithVariables::var_iterator& other) const{
91 : 14595600 : return d_wrapped != other.d_wrapped;
92 : : }
93 : 14342100 : ArithVar ArithVariables::var_iterator::operator*() const{
94 : 14342100 : return *d_wrapped;
95 : : }
96 : :
97 : 14849100 : void ArithVariables::var_iterator::nextInitialized(){
98 : 14849100 : VarInfoVec::const_iterator end = d_vars->end();
99 [ + + ][ + + ]: 29191500 : while(d_wrapped != end &&
100 [ + + ]: 14342300 : !((*d_vars)[*d_wrapped].initialized())){
101 : 150 : ++d_wrapped;
102 : : }
103 : 14849100 : }
104 : :
105 : 253460 : ArithVariables::var_iterator ArithVariables::var_begin() const {
106 : 253460 : return var_iterator(&d_vars, d_vars.begin());
107 : : }
108 : :
109 : 253460 : ArithVariables::var_iterator ArithVariables::var_end() const {
110 : 253460 : return var_iterator(&d_vars, d_vars.end());
111 : : }
112 : 39328800 : bool ArithVariables::isInteger(ArithVar x) const {
113 : 39328800 : return d_vars[x].d_type >= ArithType::Integer;
114 : : }
115 : :
116 : : /** Is the assignment to x integral? */
117 : 3159000 : bool ArithVariables::integralAssignment(ArithVar x) const {
118 : 3159000 : return getAssignment(x).isIntegral();
119 : : }
120 : 14538200 : bool ArithVariables::isAuxiliary(ArithVar x) const {
121 : 14538200 : return d_vars[x].d_auxiliary;
122 : : }
123 : :
124 : 7401290 : bool ArithVariables::isIntegerInput(ArithVar x) const {
125 [ + + ][ + + ]: 7401290 : return isInteger(x) && !isAuxiliary(x);
126 : : }
127 : :
128 : 722591 : ArithVariables::VarInfo::VarInfo()
129 : : : d_var(ARITHVAR_SENTINEL),
130 : : d_assignment(0),
131 : : d_lb(NullConstraint),
132 : : d_ub(NullConstraint),
133 : : d_cmpAssignmentLB(1),
134 : : d_cmpAssignmentUB(-1),
135 : : d_pushCount(0),
136 : : d_type(ArithType::Unset),
137 : : d_node(Node::null()),
138 : 722591 : d_auxiliary(false) {}
139 : :
140 : 43603000 : bool ArithVariables::VarInfo::initialized() const {
141 : 43603000 : return d_var != ARITHVAR_SENTINEL;
142 : : }
143 : :
144 : 363258 : void ArithVariables::VarInfo::initialize(ArithVar v, Node n, bool aux){
145 [ - + ][ - + ]: 363258 : Assert(!initialized());
[ - - ]
146 [ - + ][ - + ]: 363258 : Assert(d_lb == NullConstraint);
[ - - ]
147 [ - + ][ - + ]: 363258 : Assert(d_ub == NullConstraint);
[ - - ]
148 [ - + ][ - + ]: 363258 : Assert(d_cmpAssignmentLB > 0);
[ - - ]
149 [ - + ][ - + ]: 363258 : Assert(d_cmpAssignmentUB < 0);
[ - - ]
150 : 363258 : d_var = v;
151 : 363258 : d_node = n;
152 : 363258 : d_auxiliary = aux;
153 : :
154 [ + + ]: 363258 : if(d_auxiliary){
155 : : //The type computation is not quite accurate for Rationals that are
156 : : //integral.
157 : : //We'll use the isIntegral check from the polynomial package instead.
158 : 194192 : Polynomial p = Polynomial::parsePolynomial(n);
159 [ + + ]: 194192 : d_type = p.isIntegral() ? ArithType::Integer : ArithType::Real;
160 : : }else{
161 [ + + ]: 169066 : d_type = n.getType().isInteger() ? ArithType::Integer : ArithType::Real;
162 : : }
163 : :
164 [ - + ][ - + ]: 363258 : Assert(initialized());
[ - - ]
165 : 363258 : }
166 : :
167 : 3943 : void ArithVariables::VarInfo::uninitialize(){
168 : 3943 : d_var = ARITHVAR_SENTINEL;
169 : 3943 : d_node = Node::null();
170 : 3943 : }
171 : :
172 : 11207900 : bool ArithVariables::VarInfo::setAssignment(const DeltaRational& a, BoundsInfo& prev){
173 [ - + ][ - + ]: 11207900 : Assert(initialized());
[ - - ]
174 : 11207900 : d_assignment = a;
175 [ + + ]: 11207900 : int cmpUB = (d_ub == NullConstraint) ? -1 :
176 : 2151570 : d_assignment.cmp(d_ub->getValue());
177 : :
178 [ + + ]: 11207900 : int cmpLB = (d_lb == NullConstraint) ? 1 :
179 : 2912920 : d_assignment.cmp(d_lb->getValue());
180 : :
181 [ + + ][ + + ]: 11733700 : bool lbChanged = cmpLB != d_cmpAssignmentLB &&
182 [ + + ]: 525786 : (cmpLB == 0 || d_cmpAssignmentLB == 0);
183 [ + + ][ + + ]: 11602200 : bool ubChanged = cmpUB != d_cmpAssignmentUB &&
184 [ + + ]: 394320 : (cmpUB == 0 || d_cmpAssignmentUB == 0);
185 : :
186 [ + + ][ + + ]: 11207900 : if(lbChanged || ubChanged){
187 : 1655550 : prev = boundsInfo();
188 : : }
189 : :
190 : 11207900 : d_cmpAssignmentUB = cmpUB;
191 : 11207900 : d_cmpAssignmentLB = cmpLB;
192 [ + + ][ + + ]: 11207900 : return lbChanged || ubChanged;
193 : : }
194 : :
195 : 3943 : void ArithVariables::releaseArithVar(ArithVar v){
196 : 3943 : VarInfo& vi = d_vars.get(v);
197 : :
198 : 3943 : size_t removed CVC5_UNUSED = d_nodeToArithVarMap.erase(vi.d_node);
199 [ - + ][ - + ]: 3943 : Assert(removed == 1);
[ - - ]
200 : :
201 : 3943 : vi.uninitialize();
202 : :
203 [ + - ]: 3943 : if(d_safeAssignment.isKey(v)){
204 : 3943 : d_safeAssignment.remove(v);
205 : : }
206 [ + - ]: 3943 : if(vi.canBeReclaimed()){
207 : 3943 : d_pool.push_back(v);
208 : : }else{
209 : 0 : d_released.push_back(v);
210 : : }
211 : 3943 : }
212 : :
213 : 8407350 : bool ArithVariables::VarInfo::setUpperBound(ConstraintP ub, BoundsInfo& prev){
214 [ - + ][ - + ]: 8407350 : Assert(initialized());
[ - - ]
215 : 8407350 : bool wasNull = d_ub == NullConstraint;
216 : 8407350 : bool isNull = ub == NullConstraint;
217 : :
218 [ + + ]: 8407350 : int cmpUB = isNull ? -1 : d_assignment.cmp(ub->getValue());
219 [ + + ]: 9349880 : bool ubChanged = (wasNull != isNull) ||
220 [ + + ][ + + ]: 942536 : (cmpUB != d_cmpAssignmentUB && (cmpUB == 0 || d_cmpAssignmentUB == 0));
[ + + ]
221 [ + + ]: 8407350 : if(ubChanged){
222 : 7993680 : prev = boundsInfo();
223 : : }
224 : 8407350 : d_ub = ub;
225 : 8407350 : d_cmpAssignmentUB = cmpUB;
226 : 8407350 : return ubChanged;
227 : : }
228 : :
229 : 8918940 : bool ArithVariables::VarInfo::setLowerBound(ConstraintP lb, BoundsInfo& prev){
230 [ - + ][ - + ]: 8918940 : Assert(initialized());
[ - - ]
231 : 8918940 : bool wasNull = d_lb == NullConstraint;
232 : 8918940 : bool isNull = lb == NullConstraint;
233 : :
234 [ + + ]: 8918940 : int cmpLB = isNull ? 1 : d_assignment.cmp(lb->getValue());
235 : :
236 [ + + ]: 10399500 : bool lbChanged = (wasNull != isNull) ||
237 [ + + ][ + + ]: 1480520 : (cmpLB != d_cmpAssignmentLB && (cmpLB == 0 || d_cmpAssignmentLB == 0));
[ + + ]
238 [ + + ]: 8918940 : if(lbChanged){
239 : 8128860 : prev = boundsInfo();
240 : : }
241 : 8918940 : d_lb = lb;
242 : 8918940 : d_cmpAssignmentLB = cmpLB;
243 : 8918940 : return lbChanged;
244 : : }
245 : :
246 : 142250000 : BoundCounts ArithVariables::VarInfo::atBoundCounts() const {
247 [ + + ]: 142250000 : uint32_t lbIndc = (d_cmpAssignmentLB == 0) ? 1 : 0;
248 [ + + ]: 142250000 : uint32_t ubIndc = (d_cmpAssignmentUB == 0) ? 1 : 0;
249 : 142250000 : return BoundCounts(lbIndc, ubIndc);
250 : : }
251 : :
252 : 127225000 : BoundCounts ArithVariables::VarInfo::hasBoundCounts() const {
253 [ + + ]: 127225000 : uint32_t lbIndc = (d_lb != NullConstraint) ? 1 : 0;
254 [ + + ]: 127225000 : uint32_t ubIndc = (d_ub != NullConstraint) ? 1 : 0;
255 : 127225000 : return BoundCounts(lbIndc, ubIndc);
256 : : }
257 : :
258 : 127225000 : BoundsInfo ArithVariables::VarInfo::boundsInfo() const{
259 : 127225000 : return BoundsInfo(atBoundCounts(), hasBoundCounts());
260 : : }
261 : :
262 : 3943 : bool ArithVariables::VarInfo::canBeReclaimed() const{
263 : 3943 : return d_pushCount == 0;
264 : : }
265 : :
266 : 0 : bool ArithVariables::canBeReleased(ArithVar v) const{
267 : 0 : return d_vars[v].canBeReclaimed();
268 : : }
269 : :
270 : 359333 : void ArithVariables::attemptToReclaimReleased(){
271 : 359333 : size_t readPos = 0, writePos = 0, N = d_released.size();
272 [ - + ]: 359333 : for(; readPos < N; ++readPos){
273 : 0 : ArithVar v = d_released[readPos];
274 [ - - ]: 0 : if(canBeReleased(v)){
275 : 0 : d_pool.push_back(v);
276 : : }else{
277 : 0 : d_released[writePos] = v;
278 : 0 : writePos++;
279 : : }
280 : : }
281 : 359333 : d_released.resize(writePos);
282 : 359333 : }
283 : :
284 : 363258 : ArithVar ArithVariables::allocateVariable(){
285 [ + + ]: 363258 : if(d_pool.empty()){
286 : 359333 : attemptToReclaimReleased();
287 : : }
288 : 363258 : bool reclaim = !d_pool.empty();
289 : :
290 : : ArithVar varX;
291 [ + + ]: 363258 : if(reclaim){
292 : 3925 : varX = d_pool.back();
293 : 3925 : d_pool.pop_back();
294 : : }else{
295 : 359333 : varX = d_numberOfVariables;
296 : 359333 : ++d_numberOfVariables;
297 : : }
298 : 363258 : d_vars.set(varX, VarInfo());
299 : 363258 : return varX;
300 : : }
301 : :
302 : :
303 : 140268 : const Rational& ArithVariables::getDelta(){
304 [ + + ]: 140268 : if(!d_deltaIsSafe){
305 : 223746 : Rational nextDelta = d_deltaComputingFunc();
306 : 111873 : setDelta(nextDelta);
307 : : }
308 [ - + ][ - + ]: 140268 : Assert(d_deltaIsSafe);
[ - - ]
309 : 140268 : return d_delta;
310 : : }
311 : :
312 : 209457 : bool ArithVariables::boundsAreEqual(ArithVar x) const{
313 [ + + ][ + + ]: 209457 : if(hasLowerBound(x) && hasUpperBound(x)){
[ + + ]
314 : 90523 : return getUpperBound(x) == getLowerBound(x);
315 : : }else{
316 : 118934 : return false;
317 : : }
318 : : }
319 : :
320 : :
321 : 0 : std::pair<ConstraintP, ConstraintP> ArithVariables::explainEqualBounds(ArithVar x) const{
322 : 0 : Assert(boundsAreEqual(x));
323 : :
324 : 0 : ConstraintP lb = getLowerBoundConstraint(x);
325 : 0 : ConstraintP ub = getUpperBoundConstraint(x);
326 [ - - ]: 0 : if(lb->isEquality()){
327 : 0 : return make_pair(lb, NullConstraint);
328 [ - - ]: 0 : }else if(ub->isEquality()){
329 : 0 : return make_pair(ub, NullConstraint);
330 : : }else{
331 : 0 : return make_pair(lb, ub);
332 : : }
333 : : }
334 : :
335 : 11013700 : void ArithVariables::setAssignment(ArithVar x, const DeltaRational& r){
336 [ + - ]: 22027400 : Trace("partial_model") << "pm: updating the assignment to" << x
337 : 11013700 : << " now " << r <<endl;
338 : 11013700 : VarInfo& vi = d_vars.get(x);
339 [ + + ]: 11013700 : if(!d_safeAssignment.isKey(x)){
340 : 6515900 : d_safeAssignment.set(x, vi.d_assignment);
341 : : }
342 : 11013700 : invalidateDelta();
343 : :
344 : 11013700 : BoundsInfo prev;
345 [ + + ]: 11013700 : if(vi.setAssignment(r, prev)){
346 : 1655550 : addToBoundQueue(x, prev);
347 : : }
348 : 11013700 : }
349 : :
350 : 194192 : void ArithVariables::setAssignment(ArithVar x, const DeltaRational& safe, const DeltaRational& r){
351 [ + - ]: 388384 : Trace("partial_model") << "pm: updating the assignment to" << x
352 : 194192 : << " now " << r <<endl;
353 [ + + ]: 194192 : if(safe == r){
354 [ - + ]: 192855 : if(d_safeAssignment.isKey(x)){
355 : 0 : d_safeAssignment.remove(x);
356 : : }
357 : : }else{
358 : 1337 : d_safeAssignment.set(x, safe);
359 : : }
360 : :
361 : 194192 : invalidateDelta();
362 : 194192 : VarInfo& vi = d_vars.get(x);
363 : 194192 : BoundsInfo prev;
364 [ - + ]: 194192 : if(vi.setAssignment(r, prev)){
365 : 0 : addToBoundQueue(x, prev);
366 : : }
367 : 194192 : }
368 : :
369 : 363258 : void ArithVariables::initialize(ArithVar x, Node n, bool aux){
370 : 363258 : VarInfo& vi = d_vars.get(x);
371 : 363258 : vi.initialize(x, n, aux);
372 : 363258 : d_nodeToArithVarMap[n] = x;
373 : 363258 : }
374 : :
375 : 363258 : ArithVar ArithVariables::allocate(Node n, bool aux){
376 : 363258 : ArithVar v = allocateVariable();
377 : 363258 : initialize(v, n, aux);
378 : 363258 : return v;
379 : : }
380 : :
381 : : // void ArithVariables::initialize(ArithVar x, const DeltaRational& r){
382 : : // Assert(x == d_mapSize);
383 : : // Assert(equalSizes());
384 : : // ++d_mapSize;
385 : :
386 : : // // Is worth mentioning that this is not strictly necessary, but this maintains the internal invariant
387 : : // // that when d_assignment is set this gets set.
388 : : // invalidateDelta();
389 : : // d_assignment.push_back( r );
390 : :
391 : : // d_boundRel.push_back(BetweenBounds);
392 : :
393 : : // d_ubc.push_back(NullConstraint);
394 : : // d_lbc.push_back(NullConstraint);
395 : : // }
396 : :
397 : : /** Must know that the bound exists both calling this! */
398 : 12773300 : const DeltaRational& ArithVariables::getUpperBound(ArithVar x) const {
399 [ - + ][ - + ]: 12773300 : Assert(inMaps(x));
[ - - ]
400 [ - + ][ - + ]: 12773300 : Assert(hasUpperBound(x));
[ - - ]
401 : :
402 : 12773300 : return getUpperBoundConstraint(x)->getValue();
403 : : }
404 : :
405 : 13621700 : const DeltaRational& ArithVariables::getLowerBound(ArithVar x) const {
406 [ - + ][ - + ]: 13621700 : Assert(inMaps(x));
[ - - ]
407 [ - + ][ - + ]: 13621700 : Assert(hasLowerBound(x));
[ - - ]
408 : :
409 : 13621700 : return getLowerBoundConstraint(x)->getValue();
410 : : }
411 : :
412 : 0 : const DeltaRational& ArithVariables::getSafeAssignment(ArithVar x) const{
413 : 0 : Assert(inMaps(x));
414 [ - - ]: 0 : if(d_safeAssignment.isKey(x)){
415 : 0 : return d_safeAssignment[x];
416 : : }else{
417 : 0 : return d_vars[x].d_assignment;
418 : : }
419 : : }
420 : :
421 : 1533750 : const DeltaRational& ArithVariables::getAssignment(ArithVar x, bool safe) const{
422 [ - + ][ - + ]: 1533750 : Assert(inMaps(x));
[ - - ]
423 [ + + ][ + + ]: 1533750 : if(safe && d_safeAssignment.isKey(x)){
[ + + ]
424 : 1383 : return d_safeAssignment[x];
425 : : }else{
426 : 1532360 : return d_vars[x].d_assignment;
427 : : }
428 : : }
429 : :
430 : 41698400 : const DeltaRational& ArithVariables::getAssignment(ArithVar x) const{
431 [ - + ][ - + ]: 41698400 : Assert(inMaps(x));
[ - - ]
432 : 41698400 : return d_vars[x].d_assignment;
433 : : }
434 : :
435 : :
436 : 4459560 : void ArithVariables::setLowerBoundConstraint(ConstraintP c){
437 [ - + ]: 4459560 : AssertArgument(c != NullConstraint, "Cannot set a lower bound to NullConstraint.");
438 [ + + ][ - + ]: 4459560 : AssertArgument(c->isEquality() || c->isLowerBound(),
[ - + ]
439 : : "Constraint type must be set to an equality or UpperBound.");
440 : 4459560 : ArithVar x = c->getVariable();
441 [ + - ]: 4459560 : Trace("partial_model") << "setLowerBoundConstraint(" << x << ":" << c << ")" << endl;
442 [ - + ][ - + ]: 4459560 : Assert(inMaps(x));
[ - - ]
443 [ - + ][ - + ]: 4459560 : Assert(greaterThanLowerBound(x, c->getValue()));
[ - - ]
444 : :
445 : 4459560 : invalidateDelta();
446 : 4459560 : VarInfo& vi = d_vars.get(x);
447 : 4459560 : pushLowerBound(vi);
448 : 4459560 : BoundsInfo prev;
449 [ + + ]: 4459560 : if(vi.setLowerBound(c, prev)){
450 : 4067820 : addToBoundQueue(x, prev);
451 : : }
452 : 4459560 : }
453 : :
454 : 4203720 : void ArithVariables::setUpperBoundConstraint(ConstraintP c){
455 [ - + ]: 4203720 : AssertArgument(c != NullConstraint, "Cannot set a upper bound to NullConstraint.");
456 [ + + ][ - + ]: 4203720 : AssertArgument(c->isEquality() || c->isUpperBound(),
[ - + ]
457 : : "Constraint type must be set to an equality or UpperBound.");
458 : :
459 : 4203720 : ArithVar x = c->getVariable();
460 [ + - ]: 4203720 : Trace("partial_model") << "setUpperBoundConstraint(" << x << ":" << c << ")" << endl;
461 [ - + ][ - + ]: 4203720 : Assert(inMaps(x));
[ - - ]
462 [ - + ][ - + ]: 4203720 : Assert(lessThanUpperBound(x, c->getValue()));
[ - - ]
463 : :
464 : 4203720 : invalidateDelta();
465 : 4203720 : VarInfo& vi = d_vars.get(x);
466 : 4203720 : pushUpperBound(vi);
467 : 4203720 : BoundsInfo prev;
468 [ + + ]: 4203720 : if(vi.setUpperBound(c, prev)){
469 : 3998510 : addToBoundQueue(x, prev);
470 : : }
471 : 4203720 : }
472 : :
473 : 15652800 : int ArithVariables::cmpToLowerBound(ArithVar x, const DeltaRational& c) const{
474 [ + + ]: 15652800 : if(!hasLowerBound(x)){
475 : : // l = -\intfy
476 : : // ? c < -\infty |- _|_
477 : 10606800 : return 1;
478 : : }else{
479 : 5046030 : return c.cmp(getLowerBound(x));
480 : : }
481 : : }
482 : :
483 : 14366600 : int ArithVariables::cmpToUpperBound(ArithVar x, const DeltaRational& c) const{
484 [ + + ]: 14366600 : if(!hasUpperBound(x)){
485 : : //u = \intfy
486 : : // ? c > \infty |- _|_
487 : 10169300 : return -1;
488 : : }else{
489 : 4197310 : return c.cmp(getUpperBound(x));
490 : : }
491 : : }
492 : :
493 : 0 : bool ArithVariables::equalsLowerBound(ArithVar x, const DeltaRational& c){
494 [ - - ]: 0 : if(!hasLowerBound(x)){
495 : 0 : return false;
496 : : }else{
497 : 0 : return c == getLowerBound(x);
498 : : }
499 : : }
500 : 0 : bool ArithVariables::equalsUpperBound(ArithVar x, const DeltaRational& c){
501 [ - - ]: 0 : if(!hasUpperBound(x)){
502 : 0 : return false;
503 : : }else{
504 : 0 : return c == getUpperBound(x);
505 : : }
506 : : }
507 : :
508 : 4395400 : bool ArithVariables::hasEitherBound(ArithVar x) const{
509 [ + + ][ + + ]: 4395400 : return hasLowerBound(x) || hasUpperBound(x);
510 : : }
511 : :
512 : 2612970 : bool ArithVariables::strictlyBelowUpperBound(ArithVar x) const{
513 : 2612970 : return d_vars[x].d_cmpAssignmentUB < 0;
514 : : }
515 : :
516 : 4741740 : bool ArithVariables::strictlyAboveLowerBound(ArithVar x) const{
517 : 4741740 : return d_vars[x].d_cmpAssignmentLB > 0;
518 : : }
519 : :
520 : 30317500 : bool ArithVariables::assignmentIsConsistent(ArithVar x) const{
521 : : return
522 [ + + ]: 58984300 : d_vars[x].d_cmpAssignmentLB >= 0 &&
523 [ + + ]: 58984300 : d_vars[x].d_cmpAssignmentUB <= 0;
524 : : }
525 : :
526 : :
527 : 3531890 : void ArithVariables::clearSafeAssignments(bool revert){
528 : :
529 [ + + ][ - + ]: 3531890 : if(revert && !d_safeAssignment.empty()){
[ - + ]
530 : 0 : invalidateDelta();
531 : : }
532 : :
533 [ + + ]: 10045200 : while(!d_safeAssignment.empty()){
534 : 6513290 : ArithVar atBack = d_safeAssignment.back();
535 [ - + ]: 6513290 : if(revert){
536 : 0 : VarInfo& vi = d_vars.get(atBack);
537 : 0 : BoundsInfo prev;
538 [ - - ]: 0 : if(vi.setAssignment(d_safeAssignment[atBack], prev)){
539 : 0 : addToBoundQueue(atBack, prev);
540 : : }
541 : : }
542 : 6513290 : d_safeAssignment.pop_back();
543 : : }
544 : 3531890 : }
545 : :
546 : 86258 : void ArithVariables::revertAssignmentChanges(){
547 : 86258 : clearSafeAssignments(true);
548 : 86258 : }
549 : 3445630 : void ArithVariables::commitAssignmentChanges(){
550 : 3445630 : clearSafeAssignments(false);
551 : 3445630 : }
552 : :
553 : 2384220 : bool ArithVariables::lowerBoundIsZero(ArithVar x){
554 [ + + ][ + + ]: 2384220 : return hasLowerBound(x) && getLowerBound(x).sgn() == 0;
555 : : }
556 : :
557 : 2469860 : bool ArithVariables::upperBoundIsZero(ArithVar x){
558 [ + + ][ + + ]: 2469860 : return hasUpperBound(x) && getUpperBound(x).sgn() == 0;
559 : : }
560 : :
561 : 0 : void ArithVariables::printEntireModel(std::ostream& out) const{
562 : 0 : out << "---Printing Model ---" << std::endl;
563 [ - - ]: 0 : for(var_iterator i = var_begin(), iend = var_end(); i != iend; ++i){
564 : 0 : printModel(*i, out);
565 : : }
566 : 0 : out << "---Done Model ---" << std::endl;
567 : 0 : }
568 : :
569 : 0 : void ArithVariables::printModel(ArithVar x, std::ostream& out) const{
570 : 0 : out << "model" << x << ": "
571 : 0 : << asNode(x) << " "
572 : 0 : << getAssignment(x) << " ";
573 [ - - ]: 0 : if(!hasLowerBound(x)){
574 : 0 : out << "no lb ";
575 : : }else{
576 : 0 : out << getLowerBound(x) << " ";
577 : 0 : out << getLowerBoundConstraint(x) << " ";
578 : : }
579 [ - - ]: 0 : if(!hasUpperBound(x)){
580 : 0 : out << "no ub ";
581 : : }else{
582 : 0 : out << getUpperBound(x) << " ";
583 : 0 : out << getUpperBoundConstraint(x) << " ";
584 : : }
585 : :
586 [ - - ][ - - ]: 0 : if(isInteger(x) && !integralAssignment(x)){
[ - - ]
587 : 0 : out << "(not an integer)" << endl;
588 : : }
589 : 0 : out << endl;
590 : 0 : }
591 : :
592 : 0 : void ArithVariables::printModel(ArithVar x) const{
593 [ - - ]: 0 : printModel(x, Trace("model"));
594 : 0 : }
595 : :
596 : 4203720 : void ArithVariables::pushUpperBound(VarInfo& vi){
597 : 4203720 : ++vi.d_pushCount;
598 : 4203720 : d_ubRevertHistory.push_back(make_pair(vi.d_var, vi.d_ub));
599 : 4203720 : }
600 : 4459560 : void ArithVariables::pushLowerBound(VarInfo& vi){
601 : 4459560 : ++vi.d_pushCount;
602 : 4459560 : d_lbRevertHistory.push_back(make_pair(vi.d_var, vi.d_lb));
603 : 4459560 : }
604 : :
605 : 4203620 : void ArithVariables::popUpperBound(AVCPair* c){
606 : 4203620 : ArithVar x = c->first;
607 : 4203620 : VarInfo& vi = d_vars.get(x);
608 : 4203620 : BoundsInfo prev;
609 [ + + ]: 4203620 : if(vi.setUpperBound(c->second, prev)){
610 : 3995170 : addToBoundQueue(x, prev);
611 : : }
612 : 4203620 : --vi.d_pushCount;
613 : 4203620 : }
614 : :
615 : 4459380 : void ArithVariables::popLowerBound(AVCPair* c){
616 : 4459380 : ArithVar x = c->first;
617 : 4459380 : VarInfo& vi = d_vars.get(x);
618 : 4459380 : BoundsInfo prev;
619 [ + + ]: 4459380 : if(vi.setLowerBound(c->second, prev)){
620 : 4061040 : addToBoundQueue(x, prev);
621 : : }
622 : 4459380 : --vi.d_pushCount;
623 : 4459380 : }
624 : :
625 : 17778100 : void ArithVariables::addToBoundQueue(ArithVar v, const BoundsInfo& prev){
626 [ + + ][ + + ]: 17778100 : if(d_enqueueingBoundCounts && !d_boundsQueue.isKey(v)){
[ + + ]
627 : 10189500 : d_boundsQueue.set(v, prev);
628 : : }
629 : 17778100 : }
630 : :
631 : 989602 : BoundsInfo ArithVariables::selectBoundsInfo(ArithVar v, bool old) const {
632 [ + - ][ + + ]: 989602 : if(old && d_boundsQueue.isKey(v)){
[ + + ]
633 : 22091 : return d_boundsQueue[v];
634 : : }else{
635 : 967511 : return boundsInfo(v);
636 : : }
637 : : }
638 : :
639 : 34988700 : bool ArithVariables::boundsQueueEmpty() const {
640 : 34988700 : return d_boundsQueue.empty();
641 : : }
642 : :
643 : 15232000 : void ArithVariables::processBoundsQueue(BoundUpdateCallback& changed){
644 [ + + ]: 15232000 : while(!boundsQueueEmpty()){
645 : 9977130 : ArithVar v = d_boundsQueue.back();
646 : 9977130 : BoundsInfo prev = d_boundsQueue[v];
647 : 9977130 : d_boundsQueue.pop_back();
648 : 9977130 : BoundsInfo curr = boundsInfo(v);
649 [ + + ]: 9977130 : if(prev != curr){
650 : 9588610 : changed(v, prev);
651 : : }
652 : : }
653 : 5254850 : }
654 : :
655 : 20316900 : void ArithVariables::invalidateDelta() {
656 : 20316900 : d_deltaIsSafe = false;
657 : 20316900 : }
658 : :
659 : 111873 : void ArithVariables::setDelta(const Rational& d){
660 : 111873 : d_delta = d;
661 : 111873 : d_deltaIsSafe = true;
662 : 111873 : }
663 : :
664 : 3296570 : void ArithVariables::startQueueingBoundCounts(){
665 : 3296570 : d_enqueueingBoundCounts = true;
666 : 3296570 : }
667 : 3296570 : void ArithVariables::stopQueueingBoundCounts(){
668 : 3296570 : d_enqueueingBoundCounts = false;
669 : 3296570 : }
670 : :
671 : 78290400 : bool ArithVariables::inMaps(ArithVar x) const{
672 : 78290400 : return x < getNumberOfVariables();
673 : : }
674 : :
675 : 50287 : ArithVariables::LowerBoundCleanUp::LowerBoundCleanUp(ArithVariables* pm)
676 : 50287 : : d_pm(pm)
677 : 50287 : {}
678 : 4459380 : void ArithVariables::LowerBoundCleanUp::operator()(AVCPair& p)
679 : : {
680 : 4459380 : d_pm->popLowerBound(&p);
681 : 4459380 : }
682 : :
683 : 50287 : ArithVariables::UpperBoundCleanUp::UpperBoundCleanUp(ArithVariables* pm)
684 : 50287 : : d_pm(pm)
685 : 50287 : {}
686 : 4203620 : void ArithVariables::UpperBoundCleanUp::operator()(AVCPair& p)
687 : : {
688 : 4203620 : d_pm->popUpperBound(&p);
689 : 4203620 : }
690 : :
691 : : } // namespace arith
692 : : } // namespace theory
693 : : } // namespace cvc5::internal
|
