Code cleanup. Reducing misc. warnings in arithmetic.

diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp
index d6be9f657c9a402027ab57521788c8d54941afee..5777337ee3a7367b7c7c4e9771e1f0f71948c784 100644 (file)
--- a/src/theory/arith/approx_simplex.cpp
+++ b/src/theory/arith/approx_simplex.cpp
@@ -147,6 +147,7 @@ public:
   }
   virtual void setOptCoeffs(const ArithRatPairVec& ref);
 
+  static void printGLPKStatus(int status, std::ostream& out);
 private:
   Solution extractSolution(bool mip) const;
 };
@@ -361,7 +362,7 @@ void ApproxGLPK::setOptCoeffs(const ArithRatPairVec& ref){
  *   check with FCSimplex
  */
 
-static void printGLPKStatus(int status, std::ostream& out){
+void ApproxGLPK::printGLPKStatus(int status, std::ostream& out){
   switch(status){
   case GLP_OPT:
     out << "GLP_OPT" << endl;

diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp
index 7caee6708902d3dc3252ab729aec85127aaf3148..a9304ae76f8446a7830e7baad538c7a561d4ee97 100644 (file)
--- a/src/theory/arith/dual_simplex.cpp
+++ b/src/theory/arith/dual_simplex.cpp
@@ -196,19 +196,19 @@ bool DualSimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingI
     //DeltaRational beta_i = d_variables.getAssignment(x_i);
     ArithVar x_j = ARITHVAR_SENTINEL;
 
-    int32_t prevErrorSize = d_errorSet.errorSize();
+    int32_t prevErrorSize CVC4_UNUSED = d_errorSet.errorSize();
 
     if(d_variables.cmpAssignmentLowerBound(x_i) < 0 ){
       x_j = d_linEq.selectSlackUpperBound(x_i, pf);
       if(x_j == ARITHVAR_SENTINEL ){
         Unreachable();
-        ++(d_statistics.d_statUpdateConflicts);
-        reportConflict(x_i);
-        ++(d_statistics.d_simplexConflicts);
+        // ++(d_statistics.d_statUpdateConflicts);
+        // reportConflict(x_i);
+        // ++(d_statistics.d_simplexConflicts);
         // Node conflict = d_linEq.generateConflictBelowLowerBound(x_i); //unsat
         // d_conflictVariable = x_i;
         // reportConflict(conflict);
-        return true;
+        // return true;
       }else{
         const DeltaRational& l_i = d_variables.getLowerBound(x_i);
         d_linEq.pivotAndUpdate(x_i, x_j, l_i);
@@ -217,13 +217,13 @@ bool DualSimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingI
       x_j = d_linEq.selectSlackLowerBound(x_i, pf);
       if(x_j == ARITHVAR_SENTINEL ){
         Unreachable();
-        ++(d_statistics.d_statUpdateConflicts);
-        reportConflict(x_i);
-        ++(d_statistics.d_simplexConflicts);
+        // ++(d_statistics.d_statUpdateConflicts);
+        // reportConflict(x_i);
+        // ++(d_statistics.d_simplexConflicts);
         // Node conflict = d_linEq.generateConflictAboveUpperBound(x_i); //unsat
         // d_conflictVariable = x_i;
         // reportConflict(conflict);
-        return true;
+        // return true;
       }else{
         const DeltaRational& u_i = d_variables.getUpperBound(x_i);
         d_linEq.pivotAndUpdate(x_i, x_j, u_i);
@@ -232,16 +232,19 @@ bool DualSimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingI
     Assert(x_j != ARITHVAR_SENTINEL);
 
     bool conflict = processSignals();
-    int32_t currErrorSize = d_errorSet.errorSize();
+    int32_t currErrorSize CVC4_UNUSED = d_errorSet.errorSize();
     d_pivots++;
 
-    // cout << "#" << d_pivots
-    //      << " c" << conflict
-    //      << " d" << (prevErrorSize - currErrorSize)
-    //      << " f"  << d_errorSet.inError(x_j)
-    //      << " h" << d_conflictVariables.isMember(x_j)
-    //      << " " << x_i << "->" << x_j
-    //      << endl;
+    if(Debug.isOn("arith::dual")){
+      Debug("arith::dual")
+        << "#" << d_pivots
+        << " c" << conflict
+        << " d" << (prevErrorSize - currErrorSize)
+        << " f"  << d_errorSet.inError(x_j)
+        << " h" << d_conflictVariables.isMember(x_j)
+        << " " << x_i << "->" << x_j
+        << endl;
+    }
 
     if(conflict){
       return true;

diff --git a/src/theory/arith/options b/src/theory/arith/options
index 35cede8b4f8e9e72ed19ee55ea58be99540462dd..7d92f53515384b8c61d6a4f7a559b5da72b93cc4 100644 (file)
--- a/src/theory/arith/options
+++ b/src/theory/arith/options
@@ -94,7 +94,7 @@ option exportDioDecompositions --dio-decomps bool :default false :read-write
 option newProp --new-prop bool :default false :read-write
  Use the new row propagation system
 
-option arithPropAsLemmaLength --arith-prop-clauses int :default 8 :read-write
+option arithPropAsLemmaLength --arith-prop-clauses uint16_t :default 8 :read-write
  Rows shorter than this are propagated as clauses
 
 option soiQuickExplain --soi-qe bool :default false :read-write

diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp
index cbbdcb7f3d1f9c227bfd276e83b2b497222465cc..d0595321c1caad5868d154c22f6b2c368c2ae24c 100644 (file)
--- a/src/theory/arith/soi_simplex.cpp
+++ b/src/theory/arith/soi_simplex.cpp
@@ -711,8 +711,6 @@ std::vector< ArithVarVec > SumOfInfeasibilitiesSPD::greedyConflictSubsets(){
     underConstruction.push_back(v);
     d_soiVar = constructInfeasiblityFunction(d_statistics.d_soiConflictMinimization, v);
 
-    bool uniqueChoices = true;
-
     //cout << "trying " << v << endl;
 
     const Tableau::Entry* spoiler = NULL;