IDENTITY has been removed.

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 8ff83bb945edd58d78943986612eba6e55d9413a..edb3a1592adaab8c7ea883b6bab242ec7df5eac4 100644 (file)
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -263,9 +263,6 @@ TypeNode NodeManager::getType(TNode n, bool check)
     case kind::APPLY_UF:
       typeNode = CVC4::theory::uf::UfTypeRule::computeType(this, n, check);
       break;
-    case kind::IDENTITY:
-      typeNode = CVC4::theory::arith::ArithOperatorTypeRule::computeType(this, n, check);
-      break;
     case kind::PLUS:
       typeNode = CVC4::theory::arith::ArithOperatorTypeRule::computeType(this, n, check);
       break;

diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index 5cd4719b12f6f41091f787c29c3f38996b207b58..6808e3d8f7c9666db5f823636a1f24aabb92dea2 100644 (file)
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -12,8 +12,6 @@ operator MINUS 2 "arithmetic binary subtraction operator"
 operator UMINUS 1 "arithmetic unary negation"
 operator DIVISION 2 "arithmetic division"
 
-operator IDENTITY 1 "identity function"
-
 constant CONST_RATIONAL \
     ::CVC4::Rational \
     ::CVC4::RationalHashStrategy \

diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp
index 60f6fa022aafdd32cf5bfdcde9468fcf5b9cb8d0..1449226db3fd217c0b7f3c0afa63c84d75885989 100644 (file)
--- a/src/theory/arith/normal_form.cpp
+++ b/src/theory/arith/normal_form.cpp
@@ -70,22 +70,14 @@ VarList VarList::parseVarList(Node n) {
   }
 }
 
-VarList VarList::operator*(const VarList& vl) const {
+VarList VarList::operator*(const VarList& other) const {
   if(this->empty()) {
-    return vl;
-  } else if(vl.empty()) {
+    return other;
+  } else if(other.empty()) {
     return *this;
   } else {
     vector<Node> result;
-    back_insert_iterator< vector<Node> > bii(result);
-
-    Node::iterator
-      thisBegin = this->backingNode.begin(),
-      thisEnd = this->backingNode.end(),
-      v1Begin = vl.backingNode.begin(),
-      v1End = vl.backingNode.end();
-
-    merge(thisBegin, thisEnd, v1Begin, v1End, bii);
+    merge(other, result);
     Assert(result.size() >= 2);
     Node mult = NodeManager::currentNM()->mkNode(kind::MULT, result);
     return VarList::parseVarList(mult);

diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index 2e20c62c5b2345c7f32b6d0371977c4a65f5ed21..291929f8f7d53b396690f1068246cc4db5a14d70 100644 (file)
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -23,6 +23,7 @@
 #define __CVC4__THEORY__ARITH__NORMAL_FORM_H
 
 #include "expr/node.h"
+#include "expr/node_self_iterator.h"
 #include "util/rational.h"
 #include "theory/arith/arith_constants.h"
 #include "theory/arith/arith_utilities.h"
@@ -247,6 +248,34 @@ 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){
+  while(begin != end){
+    result.push_back(*begin);
+    ++begin;
+  }
+}
+
+template <class GetNodeIterator>
+static void merge_ranges(GetNodeIterator first1,
+                  GetNodeIterator last1,
+                  GetNodeIterator first2,
+                  GetNodeIterator last2,
+                  std::vector<Node>& result) {
+
+  while(first1 != last1 && first2 != last2){
+    if( (*first1) < (*first2) ){
+      result.push_back(*first1);
+      ++ first1;
+    }else{
+      result.push_back(*first2);
+      ++ first2;
+    }
+  }
+  copy_range(first1, last1, result);
+  copy_range(first2, last2, result);
+}
+
 /**
  * A VarList is a sorted list of variables representing a product.
  * If the VarList is empty, it represents an empty product or 1.
@@ -254,34 +283,56 @@ inline Node makeNode(Kind k, GetNodeIterator start, GetNodeIterator end) {
  *
  * A non-sorted VarList can never be successfully made in debug mode.
  */
-class VarList {
+class VarList : public NodeWrapper {
 private:
-  Node backingNode;
 
   static Node multList(const std::vector<Variable>& list) {
     Assert(list.size() >= 2);
 
     return makeNode(kind::MULT, list.begin(), list.end());
   }
-  static Node makeTuple(Node n) {
-    // MGD FOR REVIEW: drop IDENTITY kind ?
-    return NodeManager::currentNM()->mkNode(kind::IDENTITY, n);
+
+  VarList() : NodeWrapper(Node::null()) {}
+
+  VarList(Node n) : NodeWrapper(n) {
+    Assert(isSorted(begin(), end()));
   }
 
-  VarList() : backingNode(Node::null()) {}
+  typedef expr::NodeSelfIterator internal_iterator;
 
-  VarList(Node n) {
-    backingNode = (Variable::isMember(n)) ? makeTuple(n) : n;
+  internal_iterator internalBegin() const {
+    if(singleton()){
+      return expr::NodeSelfIterator::self(getNode());
+    }else{
+      return getNode().begin();
+    }
+  }
 
-    Assert(isSorted(begin(), end()));
+  internal_iterator internalEnd() const {
+    if(singleton()){
+      return expr::NodeSelfIterator::selfEnd(getNode());
+    }else{
+      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:
-  class iterator  {
+
+  class iterator {
   private:
-    Node::iterator d_iter;
+    internal_iterator d_iter;
+
   public:
-    explicit iterator(Node::iterator i) : d_iter(i) {}
+    explicit iterator(internal_iterator i) : d_iter(i) {}
 
     inline Variable operator*() {
       return Variable(*d_iter);
@@ -305,25 +356,32 @@ public:
     }
   };
 
-  Node getNode() const {
-    if(singleton()) {
-      return backingNode[0];
-    } else {
-      return backingNode;
+  iterator begin() const {
+    expr::NodeSelfIterator iter;
+    if(singleton()){
+      iter = expr::NodeSelfIterator::self(getNode());
+    }else{
+      iter = getNode().begin();
     }
+    return iterator(iter);
   }
 
-  iterator begin() const {
-    return iterator(backingNode.begin());
-  }
   iterator end() const {
-    return iterator(backingNode.end());
+    expr::NodeSelfIterator iter;
+    if(singleton()){
+      iter = expr::NodeSelfIterator::self(getNode());
+    }else{
+      iter = getNode().end();
+    }
+
+    return iterator(iter);
   }
 
-  VarList(Variable v) : backingNode(makeTuple(v.getNode())) {
+  VarList(Variable v) : NodeWrapper(v.getNode()) {
     Assert(isSorted(begin(), end()));
   }
-  VarList(const std::vector<Variable>& l) : backingNode(multList(l)) {
+
+  VarList(const std::vector<Variable>& l) : NodeWrapper(multList(l)) {
     Assert(l.size() >= 2);
     Assert(isSorted(begin(), end()));
   }
@@ -350,9 +408,17 @@ public:
     }
   }
 
-  int size() const { return backingNode.getNumChildren(); }
-  bool empty() const { return size() == 0; }
-  bool singleton() const { return backingNode.getKind() == kind::IDENTITY; }
+  bool empty() const { return getNode().isNull(); }
+  bool singleton() const {
+    return !empty() && getNode().getKind() != kind::MULT;
+  }
+
+  int size() const {
+    if(singleton())
+      return 1;
+    else
+      return getNode().getNumChildren();
+  }
 
   static VarList parseVarList(Node n);
 

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index ac3dc3d401b21c11de4de526b422ab9364344b44..4a783a6a40144b8570526c0176a31ca33b45b891 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -980,9 +980,6 @@ Node TheoryArith::getValue(TNode n, TheoryEngine* engine) {
     return nodeManager->mkConst( engine->getValue(n[0]).getConst<Rational>() /
                                  engine->getValue(n[1]).getConst<Rational>() );
 
-  case kind::IDENTITY: // 1 arg
-    return engine->getValue(n[0]);
-
   case kind::LT: // 2 args
     return nodeManager->mkConst( engine->getValue(n[0]).getConst<Rational>() <
                                  engine->getValue(n[1]).getConst<Rational>() );