src/theory/arith/normal_form.h

   1 /*********************                                                        */
   2 /*! \file normal_form.h
   3  ** \verbatim
   4  ** Original author: taking
   5  ** Major contributors: mdeters
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief [[ Add one-line brief description here ]]
  15  **
  16  ** [[ Add lengthier description here ]]
  17  ** \todo document this file
  18  **/
  19
  20 #include "cvc4_private.h"
  21
  22 #ifndef __CVC4__THEORY__ARITH__NORMAL_FORM_H
  23 #define __CVC4__THEORY__ARITH__NORMAL_FORM_H
  24
  25 #include "expr/node.h"
  26 #include "expr/node_self_iterator.h"
  27 #include "util/rational.h"
  28 #include "theory/arith/arith_constants.h"
  29 #include "theory/arith/arith_utilities.h"
  30
  31 #include <list>
  32 #include <algorithm>
  33 #include <ext/algorithm>
  34
  35 namespace CVC4 {
  36 namespace theory {
  37 namespace arith {
  38
  39 /***********************************************/
  40 /***************** Normal Form *****************/
  41 /***********************************************/
  42 /***********************************************/
  43
  44 /**
  45  * Section 1: Languages
  46  * The normal form for arithmetic nodes is defined by the language
  47  * accepted by the following BNFs with some guard conditions.
  48  * (The guard conditions are in Section 3 for completeness.)
  49  *
  50  * variable := n
  51  *   where
  52  *     n.getMetaKind() == metakind::VARIABLE
  53  *
  54  * constant := n
  55  *   where
  56  *     n.getKind() == kind::CONST_RATIONAL
  57  *
  58  * var_list := variable | (* [variable])
  59  *   where
  60  *     len [variable] >= 2
  61  *     isSorted varOrder [variable]
  62  *
  63  * monomial := constant | var_list | (* constant' var_list')
  64  *   where
  65  *     constant' \not\in {0,1}
  66  *
  67  * polynomial := monomial' | (+ [monomial])
  68  *   where
  69  *     len [monomial] >= 2
  70  *     isStrictlySorted monoOrder [monomial]
  71  *     forall (\x -> x != 0) [monomial]
  72  *
  73  * restricted_cmp := (|><| polynomial constant)
  74  *   where
  75  *     |><| is GEQ, EQ, or EQ
  76  *     not (exists constantMonomial (monomialList polynomial))
  77  *     monomialCoefficient (head (monomialList polynomial)) == 1
  78  *
  79  * comparison := TRUE | FALSE | restricted_cmp | (not restricted_cmp)
  80  *
  81  * Normal Form for terms := polynomial
  82  * Normal Form for atoms := comparison
  83  */
  84
  85 /**
  86  * Section 2: Helper Classes
  87  * The langauges accepted by each of these defintions
  88  * roughly corresponds to one of the following helper classes:
  89  *  Variable
  90  *  Constant
  91  *  VarList
  92  *  Monomial
  93  *  Polynomial
  94  *  Comparison
  95  *
  96  * Each of the classes obeys the following contracts/design decisions:
  97  * -Calling isMember(Node node) on a node returns true iff that node is a
  98  *  a member of the language. Note: isMember is O(n).
  99  * -Calling isNormalForm() on a helper class object returns true iff that
 100  *  helper class currently represents a normal form object.
 101  * -If isNormalForm() is false, then this object must have been made
 102  *  using a mk*() factory function.
 103  * -If isNormalForm() is true, calling getNode() on all of these classes
 104  *  returns a node that would be accepted by the corresponding language.
 105  *  And if isNormalForm() is false, returns Node::null().
 106  * -Each of the classes is immutable.
 107  * -Public facing constuctors have a 1-to-1 correspondence with one of
 108  *  production rules in the above grammar.
 109  * -Public facing constuctors are required to fail in debug mode when the
 110  *  guards of the production rule are not strictly met.
 111  *  For example: Monomial(Constant(1),VarList(Variable(x))) must fail.
 112  * -When a class has a Class parseClass(Node node) function,
 113  *  if isMember(node) is true, the function is required to return an instance
 114  *  of the helper class, instance, s.t. instance.getNode() == node.
 115  *  And if isMember(node) is false, this throws an assertion failure in debug
 116  *  mode and has undefined behaviour if not in debug mode.
 117  * -Only public facing constructors, parseClass(node), and mk*() functions are
 118  *  considered privileged functions for the helper class.
 119  * -Only privileged functions may use private constructors, and access
 120  *  private data members.
 121  * -All non-privileged functions are considered utility functions and
 122  *  must use a privileged function in order to create an instance of the class.
 123  */
 124
 125 /**
 126  * Section 3: Guard Conditions Misc.
 127  *
 128  *
 129  *  var_list_len vl =
 130  *    match vl with
 131  *       variable -> 1
 132  *     | (* [variable]) -> len [variable]
 133  *
 134  *  order res =
 135  *    match res with
 136  *       Empty -> (0,Node::null())
 137  *     | NonEmpty(vl) -> (var_list_len vl, vl)
 138  *
 139  *  var_listOrder a b = tuple_cmp (order a) (order b)
 140  *
 141  *  monomialVarList monomial =
 142  *    match monomial with
 143  *        constant -> Empty
 144  *      | var_list -> NonEmpty(var_list)
 145  *      | (* constant' var_list') -> NonEmpty(var_list')
 146  *
 147  *  monoOrder m0 m1 = var_listOrder (monomialVarList m0) (monomialVarList m1)
 148  *
 149  *  constantMonomial monomial =
 150  *    match monomial with
 151  *        constant -> true
 152  *      | var_list -> false
 153  *      | (* constant' var_list') -> false
 154  *
 155  *  monomialCoefficient monomial =
 156  *    match monomial with
 157  *        constant -> constant
 158  *      | var_list -> Constant(1)
 159  *      | (* constant' var_list') -> constant'
 160  *
 161  *  monomialList polynomial =
 162  *    match polynomial with
 163  *        monomial -> monomial::[]
 164  *      | (+ [monomial]) -> [monomial]
 165  */
 166
 167
 168 /**
 169  * A NodeWrapper is a class that is a thinly veiled container of a Node object.
 170  */
 171 class NodeWrapper {
 172 private:
 173   Node node;
 174 public:
 175   NodeWrapper(Node n) : node(n) {}
 176   const Node& getNode() const { return node; }
 177 };/* class NodeWrapper */
 178
 179
 180 class Variable : public NodeWrapper {
 181 public:
 182   Variable(Node n) : NodeWrapper(n) {
 183     Assert(isMember(getNode()));
 184   }
 185
 186   static bool isMember(Node n) {
 187     return n.getMetaKind() == kind::metakind::VARIABLE;
 188   }
 189
 190   bool isNormalForm() { return isMember(getNode()); }
 191
 192   bool operator<(const Variable& v) const { return getNode() < v.getNode();}
 193   bool operator==(const Variable& v) const { return getNode() == v.getNode();}
 194
 195 };/* class Variable */
 196
 197
 198 class Constant : public NodeWrapper {
 199 public:
 200   Constant(Node n) : NodeWrapper(n) {
 201     Assert(isMember(getNode()));
 202   }
 203
 204   static bool isMember(Node n) {
 205     return n.getKind() == kind::CONST_RATIONAL;
 206   }
 207
 208   bool isNormalForm() { return isMember(getNode()); }
 209
 210   static Constant mkConstant(Node n) {
 211     return Constant(coerceToRationalNode(n));
 212   }
 213
 214   static Constant mkConstant(const Rational& rat) {
 215     return Constant(mkRationalNode(rat));
 216   }
 217
 218   const Rational& getValue() const {
 219     return getNode().getConst<Rational>();
 220   }
 221
 222   bool isZero() const { return getValue() == 0; }
 223   bool isOne() const { return getValue() == 1; }
 224
 225   Constant operator*(const Constant& other) const {
 226     return mkConstant(getValue() * other.getValue());
 227   }
 228   Constant operator+(const Constant& other) const {
 229     return mkConstant(getValue() + other.getValue());
 230   }
 231   Constant operator-() const {
 232     return mkConstant(-getValue());
 233   }
 234
 235 };/* class Constant */
 236
 237
 238 template <class GetNodeIterator>
 239 inline Node makeNode(Kind k, GetNodeIterator start, GetNodeIterator end) {
 240   NodeBuilder<> nb(k);
 241
 242   while(start != end) {
 243     nb << (*start).getNode();
 244     ++start;
 245   }
 246
 247   return Node(nb);
 248 }/* makeNode<GetNodeIterator>(Kind, iterator, iterator) */
 249
 250
 251 template <class GetNodeIterator, class T>
 252 static void copy_range(GetNodeIterator begin, GetNodeIterator end, std::vector<T>& result){
 253   while(begin != end){
 254     result.push_back(*begin);
 255     ++begin;
 256   }
 257 }
 258
 259 template <class GetNodeIterator, class T>
 260 static void merge_ranges(GetNodeIterator first1,
 261                   GetNodeIterator last1,
 262                   GetNodeIterator first2,
 263                   GetNodeIterator last2,
 264                   std::vector<T>& result) {
 265
 266   while(first1 != last1 && first2 != last2){
 267     if( (*first1) < (*first2) ){
 268       result.push_back(*first1);
 269       ++ first1;
 270     }else{
 271       result.push_back(*first2);
 272       ++ first2;
 273     }
 274   }
 275   copy_range(first1, last1, result);
 276   copy_range(first2, last2, result);
 277 }
 278
 279 /**
 280  * A VarList is a sorted list of variables representing a product.
 281  * If the VarList is empty, it represents an empty product or 1.
 282  * If the VarList has size 1, it represents a single variable.
 283  *
 284  * A non-sorted VarList can never be successfully made in debug mode.
 285  */
 286 class VarList : public NodeWrapper {
 287 private:
 288
 289   static Node multList(const std::vector<Variable>& list) {
 290     Assert(list.size() >= 2);
 291
 292     return makeNode(kind::MULT, list.begin(), list.end());
 293   }
 294
 295   VarList() : NodeWrapper(Node::null()) {}
 296
 297   VarList(Node n) : NodeWrapper(n) {
 298     Assert(isSorted(begin(), end()));
 299   }
 300
 301   typedef expr::NodeSelfIterator internal_iterator;
 302
 303   internal_iterator internalBegin() const {
 304     if(singleton()){
 305       return expr::NodeSelfIterator::self(getNode());
 306     }else{
 307       return getNode().begin();
 308     }
 309   }
 310
 311   internal_iterator internalEnd() const {
 312     if(singleton()){
 313       return expr::NodeSelfIterator::selfEnd(getNode());
 314     }else{
 315       return getNode().end();
 316     }
 317   }
 318
 319 public:
 320
 321   class iterator {
 322   private:
 323     internal_iterator d_iter;
 324
 325   public:
 326     explicit iterator(internal_iterator i) : d_iter(i) {}
 327
 328     inline Variable operator*() {
 329       return Variable(*d_iter);
 330     }
 331
 332     bool operator==(const iterator& i) {
 333       return d_iter == i.d_iter;
 334     }
 335
 336     bool operator!=(const iterator& i) {
 337       return d_iter != i.d_iter;
 338     }
 339
 340     iterator operator++() {
 341       ++d_iter;
 342       return *this;
 343     }
 344
 345     iterator operator++(int) {
 346       return iterator(d_iter++);
 347     }
 348   };
 349
 350   iterator begin() const {
 351     return iterator(internalBegin());
 352   }
 353
 354   iterator end() const {
 355     return iterator(internalEnd());
 356   }
 357
 358   VarList(Variable v) : NodeWrapper(v.getNode()) {
 359     Assert(isSorted(begin(), end()));
 360   }
 361
 362   VarList(const std::vector<Variable>& l) : NodeWrapper(multList(l)) {
 363     Assert(l.size() >= 2);
 364     Assert(isSorted(begin(), end()));
 365   }
 366
 367   static bool isMember(Node n);
 368
 369   bool isNormalForm() const {
 370     return !empty();
 371   }
 372
 373   static VarList mkEmptyVarList() {
 374     return VarList();
 375   }
 376
 377
 378   /** There are no restrictions on the size of l */
 379   static VarList mkVarList(const std::vector<Variable>& l) {
 380     if(l.size() == 0) {
 381       return mkEmptyVarList();
 382     } else if(l.size() == 1) {
 383       return VarList((*l.begin()).getNode());
 384     } else {
 385       return VarList(l);
 386     }
 387   }
 388
 389   bool empty() const { return getNode().isNull(); }
 390   bool singleton() const {
 391     return !empty() && getNode().getKind() != kind::MULT;
 392   }
 393
 394   int size() const {
 395     if(singleton())
 396       return 1;
 397     else
 398       return getNode().getNumChildren();
 399   }
 400
 401   static VarList parseVarList(Node n);
 402
 403   VarList operator*(const VarList& vl) const;
 404
 405   int cmp(const VarList& vl) const;
 406
 407   bool operator<(const VarList& vl) const { return cmp(vl) < 0; }
 408
 409   bool operator==(const VarList& vl) const { return cmp(vl) == 0; }
 410
 411 private:
 412   bool isSorted(iterator start, iterator end);
 413
 414 };/* class VarList */
 415
 416
 417 class Monomial : public NodeWrapper {
 418 private:
 419   Constant constant;
 420   VarList varList;
 421   Monomial(Node n, const Constant& c, const VarList& vl):
 422     NodeWrapper(n), constant(c), varList(vl)
 423   {
 424     Assert(!c.isZero() ||  vl.empty() );
 425     Assert( c.isZero() || !vl.empty() );
 426
 427     Assert(!c.isOne() || !multStructured(n));
 428   }
 429
 430   static Node makeMultNode(const Constant& c, const VarList& vl) {
 431     Assert(!c.isZero());
 432     Assert(!c.isOne());
 433     Assert(!vl.empty());
 434     return NodeManager::currentNM()->mkNode(kind::MULT, c.getNode(), vl.getNode());
 435   }
 436
 437   static bool multStructured(Node n) {
 438     return n.getKind() ==  kind::MULT &&
 439       n[0].getKind() == kind::CONST_RATIONAL &&
 440       n.getNumChildren() == 2;
 441   }
 442
 443 public:
 444
 445   Monomial(const Constant& c):
 446     NodeWrapper(c.getNode()), constant(c), varList(VarList::mkEmptyVarList())
 447   { }
 448
 449   Monomial(const VarList& vl):
 450     NodeWrapper(vl.getNode()), constant(Constant::mkConstant(1)), varList(vl)
 451   {
 452     Assert( !varList.empty() );
 453   }
 454
 455   Monomial(const Constant& c, const VarList& vl):
 456     NodeWrapper(makeMultNode(c,vl)), constant(c), varList(vl)
 457   {
 458     Assert( !c.isZero() );
 459     Assert( !c.isOne() );
 460     Assert( !varList.empty() );
 461
 462     Assert(multStructured(getNode()));
 463   }
 464
 465   static bool isMember(TNode n);
 466
 467   /** Makes a monomial with no restrictions on c and vl. */
 468   static Monomial mkMonomial(const Constant& c, const VarList& vl);
 469
 470
 471   static Monomial parseMonomial(Node n);
 472
 473   static Monomial mkZero() {
 474     return Monomial(Constant::mkConstant(0));
 475   }
 476   static Monomial mkOne() {
 477     return Monomial(Constant::mkConstant(1));
 478   }
 479   const Constant& getConstant() const { return constant; }
 480   const VarList& getVarList() const { return varList; }
 481
 482   bool isConstant() const {
 483     return varList.empty();
 484   }
 485
 486   bool isZero() const {
 487     return constant.isZero();
 488   }
 489
 490   bool coefficientIsOne() const {
 491     return constant.isOne();
 492   }
 493
 494   Monomial operator*(const Monomial& mono) const;
 495
 496
 497   int cmp(const Monomial& mono) const {
 498     return getVarList().cmp(mono.getVarList());
 499   }
 500
 501   bool operator<(const Monomial& vl) const {
 502     return cmp(vl) < 0;
 503   }
 504
 505   bool operator==(const Monomial& vl) const {
 506     return cmp(vl) == 0;
 507   }
 508
 509   static bool isSorted(const std::vector<Monomial>& m) {
 510     return __gnu_cxx::is_sorted(m.begin(), m.end());
 511   }
 512
 513   static bool isStrictlySorted(const std::vector<Monomial>& m) {
 514     return isSorted(m) && std::adjacent_find(m.begin(),m.end()) == m.end();
 515   }
 516
 517   /**
 518    * Given a sorted list of monomials, this function transforms this
 519    * into a strictly sorted list of monomials that does not contain zero.
 520    */
 521   static std::vector<Monomial> sumLikeTerms(const std::vector<Monomial>& monos);
 522
 523   void print() const;
 524   static void printList(const std::vector<Monomial>& list);
 525
 526 };/* class Monomial */
 527
 528
 529 class Polynomial : public NodeWrapper {
 530 private:
 531   bool d_singleton;
 532
 533   Polynomial(TNode n) : NodeWrapper(n), d_singleton(Monomial::isMember(n)) {
 534     Assert(isMember(getNode()));
 535   }
 536
 537   static Node makePlusNode(const std::vector<Monomial>& m) {
 538     Assert(m.size() >= 2);
 539
 540     return makeNode(kind::PLUS, m.begin(), m.end());
 541   }
 542
 543   typedef expr::NodeSelfIterator internal_iterator;
 544
 545   internal_iterator internalBegin() const {
 546     if(singleton()){
 547       return expr::NodeSelfIterator::self(getNode());
 548     }else{
 549       return getNode().begin();
 550     }
 551   }
 552
 553   internal_iterator internalEnd() const {
 554     if(singleton()){
 555       return expr::NodeSelfIterator::selfEnd(getNode());
 556     }else{
 557       return getNode().end();
 558     }
 559   }
 560
 561   bool singleton() const { return d_singleton; }
 562
 563 public:
 564   static bool isMember(TNode n) {
 565     if(Monomial::isMember(n)){
 566       return true;
 567     }else if(n.getKind() == kind::PLUS){
 568       Assert(n.getNumChildren() >= 2);
 569       for(Node::iterator curr = n.begin(), end = n.end(); curr != end;++curr){
 570         if(!Monomial::isMember(*curr)){
 571           return false;
 572         }
 573       }
 574       return true;
 575     } else {
 576       return false;
 577     }
 578   }
 579
 580   class iterator {
 581   private:
 582     internal_iterator d_iter;
 583
 584   public:
 585     explicit iterator(internal_iterator i) : d_iter(i) {}
 586
 587     inline Monomial operator*() {
 588       return Monomial::parseMonomial(*d_iter);
 589     }
 590
 591     bool operator==(const iterator& i) {
 592       return d_iter == i.d_iter;
 593     }
 594
 595     bool operator!=(const iterator& i) {
 596       return d_iter != i.d_iter;
 597     }
 598
 599     iterator operator++() {
 600       ++d_iter;
 601       return *this;
 602     }
 603
 604     iterator operator++(int) {
 605       return iterator(d_iter++);
 606     }
 607   };
 608
 609   iterator begin() const { return iterator(internalBegin()); }
 610   iterator end() const {  return iterator(internalEnd()); }
 611
 612   Polynomial(const Monomial& m):
 613     NodeWrapper(m.getNode()), d_singleton(true)
 614   {}
 615
 616   Polynomial(const std::vector<Monomial>& m):
 617     NodeWrapper(makePlusNode(m)), d_singleton(false)
 618   {
 619     Assert( m.size() >= 2);
 620     Assert( Monomial::isStrictlySorted(m) );
 621   }
 622
 623
 624   static Polynomial mkPolynomial(const std::vector<Monomial>& m) {
 625     if(m.size() == 0) {
 626       return Polynomial(Monomial::mkZero());
 627     } else if(m.size() == 1) {
 628       return Polynomial((*m.begin()));
 629     } else {
 630       return Polynomial(m);
 631     }
 632   }
 633
 634   static Polynomial parsePolynomial(Node n) {
 635     return Polynomial(n);
 636   }
 637
 638   static Polynomial mkZero() {
 639     return Polynomial(Monomial::mkZero());
 640   }
 641   static Polynomial mkOne() {
 642     return Polynomial(Monomial::mkOne());
 643   }
 644   bool isZero() const {
 645     return singleton() && (getHead().isZero());
 646   }
 647
 648   bool isConstant() const {
 649     return singleton() && (getHead().isConstant());
 650   }
 651
 652   bool containsConstant() const {
 653     return getHead().isConstant();
 654   }
 655
 656   Monomial getHead() const {
 657     return *(begin());
 658   }
 659
 660   Polynomial getTail() const {
 661     Assert(! singleton());
 662
 663     iterator tailStart = begin();
 664     ++tailStart;
 665     std::vector<Monomial> subrange;
 666     copy_range(tailStart, end(), subrange);
 667     return mkPolynomial(subrange);
 668   }
 669
 670   void printList() const {
 671     if(Debug.isOn("normal-form")){
 672       Debug("normal-form") << "start list" << std::endl;
 673       for(iterator i = begin(), oend = end(); i != oend; ++i) {
 674         const Monomial& m =*i;
 675         m.print();
 676       }
 677       Debug("normal-form") << "end list" << std::endl;
 678     }
 679   }
 680
 681   Polynomial operator+(const Polynomial& vl) const;
 682
 683   Polynomial operator*(const Monomial& mono) const;
 684
 685   Polynomial operator*(const Polynomial& poly) const;
 686
 687 };/* class Polynomial */
 688
 689
 690 class Comparison : public NodeWrapper {
 691 private:
 692   Kind oper;
 693   Polynomial left;
 694   Constant right;
 695
 696   static Node toNode(Kind k, const Polynomial& l, const Constant& r);
 697
 698   Comparison(TNode n, Kind k, const Polynomial& l, const Constant& r):
 699     NodeWrapper(n), oper(k), left(l), right(r)
 700   { }
 701 public:
 702   Comparison(bool val) :
 703     NodeWrapper(NodeManager::currentNM()->mkConst(val)),
 704     oper(kind::CONST_BOOLEAN),
 705     left(Polynomial::mkZero()),
 706     right(Constant::mkConstant(0))
 707   { }
 708
 709   Comparison(Kind k, const Polynomial& l, const Constant& r):
 710     NodeWrapper(toNode(k, l, r)), oper(k), left(l), right(r)
 711   {
 712     Assert(isRelationOperator(oper));
 713     Assert(!left.containsConstant());
 714     Assert(left.getHead().getConstant().isOne());
 715   }
 716
 717   static Comparison mkComparison(Kind k, const Polynomial& left, const Constant& right);
 718
 719   bool isBoolean() const {
 720     return (oper == kind::CONST_BOOLEAN);
 721   }
 722
 723   bool isNormalForm() const {
 724     if(isBoolean()) {
 725       return true;
 726     } else if(left.containsConstant()) {
 727       return false;
 728     } else if(left.getHead().getConstant().isOne()) {
 729       return true;
 730     } else {
 731       return false;
 732     }
 733   }
 734
 735   const Polynomial& getLeft() const { return left; }
 736   const Constant& getRight() const { return right; }
 737
 738   Comparison addConstant(const Constant& constant) const;
 739   Comparison multiplyConstant(const Constant& constant) const;
 740
 741   static Comparison parseNormalForm(TNode n);
 742
 743 };/* class Comparison */
 744
 745 }/* CVC4::theory::arith namespace */
 746 }/* CVC4::theory namespace */
 747 }/* CVC4 namespace */
 748
 749 #endif /* __CVC4__THEORY__ARITH__NORMAL_FORM_H */