1 /********************* */
2 /*! \file expr_manager_template.cpp
4 ** Original author: dejan
5 ** Major contributors: mdeters, cconway
6 ** Minor contributors (to current version): none
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, implementation.
16 ** Public-facing expression manager interface, implementation.
19 #include "expr/node.h"
20 #include "expr/expr.h"
21 #include "expr/kind.h"
22 #include "expr/metakind.h"
23 #include "expr/type.h"
24 #include "expr/node_manager.h"
25 #include "expr/expr_manager.h"
26 #include "context/context.h"
30 // This is a hack, but an important one: if there's an error, the
31 // compiler directs the user to the template file instead of the
32 // generated one. We don't want the user to modify the generated one,
33 // since it'll get overwritten on a later build.
34 #line 35 "${template}"
37 using namespace CVC4::context
;
38 using namespace CVC4::kind
;
42 ExprManager::ExprManager() :
44 d_nodeManager(new NodeManager(d_ctxt
)) {
47 ExprManager::~ExprManager() {
52 BooleanType
ExprManager::booleanType() const {
53 NodeManagerScope
nms(d_nodeManager
);
54 return Type(d_nodeManager
, new TypeNode(d_nodeManager
->booleanType()));
57 KindType
ExprManager::kindType() const {
58 NodeManagerScope
nms(d_nodeManager
);
59 return Type(d_nodeManager
, new TypeNode(d_nodeManager
->kindType()));
62 RealType
ExprManager::realType() const {
63 NodeManagerScope
nms(d_nodeManager
);
64 return Type(d_nodeManager
, new TypeNode(d_nodeManager
->realType()));
67 IntegerType
ExprManager::integerType() const {
68 NodeManagerScope
nms(d_nodeManager
);
69 return Type(d_nodeManager
, new TypeNode(d_nodeManager
->integerType()));
72 Expr
ExprManager::mkExpr(Kind kind
, const Expr
& child1
) {
74 CheckArgument(n
>= minArity(kind
) && n
<= maxArity(kind
), kind
,
75 "Exprs with kind %s must have at least %u children and "
76 "at most %u children (the one under construction has %u)",
77 kind::kindToString(kind
).c_str(),
78 minArity(kind
), maxArity(kind
), n
);
79 NodeManagerScope
nms(d_nodeManager
);
81 return Expr(this, d_nodeManager
->mkNodePtr(kind
, child1
.getNode()));
82 } catch (const TypeCheckingExceptionPrivate
& e
) {
83 throw TypeCheckingException(Expr(this, new Node(e
.getNode())), e
.getMessage());
87 Expr
ExprManager::mkExpr(Kind kind
, const Expr
& child1
, const Expr
& child2
) {
89 CheckArgument(n
>= minArity(kind
) && n
<= maxArity(kind
), kind
,
90 "Exprs with kind %s must have at least %u children and "
91 "at most %u children (the one under construction has %u)",
92 kind::kindToString(kind
).c_str(),
93 minArity(kind
), maxArity(kind
), n
);
94 NodeManagerScope
nms(d_nodeManager
);
96 return Expr(this, d_nodeManager
->mkNodePtr(kind
,
99 } catch (const TypeCheckingExceptionPrivate
& e
) {
100 throw TypeCheckingException(Expr(this, new Node(e
.getNode())),
105 Expr
ExprManager::mkExpr(Kind kind
, const Expr
& child1
, const Expr
& child2
,
106 const Expr
& child3
) {
107 const unsigned n
= 3;
108 CheckArgument(n
>= minArity(kind
) && n
<= maxArity(kind
), kind
,
109 "Exprs with kind %s must have at least %u children and "
110 "at most %u children (the one under construction has %u)",
111 kind::kindToString(kind
).c_str(),
112 minArity(kind
), maxArity(kind
), n
);
113 NodeManagerScope
nms(d_nodeManager
);
115 return Expr(this, d_nodeManager
->mkNodePtr(kind
,
119 } catch (const TypeCheckingExceptionPrivate
& e
) {
120 throw TypeCheckingException(Expr(this, new Node(e
.getNode())),
125 Expr
ExprManager::mkExpr(Kind kind
, const Expr
& child1
, const Expr
& child2
,
126 const Expr
& child3
, const Expr
& child4
) {
127 const unsigned n
= 4;
128 CheckArgument(n
>= minArity(kind
) && n
<= maxArity(kind
), kind
,
129 "Exprs with kind %s must have at least %u children and "
130 "at most %u children (the one under construction has %u)",
131 kind::kindToString(kind
).c_str(),
132 minArity(kind
), maxArity(kind
), n
);
133 NodeManagerScope
nms(d_nodeManager
);
135 return Expr(this, d_nodeManager
->mkNodePtr(kind
,
140 } catch (const TypeCheckingExceptionPrivate
& e
) {
141 throw TypeCheckingException(Expr(this, new Node(e
.getNode())),
146 Expr
ExprManager::mkExpr(Kind kind
, const Expr
& child1
, const Expr
& child2
,
147 const Expr
& child3
, const Expr
& child4
,
148 const Expr
& child5
) {
149 const unsigned n
= 5;
150 CheckArgument(n
>= minArity(kind
) && n
<= maxArity(kind
), kind
,
151 "Exprs with kind %s must have at least %u children and "
152 "at most %u children (the one under construction has %u)",
153 kind::kindToString(kind
).c_str(),
154 minArity(kind
), maxArity(kind
), n
);
155 NodeManagerScope
nms(d_nodeManager
);
157 return Expr(this, d_nodeManager
->mkNodePtr(kind
,
163 } catch (const TypeCheckingExceptionPrivate
& e
) {
164 throw TypeCheckingException(Expr(this, new Node(e
.getNode())),
169 Expr
ExprManager::mkExpr(Kind kind
, const std::vector
<Expr
>& children
) {
170 const unsigned n
= children
.size();
171 CheckArgument(n
>= minArity(kind
) && n
<= maxArity(kind
), kind
,
172 "Exprs with kind %s must have at least %u children and "
173 "at most %u children (the one under construction has %u)",
174 kind::kindToString(kind
).c_str(),
175 minArity(kind
), maxArity(kind
), n
);
177 NodeManagerScope
nms(d_nodeManager
);
180 vector
<Expr
>::const_iterator it
= children
.begin();
181 vector
<Expr
>::const_iterator it_end
= children
.end();
182 while(it
!= it_end
) {
183 nodes
.push_back(it
->getNode());
187 return Expr(this, d_nodeManager
->mkNodePtr(kind
, nodes
));
188 } catch (const TypeCheckingExceptionPrivate
& e
) {
189 throw TypeCheckingException(Expr(this, new Node(e
.getNode())),
194 Expr
ExprManager::mkExpr(Expr opExpr
, const std::vector
<Expr
>& children
) {
195 const unsigned n
= children
.size();
196 Kind kind
= kind::operatorKindToKind(opExpr
.getKind());
197 CheckArgument(n
>= minArity(kind
) && n
<= maxArity(kind
), kind
,
198 "Exprs with kind %s must have at least %u children and "
199 "at most %u children (the one under construction has %u)",
200 kind::kindToString(kind
).c_str(),
201 minArity(kind
), maxArity(kind
), n
);
203 NodeManagerScope
nms(d_nodeManager
);
206 vector
<Expr
>::const_iterator it
= children
.begin();
207 vector
<Expr
>::const_iterator it_end
= children
.end();
208 while(it
!= it_end
) {
209 nodes
.push_back(it
->getNode());
213 return Expr(this,d_nodeManager
->mkNodePtr(opExpr
.getNode(), nodes
));
214 } catch (const TypeCheckingExceptionPrivate
& e
) {
215 throw TypeCheckingException(Expr(this, new Node(e
.getNode())), e
.getMessage());
219 /** Make a function type from domain to range. */
220 FunctionType
ExprManager::mkFunctionType(const Type
& domain
, const Type
& range
) {
221 NodeManagerScope
nms(d_nodeManager
);
222 return Type(d_nodeManager
, new TypeNode(d_nodeManager
->mkFunctionType(*domain
.d_typeNode
, *range
.d_typeNode
)));
225 /** Make a function type with input types from argTypes. */
226 FunctionType
ExprManager::mkFunctionType(const std::vector
<Type
>& argTypes
, const Type
& range
) {
227 Assert( argTypes
.size() >= 1 );
228 NodeManagerScope
nms(d_nodeManager
);
229 std::vector
<TypeNode
> argTypeNodes
;
230 for (unsigned i
= 0, i_end
= argTypes
.size(); i
< i_end
; ++ i
) {
231 argTypeNodes
.push_back(*argTypes
[i
].d_typeNode
);
233 return Type(d_nodeManager
, new TypeNode(d_nodeManager
->mkFunctionType(argTypeNodes
, *range
.d_typeNode
)));
236 FunctionType
ExprManager::mkFunctionType(const std::vector
<Type
>& sorts
) {
237 Assert( sorts
.size() >= 2 );
238 NodeManagerScope
nms(d_nodeManager
);
239 std::vector
<TypeNode
> sortNodes
;
240 for (unsigned i
= 0, i_end
= sorts
.size(); i
< i_end
; ++ i
) {
241 sortNodes
.push_back(*sorts
[i
].d_typeNode
);
243 return Type(d_nodeManager
, new TypeNode(d_nodeManager
->mkFunctionType(sortNodes
)));
246 FunctionType
ExprManager::mkPredicateType(const std::vector
<Type
>& sorts
) {
247 Assert( sorts
.size() >= 1 );
248 NodeManagerScope
nms(d_nodeManager
);
249 std::vector
<TypeNode
> sortNodes
;
250 for (unsigned i
= 0, i_end
= sorts
.size(); i
< i_end
; ++ i
) {
251 sortNodes
.push_back(*sorts
[i
].d_typeNode
);
253 return Type(d_nodeManager
, new TypeNode(d_nodeManager
->mkPredicateType(sortNodes
)));
256 TupleType
ExprManager::mkTupleType(const std::vector
<Type
>& types
) {
257 Assert( types
.size() >= 2 );
258 NodeManagerScope
nms(d_nodeManager
);
259 std::vector
<TypeNode
> typeNodes
;
260 for (unsigned i
= 0, i_end
= types
.size(); i
< i_end
; ++ i
) {
261 typeNodes
.push_back(*types
[i
].d_typeNode
);
263 return Type(d_nodeManager
, new TypeNode(d_nodeManager
->mkTupleType(typeNodes
)));
266 BitVectorType
ExprManager::mkBitVectorType(unsigned size
) const {
267 NodeManagerScope
nms(d_nodeManager
);
268 return Type(d_nodeManager
, new TypeNode(d_nodeManager
->mkBitVectorType(size
)));
271 ArrayType
ExprManager::mkArrayType(Type indexType
, Type constituentType
) const {
272 NodeManagerScope
nms(d_nodeManager
);
273 return Type(d_nodeManager
, new TypeNode(d_nodeManager
->mkArrayType(*indexType
.d_typeNode
, *constituentType
.d_typeNode
)));
276 SortType
ExprManager::mkSort(const std::string
& name
) const {
277 NodeManagerScope
nms(d_nodeManager
);
278 return Type(d_nodeManager
, new TypeNode(d_nodeManager
->mkSort(name
)));
282 * Get the type for the given Expr and optionally do type checking.
284 * Initial type computation will be near-constant time if
285 * type checking is not requested. Results are memoized, so that
286 * subsequent calls to getType() without type checking will be
289 * Initial type checking is linear in the size of the expression.
290 * Again, the results are memoized, so that subsequent calls to
291 * getType(), with or without type checking, will be constant
294 * NOTE: A TypeCheckingException can be thrown even when type
295 * checking is not requested. getType() will always return a
296 * valid and correct type and, thus, an exception will be thrown
297 * when no valid or correct type can be computed (e.g., if the
298 * arguments to a bit-vector operation aren't bit-vectors). When
299 * type checking is not requested, getType() will do the minimum
300 * amount of checking required to return a valid result.
302 * @param n the Expr for which we want a type
303 * @param check whether we should check the type as we compute it
306 Type
ExprManager::getType(const Expr
& e
, bool check
) throw (TypeCheckingException
) {
307 NodeManagerScope
nms(d_nodeManager
);
310 t
= Type(d_nodeManager
, new TypeNode(d_nodeManager
->getType(e
.getNode(), check
)));
311 } catch (const TypeCheckingExceptionPrivate
& e
) {
312 throw TypeCheckingException(Expr(this, new Node(e
.getNode())), e
.getMessage());
317 Expr
ExprManager::mkVar(const std::string
& name
, const Type
& type
) {
318 NodeManagerScope
nms(d_nodeManager
);
319 return Expr(this, d_nodeManager
->mkVarPtr(name
, *type
.d_typeNode
));
322 Expr
ExprManager::mkVar(const Type
& type
) {
323 NodeManagerScope
nms(d_nodeManager
);
324 return Expr(this, d_nodeManager
->mkVarPtr(*type
.d_typeNode
));
327 Expr
ExprManager::mkAssociative(Kind kind
,
328 const std::vector
<Expr
>& children
) {
329 CheckArgument( kind::isAssociative(kind
), kind
,
330 "Illegal kind in mkAssociative: %s",
331 kind::kindToString(kind
).c_str());
333 NodeManagerScope
nms(d_nodeManager
);
334 const unsigned int max
= maxArity(kind
);
335 const unsigned int min
= minArity(kind
);
336 unsigned int numChildren
= children
.size();
338 /* If the number of children is within bounds, then there's nothing to do. */
339 if( numChildren
<= max
) {
340 return mkExpr(kind
,children
);
343 std::vector
<Expr
>::const_iterator it
= children
.begin() ;
344 std::vector
<Expr
>::const_iterator end
= children
.end() ;
346 /* The new top-level children and the children of each sub node */
347 std::vector
<Node
> newChildren
;
348 std::vector
<Node
> subChildren
;
350 while( it
!= end
&& numChildren
> max
) {
351 /* Grab the next max children and make a node for them. */
352 for( std::vector
<Expr
>::const_iterator next
= it
+ max
;
354 ++it
, --numChildren
) {
355 subChildren
.push_back(it
->getNode());
357 Node subNode
= d_nodeManager
->mkNode(kind
,subChildren
);
358 newChildren
.push_back(subNode
);
363 /* If there's children left, "top off" the Expr. */
364 if(numChildren
> 0) {
365 /* If the leftovers are too few, just copy them into newChildren;
366 * otherwise make a new sub-node */
367 if(numChildren
< min
) {
368 for(; it
!= end
; ++it
) {
369 newChildren
.push_back(it
->getNode());
372 for(; it
!= end
; ++it
) {
373 subChildren
.push_back(it
->getNode());
375 Node subNode
= d_nodeManager
->mkNode(kind
, subChildren
);
376 newChildren
.push_back(subNode
);
380 /* It's inconceivable we could have enough children for this to fail
381 * (more than 2^32, in most cases?). */
382 AlwaysAssert( newChildren
.size() <= max
,
383 "Too many new children in mkAssociative" );
385 /* It would be really weird if this happened (it would require
386 * min > 2, for one thing), but let's make sure. */
387 AlwaysAssert( newChildren
.size() >= min
,
388 "Too few new children in mkAssociative" );
390 return Expr(this, d_nodeManager
->mkNodePtr(kind
,newChildren
) );
393 unsigned ExprManager::minArity(Kind kind
) {
394 return metakind::getLowerBoundForKind(kind
);
397 unsigned ExprManager::maxArity(Kind kind
) {
398 return metakind::getUpperBoundForKind(kind
);
401 NodeManager
* ExprManager::getNodeManager() const {
402 return d_nodeManager
;
405 Context
* ExprManager::getContext() const {
409 $
{mkConst_implementations
}
411 }/* CVC4 namespace */