Changes:

- ArithVar is no longer an attribute
- RowVector's destructor reduces the row count of its variables upon.
- Tableau's destructor now free its rows instead of leaking memory.
- Added ability to convert ReducedRowVectors into equivalent Nodes.
- getValue() should work again.

1 files changed, 8 insertions, 0 deletions

diff --git a/src/theory/arith/row_vector.h b/src/theory/arith/row_vector.h
index 05ceeb986..2b48564a4 100644
--- a/src/theory/arith/row_vector.h
+++ b/src/theory/arith/row_vector.h
@@ -89,6 +89,7 @@ public:
             const std::vector< Rational >& coefficients,
             std::vector<uint32_t>& counts);
 
+  ~RowVector();
 
   /** Returns the number of nonzero variables in the vector. */
   uint32_t size() const {
@@ -195,6 +196,13 @@ public:
   void pivot(ArithVar x_j);
 
   void substitute(const ReducedRowVector& other);
+
+  /**
+   * Returns the reduced row as an equality with
+   * the basic variable on the lhs equal to the sum of the non-basics variables.
+   * The mapped from ArithVars to Nodes is specificied by map.
+   */
+  Node asEquality(const ArithVarToNodeMap& map) const;
 }; /* class ReducedRowVector */