From: Tim King <taking@cs.nyu.edu>
Date: Fri, 28 Oct 2011 18:35:27 +0000 (+0000)
Subject: Adding a check in Polynomial::parsePolynomial to better enforce the arithmetic normal... 
X-Git-Tag: cvc5-1.0.0~8407
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9547a48a7cdab8786c080779930de9c39655c52b;p=cvc5.git

Adding a check in Polynomial::parsePolynomial to better enforce the arithmetic normal form when assertions are enabled.
---

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 {