From bb58835b6967953d1e5df3d79bda6b67bc0bb8b7 Mon Sep 17 00:00:00 2001 From: Tim King Date: Thu, 17 Feb 2011 18:00:30 +0000 Subject: [PATCH] Removed ActivityMonitor from arithmetic. This was only used for row ejection, and is now superfluous. --- src/theory/arith/arith_utilities.h | 3 --- src/theory/arith/simplex.cpp | 8 -------- src/theory/arith/simplex.h | 4 ---- src/theory/arith/tableau.cpp | 1 - src/theory/arith/tableau.h | 5 +---- src/theory/arith/theory_arith.cpp | 8 ++------ src/theory/arith/theory_arith.h | 1 - 7 files changed, 3 insertions(+), 27 deletions(-) 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 ActivityMonitor; - - inline Node mkRationalNode(const Rational& q){ return NodeManager::currentNM()->mkConst(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 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. -- 2.30.2