src/theory/arith/normal_form.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Tim King, Morgan Deters, Gereon Kremer
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 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.
  11  * ****************************************************************************
  12  *
  13  * [[ Add one-line brief description here ]]
  14  *
  15  * [[ Add lengthier description here ]]
  16  * \todo document this file
  17  */
  18
  19 #include "cvc5_private.h"
  20
  21 #ifndef CVC5__THEORY__ARITH__NORMAL_FORM_H
  22 #define CVC5__THEORY__ARITH__NORMAL_FORM_H
  23
  24 #include <algorithm>
  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 namespace cvc5 {
  33 namespace theory {
  34 namespace arith {
  35
  36 /***********************************************/
  37 /***************** Normal Form *****************/
  38 /***********************************************/
  39 /***********************************************/
  40
  41 /**
  42  * Section 1: Languages
  43  * The normal form for arithmetic nodes is defined by the language
  44  * accepted by the following BNFs with some guard conditions.
  45  * (The guard conditions are in Section 3 for completeness.)
  46  *
  47  * variable := n
  48  *   where
  49  *     n.isVar() or is foreign
  50  *     n.getType() \in {Integer, Real}
  51  *
  52  * constant := n
  53  *   where
  54  *     n.getKind() == kind::CONST_RATIONAL
  55  *
  56  * var_list := variable | (* [variable])
  57  *   where
  58  *     len [variable] >= 2
  59  *     isSorted varOrder [variable]
  60  *
  61  * monomial := constant | var_list | (* constant' var_list')
  62  *   where
  63  *     \f$ constant' \not\in {0,1} \f$
  64  *
  65  * polynomial := monomial' | (+ [monomial])
  66  *   where
  67  *     len [monomial] >= 2
  68  *     isStrictlySorted monoOrder [monomial]
  69  *     forall (\x -> x != 0) [monomial]
  70  *
  71  * rational_cmp := (|><| qpolynomial constant)
  72  *   where
  73  *     |><| is GEQ, or GT
  74  *     not (exists constantMonomial (monomialList qpolynomial))
  75  *     (exists realMonomial (monomialList qpolynomial))
  76  *     abs(monomialCoefficient (head (monomialList qpolynomial))) == 1
  77  *
  78  * integer_cmp := (>= zpolynomial constant)
  79  *   where
  80  *     not (exists constantMonomial (monomialList zpolynomial))
  81  *     (forall integerMonomial (monomialList zpolynomial))
  82  *     the gcd of all numerators of coefficients is 1
  83  *     the denominator of all coefficients and the constant is 1
  84  *     the leading coefficient is positive
  85  *
  86  * rational_eq := (= qvarlist qpolynomial)
  87  *   where
  88  *     let allMonomials = (cons qvarlist (monomialList zpolynomial))
  89  *     let variableMonomials = (drop constantMonomial allMonomials)
  90  *     isStrictlySorted variableMonomials
  91  *     exists realMonomial variableMonomials
  92  *     is not empty qvarlist
  93  *
  94  * integer_eq := (= zmonomial zpolynomial)
  95  *   where
  96  *     let allMonomials = (cons zmonomial (monomialList zpolynomial))
  97  *     let variableMonomials = (drop constantMonomial allMonomials)
  98  *     not (constantMonomial zmonomial)
  99  *     (forall integerMonomial allMonomials)
 100  *     isStrictlySorted variableMonomials
 101  *     the gcd of all numerators of coefficients is 1
 102  *     the denominator of all coefficients and the constant is 1
 103  *     the coefficient of monomial is positive
 104  *     the value of the coefficient of monomial is minimal in variableMonomials
 105  *
 106  * comparison := TRUE | FALSE
 107  *   | rational_cmp | (not rational_cmp)
 108  *   | rational_eq | (not rational_eq)
 109  *   | integer_cmp | (not integer_cmp)
 110  *   | integer_eq | (not integer_eq)
 111  *
 112  * Normal Form for terms := polynomial
 113  * Normal Form for atoms := comparison
 114  */
 115
 116 /**
 117  * Section 2: Helper Classes
 118  * The langauges accepted by each of these defintions
 119  * roughly corresponds to one of the following helper classes:
 120  *  Variable
 121  *  Constant
 122  *  VarList
 123  *  Monomial
 124  *  Polynomial
 125  *  Comparison
 126  *
 127  * Each of the classes obeys the following contracts/design decisions:
 128  * -Calling isMember(Node node) on a node returns true iff that node is a
 129  *  a member of the language. Note: isMember is O(n).
 130  * -Calling isNormalForm() on a helper class object returns true iff that
 131  *  helper class currently represents a normal form object.
 132  * -If isNormalForm() is false, then this object must have been made
 133  *  using a mk*() factory function.
 134  * -If isNormalForm() is true, calling getNode() on all of these classes
 135  *  returns a node that would be accepted by the corresponding language.
 136  *  And if isNormalForm() is false, returns Node::null().
 137  * -Each of the classes is immutable.
 138  * -Public facing constuctors have a 1-to-1 correspondence with one of
 139  *  production rules in the above grammar.
 140  * -Public facing constuctors are required to fail in debug mode when the
 141  *  guards of the production rule are not strictly met.
 142  *  For example: Monomial(Constant(1),VarList(Variable(x))) must fail.
 143  * -When a class has a Class parseClass(Node node) function,
 144  *  if isMember(node) is true, the function is required to return an instance
 145  *  of the helper class, instance, s.t. instance.getNode() == node.
 146  *  And if isMember(node) is false, this throws an assertion failure in debug
 147  *  mode and has undefined behaviour if not in debug mode.
 148  * -Only public facing constructors, parseClass(node), and mk*() functions are
 149  *  considered privileged functions for the helper class.
 150  * -Only privileged functions may use private constructors, and access
 151  *  private data members.
 152  * -All non-privileged functions are considered utility functions and
 153  *  must use a privileged function in order to create an instance of the class.
 154  */
 155
 156 /**
 157  * Section 3: Guard Conditions Misc.
 158  *
 159  *
 160  *  variable_order x y =
 161  *    if (meta_kind_variable x) and (meta_kind_variable y)
 162  *    then node_order x y
 163  *    else if (meta_kind_variable x)
 164  *    then false
 165  *    else if (meta_kind_variable y)
 166  *    then true
 167  *    else node_order x y
 168  *
 169  *  var_list_len vl =
 170  *    match vl with
 171  *       variable -> 1
 172  *     | (* [variable]) -> len [variable]
 173  *
 174  *  order res =
 175  *    match res with
 176  *       Empty -> (0,Node::null())
 177  *     | NonEmpty(vl) -> (var_list_len vl, vl)
 178  *
 179  *  var_listOrder a b = tuple_cmp (order a) (order b)
 180  *
 181  *  monomialVarList monomial =
 182  *    match monomial with
 183  *        constant -> Empty
 184  *      | var_list -> NonEmpty(var_list)
 185  *      | (* constant' var_list') -> NonEmpty(var_list')
 186  *
 187  *  monoOrder m0 m1 = var_listOrder (monomialVarList m0) (monomialVarList m1)
 188  *
 189  *  integerMonomial mono =
 190  *    forall varHasTypeInteger (monomialVarList mono)
 191  *
 192  *  realMonomial mono = not (integerMonomial mono)
 193  *
 194  *  constantMonomial monomial =
 195  *    match monomial with
 196  *        constant -> true
 197  *      | var_list -> false
 198  *      | (* constant' var_list') -> false
 199  *
 200  *  monomialCoefficient monomial =
 201  *    match monomial with
 202  *        constant -> constant
 203  *      | var_list -> Constant(1)
 204  *      | (* constant' var_list') -> constant'
 205  *
 206  *  monomialList polynomial =
 207  *    match polynomial with
 208  *        monomial -> monomial::[]
 209  *      | (+ [monomial]) -> [monomial]
 210  */
 211
 212 /**
 213  * A NodeWrapper is a class that is a thinly veiled container of a Node object.
 214  */
 215 class NodeWrapper {
 216 private:
 217   Node node;
 218 public:
 219   NodeWrapper(Node n) : node(n) {}
 220   const Node& getNode() const { return node; }
 221 };/* class NodeWrapper */
 222
 223
 224 class Variable : public NodeWrapper {
 225 public:
 226  Variable(Node n) : NodeWrapper(n) { Assert(isMember(getNode())); }
 227
 228  // TODO: check if it's a theory leaf also
 229  static bool isMember(Node n)
 230  {
 231    Kind k = n.getKind();
 232    switch (k)
 233    {
 234      case kind::CONST_RATIONAL: return false;
 235      case kind::INTS_DIVISION:
 236      case kind::INTS_MODULUS:
 237      case kind::DIVISION:
 238      case kind::INTS_DIVISION_TOTAL:
 239      case kind::INTS_MODULUS_TOTAL:
 240      case kind::DIVISION_TOTAL: return isDivMember(n);
 241      case kind::IAND: return isIAndMember(n);
 242      case kind::POW2: return isPow2Member(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 isPow2Member(Node n);
 270   static bool isDivMember(Node n);
 271   bool isDivLike() const{
 272     return isDivMember(getNode());
 273   }
 274   static bool isTranscendentalMember(Node n);
 275
 276   bool isNormalForm() { return isMember(getNode()); }
 277
 278   bool isIntegral() const {
 279     return getNode().getType().isInteger();
 280   }
 281
 282   bool isMetaKindVariable() const {
 283     return getNode().isVar();
 284   }
 285
 286   bool operator<(const Variable& v) const {
 287     VariableNodeCmp cmp;
 288     return cmp(this->getNode(), v.getNode());
 289   }
 290
 291   struct VariableNodeCmp {
 292     static inline int cmp(const Node& n, const Node& m) {
 293       if ( n == m ) { return 0; }
 294
 295       // this is now slightly off of the old variable order.
 296
 297       bool nIsInteger = n.getType().isInteger();
 298       bool mIsInteger = m.getType().isInteger();
 299
 300       if(nIsInteger == mIsInteger){
 301         bool nIsVariable = n.isVar();
 302         bool mIsVariable = m.isVar();
 303
 304         if(nIsVariable == mIsVariable){
 305           if(n < m){
 306             return -1;
 307           }else{
 308             Assert(n != m);
 309             return 1;
 310           }
 311         }else{
 312           if(nIsVariable){
 313             return -1; // nIsVariable => !mIsVariable
 314           }else{
 315             return 1; // !nIsVariable => mIsVariable
 316           }
 317         }
 318       }else{
 319         Assert(nIsInteger != mIsInteger);
 320         if(nIsInteger){
 321           return 1; // nIsInteger => !mIsInteger
 322         }else{
 323           return -1; // !nIsInteger => mIsInteger
 324         }
 325       }
 326     }
 327
 328     bool operator()(const Node& n, const Node& m) const {
 329       return VariableNodeCmp::cmp(n,m) < 0;
 330     }
 331   };
 332
 333   bool operator==(const Variable& v) const { return getNode() == v.getNode();}
 334
 335   size_t getComplexity() const;
 336 };/* class Variable */
 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 {
 476   private:
 477     internal_iterator d_iter;
 478
 479   public:
 480     /* The following types are required by trait std::iterator_traits */
 481
 482     /** Iterator tag */
 483     using iterator_category = std::forward_iterator_tag;
 484
 485     /** The type of the item */
 486     using value_type = Variable;
 487
 488     /** The pointer type of the item */
 489     using pointer = Variable*;
 490
 491     /** The reference type of the item */
 492     using reference = Variable&;
 493
 494     /** The type returned when two iterators are subtracted */
 495     using difference_type = std::ptrdiff_t;
 496
 497     /* End of std::iterator_traits required types */
 498
 499     explicit iterator(internal_iterator i) : d_iter(i) {}
 500
 501     inline Variable operator*() {
 502       return Variable(*d_iter);
 503     }
 504
 505     bool operator==(const iterator& i) {
 506       return d_iter == i.d_iter;
 507     }
 508
 509     bool operator!=(const iterator& i) {
 510       return d_iter != i.d_iter;
 511     }
 512
 513     iterator operator++() {
 514       ++d_iter;
 515       return *this;
 516     }
 517
 518     iterator operator++(int) {
 519       return iterator(d_iter++);
 520     }
 521   };
 522
 523   iterator begin() const {
 524     return iterator(internalBegin());
 525   }
 526
 527   iterator end() const {
 528     return iterator(internalEnd());
 529   }
 530
 531   Variable getHead() const {
 532     Assert(!empty());
 533     return *(begin());
 534   }
 535
 536   VarList(Variable v) : NodeWrapper(v.getNode()) {
 537     Assert(isSorted(begin(), end()));
 538   }
 539
 540   VarList(const std::vector<Variable>& l) : NodeWrapper(multList(l)) {
 541     Assert(l.size() >= 2);
 542     Assert(isSorted(begin(), end()));
 543   }
 544
 545   static bool isMember(Node n);
 546
 547   bool isNormalForm() const {
 548     return !empty();
 549   }
 550
 551   static VarList mkEmptyVarList() {
 552     return VarList();
 553   }
 554
 555
 556   /** There are no restrictions on the size of l */
 557   static VarList mkVarList(const std::vector<Variable>& l) {
 558     if(l.size() == 0) {
 559       return mkEmptyVarList();
 560     } else if(l.size() == 1) {
 561       return VarList((*l.begin()).getNode());
 562     } else {
 563       return VarList(l);
 564     }
 565   }
 566
 567   bool empty() const { return getNode().isNull(); }
 568   bool singleton() const {
 569     return !empty() && getNode().getKind() != kind::NONLINEAR_MULT;
 570   }
 571
 572   int size() const {
 573     if(singleton())
 574       return 1;
 575     else
 576       return getNode().getNumChildren();
 577   }
 578
 579   static VarList parseVarList(Node n);
 580
 581   VarList operator*(const VarList& vl) const;
 582
 583   int cmp(const VarList& vl) const;
 584
 585   bool operator<(const VarList& vl) const { return cmp(vl) < 0; }
 586
 587   bool operator==(const VarList& vl) const { return cmp(vl) == 0; }
 588
 589   bool isIntegral() const {
 590     for(iterator i = begin(), e=end(); i != e; ++i ){
 591       Variable var = *i;
 592       if(!var.isIntegral()){
 593         return false;
 594       }
 595     }
 596     return true;
 597   }
 598   size_t getComplexity() const;
 599
 600 private:
 601   bool isSorted(iterator start, iterator end);
 602
 603 };/* class VarList */
 604
 605
 606 /** Constructors have side conditions. Use the static mkMonomial functions instead. */
 607 class Monomial : public NodeWrapper {
 608 private:
 609   Constant constant;
 610   VarList varList;
 611   Monomial(Node n, const Constant& c, const VarList& vl):
 612     NodeWrapper(n), constant(c), varList(vl)
 613   {
 614     Assert(!c.isZero() || vl.empty());
 615     Assert(c.isZero() || !vl.empty());
 616
 617     Assert(!c.isOne() || !multStructured(n));
 618   }
 619
 620   static Node makeMultNode(const Constant& c, const VarList& vl) {
 621     Assert(!c.isZero());
 622     Assert(!c.isOne());
 623     Assert(!vl.empty());
 624     return NodeManager::currentNM()->mkNode(kind::MULT, c.getNode(), vl.getNode());
 625   }
 626
 627   static bool multStructured(Node n) {
 628     return n.getKind() ==  kind::MULT &&
 629       n[0].getKind() == kind::CONST_RATIONAL &&
 630       n.getNumChildren() == 2;
 631   }
 632
 633   Monomial(const Constant& c):
 634     NodeWrapper(c.getNode()), constant(c), varList(VarList::mkEmptyVarList())
 635   { }
 636
 637   Monomial(const VarList& vl):
 638     NodeWrapper(vl.getNode()), constant(Constant::mkConstant(1)), varList(vl)
 639   {
 640     Assert(!varList.empty());
 641   }
 642
 643   Monomial(const Constant& c, const VarList& vl):
 644     NodeWrapper(makeMultNode(c,vl)), constant(c), varList(vl)
 645   {
 646     Assert(!c.isZero());
 647     Assert(!c.isOne());
 648     Assert(!varList.empty());
 649
 650     Assert(multStructured(getNode()));
 651   }
 652 public:
 653   static bool isMember(TNode n);
 654
 655   /** Makes a monomial with no restrictions on c and vl. */
 656   static Monomial mkMonomial(const Constant& c, const VarList& vl);
 657
 658   /** If vl is empty, this make one. */
 659   static Monomial mkMonomial(const VarList& vl);
 660
 661   static Monomial mkMonomial(const Constant& c){
 662     return Monomial(c);
 663   }
 664
 665   static Monomial mkMonomial(const Variable& v){
 666     return Monomial(VarList(v));
 667   }
 668
 669   static Monomial parseMonomial(Node n);
 670
 671   static Monomial mkZero() {
 672     return Monomial(Constant::mkConstant(0));
 673   }
 674   static Monomial mkOne() {
 675     return Monomial(Constant::mkConstant(1));
 676   }
 677   const Constant& getConstant() const { return constant; }
 678   const VarList& getVarList() const { return varList; }
 679
 680   bool isConstant() const {
 681     return varList.empty();
 682   }
 683
 684   bool isZero() const {
 685     return constant.isZero();
 686   }
 687
 688   bool coefficientIsOne() const {
 689     return constant.isOne();
 690   }
 691
 692   bool absCoefficientIsOne() const {
 693     return coefficientIsOne() || constant.getValue() == -1;
 694   }
 695
 696   bool constantIsPositive() const {
 697     return getConstant().isPositive();
 698   }
 699
 700   Monomial operator*(const Rational& q) const;
 701   Monomial operator*(const Constant& c) const;
 702   Monomial operator*(const Monomial& mono) const;
 703
 704   Monomial operator-() const{
 705     return (*this) * Rational(-1);
 706   }
 707
 708
 709   int cmp(const Monomial& mono) const {
 710     return getVarList().cmp(mono.getVarList());
 711   }
 712
 713   bool operator<(const Monomial& vl) const {
 714     return cmp(vl) < 0;
 715   }
 716
 717   bool operator==(const Monomial& vl) const {
 718     return cmp(vl) == 0;
 719   }
 720
 721   static bool isSorted(const std::vector<Monomial>& m) {
 722     return std::is_sorted(m.begin(), m.end());
 723   }
 724
 725   static bool isStrictlySorted(const std::vector<Monomial>& m) {
 726     return isSorted(m) && std::adjacent_find(m.begin(),m.end()) == m.end();
 727   }
 728
 729   static void sort(std::vector<Monomial>& m);
 730   static void combineAdjacentMonomials(std::vector<Monomial>& m);
 731
 732   /**
 733    * The variable product
 734    */
 735   bool integralVariables() const {
 736     return getVarList().isIntegral();
 737   }
 738
 739   /**
 740    * The coefficient of the monomial is integral.
 741    */
 742   bool integralCoefficient() const {
 743     return getConstant().isIntegral();
 744   }
 745
 746   /**
 747    * A Monomial is an "integral" monomial if the constant is integral.
 748    */
 749   bool isIntegral() const {
 750     return integralCoefficient() && integralVariables();
 751   }
 752
 753   /** Returns true if the VarList is a product of at least 2 Variables.*/
 754   bool isNonlinear() const {
 755     return getVarList().size() >= 2;
 756   }
 757
 758   /**
 759    * Given a sorted list of monomials, this function transforms this
 760    * into a strictly sorted list of monomials that does not contain zero.
 761    */
 762   //static std::vector<Monomial> sumLikeTerms(const std::vector<Monomial>& monos);
 763
 764   int absCmp(const Monomial& other) const{
 765     return getConstant().getValue().absCmp(other.getConstant().getValue());
 766   }
 767   // bool absLessThan(const Monomial& other) const{
 768   //   return getConstant().abs() < other.getConstant().abs();
 769   // }
 770
 771   uint32_t coefficientLength() const{
 772     return getConstant().length();
 773   }
 774
 775   void print() const;
 776   static void printList(const std::vector<Monomial>& list);
 777
 778   size_t getComplexity() const;
 779 };/* class Monomial */
 780
 781 class SumPair;
 782 class Comparison;;
 783
 784 class Polynomial : public NodeWrapper {
 785 private:
 786   bool d_singleton;
 787
 788   Polynomial(TNode n) : NodeWrapper(n), d_singleton(Monomial::isMember(n)) {
 789     Assert(isMember(getNode()));
 790   }
 791
 792   static Node makePlusNode(const std::vector<Monomial>& m) {
 793     Assert(m.size() >= 2);
 794
 795     return makeNode(kind::PLUS, m.begin(), m.end());
 796   }
 797
 798   typedef expr::NodeSelfIterator internal_iterator;
 799
 800   internal_iterator internalBegin() const {
 801     if(singleton()){
 802       return expr::NodeSelfIterator::self(getNode());
 803     }else{
 804       return getNode().begin();
 805     }
 806   }
 807
 808   internal_iterator internalEnd() const {
 809     if(singleton()){
 810       return expr::NodeSelfIterator::selfEnd(getNode());
 811     }else{
 812       return getNode().end();
 813     }
 814   }
 815
 816   bool singleton() const { return d_singleton; }
 817
 818 public:
 819   static bool isMember(TNode n);
 820
 821   class iterator {
 822   private:
 823     internal_iterator d_iter;
 824
 825   public:
 826     /* The following types are required by trait std::iterator_traits */
 827
 828     /** Iterator tag */
 829     using iterator_category = std::forward_iterator_tag;
 830
 831     /** The type of the item */
 832     using value_type = Monomial;
 833
 834     /** The pointer type of the item */
 835     using pointer = Monomial*;
 836
 837     /** The reference type of the item */
 838     using reference = Monomial&;
 839
 840     /** The type returned when two iterators are subtracted */
 841     using difference_type = std::ptrdiff_t;
 842
 843     /* End of std::iterator_traits required types */
 844
 845     explicit iterator(internal_iterator i) : d_iter(i) {}
 846
 847     inline Monomial operator*() {
 848       return Monomial::parseMonomial(*d_iter);
 849     }
 850
 851     bool operator==(const iterator& i) {
 852       return d_iter == i.d_iter;
 853     }
 854
 855     bool operator!=(const iterator& i) {
 856       return d_iter != i.d_iter;
 857     }
 858
 859     iterator operator++() {
 860       ++d_iter;
 861       return *this;
 862     }
 863
 864     iterator operator++(int) {
 865       return iterator(d_iter++);
 866     }
 867   };
 868
 869   iterator begin() const { return iterator(internalBegin()); }
 870   iterator end() const {  return iterator(internalEnd()); }
 871
 872   Polynomial(const Monomial& m):
 873     NodeWrapper(m.getNode()), d_singleton(true)
 874   {}
 875
 876   Polynomial(const std::vector<Monomial>& m):
 877     NodeWrapper(makePlusNode(m)), d_singleton(false)
 878   {
 879     Assert(m.size() >= 2);
 880     Assert(Monomial::isStrictlySorted(m));
 881   }
 882
 883   static Polynomial mkPolynomial(const Constant& c){
 884     return Polynomial(Monomial::mkMonomial(c));
 885   }
 886
 887   static Polynomial mkPolynomial(const Variable& v){
 888     return Polynomial(Monomial::mkMonomial(v));
 889   }
 890
 891   static Polynomial mkPolynomial(const std::vector<Monomial>& m) {
 892     if(m.size() == 0) {
 893       return Polynomial(Monomial::mkZero());
 894     } else if(m.size() == 1) {
 895       return Polynomial((*m.begin()));
 896     } else {
 897       return Polynomial(m);
 898     }
 899   }
 900
 901   static Polynomial parsePolynomial(Node n) {
 902     return Polynomial(n);
 903   }
 904
 905   static Polynomial mkZero() {
 906     return Polynomial(Monomial::mkZero());
 907   }
 908   static Polynomial mkOne() {
 909     return Polynomial(Monomial::mkOne());
 910   }
 911   bool isZero() const {
 912     return singleton() && (getHead().isZero());
 913   }
 914
 915   bool isConstant() const {
 916     return singleton() && (getHead().isConstant());
 917   }
 918
 919   bool containsConstant() const {
 920     return getHead().isConstant();
 921   }
 922
 923   uint32_t size() const{
 924     if(singleton()){
 925       return 1;
 926     }else{
 927       Assert(getNode().getKind() == kind::PLUS);
 928       return getNode().getNumChildren();
 929     }
 930   }
 931
 932   Monomial getHead() const {
 933     return *(begin());
 934   }
 935
 936   Polynomial getTail() const {
 937     Assert(!singleton());
 938
 939     iterator tailStart = begin();
 940     ++tailStart;
 941     std::vector<Monomial> subrange;
 942     std::copy(tailStart, end(), std::back_inserter(subrange));
 943     return mkPolynomial(subrange);
 944   }
 945
 946   Monomial minimumVariableMonomial() const;
 947   bool variableMonomialAreStrictlyGreater(const Monomial& m) const;
 948
 949   void printList() const {
 950     if(Debug.isOn("normal-form")){
 951       Debug("normal-form") << "start list" << std::endl;
 952       for(iterator i = begin(), oend = end(); i != oend; ++i) {
 953         const Monomial& m =*i;
 954         m.print();
 955       }
 956       Debug("normal-form") << "end list" << std::endl;
 957     }
 958   }
 959
 960   /** A Polynomial is an "integral" polynomial if all of the monomials are integral. */
 961   bool allIntegralVariables() const {
 962     for(iterator i = begin(), e=end(); i!=e; ++i){
 963       if(!(*i).integralVariables()){
 964         return false;
 965       }
 966     }
 967     return true;
 968   }
 969
 970   /**
 971    * A Polynomial is an "integral" polynomial if all of the monomials are integral
 972    * and all of the coefficients are Integral. */
 973   bool isIntegral() const {
 974     for(iterator i = begin(), e=end(); i!=e; ++i){
 975       if(!(*i).isIntegral()){
 976         return false;
 977       }
 978     }
 979     return true;
 980   }
 981
 982   static Polynomial sumPolynomials(const std::vector<Polynomial>& polynomials);
 983
 984   /** Returns true if the polynomial contains a non-linear monomial.*/
 985   bool isNonlinear() const;
 986
 987   /** Check whether this polynomial is only a single variable. */
 988   bool isVariable() const
 989   {
 990     return singleton() && getHead().getVarList().singleton()
 991            && getHead().coefficientIsOne();
 992   }
 993   /** Return the variable, given that isVariable() holds. */
 994   Variable getVariable() const
 995   {
 996     Assert(isVariable());
 997     return getHead().getVarList().getHead();
 998   }
 999
1000   /**
1001    * Selects a minimal monomial in the polynomial by the absolute value of
1002    * the coefficient.
1003    */
1004   Monomial selectAbsMinimum() const;
1005
1006   /** Returns true if the absolute value of the head coefficient is one. */
1007   bool leadingCoefficientIsAbsOne() const;
1008   bool leadingCoefficientIsPositive() const;
1009   bool denominatorLCMIsOne() const;
1010   bool numeratorGCDIsOne() const;
1011
1012   bool signNormalizedReducedSum() const {
1013     return leadingCoefficientIsPositive() && denominatorLCMIsOne() && numeratorGCDIsOne();
1014   }
1015
1016   /**
1017    * Returns the Least Common Multiple of the denominators of the coefficients
1018    * of the monomials.
1019    */
1020   Integer denominatorLCM() const;
1021
1022   /**
1023    * Returns the GCD of the numerators of the monomials.
1024    * Requires this to be an isIntegral() polynomial.
1025    */
1026   Integer numeratorGCD() const;
1027
1028   /**
1029    * Returns the GCD of the coefficients of the monomials.
1030    * Requires this to be an isIntegral() polynomial.
1031    */
1032   Integer gcd() const;
1033
1034   /** z must divide all of the coefficients of the polynomial. */
1035   Polynomial exactDivide(const Integer& z) const;
1036
1037   Polynomial operator+(const Polynomial& vl) const;
1038   Polynomial operator-(const Polynomial& vl) const;
1039   Polynomial operator-() const{
1040     return (*this) * Rational(-1);
1041   }
1042
1043   Polynomial operator*(const Rational& q) const;
1044   Polynomial operator*(const Constant& c) const;
1045   Polynomial operator*(const Monomial& mono) const;
1046
1047   Polynomial operator*(const Polynomial& poly) const;
1048
1049   /**
1050    * Viewing the integer polynomial as a list [(* coeff_i mono_i)]
1051    * The quotient and remainder of p divided by the non-zero integer z is:
1052    *   q := [(* floor(coeff_i/z) mono_i )]
1053    *   r := [(* rem(coeff_i/z) mono_i)]
1054    * computeQR(p,z) returns the node (+ q r).
1055    *
1056    * q and r are members of the Polynomial class.
1057    * For example:
1058    * computeQR( p = (+ 5 (* 3 x) (* 8 y)) , z = 2) returns
1059    *   (+ (+ 2 x (* 4 y)) (+ 1 x))
1060    */
1061   static Node computeQR(const Polynomial& p, const Integer& z);
1062
1063   /** Returns the coefficient associated with the VarList in the polynomial. */
1064   Constant getCoefficient(const VarList& vl) const;
1065
1066   uint32_t maxLength() const{
1067     iterator i = begin(), e=end();
1068     if( i == e){
1069       return 1;
1070     }else{
1071       uint32_t max = (*i).coefficientLength();
1072       ++i;
1073       for(; i!=e; ++i){
1074         uint32_t curr = (*i).coefficientLength();
1075         if(curr > max){
1076           max = curr;
1077         }
1078       }
1079       return max;
1080     }
1081   }
1082
1083   uint32_t numMonomials() const {
1084     if( getNode().getKind() == kind::PLUS ){
1085       return getNode().getNumChildren();
1086     }else if(isZero()){
1087       return 0;
1088     }else{
1089       return 1;
1090     }
1091   }
1092
1093   const Rational& asConstant() const{
1094     Assert(isConstant());
1095     return getNode().getConst<Rational>();
1096     //return getHead().getConstant().getValue();
1097   }
1098
1099   bool isVarList() const {
1100     if(singleton()){
1101       return VarList::isMember(getNode());
1102     }else{
1103       return false;
1104     }
1105   }
1106
1107   VarList asVarList() const {
1108     Assert(isVarList());
1109     return getHead().getVarList();
1110   }
1111
1112   size_t getComplexity() const;
1113
1114   friend class SumPair;
1115   friend class Comparison;
1116
1117   /** Returns a node that if asserted ensures v is the abs of this polynomial.*/
1118   Node makeAbsCondition(Variable v){
1119     return makeAbsCondition(v, *this);
1120   }
1121
1122   /** Returns a node that if asserted ensures v is the abs of p.*/
1123   static Node makeAbsCondition(Variable v, Polynomial p);
1124
1125 };/* class Polynomial */
1126
1127
1128 /**
1129  * SumPair is a utility class that extends polynomials for use in computations.
1130  * A SumPair is always a combination of (+ p c) where
1131  *  c is a constant and p is a polynomial such that p = 0 or !p.containsConstant().
1132  *
1133  * These are a useful utility for representing the equation p = c as (+ p -c) where the pair
1134  * is known to implicitly be equal to 0.
1135  *
1136  * SumPairs do not have unique representations due to the potential for p = 0.
1137  * This makes them inappropriate for normal forms.
1138  */
1139 class SumPair : public NodeWrapper {
1140 private:
1141   static Node toNode(const Polynomial& p, const Constant& c){
1142     return NodeManager::currentNM()->mkNode(kind::PLUS, p.getNode(), c.getNode());
1143   }
1144
1145   SumPair(TNode n) : NodeWrapper(n) { Assert(isNormalForm()); }
1146
1147  public:
1148   SumPair(const Polynomial& p):
1149     NodeWrapper(toNode(p, Constant::mkConstant(0)))
1150   {
1151     Assert(isNormalForm());
1152   }
1153
1154   SumPair(const Polynomial& p, const Constant& c):
1155     NodeWrapper(toNode(p, c))
1156   {
1157     Assert(isNormalForm());
1158   }
1159
1160   static bool isMember(TNode n) {
1161     if(n.getKind() == kind::PLUS && n.getNumChildren() == 2){
1162       if(Constant::isMember(n[1])){
1163         if(Polynomial::isMember(n[0])){
1164           Polynomial p = Polynomial::parsePolynomial(n[0]);
1165           return p.isZero() || (!p.containsConstant());
1166         }else{
1167           return false;
1168         }
1169       }else{
1170         return false;
1171       }
1172     }else{
1173       return false;
1174     }
1175   }
1176
1177   bool isNormalForm() const {
1178     return isMember(getNode());
1179   }
1180
1181   Polynomial getPolynomial() const {
1182     return Polynomial::parsePolynomial(getNode()[0]);
1183   }
1184
1185   Constant getConstant() const {
1186     return Constant::mkConstant((getNode())[1]);
1187   }
1188
1189   SumPair operator+(const SumPair& other) const {
1190     return SumPair(getPolynomial() + other.getPolynomial(),
1191                    getConstant() + other.getConstant());
1192   }
1193
1194   SumPair operator*(const Constant& c) const {
1195     return SumPair(getPolynomial() * c, getConstant() * c);
1196   }
1197
1198   SumPair operator-(const SumPair& other) const {
1199     return (*this) + (other * Constant::mkConstant(-1));
1200   }
1201
1202   static SumPair mkSumPair(const Polynomial& p);
1203
1204   static SumPair mkSumPair(const Variable& var){
1205     return SumPair(Polynomial::mkPolynomial(var));
1206   }
1207
1208   static SumPair parseSumPair(TNode n){
1209     return SumPair(n);
1210   }
1211
1212   bool isIntegral() const{
1213     return getConstant().isIntegral() && getPolynomial().isIntegral();
1214   }
1215
1216   bool isConstant() const {
1217     return getPolynomial().isZero();
1218   }
1219
1220   bool isZero() const {
1221     return getConstant().isZero() && isConstant();
1222   }
1223
1224   uint32_t size() const{
1225     return getPolynomial().size();
1226   }
1227
1228   bool isNonlinear() const{
1229     return getPolynomial().isNonlinear();
1230   }
1231
1232   /**
1233    * Returns the greatest common divisor of gcd(getPolynomial()) and getConstant().
1234    * The SumPair must be integral.
1235    */
1236   Integer gcd() const {
1237     Assert(isIntegral());
1238     return (getPolynomial().gcd()).gcd(getConstant().getValue().getNumerator());
1239   }
1240
1241   uint32_t maxLength() const {
1242     Assert(isIntegral());
1243     return std::max(getPolynomial().maxLength(), getConstant().length());
1244   }
1245
1246   static SumPair mkZero() {
1247     return SumPair(Polynomial::mkZero(), Constant::mkConstant(0));
1248   }
1249
1250   static Node computeQR(const SumPair& sp, const Integer& div);
1251
1252 };/* class SumPair */
1253
1254 /* class OrderedPolynomialPair { */
1255 /* private: */
1256 /*   Polynomial d_first; */
1257 /*   Polynomial d_second; */
1258 /* public: */
1259 /*   OrderedPolynomialPair(const Polynomial& f, const Polynomial& s) */
1260 /*     : d_first(f), */
1261 /*       d_second(s) */
1262 /*   {} */
1263
1264 /*   /\** Returns the first part of the pair. *\/ */
1265 /*   const Polynomial& getFirst() const { */
1266 /*     return d_first; */
1267 /*   } */
1268
1269 /*   /\** Returns the second part of the pair. *\/ */
1270 /*   const Polynomial& getSecond() const { */
1271 /*     return d_second; */
1272 /*   } */
1273
1274 /*   OrderedPolynomialPair operator*(const Constant& c) const; */
1275 /*   OrderedPolynomialPair operator+(const Polynomial& p) const; */
1276
1277 /*   /\** Returns true if both of the polynomials are constant. *\/ */
1278 /*   bool isConstant() const; */
1279
1280 /*   /\** */
1281 /*    * Evaluates an isConstant() ordered pair as if */
1282 /*    *   (k getFirst() getRight()) */
1283 /*    *\/ */
1284 /*   bool evaluateConstant(Kind k) const; */
1285
1286 /*   /\** */
1287 /*    * Returns the Least Common Multiple of the monomials */
1288 /*    * on the lefthand side and the constant on the right. */
1289 /*    *\/ */
1290 /*   Integer denominatorLCM() const; */
1291
1292 /*   /\** Constructs a SumPair. *\/ */
1293 /*   SumPair toSumPair() const; */
1294
1295
1296 /*   OrderedPolynomialPair divideByGCD() const; */
1297 /*   OrderedPolynomialPair multiplyConstant(const Constant& c) const; */
1298
1299 /*   /\** */
1300 /*    * Returns true if all of the variables are integers, */
1301 /*    * and the coefficients are integers. */
1302 /*    *\/ */
1303 /*   bool isIntegral() const; */
1304
1305 /*   /\** Returns true if all of the variables are integers. *\/ */
1306 /*   bool allIntegralVariables() const { */
1307 /*     return getFirst().allIntegralVariables() && getSecond().allIntegralVariables(); */
1308 /*   } */
1309 /* }; */
1310
1311 class Comparison : public NodeWrapper {
1312 private:
1313
1314   static Node toNode(Kind k, const Polynomial& l, const Constant& c);
1315   static Node toNode(Kind k, const Polynomial& l, const Polynomial& r);
1316
1317   Comparison(TNode n);
1318
1319   /**
1320    * Creates a node in normal form equivalent to (= l 0).
1321    * All variables in l are integral.
1322    */
1323   static Node mkIntEquality(const Polynomial& l);
1324
1325   /**
1326    * Creates a comparison equivalent to (k l 0).
1327    * k is either GT or GEQ.
1328    * All variables in l are integral.
1329    */
1330   static Node mkIntInequality(Kind k, const Polynomial& l);
1331
1332   /**
1333    * Creates a node equivalent to (= l 0).
1334    * It is not the case that all variables in l are integral.
1335    */
1336   static Node mkRatEquality(const Polynomial& l);
1337
1338   /**
1339    * Creates a comparison equivalent to (k l 0).
1340    * k is either GT or GEQ.
1341    * It is not the case that all variables in l are integral.
1342    */
1343   static Node mkRatInequality(Kind k, const Polynomial& l);
1344
1345 public:
1346
1347   Comparison(bool val) :
1348     NodeWrapper(NodeManager::currentNM()->mkConst(val))
1349   { }
1350
1351   /**
1352    * Given a literal to TheoryArith return a single kind to
1353    * to indicate its underlying structure.
1354    * The function returns the following in each case:
1355    * - (K left right)           -> K where is either EQUAL, GT, or GEQ
1356    * - (CONST_BOOLEAN b)        -> CONST_BOOLEAN
1357    * - (NOT (EQUAL left right)) -> DISTINCT
1358    * - (NOT (GT left right))    -> LEQ
1359    * - (NOT (GEQ left right))   -> LT
1360    * If none of these match, it returns UNDEFINED_KIND.
1361    */
1362   static Kind comparisonKind(TNode literal);
1363
1364   Kind comparisonKind() const { return comparisonKind(getNode()); }
1365
1366   static Comparison mkComparison(Kind k, const Polynomial& l, const Polynomial& r);
1367
1368   /** Returns true if the comparison is a boolean constant. */
1369   bool isBoolean() const;
1370
1371   /**
1372    * Returns true if the comparison is either a boolean term,
1373    * in integer normal form or mixed normal form.
1374    */
1375   bool isNormalForm() const;
1376
1377 private:
1378   bool isNormalGT() const;
1379   bool isNormalGEQ() const;
1380
1381   bool isNormalLT() const;
1382   bool isNormalLEQ() const;
1383
1384   bool isNormalEquality() const;
1385   bool isNormalDistinct() const;
1386   bool isNormalEqualityOrDisequality() const;
1387
1388   bool allIntegralVariables() const {
1389     return getLeft().allIntegralVariables() && getRight().allIntegralVariables();
1390   }
1391   bool rightIsConstant() const;
1392
1393 public:
1394   Polynomial getLeft() const;
1395   Polynomial getRight() const;
1396
1397   /* /\** Normal form check if at least one variable is real. *\/ */
1398   /* bool isMixedCompareNormalForm() const; */
1399
1400   /* /\** Normal form check if at least one variable is real. *\/ */
1401   /* bool isMixedEqualsNormalForm() const; */
1402
1403   /* /\** Normal form check is all variables are integer.*\/ */
1404   /* bool isIntegerCompareNormalForm() const; */
1405
1406   /* /\** Normal form check is all variables are integer.*\/ */
1407   /* bool isIntegerEqualsNormalForm() const; */
1408
1409
1410   /**
1411    * Returns true if all of the variables are integers, the coefficients are integers,
1412    * and the right hand coefficient is an integer.
1413    */
1414   bool debugIsIntegral() const;
1415
1416   static Comparison parseNormalForm(TNode n);
1417
1418   inline static bool isNormalAtom(TNode n){
1419     Comparison parse = Comparison::parseNormalForm(n);
1420     return parse.isNormalForm();
1421   }
1422
1423   size_t getComplexity() const;
1424
1425   SumPair toSumPair() const;
1426
1427   Polynomial normalizedVariablePart() const;
1428   DeltaRational normalizedDeltaRational() const;
1429
1430   /**
1431    * Transforms a Comparison object into a stronger normal form:
1432    *    Polynomial ~Kind~ Constant
1433    *
1434    * From the comparison, this method resolved a negation (if present) and
1435    * moves everything to the left side.
1436    * If split_constant is false, the constant is always zero.
1437    * If split_constant is true, the polynomial has no constant term and is
1438    * normalized to have leading coefficient one.
1439    */
1440   std::tuple<Polynomial, Kind, Constant> decompose(
1441       bool split_constant = false) const;
1442
1443 };/* class Comparison */
1444
1445 }  // namespace arith
1446 }  // namespace theory
1447 }  // namespace cvc5
1448
1449 #endif /* CVC5__THEORY__ARITH__NORMAL_FORM_H */