src/theory/arith/normal_form.h

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