From eec3e4b96a5ba3a0acfa22d4cd8896d9a5ea66c8 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Wed, 3 Nov 2010 18:46:46 +0000
Subject: [PATCH] Adds size() to RowVector.

---
 src/theory/arith/row_vector.h | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/src/theory/arith/row_vector.h b/src/theory/arith/row_vector.h
index efb64d1c7..a967f8d68 100644
--- a/src/theory/arith/row_vector.h
+++ b/src/theory/arith/row_vector.h
@@ -73,13 +73,16 @@ protected:
 
 public:
 
-  //RowVector() : d_entries() {}
-
   RowVector(const std::vector< ArithVar >& variables,
             const std::vector< Rational >& coefficients,
             std::vector<uint32_t>& counts);
 
 
+  /** Returns the number of nonzero variables in the vector. */
+  uint32_t size() const {
+    return d_entries.size();
+  }
+
   //Iterates over the nonzero entries in the Vector
   NonZeroIterator beginNonZero() const { return d_entries.begin(); }
   NonZeroIterator endNonZero() const { return d_entries.end(); }
-- 
2.30.2