Adding cut offs for likely integer infeasible paths.

5 files changed, 41 insertions, 21 deletions

diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp
index 55e52fc53..ef3ea0484 100644
--- a/src/theory/arith/approx_simplex.cpp
+++ b/src/theory/arith/approx_simplex.cpp
@@ -155,7 +155,7 @@ private:
 };
 
 #warning "set back to 0"
-int ApproxGLPK::s_verbosity = 1;
+int ApproxGLPK::s_verbosity = 0;
 
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp
index c8d5b6f68..9db56ff68 100644
--- a/src/theory/arith/attempt_solution_simplex.cpp
+++ b/src/theory/arith/attempt_solution_simplex.cpp
@@ -103,12 +103,12 @@ Result::Sat AttemptSolutionSDP::attempt(const ApproximateSimplex::Solution& sol)
     Assert(toAdd != ARITHVAR_SENTINEL);
 
     Trace("arith::forceNewBasis") << toRemove << " " << toAdd << endl;
-    Message() << toRemove << " " << toAdd << endl;
+    //Message() << toRemove << " " << toAdd << endl;
 
     d_linEq.pivotAndUpdate(toRemove, toAdd, newValues[toRemove]);
 
     Trace("arith::forceNewBasis") << needsToBeAdded.size() << "to go" << endl;
-    Message() << needsToBeAdded.size() << "to go" << endl;
+    //Message() << needsToBeAdded.size() << "to go" << endl;
     needsToBeAdded.remove(toAdd);
 
     bool conflict = processSignals();
diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp
index 6095727a3..d7e1808e4 100644
--- a/src/theory/arith/soi_simplex.cpp
+++ b/src/theory/arith/soi_simplex.cpp
@@ -591,7 +591,7 @@ void SumOfInfeasibilitiesSPD::quickExplain(){
   d_qeConflict.clear();
   d_errorSet.pushFocusInto(d_qeConflict);
 
-  cout <<  d_qeConflict.size() << " ";
+  //cout <<  d_qeConflict.size() << " ";
   uint32_t size = d_qeConflict.size();
 
   if(size > 2){
@@ -611,7 +611,7 @@ void SumOfInfeasibilitiesSPD::quickExplain(){
     d_qeSgns.clear();
   }
 
-  cout << d_qeConflict.size() << endl;
+  //cout << d_qeConflict.size() << endl;
 
   Assert(d_qeInSoi.empty());
   Assert(d_qeInUAndNotInSoi.empty());
@@ -813,7 +813,7 @@ WitnessImprovement SumOfInfeasibilitiesSPD::SOIConflict(){
   if(options::soiQuickExplain()){
     quickExplain();
     Node conflict = generateSOIConflict(d_qeConflict);
-    cout << conflict << endl;
+    //cout << conflict << endl;
     d_conflictChannel(conflict);
   }else{
 
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 504727c0b..08907880e 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -114,6 +114,7 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context
   d_fullCheckCounter(0),
   d_cutCount(c, 0),
   d_cutInContext(c),
+  d_likelyIntegerInfeasible(c, false),
   d_statistics()
 {
   srand(79);
@@ -1574,9 +1575,11 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){
     static const int32_t relaxationLimit = 10000;
     static const int32_t mipLimit = 200000;
 
+    //cout << "start" << endl;
     d_qflraStatus = simplex.findModel(false);
+    //cout << "end" << endl;
     if(d_qflraStatus == Result::SAT_UNKNOWN ||
-       (d_qflraStatus == Result::SAT && !hasIntegerModel())){
+       (d_qflraStatus == Result::SAT && !hasIntegerModel() && !d_likelyIntegerInfeasible)){
 
       ApproximateSimplex* approxSolver = ApproximateSimplex::mkApproximateSimplexSolver(d_partialModel);
       approxSolver->setPivotLimit(relaxationLimit);
@@ -1588,23 +1591,27 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){
       case ApproximateSimplex::ApproxSat:
         {
           relaxSolution = approxSolver->extractRelaxation();
-          approxSolver->setPivotLimit(mipLimit);
-          mipRes = approxSolver->solveMIP();
-          d_errorSet.reduceToSignals();
-          Message() << "here" << endl;
-          if(mipRes == ApproximateSimplex::ApproxSat){
-            mipSolution = approxSolver->extractMIP();
-            d_qflraStatus = d_attemptSolSimplex.attempt(mipSolution);
-            //d_linEq.applySolution(mipSolution.newBasis, mipSolution.newValues);
-          }else{
+
+          if(d_likelyIntegerInfeasible){
             d_qflraStatus = d_attemptSolSimplex.attempt(relaxSolution);
-            //d_linEq.applySolution(relaxSolution.newBasis, relaxSolution.newValues);
-            // if(d_qflraStatus != UNSAT){
-            //   d_likelyIntegerUnsat = true;
-            // }
+          }else{
+            approxSolver->setPivotLimit(mipLimit);
+            mipRes = approxSolver->solveMIP();
+            d_errorSet.reduceToSignals();
+            //Message() << "here" << endl;
+            if(mipRes == ApproximateSimplex::ApproxSat){
+              mipSolution = approxSolver->extractMIP();
+              d_qflraStatus = d_attemptSolSimplex.attempt(mipSolution);
+            }else{
+              if(mipRes == ApproximateSimplex::ApproxUnsat){
+                d_likelyIntegerInfeasible = true;
+              }
+              d_qflraStatus = d_attemptSolSimplex.attempt(relaxSolution);
+            }
           }
           options::arithStandardCheckVarOrderPivots.set(pass2Limit);
           if(d_qflraStatus != Result::UNSAT){ d_qflraStatus = simplex.findModel(false); }
+          //Message() << "done" << endl;
         }
         break;
       case ApproximateSimplex::ApproxUnsat:
@@ -1624,12 +1631,14 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){
     }
 
     if(d_qflraStatus == Result::SAT_UNKNOWN){
-      Message() << "got sat unknown" << endl;
+      //Message() << "got sat unknown" << endl;
       vector<ArithVar> toCut = cutAllBounded();
       if(toCut.size() > 0){
         branchVector(toCut);
         emmittedConflictOrSplit = true;
       }else{
+        //Message() << "splitting" << endl;
+
         d_qflraStatus = simplex.findModel(noPivotLimit);
       }
     }
@@ -2659,6 +2668,10 @@ bool TheoryArithPrivate::propagateMightSucceed(ArithVar v, bool ub) const{
     ConstraintType t = ub ? UpperBound : LowerBound;
     const DeltaRational& a = d_partialModel.getAssignment(v);
 
+    if(isInteger(v) && !a.isIntegral()){
+      return true;
+    }
+
     Constraint strongestPossible = d_constraintDatabase.getBestImpliedBound(v, t, a);
     if(strongestPossible == NullConstraint){
       return false;
@@ -2754,6 +2767,11 @@ bool TheoryArithPrivate::tryToPropagate(RowIndex ridx, bool rowUp, ArithVar v, b
     d_partialModel.strictlyGreaterThanLowerBound(v, bound);
   if(weaker){
     ConstraintType t = vUb ? UpperBound : LowerBound;
+
+    if(isInteger(v)){
+      //cout << "maybe" << endl;
+      //cout << bound << endl;
+    }
     Constraint implied = d_constraintDatabase.getBestImpliedBound(v, t, bound);
     if(implied != NullConstraint){
       return rowImplicationCanBeApplied(ridx, rowUp, implied);
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index f6fb42a9c..3da064a80 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -570,6 +570,8 @@ private:
   context::CDO<unsigned> d_cutCount;
   context::CDHashSet<ArithVar, std::hash<ArithVar> > d_cutInContext;
 
+  context::CDO<bool> d_likelyIntegerInfeasible;
+
   /** These fields are designed to be accessible to TheoryArith methods. */
   class Statistics {
   public: