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