1 /********************* */
2 /*! \file partial_model.cpp
4 ** Original author: Tim King
5 ** Major contributors: none
6 ** Minor contributors (to current version): Morgan Deters
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2013 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief [[ Add one-line brief description here ]]
14 ** [[ Add lengthier description here ]]
15 ** \todo document this file
19 #include "theory/arith/partial_model.h"
20 #include "util/output.h"
21 #include "theory/arith/constraint.h"
22 #include "theory/arith/normal_form.h"
30 ArithVariables::ArithVariables(context::Context
* c
, DeltaComputeCallback deltaComputingFunc
)
33 d_numberOfVariables(0),
36 d_releasedIterator(d_released
.begin()),
37 d_nodeToArithVarMap(),
39 d_enqueueingBoundCounts(true),
40 d_lbRevertHistory(c
, true, LowerBoundCleanUp(this)),
41 d_ubRevertHistory(c
, true, UpperBoundCleanUp(this)),
44 d_deltaComputingFunc(deltaComputingFunc
)
47 ArithVariables::VarInfo::VarInfo()
48 : d_var(ARITHVAR_SENTINEL
),
53 d_cmpAssignmentUB(-1),
59 bool ArithVariables::VarInfo::initialized() const {
60 return d_var
!= ARITHVAR_SENTINEL
;
63 void ArithVariables::VarInfo::initialize(ArithVar v
, Node n
, bool slack
){
64 Assert(!initialized());
65 Assert(d_lb
== NullConstraint
);
66 Assert(d_ub
== NullConstraint
);
67 Assert(d_cmpAssignmentLB
> 0);
68 Assert(d_cmpAssignmentUB
< 0);
74 //The type computation is not quite accurate for Rationals that are
76 //We'll use the isIntegral check from the polynomial package instead.
77 Polynomial p
= Polynomial::parsePolynomial(n
);
78 d_type
= p
.isIntegral() ? ATInteger
: ATReal
;
80 d_type
= nodeToArithType(n
);
83 Assert(initialized());
85 void ArithVariables::VarInfo::uninitialize(){
86 d_var
= ARITHVAR_SENTINEL
;
87 d_node
= Node::null();
90 bool ArithVariables::VarInfo::setAssignment(const DeltaRational
& a
, BoundsInfo
& prev
){
91 Assert(initialized());
93 int cmpUB
= (d_ub
== NullConstraint
) ? -1 :
94 d_assignment
.cmp(d_ub
->getValue());
96 int cmpLB
= (d_lb
== NullConstraint
) ? 1 :
97 d_assignment
.cmp(d_lb
->getValue());
99 bool lbChanged
= cmpLB
!= d_cmpAssignmentLB
&&
100 (cmpLB
== 0 || d_cmpAssignmentLB
== 0);
101 bool ubChanged
= cmpUB
!= d_cmpAssignmentUB
&&
102 (cmpUB
== 0 || d_cmpAssignmentUB
== 0);
104 if(lbChanged
|| ubChanged
){
108 d_cmpAssignmentUB
= cmpUB
;
109 d_cmpAssignmentLB
= cmpLB
;
110 return lbChanged
|| ubChanged
;
113 void ArithVariables::releaseArithVar(ArithVar v
){
114 VarInfo
& vi
= d_vars
.get(v
);
117 if(d_safeAssignment
.isKey(v
)){
118 d_safeAssignment
.remove(v
);
120 if(vi
.canBeReclaimed()){
123 d_released
.push_back(v
);
127 bool ArithVariables::VarInfo::setUpperBound(Constraint ub
, BoundsInfo
& prev
){
128 Assert(initialized());
129 bool wasNull
= d_ub
== NullConstraint
;
130 bool isNull
= ub
== NullConstraint
;
132 int cmpUB
= isNull
? -1 : d_assignment
.cmp(ub
->getValue());
133 bool ubChanged
= (wasNull
!= isNull
) ||
134 (cmpUB
!= d_cmpAssignmentUB
&& (cmpUB
== 0 || d_cmpAssignmentUB
== 0));
139 d_cmpAssignmentUB
= cmpUB
;
143 bool ArithVariables::VarInfo::setLowerBound(Constraint lb
, BoundsInfo
& prev
){
144 Assert(initialized());
145 bool wasNull
= d_lb
== NullConstraint
;
146 bool isNull
= lb
== NullConstraint
;
148 int cmpLB
= isNull
? 1 : d_assignment
.cmp(lb
->getValue());
150 bool lbChanged
= (wasNull
!= isNull
) ||
151 (cmpLB
!= d_cmpAssignmentLB
&& (cmpLB
== 0 || d_cmpAssignmentLB
== 0));
156 d_cmpAssignmentLB
= cmpLB
;
160 BoundCounts
ArithVariables::VarInfo::atBoundCounts() const {
161 uint32_t lbIndc
= (d_cmpAssignmentLB
== 0) ? 1 : 0;
162 uint32_t ubIndc
= (d_cmpAssignmentUB
== 0) ? 1 : 0;
163 return BoundCounts(lbIndc
, ubIndc
);
166 BoundCounts
ArithVariables::VarInfo::hasBoundCounts() const {
167 uint32_t lbIndc
= (d_lb
!= NullConstraint
) ? 1 : 0;
168 uint32_t ubIndc
= (d_ub
!= NullConstraint
) ? 1 : 0;
169 return BoundCounts(lbIndc
, ubIndc
);
172 BoundsInfo
ArithVariables::VarInfo::boundsInfo() const{
173 return BoundsInfo(atBoundCounts(), hasBoundCounts());
176 bool ArithVariables::VarInfo::canBeReclaimed() const{
177 return d_pushCount
== 0;
180 void ArithVariables::attemptToReclaimReleased(){
181 std::list
<ArithVar
>::iterator i_end
= d_released
.end();
182 for(int iter
= 0; iter
< 20 && d_releasedIterator
!= i_end
; ++d_releasedIterator
){
183 ArithVar v
= *d_releasedIterator
;
184 VarInfo
& vi
= d_vars
.get(v
);
185 if(vi
.canBeReclaimed()){
187 std::list
<ArithVar
>::iterator curr
= d_releasedIterator
;
188 ++d_releasedIterator
;
189 d_released
.erase(curr
);
191 ++d_releasedIterator
;
194 if(d_releasedIterator
== i_end
){
195 d_releasedIterator
= d_released
.begin();
199 ArithVar
ArithVariables::allocateVariable(){
201 attemptToReclaimReleased();
203 bool reclaim
= !d_pool
.empty();
207 varX
= d_pool
.back();
210 varX
= d_numberOfVariables
;
211 ++d_numberOfVariables
;
213 d_vars
.set(varX
, VarInfo());
218 const Rational
& ArithVariables::getDelta(){
220 Rational nextDelta
= d_deltaComputingFunc();
223 Assert(d_deltaIsSafe
);
227 bool ArithVariables::boundsAreEqual(ArithVar x
) const{
228 if(hasLowerBound(x
) && hasUpperBound(x
)){
229 return getUpperBound(x
) == getLowerBound(x
);
235 void ArithVariables::setAssignment(ArithVar x
, const DeltaRational
& r
){
236 Debug("partial_model") << "pm: updating the assignment to" << x
237 << " now " << r
<<endl
;
238 VarInfo
& vi
= d_vars
.get(x
);
239 if(!d_safeAssignment
.isKey(x
)){
240 d_safeAssignment
.set(x
, vi
.d_assignment
);
245 if(vi
.setAssignment(r
, prev
)){
246 addToBoundQueue(x
, prev
);
250 void ArithVariables::setAssignment(ArithVar x
, const DeltaRational
& safe
, const DeltaRational
& r
){
251 Debug("partial_model") << "pm: updating the assignment to" << x
252 << " now " << r
<<endl
;
254 if(d_safeAssignment
.isKey(x
)){
255 d_safeAssignment
.remove(x
);
258 d_safeAssignment
.set(x
, safe
);
262 VarInfo
& vi
= d_vars
.get(x
);
264 if(vi
.setAssignment(r
, prev
)){
265 addToBoundQueue(x
, prev
);
269 void ArithVariables::initialize(ArithVar x
, Node n
, bool slack
){
270 VarInfo
& vi
= d_vars
.get(x
);
271 vi
.initialize(x
, n
, slack
);
272 d_nodeToArithVarMap
[n
] = x
;
275 ArithVar
ArithVariables::allocate(Node n
, bool slack
){
276 ArithVar v
= allocateVariable();
277 initialize(v
, n
, slack
);
281 // void ArithVariables::initialize(ArithVar x, const DeltaRational& r){
282 // Assert(x == d_mapSize);
283 // Assert(equalSizes());
286 // // Is worth mentioning that this is not strictly necessary, but this maintains the internal invariant
287 // // that when d_assignment is set this gets set.
288 // invalidateDelta();
289 // d_assignment.push_back( r );
291 // d_boundRel.push_back(BetweenBounds);
293 // d_ubc.push_back(NullConstraint);
294 // d_lbc.push_back(NullConstraint);
297 /** Must know that the bound exists both calling this! */
298 const DeltaRational
& ArithVariables::getUpperBound(ArithVar x
) const {
300 Assert(hasUpperBound(x
));
302 return getUpperBoundConstraint(x
)->getValue();
305 const DeltaRational
& ArithVariables::getLowerBound(ArithVar x
) const {
307 Assert(hasLowerBound(x
));
309 return getLowerBoundConstraint(x
)->getValue();
312 const DeltaRational
& ArithVariables::getSafeAssignment(ArithVar x
) const{
314 if(d_safeAssignment
.isKey(x
)){
315 return d_safeAssignment
[x
];
317 return d_vars
[x
].d_assignment
;
321 const DeltaRational
& ArithVariables::getAssignment(ArithVar x
, bool safe
) const{
323 if(safe
&& d_safeAssignment
.isKey(x
)){
324 return d_safeAssignment
[x
];
326 return d_vars
[x
].d_assignment
;
330 const DeltaRational
& ArithVariables::getAssignment(ArithVar x
) const{
332 return d_vars
[x
].d_assignment
;
336 void ArithVariables::setLowerBoundConstraint(Constraint c
){
337 AssertArgument(c
!= NullConstraint
, "Cannot set a lower bound to NullConstraint.");
338 AssertArgument(c
->isEquality() || c
->isLowerBound(),
339 "Constraint type must be set to an equality or UpperBound.");
340 ArithVar x
= c
->getVariable();
341 Debug("partial_model") << "setLowerBoundConstraint(" << x
<< ":" << c
<< ")" << endl
;
343 Assert(greaterThanLowerBound(x
, c
->getValue()));
346 VarInfo
& vi
= d_vars
.get(x
);
349 if(vi
.setLowerBound(c
, prev
)){
350 addToBoundQueue(x
, prev
);
354 void ArithVariables::setUpperBoundConstraint(Constraint c
){
355 AssertArgument(c
!= NullConstraint
, "Cannot set a upper bound to NullConstraint.");
356 AssertArgument(c
->isEquality() || c
->isUpperBound(),
357 "Constraint type must be set to an equality or UpperBound.");
359 ArithVar x
= c
->getVariable();
360 Debug("partial_model") << "setUpperBoundConstraint(" << x
<< ":" << c
<< ")" << endl
;
362 Assert(lessThanUpperBound(x
, c
->getValue()));
365 VarInfo
& vi
= d_vars
.get(x
);
368 if(vi
.setUpperBound(c
, prev
)){
369 addToBoundQueue(x
, prev
);
373 int ArithVariables::cmpToLowerBound(ArithVar x
, const DeltaRational
& c
) const{
374 if(!hasLowerBound(x
)){
376 // ? c < -\infty |- _|_
379 return c
.cmp(getLowerBound(x
));
383 int ArithVariables::cmpToUpperBound(ArithVar x
, const DeltaRational
& c
) const{
384 if(!hasUpperBound(x
)){
386 // ? c > \infty |- _|_
389 return c
.cmp(getUpperBound(x
));
393 bool ArithVariables::equalsLowerBound(ArithVar x
, const DeltaRational
& c
){
394 if(!hasLowerBound(x
)){
397 return c
== getLowerBound(x
);
400 bool ArithVariables::equalsUpperBound(ArithVar x
, const DeltaRational
& c
){
401 if(!hasUpperBound(x
)){
404 return c
== getUpperBound(x
);
408 bool ArithVariables::hasEitherBound(ArithVar x
) const{
409 return hasLowerBound(x
) || hasUpperBound(x
);
412 bool ArithVariables::strictlyBelowUpperBound(ArithVar x
) const{
413 return d_vars
[x
].d_cmpAssignmentUB
< 0;
416 bool ArithVariables::strictlyAboveLowerBound(ArithVar x
) const{
417 return d_vars
[x
].d_cmpAssignmentLB
> 0;
420 bool ArithVariables::assignmentIsConsistent(ArithVar x
) const{
422 d_vars
[x
].d_cmpAssignmentLB
>= 0 &&
423 d_vars
[x
].d_cmpAssignmentUB
<= 0;
427 void ArithVariables::clearSafeAssignments(bool revert
){
429 if(revert
&& !d_safeAssignment
.empty()){
433 while(!d_safeAssignment
.empty()){
434 ArithVar atBack
= d_safeAssignment
.back();
436 VarInfo
& vi
= d_vars
.get(atBack
);
438 if(vi
.setAssignment(d_safeAssignment
[atBack
], prev
)){
439 addToBoundQueue(atBack
, prev
);
442 d_safeAssignment
.pop_back();
446 void ArithVariables::revertAssignmentChanges(){
447 clearSafeAssignments(true);
449 void ArithVariables::commitAssignmentChanges(){
450 clearSafeAssignments(false);
453 void ArithVariables::printEntireModel(std::ostream
& out
) const{
454 out
<< "---Printing Model ---" << std::endl
;
455 for(var_iterator i
= var_begin(), iend
= var_end(); i
!= iend
; ++i
){
458 out
<< "---Done Model ---" << std::endl
;
461 void ArithVariables::printModel(ArithVar x
, std::ostream
& out
) const{
462 out
<< "model" << x
<< ": "
464 << getAssignment(x
) << " ";
465 if(!hasLowerBound(x
)){
468 out
<< getLowerBound(x
) << " ";
469 out
<< getLowerBoundConstraint(x
) << " ";
471 if(!hasUpperBound(x
)){
474 out
<< getUpperBound(x
) << " ";
475 out
<< getUpperBoundConstraint(x
) << " ";
480 void ArithVariables::printModel(ArithVar x
) const{
481 printModel(x
, Debug("model"));
484 void ArithVariables::pushUpperBound(VarInfo
& vi
){
486 d_ubRevertHistory
.push_back(make_pair(vi
.d_var
, vi
.d_ub
));
488 void ArithVariables::pushLowerBound(VarInfo
& vi
){
490 d_lbRevertHistory
.push_back(make_pair(vi
.d_var
, vi
.d_lb
));
493 void ArithVariables::popUpperBound(AVCPair
* c
){
494 ArithVar x
= c
->first
;
495 VarInfo
& vi
= d_vars
.get(x
);
497 if(vi
.setUpperBound(c
->second
, prev
)){
498 addToBoundQueue(x
, prev
);
503 void ArithVariables::popLowerBound(AVCPair
* c
){
504 ArithVar x
= c
->first
;
505 VarInfo
& vi
= d_vars
.get(x
);
507 if(vi
.setLowerBound(c
->second
, prev
)){
508 addToBoundQueue(x
, prev
);
513 void ArithVariables::addToBoundQueue(ArithVar v
, const BoundsInfo
& prev
){
514 if(d_enqueueingBoundCounts
&& !d_boundsQueue
.isKey(v
)){
515 d_boundsQueue
.set(v
, prev
);
519 BoundsInfo
ArithVariables::selectBoundsInfo(ArithVar v
, bool old
) const {
520 if(old
&& d_boundsQueue
.isKey(v
)){
521 return d_boundsQueue
[v
];
523 return boundsInfo(v
);
527 bool ArithVariables::boundsQueueEmpty() const {
528 return d_boundsQueue
.empty();
531 void ArithVariables::processBoundsQueue(BoundUpdateCallback
& changed
){
532 while(!boundsQueueEmpty()){
533 ArithVar v
= d_boundsQueue
.back();
534 BoundsInfo prev
= d_boundsQueue
[v
];
535 d_boundsQueue
.pop_back();
536 BoundsInfo curr
= boundsInfo(v
);
543 void ArithVariables::LowerBoundCleanUp::operator()(AVCPair
* p
){
544 d_pm
->popLowerBound(p
);
547 void ArithVariables::UpperBoundCleanUp::operator()(AVCPair
* p
){
548 d_pm
->popUpperBound(p
);
551 }/* CVC4::theory::arith namespace */
552 }/* CVC4::theory namespace */
553 }/* CVC4 namespace */