cvc4-1.4
expr_manager.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_manager_template.h */
30 
31 /********************* */
47 #include "cvc4_public.h"
48 
49 #ifndef __CVC4__EXPR_MANAGER_H
50 #define __CVC4__EXPR_MANAGER_H
51 
52 #include <vector>
53 
54 #include "expr/kind.h"
55 #include "expr/type.h"
56 #include "expr/expr.h"
57 #include "util/subrange_bound.h"
58 #include "util/statistics.h"
59 #include "util/sexpr.h"
60 
61 
63 #include "util/abstract_value.h"
64 #include "expr/kind.h"
65 #include "util/chain.h"
66 #include "expr/kind.h"
67 #include "util/predicate.h"
68 #include "util/bool.h"
69 #include "util/divisible.h"
70 #include "util/subrange_bound.h"
71 #include "util/rational.h"
72 #include "util/bitvector.h"
73 #include "util/bitvector.h"
74 #include "util/bitvector.h"
75 #include "util/bitvector.h"
76 #include "util/bitvector.h"
77 #include "util/bitvector.h"
78 #include "util/bitvector.h"
79 #include "util/bitvector.h"
80 #include "util/bitvector.h"
81 #include "util/bitvector.h"
82 #include "util/array_store_all.h"
83 #include "util/datatype.h"
84 #include "util/ascription_type.h"
85 #include "util/tuple.h"
86 #include "util/tuple.h"
87 #include "util/record.h"
88 #include "util/record.h"
89 #include "util/record.h"
90 #include "util/emptyset.h"
91 #include "util/regexp.h"
92 #include "util/regexp.h"
93 
94 // This is a hack, but an important one: if there's an error, the
95 // compiler directs the user to the template file instead of the
96 // generated one. We don't want the user to modify the generated one,
97 // since it'll get overwritten on a later build.
98 #line 38 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/expr/expr_manager_template.h"
99 
100 namespace CVC4 {
101 
102 class Expr;
103 class SmtEngine;
104 class NodeManager;
105 class Options;
106 class IntStat;
107 struct ExprManagerMapCollection;
108 class StatisticsRegistry;
109 
110 namespace expr {
111  namespace pickle {
112  class Pickler;
113  }/* CVC4::expr::pickle namespace */
114 }/* CVC4::expr namespace */
115 
116 namespace context {
117  class Context;
118 }/* CVC4::context namespace */
119 
120 namespace stats {
121  StatisticsRegistry* getStatisticsRegistry(ExprManager*);
122 }/* CVC4::stats namespace */
123 
125 private:
127  context::Context* d_ctxt;
128 
130  NodeManager* d_nodeManager;
131 
133  IntStat* d_exprStatisticsVars[LAST_TYPE];
134  IntStat* d_exprStatistics[kind::LAST_KIND];
135 
140  NodeManager* getNodeManager() const;
141 
146  context::Context* getContext() const;
147 
151  void checkResolvedDatatype(DatatypeType dtt) const;
152 
157  friend class SmtEngine;
158 
160  friend class ExprManagerScope;
161 
163  friend class NodeManager;
164 
166  friend ::CVC4::StatisticsRegistry* ::CVC4::stats::getStatisticsRegistry(ExprManager*);
167 
169  StatisticsRegistry* getStatisticsRegistry() throw();
170 
171  // undefined, private copy constructor and assignment op (disallow copy)
173  ExprManager& operator=(const ExprManager&) CVC4_UNDEFINED;
174 
175 public:
176 
180  ExprManager();
181 
188  explicit ExprManager(const Options& options);
189 
195  ~ExprManager() throw();
196 
198  const Options& getOptions() const;
199 
201  BooleanType booleanType() const;
202 
204  StringType stringType() const;
205 
207  RealType realType() const;
208 
210  IntegerType integerType() const;
211 
218  Expr mkExpr(Kind kind, Expr child1);
219 
227  Expr mkExpr(Kind kind, Expr child1, Expr child2);
228 
237  Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3);
238 
248  Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4);
249 
260  Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4,
261  Expr child5);
262 
271  Expr mkExpr(Kind kind, const std::vector<Expr>& children);
272 
284  Expr mkExpr(Kind kind, Expr child1, const std::vector<Expr>& otherChildren);
285 
292  Expr mkExpr(Expr opExpr);
293 
301  Expr mkExpr(Expr opExpr, Expr child1);
302 
311  Expr mkExpr(Expr opExpr, Expr child1, Expr child2);
312 
322  Expr mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3);
323 
334  Expr mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3, Expr child4);
335 
347  Expr mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3, Expr child4,
348  Expr child5);
349 
358  Expr mkExpr(Expr opExpr, const std::vector<Expr>& children);
359 
361  template <class T>
362  Expr mkConst(const T&);
363 
375  Expr mkAssociative(Kind kind, const std::vector<Expr>& children);
376 
381  static bool hasOperator(Kind k);
382 
388  Expr operatorOf(Kind k);
389 
391  FunctionType mkFunctionType(Type domain, Type range);
392 
397  FunctionType mkFunctionType(const std::vector<Type>& argTypes, Type range);
398 
405  FunctionType mkFunctionType(const std::vector<Type>& sorts);
406 
413  FunctionType mkPredicateType(const std::vector<Type>& sorts);
414 
420  TupleType mkTupleType(const std::vector<Type>& types);
421 
425  RecordType mkRecordType(const Record& rec);
426 
432  SExprType mkSExprType(const std::vector<Type>& types);
433 
435  BitVectorType mkBitVectorType(unsigned size) const;
436 
438  ArrayType mkArrayType(Type indexType, Type constituentType) const;
439 
441  SetType mkSetType(Type elementType) const;
442 
444  DatatypeType mkDatatypeType(const Datatype& datatype);
445 
450  std::vector<DatatypeType>
451  mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes);
452 
482  std::vector<DatatypeType>
483  mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
484  const std::set<Type>& unresolvedTypes);
485 
489  ConstructorType mkConstructorType(const DatatypeConstructor& constructor, Type range) const;
490 
492  SelectorType mkSelectorType(Type domain, Type range) const;
493 
495  TesterType mkTesterType(Type domain) const;
496 
498  enum {
499  SORT_FLAG_NONE = 0,
500  SORT_FLAG_PLACEHOLDER = 1
501  };/* enum */
502 
504  SortType mkSort(const std::string& name, uint32_t flags = SORT_FLAG_NONE) const;
505 
507  SortConstructorType mkSortConstructor(const std::string& name,
508  size_t arity) const;
509 
516  // not in release 1.0
517  //Type mkPredicateSubtype(Expr lambda)
518  // throw(TypeCheckingException);
519 
527  // not in release 1.0
528  //Type mkPredicateSubtype(Expr lambda, Expr witness)
529  // throw(TypeCheckingException);
530 
534  Type mkSubrangeType(const SubrangeBounds& bounds)
535  throw(TypeCheckingException);
536 
538  Type getType(Expr e, bool check = false)
539  throw(TypeCheckingException);
540 
542  enum {
543  VAR_FLAG_NONE = 0,
544  VAR_FLAG_GLOBAL = 1,
545  VAR_FLAG_DEFINED = 2
546  };/* enum */
547 
569  Expr mkVar(const std::string& name, Type type, uint32_t flags = VAR_FLAG_NONE);
570 
583  Expr mkVar(Type type, uint32_t flags = VAR_FLAG_NONE);
584 
602  Expr mkBoundVar(const std::string& name, Type type);
603 
617  Expr mkBoundVar(Type type);
618 
620  Statistics getStatistics() const throw();
621 
623  SExpr getStatistic(const std::string& name) const throw();
624 
626  //static Expr exportExpr(const Expr& e, ExprManager* em);
628  static Type exportType(const Type& t, ExprManager* em, ExprManagerMapCollection& vmap);
629 
631  static unsigned minArity(Kind kind);
632 
634  static unsigned maxArity(Kind kind);
635 
636 };/* class ExprManager */
637 
638 
639 #line 266 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/builtin/kinds"
640 template <> Expr ExprManager::mkConst(::CVC4::UninterpretedConstant const& val);
641 
642 #line 276 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/builtin/kinds"
643 template <> Expr ExprManager::mkConst(::CVC4::AbstractValue const& val);
644 
645 #line 287 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/builtin/kinds"
646 template <> Expr ExprManager::mkConst(::CVC4::Kind const& val);
647 
648 #line 309 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/builtin/kinds"
649 template <> Expr ExprManager::mkConst(::CVC4::Chain const& val);
650 
651 #line 315 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/builtin/kinds"
652 template <> Expr ExprManager::mkConst(::CVC4::TypeConstant const& val);
653 
654 #line 343 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/builtin/kinds"
655 template <> Expr ExprManager::mkConst(::CVC4::Predicate const& val);
656 
657 #line 21 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/booleans/kinds"
658 template <> Expr ExprManager::mkConst(bool const& val);
659 
660 #line 29 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/arith/kinds"
661 template <> Expr ExprManager::mkConst(::CVC4::Divisible const& val);
662 
663 #line 48 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/arith/kinds"
664 template <> Expr ExprManager::mkConst(::CVC4::SubrangeBounds const& val);
665 
666 #line 61 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/arith/kinds"
667 template <> Expr ExprManager::mkConst(::CVC4::Rational const& val);
668 
669 #line 15 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds"
670 template <> Expr ExprManager::mkConst(::CVC4::BitVectorSize const& val);
671 
672 #line 24 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds"
673 template <> Expr ExprManager::mkConst(::CVC4::BitVector const& val);
674 
675 #line 77 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds"
676 template <> Expr ExprManager::mkConst(::CVC4::BitVectorBitOf const& val);
677 
678 #line 83 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds"
679 template <> Expr ExprManager::mkConst(::CVC4::BitVectorExtract const& val);
680 
681 #line 89 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds"
682 template <> Expr ExprManager::mkConst(::CVC4::BitVectorRepeat const& val);
683 
684 #line 95 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds"
685 template <> Expr ExprManager::mkConst(::CVC4::BitVectorZeroExtend const& val);
686 
687 #line 101 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds"
688 template <> Expr ExprManager::mkConst(::CVC4::BitVectorSignExtend const& val);
689 
690 #line 107 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds"
691 template <> Expr ExprManager::mkConst(::CVC4::BitVectorRotateLeft const& val);
692 
693 #line 113 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds"
694 template <> Expr ExprManager::mkConst(::CVC4::BitVectorRotateRight const& val);
695 
696 #line 127 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds"
697 template <> Expr ExprManager::mkConst(::CVC4::IntToBitVector const& val);
698 
699 #line 35 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/arrays/kinds"
700 template <> Expr ExprManager::mkConst(::CVC4::ArrayStoreAll const& val);
701 
702 #line 45 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds"
703 template <> Expr ExprManager::mkConst(::CVC4::Datatype const& val);
704 
705 #line 77 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds"
706 template <> Expr ExprManager::mkConst(::CVC4::AscriptionType const& val);
707 
708 #line 108 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds"
709 template <> Expr ExprManager::mkConst(::CVC4::TupleSelect const& val);
710 
711 #line 116 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds"
712 template <> Expr ExprManager::mkConst(::CVC4::TupleUpdate const& val);
713 
714 #line 124 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds"
715 template <> Expr ExprManager::mkConst(::CVC4::Record const& val);
716 
717 #line 144 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds"
718 template <> Expr ExprManager::mkConst(::CVC4::RecordSelect const& val);
719 
720 #line 152 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds"
721 template <> Expr ExprManager::mkConst(::CVC4::RecordUpdate const& val);
722 
723 #line 18 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/sets/kinds"
724 template <> Expr ExprManager::mkConst(::CVC4::EmptySet const& val);
725 
726 #line 62 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/strings/kinds"
727 template <> Expr ExprManager::mkConst(::CVC4::String const& val);
728 
729 #line 68 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/strings/kinds"
730 template <> Expr ExprManager::mkConst(::CVC4::RegExp const& val);
731 
732 
733 }/* CVC4 namespace */
734 
735 #endif /* __CVC4__EXPR_MANAGER_H */
A class representing a Datatype definition.
Singleton class encapsulating the real type.
Definition: type.h:396
Class encapsulating the Selector type.
Definition: type.h:683
TypeConstant
The enumeration for the built-in atomic types.
Definition: kind.h:543
void * Expr
Class encapsulating CVC4 expressions and methods for constructing new expressions.
Definition: expr.h:227
Singleton class encapsulating the integer type.
Definition: type.h:385
Class encapsulating a user-defined sort.
Definition: type.h:515
Class encapsulating an set type.
Definition: type.h:501
Definition: options.h:60
void * ExprManager
Class encapsulating a tuple type.
Definition: type.h:470
The representation of an inductive datatype.
Definition: datatype.h:423
Expr mkConst(const T &)
Create a constant of type T.
The structure representing the extraction of one Boolean bit.
Definition: bitvector.h:432
Class encapsulating CVC4 expression types.
Definition: type.h:89
A class to represent a chained, built-in operator.
Definition: chain.h:29
STL namespace.
Simple representation of S-expressions.
A class representing a type ascription.
A multi-precision rational constant.
[[ Add one-line brief description here ]]
Representation of a constant array (an array in which the element is the same for all indices) ...
StatisticsRegistry * getStatisticsRegistry(ExprManager *)
Class encapsulating the Tester type.
Definition: type.h:701
Singleton class encapsulating the Boolean type.
Definition: type.h:374
marks the upper-bound of this enumeration
Definition: kind.h:271
Representation of subrange bounds.
Exception thrown in the case of type-checking errors.
Definition: expr.h:151
Class encapsulating an array type.
Definition: type.h:484
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
Class encapsulating a function type.
Definition: type.h:418
Class encapsulating a user-defined sort constructor.
Definition: type.h:536
Class encapsulating the datatype type.
Definition: type.h:615
Representation of abstract values.
Macros that should be defined everywhere during the building of the libraries and driver binary...
Class encapsulating a record type.
Definition: type.h:456
A class used to parameterize a type ascription.
[[ Add one-line brief description here ]]
Class encapsulating a tuple type.
Definition: type.h:438
A class representing a Record definition.
[[ Add one-line brief description here ]]
#define CVC4_UNDEFINED
Definition: cvc4_public.h:52
[[ Add one-line brief description here ]]
Singleton class encapsulating the string type.
Definition: type.h:407
Representation of predicates for predicate subtyping.
kind.h
[[ Add one-line brief description here ]]
Representation of constants of uninterpreted sorts.
void * Context
Tuple operators.
expr.h
Class encapsulating the constructor type.
Definition: type.h:661
A constructor for a Datatype.
Definition: datatype.h:174
[[ Add one-line brief description here ]]
A simple S-expression.
Definition: sexpr.h:51
Class encapsulating the bit-vector type.
Definition: type.h:596
The structure representing the divisibility-by-k predicate.
Definition: divisible.h:32
A hash function for Boolean.
Kind_t
Definition: kind.h:60
The structure representing the extraction operation for bit-vectors.
Definition: bitvector.h:403
Interface for expression types.