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