cvc4-1.4
expr.h
Go to the documentation of this file.
1 /********************* */
14 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
15 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
16 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
17 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
18 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
19 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
20 
21 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
22 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
23 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
24 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
25 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
26 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
27 
28 /* Edit the template file instead: */
29 /* /builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/expr/expr_template.h */
30 
31 /********************* */
47 #include "cvc4_public.h"
48 
49 // putting the constant-payload #includes up here allows circularity
50 // (some of them may require a completely-defined Expr type). This
51 // way, those #includes can forward-declare some stuff to get Expr's
52 // getConst<> template instantiations correct, and then #include
53 // "expr.h" safely, then go on to completely declare their own stuff.
54 
56 #include "util/abstract_value.h"
57 #include "expr/kind.h"
58 #include "util/chain.h"
59 #include "expr/kind.h"
60 #include "util/predicate.h"
61 #include "util/bool.h"
62 #include "util/divisible.h"
63 #include "util/subrange_bound.h"
64 #include "util/rational.h"
65 #include "util/bitvector.h"
66 #include "util/bitvector.h"
67 #include "util/bitvector.h"
68 #include "util/bitvector.h"
69 #include "util/bitvector.h"
70 #include "util/bitvector.h"
71 #include "util/bitvector.h"
72 #include "util/bitvector.h"
73 #include "util/bitvector.h"
74 #include "util/bitvector.h"
75 #include "util/array_store_all.h"
76 #include "util/datatype.h"
77 #include "util/ascription_type.h"
78 #include "util/tuple.h"
79 #include "util/tuple.h"
80 #include "util/record.h"
81 #include "util/record.h"
82 #include "util/record.h"
83 #include "util/emptyset.h"
84 #include "util/regexp.h"
85 #include "util/regexp.h"
86 
87 #ifndef __CVC4__EXPR_H
88 #define __CVC4__EXPR_H
89 
90 #include <string>
91 #include <iostream>
92 #include <iterator>
93 #include <stdint.h>
94 
95 #include "util/exception.h"
96 #include "util/language.h"
97 #include "util/hash.h"
98 #include "expr/options.h"
99 
100 // This is a hack, but an important one: if there's an error, the
101 // compiler directs the user to the template file instead of the
102 // generated one. We don't want the user to modify the generated one,
103 // since it'll get overwritten on a later build.
104 #line 44 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/expr/expr_template.h"
105 
106 namespace CVC4 {
107 
108 // The internal expression representation
109 template <bool ref_count>
110 class NodeTemplate;
111 
112 class NodeManager;
113 
114 class Expr;
115 class ExprManager;
116 class SmtEngine;
117 class Type;
118 class TypeCheckingException;
119 class TypeCheckingExceptionPrivate;
120 
121 namespace expr {
122  namespace pickle {
123  class Pickler;
124  }/* CVC4::expr::pickle namespace */
125 }/* CVC4::expr namespace */
126 
127 namespace prop {
128  class TheoryProxy;
129 }/* CVC4::prop namespace */
130 
131 struct ExprManagerMapCollection;
132 
133 struct ExprHashFunction;
134 
135 namespace smt {
136  class SmtEnginePrivate;
137 }/* CVC4::smt namespace */
138 
139 namespace expr {
140  class CVC4_PUBLIC ExprSetDepth;
141  class CVC4_PUBLIC ExprPrintTypes;
142  class CVC4_PUBLIC ExprDag;
143  class CVC4_PUBLIC ExprSetLanguage;
144 
145  class ExportPrivate;
146 }/* CVC4::expr namespace */
147 
152 
153  friend class SmtEngine;
154  friend class smt::SmtEnginePrivate;
155 
156 private:
157 
159  Expr* d_expr;
160 
161 protected:
162 
165  const TypeCheckingExceptionPrivate* exc) throw();
166 
167 public:
168 
169  TypeCheckingException(const Expr& expr, std::string message) throw();
170 
173 
175  ~TypeCheckingException() throw();
176 
182  Expr getExpression() const throw();
183 
189  void toStream(std::ostream& out) const throw();
190 
191  friend class ExprManager;
192 };/* class TypeCheckingException */
193 
198 public:
200  Exception("export unsupported") {
201  }
202  ExportUnsupportedException(const char* msg) throw():
203  Exception(msg) {
204  }
205 };/* class DatatypeExportUnsupportedException */
206 
207 std::ostream& operator<<(std::ostream& out,
209 
216 std::ostream& operator<<(std::ostream& out, const Expr& e) CVC4_PUBLIC;
217 
218 // for hash_maps, hash_sets..
220  size_t operator()(CVC4::Expr e) const;
221 };/* struct ExprHashFunction */
222 
227 class CVC4_PUBLIC Expr {
228 
230  NodeTemplate<true>* d_node;
231 
233  ExprManager* d_exprManager;
234 
241  Expr(ExprManager* em, NodeTemplate<true>* node);
242 
243 public:
244 
246  Expr();
247 
253  Expr(const Expr& e);
254 
256  ~Expr();
257 
266  Expr& operator=(const Expr& e);
267 
275  bool operator==(const Expr& e) const;
276 
283  bool operator!=(const Expr& e) const;
284 
295  bool operator<(const Expr& e) const;
296 
307  bool operator>(const Expr& e) const;
308 
319  bool operator<=(const Expr& e) const { return !(*this > e); }
320 
331  bool operator>=(const Expr& e) const { return !(*this < e); }
332 
339  unsigned long getId() const;
340 
346  Kind getKind() const;
347 
353  size_t getNumChildren() const;
354 
361  Expr operator[](unsigned i) const;
362 
366  std::vector<Expr> getChildren() const {
367  return std::vector<Expr>(begin(), end());
368  }
369 
373  Expr notExpr() const;
374 
379  Expr andExpr(const Expr& e) const;
380 
385  Expr orExpr(const Expr& e) const;
386 
391  Expr xorExpr(const Expr& e) const;
392 
397  Expr iffExpr(const Expr& e) const;
398 
403  Expr impExpr(const Expr& e) const;
404 
410  Expr iteExpr(const Expr& then_e, const Expr& else_e) const;
411 
415  class const_iterator : public std::iterator<std::input_iterator_tag, Expr> {
416  ExprManager* d_exprManager;
417  void* d_iterator;
418 
419  explicit const_iterator(ExprManager*, void*);
420 
421  friend class Expr;// to access void* constructor
422 
423  public:
424  const_iterator();
425  const_iterator(const const_iterator& it);
426  const_iterator& operator=(const const_iterator& it);
427  ~const_iterator();
428  bool operator==(const const_iterator& it) const;
429  bool operator!=(const const_iterator& it) const {
430  return !(*this == it);
431  }
434  Expr operator*() const;
435  };/* class Expr::const_iterator */
436 
440  const_iterator begin() const;
441 
445  const_iterator end() const;
446 
452  bool hasOperator() const;
453 
460  Expr getOperator() const;
461 
486  Type getType(bool check = false) const throw (TypeCheckingException);
487 
491  Expr substitute(Expr e, Expr replacement) const;
492 
496  Expr substitute(const std::vector<Expr> exes,
497  const std::vector<Expr>& replacements) const;
498 
502  Expr substitute(const std::hash_map<Expr, Expr, ExprHashFunction> map) const;
503 
508  std::string toString() const;
509 
522  void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1,
524 
530  bool isNull() const;
531 
537  bool isVariable() const;
538 
544  bool isConst() const;
545 
546  /* A note on isAtomic() and isAtomicFormula() (in CVC3 parlance)..
547  *
548  * It has been decided for now to hold off on implementations of
549  * these functions, as they may only be needed in CNF conversion,
550  * where it's pointless to do a lazy isAtomic determination by
551  * searching through the DAG, and storing it, since the result will
552  * only be used once. For more details see the 4/27/2010 CVC4
553  * developer's meeting notes at:
554  *
555  * http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_April_27,_2010#isAtomic.28.29_and_isAtomicFormula.28.29
556  */
557  // bool containsDecision(); // is "atomic"
558  // bool properlyContainsDecision(); // maybe not atomic but all children are
559 
561  template <class T>
562  const T& getConst() const;
563 
567  ExprManager* getExprManager() const;
568 
574  Expr exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap, uint32_t flags = 0) const;
575 
591 
606 
611 
616 
623  void printAst(std::ostream& out, int indent = 0) const;
624 
625 private:
626 
633  void debugPrint();
634 
639  NodeTemplate<true> getNode() const throw();
640 
645  NodeTemplate<false> getTNode() const throw();
646 
647  // Friend to access the actual internal expr information and private methods
648  friend class SmtEngine;
649  friend class smt::SmtEnginePrivate;
650  friend class ExprManager;
651  friend class NodeManager;
652  friend class TypeCheckingException;
653  friend class expr::pickle::Pickler;
654  friend class prop::TheoryProxy;
655  friend class expr::ExportPrivate;
656  friend std::ostream& CVC4::operator<<(std::ostream& out, const Expr& e);
657  template <bool ref_count> friend class NodeTemplate;
658 
659 };/* class Expr */
660 
661 namespace expr {
662 
682 class CVC4_PUBLIC ExprSetDepth {
686  static const int s_iosIndex;
687 
692  static const int s_defaultPrintDepth = -1;
693 
697  long d_depth;
698 
699 public:
703  ExprSetDepth(long depth) : d_depth(depth) {}
704 
705  inline void applyDepth(std::ostream& out) {
706  out.iword(s_iosIndex) = d_depth;
707  }
708 
709  static inline long getDepth(std::ostream& out) {
710  long& l = out.iword(s_iosIndex);
711  if(l == 0) {
712  // set the default print depth on this ostream
713  if(&Options::current() != NULL) {
715  }
716  if(l == 0) {
717  // if called from outside the library, we may not have options
718  // available to us at this point (or perhaps the output language
719  // is not set in Options). Default to something reasonable, but
720  // don't set "l" since that would make it "sticky" for this
721  // stream.
722  return s_defaultPrintDepth;
723  }
724  }
725  return l;
726  }
727 
728  static inline void setDepth(std::ostream& out, long depth) {
729  out.iword(s_iosIndex) = depth;
730  }
731 
738  class Scope {
739  std::ostream& d_out;
740  long d_oldDepth;
741 
742  public:
743 
744  inline Scope(std::ostream& out, long depth) :
745  d_out(out),
746  d_oldDepth(ExprSetDepth::getDepth(out)) {
747  ExprSetDepth::setDepth(out, depth);
748  }
749 
750  inline ~Scope() {
751  ExprSetDepth::setDepth(d_out, d_oldDepth);
752  }
753 
754  };/* class ExprSetDepth::Scope */
755 
756 };/* class ExprSetDepth */
757 
767 class CVC4_PUBLIC ExprPrintTypes {
771  static const int s_iosIndex;
772 
776  bool d_printTypes;
777 
778 public:
782  ExprPrintTypes(bool printTypes) : d_printTypes(printTypes) {}
783 
784  inline void applyPrintTypes(std::ostream& out) {
785  out.iword(s_iosIndex) = d_printTypes;
786  }
787 
788  static inline bool getPrintTypes(std::ostream& out) {
789  return out.iword(s_iosIndex);
790  }
791 
792  static inline void setPrintTypes(std::ostream& out, bool printTypes) {
793  out.iword(s_iosIndex) = printTypes;
794  }
795 
802  class Scope {
803  std::ostream& d_out;
804  bool d_oldPrintTypes;
805 
806  public:
807 
808  inline Scope(std::ostream& out, bool printTypes) :
809  d_out(out),
810  d_oldPrintTypes(ExprPrintTypes::getPrintTypes(out)) {
811  ExprPrintTypes::setPrintTypes(out, printTypes);
812  }
813 
814  inline ~Scope() {
815  ExprPrintTypes::setPrintTypes(d_out, d_oldPrintTypes);
816  }
817 
818  };/* class ExprPrintTypes::Scope */
819 
820 };/* class ExprPrintTypes */
821 
825 class CVC4_PUBLIC ExprDag {
829  static const int s_iosIndex;
830 
835  static const size_t s_defaultDag = 1;
836 
840  size_t d_dag;
841 
842 public:
846  explicit ExprDag(bool dag) : d_dag(dag ? 1 : 0) {}
847 
853  explicit ExprDag(int dag) : d_dag(dag < 0 ? 0 : dag) {}
854 
855  inline void applyDag(std::ostream& out) {
856  // (offset by one to detect whether default has been set yet)
857  out.iword(s_iosIndex) = static_cast<long>(d_dag) + 1;
858  }
859 
860  static inline size_t getDag(std::ostream& out) {
861  long& l = out.iword(s_iosIndex);
862  if(l == 0) {
863  // set the default dag setting on this ostream
864  // (offset by one to detect whether default has been set yet)
865  if(&Options::current() != NULL) {
866  l = options::defaultDagThresh() + 1;
867  }
868  if(l == 0) {
869  // if called from outside the library, we may not have options
870  // available to us at this point (or perhaps the output language
871  // is not set in Options). Default to something reasonable, but
872  // don't set "l" since that would make it "sticky" for this
873  // stream.
874  return s_defaultDag + 1;
875  }
876  }
877  return static_cast<size_t>(l - 1);
878  }
879 
880  static inline void setDag(std::ostream& out, size_t dag) {
881  // (offset by one to detect whether default has been set yet)
882  out.iword(s_iosIndex) = static_cast<long>(dag) + 1;
883  }
884 
891  class Scope {
892  std::ostream& d_out;
893  size_t d_oldDag;
894 
895  public:
896 
897  inline Scope(std::ostream& out, size_t dag) :
898  d_out(out),
899  d_oldDag(ExprDag::getDag(out)) {
900  ExprDag::setDag(out, dag);
901  }
902 
903  inline ~Scope() {
904  ExprDag::setDag(d_out, d_oldDag);
905  }
906 
907  };/* class ExprDag::Scope */
908 
909 };/* class ExprDag */
910 
914 class CVC4_PUBLIC ExprSetLanguage {
918  static const int s_iosIndex;
919 
925  static const int s_defaultOutputLanguage = language::output::LANG_AUTO;
926 
930  OutputLanguage d_language;
931 
932 public:
936  ExprSetLanguage(OutputLanguage l) : d_language(l) {}
937 
938  inline void applyLanguage(std::ostream& out) {
939  // (offset by one to detect whether default has been set yet)
940  out.iword(s_iosIndex) = int(d_language) + 1;
941  }
942 
943  static inline OutputLanguage getLanguage(std::ostream& out) {
944  long& l = out.iword(s_iosIndex);
945  if(l == 0) {
946  // set the default language on this ostream
947  // (offset by one to detect whether default has been set yet)
948  if(&Options::current() != NULL) {
949  l = options::outputLanguage() + 1;
950  }
951  if(l <= 0 || l > language::output::LANG_MAX) {
952  // if called from outside the library, we may not have options
953  // available to us at this point (or perhaps the output language
954  // is not set in Options). Default to something reasonable, but
955  // don't set "l" since that would make it "sticky" for this
956  // stream.
957  return OutputLanguage(s_defaultOutputLanguage);
958  }
959  }
960  return OutputLanguage(l - 1);
961  }
962 
963  static inline void setLanguage(std::ostream& out, OutputLanguage l) {
964  // (offset by one to detect whether default has been set yet)
965  out.iword(s_iosIndex) = int(l) + 1;
966  }
967 
974  class Scope {
975  std::ostream& d_out;
976  OutputLanguage d_oldLanguage;
977 
978  public:
979 
980  inline Scope(std::ostream& out, OutputLanguage language) :
981  d_out(out),
982  d_oldLanguage(ExprSetLanguage::getLanguage(out)) {
983  ExprSetLanguage::setLanguage(out, language);
984  }
985 
986  inline ~Scope() {
987  ExprSetLanguage::setLanguage(d_out, d_oldLanguage);
988  }
989 
990  };/* class ExprSetLanguage::Scope */
991 
992 };/* class ExprSetLanguage */
993 
994 }/* CVC4::expr namespace */
995 
996 
997 #line 266 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/builtin/kinds"
999 
1000 #line 276 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/builtin/kinds"
1002 
1003 #line 287 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/builtin/kinds"
1004 template <> ::CVC4::Kind const & Expr::getConst< ::CVC4::Kind >() const;
1005 
1006 #line 309 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/builtin/kinds"
1007 template <> ::CVC4::Chain const & Expr::getConst< ::CVC4::Chain >() const;
1008 
1009 #line 315 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/builtin/kinds"
1011 
1012 #line 343 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/builtin/kinds"
1013 template <> ::CVC4::Predicate const & Expr::getConst< ::CVC4::Predicate >() const;
1014 
1015 #line 21 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/booleans/kinds"
1016 template <> bool const & Expr::getConst< bool >() const;
1017 
1018 #line 29 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/arith/kinds"
1019 template <> ::CVC4::Divisible const & Expr::getConst< ::CVC4::Divisible >() const;
1020 
1021 #line 48 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/arith/kinds"
1023 
1024 #line 61 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/arith/kinds"
1025 template <> ::CVC4::Rational const & Expr::getConst< ::CVC4::Rational >() const;
1026 
1027 #line 15 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds"
1029 
1030 #line 24 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds"
1031 template <> ::CVC4::BitVector const & Expr::getConst< ::CVC4::BitVector >() const;
1032 
1033 #line 77 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds"
1035 
1036 #line 83 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds"
1038 
1039 #line 89 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds"
1041 
1042 #line 95 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds"
1044 
1045 #line 101 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds"
1047 
1048 #line 107 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds"
1050 
1051 #line 113 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds"
1053 
1054 #line 127 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds"
1056 
1057 #line 35 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/arrays/kinds"
1059 
1060 #line 45 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds"
1061 template <> ::CVC4::Datatype const & Expr::getConst< ::CVC4::Datatype >() const;
1062 
1063 #line 77 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds"
1065 
1066 #line 108 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds"
1068 
1069 #line 116 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds"
1071 
1072 #line 124 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds"
1073 template <> ::CVC4::Record const & Expr::getConst< ::CVC4::Record >() const;
1074 
1075 #line 144 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds"
1077 
1078 #line 152 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds"
1080 
1081 #line 18 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/sets/kinds"
1082 template <> ::CVC4::EmptySet const & Expr::getConst< ::CVC4::EmptySet >() const;
1083 
1084 #line 62 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/strings/kinds"
1085 template <> ::CVC4::String const & Expr::getConst< ::CVC4::String >() const;
1086 
1087 #line 68 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/strings/kinds"
1088 template <> ::CVC4::RegExp const & Expr::getConst< ::CVC4::RegExp >() const;
1089 
1090 
1091 #line 938 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/expr/expr_template.h"
1092 
1093 namespace expr {
1094 
1104 inline std::ostream& operator<<(std::ostream& out, ExprSetDepth sd) {
1105  sd.applyDepth(out);
1106  return out;
1107 }
1108 
1118 inline std::ostream& operator<<(std::ostream& out, ExprPrintTypes pt) {
1119  pt.applyPrintTypes(out);
1120  return out;
1121 }
1122 
1132 inline std::ostream& operator<<(std::ostream& out, ExprDag d) {
1133  d.applyDag(out);
1134  return out;
1135 }
1136 
1146 inline std::ostream& operator<<(std::ostream& out, ExprSetLanguage l) {
1147  l.applyLanguage(out);
1148  return out;
1149 }
1150 
1151 }/* CVC4::expr namespace */
1152 
1154  return (size_t) e.getId();
1155 }
1156 
1157 }/* CVC4 namespace */
1158 
1159 #endif /* __CVC4__EXPR_H */
A class representing a Datatype definition.
expr::ExprSetDepth setdepth
IOStream manipulator to set the maximum depth of Exprs when pretty-printing.
Definition: expr.h:590
TypeConstant
The enumeration for the built-in atomic types.
Definition: kind.h:543
Iterator type for the children of an Expr.
Definition: expr.h:415
void * Expr
language::output::Language OutputLanguage
Definition: language.h:166
::CVC4::EmptySet const & Expr::getConst< ::CVC4::EmptySet >() const
::CVC4::UninterpretedConstant const & Expr::getConst< ::CVC4::UninterpretedConstant >() const
Class encapsulating CVC4 expressions and methods for constructing new expressions.
Definition: expr.h:227
::CVC4::Record const & Expr::getConst< ::CVC4::Record >() const
expr::ExprPrintTypes printtypes
IOStream manipulator to print type ascriptions or not.
Definition: expr.h:605
Set the expression depth on the output stream for the current stack scope.
Definition: expr.h:738
Set the dag state on the output stream for the current stack scope.
Definition: expr.h:891
void applyDepth(std::ostream &out)
Definition: expr.h:705
Definition: options.h:60
::CVC4::BitVectorRotateRight const & Expr::getConst< ::CVC4::BitVectorRotateRight >() const
Set the print-types state on the output stream for the current stack scope.
Definition: expr.h:802
ExprDag(bool dag)
Construct a ExprDag with the given setting (dagification on or off).
Definition: expr.h:846
static size_t getDag(std::ostream &out)
Definition: expr.h:860
void * ExprManager
The representation of an inductive datatype.
Definition: datatype.h:423
static OutputLanguage getLanguage(std::ostream &out)
Definition: expr.h:943
IOStream manipulator to set the output language for Exprs.
Definition: expr.h:914
::CVC4::BitVectorSize const & Expr::getConst< ::CVC4::BitVectorSize >() const
::CVC4::Kind const & Expr::getConst< ::CVC4::Kind >() const
The structure representing the extraction of one Boolean bit.
Definition: bitvector.h:432
static bool getPrintTypes(std::ostream &out)
Definition: expr.h:788
::CVC4::String const & Expr::getConst< ::CVC4::String >() const
Set a language on the output stream for the current stack scope.
Definition: expr.h:974
Class encapsulating CVC4 expression types.
Definition: type.h:89
A class to represent a chained, built-in operator.
Definition: chain.h:29
[[ Add one-line brief description here ]]
STL namespace.
LANG_MAX is > any valid OutputLanguage id.
Definition: language.h:128
void applyLanguage(std::ostream &out)
Definition: expr.h:938
ExprSetLanguage(OutputLanguage l)
Construct a ExprSetLanguage with the given setting.
Definition: expr.h:936
::CVC4::AbstractValue const & Expr::getConst< ::CVC4::AbstractValue >() const
A class representing a type ascription.
A multi-precision rational constant.
bool operator>=(const Expr &e) const
Order comparison operator.
Definition: expr.h:331
::CVC4::Predicate const & Expr::getConst< ::CVC4::Predicate >() const
static void setDepth(std::ostream &out, long depth)
Definition: expr.h:728
::CVC4::TupleUpdate const & Expr::getConst< ::CVC4::TupleUpdate >() const
::CVC4::IntToBitVector const & Expr::getConst< ::CVC4::IntToBitVector >() const
TheoryId & operator++(TheoryId &id)
Definition: kind.h:610
::CVC4::BitVectorRotateLeft const & Expr::getConst< ::CVC4::BitVectorRotateLeft >() const
Representation of a constant array (an array in which the element is the same for all indices) ...
CVC4&#39;s exception base class and some associated utilities.
std::ostream & operator<<(std::ostream &out, ExprSetDepth sd)
Sets the default depth when pretty-printing a Expr to an ostream.
Definition: expr.h:1104
::CVC4::BitVectorBitOf const & Expr::getConst< ::CVC4::BitVectorBitOf >() const
Match the output language to the input language.
Definition: language.h:99
::CVC4::BitVector const & Expr::getConst< ::CVC4::BitVector >() const
Scope(std::ostream &out, long depth)
Definition: expr.h:744
IOStream manipulator to print type ascriptions or not.
Definition: expr.h:767
IOStream manipulator to print expressions as a dag (or not).
Definition: expr.h:825
Representation of subrange bounds.
Exception thrown in the case of type-checking errors.
Definition: expr.h:151
void applyDag(std::ostream &out)
Definition: expr.h:855
::CVC4::BitVectorExtract const & Expr::getConst< ::CVC4::BitVectorExtract >() const
::CVC4::RecordSelect const & Expr::getConst< ::CVC4::RecordSelect >() const
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
::CVC4::ArrayStoreAll const & Expr::getConst< ::CVC4::ArrayStoreAll >() const
Definition of input and output languages.
::CVC4::RegExp const & Expr::getConst< ::CVC4::RegExp >() const
Representation of abstract values.
::CVC4::BitVectorSignExtend const & Expr::getConst< ::CVC4::BitVectorSignExtend >() const
static void setDag(std::ostream &out, size_t dag)
Definition: expr.h:880
void applyPrintTypes(std::ostream &out)
Definition: expr.h:784
struct CVC4::options::outputLanguage__option_t outputLanguage
static Options & current()
Get the current Options in effect.
Definition: options.h:64
Macros that should be defined everywhere during the building of the libraries and driver binary...
std::vector< Expr > getChildren() const
Returns the children of this Expr.
Definition: expr.h:366
A class used to parameterize a type ascription.
bool operator!=(const const_iterator &it) const
Definition: expr.h:429
unsigned long getId() const
Get the ID of this expression (used for the comparison operators).
[[ Add one-line brief description here ]]
Scope(std::ostream &out, OutputLanguage language)
Definition: expr.h:980
static long getDepth(std::ostream &out)
Definition: expr.h:709
::CVC4::TypeConstant const & Expr::getConst< ::CVC4::TypeConstant >() const
A class representing a Record definition.
::CVC4::TupleSelect const & Expr::getConst< ::CVC4::TupleSelect >() const
ExprDag(int dag)
Construct a ExprDag with the given setting (letify only common subexpressions that appear more than &#39;...
Definition: expr.h:853
[[ Add one-line brief description here ]]
size_t operator()(CVC4::Expr e) const
Definition: expr.h:1153
struct CVC4::options::defaultDagThresh__option_t defaultDagThresh
[[ Add one-line brief description here ]]
bool operator<=(const Expr &e) const
Order comparison operator.
Definition: expr.h:319
ExprSetDepth(long depth)
Construct a ExprSetDepth with the given depth.
Definition: expr.h:703
Representation of predicates for predicate subtyping.
::CVC4::SubrangeBounds const & Expr::getConst< ::CVC4::SubrangeBounds >() const
kind.h
ExprPrintTypes(bool printTypes)
Construct a ExprPrintTypes with the given setting.
Definition: expr.h:782
[[ Add one-line brief description here ]]
expr::ExprSetLanguage setlanguage
IOStream manipulator to set the output language for Exprs.
Definition: expr.h:615
struct CVC4::options::out__option_t out
IOStream manipulator to set the maximum depth of Exprs when pretty-printing.
Definition: expr.h:682
Representation of constants of uninterpreted sorts.
Tuple operators.
::CVC4::BitVectorRepeat const & Expr::getConst< ::CVC4::BitVectorRepeat >() const
options.h
void * Type
ExportUnsupportedException(const char *msg)
Definition: expr.h:202
Scope(std::ostream &out, bool printTypes)
Definition: expr.h:808
[[ Add one-line brief description here ]]
::CVC4::AscriptionType const & Expr::getConst< ::CVC4::AscriptionType >() const
The structure representing the divisibility-by-k predicate.
Definition: divisible.h:32
bool operator!=(enum Result::Sat s, const Result &r)
::CVC4::Chain const & Expr::getConst< ::CVC4::Chain >() const
A hash function for Boolean.
struct CVC4::options::defaultExprDepth__option_t defaultExprDepth
bool operator==(enum Result::Sat s, const Result &r)
expr::ExprDag dag
IOStream manipulator to print expressions as a DAG (or not).
Definition: expr.h:610
::CVC4::RecordUpdate const & Expr::getConst< ::CVC4::RecordUpdate >() const
::CVC4::Rational const & Expr::getConst< ::CVC4::Rational >() const
static void setLanguage(std::ostream &out, OutputLanguage l)
Definition: expr.h:963
::CVC4::Divisible const & Expr::getConst< ::CVC4::Divisible >() const
Kind_t
Definition: kind.h:60
The structure representing the extraction operation for bit-vectors.
Definition: bitvector.h:403
static void setPrintTypes(std::ostream &out, bool printTypes)
Definition: expr.h:792
::CVC4::BitVectorZeroExtend const & Expr::getConst< ::CVC4::BitVectorZeroExtend >() const
Exception thrown in case of failure to export.
Definition: expr.h:197
::CVC4::Datatype const & Expr::getConst< ::CVC4::Datatype >() const
Scope(std::ostream &out, size_t dag)
Definition: expr.h:897