From a47b818c883eafb74afe066915bbbedf760c31e1 Mon Sep 17 00:00:00 2001 From: Tim King Date: Tue, 12 Oct 2010 22:04:58 +0000 Subject: IDENTITY has been removed. --- src/expr/node_manager.cpp | 3 - src/theory/arith/kinds | 2 - src/theory/arith/normal_form.cpp | 16 ++---- src/theory/arith/normal_form.h | 118 +++++++++++++++++++++++++++++--------- src/theory/arith/theory_arith.cpp | 3 - 5 files changed, 96 insertions(+), 46 deletions(-) (limited to 'src') diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 8ff83bb94..edb3a1592 100644 --- 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 5cd4719b1..6808e3d8f 100644 --- 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 60f6fa022..1449226db 100644 --- 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 result; - back_insert_iterator< vector > 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 2e20c62c5..291929f8f 100644 --- 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(Kind, iterator, iterator) */ +template +static void copy_range(GetNodeIterator begin, GetNodeIterator end, std::vector& result){ + while(begin != end){ + result.push_back(*begin); + ++begin; + } +} + +template +static void merge_ranges(GetNodeIterator first1, + GetNodeIterator last1, + GetNodeIterator first2, + GetNodeIterator last2, + std::vector& 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& 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& 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& l) : backingNode(multList(l)) { + + VarList(const std::vector& 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 ac3dc3d40..4a783a6a4 100644 --- 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() / engine->getValue(n[1]).getConst() ); - case kind::IDENTITY: // 1 arg - return engine->getValue(n[0]); - case kind::LT: // 2 args return nodeManager->mkConst( engine->getValue(n[0]).getConst() < engine->getValue(n[1]).getConst() ); -- cgit v1.2.3