src/theory/arith/normal_form.h

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