cvc4-1.3
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.3/builds/aarch64-redhat-linux-gnu/default-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/regexp.h"
84 #include "util/regexp.h"
85 
86 #ifndef __CVC4__EXPR_H
87 #define __CVC4__EXPR_H
88 
89 #include <string>
90 #include <iostream>
91 #include <iterator>
92 #include <stdint.h>
93 
94 #include "util/exception.h"
95 #include "util/language.h"
96 #include "util/hash.h"
97 #include "expr/options.h"
98 
99 // This is a hack, but an important one: if there's an error, the
100 // compiler directs the user to the template file instead of the
101 // generated one. We don't want the user to modify the generated one,
102 // since it'll get overwritten on a later build.
103 #line 44 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/expr/expr_template.h"
104 
105 namespace CVC4 {
106 
107 // The internal expression representation
108 template <bool ref_count>
110 
111 class NodeManager;
112 
113 class Expr;
114 class ExprManager;
115 class SmtEngine;
116 class Type;
118 class TypeCheckingExceptionPrivate;
119 
120 namespace expr {
121  namespace pickle {
122  class Pickler;
123  }/* CVC4::expr::pickle namespace */
124 }/* CVC4::expr namespace */
125 
126 namespace prop {
127  class TheoryProxy;
128 }/* CVC4::prop namespace */
129 
131 
132 struct ExprHashFunction;
133 
134 namespace smt {
135  class SmtEnginePrivate;
136 }/* CVC4::smt namespace */
137 
138 namespace expr {
139  class CVC4_PUBLIC ExprSetDepth;
140  class CVC4_PUBLIC ExprPrintTypes;
141  class CVC4_PUBLIC ExprDag;
142  class CVC4_PUBLIC ExprSetLanguage;
143 
145 }/* CVC4::expr namespace */
146 
151 
152  friend class SmtEngine;
153  friend class smt::SmtEnginePrivate;
154 
155 private:
156 
158  Expr* d_expr;
159 
160 protected:
161 
164  const TypeCheckingExceptionPrivate* exc) throw();
165 
166 public:
167 
168  TypeCheckingException(const Expr& expr, std::string message) throw();
169 
172 
174  ~TypeCheckingException() throw();
175 
181  Expr getExpression() const throw();
182 
188  void toStream(std::ostream& out) const throw();
189 
190  friend class ExprManager;
191 };/* class TypeCheckingException */
192 
197 public:
199  Exception("export unsupported") {
200  }
201  ExportUnsupportedException(const char* msg) throw():
202  Exception(msg) {
203  }
204 };/* class DatatypeExportUnsupportedException */
205 
206 std::ostream& operator<<(std::ostream& out,
207  const TypeCheckingException& e) CVC4_PUBLIC;
208 
215 std::ostream& operator<<(std::ostream& out, const Expr& e) CVC4_PUBLIC;
216 
217 // for hash_maps, hash_sets..
219  size_t operator()(CVC4::Expr e) const;
220 };/* struct ExprHashFunction */
221 
227 
229  NodeTemplate<true>* d_node;
230 
232  ExprManager* d_exprManager;
233 
240  Expr(ExprManager* em, NodeTemplate<true>* node);
241 
242 public:
243 
245  Expr();
246 
252  Expr(const Expr& e);
253 
255  ~Expr();
256 
265  Expr& operator=(const Expr& e);
266 
274  bool operator==(const Expr& e) const;
275 
282  bool operator!=(const Expr& e) const;
283 
294  bool operator<(const Expr& e) const;
295 
306  bool operator>(const Expr& e) const;
307 
318  bool operator<=(const Expr& e) const { return !(*this > e); }
319 
330  bool operator>=(const Expr& e) const { return !(*this < e); }
331 
338  unsigned long getId() const;
339 
345  Kind getKind() const;
346 
352  size_t getNumChildren() const;
353 
360  Expr operator[](unsigned i) const;
361 
365  std::vector<Expr> getChildren() const {
366  return std::vector<Expr>(begin(), end());
367  }
368 
372  Expr notExpr() const;
373 
378  Expr andExpr(const Expr& e) const;
379 
384  Expr orExpr(const Expr& e) const;
385 
390  Expr xorExpr(const Expr& e) const;
391 
396  Expr iffExpr(const Expr& e) const;
397 
402  Expr impExpr(const Expr& e) const;
403 
409  Expr iteExpr(const Expr& then_e, const Expr& else_e) const;
410 
414  class const_iterator : public std::iterator<std::input_iterator_tag, Expr> {
415  ExprManager* d_exprManager;
416  void* d_iterator;
417 
418  explicit const_iterator(ExprManager*, void*);
419 
420  friend class Expr;// to access void* constructor
421 
422  public:
423  const_iterator();
424  const_iterator(const const_iterator& it);
425  const_iterator& operator=(const const_iterator& it);
426  ~const_iterator();
427  bool operator==(const const_iterator& it) const;
428  bool operator!=(const const_iterator& it) const {
429  return !(*this == it);
430  }
433  Expr operator*() const;
434  };/* class Expr::const_iterator */
435 
439  const_iterator begin() const;
440 
444  const_iterator end() const;
445 
451  bool hasOperator() const;
452 
459  Expr getOperator() const;
460 
485  Type getType(bool check = false) const throw (TypeCheckingException);
486 
490  Expr substitute(Expr e, Expr replacement) const;
491 
495  Expr substitute(const std::vector<Expr> exes,
496  const std::vector<Expr>& replacements) const;
497 
501  Expr substitute(const std::hash_map<Expr, Expr, ExprHashFunction> map) const;
502 
507  std::string toString() const;
508 
521  void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1,
522  OutputLanguage language = language::output::LANG_AST) const;
523 
529  bool isNull() const;
530 
536  bool isVariable() const;
537 
543  bool isConst() const;
544 
545  /* A note on isAtomic() and isAtomicFormula() (in CVC3 parlance)..
546  *
547  * It has been decided for now to hold off on implementations of
548  * these functions, as they may only be needed in CNF conversion,
549  * where it's pointless to do a lazy isAtomic determination by
550  * searching through the DAG, and storing it, since the result will
551  * only be used once. For more details see the 4/27/2010 CVC4
552  * developer's meeting notes at:
553  *
554  * http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_April_27,_2010#isAtomic.28.29_and_isAtomicFormula.28.29
555  */
556  // bool containsDecision(); // is "atomic"
557  // bool properlyContainsDecision(); // maybe not atomic but all children are
558 
560  template <class T>
561  const T& getConst() const;
562 
566  ExprManager* getExprManager() const;
567 
573  Expr exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap, uint32_t flags = 0) const;
574 
589  typedef expr::ExprSetDepth setdepth;
590 
604  typedef expr::ExprPrintTypes printtypes;
605 
609  typedef expr::ExprDag dag;
610 
614  typedef expr::ExprSetLanguage setlanguage;
615 
622  void printAst(std::ostream& out, int indent = 0) const;
623 
624 private:
625 
632  void debugPrint();
633 
638  NodeTemplate<true> getNode() const throw();
639 
644  NodeTemplate<false> getTNode() const throw();
645 
646  // Friend to access the actual internal expr information and private methods
647  friend class SmtEngine;
648  friend class smt::SmtEnginePrivate;
649  friend class ExprManager;
650  friend class NodeManager;
651  friend class TypeCheckingException;
652  friend class expr::pickle::Pickler;
653  friend class prop::TheoryProxy;
654  friend NodeTemplate<true> expr::exportInternal(NodeTemplate<false> n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap, uint32_t flags);
655 
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 
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 
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 
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 
918  static const int s_iosIndex;
919 
925  static const int s_defaultOutputLanguage = language::output::LANG_AST;
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 264 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/builtin/kinds"
998 template <> ::CVC4::UninterpretedConstant const & Expr::getConst< ::CVC4::UninterpretedConstant >() const;
999 
1000 #line 274 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/builtin/kinds"
1001 template <> ::CVC4::AbstractValue const & Expr::getConst< ::CVC4::AbstractValue >() const;
1002 
1003 #line 285 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/builtin/kinds"
1004 template <> ::CVC4::Kind const & Expr::getConst< ::CVC4::Kind >() const;
1005 
1006 #line 304 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/builtin/kinds"
1007 template <> ::CVC4::Chain const & Expr::getConst< ::CVC4::Chain >() const;
1008 
1009 #line 310 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/builtin/kinds"
1010 template <> ::CVC4::TypeConstant const & Expr::getConst< ::CVC4::TypeConstant >() const;
1011 
1012 #line 337 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/builtin/kinds"
1013 template <> ::CVC4::Predicate const & Expr::getConst< ::CVC4::Predicate >() const;
1014 
1015 #line 21 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/booleans/kinds"
1016 template <> bool const & Expr::getConst< bool >() const;
1017 
1018 #line 30 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/arith/kinds"
1019 template <> ::CVC4::Divisible const & Expr::getConst< ::CVC4::Divisible >() const;
1020 
1021 #line 49 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/arith/kinds"
1022 template <> ::CVC4::SubrangeBounds const & Expr::getConst< ::CVC4::SubrangeBounds >() const;
1023 
1024 #line 62 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/arith/kinds"
1025 template <> ::CVC4::Rational const & Expr::getConst< ::CVC4::Rational >() const;
1026 
1027 #line 15 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/bv/kinds"
1028 template <> ::CVC4::BitVectorSize const & Expr::getConst< ::CVC4::BitVectorSize >() const;
1029 
1030 #line 24 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/bv/kinds"
1031 template <> ::CVC4::BitVector const & Expr::getConst< ::CVC4::BitVector >() const;
1032 
1033 #line 73 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/bv/kinds"
1034 template <> ::CVC4::BitVectorBitOf const & Expr::getConst< ::CVC4::BitVectorBitOf >() const;
1035 
1036 #line 79 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/bv/kinds"
1037 template <> ::CVC4::BitVectorExtract const & Expr::getConst< ::CVC4::BitVectorExtract >() const;
1038 
1039 #line 85 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/bv/kinds"
1040 template <> ::CVC4::BitVectorRepeat const & Expr::getConst< ::CVC4::BitVectorRepeat >() const;
1041 
1042 #line 91 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/bv/kinds"
1043 template <> ::CVC4::BitVectorZeroExtend const & Expr::getConst< ::CVC4::BitVectorZeroExtend >() const;
1044 
1045 #line 97 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/bv/kinds"
1046 template <> ::CVC4::BitVectorSignExtend const & Expr::getConst< ::CVC4::BitVectorSignExtend >() const;
1047 
1048 #line 103 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/bv/kinds"
1049 template <> ::CVC4::BitVectorRotateLeft const & Expr::getConst< ::CVC4::BitVectorRotateLeft >() const;
1050 
1051 #line 109 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/bv/kinds"
1052 template <> ::CVC4::BitVectorRotateRight const & Expr::getConst< ::CVC4::BitVectorRotateRight >() const;
1053 
1054 #line 123 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/bv/kinds"
1055 template <> ::CVC4::IntToBitVector const & Expr::getConst< ::CVC4::IntToBitVector >() const;
1056 
1057 #line 35 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/arrays/kinds"
1058 template <> ::CVC4::ArrayStoreAll const & Expr::getConst< ::CVC4::ArrayStoreAll >() const;
1059 
1060 #line 45 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/datatypes/kinds"
1061 template <> ::CVC4::Datatype const & Expr::getConst< ::CVC4::Datatype >() const;
1062 
1063 #line 77 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/datatypes/kinds"
1064 template <> ::CVC4::AscriptionType const & Expr::getConst< ::CVC4::AscriptionType >() const;
1065 
1066 #line 107 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/datatypes/kinds"
1067 template <> ::CVC4::TupleSelect const & Expr::getConst< ::CVC4::TupleSelect >() const;
1068 
1069 #line 115 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/datatypes/kinds"
1070 template <> ::CVC4::TupleUpdate const & Expr::getConst< ::CVC4::TupleUpdate >() const;
1071 
1072 #line 123 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/datatypes/kinds"
1073 template <> ::CVC4::Record const & Expr::getConst< ::CVC4::Record >() const;
1074 
1075 #line 143 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/datatypes/kinds"
1076 template <> ::CVC4::RecordSelect const & Expr::getConst< ::CVC4::RecordSelect >() const;
1077 
1078 #line 151 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/datatypes/kinds"
1079 template <> ::CVC4::RecordUpdate const & Expr::getConst< ::CVC4::RecordUpdate >() const;
1080 
1081 #line 50 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/strings/kinds"
1082 template <> ::CVC4::String const & Expr::getConst< ::CVC4::String >() const;
1083 
1084 #line 56 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/strings/kinds"
1085 template <> ::CVC4::RegExp const & Expr::getConst< ::CVC4::RegExp >() const;
1086 
1087 
1088 #line 939 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/expr/expr_template.h"
1089 
1090 namespace expr {
1091 
1101 inline std::ostream& operator<<(std::ostream& out, ExprSetDepth sd) {
1102  sd.applyDepth(out);
1103  return out;
1104 }
1105 
1115 inline std::ostream& operator<<(std::ostream& out, ExprPrintTypes pt) {
1116  pt.applyPrintTypes(out);
1117  return out;
1118 }
1119 
1129 inline std::ostream& operator<<(std::ostream& out, ExprDag d) {
1130  d.applyDag(out);
1131  return out;
1132 }
1133 
1143 inline std::ostream& operator<<(std::ostream& out, ExprSetLanguage l) {
1144  l.applyLanguage(out);
1145  return out;
1146 }
1147 
1148 }/* CVC4::expr namespace */
1149 
1151  return (size_t) e.getId();
1152 }
1153 
1154 }/* CVC4 namespace */
1155 
1156 #endif /* __CVC4__EXPR_H */
A class representing a Datatype definition.
TypeConstant
The enumeration for the built-in atomic types.
Definition: kind.h:483
Iterator type for the children of an Expr.
Definition: expr.h:414
void * Expr
language::output::Language OutputLanguage
Definition: language.h:150
Class encapsulating CVC4 expressions and methods for constructing new expressions.
Definition: expr.h:226
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:382
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:431
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:88
A class to represent a chained, built-in operator.
Definition: chain.h:29
[[ Add one-line brief description here ]]
LANG_MAX is > any valid OutputLanguage id.
Definition: language.h:118
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:330
NodeTemplate< true > exportInternal(NodeTemplate< false > n, ExprManager *from, ExprManager *to, ExprManagerMapCollection &vmap, uint32_t flags)
static void setDepth(std::ostream &out, long depth)
Definition: expr.h:728
TheoryId & operator++(TheoryId &id)
Definition: kind.h:550
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.
Scope(std::ostream &out, long depth)
Definition: expr.h:744
This is CVC4 release version For build and installation please see the INSTALL file included with this distribution This first official release of CVC4 is the result of more than three years of efforts by researchers at New York University and The University of Iowa The project leaders are Clark please refer to the AUTHORS file in the source distribution CVC4 is a tool for determining the satisfiability of a first order formula modulo a first order CVC CVC3 but does not directly incorporate code from any previous version CVC4 is intended to be an open and extensible SMT engine It can be used as a stand alone tool or as a library It has been designed to increase the performance and reduce the memory overhead of its predecessors It is written entirely in C and is released under a free software see the INSTALL file that comes with this distribution We recommend that you visit our CVC4 tutorials online please write to the cvc users cs nyu edu mailing list *if you need to report a bug with CVC4
Definition: README:39
The AST output language.
Definition: language.h:115
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:150
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:508
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:365
A class used to parameterize a type ascription.
bool operator!=(const const_iterator &it) const
Definition: expr.h:428
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:1150
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:318
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:201
Scope(std::ostream &out, bool printTypes)
Definition: expr.h:808
The structure representing the divisibility-by-k predicate.
Definition: divisible.h:32
bool operator!=(enum Result::Sat s, const Result &r)
A multi-precision rational constant.
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:402
static void setPrintTypes(std::ostream &out, bool printTypes)
Definition: expr.h:792
Exception thrown in case of failure to export.
Definition: expr.h:196
Scope(std::ostream &out, size_t dag)
Definition: expr.h:897