Merged the branch sparse-tableau into trunk.

1 files changed, 287 insertions, 80 deletions

diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index 31f7cfa5a..fa227757a 100644
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -25,10 +25,9 @@
 #include "theory/arith/arithvar_set.h"
 #include "theory/arith/normal_form.h"
 
-#include "theory/arith/row_vector.h"
-
-#include <ext/hash_map>
-#include <set>
+#include <queue>
+#include <vector>
+#include <utility>
 
 #ifndef __CVC4__THEORY__ARITH__TABLEAU_H
 #define __CVC4__THEORY__ARITH__TABLEAU_H
@@ -37,38 +36,229 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
-typedef PermissiveBackArithVarSet Column;
+typedef uint32_t EntryID;
+#define ENTRYID_SENTINEL std::numeric_limits<ArithVar>::max()
+
+class TableauEntry {
+private:
+  ArithVar d_rowVar;
+  ArithVar d_colVar;
+
+  EntryID d_nextRow;
+  EntryID d_nextCol;
+
+  EntryID d_prevRow;
+  EntryID d_prevCol;
+
+  Rational d_coefficient;
+
+public:
+  TableauEntry():
+    d_rowVar(ARITHVAR_SENTINEL),
+    d_colVar(ARITHVAR_SENTINEL),
+    d_nextRow(ENTRYID_SENTINEL),
+    d_nextCol(ENTRYID_SENTINEL),
+    d_prevRow(ENTRYID_SENTINEL),
+    d_prevCol(ENTRYID_SENTINEL),
+    d_coefficient(0)
+  {}
+
+  TableauEntry(ArithVar row, ArithVar col,
+               EntryID nextRowEntry, EntryID nextColEntry,
+               EntryID prevRowEntry, EntryID prevColEntry,
+               const Rational& coeff):
+    d_rowVar(row),
+    d_colVar(col),
+    d_nextRow(nextRowEntry),
+    d_nextCol(nextColEntry),
+    d_prevRow(prevRowEntry),
+    d_prevCol(prevColEntry),
+    d_coefficient(coeff)
+  {}
+
+private:
+  bool unusedConsistent() const {
+    return
+      (d_rowVar == ARITHVAR_SENTINEL && d_colVar == ARITHVAR_SENTINEL) ||
+      (d_rowVar != ARITHVAR_SENTINEL && d_colVar != ARITHVAR_SENTINEL);
+  }
+
+public:
+
+  EntryID getNextRowID() const {
+    return d_nextRow;
+  }
+
+  EntryID getNextColID() const {
+    return d_nextCol;
+  }
+  EntryID getPrevRowID() const {
+    return d_prevRow;
+  }
+
+  EntryID getPrevColID() const {
+    return d_prevCol;
+  }
+
+  void setNextRowID(EntryID id) {
+    d_nextRow = id;
+  }
+  void setNextColID(EntryID id) {
+    d_nextCol = id;
+  }
+  void setPrevRowID(EntryID id) {
+    d_prevRow = id;
+  }
+  void setPrevColID(EntryID id) {
+    d_prevCol = id;
+  }
+
+  void setRowVar(ArithVar newRowVar){
+    d_rowVar = newRowVar;
+  }
+
+  ArithVar getRowVar() const{
+    return d_rowVar;
+  }
+  ArithVar getColVar() const{
+    return d_colVar;
+  }
+
+  const Rational& getCoefficient() const {
+    return d_coefficient;
+  }
+
+  Rational& getCoefficient(){
+    return d_coefficient;
+  }
+
+  void markBlank() {
+    d_rowVar = ARITHVAR_SENTINEL;
+    d_colVar = ARITHVAR_SENTINEL;
+  }
+
+  bool blank() const{
+    Assert(unusedConsistent());
+
+    return d_rowVar == ARITHVAR_SENTINEL;
+  }
+};
+
+class TableauEntryManager {
+private:
+  typedef std::vector<TableauEntry> EntryArray;
+
+  EntryArray d_entries;
+  std::queue<EntryID> d_freedEntries;
+
+  uint32_t d_size;
+
+public:
+  TableauEntryManager():
+    d_entries(), d_freedEntries(), d_size(0)
+  {}
+
+  const TableauEntry& get(EntryID id) const{
+    Assert(inBounds(id));
+    return d_entries[id];
+  }
+
+  TableauEntry& get(EntryID id){
+    Assert(inBounds(id));
+    return d_entries[id];
+  }
+
+  void freeEntry(EntryID id);
+
+  EntryID newEntry();
 
-typedef std::vector<Column> ColumnMatrix;
+  uint32_t size() const{ return d_size; }
+  uint32_t capacity() const{ return d_entries.capacity(); }
+
+
+private:
+  bool inBounds(EntryID id) const{
+    return id <  d_entries.size();
+  }
+};
 
 class Tableau {
 private:
 
-  typedef std::vector< ReducedRowVector* > RowsTable;
+  // VectorHeadTable : ArithVar |-> EntryID of the head of the vector
+  typedef std::vector<EntryID> VectorHeadTable;
+  VectorHeadTable d_rowHeads;
+  VectorHeadTable d_colHeads;
 
-  RowsTable d_rowsTable;
+  // VectorSizeTable : ArithVar |-> length of the vector
+  typedef std::vector<uint32_t> VectorSizeTable;
+  VectorSizeTable d_colLengths;
+  VectorSizeTable d_rowLengths;
 
+  // Set of all of the basic variables in the tableau.
   ArithVarSet d_basicVariables;
 
-  std::vector<uint32_t> d_rowCount;
-  ColumnMatrix d_columnMatrix;
+  typedef std::pair<EntryID, bool> PosUsedPair;
+  typedef std::vector<PosUsedPair> PosUsedPairArray;
+  PosUsedPairArray d_mergeBuffer;
+
+  typedef std::vector<ArithVar> ArithVarArray;
+  ArithVarArray d_usedList;
+
+
+  uint32_t d_entriesInUse;
+  TableauEntryManager d_entryManager;
 
 public:
   /**
    * Constructs an empty tableau.
    */
-  Tableau() :
-    d_rowsTable(),
-    d_basicVariables(),
-    d_rowCount(),
-    d_columnMatrix()
-  {}
-
-  /** Copy constructor. */
-  Tableau(const Tableau& tab);
+  Tableau() : d_entriesInUse(0) {}
   ~Tableau();
 
-  Tableau& operator=(const Tableau& tab);
+private:
+  void addEntry(ArithVar row, ArithVar col, const Rational& coeff);
+  void removeEntry(EntryID id);
+
+  template <bool isRowIterator>
+  class Iterator {
+  private:
+    EntryID d_curr;
+    TableauEntryManager& d_entryManager;
+
+  public:
+    Iterator(EntryID start, TableauEntryManager& manager) :
+      d_curr(start), d_entryManager(manager)
+    {}
+
+  public:
+
+    EntryID getID() const {
+      return d_curr;
+    }
+
+    const TableauEntry& operator*() const{
+      Assert(!atEnd());
+      return d_entryManager.get(d_curr);
+    }
+
+    Iterator& operator++(){
+      Assert(!atEnd());
+      TableauEntry& entry = d_entryManager.get(d_curr);
+      d_curr = isRowIterator ? entry.getNextRowID() : entry.getNextColID();
+      return *this;
+    }
+
+    bool atEnd() const {
+      return d_curr == ENTRYID_SENTINEL;
+    }
+  };
+
+public:
+  typedef Iterator<true> RowIterator;
+  typedef Iterator<false> ColIterator;
+
+  double densityMeasure() const;
 
   size_t getNumRows() const {
     return d_basicVariables.size();
@@ -76,56 +266,49 @@ public:
 
   void increaseSize(){
     d_basicVariables.increaseSize();
-    d_rowsTable.push_back(NULL);
-    d_rowCount.push_back(0);
 
-    d_columnMatrix.push_back(PermissiveBackArithVarSet());
+    d_rowHeads.push_back(ENTRYID_SENTINEL);
+    d_colHeads.push_back(ENTRYID_SENTINEL);
+
+    d_colLengths.push_back(0);
+    d_rowLengths.push_back(0);
 
-    //TODO replace with version of ArithVarSet that handles misses as non-entries
-    // not as buffer overflows
-    // ColumnMatrix::iterator i = d_columnMatrix.begin(), end = d_columnMatrix.end();
-    // for(; i != end; ++i){
-    //   Column& col = *i;
-    //   col.increaseSize(d_columnMatrix.size());
-    // }
+    d_mergeBuffer.push_back(std::make_pair(ENTRYID_SENTINEL, false));
   }
 
   bool isBasic(ArithVar v) const {
     return d_basicVariables.isMember(v);
   }
 
-  ArithVarSet::iterator begin(){
+  ArithVarSet::const_iterator beginBasic() const{
     return d_basicVariables.begin();
   }
 
-  ArithVarSet::iterator end(){
+  ArithVarSet::const_iterator endBasic() const{
     return d_basicVariables.end();
   }
 
-  const Column& getColumn(ArithVar v){
-    Assert(v < d_columnMatrix.size());
-    return d_columnMatrix[v];
+  RowIterator rowIterator(ArithVar v){
+    Assert(v < d_rowHeads.size());
+    EntryID head = d_rowHeads[v];
+    return RowIterator(head, d_entryManager);
   }
 
-  Column::iterator beginColumn(ArithVar v){
-    return getColumn(v).begin();
-  }
-  Column::iterator endColumn(ArithVar v){
-    return getColumn(v).end();
+  ColIterator colIterator(ArithVar v){
+    Assert(v < d_colHeads.size());
+    EntryID head = d_colHeads[v];
+    return ColIterator(head, d_entryManager);
   }
 
 
-  ReducedRowVector& lookup(ArithVar var){
-    Assert(d_basicVariables.isMember(var));
-    Assert(d_rowsTable[var] != NULL);
-    return *(d_rowsTable[var]);
+  uint32_t getRowLength(ArithVar x) const{
+    Assert(x < d_rowLengths.size());
+    return d_rowLengths[x];
   }
 
-  uint32_t getRowCount(ArithVar x){
-    Assert(x < d_rowCount.size());
-    AlwaysAssert(d_rowCount[x] == getColumn(x).size());
-
-    return d_rowCount[x];
+  uint32_t getColLength(ArithVar x) const{
+    Assert(x < d_colLengths.size());
+    return d_colLengths[x];
   }
 
   /**
@@ -149,49 +332,73 @@ public:
    *   x_s is non-basic, and
    *   a_rs != 0.
    */
-  void pivot(ArithVar x_r, ArithVar x_s);
+  void pivot(ArithVar basicOld, ArithVar basicNew);
+private:
+  void rowPivot(ArithVar basicOld, ArithVar basicNew);
+  /** Requires merge buffer to be loaded with basicFrom and used to be empty. */
+  void rowPlusRowTimesConstant(ArithVar basicTo, const Rational& coeff, ArithVar basicFrom);
 
-  void printTableau();
+  EntryID findOnRow(ArithVar basic, ArithVar find);
+  EntryID findOnCol(ArithVar basic, ArithVar find);
 
-  ReducedRowVector* removeRow(ArithVar basic);
+  TableauEntry d_failedFind;
+public:
 
+  /** If the find fails, isUnused is true on the entry. */
+  const TableauEntry& findEntry(ArithVar row, ArithVar col);
 
   /**
-   * Let s = numNonZeroEntries(), n = getNumRows(), and m = d_columnMatrix.size().
-   * When n >= 1,
-   *   densityMeasure() := s / (n*m - n**2 + n)
-   *                    := s / (n *(m - n + 1))
-   * When n = 0, densityMeasure() := 1
+   * Prints the contents of the Tableau to Debug("tableau::print")
    */
-  double densityMeasure() const{
-    Assert(numNonZeroEntriesByRow() == numNonZeroEntries());
-    uint32_t n = getNumRows();
-    if(n == 0){
-      return 1.0;
-    }else {
-      uint32_t s = numNonZeroEntries();
-      uint32_t m = d_columnMatrix.size();
-      uint32_t divisor = (n *(m - n + 1));
-
-      Assert(n >= 1);
-      Assert(m >= n);
-      Assert(divisor > 0);
-      Assert(divisor >= s);
-
-      return (double(s)) / divisor;
-    }
-  }
+  void printTableau();
+  void printRow(ArithVar basic);
+  void printEntry(const TableauEntry& entry);
+
 
 private:
+  void loadRowIntoMergeBuffer(ArithVar basic);
+  void emptyRowFromMergeBuffer(ArithVar basic);
+  void clearUsedList();
 
-  uint32_t numNonZeroEntries() const;
+  static bool bufferPairIsNotEmpty(const PosUsedPair& p){
+    return !(p.first == ENTRYID_SENTINEL && p.second == false);
+  }
+
+  static bool bufferPairIsEmpty(const PosUsedPair& p){
+    return (p.first == ENTRYID_SENTINEL && p.second == false);
+  }
+  bool mergeBufferIsEmpty() const {
+    return d_mergeBuffer.end() == std::find_if(d_mergeBuffer.begin(),
+                                               d_mergeBuffer.end(),
+                                               bufferPairIsNotEmpty);
+  }
+
+  void setColumnUnused(ArithVar v);
+
+public:
+  uint32_t size() const {
+    return d_entriesInUse;
+  }
+  uint32_t getNumEntriesInTableau() const {
+    return d_entryManager.size();
+  }
+  uint32_t getEntryCapacity() const {
+    return d_entryManager.capacity();
+  }
+
+  void removeRow(ArithVar basic);
+  Node rowAsEquality(ArithVar basic, const ArithVarToNodeMap& map);
+private:
+  uint32_t numNonZeroEntries() const { return size(); }
   uint32_t numNonZeroEntriesByRow() const;
+  uint32_t numNonZeroEntriesByCol() const;
+
 
-  /** Copies the datastructures in tab to this.*/
-  void internalCopy(const Tableau& tab);
+  bool debugNoZeroCoefficients(ArithVar basic);
+  bool debugMatchingCountsForRow(ArithVar basic);
+  uint32_t debugCountColLength(ArithVar var);
+  uint32_t debugCountRowLength(ArithVar var);
 
-  /** Clears the structures in the tableau. */
-  void clear();
 };
 
 }; /* namespace arith  */