src/expr/expr_template.h

   1 /*********************                                                        */
   2 /*! \file expr_template.h
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: Dejan Jovanovic
   6  ** Minor contributors (to current version): Liana Hadarean, Kshitij Bansal, Tim King, Christopher L. Conway
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2013  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief Public-facing expression interface.
  13  **
  14  ** Public-facing expression interface.
  15  **/
  16
  17 #include "cvc4_public.h"
  18
  19 // putting the constant-payload #includes up here allows circularity
  20 // (some of them may require a completely-defined Expr type).  This
  21 // way, those #includes can forward-declare some stuff to get Expr's
  22 // getConst<> template instantiations correct, and then #include
  23 // "expr.h" safely, then go on to completely declare their own stuff.
  24 ${includes}
  25
  26 #ifndef __CVC4__EXPR_H
  27 #define __CVC4__EXPR_H
  28
  29 #include <string>
  30 #include <iostream>
  31 #include <iterator>
  32 #include <stdint.h>
  33
  34 #include "util/exception.h"
  35 #include "util/language.h"
  36 #include "util/hash.h"
  37 #include "expr/options.h"
  38
  39 // This is a hack, but an important one: if there's an error, the
  40 // compiler directs the user to the template file instead of the
  41 // generated one.  We don't want the user to modify the generated one,
  42 // since it'll get overwritten on a later build.
  43 #line 44 "${template}"
  44
  45 namespace CVC4 {
  46
  47 // The internal expression representation
  48 template <bool ref_count>
  49 class NodeTemplate;
  50
  51 class NodeManager;
  52
  53 class Expr;
  54 class ExprManager;
  55 class SmtEngine;
  56 class Type;
  57 class TypeCheckingException;
  58 class TypeCheckingExceptionPrivate;
  59
  60 namespace expr {
  61   namespace pickle {
  62     class Pickler;
  63   }/* CVC4::expr::pickle namespace */
  64 }/* CVC4::expr namespace */
  65
  66 namespace prop {
  67   class TheoryProxy;
  68 }/* CVC4::prop namespace */
  69
  70 struct ExprManagerMapCollection;
  71
  72 struct ExprHashFunction;
  73
  74 namespace smt {
  75   class SmtEnginePrivate;
  76 }/* CVC4::smt namespace */
  77
  78 namespace expr {
  79   class CVC4_PUBLIC ExprSetDepth;
  80   class CVC4_PUBLIC ExprPrintTypes;
  81   class CVC4_PUBLIC ExprDag;
  82   class CVC4_PUBLIC ExprSetLanguage;
  83
  84   class ExportPrivate;
  85 }/* CVC4::expr namespace */
  86
  87 /**
  88  * Exception thrown in the case of type-checking errors.
  89  */
  90 class CVC4_PUBLIC TypeCheckingException : public Exception {
  91
  92   friend class SmtEngine;
  93   friend class smt::SmtEnginePrivate;
  94
  95 private:
  96
  97   /** The expression responsible for the error */
  98   Expr* d_expr;
  99
 100 protected:
 101
 102   TypeCheckingException() throw() : Exception() {}
 103   TypeCheckingException(ExprManager* em,
 104                         const TypeCheckingExceptionPrivate* exc) throw();
 105
 106 public:
 107
 108   TypeCheckingException(const Expr& expr, std::string message) throw();
 109
 110   /** Copy constructor */
 111   TypeCheckingException(const TypeCheckingException& t) throw();
 112
 113   /** Destructor */
 114   ~TypeCheckingException() throw();
 115
 116   /**
 117    * Get the Expr that caused the type-checking to fail.
 118    *
 119    * @return the expr
 120    */
 121   Expr getExpression() const throw();
 122
 123   /**
 124    * Returns the message corresponding to the type-checking failure.
 125    * We prefer toStream() to toString() because that keeps the expr-depth
 126    * and expr-language settings present in the stream.
 127    */
 128   void toStream(std::ostream& out) const throw();
 129
 130   friend class ExprManager;
 131 };/* class TypeCheckingException */
 132
 133 /**
 134  * Exception thrown in case of failure to export
 135  */
 136 class CVC4_PUBLIC ExportUnsupportedException : public Exception {
 137 public:
 138   ExportUnsupportedException() throw():
 139     Exception("export unsupported") {
 140   }
 141   ExportUnsupportedException(const char* msg) throw():
 142     Exception(msg) {
 143   }
 144 };/* class DatatypeExportUnsupportedException */
 145
 146 std::ostream& operator<<(std::ostream& out,
 147                          const TypeCheckingException& e) CVC4_PUBLIC;
 148
 149 /**
 150  * Output operator for expressions
 151  * @param out the stream to output to
 152  * @param e the expression to output
 153  * @return the stream
 154  */
 155 std::ostream& operator<<(std::ostream& out, const Expr& e) CVC4_PUBLIC;
 156
 157 // for hash_maps, hash_sets..
 158 struct ExprHashFunction {
 159   size_t operator()(CVC4::Expr e) const;
 160 };/* struct ExprHashFunction */
 161
 162 /**
 163  * Class encapsulating CVC4 expressions and methods for constructing new
 164  * expressions.
 165  */
 166 class CVC4_PUBLIC Expr {
 167
 168   /** The internal expression representation */
 169   NodeTemplate<true>* d_node;
 170
 171   /** The responsible expression manager */
 172   ExprManager* d_exprManager;
 173
 174   /**
 175    * Constructor for internal purposes.
 176    *
 177    * @param em the expression manager that handles this expression
 178    * @param node the actual expression node pointer
 179    */
 180   Expr(ExprManager* em, NodeTemplate<true>* node);
 181
 182 public:
 183
 184   /** Default constructor, makes a null expression. */
 185   Expr();
 186
 187   /**
 188    * Copy constructor, makes a copy of a given expression
 189    *
 190    * @param e the expression to copy
 191    */
 192   Expr(const Expr& e);
 193
 194   /** Destructor */
 195   ~Expr();
 196
 197   /**
 198    * Assignment operator, makes a copy of the given expression. If the
 199    * expression managers of the two expressions differ, the expression of
 200    * the given expression will be used.
 201    *
 202    * @param e the expression to assign
 203    * @return the reference to this expression after assignment
 204    */
 205   Expr& operator=(const Expr& e);
 206
 207   /**
 208    * Syntactic comparison operator. Returns true if expressions belong to the
 209    * same expression manager and are syntactically identical.
 210    *
 211    * @param e the expression to compare to
 212    * @return true if expressions are syntactically the same, false otherwise
 213    */
 214   bool operator==(const Expr& e) const;
 215
 216   /**
 217    * Syntactic disequality operator.
 218    *
 219    * @param e the expression to compare to
 220    * @return true if expressions differ syntactically, false otherwise
 221    */
 222   bool operator!=(const Expr& e) const;
 223
 224   /**
 225    * Order comparison operator. The only invariant on the order of expressions
 226    * is that the expressions that were created sooner will be smaller in the
 227    * ordering than all the expressions created later. Null expression is the
 228    * smallest element of the ordering. The behavior of the operator is
 229    * undefined if the expressions come from two different expression managers.
 230    *
 231    * @param e the expression to compare to
 232    * @return true if this expression is smaller than the given one
 233    */
 234   bool operator<(const Expr& e) const;
 235
 236   /**
 237    * Order comparison operator. The only invariant on the order of expressions
 238    * is that the expressions that were created sooner will be smaller in the
 239    * ordering than all the expressions created later. Null expression is the
 240    * smallest element of the ordering. The behavior of the operator is
 241    * undefined if the expressions come from two different expression managers.
 242    *
 243    * @param e the expression to compare to
 244    * @return true if this expression is greater than the given one
 245    */
 246   bool operator>(const Expr& e) const;
 247
 248   /**
 249    * Order comparison operator. The only invariant on the order of expressions
 250    * is that the expressions that were created sooner will be smaller in the
 251    * ordering than all the expressions created later. Null expression is the
 252    * smallest element of the ordering. The behavior of the operator is
 253    * undefined if the expressions come from two different expression managers.
 254    *
 255    * @param e the expression to compare to
 256    * @return true if this expression is smaller or equal to the given one
 257    */
 258   bool operator<=(const Expr& e) const { return !(*this > e); }
 259
 260   /**
 261    * Order comparison operator. The only invariant on the order of expressions
 262    * is that the expressions that were created sooner will be smaller in the
 263    * ordering than all the expressions created later. Null expression is the
 264    * smallest element of the ordering. The behavior of the operator is
 265    * undefined if the expressions come from two different expression managers.
 266    *
 267    * @param e the expression to compare to
 268    * @return true if this expression is greater or equal to the given one
 269    */
 270   bool operator>=(const Expr& e) const { return !(*this < e); }
 271
 272   /**
 273    * Get the ID of this expression (used for the comparison operators).
 274    *
 275    * @return an identifier uniquely identifying the value this
 276    * expression holds.
 277    */
 278   unsigned long getId() const;
 279
 280   /**
 281    * Returns the kind of the expression (AND, PLUS ...).
 282    *
 283    * @return the kind of the expression
 284    */
 285   Kind getKind() const;
 286
 287   /**
 288    * Returns the number of children of this expression.
 289    *
 290    * @return the number of children
 291    */
 292   size_t getNumChildren() const;
 293
 294   /**
 295    * Returns the i'th child of this expression.
 296    *
 297    * @param i the index of the child to retrieve
 298    * @return the child
 299    */
 300   Expr operator[](unsigned i) const;
 301
 302   /**
 303    * Returns the children of this Expr.
 304    */
 305   std::vector<Expr> getChildren() const {
 306     return std::vector<Expr>(begin(), end());
 307   }
 308
 309   /**
 310    * Returns the Boolean negation of this Expr.
 311    */
 312   Expr notExpr() const;
 313
 314   /**
 315    * Returns the conjunction of this expression and
 316    * the given expression.
 317    */
 318   Expr andExpr(const Expr& e) const;
 319
 320   /**
 321    * Returns the disjunction of this expression and
 322    * the given expression.
 323    */
 324   Expr orExpr(const Expr& e) const;
 325
 326   /**
 327    * Returns the exclusive disjunction of this expression and
 328    * the given expression.
 329    */
 330   Expr xorExpr(const Expr& e) const;
 331
 332   /**
 333    * Returns the Boolean equivalence of this expression and
 334    * the given expression.
 335    */
 336   Expr iffExpr(const Expr& e) const;
 337
 338   /**
 339    * Returns the implication of this expression and
 340    * the given expression.
 341    */
 342   Expr impExpr(const Expr& e) const;
 343
 344   /**
 345    * Returns the if-then-else expression with this expression
 346    * as the Boolean condition and the given expressions as
 347    * the "then" and "else" expressions.
 348    */
 349   Expr iteExpr(const Expr& then_e, const Expr& else_e) const;
 350
 351   /**
 352    * Iterator type for the children of an Expr.
 353    */
 354   class const_iterator : public std::iterator<std::input_iterator_tag, Expr> {
 355     ExprManager* d_exprManager;
 356     void* d_iterator;
 357
 358     explicit const_iterator(ExprManager*, void*);
 359
 360     friend class Expr;// to access void* constructor
 361
 362   public:
 363     const_iterator();
 364     const_iterator(const const_iterator& it);
 365     const_iterator& operator=(const const_iterator& it);
 366     ~const_iterator();
 367     bool operator==(const const_iterator& it) const;
 368     bool operator!=(const const_iterator& it) const {
 369       return !(*this == it);
 370     }
 371     const_iterator& operator++();
 372     const_iterator operator++(int);
 373     Expr operator*() const;
 374   };/* class Expr::const_iterator */
 375
 376   /**
 377    * Returns an iterator to the first child of this Expr.
 378    */
 379   const_iterator begin() const;
 380
 381   /**
 382    * Returns an iterator to one-off-the-last child of this Expr.
 383    */
 384   const_iterator end() const;
 385
 386   /**
 387    * Check if this is an expression that has an operator.
 388    *
 389    * @return true if this expression has an operator
 390    */
 391   bool hasOperator() const;
 392
 393   /**
 394    * Get the operator of this expression.
 395    *
 396    * @throws IllegalArgumentException if it has no operator
 397    * @return the operator of this expression
 398    */
 399   Expr getOperator() const;
 400
 401   /**
 402    * Get the type for this Expr and optionally do type checking.
 403    *
 404    * Initial type computation will be near-constant time if
 405    * type checking is not requested. Results are memoized, so that
 406    * subsequent calls to getType() without type checking will be
 407    * constant time.
 408    *
 409    * Initial type checking is linear in the size of the expression.
 410    * Again, the results are memoized, so that subsequent calls to
 411    * getType(), with or without type checking, will be constant
 412    * time.
 413    *
 414    * NOTE: A TypeCheckingException can be thrown even when type
 415    * checking is not requested. getType() will always return a
 416    * valid and correct type and, thus, an exception will be thrown
 417    * when no valid or correct type can be computed (e.g., if the
 418    * arguments to a bit-vector operation aren't bit-vectors). When
 419    * type checking is not requested, getType() will do the minimum
 420    * amount of checking required to return a valid result.
 421    *
 422    * @param check whether we should check the type as we compute it
 423    * (default: false)
 424    */
 425   Type getType(bool check = false) const throw (TypeCheckingException);
 426
 427   /**
 428    * Substitute "replacement" in for "e".
 429    */
 430   Expr substitute(Expr e, Expr replacement) const;
 431
 432   /**
 433    * Substitute "replacements" in for "exes".
 434    */
 435   Expr substitute(const std::vector<Expr> exes,
 436                   const std::vector<Expr>& replacements) const;
 437
 438   /**
 439    * Substitute pairs of (ex,replacement) from the given map.
 440    */
 441   Expr substitute(const std::hash_map<Expr, Expr, ExprHashFunction> map) const;
 442
 443   /**
 444    * Returns the string representation of the expression.
 445    * @return a string representation of the expression
 446    */
 447   std::string toString() const;
 448
 449   /**
 450    * Outputs the string representation of the expression to the stream.
 451    *
 452    * @param out the stream to serialize this expression to
 453    * @param toDepth the depth to which to print this expression, or -1
 454    * to print it fully
 455    * @param types set to true to ascribe types to the output
 456    * expressions (might break language compliance, but good for
 457    * debugging expressions)
 458    * @param dag the dagification threshold to use (0 == off)
 459    * @param language the language in which to output
 460    */
 461   void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1,
 462                 OutputLanguage language = language::output::LANG_AST) const;
 463
 464   /**
 465    * Check if this is a null expression.
 466    *
 467    * @return true if a null expression
 468    */
 469   bool isNull() const;
 470
 471   /**
 472    * Check if this is an expression representing a variable.
 473    *
 474    * @return true if a variable expression
 475    */
 476   bool isVariable() const;
 477
 478   /**
 479    * Check if this is an expression representing a constant.
 480    *
 481    * @return true if a constant expression
 482    */
 483   bool isConst() const;
 484
 485   /* A note on isAtomic() and isAtomicFormula() (in CVC3 parlance)..
 486    *
 487    * It has been decided for now to hold off on implementations of
 488    * these functions, as they may only be needed in CNF conversion,
 489    * where it's pointless to do a lazy isAtomic determination by
 490    * searching through the DAG, and storing it, since the result will
 491    * only be used once.  For more details see the 4/27/2010 CVC4
 492    * developer's meeting notes at:
 493    *
 494    * http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_April_27,_2010#isAtomic.28.29_and_isAtomicFormula.28.29
 495    */
 496   // bool containsDecision(); // is "atomic"
 497   // bool properlyContainsDecision(); // maybe not atomic but all children are
 498
 499   /** Extract a constant of type T */
 500   template <class T>
 501   const T& getConst() const;
 502
 503   /**
 504    * Returns the expression reponsible for this expression.
 505    */
 506   ExprManager* getExprManager() const;
 507
 508   /**
 509    * Maps this Expr into one for a different ExprManager, using
 510    * variableMap for the translation and extending it with any new
 511    * mappings.
 512    */
 513   Expr exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap, uint32_t flags = 0) const;
 514
 515   /**
 516    * IOStream manipulator to set the maximum depth of Exprs when
 517    * pretty-printing.  -1 means print to any depth.  E.g.:
 518    *
 519    *   // let a, b, c, and d be VARIABLEs
 520    *   Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d)))
 521    *   out << setdepth(3) << e;
 522    *
 523    * gives "(OR a b (AND c (NOT d)))", but
 524    *
 525    *   out << setdepth(1) << [same expr as above]
 526    *
 527    * gives "(OR a b (...))"
 528    */
 529   typedef expr::ExprSetDepth setdepth;
 530
 531   /**
 532    * IOStream manipulator to print type ascriptions or not.
 533    *
 534    *   // let a, b, c, and d be variables of sort U
 535    *   Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d)))
 536    *   out << printtypes(true) << e;
 537    *
 538    * gives "(OR a:U b:U (AND c:U (NOT d:U)))", but
 539    *
 540    *   out << printtypes(false) << [same expr as above]
 541    *
 542    * gives "(OR a b (AND c (NOT d)))"
 543    */
 544   typedef expr::ExprPrintTypes printtypes;
 545
 546   /**
 547    * IOStream manipulator to print expressions as a DAG (or not).
 548    */
 549   typedef expr::ExprDag dag;
 550
 551   /**
 552    * IOStream manipulator to set the output language for Exprs.
 553    */
 554   typedef expr::ExprSetLanguage setlanguage;
 555
 556   /**
 557    * Very basic pretty printer for Expr.
 558    * This is equivalent to calling e.getNode().printAst(...)
 559    * @param out output stream to print to.
 560    * @param indent number of spaces to indent the formula by.
 561    */
 562   void printAst(std::ostream& out, int indent = 0) const;
 563
 564 private:
 565
 566   /**
 567    * Pretty printer for use within gdb
 568    * This is not intended to be used outside of gdb.
 569    * This writes to the ostream Warning() and immediately flushes
 570    * the ostream.
 571    */
 572   void debugPrint();
 573
 574   /**
 575    * Returns the actual internal node.
 576    * @return the internal node
 577    */
 578   NodeTemplate<true> getNode() const throw();
 579
 580   /**
 581    * Returns the actual internal node as a TNode.
 582    * @return the internal node
 583    */
 584   NodeTemplate<false> getTNode() const throw();
 585
 586   // Friend to access the actual internal expr information and private methods
 587   friend class SmtEngine;
 588   friend class smt::SmtEnginePrivate;
 589   friend class ExprManager;
 590   friend class NodeManager;
 591   friend class TypeCheckingException;
 592   friend class expr::pickle::Pickler;
 593   friend class prop::TheoryProxy;
 594   friend class expr::ExportPrivate;
 595   friend std::ostream& CVC4::operator<<(std::ostream& out, const Expr& e);
 596   template <bool ref_count> friend class NodeTemplate;
 597
 598 };/* class Expr */
 599
 600 namespace expr {
 601
 602 /**
 603  * IOStream manipulator to set the maximum depth of Exprs when
 604  * pretty-printing.  -1 means print to any depth.  E.g.:
 605  *
 606  *   // let a, b, c, and d be VARIABLEs
 607  *   Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d)))
 608  *   out << setdepth(3) << e;
 609  *
 610  * gives "(OR a b (AND c (NOT d)))", but
 611  *
 612  *   out << setdepth(1) << [same expr as above]
 613  *
 614  * gives "(OR a b (...))".
 615  *
 616  * The implementation of this class serves two purposes; it holds
 617  * information about the depth setting (such as the index of the
 618  * allocated word in ios_base), and serves also as the manipulator
 619  * itself (as above).
 620  */
 621 class CVC4_PUBLIC ExprSetDepth {
 622   /**
 623    * The allocated index in ios_base for our depth setting.
 624    */
 625   static const int s_iosIndex;
 626
 627   /**
 628    * The default depth to print, for ostreams that haven't yet had a
 629    * setdepth() applied to them.
 630    */
 631   static const int s_defaultPrintDepth = -1;
 632
 633   /**
 634    * When this manipulator is used, the depth is stored here.
 635    */
 636   long d_depth;
 637
 638 public:
 639   /**
 640    * Construct a ExprSetDepth with the given depth.
 641    */
 642   ExprSetDepth(long depth) : d_depth(depth) {}
 643
 644   inline void applyDepth(std::ostream& out) {
 645     out.iword(s_iosIndex) = d_depth;
 646   }
 647
 648   static inline long getDepth(std::ostream& out) {
 649     long& l = out.iword(s_iosIndex);
 650     if(l == 0) {
 651       // set the default print depth on this ostream
 652       if(&Options::current() != NULL) {
 653         l = options::defaultExprDepth();
 654       }
 655       if(l == 0) {
 656         // if called from outside the library, we may not have options
 657         // available to us at this point (or perhaps the output language
 658         // is not set in Options).  Default to something reasonable, but
 659         // don't set "l" since that would make it "sticky" for this
 660         // stream.
 661         return s_defaultPrintDepth;
 662       }
 663     }
 664     return l;
 665   }
 666
 667   static inline void setDepth(std::ostream& out, long depth) {
 668     out.iword(s_iosIndex) = depth;
 669   }
 670
 671   /**
 672    * Set the expression depth on the output stream for the current
 673    * stack scope.  This makes sure the old depth is reset on the stream
 674    * after normal OR exceptional exit from the scope, using the RAII
 675    * C++ idiom.
 676    */
 677   class Scope {
 678     std::ostream& d_out;
 679     long d_oldDepth;
 680
 681   public:
 682
 683     inline Scope(std::ostream& out, long depth) :
 684       d_out(out),
 685       d_oldDepth(ExprSetDepth::getDepth(out)) {
 686       ExprSetDepth::setDepth(out, depth);
 687     }
 688
 689     inline ~Scope() {
 690       ExprSetDepth::setDepth(d_out, d_oldDepth);
 691     }
 692
 693   };/* class ExprSetDepth::Scope */
 694
 695 };/* class ExprSetDepth */
 696
 697 /**
 698  * IOStream manipulator to print type ascriptions or not.
 699  *
 700  *   // let a, b, c, and d be variables of sort U
 701  *   Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d)))
 702  *   out << e;
 703  *
 704  * gives "(OR a:U b:U (AND c:U (NOT d:U)))", but
 705  */
 706 class CVC4_PUBLIC ExprPrintTypes {
 707   /**
 708    * The allocated index in ios_base for our setting.
 709    */
 710   static const int s_iosIndex;
 711
 712   /**
 713    * When this manipulator is used, the setting is stored here.
 714    */
 715   bool d_printTypes;
 716
 717 public:
 718   /**
 719    * Construct a ExprPrintTypes with the given setting.
 720    */
 721   ExprPrintTypes(bool printTypes) : d_printTypes(printTypes) {}
 722
 723   inline void applyPrintTypes(std::ostream& out) {
 724     out.iword(s_iosIndex) = d_printTypes;
 725   }
 726
 727   static inline bool getPrintTypes(std::ostream& out) {
 728     return out.iword(s_iosIndex);
 729   }
 730
 731   static inline void setPrintTypes(std::ostream& out, bool printTypes) {
 732     out.iword(s_iosIndex) = printTypes;
 733   }
 734
 735   /**
 736    * Set the print-types state on the output stream for the current
 737    * stack scope.  This makes sure the old state is reset on the
 738    * stream after normal OR exceptional exit from the scope, using the
 739    * RAII C++ idiom.
 740    */
 741   class Scope {
 742     std::ostream& d_out;
 743     bool d_oldPrintTypes;
 744
 745   public:
 746
 747     inline Scope(std::ostream& out, bool printTypes) :
 748       d_out(out),
 749       d_oldPrintTypes(ExprPrintTypes::getPrintTypes(out)) {
 750       ExprPrintTypes::setPrintTypes(out, printTypes);
 751     }
 752
 753     inline ~Scope() {
 754       ExprPrintTypes::setPrintTypes(d_out, d_oldPrintTypes);
 755     }
 756
 757   };/* class ExprPrintTypes::Scope */
 758
 759 };/* class ExprPrintTypes */
 760
 761 /**
 762  * IOStream manipulator to print expressions as a dag (or not).
 763  */
 764 class CVC4_PUBLIC ExprDag {
 765   /**
 766    * The allocated index in ios_base for our setting.
 767    */
 768   static const int s_iosIndex;
 769
 770   /**
 771    * The default setting, for ostreams that haven't yet had a
 772    * dag() applied to them.
 773    */
 774   static const size_t s_defaultDag = 1;
 775
 776   /**
 777    * When this manipulator is used, the setting is stored here.
 778    */
 779   size_t d_dag;
 780
 781 public:
 782   /**
 783    * Construct a ExprDag with the given setting (dagification on or off).
 784    */
 785   explicit ExprDag(bool dag) : d_dag(dag ? 1 : 0) {}
 786
 787   /**
 788    * Construct a ExprDag with the given setting (letify only common
 789    * subexpressions that appear more than 'dag' times).  dag <= 0 means
 790    * don't dagify.
 791    */
 792   explicit ExprDag(int dag) : d_dag(dag < 0 ? 0 : dag) {}
 793
 794   inline void applyDag(std::ostream& out) {
 795     // (offset by one to detect whether default has been set yet)
 796     out.iword(s_iosIndex) = static_cast<long>(d_dag) + 1;
 797   }
 798
 799   static inline size_t getDag(std::ostream& out) {
 800     long& l = out.iword(s_iosIndex);
 801     if(l == 0) {
 802       // set the default dag setting on this ostream
 803       // (offset by one to detect whether default has been set yet)
 804       if(&Options::current() != NULL) {
 805         l = options::defaultDagThresh() + 1;
 806       }
 807       if(l == 0) {
 808         // if called from outside the library, we may not have options
 809         // available to us at this point (or perhaps the output language
 810         // is not set in Options).  Default to something reasonable, but
 811         // don't set "l" since that would make it "sticky" for this
 812         // stream.
 813         return s_defaultDag + 1;
 814       }
 815     }
 816     return static_cast<size_t>(l - 1);
 817   }
 818
 819   static inline void setDag(std::ostream& out, size_t dag) {
 820     // (offset by one to detect whether default has been set yet)
 821     out.iword(s_iosIndex) = static_cast<long>(dag) + 1;
 822   }
 823
 824   /**
 825    * Set the dag state on the output stream for the current
 826    * stack scope.  This makes sure the old state is reset on the
 827    * stream after normal OR exceptional exit from the scope, using the
 828    * RAII C++ idiom.
 829    */
 830   class Scope {
 831     std::ostream& d_out;
 832     size_t d_oldDag;
 833
 834   public:
 835
 836     inline Scope(std::ostream& out, size_t dag) :
 837       d_out(out),
 838       d_oldDag(ExprDag::getDag(out)) {
 839       ExprDag::setDag(out, dag);
 840     }
 841
 842     inline ~Scope() {
 843       ExprDag::setDag(d_out, d_oldDag);
 844     }
 845
 846   };/* class ExprDag::Scope */
 847
 848 };/* class ExprDag */
 849
 850 /**
 851  * IOStream manipulator to set the output language for Exprs.
 852  */
 853 class CVC4_PUBLIC ExprSetLanguage {
 854   /**
 855    * The allocated index in ios_base for our depth setting.
 856    */
 857   static const int s_iosIndex;
 858
 859   /**
 860    * The default language to use, for ostreams that haven't yet had a
 861    * setlanguage() applied to them and where the current Options
 862    * information isn't available.
 863    */
 864   static const int s_defaultOutputLanguage = language::output::LANG_AST;
 865
 866   /**
 867    * When this manipulator is used, the setting is stored here.
 868    */
 869   OutputLanguage d_language;
 870
 871 public:
 872   /**
 873    * Construct a ExprSetLanguage with the given setting.
 874    */
 875   ExprSetLanguage(OutputLanguage l) : d_language(l) {}
 876
 877   inline void applyLanguage(std::ostream& out) {
 878     // (offset by one to detect whether default has been set yet)
 879     out.iword(s_iosIndex) = int(d_language) + 1;
 880   }
 881
 882   static inline OutputLanguage getLanguage(std::ostream& out) {
 883     long& l = out.iword(s_iosIndex);
 884     if(l == 0) {
 885       // set the default language on this ostream
 886       // (offset by one to detect whether default has been set yet)
 887       if(&Options::current() != NULL) {
 888         l = options::outputLanguage() + 1;
 889       }
 890       if(l <= 0 || l > language::output::LANG_MAX) {
 891         // if called from outside the library, we may not have options
 892         // available to us at this point (or perhaps the output language
 893         // is not set in Options).  Default to something reasonable, but
 894         // don't set "l" since that would make it "sticky" for this
 895         // stream.
 896         return OutputLanguage(s_defaultOutputLanguage);
 897       }
 898     }
 899     return OutputLanguage(l - 1);
 900   }
 901
 902   static inline void setLanguage(std::ostream& out, OutputLanguage l) {
 903     // (offset by one to detect whether default has been set yet)
 904     out.iword(s_iosIndex) = int(l) + 1;
 905   }
 906
 907   /**
 908    * Set a language on the output stream for the current stack scope.
 909    * This makes sure the old language is reset on the stream after
 910    * normal OR exceptional exit from the scope, using the RAII C++
 911    * idiom.
 912    */
 913   class Scope {
 914     std::ostream& d_out;
 915     OutputLanguage d_oldLanguage;
 916
 917   public:
 918
 919     inline Scope(std::ostream& out, OutputLanguage language) :
 920       d_out(out),
 921       d_oldLanguage(ExprSetLanguage::getLanguage(out)) {
 922       ExprSetLanguage::setLanguage(out, language);
 923     }
 924
 925     inline ~Scope() {
 926       ExprSetLanguage::setLanguage(d_out, d_oldLanguage);
 927     }
 928
 929   };/* class ExprSetLanguage::Scope */
 930
 931 };/* class ExprSetLanguage */
 932
 933 }/* CVC4::expr namespace */
 934
 935 ${getConst_instantiations}
 936
 937 #line 938 "${template}"
 938
 939 namespace expr {
 940
 941 /**
 942  * Sets the default depth when pretty-printing a Expr to an ostream.
 943  * Use like this:
 944  *
 945  *   // let out be an ostream, e an Expr
 946  *   out << Expr::setdepth(n) << e << endl;
 947  *
 948  * The depth stays permanently (until set again) with the stream.
 949  */
 950 inline std::ostream& operator<<(std::ostream& out, ExprSetDepth sd) {
 951   sd.applyDepth(out);
 952   return out;
 953 }
 954
 955 /**
 956  * Sets the default print-types setting when pretty-printing an Expr
 957  * to an ostream.  Use like this:
 958  *
 959  *   // let out be an ostream, e an Expr
 960  *   out << Expr::printtypes(true) << e << endl;
 961  *
 962  * The setting stays permanently (until set again) with the stream.
 963  */
 964 inline std::ostream& operator<<(std::ostream& out, ExprPrintTypes pt) {
 965   pt.applyPrintTypes(out);
 966   return out;
 967 }
 968
 969 /**
 970  * Sets the default dag setting when pretty-printing a Expr to an ostream.
 971  * Use like this:
 972  *
 973  *   // let out be an ostream, e an Expr
 974  *   out << Expr::dag(true) << e << endl;
 975  *
 976  * The setting stays permanently (until set again) with the stream.
 977  */
 978 inline std::ostream& operator<<(std::ostream& out, ExprDag d) {
 979   d.applyDag(out);
 980   return out;
 981 }
 982
 983 /**
 984  * Sets the output language when pretty-printing a Expr to an ostream.
 985  * Use like this:
 986  *
 987  *   // let out be an ostream, e an Expr
 988  *   out << Expr::setlanguage(LANG_SMTLIB_V2) << e << endl;
 989  *
 990  * The setting stays permanently (until set again) with the stream.
 991  */
 992 inline std::ostream& operator<<(std::ostream& out, ExprSetLanguage l) {
 993   l.applyLanguage(out);
 994   return out;
 995 }
 996
 997 }/* CVC4::expr namespace */
 998
 999 inline size_t ExprHashFunction::operator()(CVC4::Expr e) const {
1000   return (size_t) e.getId();
1001 }
1002
1003 }/* CVC4 namespace */
1004
1005 #endif /* __CVC4__EXPR_H */