diff options
Diffstat (limited to 'src/theory/arith/error_set.cpp')
| -rw-r--r-- | src/theory/arith/error_set.cpp | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/theory/arith/error_set.cpp b/src/theory/arith/error_set.cpp index dea78acf7..6d341ed12 100644 --- a/src/theory/arith/error_set.cpp +++ b/src/theory/arith/error_set.cpp @@ -39,7 +39,7 @@ ErrorInformation::ErrorInformation() Debug("arith::error::mem") << "def constructor " << d_variable << " " << d_amount << endl; } -ErrorInformation::ErrorInformation(ArithVar var, Constraint vio, int sgn) +ErrorInformation::ErrorInformation(ArithVar var, ConstraintP vio, int sgn) : d_variable(var) , d_violated(vio) , d_sgn(sgn) @@ -105,7 +105,7 @@ ErrorInformation& ErrorInformation::operator=(const ErrorInformation& ei){ return *this; } -void ErrorInformation::reset(Constraint c, int sgn){ +void ErrorInformation::reset(ConstraintP c, int sgn){ Assert(!isRelaxed()); Assert(c != NullConstraint); d_violated = c; @@ -272,7 +272,7 @@ void ErrorSet::transitionVariableOutOfError(ArithVar v) { ErrorInformation& ei = d_errInfo.get(v); Assert(ei.debugInitialized()); if(ei.isRelaxed()){ - Constraint viol = ei.getViolated(); + ConstraintP viol = ei.getViolated(); if(ei.sgn() > 0){ d_variables.setLowerBoundConstraint(viol); }else{ @@ -293,7 +293,7 @@ void ErrorSet::transitionVariableIntoError(ArithVar v) { Assert(inconsistent(v)); bool vilb = d_variables.cmpAssignmentLowerBound(v) < 0; int sgn = vilb ? 1 : -1; - Constraint c = vilb ? + ConstraintP c = vilb ? d_variables.getLowerBoundConstraint(v) : d_variables.getUpperBoundConstraint(v); d_errInfo.set(v, ErrorInformation(v, c, sgn)); ErrorInformation& ei = d_errInfo.get(v); @@ -373,7 +373,7 @@ int ErrorSet::popSignal() { Assert(!vilb || !viub); int currSgn = vilb ? 1 : -1; if(currSgn != prevSgn){ - Constraint curr = vilb ? d_variables.getLowerBoundConstraint(back) + ConstraintP curr = vilb ? d_variables.getLowerBoundConstraint(back) : d_variables.getUpperBoundConstraint(back); ei.reset(curr, currSgn); } |