Removed vector<Monomial> monos from Polynomial. Now using expr::NodeSelfIterator.

2 files changed, 130 insertions, 72 deletions

diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp
index 1449226db..7c3e5ba93 100644
--- a/src/theory/arith/normal_form.cpp
+++ b/src/theory/arith/normal_form.cpp
@@ -77,13 +77,31 @@ VarList VarList::operator*(const VarList& other) const {
     return *this;
   } else {
     vector<Node> result;
-    merge(other, result);
+
+    internal_iterator
+      thisBegin = this->internalBegin(),
+      thisEnd = this->internalEnd(),
+      otherBegin = other.internalBegin(),
+      otherEnd = other.internalEnd();
+
+    merge_ranges(thisBegin, thisEnd, otherBegin, otherEnd, result);
+
     Assert(result.size() >= 2);
     Node mult = NodeManager::currentNM()->mkNode(kind::MULT, result);
     return VarList::parseVarList(mult);
   }
 }
 
+bool Monomial::isMember(TNode n){
+  if(n.getKind() == kind::CONST_RATIONAL) {
+    return true;
+  } else if(multStructured(n)) {
+    return VarList::isMember(n[1]);
+  } else {
+    return VarList::isMember(n);
+  }
+}
+
 Monomial Monomial::mkMonomial(const Constant& c, const VarList& vl) {
   if(c.isZero() || vl.empty() ) {
     return Monomial(c);
@@ -139,20 +157,22 @@ vector<Monomial> Monomial::sumLikeTerms(const vector<Monomial> & monos) {
   return outMonomials;
 }
 
-void Monomial::printList(const std::vector<Monomial>& monos) {
-  typedef std::vector<Monomial>::const_iterator iterator;
-  for(iterator i = monos.begin(), end = monos.end(); i != end; ++i) {
-    Debug("blah") <<  ((*i).getNode()) << std::endl;
-  }
+void Monomial::print() const {
+  Debug("normal-form") <<  getNode() << std::endl;
 }
 
+void Monomial::printList(const vector<Monomial>& list) {
+  for(vector<Monomial>::const_iterator i = list.begin(), end = list.end(); i != end; ++i) {
+    const Monomial& m =*i;
+    m.print();
+  }
+}
 Polynomial Polynomial::operator+(const Polynomial& vl) const {
   this->printList();
   vl.printList();
 
   std::vector<Monomial> sortedMonos;
-  std::back_insert_iterator<std::vector<Monomial> > bii(sortedMonos);
-  std::merge(begin(), end(), vl.begin(), vl.end(), bii);
+  merge_ranges(begin(), end(), vl.begin(), vl.end(), sortedMonos);
 
   std::vector<Monomial> combined = Monomial::sumLikeTerms(sortedMonos);
 
diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index 291929f8f..0a962283c 100644
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -248,20 +248,20 @@ inline Node makeNode(Kind k, GetNodeIterator start, GetNodeIterator end) {
 }/* makeNode<GetNodeIterator>(Kind, iterator, iterator) */
 
 
-template <class GetNodeIterator>
-static void copy_range(GetNodeIterator begin, GetNodeIterator end, std::vector<Node>& result){
+template <class GetNodeIterator, class T>
+static void copy_range(GetNodeIterator begin, GetNodeIterator end, std::vector<T>& result){
   while(begin != end){
     result.push_back(*begin);
     ++begin;
   }
 }
 
-template <class GetNodeIterator>
+template <class GetNodeIterator, class T>
 static void merge_ranges(GetNodeIterator first1,
                   GetNodeIterator last1,
                   GetNodeIterator first2,
                   GetNodeIterator last2,
-                  std::vector<Node>& result) {
+                  std::vector<T>& result) {
 
   while(first1 != last1 && first2 != last2){
     if( (*first1) < (*first2) ){
@@ -315,15 +315,6 @@ private:
       return getNode().end();
     }
   }
-  void merge(const VarList& other, std::vector<Node>& result) const{
-    internal_iterator
-      thisBegin = this->internalBegin(),
-      thisEnd = this->internalEnd(),
-      otherBegin = other.internalBegin(),
-      otherEnd = other.internalEnd();
-
-    merge_ranges(thisBegin, thisEnd, otherBegin, otherEnd, result);
-  }
 
 public:
 
@@ -357,24 +348,11 @@ public:
   };
 
   iterator begin() const {
-    expr::NodeSelfIterator iter;
-    if(singleton()){
-      iter = expr::NodeSelfIterator::self(getNode());
-    }else{
-      iter = getNode().begin();
-    }
-    return iterator(iter);
+    return iterator(internalBegin());
   }
 
   iterator end() const {
-    expr::NodeSelfIterator iter;
-    if(singleton()){
-      iter = expr::NodeSelfIterator::self(getNode());
-    }else{
-      iter = getNode().end();
-    }
-
-    return iterator(iter);
+    return iterator(internalEnd());
   }
 
   VarList(Variable v) : NodeWrapper(v.getNode()) {
@@ -484,6 +462,8 @@ public:
     Assert(multStructured(getNode()));
   }
 
+  static bool isMember(TNode n);
+
   /** Makes a monomial with no restrictions on c and vl. */
   static Monomial mkMonomial(const Constant& c, const VarList& vl);
 
@@ -540,20 +520,18 @@ public:
    */
   static std::vector<Monomial> sumLikeTerms(const std::vector<Monomial>& monos);
 
-  static void printList(const std::vector<Monomial>& monos);
+  void print() const;
+  static void printList(const std::vector<Monomial>& list);
+
 };/* class Monomial */
 
 
 class Polynomial : public NodeWrapper {
 private:
-  // MGD FOR REVIEW: do not create this vector<>!
-  std::vector<Monomial> monos;
+  bool d_singleton;
 
-  Polynomial(Node n, const std::vector<Monomial>& m):
-    NodeWrapper(n), monos(m)
-  {
-    Assert( !monos.empty() );
-    Assert( Monomial::isStrictlySorted(monos) );
+  Polynomial(TNode n) : NodeWrapper(n), d_singleton(Monomial::isMember(n)) {
+    Assert(isMember(getNode()));
   }
 
   static Node makePlusNode(const std::vector<Monomial>& m) {
@@ -562,22 +540,84 @@ private:
     return makeNode(kind::PLUS, m.begin(), m.end());
   }
 
+  typedef expr::NodeSelfIterator internal_iterator;
+
+  internal_iterator internalBegin() const {
+    if(singleton()){
+      return expr::NodeSelfIterator::self(getNode());
+    }else{
+      return getNode().begin();
+    }
+  }
+
+  internal_iterator internalEnd() const {
+    if(singleton()){
+      return expr::NodeSelfIterator::selfEnd(getNode());
+    }else{
+      return getNode().end();
+    }
+  }
+
+  bool singleton() const { return d_singleton; }
+
 public:
-  typedef std::vector<Monomial>::const_iterator iterator;
+  static bool isMember(TNode n) {
+    if(Monomial::isMember(n)){
+      return true;
+    }else if(n.getKind() == kind::PLUS){
+      Assert(n.getNumChildren() >= 2);
+      for(Node::iterator curr = n.begin(), end = n.end(); curr != end;++curr){
+        if(!Monomial::isMember(*curr)){
+          return false;
+        }
+      }
+      return true;
+    } else {
+      return false;
+    }
+  }
+
+  class iterator {
+  private:
+    internal_iterator d_iter;
+
+  public:
+    explicit iterator(internal_iterator i) : d_iter(i) {}
+
+    inline Monomial operator*() {
+      return Monomial::parseMonomial(*d_iter);
+    }
+
+    bool operator==(const iterator& i) {
+      return d_iter == i.d_iter;
+    }
+
+    bool operator!=(const iterator& i) {
+      return d_iter != i.d_iter;
+    }
+
+    iterator operator++() {
+      ++d_iter;
+      return *this;
+    }
 
-  iterator begin() const { return monos.begin(); }
-  iterator end() const { return monos.end(); }
+    iterator operator++(int) {
+      return iterator(d_iter++);
+    }
+  };
+
+  iterator begin() const { return iterator(internalBegin()); }
+  iterator end() const {  return iterator(internalEnd()); }
 
   Polynomial(const Monomial& m):
-    NodeWrapper(m.getNode()), monos()
-  {
-    monos.push_back(m);
-  }
+    NodeWrapper(m.getNode()), d_singleton(true)
+  {}
+
   Polynomial(const std::vector<Monomial>& m):
-    NodeWrapper(makePlusNode(m)), monos(m)
+    NodeWrapper(makePlusNode(m)), d_singleton(false)
   {
-    Assert( monos.size() >= 2);
-    Assert( Monomial::isStrictlySorted(monos) );
+    Assert( m.size() >= 2);
+    Assert( Monomial::isStrictlySorted(m) );
   }
 
 
@@ -591,17 +631,8 @@ public:
     }
   }
 
-  // MGD FOR REVIEW: make this constant time (for non-debug mode)
   static Polynomial parsePolynomial(Node n) {
-    std::vector<Monomial> monos;
-    if(n.getKind() == kind::PLUS) {
-      for(Node::iterator i=n.begin(), end=n.end(); i != end; ++i) {
-        monos.push_back(Monomial::parseMonomial(*i));
-      }
-    } else {
-      monos.push_back(Monomial::parseMonomial(n));
-    }
-    return Polynomial(n,monos);
+    return Polynomial(n);
   }
 
   static Polynomial mkZero() {
@@ -611,11 +642,11 @@ public:
     return Polynomial(Monomial::mkOne());
   }
   bool isZero() const {
-    return (monos.size() == 1) && (getHead().isZero());
+    return singleton() && (getHead().isZero());
   }
 
   bool isConstant() const {
-    return (monos.size() == 1) && (getHead().isConstant());
+    return singleton() && (getHead().isConstant());
   }
 
   bool containsConstant() const {
@@ -627,17 +658,24 @@ public:
   }
 
   Polynomial getTail() const {
-    Assert(monos.size() >= 1);
+    Assert(! singleton());
 
-    iterator start = begin()+1;
-    std::vector<Monomial> subrange(start, end());
+    iterator tailStart = begin();
+    ++tailStart;
+    std::vector<Monomial> subrange;
+    copy_range(tailStart, end(), subrange);
     return mkPolynomial(subrange);
   }
 
   void printList() const {
-    Debug("normal-form") << "start list" << std::endl;
-    Monomial::printList(monos);
-    Debug("normal-form") << "end list" << std::endl;
+    if(Debug.isOn("normal-form")){
+      Debug("normal-form") << "start list" << std::endl;
+      for(iterator i = begin(), oend = end(); i != oend; ++i) {
+        const Monomial& m =*i;
+        m.print();
+      }
+      Debug("normal-form") << "end list" << std::endl;
+    }
   }
 
   Polynomial operator+(const Polynomial& vl) const;