From 1e9fcef592fa5c841e1430446659c8d33fdcc3e2 Mon Sep 17 00:00:00 2001 From: Tim King Date: Wed, 13 Oct 2010 01:17:24 +0000 Subject: [PATCH] Removed vector monos from Polynomial. Now using expr::NodeSelfIterator. --- src/theory/arith/normal_form.cpp | 36 +++++-- src/theory/arith/normal_form.h | 166 +++++++++++++++++++------------ 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 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::sumLikeTerms(const vector & monos) { return outMonomials; } -void Monomial::printList(const std::vector& monos) { - typedef std::vector::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& list) { + for(vector::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 sortedMonos; - std::back_insert_iterator > bii(sortedMonos); - std::merge(begin(), end(), vl.begin(), vl.end(), bii); + merge_ranges(begin(), end(), vl.begin(), vl.end(), sortedMonos); std::vector 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(Kind, iterator, iterator) */ -template -static void copy_range(GetNodeIterator begin, GetNodeIterator end, std::vector& result){ +template +static void copy_range(GetNodeIterator begin, GetNodeIterator end, std::vector& result){ while(begin != end){ result.push_back(*begin); ++begin; } } -template +template static void merge_ranges(GetNodeIterator first1, GetNodeIterator last1, GetNodeIterator first2, GetNodeIterator last2, - std::vector& result) { + std::vector& result) { while(first1 != last1 && first2 != last2){ if( (*first1) < (*first2) ){ @@ -315,15 +315,6 @@ private: 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: @@ -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 sumLikeTerms(const std::vector& monos); - static void printList(const std::vector& monos); + void print() const; + static void printList(const std::vector& list); + };/* class Monomial */ class Polynomial : public NodeWrapper { private: - // MGD FOR REVIEW: do not create this vector<>! - std::vector monos; + bool d_singleton; - Polynomial(Node n, const std::vector& 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& 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::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& 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 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 subrange(start, end()); + iterator tailStart = begin(); + ++tailStart; + std::vector 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; -- 2.30.2