1 /********************* */
2 /*! \file expr_manager_template.h
4 ** Original author: dejan
5 ** Major contributors: mdeters
6 ** Minor contributors (to current version): taking, cconway
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
&);
177 * Create an Expr by applying an associative operator to the children.
178 * If <code>children.size()</code> is greater than the max arity for
179 * <code>kind</code>, then the expression will be broken up into
180 * suitably-sized chunks, taking advantage of the associativity of
181 * <code>kind</code>. For example, if kind <code>FOO</code> has max arity
182 * 2, then calling <code>mkAssociative(FOO,a,b,c)</code> will return
183 * <code>(FOO (FOO a b) c)</code> or code>(FOO a (FOO b c))</code>.
184 * The order of the arguments will be preserved in a left-to-right
185 * traversal of the resulting tree.
187 Expr
mkAssociative(Kind kind
, const std::vector
<Expr
>& children
);
190 /** Make a function type from domain to range. */
191 FunctionType
mkFunctionType(const Type
& domain
, const Type
& range
);
194 * Make a function type with input types from argTypes.
195 * <code>argTypes</code> must have at least one element.
197 FunctionType
mkFunctionType(const std::vector
<Type
>& argTypes
, const Type
& range
);
200 * Make a function type with input types from
201 * <code>sorts[0..sorts.size()-2]</code> and result type
202 * <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have
203 * at least 2 elements.
205 FunctionType
mkFunctionType(const std::vector
<Type
>& sorts
);
208 * Make a predicate type with input types from
209 * <code>sorts</code>. The result with be a function type with range
210 * <code>BOOLEAN</code>. <code>sorts</code> must have at least one
213 FunctionType
mkPredicateType(const std::vector
<Type
>& sorts
);
216 * Make a tuple type with types from
217 * <code>types[0..types.size()-1]</code>. <code>types</code> must
218 * have at least 2 elements.
220 TupleType
mkTupleType(const std::vector
<Type
>& types
);
222 /** Make a type representing a bit-vector of the given size */
223 BitVectorType
mkBitVectorType(unsigned size
) const;
225 /** Make the type of arrays with the given parameterization */
226 ArrayType
mkArrayType(Type indexType
, Type constituentType
) const;
228 /** Make a new sort with the given name. */
229 SortType
mkSort(const std::string
& name
) const;
231 /** Make a new sort from a constructor */
232 SortType
mkSort(SortConstructorType constructor
,
233 const std::vector
<TypeNode
>& children
) const;
235 /** Make a sort constructor from a name and arity */
236 SortConstructorType
mkSortConstructor(const std::string
& name
,
239 /** Get the type of an expression */
240 Type
getType(const Expr
& e
, bool check
= false)
241 throw (TypeCheckingException
);
243 // variables are special, because duplicates are permitted
244 Expr
mkVar(const std::string
& name
, const Type
& type
);
245 Expr
mkVar(const Type
& type
);
247 /** Returns the minimum arity of the given kind. */
248 static unsigned minArity(Kind kind
);
250 /** Returns the maximum arity of the given kind. */
251 static unsigned maxArity(Kind kind
);
254 $
{mkConst_instantiations
}
256 }/* CVC4 namespace */
258 #endif /* __CVC4__EXPR_MANAGER_H */