src/theory/arith/normal_form.h

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