From 9eaf94708275337a4749b7ef2f44bf1c6746d8fc Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Thu, 16 Sep 2010 21:16:59 +0000
Subject: [PATCH] Bug fix to CVC4::theory::arith::VarList as well as some
 superficial changes. test/regress/regress0/arith/arith.03.cvc now passes and
 is turned on by default.  Tiny documentation fix for the arithmetic normal
 form.

---
 src/theory/arith/normal_form.cpp        | 36 +++++++++++++------------
 src/theory/arith/normal_form.h          |  5 ++--
 test/regress/regress0/arith/Makefile.am |  3 ++-
 3 files changed, 23 insertions(+), 21 deletions(-)

diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp
index 18e31848b..6e476bb7f 100644
--- a/src/theory/arith/normal_form.cpp
+++ b/src/theory/arith/normal_form.cpp
@@ -58,23 +58,20 @@ VarList VarList::operator*(const VarList& vl) const{
   }else if(vl.empty()){
     return *this;
   }else{
-    vector<Variable> result;
-    vector<Variable> thisAsVec = this->asList();
-    vector<Variable> vlAsVec = vl.asList();
-    back_insert_iterator<vector<Variable> > bii(result);
-
-    merge(thisAsVec.begin(), thisAsVec.end(), vlAsVec.begin(), vlAsVec.end(), bii);
-
-    return VarList::mkVarList(result);
-  }
-}
-
-std::vector<Variable> VarList::asList() const {
-  vector<Variable> res;
-  for(iterator i = begin(), e = end(); i != e; ++i){
-    res.push_back(*i);
+    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);
+    Assert(result.size() >= 2);
+    Node mult = NodeManager::currentNM()->mkNode(kind::MULT, result);
+    return VarList::parseVarList(mult);
   }
-  return res;
 }
 
 Monomial Monomial::mkMonomial(const Constant& c, const VarList& vl){
@@ -162,12 +159,17 @@ Polynomial Polynomial::operator*(const Monomial& mono) const{
     for(iterator i = this->begin(), end = this->end(); i != end; ++i){
       newMonos.push_back(mono * (*i));
     }
+
+    // We may need to sort newMonos.
+    // Suppose this = (+ x y), mono = x, (* x y).getId() < (* x x).getId()
+    // newMonos = <(* x x), (* x y)> after this loop.
+    // This is not sorted according to the current VarList order.
+    std::sort(newMonos.begin(), newMonos.end());
     return Polynomial::mkPolynomial(newMonos);
   }
 }
 
 Polynomial Polynomial::operator*(const Polynomial& poly) const{
-
   Polynomial res = Polynomial::mkZero();
   for(iterator i = this->begin(), end = this->end(); i != end; ++i){
     Monomial curr = *i;
diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index 1f7bc6be3..0762868cf 100644
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -43,10 +43,11 @@ namespace arith {
  *   where
  *     constant' \not\in {0,1}
 
- * polynomial := monomial | (+ [monomial])
+ * polynomial := monomial' | (+ [monomial])
  *   where
  *     len [monomial] >= 2
  *     isStrictlySorted monoOrder [monomial]
+ *     forall (\x -> x != 0) [monomial]
 
  * restricted_cmp := (|><| polynomial constant)
  *   where
@@ -335,8 +336,6 @@ public:
 
   bool operator==(const VarList& vl) const{ return cmp(vl) == 0; }
 
-  std::vector<Variable> asList() const;
-
 private:
   bool isSorted(iterator start, iterator end);
 };
diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am
index e4fc110b4..18ca5fe86 100644
--- a/test/regress/regress0/arith/Makefile.am
+++ b/test/regress/regress0/arith/Makefile.am
@@ -5,7 +5,8 @@ TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4
 # put it below in "TESTS +="
 TESTS =	\
 	arith.01.cvc \
-	arith.02.cvc 
+	arith.02.cvc \
+	arith.03.cvc
 
 EXTRA_DIST = $(TESTS)
 
-- 
2.30.2