Merging the branch branches/arithmetic/shared-terms into trunk. Arithmetic now supports propagating equalities when a slack variable corresponding to a difference of shared terms must be 0. Similarly disequalities are propagated when these variables cannot be zero.

11 files changed, 358 insertions, 26 deletions

diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am
index 36ab2cd68..4ca8aff0b 100644
--- a/src/theory/arith/Makefile.am
+++ b/src/theory/arith/Makefile.am
@@ -16,6 +16,8 @@ libarith_la_SOURCES = \
 	arithvar_node_map.h \
 	atom_database.h \
 	atom_database.cpp \
+	difference_manager.h \
+	difference_manager.cpp \
 	normal_form.h\
 	normal_form.cpp \
 	arith_utilities.h \
diff --git a/src/theory/arith/arith_prop_manager.cpp b/src/theory/arith/arith_prop_manager.cpp
index d1fce5b90..6d2e04de1 100644
--- a/src/theory/arith/arith_prop_manager.cpp
+++ b/src/theory/arith/arith_prop_manager.cpp
@@ -135,7 +135,7 @@ bool ArithPropManager::propagateArithVar(bool upperbound, ArithVar var, const De
     bool asserted = isAsserted(bestImplied);
 
     if( !asserted && !isPropagated(bestImplied)){
-      propagate(bestImplied, reason);
+      propagate(bestImplied, reason, false);
       ++d_statistics.d_addedPropagation;
       success = true;
     }else if(!asserted){
diff --git a/src/theory/arith/arith_prop_manager.h b/src/theory/arith/arith_prop_manager.h
index 82f58c7a0..912c4fdf8 100644
--- a/src/theory/arith/arith_prop_manager.h
+++ b/src/theory/arith/arith_prop_manager.h
@@ -39,36 +39,55 @@ namespace theory {
 namespace arith {
 
 class PropManager {
+public:
+  struct PropUnit {
+    // consequent <= antecedent
+    Node consequent;
+    Node antecedent;
+    bool flag;
+    PropUnit(Node c, Node a, bool f) :
+      consequent(c), antecedent(a), flag(f)
+    {}
+  };
+
 private:
-  context::CDList<TNode> d_propagated;
+  context::CDList<PropUnit> d_propagated;
+
   context::CDO<uint32_t> d_propagatedPos;
-  typedef context::CDMap<TNode, TNode, TNodeHashFunction> ExplainMap;
+  typedef context::CDMap<Node, size_t, NodeHashFunction> ExplainMap;
 
   ExplainMap d_explanationMap;
 
-  context::CDList<Node> d_reasons;
+  size_t getIndex(TNode n) const {
+    Assert(isPropagated(n));
+    return (*(d_explanationMap.find(n))).second;
+  }
 
 public:
 
   PropManager(context::Context* c):
     d_propagated(c),
     d_propagatedPos(c, 0),
-    d_explanationMap(c),
-    d_reasons(c)
+    d_explanationMap(c)
   { }
 
+  const PropUnit& getUnit(TNode n) const {
+    return d_propagated[getIndex(n)];
+  }
+
   bool isPropagated(TNode n) const {
     return d_explanationMap.find(n) != d_explanationMap.end();
   }
 
-  void propagate(TNode n, Node reason) {
-    Assert(!isPropagated(n));
-    Assert(reason.getKind() == kind::AND);
+  bool isFlagged(TNode n) const {
+    return getUnit(n).flag;
+  }
 
-    d_explanationMap.insert(n, reason);
+  void propagate(TNode n, Node reason, bool flag) {
+    Assert(!isPropagated(n));
 
-    d_reasons.push_back(reason);
-    d_propagated.push_back(n);
+    d_explanationMap.insert(n, d_propagated.size());
+    d_propagated.push_back(PropUnit(n, reason, flag));
 
     Debug("ArithPropManager") << n  << std::endl << "<="<< reason<< std::endl;
   }
@@ -77,17 +96,15 @@ public:
     return d_propagatedPos < d_propagated.size();
   }
 
-  TNode getPropagation() {
+  const PropUnit& getNextPropagation() {
     Assert(hasMorePropagations());
-    TNode prop = d_propagated[d_propagatedPos];
+    const PropUnit& prop = d_propagated[d_propagatedPos];
     d_propagatedPos = d_propagatedPos + 1;
     return prop;
   }
 
   TNode explain(TNode n) const {
-    Assert(isPropagated(n));
-    ExplainMap::iterator p = d_explanationMap.find(n);
-    return (*p).second;
+    return getUnit(n).antecedent;
   }
 
 };/* class PropManager */
diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h
index c8a5e39a7..fdc3bee3b 100644
--- a/src/theory/arith/delta_rational.h
+++ b/src/theory/arith/delta_rational.h
@@ -54,6 +54,15 @@ public:
     return c;
   }
 
+  int sgn() const {
+    int x = getNoninfinitesimalPart().sgn();
+    if(x == 0){
+      return getInfinitesimalPart().sgn();
+    }else{
+      return x;
+    }
+  }
+
   DeltaRational operator+(const DeltaRational& other) const{
     CVC4::Rational tmpC = c+other.c;
     CVC4::Rational tmpK = k+other.k;
diff --git a/src/theory/arith/difference_manager.cpp b/src/theory/arith/difference_manager.cpp
new file mode 100644
index 000000000..dfb07bcf4
--- /dev/null
+++ b/src/theory/arith/difference_manager.cpp
@@ -0,0 +1,102 @@
+#include "theory/arith/difference_manager.h"
+#include "theory/uf/equality_engine_impl.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+DifferenceManager::DifferenceManager(context::Context* c, PropManager& pm)
+  : d_reasons(c),
+    d_queue(pm),
+    d_notify(*this),
+    d_ee(d_notify, c, "theory::arith::DifferenceManager"),
+    d_false(NodeManager::currentNM()->mkConst<bool>(false))
+{}
+
+void DifferenceManager::propagate(TNode x){
+  Debug("arith::differenceManager")<< "DifferenceManager::propagate("<<x<<")"<<std::endl;
+
+  d_queue.propagate(x, Node::null(), true);
+}
+
+void DifferenceManager::explain(TNode literal, std::vector<TNode>& assumptions) {
+  TNode lhs, rhs;
+  switch (literal.getKind()) {
+    case kind::EQUAL:
+      lhs = literal[0];
+      rhs = literal[1];
+      break;
+    case kind::NOT:
+      lhs = literal[0];
+      rhs = d_false;
+      break;
+    default:
+      Unreachable();
+  }
+  d_ee.getExplanation(lhs, rhs, assumptions);
+}
+
+#warning "Stolen from theory_uf.h verbatim. Generalize me!"
+Node mkAnd(const std::vector<TNode>& conjunctions) {
+  Assert(conjunctions.size() > 0);
+
+  std::set<TNode> all;
+  all.insert(conjunctions.begin(), conjunctions.end());
+
+  if (all.size() == 1) {
+    // All the same, or just one
+    return conjunctions[0];
+  }
+
+  NodeBuilder<> conjunction(kind::AND);
+  std::set<TNode>::const_iterator it = all.begin();
+  std::set<TNode>::const_iterator it_end = all.end();
+  while (it != it_end) {
+    conjunction << *it;
+    ++ it;
+  }
+
+  return conjunction;
+}
+
+
+Node DifferenceManager::explain(TNode lit){
+  std::vector<TNode> assumptions;
+  explain(lit, assumptions);
+  return mkAnd(assumptions);
+}
+
+void DifferenceManager::addDifference(ArithVar s, Node x, Node y){
+  Assert(s >= d_differences.size() || !isDifferenceSlack(s));
+
+  Debug("arith::differenceManager") << s << x << y << std::endl;
+
+  d_differences.resize(s+1);
+  d_differences[s] = Difference(x,y);
+}
+
+void DifferenceManager::differenceIsZero(ArithVar s, TNode reason){
+  Assert(isDifferenceSlack(s));
+  TNode x = d_differences[s].x;
+  TNode y = d_differences[s].y;
+
+  d_reasons.push_back(reason);
+  d_ee.addEquality(x, y, reason);
+}
+
+void DifferenceManager::differenceCannotBeZero(ArithVar s, TNode reason){
+  Assert(isDifferenceSlack(s));
+  TNode x = d_differences[s].x;
+  TNode y = d_differences[s].y;
+
+  d_reasons.push_back(reason);
+  d_ee.addDisequality(x, y, reason);
+}
+
+void DifferenceManager::addSharedTerm(Node x){
+  d_ee.addTriggerTerm(x);
+}
+
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/arith/difference_manager.h b/src/theory/arith/difference_manager.h
new file mode 100644
index 000000000..01f42dcfe
--- /dev/null
+++ b/src/theory/arith/difference_manager.h
@@ -0,0 +1,95 @@
+
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__ARITH__DIFFERENCE_MANAGER_H
+#define __CVC4__THEORY__ARITH__DIFFERENCE_MANAGER_H
+
+#include "theory/arith/arith_utilities.h"
+#include "theory/uf/equality_engine.h"
+#include "context/cdo.h"
+#include "context/cdlist.h"
+#include "context/context.h"
+#include "util/stats.h"
+#include "theory/arith/arith_prop_manager.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+class DifferenceManager {
+private:
+  struct Difference {
+    bool isSlack;
+    TNode x;
+    TNode y;
+    Difference() : isSlack(false), x(TNode::null()),  y(TNode::null()){}
+    Difference(TNode a, TNode b) : isSlack(true), x(a), y(b) {
+      Assert(x < y);
+    }
+  };
+
+
+  class DifferenceNotifyClass {
+  private:
+    DifferenceManager& d_dm;
+  public:
+    DifferenceNotifyClass(DifferenceManager& dm): d_dm(dm) {}
+
+    bool notify(TNode propagation) {
+      Debug("arith::differences") << "DifferenceNotifyClass::notify(" << propagation << ")" << std::endl;
+      // Just forward to dm
+      d_dm.propagate(propagation);
+      return true;
+    }
+
+    void notify(TNode t1, TNode t2) {
+      Debug("arith::differences") << "DifferenceNotifyClass::notify(" << t1 << ", " << t2 << ")" << std::endl;
+      Node equality = t1.eqNode(t2);
+      d_dm.propagate(equality);
+    }
+  };
+
+  std::vector< Difference > d_differences;
+
+  context::CDList<Node> d_reasons;
+  PropManager& d_queue;
+
+
+  DifferenceNotifyClass d_notify;
+  theory::uf::EqualityEngine<DifferenceNotifyClass> d_ee;
+
+  void propagate(TNode x);
+  void explain(TNode literal, std::vector<TNode>& assumptions);
+
+  Node d_false;
+
+public:
+
+  DifferenceManager(context::Context*, PropManager&);
+
+  Node explain(TNode literal);
+
+  void addDifference(ArithVar s, Node x, Node y);
+
+  inline bool isDifferenceSlack(ArithVar s) const{
+    if(s < d_differences.size()){
+      return d_differences[s].isSlack;
+    }else{
+      return false;
+    }
+  }
+
+  void differenceIsZero(ArithVar s, TNode reason);
+
+  void differenceCannotBeZero(ArithVar s, TNode reason);
+
+  void addSharedTerm(Node x);
+};/* class DifferenceManager */
+
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__ARITH__DIFFERENCE_MANAGER_H */
+
diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp
index ed8f837d1..73f80a70d 100644
--- a/src/theory/arith/partial_model.cpp
+++ b/src/theory/arith/partial_model.cpp
@@ -27,19 +27,52 @@ using namespace CVC4;
 using namespace CVC4::theory;
 using namespace CVC4::theory::arith;
 
+
+
+void ArithPartialModel::zeroDifferenceDetected(ArithVar x){
+  Assert(d_dm.isDifferenceSlack(x));
+  Assert(upperBoundIsZero(x));
+  Assert(lowerBoundIsZero(x));
+
+  Node lb = getLowerConstraint(x);
+  Node ub = getUpperConstraint(x);
+  Node reason = lb != ub ? lb.andNode(ub) : lb;
+  d_dm.differenceIsZero(x, reason);
+}
+
 void ArithPartialModel::setUpperBound(ArithVar x, const DeltaRational& r){
   d_deltaIsSafe = false;
 
   Debug("partial_model") << "setUpperBound(" << x << "," << r << ")" << endl;
   d_hasHadABound[x] = true;
   d_upperBound.set(x,r);
+
+  if(d_dm.isDifferenceSlack(x)){
+    int sgn = r.sgn();
+    if(sgn < 0){
+      d_dm.differenceCannotBeZero(x, getUpperConstraint(x));
+    }else if(sgn == 0 && lowerBoundIsZero(x)){
+      zeroDifferenceDetected(x);
+    }
+  }
 }
 
 void ArithPartialModel::setLowerBound(ArithVar x, const DeltaRational& r){
   d_deltaIsSafe = false;
 
+  Debug("partial_model") << "setLowerBound(" << x << "," << r << ")" << endl;
   d_hasHadABound[x] = true;
   d_lowerBound.set(x,r);
+
+
+  if(d_dm.isDifferenceSlack(x)){
+    int sgn = r.sgn();
+    if(sgn > 0){
+      d_dm.differenceCannotBeZero(x, getLowerConstraint(x));
+    }else if(sgn == 0 && upperBoundIsZero(x)){
+      zeroDifferenceDetected(x);
+    }
+  }
 }
 
 void ArithPartialModel::setAssignment(ArithVar x, const DeltaRational& r){
diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index 9c5e343ef..6e85f7e80 100644
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -26,6 +26,8 @@
 #include "expr/attribute.h"
 #include "expr/node.h"
 
+#include "theory/arith/difference_manager.h"
+
 #include <deque>
 
 #ifndef __CVC4__THEORY__ARITH__PARTIAL_MODEL_H
@@ -52,6 +54,7 @@ private:
   context::CDVector<Node> d_upperConstraint;
   context::CDVector<Node> d_lowerConstraint;
 
+
   bool d_deltaIsSafe;
   Rational d_delta;
 
@@ -61,9 +64,11 @@ private:
   typedef std::vector<ArithVar> HistoryList;
   HistoryList d_history;
 
+  DifferenceManager& d_dm;
+
 public:
 
-  ArithPartialModel(context::Context* c):
+  ArithPartialModel(context::Context* c, DifferenceManager& dm):
     d_mapSize(0),
     d_hasHadABound(),
     d_hasSafeAssignment(),
@@ -75,7 +80,8 @@ public:
     d_lowerConstraint(c,true),
     d_deltaIsSafe(false),
     d_delta(-1,1),
-    d_history()
+    d_history(),
+    d_dm(dm)
   { }
 
   void setLowerConstraint(ArithVar x, TNode constraint);
@@ -98,6 +104,18 @@ public:
   void commitAssignmentChanges();
 
 
+  inline bool lowerBoundIsZero(ArithVar x){
+    return hasLowerBound(x) && getLowerBound(x).sgn() == 0;
+  }
+
+  inline bool upperBoundIsZero(ArithVar x){
+    return hasUpperBound(x) && getUpperBound(x).sgn() == 0;
+  }
+
+private:
+  void zeroDifferenceDetected(ArithVar x);
+
+public:
 
 
   void setUpperBound(ArithVar x, const DeltaRational& r);
@@ -114,6 +132,7 @@ public:
   const DeltaRational& getAssignment(ArithVar x) const;
 
 
+
   /**
    * x >= l
    * ? c < l
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index 77e7e1060..27fb0bb02 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -339,7 +339,7 @@ bool SimplexDecisionProcedure::propagateCandidateBound(ArithVar basic, bool uppe
           explainNonbasicsLowerBound(basic, nb);
         }
         Node explanation = nb;
-        d_propManager.propagate(bestImplied, explanation);
+        d_propManager.propagate(bestImplied, explanation, false);
         return true;
       }else{
         Debug("arith::prop") << basic << " " << asserted << " " << propagated << endl;
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 289d5ace4..53559d949 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -61,7 +61,7 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha
   d_atomsInContext(c),
   d_learner(d_pbSubstitutions),
   d_nextIntegerCheckVar(0),
-  d_partialModel(c),
+  d_partialModel(c, d_differenceManager),
   d_userVariables(),
   d_diseq(c),
   d_tableau(),
@@ -73,6 +73,7 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha
   d_tableauResetPeriod(10),
   d_atomDatabase(c, out),
   d_propManager(c, d_arithvarNodeMap, d_atomDatabase, valuation),
+  d_differenceManager(c, d_propManager),
   d_simplex(d_propManager, d_partialModel, d_tableau),
   d_DELTA_ZERO(0),
   d_statistics()
@@ -89,6 +90,7 @@ TheoryArith::Statistics::Statistics():
   d_staticLearningTimer("theory::arith::staticLearningTimer"),
   d_permanentlyRemovedVariables("theory::arith::permanentlyRemovedVariables", 0),
   d_presolveTime("theory::arith::presolveTime"),
+  d_externalBranchAndBounds("theory::arith::externalBranchAndBounds",0),
   d_initialTableauSize("theory::arith::initialTableauSize", 0),
   d_currSetToSmaller("theory::arith::currSetToSmaller", 0),
   d_smallerSetToCurr("theory::arith::smallerSetToCurr", 0),
@@ -104,6 +106,7 @@ TheoryArith::Statistics::Statistics():
   StatisticsRegistry::registerStat(&d_permanentlyRemovedVariables);
   StatisticsRegistry::registerStat(&d_presolveTime);
 
+  StatisticsRegistry::registerStat(&d_externalBranchAndBounds);
 
   StatisticsRegistry::registerStat(&d_initialTableauSize);
   StatisticsRegistry::registerStat(&d_currSetToSmaller);
@@ -122,6 +125,7 @@ TheoryArith::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_permanentlyRemovedVariables);
   StatisticsRegistry::unregisterStat(&d_presolveTime);
 
+  StatisticsRegistry::unregisterStat(&d_externalBranchAndBounds);
 
   StatisticsRegistry::unregisterStat(&d_initialTableauSize);
   StatisticsRegistry::unregisterStat(&d_currSetToSmaller);
@@ -129,6 +133,11 @@ TheoryArith::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_restartTimer);
 }
 
+
+void TheoryArith::addSharedTerm(TNode n){
+  d_differenceManager.addSharedTerm(n);
+}
+
 Node TheoryArith::preprocess(TNode atom) {
   Debug("arith::preprocess") << "arith::preprocess() : " << atom << endl;
 
@@ -332,6 +341,26 @@ void TheoryArith::setupPolynomial(const Polynomial& poly) {
     d_tableau.addRow(varSlack, coefficients, variables);
     setupInitialValue(varSlack);
 
+    //Add differences to the difference manager
+    Polynomial::iterator i = poly.begin(), end = poly.end();
+    if(i != end){
+      Monomial first = *i;
+      ++i;
+      if(i != end){
+        Monomial second = *i;
+        ++i;
+        if(i == end){
+          if(first.getConstant().isOne() && second.getConstant().getValue() == -1){
+            VarList vl0 = first.getVarList();
+            VarList vl1 = second.getVarList();
+            if(vl0.singleton() && vl1.singleton()){
+              d_differenceManager.addDifference(varSlack, vl0.getNode(), vl1.getNode());
+            }
+          }
+        }
+      }
+    }
+
     ++(d_statistics.d_statSlackVariables);
     markSetup(polyNode);
   }
@@ -718,6 +747,7 @@ void TheoryArith::check(Effort effortLevel){
             } else {
               Debug("integers") << "    " << lem[1] << " is not assigned a SAT literal" << endl;
             }
+            ++(d_statistics.d_externalBranchAndBounds);
             d_out->lemma(lem);
 
             // split only on one var
@@ -743,6 +773,7 @@ void TheoryArith::check(Effort effortLevel){
             } else {
               Debug("integers") << "    " << lem[1] << " is not assigned a SAT literal" << endl;
             }
+            ++(d_statistics.d_externalBranchAndBounds);
             d_out->lemma(lem);
 
             // split only on one var
@@ -771,6 +802,7 @@ void TheoryArith::check(Effort effortLevel){
           } else {
             Debug("integers") << "    " << lem[1] << " is not assigned a SAT literal" << endl;
           }
+          ++(d_statistics.d_externalBranchAndBounds);
           d_out->lemma(lem);
 
           // split only on one var
@@ -849,7 +881,12 @@ void TheoryArith::debugPrintModel(){
 Node TheoryArith::explain(TNode n) {
   Debug("explain") << "explain @" << getContext()->getLevel() << ": " << n << endl;
   Assert(d_propManager.isPropagated(n));
-  return d_propManager.explain(n);
+
+  if(d_propManager.isFlagged(n)){
+    return d_differenceManager.explain(n);
+  }else{
+    return d_propManager.explain(n);
+  }
 }
 
 void TheoryArith::propagate(Effort e) {
@@ -862,9 +899,20 @@ void TheoryArith::propagate(Effort e) {
     }
 
     while(d_propManager.hasMorePropagations()){
-      TNode toProp = d_propManager.getPropagation();
+      const PropManager::PropUnit next = d_propManager.getNextPropagation();
+      bool flag = next.flag;
+      TNode toProp = next.consequent;
+
       TNode atom = (toProp.getKind() == kind::NOT) ? toProp[0] : toProp;
-      if(inContextAtom(atom)){
+
+      Debug("arith::propagate") << "propagate " << flag << " " << toProp << endl;
+
+      if(flag) {
+        //Currently if the flag is set this came from an equality detected by the
+        //equality engine in the the difference manager.
+        d_out->propagate(toProp);
+        propagated = true;
+      }else if(inContextAtom(atom)){
         Node satValue = d_valuation.getSatValue(toProp);
         AlwaysAssert(satValue.isNull());
         propagated = true;
@@ -872,7 +920,7 @@ void TheoryArith::propagate(Effort e) {
       }else{
         //Not clear if this is a good time to do this or not...
         Debug("arith::propagate") << "Atom is not in context" << toProp << endl;
-        #warning "enable remove atom in database"
+#warning "enable remove atom in database"
         //d_atomDatabase.removeAtom(atom);
       }
     }
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index e8d920084..6255efbbc 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -39,6 +39,7 @@
 #include "theory/arith/arith_prop_manager.h"
 #include "theory/arith/arithvar_node_map.h"
 #include "theory/arith/dio_solver.h"
+#include "theory/arith/difference_manager.h"
 
 #include "util/stats.h"
 
@@ -196,9 +197,11 @@ private:
   /** This manager keeps track of information needed to propagate. */
   ArithPropManager d_propManager;
 
+  /** This keeps track of difference equalities. Mostly for sharing. */
+  DifferenceManager d_differenceManager;
+
   /** This implements the Simplex decision procedure. */
   SimplexDecisionProcedure d_simplex;
-
 public:
   TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation);
   virtual ~TheoryArith();
@@ -228,6 +231,8 @@ public:
 
   EqualityStatus getEqualityStatus(TNode a, TNode b);
 
+  void addSharedTerm(TNode n);
+
 private:
   /** The constant zero. */
   DeltaRational d_DELTA_ZERO;
@@ -329,6 +334,8 @@ private:
     IntStat d_permanentlyRemovedVariables;
     TimerStat d_presolveTime;
 
+    IntStat d_externalBranchAndBounds;
+
     IntStat d_initialTableauSize;
     IntStat d_currSetToSmaller;
     IntStat d_smallerSetToCurr;