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