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