cvc4-1.3
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.3/builds/aarch64-redhat-linux-gnu/default-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/regexp.h"
91 #include "util/regexp.h"
92 
93 // This is a hack, but an important one: if there's an error, the
94 // compiler directs the user to the template file instead of the
95 // generated one. We don't want the user to modify the generated one,
96 // since it'll get overwritten on a later build.
97 #line 38 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/expr/expr_manager_template.h"
98 
99 namespace CVC4 {
100 
101 class Expr;
102 class SmtEngine;
103 class NodeManager;
104 class Options;
105 class IntStat;
106 struct ExprManagerMapCollection;
107 class StatisticsRegistry;
108 
109 namespace expr {
110  namespace pickle {
111  class Pickler;
112  }/* CVC4::expr::pickle namespace */
113 }/* CVC4::expr namespace */
114 
115 namespace context {
116  class Context;
117 }/* CVC4::context namespace */
118 
119 namespace stats {
120  StatisticsRegistry* getStatisticsRegistry(ExprManager*);
121 }/* CVC4::stats namespace */
122 
124 private:
126  context::Context* d_ctxt;
127 
129  NodeManager* d_nodeManager;
130 
132  IntStat* d_exprStatisticsVars[LAST_TYPE];
133  IntStat* d_exprStatistics[kind::LAST_KIND];
134 
139  NodeManager* getNodeManager() const;
140 
145  context::Context* getContext() const;
146 
150  void checkResolvedDatatype(DatatypeType dtt) const;
151 
156  friend class SmtEngine;
157 
159  friend class ExprManagerScope;
160 
162  friend class NodeManager;
163 
165  friend ::CVC4::StatisticsRegistry* ::CVC4::stats::getStatisticsRegistry(ExprManager*);
166 
168  StatisticsRegistry* getStatisticsRegistry() throw();
169 
170  // undefined, private copy constructor and assignment op (disallow copy)
172  ExprManager& operator=(const ExprManager&) CVC4_UNDEFINED;
173 
174 public:
175 
179  ExprManager();
180 
187  explicit ExprManager(const Options& options);
188 
194  ~ExprManager() throw();
195 
197  const Options& getOptions() const;
198 
200  BooleanType booleanType() const;
201 
203  StringType stringType() const;
204 
206  RealType realType() const;
207 
209  IntegerType integerType() const;
210 
217  Expr mkExpr(Kind kind, Expr child1);
218 
226  Expr mkExpr(Kind kind, Expr child1, Expr child2);
227 
236  Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3);
237 
247  Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4);
248 
259  Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4,
260  Expr child5);
261 
270  Expr mkExpr(Kind kind, const std::vector<Expr>& children);
271 
283  Expr mkExpr(Kind kind, Expr child1, const std::vector<Expr>& otherChildren);
284 
291  Expr mkExpr(Expr opExpr);
292 
300  Expr mkExpr(Expr opExpr, Expr child1);
301 
310  Expr mkExpr(Expr opExpr, Expr child1, Expr child2);
311 
321  Expr mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3);
322 
333  Expr mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3, Expr child4);
334 
346  Expr mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3, Expr child4,
347  Expr child5);
348 
357  Expr mkExpr(Expr opExpr, const std::vector<Expr>& children);
358 
360  template <class T>
361  Expr mkConst(const T&);
362 
374  Expr mkAssociative(Kind kind, const std::vector<Expr>& children);
375 
380  static bool hasOperator(Kind k);
381 
387  Expr operatorOf(Kind k);
388 
390  FunctionType mkFunctionType(Type domain, Type range);
391 
396  FunctionType mkFunctionType(const std::vector<Type>& argTypes, Type range);
397 
404  FunctionType mkFunctionType(const std::vector<Type>& sorts);
405 
412  FunctionType mkPredicateType(const std::vector<Type>& sorts);
413 
419  TupleType mkTupleType(const std::vector<Type>& types);
420 
424  RecordType mkRecordType(const Record& rec);
425 
431  SExprType mkSExprType(const std::vector<Type>& types);
432 
434  BitVectorType mkBitVectorType(unsigned size) const;
435 
437  ArrayType mkArrayType(Type indexType, Type constituentType) const;
438 
440  DatatypeType mkDatatypeType(const Datatype& datatype);
441 
446  std::vector<DatatypeType>
447  mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes);
448 
478  std::vector<DatatypeType>
479  mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
480  const std::set<Type>& unresolvedTypes);
481 
485  ConstructorType mkConstructorType(const DatatypeConstructor& constructor, Type range) const;
486 
488  SelectorType mkSelectorType(Type domain, Type range) const;
489 
491  TesterType mkTesterType(Type domain) const;
492 
494  enum {
495  SORT_FLAG_NONE = 0,
496  SORT_FLAG_PLACEHOLDER = 1
497  };/* enum */
498 
500  SortType mkSort(const std::string& name, uint32_t flags = SORT_FLAG_NONE) const;
501 
503  SortConstructorType mkSortConstructor(const std::string& name,
504  size_t arity) const;
505 
512  // not in release 1.0
513  //Type mkPredicateSubtype(Expr lambda)
514  // throw(TypeCheckingException);
515 
523  // not in release 1.0
524  //Type mkPredicateSubtype(Expr lambda, Expr witness)
525  // throw(TypeCheckingException);
526 
530  Type mkSubrangeType(const SubrangeBounds& bounds)
531  throw(TypeCheckingException);
532 
534  Type getType(Expr e, bool check = false)
535  throw(TypeCheckingException);
536 
538  enum {
539  VAR_FLAG_NONE = 0,
540  VAR_FLAG_GLOBAL = 1,
541  VAR_FLAG_DEFINED = 2
542  };/* enum */
543 
565  Expr mkVar(const std::string& name, Type type, uint32_t flags = VAR_FLAG_NONE);
566 
579  Expr mkVar(Type type, uint32_t flags = VAR_FLAG_NONE);
580 
598  Expr mkBoundVar(const std::string& name, Type type);
599 
613  Expr mkBoundVar(Type type);
614 
616  Statistics getStatistics() const throw();
617 
619  SExpr getStatistic(const std::string& name) const throw();
620 
622  //static Expr exportExpr(const Expr& e, ExprManager* em);
624  static Type exportType(const Type& t, ExprManager* em, ExprManagerMapCollection& vmap);
625 
627  static unsigned minArity(Kind kind);
628 
630  static unsigned maxArity(Kind kind);
631 
632 };/* class ExprManager */
633 
634 
635 #line 264 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/builtin/kinds"
636 template <> Expr ExprManager::mkConst(::CVC4::UninterpretedConstant const& val);
637 
638 #line 274 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/builtin/kinds"
639 template <> Expr ExprManager::mkConst(::CVC4::AbstractValue const& val);
640 
641 #line 285 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/builtin/kinds"
642 template <> Expr ExprManager::mkConst(::CVC4::Kind const& val);
643 
644 #line 304 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/builtin/kinds"
645 template <> Expr ExprManager::mkConst(::CVC4::Chain const& val);
646 
647 #line 310 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/builtin/kinds"
648 template <> Expr ExprManager::mkConst(::CVC4::TypeConstant const& val);
649 
650 #line 337 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/builtin/kinds"
651 template <> Expr ExprManager::mkConst(::CVC4::Predicate const& val);
652 
653 #line 21 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/booleans/kinds"
654 template <> Expr ExprManager::mkConst(bool const& val);
655 
656 #line 30 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/arith/kinds"
657 template <> Expr ExprManager::mkConst(::CVC4::Divisible const& val);
658 
659 #line 49 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/arith/kinds"
660 template <> Expr ExprManager::mkConst(::CVC4::SubrangeBounds const& val);
661 
662 #line 62 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/arith/kinds"
663 template <> Expr ExprManager::mkConst(::CVC4::Rational const& val);
664 
665 #line 15 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/bv/kinds"
666 template <> Expr ExprManager::mkConst(::CVC4::BitVectorSize const& val);
667 
668 #line 24 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/bv/kinds"
669 template <> Expr ExprManager::mkConst(::CVC4::BitVector const& val);
670 
671 #line 73 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/bv/kinds"
672 template <> Expr ExprManager::mkConst(::CVC4::BitVectorBitOf const& val);
673 
674 #line 79 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/bv/kinds"
675 template <> Expr ExprManager::mkConst(::CVC4::BitVectorExtract const& val);
676 
677 #line 85 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/bv/kinds"
678 template <> Expr ExprManager::mkConst(::CVC4::BitVectorRepeat const& val);
679 
680 #line 91 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/bv/kinds"
681 template <> Expr ExprManager::mkConst(::CVC4::BitVectorZeroExtend const& val);
682 
683 #line 97 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/bv/kinds"
684 template <> Expr ExprManager::mkConst(::CVC4::BitVectorSignExtend const& val);
685 
686 #line 103 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/bv/kinds"
687 template <> Expr ExprManager::mkConst(::CVC4::BitVectorRotateLeft const& val);
688 
689 #line 109 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/bv/kinds"
690 template <> Expr ExprManager::mkConst(::CVC4::BitVectorRotateRight const& val);
691 
692 #line 123 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/bv/kinds"
693 template <> Expr ExprManager::mkConst(::CVC4::IntToBitVector const& val);
694 
695 #line 35 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/arrays/kinds"
696 template <> Expr ExprManager::mkConst(::CVC4::ArrayStoreAll const& val);
697 
698 #line 45 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/datatypes/kinds"
699 template <> Expr ExprManager::mkConst(::CVC4::Datatype const& val);
700 
701 #line 77 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/datatypes/kinds"
702 template <> Expr ExprManager::mkConst(::CVC4::AscriptionType const& val);
703 
704 #line 107 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/datatypes/kinds"
705 template <> Expr ExprManager::mkConst(::CVC4::TupleSelect const& val);
706 
707 #line 115 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/datatypes/kinds"
708 template <> Expr ExprManager::mkConst(::CVC4::TupleUpdate const& val);
709 
710 #line 123 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/datatypes/kinds"
711 template <> Expr ExprManager::mkConst(::CVC4::Record const& val);
712 
713 #line 143 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/datatypes/kinds"
714 template <> Expr ExprManager::mkConst(::CVC4::RecordSelect const& val);
715 
716 #line 151 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/datatypes/kinds"
717 template <> Expr ExprManager::mkConst(::CVC4::RecordUpdate const& val);
718 
719 #line 50 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/strings/kinds"
720 template <> Expr ExprManager::mkConst(::CVC4::String const& val);
721 
722 #line 56 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/strings/kinds"
723 template <> Expr ExprManager::mkConst(::CVC4::RegExp const& val);
724 
725 
726 }/* CVC4 namespace */
727 
728 #endif /* __CVC4__EXPR_MANAGER_H */
A class representing a Datatype definition.
Singleton class encapsulating the real type.
Definition: type.h:389
Class encapsulating the Selector type.
Definition: type.h:662
TypeConstant
The enumeration for the built-in atomic types.
Definition: kind.h:483
void * Expr
Class encapsulating CVC4 expressions and methods for constructing new expressions.
Definition: expr.h:226
Singleton class encapsulating the integer type.
Definition: type.h:378
Class encapsulating a user-defined sort.
Definition: type.h:494
Class encapsulating a tuple type.
Definition: type.h:463
The representation of an inductive datatype.
Definition: datatype.h:382
Expr mkConst(const T &)
Create a constant of type T.
The structure representing the extraction of one Boolean bit.
Definition: bitvector.h:431
Class encapsulating CVC4 expression types.
Definition: type.h:88
A class to represent a chained, built-in operator.
Definition: chain.h:29
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:680
Singleton class encapsulating the Boolean type.
Definition: type.h:367
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
marks the upper-bound of this enumeration
Definition: kind.h:241
Representation of subrange bounds.
Exception thrown in the case of type-checking errors.
Definition: expr.h:150
Class encapsulating an array type.
Definition: type.h:477
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
Class encapsulating a function type.
Definition: type.h:411
Class encapsulating a user-defined sort constructor.
Definition: type.h:515
Class encapsulating the datatype type.
Definition: type.h:594
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:449
A class used to parameterize a type ascription.
[[ Add one-line brief description here ]]
Class encapsulating a tuple type.
Definition: type.h:431
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:400
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:640
A constructor for a Datatype.
Definition: datatype.h:133
A simple S-expression.
Definition: sexpr.h:51
Class encapsulating the bit-vector type.
Definition: type.h:575
The structure representing the divisibility-by-k predicate.
Definition: divisible.h:32
A multi-precision rational constant.
Kind_t
Definition: kind.h:60
The structure representing the extraction operation for bit-vectors.
Definition: bitvector.h:402
Interface for expression types.