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/arith/delta_rational.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 isLeafMember(n);
 251     }
 252   }
 253
 254   static bool isLeafMember(Node n);
 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   size_t getComplexity() const;
 290 };/* class Variable */
 291
 292
 293 class Constant : public NodeWrapper {
 294 public:
 295   Constant(Node n) : NodeWrapper(n) {
 296     Assert(isMember(getNode()));
 297   }
 298
 299   static bool isMember(Node n) {
 300     return n.getKind() == kind::CONST_RATIONAL;
 301   }
 302
 303   bool isNormalForm() { return isMember(getNode()); }
 304
 305   static Constant mkConstant(Node n) {
 306     Assert(n.getKind() == kind::CONST_RATIONAL);
 307     return Constant(n);
 308   }
 309
 310   static Constant mkConstant(const Rational& rat);
 311
 312   static Constant mkZero() {
 313     return mkConstant(Rational(0));
 314   }
 315
 316   static Constant mkOne() {
 317     return mkConstant(Rational(1));
 318   }
 319
 320   const Rational& getValue() const {
 321     return getNode().getConst<Rational>();
 322   }
 323
 324   static int absCmp(const Constant& a, const Constant& b);
 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   size_t getComplexity() const;
 377
 378 };/* class Constant */
 379
 380
 381 template <class GetNodeIterator>
 382 inline Node makeNode(Kind k, GetNodeIterator start, GetNodeIterator end) {
 383   NodeBuilder<> nb(k);
 384
 385   while(start != end) {
 386     nb << (*start).getNode();
 387     ++start;
 388   }
 389
 390   return Node(nb);
 391 }/* makeNode<GetNodeIterator>(Kind, iterator, iterator) */
 392
 393
 394 template <class GetNodeIterator, class T>
 395 static void copy_range(GetNodeIterator begin, GetNodeIterator end, std::vector<T>& result){
 396   while(begin != end){
 397     result.push_back(*begin);
 398     ++begin;
 399   }
 400 }
 401
 402 template <class GetNodeIterator, class T>
 403 static void merge_ranges(GetNodeIterator first1,
 404                   GetNodeIterator last1,
 405                   GetNodeIterator first2,
 406                   GetNodeIterator last2,
 407                   std::vector<T>& result) {
 408
 409   while(first1 != last1 && first2 != last2){
 410     if( (*first1) < (*first2) ){
 411       result.push_back(*first1);
 412       ++ first1;
 413     }else{
 414       result.push_back(*first2);
 415       ++ first2;
 416     }
 417   }
 418   copy_range(first1, last1, result);
 419   copy_range(first2, last2, result);
 420 }
 421
 422 /**
 423  * A VarList is a sorted list of variables representing a product.
 424  * If the VarList is empty, it represents an empty product or 1.
 425  * If the VarList has size 1, it represents a single variable.
 426  *
 427  * A non-sorted VarList can never be successfully made in debug mode.
 428  */
 429 class VarList : public NodeWrapper {
 430 private:
 431
 432   static Node multList(const std::vector<Variable>& list) {
 433     Assert(list.size() >= 2);
 434
 435     return makeNode(kind::MULT, list.begin(), list.end());
 436   }
 437
 438   VarList() : NodeWrapper(Node::null()) {}
 439
 440   VarList(Node n) : NodeWrapper(n) {
 441     Assert(isSorted(begin(), end()));
 442   }
 443
 444   typedef expr::NodeSelfIterator internal_iterator;
 445
 446   internal_iterator internalBegin() const {
 447     if(singleton()){
 448       return expr::NodeSelfIterator::self(getNode());
 449     }else{
 450       return getNode().begin();
 451     }
 452   }
 453
 454   internal_iterator internalEnd() const {
 455     if(singleton()){
 456       return expr::NodeSelfIterator::selfEnd(getNode());
 457     }else{
 458       return getNode().end();
 459     }
 460   }
 461
 462 public:
 463
 464   class iterator {
 465   private:
 466     internal_iterator d_iter;
 467
 468   public:
 469     explicit iterator(internal_iterator i) : d_iter(i) {}
 470
 471     inline Variable operator*() {
 472       return Variable(*d_iter);
 473     }
 474
 475     bool operator==(const iterator& i) {
 476       return d_iter == i.d_iter;
 477     }
 478
 479     bool operator!=(const iterator& i) {
 480       return d_iter != i.d_iter;
 481     }
 482
 483     iterator operator++() {
 484       ++d_iter;
 485       return *this;
 486     }
 487
 488     iterator operator++(int) {
 489       return iterator(d_iter++);
 490     }
 491   };
 492
 493   iterator begin() const {
 494     return iterator(internalBegin());
 495   }
 496
 497   iterator end() const {
 498     return iterator(internalEnd());
 499   }
 500
 501   Variable getHead() const {
 502     Assert(!empty());
 503     return *(begin());
 504   }
 505
 506   VarList(Variable v) : NodeWrapper(v.getNode()) {
 507     Assert(isSorted(begin(), end()));
 508   }
 509
 510   VarList(const std::vector<Variable>& l) : NodeWrapper(multList(l)) {
 511     Assert(l.size() >= 2);
 512     Assert(isSorted(begin(), end()));
 513   }
 514
 515   static bool isMember(Node n);
 516
 517   bool isNormalForm() const {
 518     return !empty();
 519   }
 520
 521   static VarList mkEmptyVarList() {
 522     return VarList();
 523   }
 524
 525
 526   /** There are no restrictions on the size of l */
 527   static VarList mkVarList(const std::vector<Variable>& l) {
 528     if(l.size() == 0) {
 529       return mkEmptyVarList();
 530     } else if(l.size() == 1) {
 531       return VarList((*l.begin()).getNode());
 532     } else {
 533       return VarList(l);
 534     }
 535   }
 536
 537   bool empty() const { return getNode().isNull(); }
 538   bool singleton() const {
 539     return !empty() && getNode().getKind() != kind::MULT;
 540   }
 541
 542   int size() const {
 543     if(singleton())
 544       return 1;
 545     else
 546       return getNode().getNumChildren();
 547   }
 548
 549   static VarList parseVarList(Node n);
 550
 551   VarList operator*(const VarList& vl) const;
 552
 553   int cmp(const VarList& vl) const;
 554
 555   bool operator<(const VarList& vl) const { return cmp(vl) < 0; }
 556
 557   bool operator==(const VarList& vl) const { return cmp(vl) == 0; }
 558
 559   bool isIntegral() const {
 560     for(iterator i = begin(), e=end(); i != e; ++i ){
 561       Variable var = *i;
 562       if(!var.isIntegral()){
 563         return false;
 564       }
 565     }
 566     return true;
 567   }
 568   size_t getComplexity() const;
 569
 570 private:
 571   bool isSorted(iterator start, iterator end);
 572
 573 };/* class VarList */
 574
 575
 576 class Monomial : public NodeWrapper {
 577 private:
 578   Constant constant;
 579   VarList varList;
 580   Monomial(Node n, const Constant& c, const VarList& vl):
 581     NodeWrapper(n), constant(c), varList(vl)
 582   {
 583     Assert(!c.isZero() ||  vl.empty() );
 584     Assert( c.isZero() || !vl.empty() );
 585
 586     Assert(!c.isOne() || !multStructured(n));
 587   }
 588
 589   static Node makeMultNode(const Constant& c, const VarList& vl) {
 590     Assert(!c.isZero());
 591     Assert(!c.isOne());
 592     Assert(!vl.empty());
 593     return NodeManager::currentNM()->mkNode(kind::MULT, c.getNode(), vl.getNode());
 594   }
 595
 596   static bool multStructured(Node n) {
 597     return n.getKind() ==  kind::MULT &&
 598       n[0].getKind() == kind::CONST_RATIONAL &&
 599       n.getNumChildren() == 2;
 600   }
 601
 602 public:
 603
 604   Monomial(const Constant& c):
 605     NodeWrapper(c.getNode()), constant(c), varList(VarList::mkEmptyVarList())
 606   { }
 607
 608   Monomial(const VarList& vl):
 609     NodeWrapper(vl.getNode()), constant(Constant::mkConstant(1)), varList(vl)
 610   {
 611     Assert( !varList.empty() );
 612   }
 613
 614   Monomial(const Constant& c, const VarList& vl):
 615     NodeWrapper(makeMultNode(c,vl)), constant(c), varList(vl)
 616   {
 617     Assert( !c.isZero() );
 618     Assert( !c.isOne() );
 619     Assert( !varList.empty() );
 620
 621     Assert(multStructured(getNode()));
 622   }
 623
 624   static bool isMember(TNode n);
 625
 626   /** Makes a monomial with no restrictions on c and vl. */
 627   static Monomial mkMonomial(const Constant& c, const VarList& vl);
 628
 629   static Monomial mkMonomial(const Variable& v){
 630     return Monomial(VarList(v));
 631   }
 632
 633   static Monomial parseMonomial(Node n);
 634
 635   static Monomial mkZero() {
 636     return Monomial(Constant::mkConstant(0));
 637   }
 638   static Monomial mkOne() {
 639     return Monomial(Constant::mkConstant(1));
 640   }
 641   const Constant& getConstant() const { return constant; }
 642   const VarList& getVarList() const { return varList; }
 643
 644   bool isConstant() const {
 645     return varList.empty();
 646   }
 647
 648   bool isZero() const {
 649     return constant.isZero();
 650   }
 651
 652   bool coefficientIsOne() const {
 653     return constant.isOne();
 654   }
 655
 656   bool absCoefficientIsOne() const {
 657     return coefficientIsOne() || constant.getValue() == -1;
 658   }
 659
 660   bool constantIsPositive() const {
 661     return getConstant().isPositive();
 662   }
 663
 664   Monomial operator*(const Rational& q) const;
 665   Monomial operator*(const Constant& c) const;
 666   Monomial operator*(const Monomial& mono) const;
 667
 668   Monomial operator-() const{
 669     return (*this) * Rational(-1);
 670   }
 671
 672
 673   int cmp(const Monomial& mono) const {
 674     return getVarList().cmp(mono.getVarList());
 675   }
 676
 677   bool operator<(const Monomial& vl) const {
 678     return cmp(vl) < 0;
 679   }
 680
 681   bool operator==(const Monomial& vl) const {
 682     return cmp(vl) == 0;
 683   }
 684
 685   static bool isSorted(const std::vector<Monomial>& m) {
 686     return __gnu_cxx::is_sorted(m.begin(), m.end());
 687   }
 688
 689   static bool isStrictlySorted(const std::vector<Monomial>& m) {
 690     return isSorted(m) && std::adjacent_find(m.begin(),m.end()) == m.end();
 691   }
 692
 693   static void sort(std::vector<Monomial>& m);
 694   static void combineAdjacentMonomials(std::vector<Monomial>& m);
 695
 696   /**
 697    * The variable product
 698    */
 699   bool integralVariables() const {
 700     return getVarList().isIntegral();
 701   }
 702
 703   /**
 704    * The coefficient of the monomial is integral.
 705    */
 706   bool integralCoefficient() const {
 707     return getConstant().isIntegral();
 708   }
 709
 710   /**
 711    * A Monomial is an "integral" monomial if the constant is integral.
 712    */
 713   bool isIntegral() const {
 714     return integralCoefficient() && integralVariables();
 715   }
 716
 717   /** Returns true if the VarList is a product of at least 2 Variables.*/
 718   bool isNonlinear() const {
 719     return getVarList().size() >= 2;
 720   }
 721
 722   /**
 723    * Given a sorted list of monomials, this function transforms this
 724    * into a strictly sorted list of monomials that does not contain zero.
 725    */
 726   //static std::vector<Monomial> sumLikeTerms(const std::vector<Monomial>& monos);
 727
 728   int absCmp(const Monomial& other) const{
 729     return getConstant().getValue().absCmp(other.getConstant().getValue());
 730   }
 731   // bool absLessThan(const Monomial& other) const{
 732   //   return getConstant().abs() < other.getConstant().abs();
 733   // }
 734
 735   uint32_t coefficientLength() const{
 736     return getConstant().length();
 737   }
 738
 739   void print() const;
 740   static void printList(const std::vector<Monomial>& list);
 741
 742   size_t getComplexity() const;
 743 };/* class Monomial */
 744
 745 class SumPair;
 746 class Comparison;;
 747
 748 class Polynomial : public NodeWrapper {
 749 private:
 750   bool d_singleton;
 751
 752   Polynomial(TNode n) : NodeWrapper(n), d_singleton(Monomial::isMember(n)) {
 753     Assert(isMember(getNode()));
 754   }
 755
 756   static Node makePlusNode(const std::vector<Monomial>& m) {
 757     Assert(m.size() >= 2);
 758
 759     return makeNode(kind::PLUS, m.begin(), m.end());
 760   }
 761
 762   typedef expr::NodeSelfIterator internal_iterator;
 763
 764   internal_iterator internalBegin() const {
 765     if(singleton()){
 766       return expr::NodeSelfIterator::self(getNode());
 767     }else{
 768       return getNode().begin();
 769     }
 770   }
 771
 772   internal_iterator internalEnd() const {
 773     if(singleton()){
 774       return expr::NodeSelfIterator::selfEnd(getNode());
 775     }else{
 776       return getNode().end();
 777     }
 778   }
 779
 780   bool singleton() const { return d_singleton; }
 781
 782 public:
 783   static bool isMember(TNode n) {
 784     if(Monomial::isMember(n)){
 785       return true;
 786     }else if(n.getKind() == kind::PLUS){
 787       Assert(n.getNumChildren() >= 2);
 788       Node::iterator currIter = n.begin(), end = n.end();
 789       Node prev = *currIter;
 790       if(!Monomial::isMember(prev)){
 791         return false;
 792       }
 793
 794       Monomial mprev = Monomial::parseMonomial(prev);
 795       ++currIter;
 796       for(; currIter != end; ++currIter){
 797         Node curr = *currIter;
 798         if(!Monomial::isMember(curr)){
 799           return false;
 800         }
 801         Monomial mcurr = Monomial::parseMonomial(curr);
 802         if(!(mprev < mcurr)){
 803           return false;
 804         }
 805         mprev = mcurr;
 806       }
 807       return true;
 808     } else {
 809       return false;
 810     }
 811   }
 812
 813   class iterator {
 814   private:
 815     internal_iterator d_iter;
 816
 817   public:
 818     explicit iterator(internal_iterator i) : d_iter(i) {}
 819
 820     inline Monomial operator*() {
 821       return Monomial::parseMonomial(*d_iter);
 822     }
 823
 824     bool operator==(const iterator& i) {
 825       return d_iter == i.d_iter;
 826     }
 827
 828     bool operator!=(const iterator& i) {
 829       return d_iter != i.d_iter;
 830     }
 831
 832     iterator operator++() {
 833       ++d_iter;
 834       return *this;
 835     }
 836
 837     iterator operator++(int) {
 838       return iterator(d_iter++);
 839     }
 840   };
 841
 842   iterator begin() const { return iterator(internalBegin()); }
 843   iterator end() const {  return iterator(internalEnd()); }
 844
 845   Polynomial(const Monomial& m):
 846     NodeWrapper(m.getNode()), d_singleton(true)
 847   {}
 848
 849   Polynomial(const std::vector<Monomial>& m):
 850     NodeWrapper(makePlusNode(m)), d_singleton(false)
 851   {
 852     Assert( m.size() >= 2);
 853     Assert( Monomial::isStrictlySorted(m) );
 854   }
 855
 856   static Polynomial mkPolynomial(const Variable& v){
 857     return Monomial::mkMonomial(v);
 858   }
 859
 860   static Polynomial mkPolynomial(const std::vector<Monomial>& m) {
 861     if(m.size() == 0) {
 862       return Polynomial(Monomial::mkZero());
 863     } else if(m.size() == 1) {
 864       return Polynomial((*m.begin()));
 865     } else {
 866       return Polynomial(m);
 867     }
 868   }
 869
 870   static Polynomial parsePolynomial(Node n) {
 871     return Polynomial(n);
 872   }
 873
 874   static Polynomial mkZero() {
 875     return Polynomial(Monomial::mkZero());
 876   }
 877   static Polynomial mkOne() {
 878     return Polynomial(Monomial::mkOne());
 879   }
 880   bool isZero() const {
 881     return singleton() && (getHead().isZero());
 882   }
 883
 884   bool isConstant() const {
 885     return singleton() && (getHead().isConstant());
 886   }
 887
 888   bool containsConstant() const {
 889     return getHead().isConstant();
 890   }
 891
 892   uint32_t size() const{
 893     if(singleton()){
 894       return 1;
 895     }else{
 896       Assert(getNode().getKind() == kind::PLUS);
 897       return getNode().getNumChildren();
 898     }
 899   }
 900
 901   Monomial getHead() const {
 902     return *(begin());
 903   }
 904
 905   Polynomial getTail() const {
 906     Assert(! singleton());
 907
 908     iterator tailStart = begin();
 909     ++tailStart;
 910     std::vector<Monomial> subrange;
 911     copy_range(tailStart, end(), subrange);
 912     return mkPolynomial(subrange);
 913   }
 914
 915   Monomial minimumVariableMonomial() const;
 916   bool variableMonomialAreStrictlyGreater(const Monomial& m) const;
 917
 918   void printList() const {
 919     if(Debug.isOn("normal-form")){
 920       Debug("normal-form") << "start list" << std::endl;
 921       for(iterator i = begin(), oend = end(); i != oend; ++i) {
 922         const Monomial& m =*i;
 923         m.print();
 924       }
 925       Debug("normal-form") << "end list" << std::endl;
 926     }
 927   }
 928
 929   /** A Polynomial is an "integral" polynomial if all of the monomials are integral. */
 930   bool allIntegralVariables() const {
 931     for(iterator i = begin(), e=end(); i!=e; ++i){
 932       if(!(*i).integralVariables()){
 933         return false;
 934       }
 935     }
 936     return true;
 937   }
 938
 939   /**
 940    * A Polynomial is an "integral" polynomial if all of the monomials are integral
 941    * and all of the coefficients are Integral. */
 942   bool isIntegral() const {
 943     for(iterator i = begin(), e=end(); i!=e; ++i){
 944       if(!(*i).isIntegral()){
 945         return false;
 946       }
 947     }
 948     return true;
 949   }
 950
 951   static Polynomial sumPolynomials(const std::vector<Polynomial>& polynomials);
 952
 953   /** Returns true if the polynomial contains a non-linear monomial.*/
 954   bool isNonlinear() const;
 955
 956
 957   /**
 958    * Selects a minimal monomial in the polynomial by the absolute value of
 959    * the coefficient.
 960    */
 961   Monomial selectAbsMinimum() const;
 962
 963   /** Returns true if the absolute value of the head coefficient is one. */
 964   bool leadingCoefficientIsAbsOne() const;
 965   bool leadingCoefficientIsPositive() const;
 966   bool denominatorLCMIsOne() const;
 967   bool numeratorGCDIsOne() const;
 968
 969   bool signNormalizedReducedSum() const {
 970     return leadingCoefficientIsPositive() && denominatorLCMIsOne() && numeratorGCDIsOne();
 971   }
 972
 973   /**
 974    * Returns the Least Common Multiple of the denominators of the coefficients
 975    * of the monomials.
 976    */
 977   Integer denominatorLCM() const;
 978
 979   /**
 980    * Returns the GCD of the numerators of the monomials.
 981    * Requires this to be an isIntegral() polynomial.
 982    */
 983   Integer numeratorGCD() const;
 984
 985   /**
 986    * Returns the GCD of the coefficients of the monomials.
 987    * Requires this to be an isIntegral() polynomial.
 988    */
 989   Integer gcd() const;
 990
 991   Polynomial exactDivide(const Integer& z) const {
 992     Assert(isIntegral());
 993     Constant invz = Constant::mkConstant(Rational(1,z));
 994     Polynomial prod = (*this) * Monomial(invz);
 995     Assert(prod.isIntegral());
 996     return prod;
 997   }
 998
 999   Polynomial operator+(const Polynomial& vl) const;
1000   Polynomial operator-(const Polynomial& vl) const;
1001   Polynomial operator-() const{
1002     return (*this) * Rational(-1);
1003   }
1004
1005   Polynomial operator*(const Rational& q) const;
1006   Polynomial operator*(const Constant& c) const;
1007   Polynomial operator*(const Monomial& mono) const;
1008
1009   Polynomial operator*(const Polynomial& poly) const;
1010
1011   /**
1012    * Viewing the integer polynomial as a list [(* coeff_i mono_i)]
1013    * The quotient and remainder of p divided by the non-zero integer z is:
1014    *   q := [(* floor(coeff_i/z) mono_i )]
1015    *   r := [(* rem(coeff_i/z) mono_i)]
1016    * computeQR(p,z) returns the node (+ q r).
1017    *
1018    * q and r are members of the Polynomial class.
1019    * For example:
1020    * computeQR( p = (+ 5 (* 3 x) (* 8 y)) , z = 2) returns
1021    *   (+ (+ 2 x (* 4 y)) (+ 1 x))
1022    */
1023   static Node computeQR(const Polynomial& p, const Integer& z);
1024
1025   /** Returns the coefficient associated with the VarList in the polynomial. */
1026   Constant getCoefficient(const VarList& vl) const;
1027
1028   uint32_t maxLength() const{
1029     iterator i = begin(), e=end();
1030     if( i == e){
1031       return 1;
1032     }else{
1033       uint32_t max = (*i).coefficientLength();
1034       ++i;
1035       for(; i!=e; ++i){
1036         uint32_t curr = (*i).coefficientLength();
1037         if(curr > max){
1038           max = curr;
1039         }
1040       }
1041       return max;
1042     }
1043   }
1044
1045   uint32_t numMonomials() const {
1046     if( getNode().getKind() == kind::PLUS ){
1047       return getNode().getNumChildren();
1048     }else if(isZero()){
1049       return 0;
1050     }else{
1051       return 1;
1052     }
1053   }
1054
1055   const Rational& asConstant() const{
1056     Assert(isConstant());
1057     return getNode().getConst<Rational>();
1058     //return getHead().getConstant().getValue();
1059   }
1060
1061   bool isVarList() const {
1062     if(singleton()){
1063       return VarList::isMember(getNode());
1064     }else{
1065       return false;
1066     }
1067   }
1068
1069   VarList asVarList() const {
1070     Assert(isVarList());
1071     return getHead().getVarList();
1072   }
1073
1074   size_t getComplexity() const;
1075
1076   friend class SumPair;
1077   friend class Comparison;
1078
1079   /** Returns a node that if asserted ensures v is the abs of this polynomial.*/
1080   Node makeAbsCondition(Variable v){
1081     return makeAbsCondition(v, *this);
1082   }
1083
1084   /** Returns a node that if asserted ensures v is the abs of p.*/
1085   static Node makeAbsCondition(Variable v, Polynomial p);
1086
1087 };/* class Polynomial */
1088
1089
1090 /**
1091  * SumPair is a utility class that extends polynomials for use in computations.
1092  * A SumPair is always a combination of (+ p c) where
1093  *  c is a constant and p is a polynomial such that p = 0 or !p.containsConstant().
1094  *
1095  * These are a useful utility for representing the equation p = c as (+ p -c) where the pair
1096  * is known to implicitly be equal to 0.
1097  *
1098  * SumPairs do not have unique representations due to the potential for p = 0.
1099  * This makes them inappropriate for normal forms.
1100  */
1101 class SumPair : public NodeWrapper {
1102 private:
1103   static Node toNode(const Polynomial& p, const Constant& c){
1104     return NodeManager::currentNM()->mkNode(kind::PLUS, p.getNode(), c.getNode());
1105   }
1106
1107   SumPair(TNode n) :
1108     NodeWrapper(n)
1109   {
1110     Assert(isNormalForm());
1111   }
1112
1113 public:
1114
1115   SumPair(const Polynomial& p):
1116     NodeWrapper(toNode(p, Constant::mkConstant(0)))
1117   {
1118     Assert(isNormalForm());
1119   }
1120
1121   SumPair(const Polynomial& p, const Constant& c):
1122     NodeWrapper(toNode(p, c))
1123   {
1124     Assert(isNormalForm());
1125   }
1126
1127   static bool isMember(TNode n) {
1128     if(n.getKind() == kind::PLUS && n.getNumChildren() == 2){
1129       if(Constant::isMember(n[1])){
1130         if(Polynomial::isMember(n[0])){
1131           Polynomial p = Polynomial::parsePolynomial(n[0]);
1132           return p.isZero() || (!p.containsConstant());
1133         }else{
1134           return false;
1135         }
1136       }else{
1137         return false;
1138       }
1139     }else{
1140       return false;
1141     }
1142   }
1143
1144   bool isNormalForm() const {
1145     return isMember(getNode());
1146   }
1147
1148   Polynomial getPolynomial() const {
1149     return Polynomial::parsePolynomial(getNode()[0]);
1150   }
1151
1152   Constant getConstant() const {
1153     return Constant::mkConstant((getNode())[1]);
1154   }
1155
1156   SumPair operator+(const SumPair& other) const {
1157     return SumPair(getPolynomial() + other.getPolynomial(),
1158                    getConstant() + other.getConstant());
1159   }
1160
1161   SumPair operator*(const Constant& c) const {
1162     return SumPair(getPolynomial() * c, getConstant() * c);
1163   }
1164
1165   SumPair operator-(const SumPair& other) const {
1166     return (*this) + (other * Constant::mkConstant(-1));
1167   }
1168
1169   static SumPair mkSumPair(const Polynomial& p);
1170
1171   static SumPair mkSumPair(const Variable& var){
1172     return SumPair(Polynomial::mkPolynomial(var));
1173   }
1174
1175   static SumPair parseSumPair(TNode n){
1176     return SumPair(n);
1177   }
1178
1179   bool isIntegral() const{
1180     return getConstant().isIntegral() && getPolynomial().isIntegral();
1181   }
1182
1183   bool isConstant() const {
1184     return getPolynomial().isZero();
1185   }
1186
1187   bool isZero() const {
1188     return getConstant().isZero() && isConstant();
1189   }
1190
1191   uint32_t size() const{
1192     return getPolynomial().size();
1193   }
1194
1195   bool isNonlinear() const{
1196     return getPolynomial().isNonlinear();
1197   }
1198
1199   /**
1200    * Returns the greatest common divisor of gcd(getPolynomial()) and getConstant().
1201    * The SumPair must be integral.
1202    */
1203   Integer gcd() const {
1204     Assert(isIntegral());
1205     return (getPolynomial().gcd()).gcd(getConstant().getValue().getNumerator());
1206   }
1207
1208   uint32_t maxLength() const {
1209     Assert(isIntegral());
1210     return std::max(getPolynomial().maxLength(), getConstant().length());
1211   }
1212
1213   static SumPair mkZero() {
1214     return SumPair(Polynomial::mkZero(), Constant::mkConstant(0));
1215   }
1216
1217   static Node computeQR(const SumPair& sp, const Integer& div);
1218
1219 };/* class SumPair */
1220
1221 /* class OrderedPolynomialPair { */
1222 /* private: */
1223 /*   Polynomial d_first; */
1224 /*   Polynomial d_second; */
1225 /* public: */
1226 /*   OrderedPolynomialPair(const Polynomial& f, const Polynomial& s) */
1227 /*     : d_first(f), */
1228 /*       d_second(s) */
1229 /*   {} */
1230
1231 /*   /\** Returns the first part of the pair. *\/ */
1232 /*   const Polynomial& getFirst() const { */
1233 /*     return d_first; */
1234 /*   } */
1235
1236 /*   /\** Returns the second part of the pair. *\/ */
1237 /*   const Polynomial& getSecond() const { */
1238 /*     return d_second; */
1239 /*   } */
1240
1241 /*   OrderedPolynomialPair operator*(const Constant& c) const; */
1242 /*   OrderedPolynomialPair operator+(const Polynomial& p) const; */
1243
1244 /*   /\** Returns true if both of the polynomials are constant. *\/ */
1245 /*   bool isConstant() const; */
1246
1247 /*   /\** */
1248 /*    * Evaluates an isConstant() ordered pair as if */
1249 /*    *   (k getFirst() getRight()) */
1250 /*    *\/ */
1251 /*   bool evaluateConstant(Kind k) const; */
1252
1253 /*   /\** */
1254 /*    * Returns the Least Common Multiple of the monomials */
1255 /*    * on the lefthand side and the constant on the right. */
1256 /*    *\/ */
1257 /*   Integer denominatorLCM() const; */
1258
1259 /*   /\** Constructs a SumPair. *\/ */
1260 /*   SumPair toSumPair() const; */
1261
1262
1263 /*   OrderedPolynomialPair divideByGCD() const; */
1264 /*   OrderedPolynomialPair multiplyConstant(const Constant& c) const; */
1265
1266 /*   /\** */
1267 /*    * Returns true if all of the variables are integers, */
1268 /*    * and the coefficients are integers. */
1269 /*    *\/ */
1270 /*   bool isIntegral() const; */
1271
1272 /*   /\** Returns true if all of the variables are integers. *\/ */
1273 /*   bool allIntegralVariables() const { */
1274 /*     return getFirst().allIntegralVariables() && getSecond().allIntegralVariables(); */
1275 /*   } */
1276 /* }; */
1277
1278 class Comparison : public NodeWrapper {
1279 private:
1280
1281   static Node toNode(Kind k, const Polynomial& l, const Constant& c);
1282   static Node toNode(Kind k, const Polynomial& l, const Polynomial& r);
1283
1284   Comparison(TNode n);
1285
1286   /**
1287    * Creates a node in normal form equivalent to (= l 0).
1288    * All variables in l are integral.
1289    */
1290   static Node mkIntEquality(const Polynomial& l);
1291
1292   /**
1293    * Creates a comparison equivalent to (k l 0).
1294    * k is either GT or GEQ.
1295    * All variables in l are integral.
1296    */
1297   static Node mkIntInequality(Kind k, const Polynomial& l);
1298
1299   /**
1300    * Creates a node equivalent to (= l 0).
1301    * It is not the case that all variables in l are integral.
1302    */
1303   static Node mkRatEquality(const Polynomial& l);
1304
1305   /**
1306    * Creates a comparison equivalent to (k l 0).
1307    * k is either GT or GEQ.
1308    * It is not the case that all variables in l are integral.
1309    */
1310   static Node mkRatInequality(Kind k, const Polynomial& l);
1311
1312 public:
1313
1314   Comparison(bool val) :
1315     NodeWrapper(NodeManager::currentNM()->mkConst(val))
1316   { }
1317
1318   /**
1319    * Given a literal to TheoryArith return a single kind to
1320    * to indicate its underlying structure.
1321    * The function returns the following in each case:
1322    * - (K left right)           -> K where is either EQUAL, GT, or GEQ
1323    * - (CONST_BOOLEAN b)        -> CONST_BOOLEAN
1324    * - (NOT (EQUAL left right)) -> DISTINCT
1325    * - (NOT (GT left right))    -> LEQ
1326    * - (NOT (GEQ left right))   -> LT
1327    * If none of these match, it returns UNDEFINED_KIND.
1328    */
1329   static Kind comparisonKind(TNode literal);
1330
1331   Kind comparisonKind() const { return comparisonKind(getNode()); }
1332
1333   static Comparison mkComparison(Kind k, const Polynomial& l, const Polynomial& r);
1334
1335   /** Returns true if the comparison is a boolean constant. */
1336   bool isBoolean() const;
1337
1338   /**
1339    * Returns true if the comparison is either a boolean term,
1340    * in integer normal form or mixed normal form.
1341    */
1342   bool isNormalForm() const;
1343
1344 private:
1345   bool isNormalGT() const;
1346   bool isNormalGEQ() const;
1347
1348   bool isNormalLT() const;
1349   bool isNormalLEQ() const;
1350
1351   bool isNormalEquality() const;
1352   bool isNormalDistinct() const;
1353   bool isNormalEqualityOrDisequality() const;
1354
1355   bool allIntegralVariables() const {
1356     return getLeft().allIntegralVariables() && getRight().allIntegralVariables();
1357   }
1358   bool rightIsConstant() const;
1359
1360 public:
1361   Polynomial getLeft() const;
1362   Polynomial getRight() const;
1363
1364   /* /\** Normal form check if at least one variable is real. *\/ */
1365   /* bool isMixedCompareNormalForm() const; */
1366
1367   /* /\** Normal form check if at least one variable is real. *\/ */
1368   /* bool isMixedEqualsNormalForm() const; */
1369
1370   /* /\** Normal form check is all variables are integer.*\/ */
1371   /* bool isIntegerCompareNormalForm() const; */
1372
1373   /* /\** Normal form check is all variables are integer.*\/ */
1374   /* bool isIntegerEqualsNormalForm() const; */
1375
1376
1377   /**
1378    * Returns true if all of the variables are integers, the coefficients are integers,
1379    * and the right hand coefficient is an integer.
1380    */
1381   bool debugIsIntegral() const;
1382
1383   static Comparison parseNormalForm(TNode n);
1384
1385   inline static bool isNormalAtom(TNode n){
1386     Comparison parse = Comparison::parseNormalForm(n);
1387     return parse.isNormalForm();
1388   }
1389
1390   size_t getComplexity() const;
1391
1392   SumPair toSumPair() const;
1393
1394   Polynomial normalizedVariablePart() const;
1395   DeltaRational normalizedDeltaRational() const;
1396
1397 };/* class Comparison */
1398
1399 }/* CVC4::theory::arith namespace */
1400 }/* CVC4::theory namespace */
1401 }/* CVC4 namespace */
1402
1403 #endif /* __CVC4__THEORY__ARITH__NORMAL_FORM_H */