From: Tim King <taking@cs.nyu.edu>
Date: Thu, 17 Feb 2011 18:00:30 +0000 (+0000)
Subject: Removed ActivityMonitor from arithmetic. This was only used for row ejection, and... 
X-Git-Tag: cvc5-1.0.0~8703
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bb58835b6967953d1e5df3d79bda6b67bc0bb8b7;p=cvc5.git

Removed ActivityMonitor from arithmetic. This was only used for row ejection, and is now superfluous.
---

diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index c8532f1a2..6a9102a19 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -56,9 +56,6 @@ inline void setArithVar(TNode x, ArithVar a){
   return x.setAttribute(ArithVarAttr(), (uint64_t)a);
 }
 
-typedef std::vector<uint64_t> ActivityMonitor;
-
-
 inline Node mkRationalNode(const Rational& q){
   return NodeManager::currentNM()->mkConst<Rational>(q);
 }
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index 9e3ba726a..6e7685570 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -129,7 +129,6 @@ bool SimplexDecisionProcedure::AssertLower(ArithVar x_i, const DeltaRational& c_
 
   d_partialModel.setLowerConstraint(x_i,original);
   d_partialModel.setLowerBound(x_i, c_i);
-  d_activityMonitor[x_i] = 0;
 
   if(!d_basicManager.isMember(x_i)){
     if(d_partialModel.getAssignment(x_i) < c_i){
@@ -167,8 +166,6 @@ bool SimplexDecisionProcedure::AssertUpper(ArithVar x_i, const DeltaRational& c_
   d_partialModel.setUpperConstraint(x_i,original);
   d_partialModel.setUpperBound(x_i, c_i);
 
-  d_activityMonitor[x_i] = 0;
-
   if(!d_basicManager.isMember(x_i)){
     if(d_partialModel.getAssignment(x_i) > c_i){
       update(x_i, c_i);
@@ -220,7 +217,6 @@ bool SimplexDecisionProcedure::AssertEquality(ArithVar x_i, const DeltaRational&
 
   d_partialModel.setUpperConstraint(x_i,original);
   d_partialModel.setUpperBound(x_i, c_i);
-  d_activityMonitor[x_i] = 0;
 
   if(!d_basicManager.isMember(x_i)){
     if(!(d_partialModel.getAssignment(x_i) == c_i)){
@@ -255,8 +251,6 @@ void SimplexDecisionProcedure::update(ArithVar x_i, const DeltaRational& v){
       DeltaRational  nAssignment = assignment+(diff * a_ji);
       d_partialModel.setAssignment(x_j, nAssignment);
 
-      d_activityMonitor[x_j] += 1;
-
       checkBasicVariable(x_j);
     }
   }
@@ -322,8 +316,6 @@ void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaR
       DeltaRational nextAssignment = d_partialModel.getAssignment(x_k) + (theta * a_kj);
       d_partialModel.setAssignment(x_k, nextAssignment);
 
-      d_activityMonitor[x_j] += 1;
-
       checkBasicVariable(x_k);
     }
   }
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index 7589e7936..e02e001e3 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -56,11 +56,9 @@ private:
   ArithPartialModel& d_partialModel;
 
   ArithVarSet& d_basicManager;
-  ActivityMonitor& d_activityMonitor;
 
   OutputChannel* d_out;
 
-
   Tableau& d_tableau;
 
   ArithVar d_numVariables;
@@ -72,13 +70,11 @@ public:
                            ArithPartialModel& pm,
                            ArithVarSet& bm,
                            OutputChannel* out,
-                           ActivityMonitor& am,
                            Tableau& tableau) :
     d_possiblyInconsistent(),
     d_constants(constants),
     d_partialModel(pm),
     d_basicManager(bm),
-    d_activityMonitor(am),
     d_out(out),
     d_tableau(tableau),
     d_numVariables(0),
diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp
index 95ea166af..75363af7f 100644
--- a/src/theory/arith/tableau.cpp
+++ b/src/theory/arith/tableau.cpp
@@ -101,7 +101,6 @@ void Tableau::pivot(ArithVar x_r, ArithVar x_s){
 
     ReducedRowVector& row_k = lookup(basic);
     if(row_k.has(x_s)){
-      d_activityMonitor[basic] += 30;
       row_k.substitute(*row_s);
     }
   }
diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index 5f2a36505..f74e662cf 100644
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -45,8 +45,6 @@ private:
   ArithVarSet d_activeBasicVars;
   RowsTable d_rowsTable;
 
-
-  ActivityMonitor& d_activityMonitor;
   ArithVarSet& d_basicManager;
 
   std::vector<uint32_t> d_rowCount;
@@ -55,10 +53,9 @@ public:
   /**
    * Constructs an empty tableau.
    */
-  Tableau(ActivityMonitor &am, ArithVarSet& bm) :
+  Tableau(ArithVarSet& bm) :
     d_activeBasicVars(),
     d_rowsTable(),
-    d_activityMonitor(am),
     d_basicManager(bm)
   {}
 
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index ecc740655..ca3b76410 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -59,11 +59,10 @@ TheoryArith::TheoryArith(context::Context* c, OutputChannel& out) :
   d_partialModel(c),
   d_basicManager(),
   d_userVariables(),
-  d_activityMonitor(),
   d_diseq(c),
-  d_tableau(d_activityMonitor, d_basicManager),
+  d_tableau(d_basicManager),
   d_propagator(c, out),
-  d_simplex(d_constants, d_partialModel, d_basicManager,  d_out, d_activityMonitor, d_tableau),
+  d_simplex(d_constants, d_partialModel, d_basicManager,  d_out, d_tableau),
   d_statistics()
 {}
 
@@ -262,9 +261,6 @@ ArithVar TheoryArith::requestArithVar(TNode x, bool basic){
 
   setArithVar(x,varX);
 
-  Assert(varX == d_activityMonitor.size());
-  d_activityMonitor.push_back(0);
-
   d_basicManager.init(varX,basic);
   d_userVariables.init(varX, !basic);
   d_tableau.increaseSize();
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index fa60b5fcf..fd3cf0c45 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -86,7 +86,6 @@ private:
 
   ArithVarSet d_basicManager;
   ArithVarSet d_userVariables;
-  ActivityMonitor d_activityMonitor;
 
   /**
    * List of all of the inequalities asserted in the current context.