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