src/expr/expr_template.h

   1 /*********************                                                        */
   2 /*! \file expr_template.h
   3  ** \verbatim
   4  ** Original author: dejan
   5  ** Major contributors: mdeters
   6  ** Minor contributors (to current version): taking, cconway
   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 Public-facing expression interface.
  15  **
  16  ** Public-facing expression interface.
  17  **/
  18
  19 #include "cvc4_public.h"
  20
  21 #ifndef __CVC4__EXPR_H
  22 #define __CVC4__EXPR_H
  23
  24 #include "expr/type.h"
  25 #include <string>
  26 #include <iostream>
  27 #include <stdint.h>
  28
  29 ${includes}
  30
  31 // This is a hack, but an important one: if there's an error, the
  32 // compiler directs the user to the template file instead of the
  33 // generated one.  We don't want the user to modify the generated one,
  34 // since it'll get overwritten on a later build.
  35 #line 36 "${template}"
  36
  37 namespace CVC4 {
  38
  39 // The internal expression representation
  40 template <bool ref_count>
  41 class NodeTemplate;
  42
  43 class Expr;
  44
  45 namespace expr {
  46   class CVC4_PUBLIC ExprSetDepth;
  47   class CVC4_PUBLIC ExprPrintTypes;
  48 }/* CVC4::expr namespace */
  49
  50 /**
  51  * Exception thrown in the case of type-checking errors.
  52  */
  53 class CVC4_PUBLIC TypeCheckingException : public Exception {
  54
  55 private:
  56
  57   /** The expression responsible for the error */
  58   Expr* d_expr;
  59
  60 protected:
  61
  62   TypeCheckingException(): Exception() {}
  63   TypeCheckingException(const Expr& expr, std::string message);
  64
  65 public:
  66
  67   /** Copy constructor */
  68   TypeCheckingException(const TypeCheckingException& t);
  69
  70   /** Destructor */
  71   ~TypeCheckingException() throw ();
  72
  73   /**
  74    * Get the Expr that caused the type-checking to fail.
  75    * @return the expr
  76    */
  77   Expr getExpression() const;
  78
  79   /** Returns the message corresponding to the type-checking failure */
  80   std::string toString() const;
  81
  82   friend class ExprManager;
  83 };
  84
  85 /**
  86  * Class encapsulating CVC4 expressions and methods for constructing new
  87  * expressions.
  88  */
  89 class CVC4_PUBLIC Expr {
  90 protected:
  91
  92   /** The internal expression representation */
  93   NodeTemplate<true>* d_node;
  94
  95   /** The responsible expression manager */
  96   ExprManager* d_exprManager;
  97
  98   /**
  99    * Constructor for internal purposes.
 100    * @param em the expression manager that handles this expression
 101    * @param node the actual expression node pointer
 102    */
 103   Expr(ExprManager* em, NodeTemplate<true>* node);
 104
 105 public:
 106
 107   /** Default constructor, makes a null expression. */
 108   Expr();
 109
 110   /**
 111    * Copy constructor, makes a copy of a given expression
 112    * @param e the expression to copy
 113    */
 114   Expr(const Expr& e);
 115
 116   /**
 117    * Initialize from an integer. Fails if the integer is not 0.
 118    * NOTE: This is here purely to support the auto-initialization
 119    * behavior of the ANTLR3 C backend. Should be removed if future
 120    * versions of ANTLR fix the problem.
 121    */
 122   Expr(uintptr_t n);
 123
 124   /** Destructor */
 125   ~Expr();
 126
 127   /**
 128    * Assignment operator, makes a copy of the given expression. If the
 129    * expression managers of the two expressions differ, the expression of
 130    * the given expression will be used.
 131    * @param e the expression to assign
 132    * @return the reference to this expression after assignment
 133    */
 134   Expr& operator=(const Expr& e);
 135
 136   /**
 137    * Syntactic comparison operator. Returns true if expressions belong to the
 138    * same expression manager and are syntactically identical.
 139    * @param e the expression to compare to
 140    * @return true if expressions are syntactically the same, false otherwise
 141    */
 142   bool operator==(const Expr& e) const;
 143
 144   /**
 145    * Syntactic dis-equality operator.
 146    * @param e the expression to compare to
 147    * @return true if expressions differ syntactically, false otherwise
 148    */
 149   bool operator!=(const Expr& e) const;
 150
 151   /**
 152    * Order comparison operator. The only invariant on the order of expressions
 153    * is that the expressions that were created sooner will be smaller in the
 154    * ordering than all the expressions created later. Null expression is the
 155    * smallest element of the ordering. The behavior of the operator is
 156    * undefined if the expressions come from two different expression managers.
 157    * @param e the expression to compare to
 158    * @return true if this expression is smaller than the given one
 159    */
 160   bool operator<(const Expr& e) const;
 161
 162   /**
 163    * Order comparison operator. The only invariant on the order of expressions
 164    * is that the expressions that were created sooner will be smaller in the
 165    * ordering than all the expressions created later. Null expression is the
 166    * smallest element of the ordering. The behavior of the operator is
 167    * undefined if the expressions come from two different expression managers.
 168    * @param e the expression to compare to
 169    * @return true if this expression is greater than the given one
 170    */
 171   bool operator>(const Expr& e) const;
 172
 173   /**
 174    * Order comparison operator. The only invariant on the order of expressions
 175    * is that the expressions that were created sooner will be smaller in the
 176    * ordering than all the expressions created later. Null expression is the
 177    * smallest element of the ordering. The behavior of the operator is
 178    * undefined if the expressions come from two different expression managers.
 179    * @param e the expression to compare to
 180    * @return true if this expression is smaller or equal to the given one
 181    */
 182   bool operator<=(const Expr& e) const { return !(*this > e); }
 183
 184   /**
 185    * Order comparison operator. The only invariant on the order of expressions
 186    * is that the expressions that were created sooner will be smaller in the
 187    * ordering than all the expressions created later. Null expression is the
 188    * smallest element of the ordering. The behavior of the operator is
 189    * undefined if the expressions come from two different expression managers.
 190    * @param e the expression to compare to
 191    * @return true if this expression is greater or equal to the given one
 192    */
 193   bool operator>=(const Expr& e) const { return !(*this < e); }
 194
 195   /**
 196    * Returns the kind of the expression (AND, PLUS ...).
 197    * @return the kind of the expression
 198    */
 199   Kind getKind() const;
 200
 201   /**
 202    * Returns the number of children of this expression.
 203    * @return the number of children
 204    */
 205   size_t getNumChildren() const;
 206
 207   /**
 208    * Returns the i'th child of this expression.
 209    * @param i the index of the child to retrieve
 210    * @return the child
 211    */
 212   Expr getChild(unsigned int i) const;
 213
 214   /**
 215    * Check if this is an expression that has an operator.
 216    * @return true if this expression has an operator
 217    */
 218   bool hasOperator() const;
 219
 220   /**
 221    * Get the operator of this expression.
 222    * @throws IllegalArgumentException if it has no operator
 223    * @return the operator of this expression
 224    */
 225   Expr getOperator() const;
 226
 227   /**
 228    * Get the type for this Expr and optionally do type checking.
 229    *
 230    * Initial type computation will be near-constant time if
 231    * type checking is not requested. Results are memoized, so that
 232    * subsequent calls to getType() without type checking will be
 233    * constant time.
 234    *
 235    * Initial type checking is linear in the size of the expression.
 236    * Again, the results are memoized, so that subsequent calls to
 237    * getType(), with or without type checking, will be constant
 238    * time.
 239    *
 240    * NOTE: A TypeCheckingException can be thrown even when type
 241    * checking is not requested. getType() will always return a
 242    * valid and correct type and, thus, an exception will be thrown
 243    * when no valid or correct type can be computed (e.g., if the
 244    * arguments to a bit-vector operation aren't bit-vectors). When
 245    * type checking is not requested, getType() will do the minimum
 246    * amount of checking required to return a valid result.
 247    *
 248    * @param check whether we should check the type as we compute it
 249    * (default: false)
 250    */
 251   Type getType(bool check = false) const throw (TypeCheckingException);
 252
 253   /**
 254    * Returns the string representation of the expression.
 255    * @return a string representation of the expression
 256    */
 257   std::string toString() const;
 258
 259   /**
 260    * Outputs the string representation of the expression to the stream.
 261    * @param out the output stream
 262    */
 263   void toStream(std::ostream& out, int depth = -1, bool types = false) const;
 264
 265   /**
 266    * Check if this is a null expression.
 267    * @return true if a null expression
 268    */
 269   bool isNull() const;
 270
 271   /**
 272    * Check if this is a null expression.
 273    * @return true if NOT a null expression
 274    */
 275   operator bool() const;
 276
 277   /**
 278    * Check if this is an expression representing a constant.
 279    * @return true if a constant expression
 280    */
 281   bool isConst() const;
 282
 283   /* A note on isAtomic() and isAtomicFormula() (in CVC3 parlance)..
 284    *
 285    * It has been decided for now to hold off on implementations of
 286    * these functions, as they may only be needed in CNF conversion,
 287    * where it's pointless to do a lazy isAtomic determination by
 288    * searching through the DAG, and storing it, since the result will
 289    * only be used once.  For more details see the 4/27/2010 CVC4
 290    * developer's meeting notes at:
 291    *
 292    * http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_April_27,_2010#isAtomic.28.29_and_isAtomicFormula.28.29
 293    */
 294   // bool containsDecision(); // is "atomic"
 295   // bool properlyContainsDecision(); // maybe not atomic but all children are
 296
 297   /** Extract a constant of type T */
 298   template <class T>
 299   const T& getConst() const;
 300
 301   /**
 302    * Returns the expression reponsible for this expression.
 303    */
 304   ExprManager* getExprManager() const;
 305
 306   /**
 307    * IOStream manipulator to set the maximum depth of Exprs when
 308    * pretty-printing.  -1 means print to any depth.  E.g.:
 309    *
 310    *   // let a, b, c, and d be VARIABLEs
 311    *   Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d)))
 312    *   out << setdepth(3) << e;
 313    *
 314    * gives "(OR a b (AND c (NOT d)))", but
 315    *
 316    *   out << setdepth(1) << [same expr as above]
 317    *
 318    * gives "(OR a b (...))"
 319    */
 320   typedef expr::ExprSetDepth setdepth;
 321
 322   /**
 323    * IOStream manipulator to print type ascriptions or not.
 324    *
 325    *   // let a, b, c, and d be variables of sort U
 326    *   Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d)))
 327    *   out << e;
 328    *
 329    * gives "(OR a:U b:U (AND c:U (NOT d:U)))", but
 330    */
 331   typedef expr::ExprPrintTypes printtypes;
 332
 333   /**
 334    * Very basic pretty printer for Expr.
 335    * This is equivalent to calling e.getNode().printAst(...)
 336    * @param out output stream to print to.
 337    * @param indent number of spaces to indent the formula by.
 338    */
 339   void printAst(std::ostream& out, int indent = 0) const;
 340
 341 private:
 342
 343   /**
 344    * Pretty printer for use within gdb
 345    * This is not intended to be used outside of gdb.
 346    * This writes to the ostream Warning() and immediately flushes
 347    * the ostream.
 348    */
 349   void debugPrint();
 350
 351 protected:
 352
 353   /**
 354    * Returns the actual internal node.
 355    * @return the internal node
 356    */
 357   NodeTemplate<true> getNode() const;
 358
 359   // Friend to access the actual internal expr information and private methods
 360   friend class SmtEngine;
 361   friend class ExprManager;
 362 };
 363
 364 /**
 365  * Output operator for expressions
 366  * @param out the stream to output to
 367  * @param e the expression to output
 368  * @return the stream
 369  */
 370 std::ostream& operator<<(std::ostream& out, const Expr& e) CVC4_PUBLIC;
 371
 372 /**
 373  * Extending the expression with the capability to construct Boolean
 374  * expressions.
 375  */
 376 class CVC4_PUBLIC BoolExpr : public Expr {
 377
 378 public:
 379
 380   /** Default constructor, makes a null expression */
 381   BoolExpr();
 382
 383   /**
 384    * Convert an expression to a Boolean expression
 385    */
 386   BoolExpr(const Expr& e);
 387
 388   /**
 389    * Negate this expression.
 390    * @return the logical negation of this expression.
 391    */
 392   BoolExpr notExpr() const;
 393
 394   /**
 395    * Conjunct the given expression to this expression.
 396    * @param e the expression to conjunct
 397    * @return the conjunction of this expression and e
 398    */
 399   BoolExpr andExpr(const BoolExpr& e) const;
 400
 401   /**
 402    * Disjunct the given expression to this expression.
 403    * @param e the expression to disjunct
 404    * @return the disjunction of this expression and e
 405    */
 406   BoolExpr orExpr(const BoolExpr& e) const;
 407
 408   /**
 409    * Make an exclusive or expression out of this expression and the given
 410    * expression.
 411    * @param e the right side of the xor
 412    * @return the xor of this expression and e
 413    */
 414   BoolExpr xorExpr(const BoolExpr& e) const;
 415
 416   /**
 417    * Make an equivalence expression out of this expression and the given
 418    * expression.
 419    * @param e the right side of the equivalence
 420    * @return the equivalence expression
 421    */
 422   BoolExpr iffExpr(const BoolExpr& e) const;
 423
 424   /**
 425    * Make an implication expression out of this expression and the given
 426    * expression.
 427    * @param e the right side of the equivalence
 428    * @return the equivalence expression
 429    */
 430   BoolExpr impExpr(const BoolExpr& e) const;
 431
 432   /**
 433    * Make a Boolean if-then-else expression using this expression as the
 434    * condition, and given the then and else parts
 435    * @param then_e the then branch expression
 436    * @param else_e the else branch expression
 437    * @return the if-then-else expression
 438    */
 439   BoolExpr iteExpr(const BoolExpr& then_e, const BoolExpr& else_e) const;
 440
 441   /**
 442    * Make a term if-then-else expression using this expression as the
 443    * condition, and given the then and else parts
 444    * @param then_e the then branch expression
 445    * @param else_e the else branch expression
 446    * @return the if-then-else expression
 447    */
 448   Expr iteExpr(const Expr& then_e, const Expr& else_e) const;
 449 };
 450
 451 namespace expr {
 452
 453 /**
 454  * IOStream manipulator to set the maximum depth of Exprs when
 455  * pretty-printing.  -1 means print to any depth.  E.g.:
 456  *
 457  *   // let a, b, c, and d be VARIABLEs
 458  *   Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d)))
 459  *   out << setdepth(3) << e;
 460  *
 461  * gives "(OR a b (AND c (NOT d)))", but
 462  *
 463  *   out << setdepth(1) << [same expr as above]
 464  *
 465  * gives "(OR a b (...))".
 466  *
 467  * The implementation of this class serves two purposes; it holds
 468  * information about the depth setting (such as the index of the
 469  * allocated word in ios_base), and serves also as the manipulator
 470  * itself (as above).
 471  */
 472 class CVC4_PUBLIC ExprSetDepth {
 473   /**
 474    * The allocated index in ios_base for our depth setting.
 475    */
 476   static const int s_iosIndex;
 477
 478   /**
 479    * The default depth to print, for ostreams that haven't yet had a
 480    * setdepth() applied to them.
 481    */
 482   static const int s_defaultPrintDepth = 3;
 483
 484   /**
 485    * When this manipulator is used, the depth is stored here.
 486    */
 487   long d_depth;
 488
 489 public:
 490   /**
 491    * Construct a ExprSetDepth with the given depth.
 492    */
 493   ExprSetDepth(long depth) : d_depth(depth) {}
 494
 495   inline void applyDepth(std::ostream& out) {
 496     out.iword(s_iosIndex) = d_depth;
 497   }
 498
 499   static inline long getDepth(std::ostream& out) {
 500     long& l = out.iword(s_iosIndex);
 501     if(l == 0) {
 502       // set the default print depth on this ostream
 503       l = s_defaultPrintDepth;
 504     }
 505     return l;
 506   }
 507
 508   static inline void setDepth(std::ostream& out, long depth) {
 509     out.iword(s_iosIndex) = depth;
 510   }
 511 };
 512
 513 /**
 514  * IOStream manipulator to print type ascriptions or not.
 515  *
 516  *   // let a, b, c, and d be variables of sort U
 517  *   Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d)))
 518  *   out << e;
 519  *
 520  * gives "(OR a:U b:U (AND c:U (NOT d:U)))", but
 521  */
 522 class CVC4_PUBLIC ExprPrintTypes {
 523   /**
 524    * The allocated index in ios_base for our depth setting.
 525    */
 526   static const int s_iosIndex;
 527
 528   /**
 529    * The default depth to print, for ostreams that haven't yet had a
 530    * setdepth() applied to them.
 531    */
 532   static const int s_defaultPrintTypes = false;
 533
 534   /**
 535    * When this manipulator is used, the setting is stored here.
 536    */
 537   bool d_printTypes;
 538
 539 public:
 540   /**
 541    * Construct a ExprPrintTypes with the given setting.
 542    */
 543   ExprPrintTypes(bool printTypes) : d_printTypes(printTypes) {}
 544
 545   inline void applyPrintTypes(std::ostream& out) {
 546     out.iword(s_iosIndex) = d_printTypes;
 547   }
 548
 549   static inline bool getPrintTypes(std::ostream& out) {
 550     return out.iword(s_iosIndex);
 551   }
 552
 553   static inline void setPrintTypes(std::ostream& out, bool printTypes) {
 554     out.iword(s_iosIndex) = printTypes;
 555   }
 556 };
 557
 558 }/* CVC4::expr namespace */
 559
 560 ${getConst_instantiations}
 561
 562 #line 388 "${template}"
 563
 564 namespace expr {
 565
 566 /**
 567  * Sets the default print-types setting when pretty-printing an Expr
 568  * to an ostream.  Use like this:
 569  *
 570  *   // let out be an ostream, e an Expr
 571  *   out << Expr::setdepth(n) << e << endl;
 572  *
 573  * The depth stays permanently (until set again) with the stream.
 574  */
 575 inline std::ostream& operator<<(std::ostream& out, ExprSetDepth sd) {
 576   sd.applyDepth(out);
 577   return out;
 578 }
 579
 580 /**
 581  * Sets the default depth when pretty-printing a Expr to an ostream.
 582  * Use like this:
 583  *
 584  *   // let out be an ostream, e an Expr
 585  *   out << Expr::setprinttypes(true) << e << endl;
 586  *
 587  * The setting stays permanently (until set again) with the stream.
 588  */
 589 inline std::ostream& operator<<(std::ostream& out, ExprPrintTypes pt) {
 590   pt.applyPrintTypes(out);
 591   return out;
 592 }
 593
 594 }/* CVC4::expr namespace */
 595
 596 }/* CVC4 namespace */
 597
 598 #endif /* __CVC4__EXPR_H */