Merging the arithmetic theory draft (lra-init) back into the main trunk. This should not affect other parts of the system. This code is untested, and is volatile. It is going to be improved in the future so don't pick on it too much. I am merging this code in its current state back into the main trunk because it was getting unruly to keep merging the updated trunk back into the branch.

1 files changed, 243 insertions, 0 deletions

diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
new file mode 100644
index 000000000..10daa0c13
--- /dev/null
+++ b/src/theory/arith/tableau.h
@@ -0,0 +1,243 @@
+
+#include "expr/node.h"
+#include "expr/attribute.h"
+
+#include "theory/arith/basic.h"
+
+#include <ext/hash_map>
+#include <set>
+
+#ifndef __CVC4__THEORY__ARITH__TABLEAU_H
+#define __CVC4__THEORY__ARITH__TABLEAU_H
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+
+class Row {
+  TNode d_x_i;
+
+  typedef __gnu_cxx::hash_map<TNode, Rational, NodeHashFunction> CoefficientTable;
+
+  std::set<TNode> d_nonbasic;
+  CoefficientTable d_coeffs;
+
+public:
+
+  /**
+   * Construct a row equal to:
+   *   basic = \sum_{x_i} c_i * x_i
+   */
+  Row(TNode basic, TNode sum): d_x_i(basic),d_nonbasic(), d_coeffs(){
+    using namespace CVC4::kind;
+
+    Assert(d_x_i.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+
+    //TODO Assert(d_x_i.getType() == REAL);
+    Assert(sum.getKind() == PLUS);
+
+    for(TNode::iterator iter=sum.begin(); iter != sum.end(); ++iter){
+      TNode pair = *iter;
+      Assert(pair.getKind() == MULT);
+      Assert(pair.getNumChildren() == 2);
+      TNode coeff = pair[0];
+      TNode var_i = pair[1];
+      Assert(coeff.getKind() == CONST_RATIONAL);
+      Assert(var_i.getKind() == VARIABLE);
+      //TODO Assert(var_i.getKind() == REAL);
+      Assert(!has(var_i));
+      d_nonbasic.insert(var_i);
+      d_coeffs[var_i] = coeff.getConst<Rational>();
+    }
+  }
+
+  std::set<TNode>::iterator begin(){
+    return d_nonbasic.begin();
+  }
+
+  std::set<TNode>::iterator end(){
+    return d_nonbasic.end();
+  }
+
+  TNode basicVar(){
+    return d_x_i;
+  }
+
+  bool has(TNode x_j){
+    CoefficientTable::iterator x_jPos = d_coeffs.find(x_j);
+
+    return x_jPos != d_coeffs.end();
+  }
+
+  Rational& lookup(TNode x_j){
+    return d_coeffs[x_j];
+  }
+
+  void pivot(TNode x_j){
+    Rational negInverseA_rs = -(lookup(x_j).inverse());
+    d_coeffs[d_x_i] = Rational(Integer(-1));
+    d_coeffs.erase(x_j);
+
+    d_nonbasic.erase(x_j);
+    d_nonbasic.insert(d_x_i);
+    d_x_i = x_j;
+
+    for(std::set<TNode>::iterator nonbasicIter = d_nonbasic.begin();
+        nonbasicIter != d_nonbasic.end();
+        ++nonbasicIter){
+      TNode nb = *nonbasicIter;
+      d_coeffs[nb] = d_coeffs[nb] * negInverseA_rs;
+    }
+  }
+
+  void subsitute(Row& row_s){
+    TNode x_s = row_s.basicVar();
+
+    Assert(!has(x_s));
+    Assert(x_s != d_x_i);
+
+
+    Rational a_rs = lookup(x_s);
+    d_coeffs.erase(x_s);
+
+    for(std::set<TNode>::iterator iter = row_s.d_nonbasic.begin();
+        iter != row_s.d_nonbasic.end();
+        ++iter){
+      TNode x_j = *iter;
+      Rational a_sj = a_rs * row_s.lookup(x_j);
+      if(has(x_j)){
+        d_coeffs[x_j] = d_coeffs[x_j] + a_sj;
+      }else{
+        d_nonbasic.insert(x_j);
+        d_coeffs[x_j] = a_sj;
+      }
+    }
+  }
+};
+
+class Tableau {
+public:
+  typedef std::set<TNode> VarSet;
+
+private:
+  typedef __gnu_cxx::hash_map<TNode, Row*, NodeHashFunction> RowsTable;
+
+  VarSet d_basicVars;
+  RowsTable d_rows;
+
+  inline bool contains(TNode var){
+    return d_basicVars.find(var) != d_basicVars.end();
+  }
+
+public:
+  /**
+   * Constructs an empty tableau.
+   */
+  Tableau() : d_basicVars(), d_rows() {}
+
+  VarSet::iterator begin(){
+    return d_basicVars.begin();
+  }
+
+  VarSet::iterator end(){
+    return d_basicVars.end();
+  }
+
+  Row* lookup(TNode var){
+    Assert(contains(var));
+    return d_rows[var];
+  }
+
+  /**
+   * Iterator for the tableau. Iterates over rows.
+   */
+  /* TODO add back in =(
+  class iterator {
+  private:
+    const Tableau*  table_ref;
+    VarSet::iterator variableIter;
+
+    iterator(const Tableau* tr, VarSet::iterator& i) :
+      table_ref(tr), variableIter(i){}
+
+  public:
+    void operator++(){
+      ++variableIter;
+    }
+
+    bool operator==(iterator& other){
+      return variableIter == other.variableIter;
+    }
+    bool operator!=(iterator& other){
+      return variableIter != other.variableIter;
+    }
+
+    Row& operator*() const{
+      TNode var = *variableIter;
+      RowsTable::iterator iter = table_ref->d_rows.find(var);
+      return *iter;
+    }
+  };
+  iterator begin(){
+    return iterator(this, d_basicVars.begin());
+  }
+  iterator end(){
+    return iterator(this, d_basicVars.end());
+  }*/
+
+  void addRow(TNode eq){
+    Assert(eq.getKind() == kind::EQUAL);
+    Assert(eq.getNumChildren() == 2);
+
+    TNode var = eq[0];
+    TNode sum = eq[1];
+
+    //Assert(isAdmissableVariable(var));
+    Assert(var.getAttribute(IsBasic()));
+
+    Assert(d_basicVars.find(var) != d_basicVars.end());
+    d_basicVars.insert(var);
+    d_rows[var] = new Row(var,sum);
+  }
+
+  /**
+   * preconditions:
+   *   x_r is basic,
+   *   x_s is non-basic, and
+   *   a_rs != 0.
+   */
+  void pivot(TNode x_r, TNode x_s){
+    RowsTable::iterator ptrRow_r = d_rows.find(x_r);
+    Assert(ptrRow_r != d_rows.end());
+
+    Row* row_s = (*ptrRow_r).second;
+
+    Assert(row_s->has(x_s));
+    row_s->pivot(x_s);
+
+    d_rows.erase(ptrRow_r);
+    d_basicVars.erase(x_r);
+    makeNonbasic(x_r);
+
+    d_rows.insert(std::make_pair(x_s,row_s));
+    d_basicVars.insert(x_s);
+    makeBasic(x_s);
+
+    for(VarSet::iterator basicIter = begin(); basicIter != end(); ++basicIter){
+      TNode basic = *basicIter;
+      Row* row_k = lookup(basic);
+      if(row_k->basicVar() != x_s){
+        if(row_k->has(x_s)){
+          row_k->subsitute(*row_s);
+        }
+      }
+    }
+  }
+};
+
+}; /* namespace arith  */
+}; /* namespace theory */
+}; /* namespace CVC4   */
+
+#endif /* __CVC4__THEORY__ARITH__TABLEAU_H */