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/armv7hl-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/armv7hl-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>
111 
112 class NodeManager;
113 
114 class Expr;
115 class ExprManager;
116 class SmtEngine;
117 class Type;
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 
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,
208  const TypeCheckingException& e) CVC4_PUBLIC;
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,
523  OutputLanguage language = language::output::LANG_AUTO) const;
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 
590  typedef expr::ExprSetDepth setdepth;
591 
605  typedef expr::ExprPrintTypes printtypes;
606 
610  typedef expr::ExprDag dag;
611 
615  typedef expr::ExprSetLanguage setlanguage;
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/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/builtin/kinds"
998 template <> ::CVC4::UninterpretedConstant const & Expr::getConst< ::CVC4::UninterpretedConstant >() const;
999 
1000 #line 276 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/builtin/kinds"
1001 template <> ::CVC4::AbstractValue const & Expr::getConst< ::CVC4::AbstractValue >() const;
1002 
1003 #line 287 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-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/armv7hl-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/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/builtin/kinds"
1010 template <> ::CVC4::TypeConstant const & Expr::getConst< ::CVC4::TypeConstant >() const;
1011 
1012 #line 343 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-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/armv7hl-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/armv7hl-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/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/arith/kinds"
1022 template <> ::CVC4::SubrangeBounds const & Expr::getConst< ::CVC4::SubrangeBounds >() const;
1023 
1024 #line 61 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-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/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds"
1028 template <> ::CVC4::BitVectorSize const & Expr::getConst< ::CVC4::BitVectorSize >() const;
1029 
1030 #line 24 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-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/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds"
1034 template <> ::CVC4::BitVectorBitOf const & Expr::getConst< ::CVC4::BitVectorBitOf >() const;
1035 
1036 #line 83 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds"
1037 template <> ::CVC4::BitVectorExtract const & Expr::getConst< ::CVC4::BitVectorExtract >() const;
1038 
1039 #line 89 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds"
1040 template <> ::CVC4::BitVectorRepeat const & Expr::getConst< ::CVC4::BitVectorRepeat >() const;
1041 
1042 #line 95 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds"
1043 template <> ::CVC4::BitVectorZeroExtend const & Expr::getConst< ::CVC4::BitVectorZeroExtend >() const;
1044 
1045 #line 101 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds"
1046 template <> ::CVC4::BitVectorSignExtend const & Expr::getConst< ::CVC4::BitVectorSignExtend >() const;
1047 
1048 #line 107 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds"
1049 template <> ::CVC4::BitVectorRotateLeft const & Expr::getConst< ::CVC4::BitVectorRotateLeft >() const;
1050 
1051 #line 113 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds"
1052 template <> ::CVC4::BitVectorRotateRight const & Expr::getConst< ::CVC4::BitVectorRotateRight >() const;
1053 
1054 #line 127 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds"
1055 template <> ::CVC4::IntToBitVector const & Expr::getConst< ::CVC4::IntToBitVector >() const;
1056 
1057 #line 35 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/arrays/kinds"
1058 template <> ::CVC4::ArrayStoreAll const & Expr::getConst< ::CVC4::ArrayStoreAll >() const;
1059 
1060 #line 45 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-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/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds"
1064 template <> ::CVC4::AscriptionType const & Expr::getConst< ::CVC4::AscriptionType >() const;
1065 
1066 #line 108 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds"
1067 template <> ::CVC4::TupleSelect const & Expr::getConst< ::CVC4::TupleSelect >() const;
1068 
1069 #line 116 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds"
1070 template <> ::CVC4::TupleUpdate const & Expr::getConst< ::CVC4::TupleUpdate >() const;
1071 
1072 #line 124 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-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/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds"
1076 template <> ::CVC4::RecordSelect const & Expr::getConst< ::CVC4::RecordSelect >() const;
1077 
1078 #line 152 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds"
1079 template <> ::CVC4::RecordUpdate const & Expr::getConst< ::CVC4::RecordUpdate >() const;
1080 
1081 #line 18 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-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/armv7hl-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/armv7hl-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/armv7hl-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.
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
Class encapsulating CVC4 expressions and methods for constructing new expressions.
Definition: expr.h:227
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
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
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
The structure representing the extraction of one Boolean bit.
Definition: bitvector.h:432
static bool getPrintTypes(std::ostream &out)
Definition: expr.h:788
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
A class representing a type ascription.
A multi-precision rational constant.
bool operator>=(const Expr &e) const
Order comparison operator.
Definition: expr.h:331
static void setDepth(std::ostream &out, long depth)
Definition: expr.h:728
TheoryId & operator++(TheoryId &id)
Definition: kind.h:610
Representation of a constant array (an array in which the element is the same for all indices) ...
CVC4's exception base class and some associated utilities.
Match the output language to the input language.
Definition: language.h:99
Auto-detect the language.
Definition: language.h:37
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
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
Definition of input and output languages.
std::ostream & operator<<(std::ostream &out, TypeConstant typeConstant)
Definition: kind.h:568
Representation of abstract values.
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
A class representing a Record definition.
ExprDag(int dag)
Construct a ExprDag with the given setting (letify only common subexpressions that appear more than '...
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.
kind.h
ExprPrintTypes(bool printTypes)
Construct a ExprPrintTypes with the given setting.
Definition: expr.h:782
[[ Add one-line brief description here ]]
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.
options.h
ExportUnsupportedException(const char *msg)
Definition: expr.h:202
Scope(std::ostream &out, bool printTypes)
Definition: expr.h:808
[[ Add one-line brief description here ]]
The structure representing the divisibility-by-k predicate.
Definition: divisible.h:32
bool operator!=(enum Result::Sat s, const Result &r)
A hash function for Boolean.
struct CVC4::options::defaultExprDepth__option_t defaultExprDepth
bool operator==(enum Result::Sat s, const Result &r)
static void setLanguage(std::ostream &out, OutputLanguage l)
Definition: expr.h:963
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
Exception thrown in case of failure to export.
Definition: expr.h:197
Scope(std::ostream &out, size_t dag)
Definition: expr.h:897