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