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