src/theory/arith/normal_form.h

   1 /*********************                                                        */
   2 /*! \file normal_form.h
   3  ** \verbatim
   4  ** Original author: taking
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): dejan, mdeters
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009-2012  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief [[ Add one-line brief description here ]]
  13  **
  14  ** [[ Add lengthier description here ]]
  15  ** \todo document this file
  16  **/
  17
  18 #include "cvc4_private.h"
  19
  20 #ifndef __CVC4__THEORY__ARITH__NORMAL_FORM_H
  21 #define __CVC4__THEORY__ARITH__NORMAL_FORM_H
  22
  23 #include "expr/node.h"
  24 #include "expr/node_self_iterator.h"
  25 #include "util/rational.h"
  26 #include "theory/theory.h"
  27 #include "theory/arith/arith_utilities.h"
  28
  29 #include <list>
  30 #include <algorithm>
  31 #include <ext/algorithm>
  32
  33 namespace CVC4 {
  34 namespace theory {
  35 namespace arith {
  36
  37 /***********************************************/
  38 /***************** Normal Form *****************/
  39 /***********************************************/
  40 /***********************************************/
  41
  42 /**
  43  * Section 1: Languages
  44  * The normal form for arithmetic nodes is defined by the language
  45  * accepted by the following BNFs with some guard conditions.
  46  * (The guard conditions are in Section 3 for completeness.)
  47  *
  48  * variable := n
  49  *   where
  50  *     n.isVar() or is foreign
  51  *     n.getType() \in {Integer, Real}
  52  *
  53  * constant := n
  54  *   where
  55  *     n.getKind() == kind::CONST_RATIONAL
  56  *
  57  * var_list := variable | (* [variable])
  58  *   where
  59  *     len [variable] >= 2
  60  *     isSorted varOrder [variable]
  61  *
  62  * monomial := constant | var_list | (* constant' var_list')
  63  *   where
  64  *     \f$ constant' \not\in {0,1} \f$
  65  *
  66  * polynomial := monomial' | (+ [monomial])
  67  *   where
  68  *     len [monomial] >= 2
  69  *     isStrictlySorted monoOrder [monomial]
  70  *     forall (\x -> x != 0) [monomial]
  71  *
  72  * rational_cmp := (|><| qpolynomial constant)
  73  *   where
  74  *     |><| is GEQ, or GT
  75  *     not (exists constantMonomial (monomialList qpolynomial))
  76  *     (exists realMonomial (monomialList qpolynomial))
  77  *     abs(monomialCoefficient (head (monomialList qpolynomial))) == 1
  78  *
  79  * integer_cmp := (<= zpolynomial constant)
  80  *   where
  81  *     not (exists constantMonomial (monomialList zpolynomial))
  82  *     (forall integerMonomial (monomialList zpolynomial))
  83  *     the gcd of all numerators of coefficients is 1
  84  *     the denominator of all coefficients and the constant is 1
  85  *
  86  * rational_eq := (= qvarlist qpolynomial)
  87  *   where
  88  *     let allMonomials = (cons qvarlist (monomialList zpolynomial))
  89  *     let variableMonomials = (drop constantMonomial allMonomials)
  90  *     isStrictlySorted variableMonomials
  91  *     exists realMonomial variableMonomials
  92  *     is not empty qvarlist
  93  *
  94  * integer_eq := (= zmonomial zpolynomial)
  95  *   where
  96  *     let allMonomials = (cons zmonomial (monomialList zpolynomial))
  97  *     let variableMonomials = (drop constantMonomial allMonomials)
  98  *     not (constantMonomial zmonomial)
  99  *     (forall integerMonomial allMonomials)
 100  *     isStrictlySorted variableMonomials
 101  *     the gcd of all numerators of coefficients is 1
 102  *     the denominator of all coefficients and the constant is 1
 103  *     the coefficient of monomial is positive
 104  *     the value of the coefficient of monomial is minimal in variableMonomials
 105  *
 106  * comparison := TRUE | FALSE
 107  *   | rational_cmp | (not rational_cmp)
 108  *   | rational_eq | (not rational_eq)
 109  *   | integer_cmp | (not integer_cmp)
 110  *   | integer_eq | (not integer_eq)
 111  *
 112  * Normal Form for terms := polynomial
 113  * Normal Form for atoms := comparison
 114  */
 115
 116 /**
 117  * Section 2: Helper Classes
 118  * The langauges accepted by each of these defintions
 119  * roughly corresponds to one of the following helper classes:
 120  *  Variable
 121  *  Constant
 122  *  VarList
 123  *  Monomial
 124  *  Polynomial
 125  *  Comparison
 126  *
 127  * Each of the classes obeys the following contracts/design decisions:
 128  * -Calling isMember(Node node) on a node returns true iff that node is a
 129  *  a member of the language. Note: isMember is O(n).
 130  * -Calling isNormalForm() on a helper class object returns true iff that
 131  *  helper class currently represents a normal form object.
 132  * -If isNormalForm() is false, then this object must have been made
 133  *  using a mk*() factory function.
 134  * -If isNormalForm() is true, calling getNode() on all of these classes
 135  *  returns a node that would be accepted by the corresponding language.
 136  *  And if isNormalForm() is false, returns Node::null().
 137  * -Each of the classes is immutable.
 138  * -Public facing constuctors have a 1-to-1 correspondence with one of
 139  *  production rules in the above grammar.
 140  * -Public facing constuctors are required to fail in debug mode when the
 141  *  guards of the production rule are not strictly met.
 142  *  For example: Monomial(Constant(1),VarList(Variable(x))) must fail.
 143  * -When a class has a Class parseClass(Node node) function,
 144  *  if isMember(node) is true, the function is required to return an instance
 145  *  of the helper class, instance, s.t. instance.getNode() == node.
 146  *  And if isMember(node) is false, this throws an assertion failure in debug
 147  *  mode and has undefined behaviour if not in debug mode.
 148  * -Only public facing constructors, parseClass(node), and mk*() functions are
 149  *  considered privileged functions for the helper class.
 150  * -Only privileged functions may use private constructors, and access
 151  *  private data members.
 152  * -All non-privileged functions are considered utility functions and
 153  *  must use a privileged function in order to create an instance of the class.
 154  */
 155
 156 /**
 157  * Section 3: Guard Conditions Misc.
 158  *
 159  *
 160  *  variable_order x y =
 161  *    if (meta_kind_variable x) and (meta_kind_variable y)
 162  *    then node_order x y
 163  *    else if (meta_kind_variable x)
 164  *    then false
 165  *    else if (meta_kind_variable y)
 166  *    then true
 167  *    else node_order x y
 168  *
 169  *  var_list_len vl =
 170  *    match vl with
 171  *       variable -> 1
 172  *     | (* [variable]) -> len [variable]
 173  *
 174  *  order res =
 175  *    match res with
 176  *       Empty -> (0,Node::null())
 177  *     | NonEmpty(vl) -> (var_list_len vl, vl)
 178  *
 179  *  var_listOrder a b = tuple_cmp (order a) (order b)
 180  *
 181  *  monomialVarList monomial =
 182  *    match monomial with
 183  *        constant -> Empty
 184  *      | var_list -> NonEmpty(var_list)
 185  *      | (* constant' var_list') -> NonEmpty(var_list')
 186  *
 187  *  monoOrder m0 m1 = var_listOrder (monomialVarList m0) (monomialVarList m1)
 188  *
 189  *  integerMonomial mono =
 190  *    forall varHasTypeInteger (monomialVarList mono)
 191  *
 192  *  realMonomial mono = not (integerMonomial mono)
 193  *
 194  *  constantMonomial monomial =
 195  *    match monomial with
 196  *        constant -> true
 197  *      | var_list -> false
 198  *      | (* constant' var_list') -> false
 199  *
 200  *  monomialCoefficient monomial =
 201  *    match monomial with
 202  *        constant -> constant
 203  *      | var_list -> Constant(1)
 204  *      | (* constant' var_list') -> constant'
 205  *
 206  *  monomialList polynomial =
 207  *    match polynomial with
 208  *        monomial -> monomial::[]
 209  *      | (+ [monomial]) -> [monomial]
 210  */
 211
 212 /**
 213  * A NodeWrapper is a class that is a thinly veiled container of a Node object.
 214  */
 215 class NodeWrapper {
 216 private:
 217   Node node;
 218 public:
 219   NodeWrapper(Node n) : node(n) {}
 220   const Node& getNode() const { return node; }
 221 };/* class NodeWrapper */
 222
 223
 224 class Variable : public NodeWrapper {
 225 public:
 226   Variable(Node n) : NodeWrapper(n) {
 227     Assert(isMember(getNode()));
 228   }
 229
 230   // TODO: check if it's a theory leaf also
 231   static bool isMember(Node n) {
 232     Kind k = n.getKind();
 233     switch(k){
 234     case kind::CONST_RATIONAL:
 235       return false;
 236     case kind::INTS_DIVISION:
 237     case kind::INTS_MODULUS:
 238     case kind::DIVISION:
 239     case kind::INTS_DIVISION_TOTAL:
 240     case kind::INTS_MODULUS_TOTAL:
 241     case kind::DIVISION_TOTAL:
 242       return isDivMember(n);
 243     default:
 244       return (!isRelationOperator(k)) &&
 245         (Theory::isLeafOf(n, theory::THEORY_ARITH));
 246     }
 247   }
 248
 249   static bool isDivMember(Node n);
 250   bool isDivLike() const{
 251     return isDivMember(getNode());
 252   }
 253
 254   bool isNormalForm() { return isMember(getNode()); }
 255
 256   bool isIntegral() const {
 257     return getNode().getType().isInteger();
 258   }
 259
 260   bool isMetaKindVariable() const {
 261     return getNode().isVar();
 262   }
 263
 264   bool operator<(const Variable& v) const {
 265     bool thisIsVariable = isMetaKindVariable();
 266     bool vIsVariable = v.isMetaKindVariable();
 267
 268     if(thisIsVariable == vIsVariable){
 269       bool thisIsInteger = isIntegral();
 270       bool vIsInteger = v.isIntegral();
 271       if(thisIsInteger == vIsInteger){
 272         return getNode() < v.getNode();
 273       }else{
 274         return thisIsInteger && !vIsInteger;
 275       }
 276     }else{
 277       return thisIsVariable && !vIsVariable;
 278     }
 279   }
 280
 281   bool operator==(const Variable& v) const { return getNode() == v.getNode();}
 282
 283 };/* class Variable */
 284
 285
 286 class Constant : public NodeWrapper {
 287 public:
 288   Constant(Node n) : NodeWrapper(n) {
 289     Assert(isMember(getNode()));
 290   }
 291
 292   static bool isMember(Node n) {
 293     return n.getKind() == kind::CONST_RATIONAL;
 294   }
 295
 296   bool isNormalForm() { return isMember(getNode()); }
 297
 298   static Constant mkConstant(Node n) {
 299     Assert(n.getKind() == kind::CONST_RATIONAL);
 300     return Constant(n);
 301   }
 302
 303   static Constant mkConstant(const Rational& rat) {
 304     return Constant(mkRationalNode(rat));
 305   }
 306
 307   static Constant mkZero() {
 308     return mkConstant(Rational(0));
 309   }
 310
 311   static Constant mkOne() {
 312     return mkConstant(Rational(1));
 313   }
 314
 315   const Rational& getValue() const {
 316     return getNode().getConst<Rational>();
 317   }
 318
 319   bool isIntegral() const { return getValue().isIntegral(); }
 320
 321   int sgn() const { return getValue().sgn(); }
 322
 323   bool isZero() const { return sgn() == 0; }
 324   bool isNegative() const { return sgn() < 0; }
 325   bool isPositive() const { return sgn() > 0; }
 326
 327   bool isOne() const { return getValue() == 1; }
 328
 329   Constant operator*(const Rational& other) const {
 330     return mkConstant(getValue() * other);
 331   }
 332
 333   Constant operator*(const Constant& other) const {
 334     return mkConstant(getValue() * other.getValue());
 335   }
 336   Constant operator+(const Constant& other) const {
 337     return mkConstant(getValue() + other.getValue());
 338   }
 339   Constant operator-() const {
 340     return mkConstant(-getValue());
 341   }
 342
 343   Constant inverse() const{
 344     Assert(!isZero());
 345     return mkConstant(getValue().inverse());
 346   }
 347
 348   bool operator<(const Constant& other) const {
 349     return getValue() < other.getValue();
 350   }
 351
 352   bool operator==(const Constant& other) const {
 353     //Rely on node uniqueness.
 354     return getNode() == other.getNode();
 355   }
 356
 357   Constant abs() const {
 358     if(isNegative()){
 359       return -(*this);
 360     }else{
 361       return (*this);
 362     }
 363   }
 364
 365   uint32_t length() const{
 366     Assert(isIntegral());
 367     return getValue().getNumerator().length();
 368   }
 369
 370 };/* class Constant */
 371
 372
 373 template <class GetNodeIterator>
 374 inline Node makeNode(Kind k, GetNodeIterator start, GetNodeIterator end) {
 375   NodeBuilder<> nb(k);
 376
 377   while(start != end) {
 378     nb << (*start).getNode();
 379     ++start;
 380   }
 381
 382   return Node(nb);
 383 }/* makeNode<GetNodeIterator>(Kind, iterator, iterator) */
 384
 385
 386 template <class GetNodeIterator, class T>
 387 static void copy_range(GetNodeIterator begin, GetNodeIterator end, std::vector<T>& result){
 388   while(begin != end){
 389     result.push_back(*begin);
 390     ++begin;
 391   }
 392 }
 393
 394 template <class GetNodeIterator, class T>
 395 static void merge_ranges(GetNodeIterator first1,
 396                   GetNodeIterator last1,
 397                   GetNodeIterator first2,
 398                   GetNodeIterator last2,
 399                   std::vector<T>& result) {
 400
 401   while(first1 != last1 && first2 != last2){
 402     if( (*first1) < (*first2) ){
 403       result.push_back(*first1);
 404       ++ first1;
 405     }else{
 406       result.push_back(*first2);
 407       ++ first2;
 408     }
 409   }
 410   copy_range(first1, last1, result);
 411   copy_range(first2, last2, result);
 412 }
 413
 414 /**
 415  * A VarList is a sorted list of variables representing a product.
 416  * If the VarList is empty, it represents an empty product or 1.
 417  * If the VarList has size 1, it represents a single variable.
 418  *
 419  * A non-sorted VarList can never be successfully made in debug mode.
 420  */
 421 class VarList : public NodeWrapper {
 422 private:
 423
 424   static Node multList(const std::vector<Variable>& list) {
 425     Assert(list.size() >= 2);
 426
 427     return makeNode(kind::MULT, list.begin(), list.end());
 428   }
 429
 430   VarList() : NodeWrapper(Node::null()) {}
 431
 432   VarList(Node n) : NodeWrapper(n) {
 433     Assert(isSorted(begin(), end()));
 434   }
 435
 436   typedef expr::NodeSelfIterator internal_iterator;
 437
 438   internal_iterator internalBegin() const {
 439     if(singleton()){
 440       return expr::NodeSelfIterator::self(getNode());
 441     }else{
 442       return getNode().begin();
 443     }
 444   }
 445
 446   internal_iterator internalEnd() const {
 447     if(singleton()){
 448       return expr::NodeSelfIterator::selfEnd(getNode());
 449     }else{
 450       return getNode().end();
 451     }
 452   }
 453
 454 public:
 455
 456   class iterator {
 457   private:
 458     internal_iterator d_iter;
 459
 460   public:
 461     explicit iterator(internal_iterator i) : d_iter(i) {}
 462
 463     inline Variable operator*() {
 464       return Variable(*d_iter);
 465     }
 466
 467     bool operator==(const iterator& i) {
 468       return d_iter == i.d_iter;
 469     }
 470
 471     bool operator!=(const iterator& i) {
 472       return d_iter != i.d_iter;
 473     }
 474
 475     iterator operator++() {
 476       ++d_iter;
 477       return *this;
 478     }
 479
 480     iterator operator++(int) {
 481       return iterator(d_iter++);
 482     }
 483   };
 484
 485   iterator begin() const {
 486     return iterator(internalBegin());
 487   }
 488
 489   iterator end() const {
 490     return iterator(internalEnd());
 491   }
 492
 493   Variable getHead() const {
 494     Assert(!empty());
 495     return *(begin());
 496   }
 497
 498   VarList(Variable v) : NodeWrapper(v.getNode()) {
 499     Assert(isSorted(begin(), end()));
 500   }
 501
 502   VarList(const std::vector<Variable>& l) : NodeWrapper(multList(l)) {
 503     Assert(l.size() >= 2);
 504     Assert(isSorted(begin(), end()));
 505   }
 506
 507   static bool isMember(Node n);
 508
 509   bool isNormalForm() const {
 510     return !empty();
 511   }
 512
 513   static VarList mkEmptyVarList() {
 514     return VarList();
 515   }
 516
 517
 518   /** There are no restrictions on the size of l */
 519   static VarList mkVarList(const std::vector<Variable>& l) {
 520     if(l.size() == 0) {
 521       return mkEmptyVarList();
 522     } else if(l.size() == 1) {
 523       return VarList((*l.begin()).getNode());
 524     } else {
 525       return VarList(l);
 526     }
 527   }
 528
 529   bool empty() const { return getNode().isNull(); }
 530   bool singleton() const {
 531     return !empty() && getNode().getKind() != kind::MULT;
 532   }
 533
 534   int size() const {
 535     if(singleton())
 536       return 1;
 537     else
 538       return getNode().getNumChildren();
 539   }
 540
 541   static VarList parseVarList(Node n);
 542
 543   VarList operator*(const VarList& vl) const;
 544
 545   int cmp(const VarList& vl) const;
 546
 547   bool operator<(const VarList& vl) const { return cmp(vl) < 0; }
 548
 549   bool operator==(const VarList& vl) const { return cmp(vl) == 0; }
 550
 551   bool isIntegral() const {
 552     for(iterator i = begin(), e=end(); i != e; ++i ){
 553       Variable var = *i;
 554       if(!var.isIntegral()){
 555         return false;
 556       }
 557     }
 558     return true;
 559   }
 560
 561 private:
 562   bool isSorted(iterator start, iterator end);
 563
 564 };/* class VarList */
 565
 566
 567 class Monomial : public NodeWrapper {
 568 private:
 569   Constant constant;
 570   VarList varList;
 571   Monomial(Node n, const Constant& c, const VarList& vl):
 572     NodeWrapper(n), constant(c), varList(vl)
 573   {
 574     Assert(!c.isZero() ||  vl.empty() );
 575     Assert( c.isZero() || !vl.empty() );
 576
 577     Assert(!c.isOne() || !multStructured(n));
 578   }
 579
 580   static Node makeMultNode(const Constant& c, const VarList& vl) {
 581     Assert(!c.isZero());
 582     Assert(!c.isOne());
 583     Assert(!vl.empty());
 584     return NodeManager::currentNM()->mkNode(kind::MULT, c.getNode(), vl.getNode());
 585   }
 586
 587   static bool multStructured(Node n) {
 588     return n.getKind() ==  kind::MULT &&
 589       n[0].getKind() == kind::CONST_RATIONAL &&
 590       n.getNumChildren() == 2;
 591   }
 592
 593 public:
 594
 595   Monomial(const Constant& c):
 596     NodeWrapper(c.getNode()), constant(c), varList(VarList::mkEmptyVarList())
 597   { }
 598
 599   Monomial(const VarList& vl):
 600     NodeWrapper(vl.getNode()), constant(Constant::mkConstant(1)), varList(vl)
 601   {
 602     Assert( !varList.empty() );
 603   }
 604
 605   Monomial(const Constant& c, const VarList& vl):
 606     NodeWrapper(makeMultNode(c,vl)), constant(c), varList(vl)
 607   {
 608     Assert( !c.isZero() );
 609     Assert( !c.isOne() );
 610     Assert( !varList.empty() );
 611
 612     Assert(multStructured(getNode()));
 613   }
 614
 615   static bool isMember(TNode n);
 616
 617   /** Makes a monomial with no restrictions on c and vl. */
 618   static Monomial mkMonomial(const Constant& c, const VarList& vl);
 619
 620   static Monomial mkMonomial(const Variable& v){
 621     return Monomial(VarList(v));
 622   }
 623
 624   static Monomial parseMonomial(Node n);
 625
 626   static Monomial mkZero() {
 627     return Monomial(Constant::mkConstant(0));
 628   }
 629   static Monomial mkOne() {
 630     return Monomial(Constant::mkConstant(1));
 631   }
 632   const Constant& getConstant() const { return constant; }
 633   const VarList& getVarList() const { return varList; }
 634
 635   bool isConstant() const {
 636     return varList.empty();
 637   }
 638
 639   bool isZero() const {
 640     return constant.isZero();
 641   }
 642
 643   bool coefficientIsOne() const {
 644     return constant.isOne();
 645   }
 646
 647   bool absCoefficientIsOne() const {
 648     return coefficientIsOne() || constant.getValue() == -1;
 649   }
 650
 651   bool constantIsPositive() const {
 652     return getConstant().isPositive();
 653   }
 654
 655   Monomial operator*(const Rational& q) const;
 656   Monomial operator*(const Constant& c) const;
 657   Monomial operator*(const Monomial& mono) const;
 658
 659   Monomial operator-() const{
 660     return (*this) * Rational(-1);
 661   }
 662
 663
 664   int cmp(const Monomial& mono) const {
 665     return getVarList().cmp(mono.getVarList());
 666   }
 667
 668   bool operator<(const Monomial& vl) const {
 669     return cmp(vl) < 0;
 670   }
 671
 672   bool operator==(const Monomial& vl) const {
 673     return cmp(vl) == 0;
 674   }
 675
 676   static bool isSorted(const std::vector<Monomial>& m) {
 677     return __gnu_cxx::is_sorted(m.begin(), m.end());
 678   }
 679
 680   static bool isStrictlySorted(const std::vector<Monomial>& m) {
 681     return isSorted(m) && std::adjacent_find(m.begin(),m.end()) == m.end();
 682   }
 683
 684   /**
 685    * The variable product
 686    */
 687   bool integralVariables() const {
 688     return getVarList().isIntegral();
 689   }
 690
 691   /**
 692    * The coefficient of the monomial is integral.
 693    */
 694   bool integralCoefficient() const {
 695     return getConstant().isIntegral();
 696   }
 697
 698   /**
 699    * A Monomial is an "integral" monomial if the constant is integral.
 700    */
 701   bool isIntegral() const {
 702     return integralCoefficient() && integralVariables();
 703   }
 704
 705   /**
 706    * Given a sorted list of monomials, this function transforms this
 707    * into a strictly sorted list of monomials that does not contain zero.
 708    */
 709   static std::vector<Monomial> sumLikeTerms(const std::vector<Monomial>& monos);
 710
 711   bool absLessThan(const Monomial& other) const{
 712     return getConstant().abs() < other.getConstant().abs();
 713   }
 714
 715   uint32_t coefficientLength() const{
 716     return getConstant().length();
 717   }
 718
 719   void print() const;
 720   static void printList(const std::vector<Monomial>& list);
 721
 722 };/* class Monomial */
 723
 724 class SumPair;
 725 class Comparison;;
 726
 727 class Polynomial : public NodeWrapper {
 728 private:
 729   bool d_singleton;
 730
 731   Polynomial(TNode n) : NodeWrapper(n), d_singleton(Monomial::isMember(n)) {
 732     Assert(isMember(getNode()));
 733   }
 734
 735   static Node makePlusNode(const std::vector<Monomial>& m) {
 736     Assert(m.size() >= 2);
 737
 738     return makeNode(kind::PLUS, m.begin(), m.end());
 739   }
 740
 741   typedef expr::NodeSelfIterator internal_iterator;
 742
 743   internal_iterator internalBegin() const {
 744     if(singleton()){
 745       return expr::NodeSelfIterator::self(getNode());
 746     }else{
 747       return getNode().begin();
 748     }
 749   }
 750
 751   internal_iterator internalEnd() const {
 752     if(singleton()){
 753       return expr::NodeSelfIterator::selfEnd(getNode());
 754     }else{
 755       return getNode().end();
 756     }
 757   }
 758
 759   bool singleton() const { return d_singleton; }
 760
 761 public:
 762   static bool isMember(TNode n) {
 763     if(Monomial::isMember(n)){
 764       return true;
 765     }else if(n.getKind() == kind::PLUS){
 766       Assert(n.getNumChildren() >= 2);
 767       Node::iterator currIter = n.begin(), end = n.end();
 768       Node prev = *currIter;
 769       if(!Monomial::isMember(prev)){
 770         return false;
 771       }
 772
 773       Monomial mprev = Monomial::parseMonomial(prev);
 774       ++currIter;
 775       for(; currIter != end; ++currIter){
 776         Node curr = *currIter;
 777         if(!Monomial::isMember(curr)){
 778           return false;
 779         }
 780         Monomial mcurr = Monomial::parseMonomial(curr);
 781         if(!(mprev < mcurr)){
 782           return false;
 783         }
 784         mprev = mcurr;
 785       }
 786       return true;
 787     } else {
 788       return false;
 789     }
 790   }
 791
 792   class iterator {
 793   private:
 794     internal_iterator d_iter;
 795
 796   public:
 797     explicit iterator(internal_iterator i) : d_iter(i) {}
 798
 799     inline Monomial operator*() {
 800       return Monomial::parseMonomial(*d_iter);
 801     }
 802
 803     bool operator==(const iterator& i) {
 804       return d_iter == i.d_iter;
 805     }
 806
 807     bool operator!=(const iterator& i) {
 808       return d_iter != i.d_iter;
 809     }
 810
 811     iterator operator++() {
 812       ++d_iter;
 813       return *this;
 814     }
 815
 816     iterator operator++(int) {
 817       return iterator(d_iter++);
 818     }
 819   };
 820
 821   iterator begin() const { return iterator(internalBegin()); }
 822   iterator end() const {  return iterator(internalEnd()); }
 823
 824   Polynomial(const Monomial& m):
 825     NodeWrapper(m.getNode()), d_singleton(true)
 826   {}
 827
 828   Polynomial(const std::vector<Monomial>& m):
 829     NodeWrapper(makePlusNode(m)), d_singleton(false)
 830   {
 831     Assert( m.size() >= 2);
 832     Assert( Monomial::isStrictlySorted(m) );
 833   }
 834
 835   static Polynomial mkPolynomial(const Variable& v){
 836     return Monomial::mkMonomial(v);
 837   }
 838
 839   static Polynomial mkPolynomial(const std::vector<Monomial>& m) {
 840     if(m.size() == 0) {
 841       return Polynomial(Monomial::mkZero());
 842     } else if(m.size() == 1) {
 843       return Polynomial((*m.begin()));
 844     } else {
 845       return Polynomial(m);
 846     }
 847   }
 848
 849   static Polynomial parsePolynomial(Node n) {
 850     return Polynomial(n);
 851   }
 852
 853   static Polynomial mkZero() {
 854     return Polynomial(Monomial::mkZero());
 855   }
 856   static Polynomial mkOne() {
 857     return Polynomial(Monomial::mkOne());
 858   }
 859   bool isZero() const {
 860     return singleton() && (getHead().isZero());
 861   }
 862
 863   bool isConstant() const {
 864     return singleton() && (getHead().isConstant());
 865   }
 866
 867   bool containsConstant() const {
 868     return getHead().isConstant();
 869   }
 870
 871   uint32_t size() const{
 872     if(singleton()){
 873       return 1;
 874     }else{
 875       Assert(getNode().getKind() == kind::PLUS);
 876       return getNode().getNumChildren();
 877     }
 878   }
 879
 880   Monomial getHead() const {
 881     return *(begin());
 882   }
 883
 884   Polynomial getTail() const {
 885     Assert(! singleton());
 886
 887     iterator tailStart = begin();
 888     ++tailStart;
 889     std::vector<Monomial> subrange;
 890     copy_range(tailStart, end(), subrange);
 891     return mkPolynomial(subrange);
 892   }
 893
 894   Monomial minimumVariableMonomial() const;
 895   bool variableMonomialAreStrictlyGreater(const Monomial& m) const;
 896
 897   void printList() const {
 898     if(Debug.isOn("normal-form")){
 899       Debug("normal-form") << "start list" << std::endl;
 900       for(iterator i = begin(), oend = end(); i != oend; ++i) {
 901         const Monomial& m =*i;
 902         m.print();
 903       }
 904       Debug("normal-form") << "end list" << std::endl;
 905     }
 906   }
 907
 908   /** A Polynomial is an "integral" polynomial if all of the monomials are integral. */
 909   bool allIntegralVariables() const {
 910     for(iterator i = begin(), e=end(); i!=e; ++i){
 911       if(!(*i).integralVariables()){
 912         return false;
 913       }
 914     }
 915     return true;
 916   }
 917
 918   /**
 919    * A Polynomial is an "integral" polynomial if all of the monomials are integral
 920    * and all of the coefficients are Integral. */
 921   bool isIntegral() const {
 922     for(iterator i = begin(), e=end(); i!=e; ++i){
 923       if(!(*i).isIntegral()){
 924         return false;
 925       }
 926     }
 927     return true;
 928   }
 929
 930   /**
 931    * Selects a minimal monomial in the polynomial by the absolute value of
 932    * the coefficient.
 933    */
 934   Monomial selectAbsMinimum() const;
 935
 936   /** Returns true if the absolute value of the head coefficient is one. */
 937   bool leadingCoefficientIsAbsOne() const;
 938   bool leadingCoefficientIsPositive() const;
 939   bool denominatorLCMIsOne() const;
 940   bool numeratorGCDIsOne() const;
 941
 942   /**
 943    * Returns the Least Common Multiple of the denominators of the coefficients
 944    * of the monomials.
 945    */
 946   Integer denominatorLCM() const;
 947
 948   /**
 949    * Returns the GCD of the numerators of the monomials.
 950    * Requires this to be an isIntegral() polynomial.
 951    */
 952   Integer numeratorGCD() const;
 953
 954   /**
 955    * Returns the GCD of the coefficients of the monomials.
 956    * Requires this to be an isIntegral() polynomial.
 957    */
 958   Integer gcd() const;
 959
 960   Polynomial exactDivide(const Integer& z) const {
 961     Assert(isIntegral());
 962     Constant invz = Constant::mkConstant(Rational(1,z));
 963     Polynomial prod = (*this) * Monomial(invz);
 964     Assert(prod.isIntegral());
 965     return prod;
 966   }
 967
 968   Polynomial operator+(const Polynomial& vl) const;
 969   Polynomial operator-(const Polynomial& vl) const;
 970   Polynomial operator-() const{
 971     return (*this) * Rational(-1);
 972   }
 973
 974   Polynomial operator*(const Rational& q) const;
 975   Polynomial operator*(const Constant& c) const;
 976   Polynomial operator*(const Monomial& mono) const;
 977
 978   Polynomial operator*(const Polynomial& poly) const;
 979
 980   /**
 981    * Viewing the integer polynomial as a list [(* coeff_i mono_i)]
 982    * The quotient and remainder of p divided by the non-zero integer z is:
 983    *   q := [(* floor(coeff_i/z) mono_i )]
 984    *   r := [(* rem(coeff_i/z) mono_i)]
 985    * computeQR(p,z) returns the node (+ q r).
 986    *
 987    * q and r are members of the Polynomial class.
 988    * For example:
 989    * computeQR( p = (+ 5 (* 3 x) (* 8 y)) , z = 2) returns
 990    *   (+ (+ 2 x (* 4 y)) (+ 1 x))
 991    */
 992   static Node computeQR(const Polynomial& p, const Integer& z);
 993
 994   /** Returns the coefficient associated with the VarList in the polynomial. */
 995   Constant getCoefficient(const VarList& vl) const;
 996
 997   uint32_t maxLength() const{
 998     iterator i = begin(), e=end();
 999     if( i == e){
1000       return 1;
1001     }else{
1002       uint32_t max = (*i).coefficientLength();
1003       ++i;
1004       for(; i!=e; ++i){
1005         uint32_t curr = (*i).coefficientLength();
1006         if(curr > max){
1007           max = curr;
1008         }
1009       }
1010       return max;
1011     }
1012   }
1013
1014   uint32_t numMonomials() const {
1015     if( getNode().getKind() == kind::PLUS ){
1016       return getNode().getNumChildren();
1017     }else if(isZero()){
1018       return 0;
1019     }else{
1020       return 1;
1021     }
1022   }
1023
1024   const Rational& asConstant() const{
1025     Assert(isConstant());
1026     return getNode().getConst<Rational>();
1027     //return getHead().getConstant().getValue();
1028   }
1029
1030   bool isVarList() const {
1031     if(singleton()){
1032       return VarList::isMember(getNode());
1033     }else{
1034       return false;
1035     }
1036   }
1037
1038   VarList asVarList() const {
1039     Assert(isVarList());
1040     return getHead().getVarList();
1041   }
1042
1043   friend class SumPair;
1044   friend class Comparison;
1045
1046   /** Returns a node that if asserted ensures v is the abs of this polynomial.*/
1047   Node makeAbsCondition(Variable v){
1048     return makeAbsCondition(v, *this);
1049   }
1050
1051   /** Returns a node that if asserted ensures v is the abs of p.*/
1052   static Node makeAbsCondition(Variable v, Polynomial p);
1053
1054 };/* class Polynomial */
1055
1056
1057 /**
1058  * SumPair is a utility class that extends polynomials for use in computations.
1059  * A SumPair is always a combination of (+ p c) where
1060  *  c is a constant and p is a polynomial such that p = 0 or !p.containsConstant().
1061  *
1062  * These are a useful utility for representing the equation p = c as (+ p -c) where the pair
1063  * is known to implicitly be equal to 0.
1064  *
1065  * SumPairs do not have unique representations due to the potential for p = 0.
1066  * This makes them inappropriate for normal forms.
1067  */
1068 class SumPair : public NodeWrapper {
1069 private:
1070   static Node toNode(const Polynomial& p, const Constant& c){
1071     return NodeManager::currentNM()->mkNode(kind::PLUS, p.getNode(), c.getNode());
1072   }
1073
1074   SumPair(TNode n) :
1075     NodeWrapper(n)
1076   {
1077     Assert(isNormalForm());
1078   }
1079
1080 public:
1081
1082   SumPair(const Polynomial& p):
1083     NodeWrapper(toNode(p, Constant::mkConstant(0)))
1084   {
1085     Assert(isNormalForm());
1086   }
1087
1088   SumPair(const Polynomial& p, const Constant& c):
1089     NodeWrapper(toNode(p, c))
1090   {
1091     Assert(isNormalForm());
1092   }
1093
1094   static bool isMember(TNode n) {
1095     if(n.getKind() == kind::PLUS && n.getNumChildren() == 2){
1096       if(Constant::isMember(n[1])){
1097         if(Polynomial::isMember(n[0])){
1098           Polynomial p = Polynomial::parsePolynomial(n[0]);
1099           return p.isZero() || (!p.containsConstant());
1100         }else{
1101           return false;
1102         }
1103       }else{
1104         return false;
1105       }
1106     }else{
1107       return false;
1108     }
1109   }
1110
1111   bool isNormalForm() const {
1112     return isMember(getNode());
1113   }
1114
1115   Polynomial getPolynomial() const {
1116     return Polynomial::parsePolynomial(getNode()[0]);
1117   }
1118
1119   Constant getConstant() const {
1120     return Constant::mkConstant((getNode())[1]);
1121   }
1122
1123   SumPair operator+(const SumPair& other) const {
1124     return SumPair(getPolynomial() + other.getPolynomial(),
1125                    getConstant() + other.getConstant());
1126   }
1127
1128   SumPair operator*(const Constant& c) const {
1129     return SumPair(getPolynomial() * c, getConstant() * c);
1130   }
1131
1132   SumPair operator-(const SumPair& other) const {
1133     return (*this) + (other * Constant::mkConstant(-1));
1134   }
1135
1136   static SumPair mkSumPair(const Polynomial& p);
1137
1138   static SumPair mkSumPair(const Variable& var){
1139     return SumPair(Polynomial::mkPolynomial(var));
1140   }
1141
1142   static SumPair parseSumPair(TNode n){
1143     return SumPair(n);
1144   }
1145
1146   bool isIntegral() const{
1147     return getConstant().isIntegral() && getPolynomial().isIntegral();
1148   }
1149
1150   bool isConstant() const {
1151     return getPolynomial().isZero();
1152   }
1153
1154   bool isZero() const {
1155     return getConstant().isZero() && isConstant();
1156   }
1157
1158   /**
1159    * Returns the greatest common divisor of gcd(getPolynomial()) and getConstant().
1160    * The SumPair must be integral.
1161    */
1162   Integer gcd() const {
1163     Assert(isIntegral());
1164     return (getPolynomial().gcd()).gcd(getConstant().getValue().getNumerator());
1165   }
1166
1167   uint32_t maxLength() const {
1168     Assert(isIntegral());
1169     return std::max(getPolynomial().maxLength(), getConstant().length());
1170   }
1171
1172   static SumPair mkZero() {
1173     return SumPair(Polynomial::mkZero(), Constant::mkConstant(0));
1174   }
1175
1176   static Node computeQR(const SumPair& sp, const Integer& div);
1177
1178 };/* class SumPair */
1179
1180 /* class OrderedPolynomialPair { */
1181 /* private: */
1182 /*   Polynomial d_first; */
1183 /*   Polynomial d_second; */
1184 /* public: */
1185 /*   OrderedPolynomialPair(const Polynomial& f, const Polynomial& s) */
1186 /*     : d_first(f), */
1187 /*       d_second(s) */
1188 /*   {} */
1189
1190 /*   /\** Returns the first part of the pair. *\/ */
1191 /*   const Polynomial& getFirst() const { */
1192 /*     return d_first; */
1193 /*   } */
1194
1195 /*   /\** Returns the second part of the pair. *\/ */
1196 /*   const Polynomial& getSecond() const { */
1197 /*     return d_second; */
1198 /*   } */
1199
1200 /*   OrderedPolynomialPair operator*(const Constant& c) const; */
1201 /*   OrderedPolynomialPair operator+(const Polynomial& p) const; */
1202
1203 /*   /\** Returns true if both of the polynomials are constant. *\/ */
1204 /*   bool isConstant() const; */
1205
1206 /*   /\** */
1207 /*    * Evaluates an isConstant() ordered pair as if */
1208 /*    *   (k getFirst() getRight()) */
1209 /*    *\/ */
1210 /*   bool evaluateConstant(Kind k) const; */
1211
1212 /*   /\** */
1213 /*    * Returns the Least Common Multiple of the monomials */
1214 /*    * on the lefthand side and the constant on the right. */
1215 /*    *\/ */
1216 /*   Integer denominatorLCM() const; */
1217
1218 /*   /\** Constructs a SumPair. *\/ */
1219 /*   SumPair toSumPair() const; */
1220
1221
1222 /*   OrderedPolynomialPair divideByGCD() const; */
1223 /*   OrderedPolynomialPair multiplyConstant(const Constant& c) const; */
1224
1225 /*   /\** */
1226 /*    * Returns true if all of the variables are integers, */
1227 /*    * and the coefficients are integers. */
1228 /*    *\/ */
1229 /*   bool isIntegral() const; */
1230
1231 /*   /\** Returns true if all of the variables are integers. *\/ */
1232 /*   bool allIntegralVariables() const { */
1233 /*     return getFirst().allIntegralVariables() && getSecond().allIntegralVariables(); */
1234 /*   } */
1235 /* }; */
1236
1237 class Comparison : public NodeWrapper {
1238 private:
1239
1240   static Node toNode(Kind k, const Polynomial& l, const Constant& c);
1241   static Node toNode(Kind k, const Polynomial& l, const Polynomial& r);
1242
1243   Comparison(TNode n);
1244
1245   /**
1246    * Creates a node in normal form equivalent to (= l 0).
1247    * All variables in l are integral.
1248    */
1249   static Node mkIntEquality(const Polynomial& l);
1250
1251   /**
1252    * Creates a comparison equivalent to (k l 0).
1253    * k is either GT or GEQ.
1254    * All variables in l are integral.
1255    */
1256   static Node mkIntInequality(Kind k, const Polynomial& l);
1257
1258   /**
1259    * Creates a node equivalent to (= l 0).
1260    * It is not the case that all variables in l are integral.
1261    */
1262   static Node mkRatEquality(const Polynomial& l);
1263
1264   /**
1265    * Creates a comparison equivalent to (k l 0).
1266    * k is either GT or GEQ.
1267    * It is not the case that all variables in l are integral.
1268    */
1269   static Node mkRatInequality(Kind k, const Polynomial& l);
1270
1271 public:
1272
1273   Comparison(bool val) :
1274     NodeWrapper(NodeManager::currentNM()->mkConst(val))
1275   { }
1276
1277   /**
1278    * Given a literal to TheoryArith return a single kind to
1279    * to indicate its underlying structure.
1280    * The function returns the following in each case:
1281    * - (K left right)           -> K where is either EQUAL, GT, or GEQ
1282    * - (CONST_BOOLEAN b)        -> CONST_BOOLEAN
1283    * - (NOT (EQUAL left right)) -> DISTINCT
1284    * - (NOT (GT left right))    -> LEQ
1285    * - (NOT (GEQ left right))   -> LT
1286    * If none of these match, it returns UNDEFINED_KIND.
1287    */
1288   static Kind comparisonKind(TNode literal);
1289
1290   Kind comparisonKind() const { return comparisonKind(getNode()); }
1291
1292   static Comparison mkComparison(Kind k, const Polynomial& l, const Polynomial& r);
1293
1294   /** Returns true if the comparison is a boolean constant. */
1295   bool isBoolean() const;
1296
1297   /**
1298    * Returns true if the comparison is either a boolean term,
1299    * in integer normal form or mixed normal form.
1300    */
1301   bool isNormalForm() const;
1302
1303 private:
1304   bool isNormalGT() const;
1305   bool isNormalGEQ() const;
1306
1307   bool isNormalLT() const;
1308   bool isNormalLEQ() const;
1309
1310   bool isNormalEquality() const;
1311   bool isNormalDistinct() const;
1312   bool isNormalEqualityOrDisequality() const;
1313
1314   bool allIntegralVariables() const {
1315     return getLeft().allIntegralVariables() && getRight().allIntegralVariables();
1316   }
1317   bool rightIsConstant() const;
1318
1319 public:
1320   Polynomial getLeft() const;
1321   Polynomial getRight() const;
1322
1323   /* /\** Normal form check if at least one variable is real. *\/ */
1324   /* bool isMixedCompareNormalForm() const; */
1325
1326   /* /\** Normal form check if at least one variable is real. *\/ */
1327   /* bool isMixedEqualsNormalForm() const; */
1328
1329   /* /\** Normal form check is all variables are integer.*\/ */
1330   /* bool isIntegerCompareNormalForm() const; */
1331
1332   /* /\** Normal form check is all variables are integer.*\/ */
1333   /* bool isIntegerEqualsNormalForm() const; */
1334
1335
1336   /**
1337    * Returns true if all of the variables are integers, the coefficients are integers,
1338    * and the right hand coefficient is an integer.
1339    */
1340   bool debugIsIntegral() const;
1341
1342   static Comparison parseNormalForm(TNode n);
1343
1344   inline static bool isNormalAtom(TNode n){
1345     Comparison parse = Comparison::parseNormalForm(n);
1346     return parse.isNormalForm();
1347   }
1348
1349   SumPair toSumPair() const;
1350
1351   Polynomial normalizedVariablePart() const;
1352   DeltaRational normalizedDeltaRational() const;
1353
1354 };/* class Comparison */
1355
1356 }/* CVC4::theory::arith namespace */
1357 }/* CVC4::theory namespace */
1358 }/* CVC4 namespace */
1359
1360 #endif /* __CVC4__THEORY__ARITH__NORMAL_FORM_H */