From: Tim King <tim.king@imag.fr>
Date: Sat, 13 Jun 2015 14:25:23 +0000 (+0200)
Subject: A return value for an ApproxGLPK::loadVB() failure case was incorrect.
X-Git-Tag: cvc5-1.0.0~6284
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f28e715326669c2524e5dc552ff9eb05e5799f33;p=cvc5.git

A return value for an ApproxGLPK::loadVB() failure case was incorrect.
---

diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp
index 860868df0..5b3c87b3d 100644
--- a/src/theory/arith/approx_simplex.cpp
+++ b/src/theory/arith/approx_simplex.cpp
@@ -2281,6 +2281,7 @@ bool ApproxGLPK::attemptMir(int nid, const MirInfo& mir){
   //return makeCutNodes(nid, mir);
 }
 
+/** Returns true on failure. */
 bool ApproxGLPK::loadVB(int nid, int M, int j, int ri, bool wantUb, VirtualBound& tmp){
   if(ri <= 0) { return true; }
 
@@ -2290,26 +2291,61 @@ bool ApproxGLPK::loadVB(int nid, int M, int j, int ri, bool wantUb, VirtualBound
 
   ArithVar rowVar = _getArithVar(nid, M, ri);
   ArithVar contVar = _getArithVar(nid, M, j);
-  if(rowVar == ARITHVAR_SENTINEL){ return true; }
-  if(contVar == ARITHVAR_SENTINEL){ return true; }
+  if(rowVar == ARITHVAR_SENTINEL){
+    Debug("glpk::loadVB") << "loadVB() " << instance
+                          << " rowVar is ARITHVAR_SENTINEL " << rowVar << endl;
+    return true;
+  }
+  if(contVar == ARITHVAR_SENTINEL){
+    Debug("glpk::loadVB") << "loadVB() " << instance
+                          << " contVar is ARITHVAR_SENTINEL " << contVar << endl;        
+    return true; }
 
-  if(!d_vars.isAuxiliary(rowVar)){ return true; }
+  if(!d_vars.isAuxiliary(rowVar)){
+    Debug("glpk::loadVB") << "loadVB() " << instance
+                          << " rowVar is not auxilliary " << rowVar << endl;    
+    return true;
+  }
   // is integer is correct here
-  if(d_vars.isInteger(contVar)){ return true; }
+  if(d_vars.isInteger(contVar)){
+    Debug("glpk::loadVB") << "loadVB() " << instance
+                          << " contVar is integer " << contVar << endl;    
+    return true;
+  }
 
   ConstraintP lb = d_vars.getLowerBoundConstraint(rowVar);
   ConstraintP ub = d_vars.getUpperBoundConstraint(rowVar);
 
-  if(lb != NullConstraint && ub != NullConstraint){ return true; }
+  if(lb != NullConstraint && ub != NullConstraint){
+    Debug("glpk::loadVB") << "loadVB() " << instance
+                          << " lb and ub are both NULL " << lb << " " << ub << endl;    
+    return true;
+  }
 
   ConstraintP rcon = lb == NullConstraint ? ub : lb;
-  if(rcon == NullConstraint) { return true; }
+  if(rcon == NullConstraint) {
+    Debug("glpk::loadVB") << "loadVB() " << instance
+                          << " rcon is NULL " << rcon << endl;    
+    return true;
+  }
 
-  if(!rcon->getValue().isZero()){ return true; }
+  if(!rcon->getValue().isZero()){
+    Debug("glpk::loadVB") << "loadVB() " << instance
+                          << " rcon value is not 0 " << rcon->getValue() << endl;
+    return true;
+  }
+
+  if(!d_vars.hasNode(rowVar)){
+    Debug("glpk::loadVB") << "loadVB() " << instance
+                          << " does not have node " << rowVar << endl;
+    return true;
+  }
 
-  if(!d_vars.hasNode(rowVar)){ return true; }
   Polynomial p = Polynomial::parsePolynomial(d_vars.asNode(rowVar));
-  if(p.size() != 2) { return false; }
+  if(p.size() != 2) {  
+    Debug("glpk::loadVB") << "loadVB() " << instance << " polynomial is not binary: " << p.getNode() << endl;
+    return true;
+  }
 
   Monomial first = p.getHead(), second = p.getTail().getHead();
   Rational c1 = first.getConstant().getValue();
@@ -2317,8 +2353,16 @@ bool ApproxGLPK::loadVB(int nid, int M, int j, int ri, bool wantUb, VirtualBound
   Node nx1 = first.getVarList().getNode();
   Node nx2 = second.getVarList().getNode();
 
-  if(!d_vars.hasArithVar(nx1)) { return true; }
-  if(!d_vars.hasArithVar(nx2)) { return true; }
+  if(!d_vars.hasArithVar(nx1)) {
+    Debug("glpk::loadVB") << "loadVB() " << instance
+                          << " does not have a variable for nx1: " << nx1 << endl;
+    return true;
+  }
+  if(!d_vars.hasArithVar(nx2)) {
+    Debug("glpk::loadVB") << "loadVB() " << instance
+                          << " does not have a variable for nx2 " << nx2 << endl;
+    return true;
+  }
   ArithVar x1 = d_vars.asArithVar(nx1), x2 = d_vars.asArithVar(nx2);
 
   Assert(x1 != x2);
@@ -2344,7 +2388,11 @@ bool ApproxGLPK::loadVB(int nid, int M, int j, int ri, bool wantUb, VirtualBound
     << " iv " << iv
     << " c2 " << ic << endl;
 
-  if(!d_vars.isIntegerInput(iv)){ return true; }
+  if(!d_vars.isIntegerInput(iv)){
+    Debug("glpk::loadVB") << "loadVB() " << instance
+                          << " iv is not an integer input variable " << iv << endl;    
+    return true;
+  }
   // cc * cv + ic * iv <= 0 or
   // cc * cv + ic * iv <= 0
 
@@ -2366,11 +2414,17 @@ bool ApproxGLPK::loadVB(int nid, int M, int j, int ri, bool wantUb, VirtualBound
   Rational d = -ic/cc;
   Debug("glpk::loadVB") << d << " " << cc.sgn() << endl;
   bool nowUb = cc.sgn() < 0;
-  if(wantUb != nowUb) { return true; }
+  if(wantUb != nowUb) {
+    Debug("glpk::loadVB") << "loadVB() " << instance
+                          << " wantUb is not nowUb " << wantUb << " " << nowUb << endl;    
+    
+    return true;
+  }
 
   Kind rel = wantUb ? kind::LEQ : kind::GEQ;
 
   tmp = VirtualBound(contVar, rel, d, iv, rcon);
+    Debug("glpk::loadVB") << "loadVB() " << instance << " was successful" << endl;    
   return false;
 }