diff options
author | Tim King <taking@cs.nyu.edu> | 2010-10-22 01:28:40 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-10-22 01:28:40 +0000 |
commit | c2cf1a6aafd516759a3f6a43d91222a97fcfe8f7 (patch) | |
tree | 4ad84f3e47bf3d8e7151f73669157f6b10287464 /src/theory/arith/partial_model.cpp | |
parent | 22f47a144520f39801abb3acacbf3639886b0478 (diff) |
Fixes to getValue for TheoryArith.
Diffstat (limited to 'src/theory/arith/partial_model.cpp')
-rw-r--r-- | src/theory/arith/partial_model.cpp | 35 |
1 files changed, 21 insertions, 14 deletions
diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp index a0f0247be..bee24aa39 100644 --- a/src/theory/arith/partial_model.cpp +++ b/src/theory/arith/partial_model.cpp @@ -250,27 +250,34 @@ void ArithPartialModel::printModel(ArithVar x){ } } +void ArithPartialModel::deltaIsSmallerThan(const DeltaRational& l, const DeltaRational& u){ + const Rational& c = l.getNoninfinitesimalPart(); + const Rational& k = l.getInfinitesimalPart(); + const Rational& d = u.getNoninfinitesimalPart(); + const Rational& h = u.getInfinitesimalPart(); + + if(c < d && k > h){ + Rational ep = (d-c)/(k-h); + if(ep < d_delta){ + d_delta = ep; + } + } +} + void ArithPartialModel::computeDelta(){ Assert(!d_deltaIsSafe); - d_deltaIsSafe = true; d_delta = 1; for(ArithVar x = 0; x < d_mapSize; ++x){ - if(hasBounds(x)){ + const DeltaRational& a = getAssignment(x); + if(!d_lowerConstraint[x].isNull()){ const DeltaRational& l = getLowerBound(x); + deltaIsSmallerThan(l,a); + } + if(!d_upperConstraint[x].isNull()){ const DeltaRational& u = getUpperBound(x); - // c + k\ep <= d + h\ep - const Rational& c = l.getNoninfinitesimalPart(); - const Rational& k = l.getInfinitesimalPart(); - const Rational& d = u.getNoninfinitesimalPart(); - const Rational& h = u.getInfinitesimalPart(); - - if(c < d && k > h){ - Rational ep = (d-c)/(k-h); - if(ep < d_delta){ - d_delta = ep; - } - } + deltaIsSmallerThan(a,u); } } + d_deltaIsSafe = true; } |