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.h b/src/theory/arith/error_set.h
index d1b692cb4..b87282ba0 100644
--- a/src/theory/arith/error_set.h
+++ b/src/theory/arith/error_set.h
@@ -120,7 +120,7 @@ private:
    * This needs to be saved in case that the
    * violated constraint
    */
-  Constraint d_violated;
+  ConstraintP d_violated;
 
   /**
    * This is the sgn of the first derivate the variable must move to satisfy
@@ -155,12 +155,12 @@ private:
 
 public:
   ErrorInformation();
-  ErrorInformation(ArithVar var, Constraint vio, int sgn);
+  ErrorInformation(ArithVar var, ConstraintP vio, int sgn);
   ~ErrorInformation();
   ErrorInformation(const ErrorInformation& ei);
   ErrorInformation& operator=(const ErrorInformation& ei);
 
-  void reset(Constraint c, int sgn);
+  void reset(ConstraintP c, int sgn);
 
   inline ArithVar getVariable() const { return d_variable; }
 
@@ -192,7 +192,7 @@ public:
   }
   inline const FocusSetHandle& getHandle() const{ return d_handle; }
 
-  inline Constraint getViolated() const { return d_violated; }
+  inline ConstraintP getViolated() const { return d_violated; }
 
   bool debugInitialized() const {
     return
@@ -389,7 +389,7 @@ public:
     return d_errInfo[a].getMetric();
   }
 
-  Constraint getViolated(ArithVar a) const {
+  ConstraintP getViolated(ArithVar a) const {
     return d_errInfo[a].getViolated();
   }