diff options
Diffstat (limited to 'src/theory/arith/simplex_update.h')
-rw-r--r-- | src/theory/arith/simplex_update.h | 44 |
1 files changed, 25 insertions, 19 deletions
diff --git a/src/theory/arith/simplex_update.h b/src/theory/arith/simplex_update.h index 7b487c8a3..70c9a5998 100644 --- a/src/theory/arith/simplex_update.h +++ b/src/theory/arith/simplex_update.h @@ -145,7 +145,7 @@ private: * d_nonbasicDelta is zero() or its sgn() must agree with d_nonbasicDirection. */ bool debugSgnAgreement() const { - int deltaSgn = d_nonbasicDelta.constValue().sgn(); + int deltaSgn = d_nonbasicDelta.value().sgn(); return deltaSgn == 0 || deltaSgn == d_nonbasicDirection; } @@ -228,16 +228,19 @@ public: inline int nonbasicDirection() const{ return d_nonbasicDirection; } /** Requires errorsChange to be set through setErrorsChange or updateProposal. */ - inline int errorsChange() const { return d_errorsChange; } + inline int errorsChange() const { return d_errorsChange.value(); } /** * If errorsChange has been set, return errorsChange(). * Otherwise, return def. */ inline int errorsChangeSafe(int def) const { - if(d_errorsChange.just()){ - return d_errorsChange; - }else{ + if (d_errorsChange) + { + return d_errorsChange.value(); + } + else + { return def; } } @@ -250,7 +253,7 @@ public: /** Requires errorsChange to be set through setErrorsChange or updateProposal. */ - inline int focusDirection() const{ return d_focusDirection; } + inline int focusDirection() const { return d_focusDirection.value(); } /** Sets the focusDirection. */ void setFocusDirection(int fd){ @@ -265,18 +268,16 @@ public: * The burden for this being safe is on the user! */ void determineFocusDirection(){ - int deltaSgn = d_nonbasicDelta.constValue().sgn(); + const int deltaSgn = d_nonbasicDelta.value().sgn(); setFocusDirection(deltaSgn * d_nonbasicDirection); } /** Requires nonbasicDelta to be set through updateProposal(...). */ - const DeltaRational& nonbasicDelta() const { - return d_nonbasicDelta; - } + const DeltaRational& nonbasicDelta() const { return d_nonbasicDelta.value(); } const Rational& getCoefficient() const { Assert(describesPivot()); - Assert(d_tableauCoefficient.constValue() != NULL); - return *(d_tableauCoefficient.constValue()); + Assert(d_tableauCoefficient.value() != NULL); + return *(d_tableauCoefficient.value()); } int basicDirection() const { return nonbasicDirection() * (getCoefficient().sgn()); @@ -301,9 +302,7 @@ public: } } - const DeltaRational& focusChange() const { - return d_focusChange; - } + const DeltaRational& focusChange() const { return d_focusChange.value(); } void setFocusChange(const DeltaRational& fc) { d_focusChange = fc; } @@ -329,13 +328,20 @@ private: WitnessImprovement computeWitness() const { if(d_foundConflict){ return ConflictFound; - }else if(d_errorsChange.just() && d_errorsChange < 0){ + } + else if (d_errorsChange.just() && d_errorsChange.value() < 0) + { return ErrorDropped; - }else if(d_errorsChange.nothing() || d_errorsChange == 0){ + } + else if (d_errorsChange.nothing() || d_errorsChange.value() == 0) + { if(d_focusDirection.just()){ - if(d_focusDirection > 0){ + if (d_focusDirection.value() > 0) + { return FocusImproved; - }else if(d_focusDirection == 0){ + } + else if (d_focusDirection.value() == 0) + { return Degenerate; } } |