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, 11 insertions, 11 deletions

diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h
index 293a0ddad..804ad29ac 100644
--- a/src/theory/arith/linear_equality.h
+++ b/src/theory/arith/linear_equality.h
@@ -46,7 +46,7 @@ namespace arith {
 
 struct Border{
   // The constraint for the border
-  Constraint d_bound;
+  ConstraintP d_bound;
 
   // The change to the nonbasic to reach the border
   DeltaRational d_diff;
@@ -65,11 +65,11 @@ struct Border{
     d_bound(NullConstraint) // ignore the other values
   {}
 
-  Border(Constraint l, const DeltaRational& diff, bool areFixing, const Tableau::Entry* en, bool ub):
+  Border(ConstraintP l, const DeltaRational& diff, bool areFixing, const Tableau::Entry* en, bool ub):
     d_bound(l), d_diff(diff), d_areFixing(areFixing), d_entry(en),  d_upperbound(ub)
   {}
 
-  Border(Constraint l, const DeltaRational& diff, bool areFixing, bool ub):
+  Border(ConstraintP l, const DeltaRational& diff, bool areFixing, bool ub):
     d_bound(l), d_diff(diff), d_areFixing(areFixing), d_entry(NULL),  d_upperbound(ub)
   {}
   bool operator<(const Border& other) const{
@@ -414,13 +414,13 @@ public:
    * The constraint on a basic variable b is implied by the constraints
    * on its row.  This is a wrapper for propagateRow().
    */
-  void propagateBasicFromRow(Constraint c);
+  void propagateBasicFromRow(ConstraintP c);
 
   /**
    * Exports either the explanation of an upperbound or a lower bound
    * of the basic variable basic, using the non-basic variables in the row.
    */
-  void propagateRow(std::vector<Constraint>& into, RowIndex ridx, bool rowUp, Constraint c);
+  void propagateRow(ConstraintCPVec& into, RowIndex ridx, bool rowUp, ConstraintP c);
 
   /**
    * Computes the value of a basic variable using the assignments
@@ -592,26 +592,26 @@ private:
    * with the weakest possible constraint that is consistent with the surplus
    * surplus.
    */
-  Constraint weakestExplanation(bool aboveUpper, DeltaRational& surplus, ArithVar v,
+  ConstraintP weakestExplanation(bool aboveUpper, DeltaRational& surplus, ArithVar v,
                                 const Rational& coeff, bool& anyWeakening, ArithVar basic) const;
 
 public:
   /**
    * Constructs a minimally weak conflict for the basic variable basicVar.
    */
-  Node minimallyWeakConflict(bool aboveUpper, ArithVar basicVar) const;
+  void minimallyWeakConflict(bool aboveUpper, ArithVar basicVar, RaiseConflict& rc) const;
 
   /**
    * Given a non-basic variable that is know to have a conflict on it,
    * construct and return a conflict.
    * Follows section 4.2 in the CAV06 paper.
    */
-  inline Node generateConflictAboveUpperBound(ArithVar conflictVar) const {
-    return minimallyWeakConflict(true, conflictVar);
+  inline void generateConflictAboveUpperBound(ArithVar conflictVar, RaiseConflict& rc) const {
+    minimallyWeakConflict(true, conflictVar, rc);
   }
 
-  inline Node generateConflictBelowLowerBound(ArithVar conflictVar) const {
-    return minimallyWeakConflict(false, conflictVar);
+  inline void generateConflictBelowLowerBound(ArithVar conflictVar, RaiseConflict& rc) const {
+    minimallyWeakConflict(false, conflictVar, rc);
   }
 
   /**