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   uint32_t size() const{
 858     if(singleton()){
 859       return 1;
 860     }else{
 861       Assert(getNode().getKind() == kind::PLUS);
 862       return getNode().getNumChildren();
 863     }
 864   }
 865
 866   Monomial getHead() const {
 867     return *(begin());
 868   }
 869
 870   Polynomial getTail() const {
 871     Assert(! singleton());
 872
 873     iterator tailStart = begin();
 874     ++tailStart;
 875     std::vector<Monomial> subrange;
 876     copy_range(tailStart, end(), subrange);
 877     return mkPolynomial(subrange);
 878   }
 879
 880   Monomial minimumVariableMonomial() const;
 881   bool variableMonomialAreStrictlyGreater(const Monomial& m) const;
 882
 883   void printList() const {
 884     if(Debug.isOn("normal-form")){
 885       Debug("normal-form") << "start list" << std::endl;
 886       for(iterator i = begin(), oend = end(); i != oend; ++i) {
 887         const Monomial& m =*i;
 888         m.print();
 889       }
 890       Debug("normal-form") << "end list" << std::endl;
 891     }
 892   }
 893
 894   /** A Polynomial is an "integral" polynomial if all of the monomials are integral. */
 895   bool allIntegralVariables() const {
 896     for(iterator i = begin(), e=end(); i!=e; ++i){
 897       if(!(*i).integralVariables()){
 898         return false;
 899       }
 900     }
 901     return true;
 902   }
 903
 904   /**
 905    * A Polynomial is an "integral" polynomial if all of the monomials are integral
 906    * and all of the coefficients are Integral. */
 907   bool isIntegral() const {
 908     for(iterator i = begin(), e=end(); i!=e; ++i){
 909       if(!(*i).isIntegral()){
 910         return false;
 911       }
 912     }
 913     return true;
 914   }
 915
 916   /**
 917    * Selects a minimal monomial in the polynomial by the absolute value of
 918    * the coefficient.
 919    */
 920   Monomial selectAbsMinimum() const;
 921
 922   /** Returns true if the absolute value of the head coefficient is one. */
 923   bool leadingCoefficientIsAbsOne() const;
 924   bool leadingCoefficientIsPositive() const;
 925   bool denominatorLCMIsOne() const;
 926   bool numeratorGCDIsOne() const;
 927
 928   /**
 929    * Returns the Least Common Multiple of the denominators of the coefficients
 930    * of the monomials.
 931    */
 932   Integer denominatorLCM() const;
 933
 934   /**
 935    * Returns the GCD of the numerators of the monomials.
 936    * Requires this to be an isIntegral() polynomial.
 937    */
 938   Integer numeratorGCD() const;
 939
 940   /**
 941    * Returns the GCD of the coefficients of the monomials.
 942    * Requires this to be an isIntegral() polynomial.
 943    */
 944   Integer gcd() const;
 945
 946   Polynomial exactDivide(const Integer& z) const {
 947     Assert(isIntegral());
 948     Constant invz = Constant::mkConstant(Rational(1,z));
 949     Polynomial prod = (*this) * Monomial(invz);
 950     Assert(prod.isIntegral());
 951     return prod;
 952   }
 953
 954   Polynomial operator+(const Polynomial& vl) const;
 955   Polynomial operator-(const Polynomial& vl) const;
 956   Polynomial operator-() const{
 957     return (*this) * Rational(-1);
 958   }
 959
 960   Polynomial operator*(const Rational& q) const;
 961   Polynomial operator*(const Constant& c) const;
 962   Polynomial operator*(const Monomial& mono) const;
 963
 964   Polynomial operator*(const Polynomial& poly) const;
 965
 966   /**
 967    * Viewing the integer polynomial as a list [(* coeff_i mono_i)]
 968    * The quotient and remainder of p divided by the non-zero integer z is:
 969    *   q := [(* floor(coeff_i/z) mono_i )]
 970    *   r := [(* rem(coeff_i/z) mono_i)]
 971    * computeQR(p,z) returns the node (+ q r).
 972    *
 973    * q and r are members of the Polynomial class.
 974    * For example:
 975    * computeQR( p = (+ 5 (* 3 x) (* 8 y)) , z = 2) returns
 976    *   (+ (+ 2 x (* 4 y)) (+ 1 x))
 977    */
 978   static Node computeQR(const Polynomial& p, const Integer& z);
 979
 980   /** Returns the coefficient associated with the VarList in the polynomial. */
 981   Constant getCoefficient(const VarList& vl) const;
 982
 983   uint32_t maxLength() const{
 984     iterator i = begin(), e=end();
 985     if( i == e){
 986       return 1;
 987     }else{
 988       uint32_t max = (*i).coefficientLength();
 989       ++i;
 990       for(; i!=e; ++i){
 991         uint32_t curr = (*i).coefficientLength();
 992         if(curr > max){
 993           max = curr;
 994         }
 995       }
 996       return max;
 997     }
 998   }
 999
1000   uint32_t numMonomials() const {
1001     if( getNode().getKind() == kind::PLUS ){
1002       return getNode().getNumChildren();
1003     }else if(isZero()){
1004       return 0;
1005     }else{
1006       return 1;
1007     }
1008   }
1009
1010   const Rational& asConstant() const{
1011     Assert(isConstant());
1012     return getNode().getConst<Rational>();
1013     //return getHead().getConstant().getValue();
1014   }
1015
1016   bool isVarList() const {
1017     if(singleton()){
1018       return VarList::isMember(getNode());
1019     }else{
1020       return false;
1021     }
1022   }
1023
1024   VarList asVarList() const {
1025     Assert(isVarList());
1026     return getHead().getVarList();
1027   }
1028
1029   friend class SumPair;
1030   friend class Comparison;;
1031
1032 };/* class Polynomial */
1033
1034
1035 /**
1036  * SumPair is a utility class that extends polynomials for use in computations.
1037  * A SumPair is always a combination of (+ p c) where
1038  *  c is a constant and p is a polynomial such that p = 0 or !p.containsConstant().
1039  *
1040  * These are a useful utility for representing the equation p = c as (+ p -c) where the pair
1041  * is known to implicitly be equal to 0.
1042  *
1043  * SumPairs do not have unique representations due to the potential for p = 0.
1044  * This makes them inappropriate for normal forms.
1045  */
1046 class SumPair : public NodeWrapper {
1047 private:
1048   static Node toNode(const Polynomial& p, const Constant& c){
1049     return NodeManager::currentNM()->mkNode(kind::PLUS, p.getNode(), c.getNode());
1050   }
1051
1052   SumPair(TNode n) :
1053     NodeWrapper(n)
1054   {
1055     Assert(isNormalForm());
1056   }
1057
1058 public:
1059
1060   SumPair(const Polynomial& p):
1061     NodeWrapper(toNode(p, Constant::mkConstant(0)))
1062   {
1063     Assert(isNormalForm());
1064   }
1065
1066   SumPair(const Polynomial& p, const Constant& c):
1067     NodeWrapper(toNode(p, c))
1068   {
1069     Assert(isNormalForm());
1070   }
1071
1072   static bool isMember(TNode n) {
1073     if(n.getKind() == kind::PLUS && n.getNumChildren() == 2){
1074       if(Constant::isMember(n[1])){
1075         if(Polynomial::isMember(n[0])){
1076           Polynomial p = Polynomial::parsePolynomial(n[0]);
1077           return p.isZero() || (!p.containsConstant());
1078         }else{
1079           return false;
1080         }
1081       }else{
1082         return false;
1083       }
1084     }else{
1085       return false;
1086     }
1087   }
1088
1089   bool isNormalForm() const {
1090     return isMember(getNode());
1091   }
1092
1093   Polynomial getPolynomial() const {
1094     return Polynomial::parsePolynomial(getNode()[0]);
1095   }
1096
1097   Constant getConstant() const {
1098     return Constant::mkConstant((getNode())[1]);
1099   }
1100
1101   SumPair operator+(const SumPair& other) const {
1102     return SumPair(getPolynomial() + other.getPolynomial(),
1103                    getConstant() + other.getConstant());
1104   }
1105
1106   SumPair operator*(const Constant& c) const {
1107     return SumPair(getPolynomial() * c, getConstant() * c);
1108   }
1109
1110   SumPair operator-(const SumPair& other) const {
1111     return (*this) + (other * Constant::mkConstant(-1));
1112   }
1113
1114   static SumPair mkSumPair(const Polynomial& p);
1115
1116   static SumPair mkSumPair(const Variable& var){
1117     return SumPair(Polynomial::mkPolynomial(var));
1118   }
1119
1120   static SumPair parseSumPair(TNode n){
1121     return SumPair(n);
1122   }
1123
1124   bool isIntegral() const{
1125     return getConstant().isIntegral() && getPolynomial().isIntegral();
1126   }
1127
1128   bool isConstant() const {
1129     return getPolynomial().isZero();
1130   }
1131
1132   bool isZero() const {
1133     return getConstant().isZero() && isConstant();
1134   }
1135
1136   /**
1137    * Returns the greatest common divisor of gcd(getPolynomial()) and getConstant().
1138    * The SumPair must be integral.
1139    */
1140   Integer gcd() const {
1141     Assert(isIntegral());
1142     return (getPolynomial().gcd()).gcd(getConstant().getValue().getNumerator());
1143   }
1144
1145   uint32_t maxLength() const {
1146     Assert(isIntegral());
1147     return std::max(getPolynomial().maxLength(), getConstant().length());
1148   }
1149
1150   static SumPair mkZero() {
1151     return SumPair(Polynomial::mkZero(), Constant::mkConstant(0));
1152   }
1153
1154   static Node computeQR(const SumPair& sp, const Integer& div);
1155
1156 };/* class SumPair */
1157
1158 /* class OrderedPolynomialPair { */
1159 /* private: */
1160 /*   Polynomial d_first; */
1161 /*   Polynomial d_second; */
1162 /* public: */
1163 /*   OrderedPolynomialPair(const Polynomial& f, const Polynomial& s) */
1164 /*     : d_first(f), */
1165 /*       d_second(s) */
1166 /*   {} */
1167
1168 /*   /\** Returns the first part of the pair. *\/ */
1169 /*   const Polynomial& getFirst() const { */
1170 /*     return d_first; */
1171 /*   } */
1172
1173 /*   /\** Returns the second part of the pair. *\/ */
1174 /*   const Polynomial& getSecond() const { */
1175 /*     return d_second; */
1176 /*   } */
1177
1178 /*   OrderedPolynomialPair operator*(const Constant& c) const; */
1179 /*   OrderedPolynomialPair operator+(const Polynomial& p) const; */
1180
1181 /*   /\** Returns true if both of the polynomials are constant. *\/ */
1182 /*   bool isConstant() const; */
1183
1184 /*   /\** */
1185 /*    * Evaluates an isConstant() ordered pair as if */
1186 /*    *   (k getFirst() getRight()) */
1187 /*    *\/ */
1188 /*   bool evaluateConstant(Kind k) const; */
1189
1190 /*   /\** */
1191 /*    * Returns the Least Common Multiple of the monomials */
1192 /*    * on the lefthand side and the constant on the right. */
1193 /*    *\/ */
1194 /*   Integer denominatorLCM() const; */
1195
1196 /*   /\** Constructs a SumPair. *\/ */
1197 /*   SumPair toSumPair() const; */
1198
1199
1200 /*   OrderedPolynomialPair divideByGCD() const; */
1201 /*   OrderedPolynomialPair multiplyConstant(const Constant& c) const; */
1202
1203 /*   /\** */
1204 /*    * Returns true if all of the variables are integers, */
1205 /*    * and the coefficients are integers. */
1206 /*    *\/ */
1207 /*   bool isIntegral() const; */
1208
1209 /*   /\** Returns true if all of the variables are integers. *\/ */
1210 /*   bool allIntegralVariables() const { */
1211 /*     return getFirst().allIntegralVariables() && getSecond().allIntegralVariables(); */
1212 /*   } */
1213 /* }; */
1214
1215 class Comparison : public NodeWrapper {
1216 private:
1217
1218   static Node toNode(Kind k, const Polynomial& l, const Constant& c);
1219   static Node toNode(Kind k, const Polynomial& l, const Polynomial& r);
1220
1221   Comparison(TNode n);
1222
1223   /**
1224    * Creates a node in normal form equivalent to (= l 0).
1225    * All variables in l are integral.
1226    */
1227   static Node mkIntEquality(const Polynomial& l);
1228
1229   /**
1230    * Creates a comparison equivalent to (k l 0).
1231    * k is either GT or GEQ.
1232    * All variables in l are integral.
1233    */
1234   static Node mkIntInequality(Kind k, const Polynomial& l);
1235
1236   /**
1237    * Creates a node equivalent to (= l 0).
1238    * It is not the case that all variables in l are integral.
1239    */
1240   static Node mkRatEquality(const Polynomial& l);
1241
1242   /**
1243    * Creates a comparison equivalent to (k l 0).
1244    * k is either GT or GEQ.
1245    * It is not the case that all variables in l are integral.
1246    */
1247   static Node mkRatInequality(Kind k, const Polynomial& l);
1248
1249 public:
1250
1251   Comparison(bool val) :
1252     NodeWrapper(NodeManager::currentNM()->mkConst(val))
1253   { }
1254
1255   /**
1256    * Given a literal to TheoryArith return a single kind to
1257    * to indicate its underlying structure.
1258    * The function returns the following in each case:
1259    * - (K left right)           -> K where is either EQUAL, GT, or GEQ
1260    * - (CONST_BOOLEAN b)        -> CONST_BOOLEAN
1261    * - (NOT (EQUAL left right)) -> DISTINCT
1262    * - (NOT (GT left right))    -> LEQ
1263    * - (NOT (GEQ left right))   -> LT
1264    * If none of these match, it returns UNDEFINED_KIND.
1265    */
1266   static Kind comparisonKind(TNode literal);
1267
1268   Kind comparisonKind() const { return comparisonKind(getNode()); }
1269
1270   static Comparison mkComparison(Kind k, const Polynomial& l, const Polynomial& r);
1271
1272   /** Returns true if the comparison is a boolean constant. */
1273   bool isBoolean() const;
1274
1275   /**
1276    * Returns true if the comparison is either a boolean term,
1277    * in integer normal form or mixed normal form.
1278    */
1279   bool isNormalForm() const;
1280
1281 private:
1282   bool isNormalGT() const;
1283   bool isNormalGEQ() const;
1284
1285   bool isNormalLT() const;
1286   bool isNormalLEQ() const;
1287
1288   bool isNormalEquality() const;
1289   bool isNormalDistinct() const;
1290   bool isNormalEqualityOrDisequality() const;
1291
1292   bool allIntegralVariables() const {
1293     return getLeft().allIntegralVariables() && getRight().allIntegralVariables();
1294   }
1295   bool rightIsConstant() const;
1296
1297 public:
1298   Polynomial getLeft() const;
1299   Polynomial getRight() const;
1300
1301   /* /\** Normal form check if at least one variable is real. *\/ */
1302   /* bool isMixedCompareNormalForm() const; */
1303
1304   /* /\** Normal form check if at least one variable is real. *\/ */
1305   /* bool isMixedEqualsNormalForm() const; */
1306
1307   /* /\** Normal form check is all variables are integer.*\/ */
1308   /* bool isIntegerCompareNormalForm() const; */
1309
1310   /* /\** Normal form check is all variables are integer.*\/ */
1311   /* bool isIntegerEqualsNormalForm() const; */
1312
1313
1314   /**
1315    * Returns true if all of the variables are integers, the coefficients are integers,
1316    * and the right hand coefficient is an integer.
1317    */
1318   bool debugIsIntegral() const;
1319
1320   static Comparison parseNormalForm(TNode n);
1321
1322   inline static bool isNormalAtom(TNode n){
1323     Comparison parse = Comparison::parseNormalForm(n);
1324     return parse.isNormalForm();
1325   }
1326
1327   SumPair toSumPair() const;
1328
1329   Polynomial normalizedVariablePart() const;
1330   DeltaRational normalizedDeltaRational() const;
1331
1332 };/* class Comparison */
1333
1334 }/* CVC4::theory::arith namespace */
1335 }/* CVC4::theory namespace */
1336 }/* CVC4 namespace */
1337
1338 #endif /* __CVC4__THEORY__ARITH__NORMAL_FORM_H */