Merging a squash of the branch timothy-king/CVC4/glpknecfix c95bf7d4f1 into master. See the CAV14 submission for an explanation of the changes to the integer solver's behavior. If compiled against the our custom extension of glpk, https://github.com/timothy-king/glpk-cut-log, this should have substantial differences in behavior. This should have moderate performance differences for linear real and integer arithmetic even if these features are disabled.

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);
       }