diff options
| author | Tim King <taking@cs.nyu.edu> | 2011-02-17 18:00:30 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2011-02-17 18:00:30 +0000 |
| commit | bb58835b6967953d1e5df3d79bda6b67bc0bb8b7 (patch) | |
| tree | 464d4c787d272578c640532a2086346137b975a0 /src/theory/arith/tableau.h | |
| parent | 907850f58916c4a6890156a08301a68b5be43fcb (diff) | |
Removed ActivityMonitor from arithmetic. This was only used for row ejection, and is now superfluous.
Diffstat (limited to 'src/theory/arith/tableau.h')
| -rw-r--r-- | src/theory/arith/tableau.h | 5 |
1 files changed, 1 insertions, 4 deletions
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) {} |