diff options
author | Tim King <taking@cs.nyu.edu> | 2011-10-28 18:35:27 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2011-10-28 18:35:27 +0000 |
commit | 9547a48a7cdab8786c080779930de9c39655c52b (patch) | |
tree | 7d95aeef2b6153f1f7ce36b9a9437263461ea2ce /src/theory/arith | |
parent | c9482b86edaabbd49f509c4477d0c181b2ebe33f (diff) |
Adding a check in Polynomial::parsePolynomial to better enforce the arithmetic normal form when assertions are enabled.
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/normal_form.h | 18 |
1 files changed, 16 insertions, 2 deletions
diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h index a182bc3b0..a1a33fed0 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -570,10 +570,24 @@ public: 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)){ + Node::iterator currIter = n.begin(), end = n.end(); + Node prev = *currIter; + if(!Monomial::isMember(prev)){ + return false; + } + + Monomial mprev = Monomial::parseMonomial(prev); + ++currIter; + for(; currIter != end; ++currIter){ + Node curr = *currIter; + if(!Monomial::isMember(curr)){ + return false; + } + Monomial mcurr = Monomial::parseMonomial(curr); + if(!(mprev < mcurr)){ return false; } + mprev = mcurr; } return true; } else { |