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