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 "theory/arith/linear/partial_model.h"
17 : :
18 : : #include "base/output.h"
19 : : #include "theory/arith/linear/constraint.h"
20 : : #include "theory/arith/linear/normal_form.h"
21 : :
22 : : using namespace std;
23 : :
24 : : namespace cvc5::internal {
25 : : namespace theory {
26 : : namespace arith::linear {
27 : :
28 : 28663 : ArithVariables::ArithVariables(context::Context* c,
29 : 28663 : DeltaComputeCallback deltaComputingFunc)
30 : 28663 : : d_vars(),
31 : 28663 : d_safeAssignment(),
32 : 28663 : d_numberOfVariables(0),
33 : 28663 : d_pool(),
34 : 28663 : d_released(),
35 : 28663 : d_nodeToArithVarMap(),
36 : 28663 : d_boundsQueue(),
37 : 28663 : d_enqueueingBoundCounts(true),
38 : 28663 : d_lbRevertHistory(c, true, LowerBoundCleanUp(this)),
39 : 28663 : d_ubRevertHistory(c, true, UpperBoundCleanUp(this)),
40 : 28663 : d_deltaIsSafe(false),
41 : 28663 : d_delta(-1, 1),
42 : 28663 : d_deltaComputingFunc(deltaComputingFunc)
43 : : {
44 : 28663 : }
45 : :
46 : 78417712 : ArithVar ArithVariables::getNumberOfVariables() const
47 : : {
48 : 78417712 : return d_numberOfVariables;
49 : : }
50 : :
51 : 13274234 : bool ArithVariables::hasArithVar(TNode x) const
52 : : {
53 : 13274234 : return d_nodeToArithVarMap.find(x) != d_nodeToArithVarMap.end();
54 : : }
55 : :
56 : 29784084 : bool ArithVariables::hasNode(ArithVar a) const { return d_vars.isKey(a); }
57 : :
58 : 5544103 : ArithVar ArithVariables::asArithVar(TNode x) const
59 : : {
60 [ - + ][ - + ]: 5544103 : Assert(hasArithVar(x));
[ - - ]
61 [ - + ][ - + ]: 5544103 : Assert((d_nodeToArithVarMap.find(x))->second <= ARITHVAR_SENTINEL);
[ - - ]
62 : 5544103 : return (d_nodeToArithVarMap.find(x))->second;
63 : : }
64 : :
65 : 19172811 : Node ArithVariables::asNode(ArithVar a) const
66 : : {
67 [ - + ][ - + ]: 19172811 : Assert(hasNode(a));
[ - - ]
68 : 19172811 : return d_vars[a].d_node;
69 : : }
70 : :
71 : 0 : ArithVariables::var_iterator::var_iterator() : d_vars(nullptr), d_wrapped() {}
72 : :
73 : 462674 : ArithVariables::var_iterator::var_iterator(const VarInfoVec* vars,
74 : 462674 : VarInfoVec::const_iterator ci)
75 : 462674 : : d_vars(vars), d_wrapped(ci)
76 : : {
77 : 462674 : nextInitialized();
78 : 462674 : }
79 : :
80 : 15225162 : ArithVariables::var_iterator& ArithVariables::var_iterator::operator++()
81 : : {
82 : 15225162 : ++d_wrapped;
83 : 15225162 : nextInitialized();
84 : 15225162 : return *this;
85 : : }
86 : 0 : bool ArithVariables::var_iterator::operator==(
87 : : const ArithVariables::var_iterator& other) const
88 : : {
89 : 0 : return d_wrapped == other.d_wrapped;
90 : : }
91 : 15456499 : bool ArithVariables::var_iterator::operator!=(
92 : : const ArithVariables::var_iterator& other) const
93 : : {
94 : 15456499 : return d_wrapped != other.d_wrapped;
95 : : }
96 : 15225162 : ArithVar ArithVariables::var_iterator::operator*() const { return *d_wrapped; }
97 : :
98 : 15687836 : void ArithVariables::var_iterator::nextInitialized()
99 : : {
100 : 15687836 : VarInfoVec::const_iterator end = d_vars->end();
101 [ + + ][ + + ]: 15687986 : while (d_wrapped != end && !((*d_vars)[*d_wrapped].initialized()))
[ + + ]
102 : : {
103 : 150 : ++d_wrapped;
104 : : }
105 : 15687836 : }
106 : :
107 : 231337 : ArithVariables::var_iterator ArithVariables::var_begin() const
108 : : {
109 : 231337 : return var_iterator(&d_vars, d_vars.begin());
110 : : }
111 : :
112 : 231337 : ArithVariables::var_iterator ArithVariables::var_end() const
113 : : {
114 : 231337 : return var_iterator(&d_vars, d_vars.end());
115 : : }
116 : 38152959 : bool ArithVariables::isInteger(ArithVar x) const
117 : : {
118 : 38152959 : return d_vars[x].d_type >= ArithType::Integer;
119 : : }
120 : :
121 : : /** Is the assignment to x integral? */
122 : 3375260 : bool ArithVariables::integralAssignment(ArithVar x) const
123 : : {
124 : 3375260 : return getAssignment(x).isIntegral();
125 : : }
126 : 15411015 : bool ArithVariables::isAuxiliary(ArithVar x) const
127 : : {
128 : 15411015 : return d_vars[x].d_auxiliary;
129 : : }
130 : :
131 : 7842885 : bool ArithVariables::isIntegerInput(ArithVar x) const
132 : : {
133 [ + + ][ + + ]: 7842885 : return isInteger(x) && !isAuxiliary(x);
134 : : }
135 : :
136 : 708404 : ArithVariables::VarInfo::VarInfo()
137 : 708404 : : d_var(ARITHVAR_SENTINEL),
138 : 708404 : d_assignment(0),
139 : 708404 : d_lb(NullConstraint),
140 : 708404 : d_ub(NullConstraint),
141 : 708404 : d_cmpAssignmentLB(1),
142 : 708404 : d_cmpAssignmentUB(-1),
143 : 708404 : d_pushCount(0),
144 : 708404 : d_type(ArithType::Unset),
145 : 708404 : d_node(Node::null()),
146 : 708404 : d_auxiliary(false)
147 : : {
148 : 708404 : }
149 : :
150 : 42845891 : bool ArithVariables::VarInfo::initialized() const
151 : : {
152 : 42845891 : return d_var != ARITHVAR_SENTINEL;
153 : : }
154 : :
155 : 356241 : void ArithVariables::VarInfo::initialize(ArithVar v, Node n, bool aux)
156 : : {
157 [ - + ][ - + ]: 356241 : Assert(!initialized());
[ - - ]
158 [ - + ][ - + ]: 356241 : Assert(d_lb == NullConstraint);
[ - - ]
159 [ - + ][ - + ]: 356241 : Assert(d_ub == NullConstraint);
[ - - ]
160 [ - + ][ - + ]: 356241 : Assert(d_cmpAssignmentLB > 0);
[ - - ]
161 [ - + ][ - + ]: 356241 : Assert(d_cmpAssignmentUB < 0);
[ - - ]
162 : 356241 : d_var = v;
163 : 356241 : d_node = n;
164 : 356241 : d_auxiliary = aux;
165 : :
166 [ + + ]: 356241 : if (d_auxiliary)
167 : : {
168 : : // The type computation is not quite accurate for Rationals that are
169 : : // integral.
170 : : // We'll use the isIntegral check from the polynomial package instead.
171 : 193523 : Polynomial p = Polynomial::parsePolynomial(n);
172 [ + + ]: 193523 : d_type = p.isIntegral() ? ArithType::Integer : ArithType::Real;
173 : 193523 : }
174 : : else
175 : : {
176 [ + + ]: 162718 : d_type = n.getType().isInteger() ? ArithType::Integer : ArithType::Real;
177 : : }
178 : :
179 [ - + ][ - + ]: 356241 : Assert(initialized());
[ - - ]
180 : 356241 : }
181 : :
182 : 4096 : void ArithVariables::VarInfo::uninitialize()
183 : : {
184 : 4096 : d_var = ARITHVAR_SENTINEL;
185 : 4096 : d_node = Node::null();
186 : 4096 : }
187 : :
188 : 10480335 : bool ArithVariables::VarInfo::setAssignment(const DeltaRational& a,
189 : : BoundsInfo& prev)
190 : : {
191 [ - + ][ - + ]: 10480335 : Assert(initialized());
[ - - ]
192 : 10480335 : d_assignment = a;
193 : : int cmpUB =
194 [ + + ]: 10480335 : (d_ub == NullConstraint) ? -1 : d_assignment.cmp(d_ub->getValue());
195 : :
196 [ + + ]: 10480335 : int cmpLB = (d_lb == NullConstraint) ? 1 : d_assignment.cmp(d_lb->getValue());
197 : :
198 : 10480335 : bool lbChanged =
199 [ + + ][ + + ]: 10480335 : cmpLB != d_cmpAssignmentLB && (cmpLB == 0 || d_cmpAssignmentLB == 0);
[ + + ]
200 : 10480335 : bool ubChanged =
201 [ + + ][ + + ]: 10480335 : cmpUB != d_cmpAssignmentUB && (cmpUB == 0 || d_cmpAssignmentUB == 0);
[ + + ]
202 : :
203 [ + + ][ + + ]: 10480335 : if (lbChanged || ubChanged)
204 : : {
205 : 1485899 : prev = boundsInfo();
206 : : }
207 : :
208 : 10480335 : d_cmpAssignmentUB = cmpUB;
209 : 10480335 : d_cmpAssignmentLB = cmpLB;
210 [ + + ][ + + ]: 10480335 : return lbChanged || ubChanged;
211 : : }
212 : :
213 : 4096 : void ArithVariables::releaseArithVar(ArithVar v)
214 : : {
215 : 4096 : VarInfo& vi = d_vars.get(v);
216 : :
217 : 4096 : size_t removed CVC5_UNUSED = d_nodeToArithVarMap.erase(vi.d_node);
218 [ - + ][ - + ]: 4096 : Assert(removed == 1);
[ - - ]
219 : :
220 : 4096 : vi.uninitialize();
221 : :
222 [ + - ]: 4096 : if (d_safeAssignment.isKey(v))
223 : : {
224 : 4096 : d_safeAssignment.remove(v);
225 : : }
226 [ + - ]: 4096 : if (vi.canBeReclaimed())
227 : : {
228 : 4096 : d_pool.push_back(v);
229 : : }
230 : : else
231 : : {
232 : 0 : d_released.push_back(v);
233 : : }
234 : 4096 : }
235 : :
236 : 8000834 : bool ArithVariables::VarInfo::setUpperBound(ConstraintP ub, BoundsInfo& prev)
237 : : {
238 [ - + ][ - + ]: 8000834 : Assert(initialized());
[ - - ]
239 : 8000834 : bool wasNull = d_ub == NullConstraint;
240 : 8000834 : bool isNull = ub == NullConstraint;
241 : :
242 [ + + ]: 8000834 : int cmpUB = isNull ? -1 : d_assignment.cmp(ub->getValue());
243 : 8000834 : bool ubChanged =
244 : : (wasNull != isNull)
245 [ + + ][ + + ]: 8000834 : || (cmpUB != d_cmpAssignmentUB && (cmpUB == 0 || d_cmpAssignmentUB == 0));
[ + + ][ + + ]
246 [ + + ]: 8000834 : if (ubChanged)
247 : : {
248 : 7600526 : prev = boundsInfo();
249 : : }
250 : 8000834 : d_ub = ub;
251 : 8000834 : d_cmpAssignmentUB = cmpUB;
252 : 8000834 : return ubChanged;
253 : : }
254 : :
255 : 8426924 : bool ArithVariables::VarInfo::setLowerBound(ConstraintP lb, BoundsInfo& prev)
256 : : {
257 [ - + ][ - + ]: 8426924 : Assert(initialized());
[ - - ]
258 : 8426924 : bool wasNull = d_lb == NullConstraint;
259 : 8426924 : bool isNull = lb == NullConstraint;
260 : :
261 [ + + ]: 8426924 : int cmpLB = isNull ? 1 : d_assignment.cmp(lb->getValue());
262 : :
263 : 8426924 : bool lbChanged =
264 : : (wasNull != isNull)
265 [ + + ][ + + ]: 8426924 : || (cmpLB != d_cmpAssignmentLB && (cmpLB == 0 || d_cmpAssignmentLB == 0));
[ + + ][ + + ]
266 [ + + ]: 8426924 : if (lbChanged)
267 : : {
268 : 7618933 : prev = boundsInfo();
269 : : }
270 : 8426924 : d_lb = lb;
271 : 8426924 : d_cmpAssignmentLB = cmpLB;
272 : 8426924 : return lbChanged;
273 : : }
274 : :
275 : 122108749 : BoundCounts ArithVariables::VarInfo::atBoundCounts() const
276 : : {
277 [ + + ]: 122108749 : uint32_t lbIndc = (d_cmpAssignmentLB == 0) ? 1 : 0;
278 [ + + ]: 122108749 : uint32_t ubIndc = (d_cmpAssignmentUB == 0) ? 1 : 0;
279 : 122108749 : return BoundCounts(lbIndc, ubIndc);
280 : : }
281 : :
282 : 107847907 : BoundCounts ArithVariables::VarInfo::hasBoundCounts() const
283 : : {
284 [ + + ]: 107847907 : uint32_t lbIndc = (d_lb != NullConstraint) ? 1 : 0;
285 [ + + ]: 107847907 : uint32_t ubIndc = (d_ub != NullConstraint) ? 1 : 0;
286 : 107847907 : return BoundCounts(lbIndc, ubIndc);
287 : : }
288 : :
289 : 107847907 : BoundsInfo ArithVariables::VarInfo::boundsInfo() const
290 : : {
291 : 107847907 : return BoundsInfo(atBoundCounts(), hasBoundCounts());
292 : : }
293 : :
294 : 4096 : bool ArithVariables::VarInfo::canBeReclaimed() const
295 : : {
296 : 4096 : return d_pushCount == 0;
297 : : }
298 : :
299 : 0 : bool ArithVariables::canBeReleased(ArithVar v) const
300 : : {
301 : 0 : return d_vars[v].canBeReclaimed();
302 : : }
303 : :
304 : 352163 : void ArithVariables::attemptToReclaimReleased()
305 : : {
306 : 352163 : size_t readPos = 0, writePos = 0, N = d_released.size();
307 [ - + ]: 352163 : for (; readPos < N; ++readPos)
308 : : {
309 : 0 : ArithVar v = d_released[readPos];
310 [ - - ]: 0 : if (canBeReleased(v))
311 : : {
312 : 0 : d_pool.push_back(v);
313 : : }
314 : : else
315 : : {
316 : 0 : d_released[writePos] = v;
317 : 0 : writePos++;
318 : : }
319 : : }
320 : 352163 : d_released.resize(writePos);
321 : 352163 : }
322 : :
323 : 356241 : ArithVar ArithVariables::allocateVariable()
324 : : {
325 [ + + ]: 356241 : if (d_pool.empty())
326 : : {
327 : 352163 : attemptToReclaimReleased();
328 : : }
329 : 356241 : bool reclaim = !d_pool.empty();
330 : :
331 : : ArithVar varX;
332 [ + + ]: 356241 : if (reclaim)
333 : : {
334 : 4078 : varX = d_pool.back();
335 : 4078 : d_pool.pop_back();
336 : : }
337 : : else
338 : : {
339 : 352163 : varX = d_numberOfVariables;
340 : 352163 : ++d_numberOfVariables;
341 : : }
342 : 356241 : d_vars.set(varX, VarInfo());
343 : 356241 : return varX;
344 : : }
345 : :
346 : 128725 : const Rational& ArithVariables::getDelta()
347 : : {
348 [ + + ]: 128725 : if (!d_deltaIsSafe)
349 : : {
350 : 100273 : Rational nextDelta = d_deltaComputingFunc();
351 : 100273 : setDelta(nextDelta);
352 : 100273 : }
353 [ - + ][ - + ]: 128725 : Assert(d_deltaIsSafe);
[ - - ]
354 : 128725 : return d_delta;
355 : : }
356 : :
357 : 249800 : bool ArithVariables::boundsAreEqual(ArithVar x) const
358 : : {
359 [ + + ][ + + ]: 249800 : if (hasLowerBound(x) && hasUpperBound(x))
[ + + ]
360 : : {
361 : 113118 : return getUpperBound(x) == getLowerBound(x);
362 : : }
363 : : else
364 : : {
365 : 136682 : return false;
366 : : }
367 : : }
368 : :
369 : 0 : std::pair<ConstraintP, ConstraintP> ArithVariables::explainEqualBounds(
370 : : ArithVar x) const
371 : : {
372 : 0 : Assert(boundsAreEqual(x));
373 : :
374 : 0 : ConstraintP lb = getLowerBoundConstraint(x);
375 : 0 : ConstraintP ub = getUpperBoundConstraint(x);
376 [ - - ]: 0 : if (lb->isEquality())
377 : : {
378 : 0 : return make_pair(lb, NullConstraint);
379 : : }
380 [ - - ]: 0 : else if (ub->isEquality())
381 : : {
382 : 0 : return make_pair(ub, NullConstraint);
383 : : }
384 : : else
385 : : {
386 : 0 : return make_pair(lb, ub);
387 : : }
388 : : }
389 : :
390 : 10286812 : void ArithVariables::setAssignment(ArithVar x, const DeltaRational& r)
391 : : {
392 [ + - ]: 20573624 : Trace("partial_model") << "pm: updating the assignment to" << x << " now "
393 : 10286812 : << r << endl;
394 : 10286812 : VarInfo& vi = d_vars.get(x);
395 [ + + ]: 10286812 : if (!d_safeAssignment.isKey(x))
396 : : {
397 : 6087601 : d_safeAssignment.set(x, vi.d_assignment);
398 : : }
399 : 10286812 : invalidateDelta();
400 : :
401 : 10286812 : BoundsInfo prev;
402 [ + + ]: 10286812 : if (vi.setAssignment(r, prev))
403 : : {
404 : 1485899 : addToBoundQueue(x, prev);
405 : : }
406 : 10286812 : }
407 : :
408 : 193523 : void ArithVariables::setAssignment(ArithVar x,
409 : : const DeltaRational& safe,
410 : : const DeltaRational& r)
411 : : {
412 [ + - ]: 387046 : Trace("partial_model") << "pm: updating the assignment to" << x << " now "
413 : 193523 : << r << endl;
414 [ + + ]: 193523 : if (safe == r)
415 : : {
416 [ - + ]: 191989 : if (d_safeAssignment.isKey(x))
417 : : {
418 : 0 : d_safeAssignment.remove(x);
419 : : }
420 : : }
421 : : else
422 : : {
423 : 1534 : d_safeAssignment.set(x, safe);
424 : : }
425 : :
426 : 193523 : invalidateDelta();
427 : 193523 : VarInfo& vi = d_vars.get(x);
428 : 193523 : BoundsInfo prev;
429 [ - + ]: 193523 : if (vi.setAssignment(r, prev))
430 : : {
431 : 0 : addToBoundQueue(x, prev);
432 : : }
433 : 193523 : }
434 : :
435 : 356241 : void ArithVariables::initialize(ArithVar x, Node n, bool aux)
436 : : {
437 : 356241 : VarInfo& vi = d_vars.get(x);
438 : 356241 : vi.initialize(x, n, aux);
439 : 356241 : d_nodeToArithVarMap[n] = x;
440 : 356241 : }
441 : :
442 : 356241 : ArithVar ArithVariables::allocate(Node n, bool aux)
443 : : {
444 : 356241 : ArithVar v = allocateVariable();
445 : 356241 : initialize(v, n, aux);
446 : 356241 : return v;
447 : : }
448 : :
449 : : // void ArithVariables::initialize(ArithVar x, const DeltaRational& r){
450 : : // Assert(x == d_mapSize);
451 : : // Assert(equalSizes());
452 : : // ++d_mapSize;
453 : :
454 : : // // Is worth mentioning that this is not strictly necessary, but this
455 : : // maintains the internal invariant
456 : : // // that when d_assignment is set this gets set.
457 : : // invalidateDelta();
458 : : // d_assignment.push_back( r );
459 : :
460 : : // d_boundRel.push_back(BetweenBounds);
461 : :
462 : : // d_ubc.push_back(NullConstraint);
463 : : // d_lbc.push_back(NullConstraint);
464 : : // }
465 : :
466 : : /** Must know that the bound exists both calling this! */
467 : 12518339 : const DeltaRational& ArithVariables::getUpperBound(ArithVar x) const
468 : : {
469 [ - + ][ - + ]: 12518339 : Assert(inMaps(x));
[ - - ]
470 [ - + ][ - + ]: 12518339 : Assert(hasUpperBound(x));
[ - - ]
471 : :
472 : 12518339 : return getUpperBoundConstraint(x)->getValue();
473 : : }
474 : :
475 : 13504524 : const DeltaRational& ArithVariables::getLowerBound(ArithVar x) const
476 : : {
477 [ - + ][ - + ]: 13504524 : Assert(inMaps(x));
[ - - ]
478 [ - + ][ - + ]: 13504524 : Assert(hasLowerBound(x));
[ - - ]
479 : :
480 : 13504524 : return getLowerBoundConstraint(x)->getValue();
481 : : }
482 : :
483 : 0 : const DeltaRational& ArithVariables::getSafeAssignment(ArithVar x) const
484 : : {
485 : 0 : Assert(inMaps(x));
486 [ - - ]: 0 : if (d_safeAssignment.isKey(x))
487 : : {
488 : 0 : return d_safeAssignment[x];
489 : : }
490 : : else
491 : : {
492 : 0 : return d_vars[x].d_assignment;
493 : : }
494 : : }
495 : :
496 : 1566604 : const DeltaRational& ArithVariables::getAssignment(ArithVar x, bool safe) const
497 : : {
498 [ - + ][ - + ]: 1566604 : Assert(inMaps(x));
[ - - ]
499 [ + + ][ + + ]: 1566604 : if (safe && d_safeAssignment.isKey(x))
[ + + ]
500 : : {
501 : 1605 : return d_safeAssignment[x];
502 : : }
503 : : else
504 : : {
505 : 1564999 : return d_vars[x].d_assignment;
506 : : }
507 : : }
508 : :
509 : 41764897 : const DeltaRational& ArithVariables::getAssignment(ArithVar x) const
510 : : {
511 [ - + ][ - + ]: 41764897 : Assert(inMaps(x));
[ - - ]
512 : 41764897 : return d_vars[x].d_assignment;
513 : : }
514 : :
515 : 4213462 : void ArithVariables::setLowerBoundConstraint(ConstraintP c)
516 : : {
517 [ - + ]: 4213462 : AssertArgument(c != NullConstraint,
518 : : "Cannot set a lower bound to NullConstraint.");
519 [ + + ][ - + ]: 4213462 : AssertArgument(c->isEquality() || c->isLowerBound(),
[ - + ]
520 : : "Constraint type must be set to an equality or UpperBound.");
521 : 4213462 : ArithVar x = c->getVariable();
522 [ + - ]: 8426924 : Trace("partial_model") << "setLowerBoundConstraint(" << x << ":" << c << ")"
523 : 4213462 : << endl;
524 [ - + ][ - + ]: 4213462 : Assert(inMaps(x));
[ - - ]
525 [ - + ][ - + ]: 4213462 : Assert(greaterThanLowerBound(x, c->getValue()));
[ - - ]
526 : :
527 : 4213462 : invalidateDelta();
528 : 4213462 : VarInfo& vi = d_vars.get(x);
529 : 4213462 : pushLowerBound(vi);
530 : 4213462 : BoundsInfo prev;
531 [ + + ]: 4213462 : if (vi.setLowerBound(c, prev))
532 : : {
533 : 3812730 : addToBoundQueue(x, prev);
534 : : }
535 : 4213462 : }
536 : :
537 : 4000417 : void ArithVariables::setUpperBoundConstraint(ConstraintP c)
538 : : {
539 [ - + ]: 4000417 : AssertArgument(c != NullConstraint,
540 : : "Cannot set a upper bound to NullConstraint.");
541 [ + + ][ - + ]: 4000417 : AssertArgument(c->isEquality() || c->isUpperBound(),
[ - + ]
542 : : "Constraint type must be set to an equality or UpperBound.");
543 : :
544 : 4000417 : ArithVar x = c->getVariable();
545 [ + - ]: 8000834 : Trace("partial_model") << "setUpperBoundConstraint(" << x << ":" << c << ")"
546 : 4000417 : << endl;
547 [ - + ][ - + ]: 4000417 : Assert(inMaps(x));
[ - - ]
548 [ - + ][ - + ]: 4000417 : Assert(lessThanUpperBound(x, c->getValue()));
[ - - ]
549 : :
550 : 4000417 : invalidateDelta();
551 : 4000417 : VarInfo& vi = d_vars.get(x);
552 : 4000417 : pushUpperBound(vi);
553 : 4000417 : BoundsInfo prev;
554 [ + + ]: 4000417 : if (vi.setUpperBound(c, prev))
555 : : {
556 : 3802030 : addToBoundQueue(x, prev);
557 : : }
558 : 4000417 : }
559 : :
560 : 14804710 : int ArithVariables::cmpToLowerBound(ArithVar x, const DeltaRational& c) const
561 : : {
562 [ + + ]: 14804710 : if (!hasLowerBound(x))
563 : : {
564 : : // l = -\intfy
565 : : // ? c < -\infty |- _|_
566 : 9974839 : return 1;
567 : : }
568 : : else
569 : : {
570 : 4829871 : return c.cmp(getLowerBound(x));
571 : : }
572 : : }
573 : :
574 : 13628685 : int ArithVariables::cmpToUpperBound(ArithVar x, const DeltaRational& c) const
575 : : {
576 [ + + ]: 13628685 : if (!hasUpperBound(x))
577 : : {
578 : : // u = \intfy
579 : : // ? c > \infty |- _|_
580 : 9684606 : return -1;
581 : : }
582 : : else
583 : : {
584 : 3944079 : return c.cmp(getUpperBound(x));
585 : : }
586 : : }
587 : :
588 : 0 : bool ArithVariables::equalsLowerBound(ArithVar x, const DeltaRational& c)
589 : : {
590 [ - - ]: 0 : if (!hasLowerBound(x))
591 : : {
592 : 0 : return false;
593 : : }
594 : : else
595 : : {
596 : 0 : return c == getLowerBound(x);
597 : : }
598 : : }
599 : 0 : bool ArithVariables::equalsUpperBound(ArithVar x, const DeltaRational& c)
600 : : {
601 [ - - ]: 0 : if (!hasUpperBound(x))
602 : : {
603 : 0 : return false;
604 : : }
605 : : else
606 : : {
607 : 0 : return c == getUpperBound(x);
608 : : }
609 : : }
610 : :
611 : 3284266 : bool ArithVariables::hasEitherBound(ArithVar x) const
612 : : {
613 [ + + ][ + + ]: 3284266 : return hasLowerBound(x) || hasUpperBound(x);
614 : : }
615 : :
616 : 1979716 : bool ArithVariables::strictlyBelowUpperBound(ArithVar x) const
617 : : {
618 : 1979716 : return d_vars[x].d_cmpAssignmentUB < 0;
619 : : }
620 : :
621 : 3400491 : bool ArithVariables::strictlyAboveLowerBound(ArithVar x) const
622 : : {
623 : 3400491 : return d_vars[x].d_cmpAssignmentLB > 0;
624 : : }
625 : :
626 : 28272818 : bool ArithVariables::assignmentIsConsistent(ArithVar x) const
627 : : {
628 [ + + ][ + + ]: 28272818 : return d_vars[x].d_cmpAssignmentLB >= 0 && d_vars[x].d_cmpAssignmentUB <= 0;
629 : : }
630 : :
631 : 3528954 : void ArithVariables::clearSafeAssignments(bool revert)
632 : : {
633 [ + + ][ - + ]: 3528954 : if (revert && !d_safeAssignment.empty())
[ - + ]
634 : : {
635 : 0 : invalidateDelta();
636 : : }
637 : :
638 [ + + ]: 9613993 : while (!d_safeAssignment.empty())
639 : : {
640 : 6085039 : ArithVar atBack = d_safeAssignment.back();
641 [ - + ]: 6085039 : if (revert)
642 : : {
643 : 0 : VarInfo& vi = d_vars.get(atBack);
644 : 0 : BoundsInfo prev;
645 [ - - ]: 0 : if (vi.setAssignment(d_safeAssignment[atBack], prev))
646 : : {
647 : 0 : addToBoundQueue(atBack, prev);
648 : : }
649 : : }
650 : 6085039 : d_safeAssignment.pop_back();
651 : : }
652 : 3528954 : }
653 : :
654 : 87229 : void ArithVariables::revertAssignmentChanges() { clearSafeAssignments(true); }
655 : 3441725 : void ArithVariables::commitAssignmentChanges() { clearSafeAssignments(false); }
656 : :
657 : 2016802 : bool ArithVariables::lowerBoundIsZero(ArithVar x)
658 : : {
659 [ + + ][ + + ]: 2016802 : return hasLowerBound(x) && getLowerBound(x).sgn() == 0;
660 : : }
661 : :
662 : 2057664 : bool ArithVariables::upperBoundIsZero(ArithVar x)
663 : : {
664 [ + + ][ + + ]: 2057664 : return hasUpperBound(x) && getUpperBound(x).sgn() == 0;
665 : : }
666 : :
667 : 0 : void ArithVariables::printEntireModel(std::ostream& out) const
668 : : {
669 : 0 : out << "---Printing Model ---" << std::endl;
670 [ - - ]: 0 : for (var_iterator i = var_begin(), iend = var_end(); i != iend; ++i)
671 : : {
672 : 0 : printModel(*i, out);
673 : : }
674 : 0 : out << "---Done Model ---" << std::endl;
675 : 0 : }
676 : :
677 : 0 : void ArithVariables::printModel(ArithVar x, std::ostream& out) const
678 : : {
679 : 0 : out << "model" << x << ": " << asNode(x) << " " << getAssignment(x) << " ";
680 [ - - ]: 0 : if (!hasLowerBound(x))
681 : : {
682 : 0 : out << "no lb ";
683 : : }
684 : : else
685 : : {
686 : 0 : out << getLowerBound(x) << " ";
687 : 0 : out << getLowerBoundConstraint(x) << " ";
688 : : }
689 [ - - ]: 0 : if (!hasUpperBound(x))
690 : : {
691 : 0 : out << "no ub ";
692 : : }
693 : : else
694 : : {
695 : 0 : out << getUpperBound(x) << " ";
696 : 0 : out << getUpperBoundConstraint(x) << " ";
697 : : }
698 : :
699 [ - - ][ - - ]: 0 : if (isInteger(x) && !integralAssignment(x))
[ - - ]
700 : : {
701 : 0 : out << "(not an integer)" << endl;
702 : : }
703 : 0 : out << endl;
704 : 0 : }
705 : :
706 : 0 : void ArithVariables::printModel(ArithVar x) const
707 : : {
708 [ - - ]: 0 : printModel(x, Trace("model"));
709 : 0 : }
710 : :
711 : 4000417 : void ArithVariables::pushUpperBound(VarInfo& vi)
712 : : {
713 : 4000417 : ++vi.d_pushCount;
714 : 4000417 : d_ubRevertHistory.push_back(make_pair(vi.d_var, vi.d_ub));
715 : 4000417 : }
716 : 4213462 : void ArithVariables::pushLowerBound(VarInfo& vi)
717 : : {
718 : 4213462 : ++vi.d_pushCount;
719 : 4213462 : d_lbRevertHistory.push_back(make_pair(vi.d_var, vi.d_lb));
720 : 4213462 : }
721 : :
722 : 4000417 : void ArithVariables::popUpperBound(AVCPair* c)
723 : : {
724 : 4000417 : ArithVar x = c->first;
725 : 4000417 : VarInfo& vi = d_vars.get(x);
726 : 4000417 : BoundsInfo prev;
727 [ + + ]: 4000417 : if (vi.setUpperBound(c->second, prev))
728 : : {
729 : 3798496 : addToBoundQueue(x, prev);
730 : : }
731 : 4000417 : --vi.d_pushCount;
732 : 4000417 : }
733 : :
734 : 4213462 : void ArithVariables::popLowerBound(AVCPair* c)
735 : : {
736 : 4213462 : ArithVar x = c->first;
737 : 4213462 : VarInfo& vi = d_vars.get(x);
738 : 4213462 : BoundsInfo prev;
739 [ + + ]: 4213462 : if (vi.setLowerBound(c->second, prev))
740 : : {
741 : 3806203 : addToBoundQueue(x, prev);
742 : : }
743 : 4213462 : --vi.d_pushCount;
744 : 4213462 : }
745 : :
746 : 16705358 : void ArithVariables::addToBoundQueue(ArithVar v, const BoundsInfo& prev)
747 : : {
748 [ + + ][ + + ]: 16705358 : if (d_enqueueingBoundCounts && !d_boundsQueue.isKey(v))
[ + + ]
749 : : {
750 : 9612750 : d_boundsQueue.set(v, prev);
751 : : }
752 : 16705358 : }
753 : :
754 : 1006778 : BoundsInfo ArithVariables::selectBoundsInfo(ArithVar v, bool old) const
755 : : {
756 [ + - ][ + + ]: 1006778 : if (old && d_boundsQueue.isKey(v))
[ + + ]
757 : : {
758 : 23263 : return d_boundsQueue[v];
759 : : }
760 : : else
761 : : {
762 : 983515 : return boundsInfo(v);
763 : : }
764 : : }
765 : :
766 : 33404784 : bool ArithVariables::boundsQueueEmpty() const { return d_boundsQueue.empty(); }
767 : :
768 : 5254052 : void ArithVariables::processBoundsQueue(BoundUpdateCallback& changed)
769 : : {
770 [ + + ]: 14668411 : while (!boundsQueueEmpty())
771 : : {
772 : 9414359 : ArithVar v = d_boundsQueue.back();
773 : 9414359 : BoundsInfo prev = d_boundsQueue[v];
774 : 9414359 : d_boundsQueue.pop_back();
775 : 9414359 : BoundsInfo curr = boundsInfo(v);
776 [ + + ]: 9414359 : if (prev != curr)
777 : : {
778 : 9076685 : changed(v, prev);
779 : : }
780 : : }
781 : 5254052 : }
782 : :
783 : 19166071 : void ArithVariables::invalidateDelta() { d_deltaIsSafe = false; }
784 : :
785 : 100273 : void ArithVariables::setDelta(const Rational& d)
786 : : {
787 : 100273 : d_delta = d;
788 : 100273 : d_deltaIsSafe = true;
789 : 100273 : }
790 : :
791 : 3295680 : void ArithVariables::startQueueingBoundCounts()
792 : : {
793 : 3295680 : d_enqueueingBoundCounts = true;
794 : 3295680 : }
795 : 3295680 : void ArithVariables::stopQueueingBoundCounts()
796 : : {
797 : 3295680 : d_enqueueingBoundCounts = false;
798 : 3295680 : }
799 : :
800 : 77568243 : bool ArithVariables::inMaps(ArithVar x) const
801 : : {
802 : 77568243 : return x < getNumberOfVariables();
803 : : }
804 : :
805 : 28663 : ArithVariables::LowerBoundCleanUp::LowerBoundCleanUp(ArithVariables* pm)
806 : 28663 : : d_pm(pm)
807 : : {
808 : 28663 : }
809 : 4213462 : void ArithVariables::LowerBoundCleanUp::operator()(AVCPair& p)
810 : : {
811 : 4213462 : d_pm->popLowerBound(&p);
812 : 4213462 : }
813 : :
814 : 28663 : ArithVariables::UpperBoundCleanUp::UpperBoundCleanUp(ArithVariables* pm)
815 : 28663 : : d_pm(pm)
816 : : {
817 : 28663 : }
818 : 4000417 : void ArithVariables::UpperBoundCleanUp::operator()(AVCPair& p)
819 : : {
820 : 4000417 : d_pm->popUpperBound(&p);
821 : 4000417 : }
822 : :
823 : : } // namespace arith::linear
824 : : } // namespace theory
825 : : } // namespace cvc5::internal
|
