aaaaf0026fbd9d6ef6b4881b0a52d7e7485be665
1 /********************* */
2 /*! \file expr_manager_template.h
4 ** Original author: dejan
5 ** Major contributors: cconway, mdeters
6 ** Minor contributors (to current version): taking
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief Public-facing expression manager interface.
16 ** Public-facing expression manager interface.
19 #include "cvc4_public.h"
21 #ifndef __CVC4__EXPR_MANAGER_H
22 #define __CVC4__EXPR_MANAGER_H
26 #include "expr/kind.h"
27 #include "expr/type.h"
28 #include "expr/expr.h"
32 // This is a hack, but an important one: if there's an error, the
33 // compiler directs the user to the template file instead of the
34 // generated one. We don't want the user to modify the generated one,
35 // since it'll get overwritten on a later build.
36 #line 37 "${template}"
46 }/* CVC4::context namespace */
48 class CVC4_PUBLIC ExprManager
{
51 context::Context
* d_ctxt
;
53 /** The internal node manager */
54 NodeManager
* d_nodeManager
;
57 * Returns the internal node manager. This should only be used by
58 * internal users, i.e. the friend classes.
60 NodeManager
* getNodeManager() const;
63 * Returns the internal Context. Used by internal users, i.e. the
66 context::Context
* getContext() const;
69 * SmtEngine will use all the internals, so it will grab the
72 friend class SmtEngine
;
74 /** ExprManagerScope reaches in to get the NodeManager */
75 friend class ExprManagerScope
;
80 * Creates an expression manager.
85 * Destroys the expression manager. No will be deallocated at this point, so
86 * any expression references that used to be managed by this expression
87 * manager and are left-over are bad.
91 /** Get the type for booleans */
92 BooleanType
booleanType() const;
94 /** Get the type for sorts. */
95 KindType
kindType() const;
97 /** Get the type for reals. */
98 RealType
realType() const;
100 /** Get the type for integers */
101 IntegerType
integerType() const;
104 * Make a unary expression of a given kind (NOT, BVNOT, ...).
105 * @param child1 kind the kind of expression
106 * @return the expression
108 Expr
mkExpr(Kind kind
, const Expr
& child1
);
111 * Make a binary expression of a given kind (AND, PLUS, ...).
112 * @param kind the kind of expression
113 * @param child1 the first child of the new expression
114 * @param child2 the second child of the new expression
115 * @return the expression
117 Expr
mkExpr(Kind kind
, const Expr
& child1
, const Expr
& child2
);
120 * Make a 3-ary expression of a given kind (AND, PLUS, ...).
121 * @param kind the kind of expression
122 * @param child1 the first child of the new expression
123 * @param child2 the second child of the new expression
124 * @param child3 the third child of the new expression
125 * @return the expression
127 Expr
mkExpr(Kind kind
, const Expr
& child1
, const Expr
& child2
,
131 * Make a 4-ary expression of a given kind (AND, PLUS, ...).
132 * @param kind the kind of expression
133 * @param child1 the first child of the new expression
134 * @param child2 the second child of the new expression
135 * @param child3 the third child of the new expression
136 * @param child4 the fourth child of the new expression
137 * @return the expression
139 Expr
mkExpr(Kind kind
, const Expr
& child1
, const Expr
& child2
,
140 const Expr
& child3
, const Expr
& child4
);
143 * Make a 5-ary expression of a given kind (AND, PLUS, ...).
144 * @param kind the kind of expression
145 * @param child1 the first child of the new expression
146 * @param child2 the second child of the new expression
147 * @param child3 the third child of the new expression
148 * @param child4 the fourth child of the new expression
149 * @param child5 the fifth child of the new expression
150 * @return the expression
152 Expr
mkExpr(Kind kind
, const Expr
& child1
, const Expr
& child2
,
153 const Expr
& child3
, const Expr
& child4
, const Expr
& child5
);
156 * Make an n-ary expression of given kind given a vector of it's children
157 * @param kind the kind of expression to build
158 * @param children the subexpressions
159 * @return the n-ary expression
161 Expr
mkExpr(Kind kind
, const std::vector
<Expr
>& children
);
164 * Make an n-ary expression of given tre operator to appply and a vector of
166 * @param opExpr the operator expression
167 * @param children the subexpressions
168 * @return the n-ary expression
170 Expr
mkExpr(Expr opExpr
, const std::vector
<Expr
>& children
);
172 /** Create a constant of type T */
174 Expr
mkConst(const T
&);
176 /** Create an Expr by applying an associative operator to the children.
177 * If <code>children.size()</code> is greater than the max arity for
178 * <code>kind</code>, then the expression will be broken up into
179 * suitably-sized chunks, taking advantage of the associativity of
180 * <code>kind</code>. For example, if kind <code>FOO</code> has max arity
181 * 2, then calling <code>mkAssociative(FOO,a,b,c)</code> will return
182 * <code>(FOO (FOO a b) c)</code> or code>(FOO a (FOO b c))</code>.
183 * The order of the arguments will be preserved in a left-to-right
184 * traversal of the resulting tree.
186 Expr
mkAssociative(Kind kind
, const std::vector
<Expr
>& children
);
189 /** Make a function type from domain to range. */
190 FunctionType
mkFunctionType(const Type
& domain
, const Type
& range
);
193 * Make a function type with input types from argTypes.
194 * <code>argTypes</code> must have at least one element.
196 FunctionType
mkFunctionType(const std::vector
<Type
>& argTypes
, const Type
& range
);
199 * Make a function type with input types from
200 * <code>sorts[0..sorts.size()-2]</code> and result type
201 * <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have
202 * at least 2 elements.
204 FunctionType
mkFunctionType(const std::vector
<Type
>& sorts
);
207 * Make a predicate type with input types from
208 * <code>sorts</code>. The result with be a function type with range
209 * <code>BOOLEAN</code>. <code>sorts</code> must have at least one
212 FunctionType
mkPredicateType(const std::vector
<Type
>& sorts
);
215 * Make a tuple type with types from
216 * <code>types[0..types.size()-1]</code>. <code>types</code> must
217 * have at least 2 elements.
219 TupleType
mkTupleType(const std::vector
<Type
>& types
);
221 /** Make a type representing a bit-vector of the given size */
222 BitVectorType
mkBitVectorType(unsigned size
) const;
224 /** Make the type of arrays with the given parameterization */
225 ArrayType
mkArrayType(Type indexType
, Type constituentType
) const;
227 /** Make a new sort with the given name. */
228 SortType
mkSort(const std::string
& name
) const;
230 /** Get the type of an expression */
231 Type
getType(const Expr
& e
, bool check
= false)
232 throw (TypeCheckingException
);
234 // variables are special, because duplicates are permitted
235 Expr
mkVar(const std::string
& name
, const Type
& type
);
236 Expr
mkVar(const Type
& type
);
238 /** Returns the minimum arity of the given kind. */
239 static unsigned minArity(Kind kind
);
241 /** Returns the maximum arity of the given kind. */
242 static unsigned maxArity(Kind kind
);
245 $
{mkConst_instantiations
}
247 }/* CVC4 namespace */
249 #endif /* __CVC4__EXPR_MANAGER_H */