diff options
Diffstat (limited to 'src/theory/arith/partial_model.cpp')
-rw-r--r-- | src/theory/arith/partial_model.cpp | 105 |
1 files changed, 62 insertions, 43 deletions
diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp index 4a126ec55..f113c4d34 100644 --- a/src/theory/arith/partial_model.cpp +++ b/src/theory/arith/partial_model.cpp @@ -209,21 +209,52 @@ TNode ArithPartialModel::getUpperConstraint(ArithVar x){ return d_upperConstraint[x]; } - - -bool ArithPartialModel::belowLowerBound(ArithVar x, const DeltaRational& c, bool strict){ +int ArithPartialModel::cmpToLowerBound(ArithVar x, const DeltaRational& c){ if(!hasLowerBound(x)){ // l = -\intfy // ? c < -\infty |- _|_ - return false; + return 1; + }else{ + return c.cmp(d_lowerBound[x]); } - if(strict){ - return c < d_lowerBound[x]; +} + +int ArithPartialModel::cmpToUpperBound(ArithVar x, const DeltaRational& c){ + if(!hasUpperBound(x)){ + //u = \intfy + // ? c > \infty |- _|_ + return -1; }else{ - return c <= d_lowerBound[x]; + return c.cmp(d_upperBound[x]); } } +// bool ArithPartialModel::belowLowerBound(ArithVar x, const DeltaRational& c, bool strict){ +// if(!hasLowerBound(x)){ +// // l = -\intfy +// // ? c < -\infty |- _|_ +// return false; +// } +// if(strict){ +// return c < d_lowerBound[x]; +// }else{ +// return c <= d_lowerBound[x]; +// } +// } + +// bool ArithPartialModel::aboveUpperBound(ArithVar x, const DeltaRational& c, bool strict){ +// if(!hasUpperBound(x)){ +// // u = \intfy +// // ? c > \infty |- _|_ +// return false; +// } +// if(strict){ +// return c > d_upperBound[x]; +// }else{ +// return c >= d_upperBound[x]; +// } +// } + bool ArithPartialModel::equalsLowerBound(ArithVar x, const DeltaRational& c){ if(!hasLowerBound(x)){ return false; @@ -239,18 +270,6 @@ bool ArithPartialModel::equalsUpperBound(ArithVar x, const DeltaRational& c){ } } -bool ArithPartialModel::aboveUpperBound(ArithVar x, const DeltaRational& c, bool strict){ - if(!hasUpperBound(x)){ - // u = \intfy - // ? c > \infty |- _|_ - return false; - } - if(strict){ - return c > d_upperBound[x]; - }else{ - return c >= d_upperBound[x]; - } -} bool ArithPartialModel::hasEitherBound(ArithVar x){ return hasLowerBound(x) || hasUpperBound(x); } @@ -271,35 +290,35 @@ bool ArithPartialModel::strictlyAboveLowerBound(ArithVar x){ return d_lowerBound[x] < d_assignment[x]; } -/** - * x <= u - * ? c < u - */ -bool ArithPartialModel::strictlyBelowUpperBound(ArithVar x, const DeltaRational& c){ - Assert(inMaps(x)); - if(!hasUpperBound(x)){ // u = \infty - return true; - } - return c < d_upperBound[x]; -} - -/** - * x <= u - * ? c < u - */ -bool ArithPartialModel::strictlyAboveLowerBound(ArithVar x, const DeltaRational& c){ - Assert(inMaps(x)); - if(!hasLowerBound(x)){ // l = -\infty - return true; - } - return d_lowerBound[x] < c; -} +// /** +// * x <= u +// * ? c < u +// */ +// bool ArithPartialModel::strictlyBelowUpperBound(ArithVar x, const DeltaRational& c){ +// Assert(inMaps(x)); +// if(!hasUpperBound(x)){ // u = \infty +// return true; +// } +// return c < d_upperBound[x]; +// } + +// /** +// * x <= u +// * ? c < u +// */ +// bool ArithPartialModel::strictlyAboveLowerBound(ArithVar x, const DeltaRational& c){ +// Assert(inMaps(x)); +// if(!hasLowerBound(x)){ // l = -\infty +// return true; +// } +// return d_lowerBound[x] < c; +// } bool ArithPartialModel::assignmentIsConsistent(ArithVar x){ const DeltaRational& beta = getAssignment(x); //l_i <= beta(x_i) <= u_i - return !belowLowerBound(x,beta,true) && !aboveUpperBound(x,beta,true); + return cmpToLowerBound(x,beta) >= 0 && cmpToUpperBound(x,beta) <= 0; } |