1 /********************* */
2 /*! \file expr_manager_template.cpp
4 ** Original author: Morgan Deters
5 ** Major contributors: Dejan Jovanovic, Christopher L. Conway
6 ** Minor contributors (to current version): Kshitij Bansal, Andrew Reynolds
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2013 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief Public-facing expression manager interface, implementation
14 ** Public-facing expression manager interface, implementation.
17 #include "expr/node_manager.h"
18 #include "expr/expr_manager.h"
19 #include "expr/variable_type_map.h"
20 #include "context/context.h"
21 #include "options/options.h"
22 #include "util/statistics_registry.h"
28 // This is a hack, but an important one: if there's an error, the
29 // compiler directs the user to the template file instead of the
30 // generated one. We don't want the user to modify the generated one,
31 // since it'll get overwritten on a later build.
32 #line 33 "${template}"
34 #ifdef CVC4_STATISTICS_ON
35 #define INC_STAT(kind) \
37 if (d_exprStatistics[kind] == NULL) { \
38 stringstream statName; \
39 statName << "expr::ExprManager::" << kind; \
40 d_exprStatistics[kind] = new IntStat(statName.str(), 0); \
41 d_nodeManager->getStatisticsRegistry()->registerStat_(d_exprStatistics[kind]); \
43 ++ *(d_exprStatistics[kind]); \
45 #define INC_STAT_VAR(type, bound_var) \
47 TypeNode* typeNode = Type::getTypeNode(type); \
48 TypeConstant type = typeNode->getKind() == kind::TYPE_CONSTANT ? typeNode->getConst<TypeConstant>() : LAST_TYPE; \
49 if (d_exprStatisticsVars[type] == NULL) { \
50 stringstream statName; \
51 if (type == LAST_TYPE) { \
52 statName << "expr::ExprManager::" << ((bound_var) ? "BOUND_VARIABLE" : "VARIABLE") << ":Parameterized type"; \
54 statName << "expr::ExprManager::" << ((bound_var) ? "BOUND_VARIABLE" : "VARIABLE") << ":" << type; \
56 d_exprStatisticsVars[type] = new IntStat(statName.str(), 0); \
57 d_nodeManager->getStatisticsRegistry()->registerStat_(d_exprStatisticsVars[type]); \
59 ++ *(d_exprStatisticsVars[type]); \
62 #define INC_STAT(kind)
63 #define INC_STAT_VAR(type, bound_var)
67 using namespace CVC4::context
;
68 using namespace CVC4::kind
;
72 ExprManager::ExprManager() :
73 d_ctxt(new Context()),
74 d_nodeManager(new NodeManager(d_ctxt
, this)) {
75 #ifdef CVC4_STATISTICS_ON
76 for (unsigned i
= 0; i
< kind::LAST_KIND
; ++ i
) {
77 d_exprStatistics
[i
] = NULL
;
79 for (unsigned i
= 0; i
< LAST_TYPE
; ++ i
) {
80 d_exprStatisticsVars
[i
] = NULL
;
85 ExprManager::ExprManager(const Options
& options
) :
86 d_ctxt(new Context()),
87 d_nodeManager(new NodeManager(d_ctxt
, this, options
)) {
88 #ifdef CVC4_STATISTICS_ON
89 for (unsigned i
= 0; i
< LAST_TYPE
; ++ i
) {
90 d_exprStatisticsVars
[i
] = NULL
;
92 for (unsigned i
= 0; i
< kind::LAST_KIND
; ++ i
) {
93 d_exprStatistics
[i
] = NULL
;
98 ExprManager::~ExprManager() throw() {
99 NodeManagerScope
nms(d_nodeManager
);
103 #ifdef CVC4_STATISTICS_ON
104 for (unsigned i
= 0; i
< kind::LAST_KIND
; ++ i
) {
105 if (d_exprStatistics
[i
] != NULL
) {
106 d_nodeManager
->getStatisticsRegistry()->unregisterStat_(d_exprStatistics
[i
]);
107 delete d_exprStatistics
[i
];
110 for (unsigned i
= 0; i
< LAST_TYPE
; ++ i
) {
111 if (d_exprStatisticsVars
[i
] != NULL
) {
112 d_nodeManager
->getStatisticsRegistry()->unregisterStat_(d_exprStatisticsVars
[i
]);
113 delete d_exprStatisticsVars
[i
];
118 delete d_nodeManager
;
121 } catch(Exception
& e
) {
122 Warning() << "CVC4 threw an exception during cleanup." << std::endl
127 StatisticsRegistry
* ExprManager::getStatisticsRegistry() throw() {
128 return d_nodeManager
->getStatisticsRegistry();
131 const Options
& ExprManager::getOptions() const {
132 return d_nodeManager
->getOptions();
135 BooleanType
ExprManager::booleanType() const {
136 NodeManagerScope
nms(d_nodeManager
);
137 return BooleanType(Type(d_nodeManager
, new TypeNode(d_nodeManager
->booleanType())));
140 StringType
ExprManager::stringType() const {
141 NodeManagerScope
nms(d_nodeManager
);
142 return StringType(Type(d_nodeManager
, new TypeNode(d_nodeManager
->stringType())));
145 RealType
ExprManager::realType() const {
146 NodeManagerScope
nms(d_nodeManager
);
147 return RealType(Type(d_nodeManager
, new TypeNode(d_nodeManager
->realType())));
150 IntegerType
ExprManager::integerType() const {
151 NodeManagerScope
nms(d_nodeManager
);
152 return IntegerType(Type(d_nodeManager
, new TypeNode(d_nodeManager
->integerType())));
155 Expr
ExprManager::mkExpr(Kind kind
, Expr child1
) {
156 const unsigned n
= 1 - (kind::metaKindOf(kind
) == kind::metakind::PARAMETERIZED
? 1 : 0);
157 CheckArgument(n
>= minArity(kind
) && n
<= maxArity(kind
), kind
,
158 "Exprs with kind %s must have at least %u children and "
159 "at most %u children (the one under construction has %u)",
160 kind::kindToString(kind
).c_str(),
161 minArity(kind
), maxArity(kind
), n
);
162 NodeManagerScope
nms(d_nodeManager
);
165 return Expr(this, d_nodeManager
->mkNodePtr(kind
, child1
.getNode()));
166 } catch (const TypeCheckingExceptionPrivate
& e
) {
167 throw TypeCheckingException(this, &e
);
171 Expr
ExprManager::mkExpr(Kind kind
, Expr child1
, Expr child2
) {
172 const unsigned n
= 2 - (kind::metaKindOf(kind
) == kind::metakind::PARAMETERIZED
? 1 : 0);
173 CheckArgument(n
>= minArity(kind
) && n
<= maxArity(kind
), kind
,
174 "Exprs with kind %s must have at least %u children and "
175 "at most %u children (the one under construction has %u)",
176 kind::kindToString(kind
).c_str(),
177 minArity(kind
), maxArity(kind
), n
);
178 NodeManagerScope
nms(d_nodeManager
);
181 return Expr(this, d_nodeManager
->mkNodePtr(kind
,
184 } catch (const TypeCheckingExceptionPrivate
& e
) {
185 throw TypeCheckingException(this, &e
);
189 Expr
ExprManager::mkExpr(Kind kind
, Expr child1
, Expr child2
,
191 const unsigned n
= 3 - (kind::metaKindOf(kind
) == kind::metakind::PARAMETERIZED
? 1 : 0);
192 CheckArgument(n
>= minArity(kind
) && n
<= maxArity(kind
), kind
,
193 "Exprs with kind %s must have at least %u children and "
194 "at most %u children (the one under construction has %u)",
195 kind::kindToString(kind
).c_str(),
196 minArity(kind
), maxArity(kind
), n
);
197 NodeManagerScope
nms(d_nodeManager
);
200 return Expr(this, d_nodeManager
->mkNodePtr(kind
,
204 } catch (const TypeCheckingExceptionPrivate
& e
) {
205 throw TypeCheckingException(this, &e
);
209 Expr
ExprManager::mkExpr(Kind kind
, Expr child1
, Expr child2
,
210 Expr child3
, Expr child4
) {
211 const unsigned n
= 4 - (kind::metaKindOf(kind
) == kind::metakind::PARAMETERIZED
? 1 : 0);
212 CheckArgument(n
>= minArity(kind
) && n
<= maxArity(kind
), kind
,
213 "Exprs with kind %s must have at least %u children and "
214 "at most %u children (the one under construction has %u)",
215 kind::kindToString(kind
).c_str(),
216 minArity(kind
), maxArity(kind
), n
);
217 NodeManagerScope
nms(d_nodeManager
);
220 return Expr(this, d_nodeManager
->mkNodePtr(kind
,
225 } catch (const TypeCheckingExceptionPrivate
& e
) {
226 throw TypeCheckingException(this, &e
);
230 Expr
ExprManager::mkExpr(Kind kind
, Expr child1
, Expr child2
,
231 Expr child3
, Expr child4
,
233 const unsigned n
= 5 - (kind::metaKindOf(kind
) == kind::metakind::PARAMETERIZED
? 1 : 0);
234 CheckArgument(n
>= minArity(kind
) && n
<= maxArity(kind
), kind
,
235 "Exprs with kind %s must have at least %u children and "
236 "at most %u children (the one under construction has %u)",
237 kind::kindToString(kind
).c_str(),
238 minArity(kind
), maxArity(kind
), n
);
239 NodeManagerScope
nms(d_nodeManager
);
242 return Expr(this, d_nodeManager
->mkNodePtr(kind
,
248 } catch (const TypeCheckingExceptionPrivate
& e
) {
249 throw TypeCheckingException(this, &e
);
253 Expr
ExprManager::mkExpr(Kind kind
, const std::vector
<Expr
>& children
) {
254 const unsigned n
= children
.size() - (kind::metaKindOf(kind
) == kind::metakind::PARAMETERIZED
? 1 : 0);
255 CheckArgument(n
>= minArity(kind
) && n
<= maxArity(kind
), kind
,
256 "Exprs with kind %s must have at least %u children and "
257 "at most %u children (the one under construction has %u)",
258 kind::kindToString(kind
).c_str(),
259 minArity(kind
), maxArity(kind
), n
);
261 NodeManagerScope
nms(d_nodeManager
);
264 vector
<Expr
>::const_iterator it
= children
.begin();
265 vector
<Expr
>::const_iterator it_end
= children
.end();
266 while(it
!= it_end
) {
267 nodes
.push_back(it
->getNode());
272 return Expr(this, d_nodeManager
->mkNodePtr(kind
, nodes
));
273 } catch (const TypeCheckingExceptionPrivate
& e
) {
274 throw TypeCheckingException(this, &e
);
278 Expr
ExprManager::mkExpr(Kind kind
, Expr child1
, const std::vector
<Expr
>& otherChildren
) {
279 const unsigned n
= otherChildren
.size() - (kind::metaKindOf(kind
) == kind::metakind::PARAMETERIZED
? 1 : 0) + 1;
280 CheckArgument(n
>= minArity(kind
) && n
<= maxArity(kind
), kind
,
281 "Exprs with kind %s must have at least %u children and "
282 "at most %u children (the one under construction has %u)",
283 kind::kindToString(kind
).c_str(),
284 minArity(kind
), maxArity(kind
), n
);
286 NodeManagerScope
nms(d_nodeManager
);
289 nodes
.push_back(child1
.getNode());
291 vector
<Expr
>::const_iterator it
= otherChildren
.begin();
292 vector
<Expr
>::const_iterator it_end
= otherChildren
.end();
293 while(it
!= it_end
) {
294 nodes
.push_back(it
->getNode());
299 return Expr(this, d_nodeManager
->mkNodePtr(kind
, nodes
));
300 } catch (const TypeCheckingExceptionPrivate
& e
) {
301 throw TypeCheckingException(this, &e
);
305 Expr
ExprManager::mkExpr(Expr opExpr
) {
306 const unsigned n
= 0;
307 Kind kind
= NodeManager::operatorToKind(opExpr
.getNode());
308 CheckArgument(opExpr
.getKind() == kind::BUILTIN
|| kind::metaKindOf(kind
) == kind::metakind::PARAMETERIZED
, opExpr
,
309 "This Expr constructor is for parameterized kinds only");
310 CheckArgument(n
>= minArity(kind
) && n
<= maxArity(kind
), kind
,
311 "Exprs with kind %s must have at least %u children and "
312 "at most %u children (the one under construction has %u)",
313 kind::kindToString(kind
).c_str(),
314 minArity(kind
), maxArity(kind
), n
);
315 NodeManagerScope
nms(d_nodeManager
);
318 return Expr(this, d_nodeManager
->mkNodePtr(opExpr
.getNode()));
319 } catch (const TypeCheckingExceptionPrivate
& e
) {
320 throw TypeCheckingException(this, &e
);
324 Expr
ExprManager::mkExpr(Expr opExpr
, Expr child1
) {
325 const unsigned n
= 1;
326 Kind kind
= NodeManager::operatorToKind(opExpr
.getNode());
327 CheckArgument(opExpr
.getKind() == kind::BUILTIN
|| kind::metaKindOf(kind
) == kind::metakind::PARAMETERIZED
, opExpr
,
328 "This Expr constructor is for parameterized kinds only");
329 CheckArgument(n
>= minArity(kind
) && n
<= maxArity(kind
), kind
,
330 "Exprs with kind %s must have at least %u children and "
331 "at most %u children (the one under construction has %u)",
332 kind::kindToString(kind
).c_str(),
333 minArity(kind
), maxArity(kind
), n
);
334 NodeManagerScope
nms(d_nodeManager
);
337 return Expr(this, d_nodeManager
->mkNodePtr(opExpr
.getNode(), child1
.getNode()));
338 } catch (const TypeCheckingExceptionPrivate
& e
) {
339 throw TypeCheckingException(this, &e
);
343 Expr
ExprManager::mkExpr(Expr opExpr
, Expr child1
, Expr child2
) {
344 const unsigned n
= 2;
345 Kind kind
= NodeManager::operatorToKind(opExpr
.getNode());
346 CheckArgument(opExpr
.getKind() == kind::BUILTIN
|| kind::metaKindOf(kind
) == kind::metakind::PARAMETERIZED
, opExpr
,
347 "This Expr constructor is for parameterized kinds only");
348 CheckArgument(n
>= minArity(kind
) && n
<= maxArity(kind
), kind
,
349 "Exprs with kind %s must have at least %u children and "
350 "at most %u children (the one under construction has %u)",
351 kind::kindToString(kind
).c_str(),
352 minArity(kind
), maxArity(kind
), n
);
353 NodeManagerScope
nms(d_nodeManager
);
356 return Expr(this, d_nodeManager
->mkNodePtr(opExpr
.getNode(),
359 } catch (const TypeCheckingExceptionPrivate
& e
) {
360 throw TypeCheckingException(this, &e
);
364 Expr
ExprManager::mkExpr(Expr opExpr
, Expr child1
, Expr child2
, Expr child3
) {
365 const unsigned n
= 3;
366 Kind kind
= NodeManager::operatorToKind(opExpr
.getNode());
367 CheckArgument(opExpr
.getKind() == kind::BUILTIN
|| kind::metaKindOf(kind
) == kind::metakind::PARAMETERIZED
, opExpr
,
368 "This Expr constructor is for parameterized kinds only");
369 CheckArgument(n
>= minArity(kind
) && n
<= maxArity(kind
), kind
,
370 "Exprs with kind %s must have at least %u children and "
371 "at most %u children (the one under construction has %u)",
372 kind::kindToString(kind
).c_str(),
373 minArity(kind
), maxArity(kind
), n
);
374 NodeManagerScope
nms(d_nodeManager
);
377 return Expr(this, d_nodeManager
->mkNodePtr(opExpr
.getNode(),
381 } catch (const TypeCheckingExceptionPrivate
& e
) {
382 throw TypeCheckingException(this, &e
);
386 Expr
ExprManager::mkExpr(Expr opExpr
, Expr child1
, Expr child2
, Expr child3
,
388 const unsigned n
= 4;
389 Kind kind
= NodeManager::operatorToKind(opExpr
.getNode());
390 CheckArgument(opExpr
.getKind() == kind::BUILTIN
|| kind::metaKindOf(kind
) == kind::metakind::PARAMETERIZED
, opExpr
,
391 "This Expr constructor is for parameterized kinds only");
392 CheckArgument(n
>= minArity(kind
) && n
<= maxArity(kind
), kind
,
393 "Exprs with kind %s must have at least %u children and "
394 "at most %u children (the one under construction has %u)",
395 kind::kindToString(kind
).c_str(),
396 minArity(kind
), maxArity(kind
), n
);
397 NodeManagerScope
nms(d_nodeManager
);
400 return Expr(this, d_nodeManager
->mkNodePtr(opExpr
.getNode(),
405 } catch (const TypeCheckingExceptionPrivate
& e
) {
406 throw TypeCheckingException(this, &e
);
410 Expr
ExprManager::mkExpr(Expr opExpr
, Expr child1
, Expr child2
, Expr child3
,
411 Expr child4
, Expr child5
) {
412 const unsigned n
= 5;
413 Kind kind
= NodeManager::operatorToKind(opExpr
.getNode());
414 CheckArgument(opExpr
.getKind() == kind::BUILTIN
|| kind::metaKindOf(kind
) == kind::metakind::PARAMETERIZED
, opExpr
,
415 "This Expr constructor is for parameterized kinds only");
416 CheckArgument(n
>= minArity(kind
) && n
<= maxArity(kind
), kind
,
417 "Exprs with kind %s must have at least %u children and "
418 "at most %u children (the one under construction has %u)",
419 kind::kindToString(kind
).c_str(),
420 minArity(kind
), maxArity(kind
), n
);
421 NodeManagerScope
nms(d_nodeManager
);
424 return Expr(this, d_nodeManager
->mkNodePtr(opExpr
.getNode(),
430 } catch (const TypeCheckingExceptionPrivate
& e
) {
431 throw TypeCheckingException(this, &e
);
435 Expr
ExprManager::mkExpr(Expr opExpr
, const std::vector
<Expr
>& children
) {
436 const unsigned n
= children
.size();
437 Kind kind
= NodeManager::operatorToKind(opExpr
.getNode());
438 CheckArgument(opExpr
.getKind() == kind::BUILTIN
|| kind::metaKindOf(kind
) == kind::metakind::PARAMETERIZED
, opExpr
,
439 "This Expr constructor is for parameterized kinds only");
440 CheckArgument(n
>= minArity(kind
) && n
<= maxArity(kind
), kind
,
441 "Exprs with kind %s must have at least %u children and "
442 "at most %u children (the one under construction has %u)",
443 kind::kindToString(kind
).c_str(),
444 minArity(kind
), maxArity(kind
), n
);
446 NodeManagerScope
nms(d_nodeManager
);
449 vector
<Expr
>::const_iterator it
= children
.begin();
450 vector
<Expr
>::const_iterator it_end
= children
.end();
451 while(it
!= it_end
) {
452 nodes
.push_back(it
->getNode());
457 return Expr(this,d_nodeManager
->mkNodePtr(opExpr
.getNode(), nodes
));
458 } catch (const TypeCheckingExceptionPrivate
& e
) {
459 throw TypeCheckingException(this, &e
);
463 bool ExprManager::hasOperator(Kind k
) {
464 return NodeManager::hasOperator(k
);
467 Expr
ExprManager::operatorOf(Kind k
) {
468 NodeManagerScope
nms(d_nodeManager
);
470 return d_nodeManager
->operatorOf(k
).toExpr();
473 /** Make a function type from domain to range. */
474 FunctionType
ExprManager::mkFunctionType(Type domain
, Type range
) {
475 NodeManagerScope
nms(d_nodeManager
);
476 return FunctionType(Type(d_nodeManager
, new TypeNode(d_nodeManager
->mkFunctionType(*domain
.d_typeNode
, *range
.d_typeNode
))));
479 /** Make a function type with input types from argTypes. */
480 FunctionType
ExprManager::mkFunctionType(const std::vector
<Type
>& argTypes
, Type range
) {
481 NodeManagerScope
nms(d_nodeManager
);
482 Assert( argTypes
.size() >= 1 );
483 std::vector
<TypeNode
> argTypeNodes
;
484 for (unsigned i
= 0, i_end
= argTypes
.size(); i
< i_end
; ++ i
) {
485 argTypeNodes
.push_back(*argTypes
[i
].d_typeNode
);
487 return FunctionType(Type(d_nodeManager
, new TypeNode(d_nodeManager
->mkFunctionType(argTypeNodes
, *range
.d_typeNode
))));
490 FunctionType
ExprManager::mkFunctionType(const std::vector
<Type
>& sorts
) {
491 NodeManagerScope
nms(d_nodeManager
);
492 Assert( sorts
.size() >= 2 );
493 std::vector
<TypeNode
> sortNodes
;
494 for (unsigned i
= 0, i_end
= sorts
.size(); i
< i_end
; ++ i
) {
495 sortNodes
.push_back(*sorts
[i
].d_typeNode
);
497 return FunctionType(Type(d_nodeManager
, new TypeNode(d_nodeManager
->mkFunctionType(sortNodes
))));
500 FunctionType
ExprManager::mkPredicateType(const std::vector
<Type
>& sorts
) {
501 NodeManagerScope
nms(d_nodeManager
);
502 Assert( sorts
.size() >= 1 );
503 std::vector
<TypeNode
> sortNodes
;
504 for (unsigned i
= 0, i_end
= sorts
.size(); i
< i_end
; ++ i
) {
505 sortNodes
.push_back(*sorts
[i
].d_typeNode
);
507 return FunctionType(Type(d_nodeManager
, new TypeNode(d_nodeManager
->mkPredicateType(sortNodes
))));
510 TupleType
ExprManager::mkTupleType(const std::vector
<Type
>& types
) {
511 NodeManagerScope
nms(d_nodeManager
);
512 std::vector
<TypeNode
> typeNodes
;
513 for (unsigned i
= 0, i_end
= types
.size(); i
< i_end
; ++ i
) {
514 typeNodes
.push_back(*types
[i
].d_typeNode
);
516 return TupleType(Type(d_nodeManager
, new TypeNode(d_nodeManager
->mkTupleType(typeNodes
))));
519 RecordType
ExprManager::mkRecordType(const Record
& rec
) {
520 NodeManagerScope
nms(d_nodeManager
);
521 return RecordType(Type(d_nodeManager
, new TypeNode(d_nodeManager
->mkRecordType(rec
))));
524 SExprType
ExprManager::mkSExprType(const std::vector
<Type
>& types
) {
525 NodeManagerScope
nms(d_nodeManager
);
526 std::vector
<TypeNode
> typeNodes
;
527 for (unsigned i
= 0, i_end
= types
.size(); i
< i_end
; ++ i
) {
528 typeNodes
.push_back(*types
[i
].d_typeNode
);
530 return SExprType(Type(d_nodeManager
, new TypeNode(d_nodeManager
->mkSExprType(typeNodes
))));
533 BitVectorType
ExprManager::mkBitVectorType(unsigned size
) const {
534 NodeManagerScope
nms(d_nodeManager
);
535 return BitVectorType(Type(d_nodeManager
, new TypeNode(d_nodeManager
->mkBitVectorType(size
))));
538 ArrayType
ExprManager::mkArrayType(Type indexType
, Type constituentType
) const {
539 NodeManagerScope
nms(d_nodeManager
);
540 return ArrayType(Type(d_nodeManager
, new TypeNode(d_nodeManager
->mkArrayType(*indexType
.d_typeNode
, *constituentType
.d_typeNode
))));
543 DatatypeType
ExprManager::mkDatatypeType(const Datatype
& datatype
) {
544 // Not worth a special implementation; this doesn't need to be fast
546 vector
<Datatype
> datatypes
;
547 datatypes
.push_back(datatype
);
548 vector
<DatatypeType
> result
= mkMutualDatatypeTypes(datatypes
);
549 Assert(result
.size() == 1);
550 return result
.front();
553 std::vector
<DatatypeType
>
554 ExprManager::mkMutualDatatypeTypes(const std::vector
<Datatype
>& datatypes
) {
555 return mkMutualDatatypeTypes(datatypes
, set
<Type
>());
558 std::vector
<DatatypeType
>
559 ExprManager::mkMutualDatatypeTypes(const std::vector
<Datatype
>& datatypes
,
560 const std::set
<Type
>& unresolvedTypes
) {
561 NodeManagerScope
nms(d_nodeManager
);
562 std::map
<std::string
, DatatypeType
> nameResolutions
;
563 std::vector
<DatatypeType
> dtts
;
565 // First do some sanity checks, set up the final Type to be used for
566 // each datatype, and set up the "named resolutions" used to handle
567 // simple self- and mutual-recursion, for example in the definition
568 // "nat = succ(pred:nat) | zero", a named resolution can handle the
570 for(std::vector
<Datatype
>::const_iterator i
= datatypes
.begin(),
571 i_end
= datatypes
.end();
575 if( (*i
).getNumParameters() == 0 ) {
576 typeNode
= new TypeNode(d_nodeManager
->mkTypeConst(*i
));
578 TypeNode cons
= d_nodeManager
->mkTypeConst(*i
);
579 std::vector
< TypeNode
> params
;
580 params
.push_back( cons
);
581 for( unsigned int ip
= 0; ip
< (*i
).getNumParameters(); ++ip
) {
582 params
.push_back( TypeNode::fromType( (*i
).getParameter( ip
) ) );
585 typeNode
= new TypeNode(d_nodeManager
->mkTypeNode(kind::PARAMETRIC_DATATYPE
, params
));
587 Type
type(d_nodeManager
, typeNode
);
588 DatatypeType
dtt(type
);
589 CheckArgument(nameResolutions
.find((*i
).getName()) == nameResolutions
.end(),
591 "cannot construct two datatypes at the same time "
592 "with the same name `%s'",
593 (*i
).getName().c_str());
594 nameResolutions
.insert(std::make_pair((*i
).getName(), dtt
));
598 // Second, set up the type substitution map for complex type
599 // resolution (e.g. if "list" is the type we're defining, and it has
600 // a selector of type "ARRAY INT OF list", this can't be taken care
601 // of using the named resolutions that we set up above. A
602 // preliminary array type was set up, and now needs to have "list"
603 // substituted in it for the correct type.
605 // @TODO get rid of named resolutions altogether and handle
606 // everything with these resolutions?
607 std::vector
< SortConstructorType
> paramTypes
;
608 std::vector
< DatatypeType
> paramReplacements
;
609 std::vector
<Type
> placeholders
;// to hold the "unresolved placeholders"
610 std::vector
<Type
> replacements
;// to hold our final, resolved types
611 for(std::set
<Type
>::const_iterator i
= unresolvedTypes
.begin(),
612 i_end
= unresolvedTypes
.end();
616 if( (*i
).isSort() ) {
617 name
= SortType(*i
).getName();
619 Assert( (*i
).isSortConstructor() );
620 name
= SortConstructorType(*i
).getName();
622 std::map
<std::string
, DatatypeType
>::const_iterator resolver
=
623 nameResolutions
.find(name
);
624 CheckArgument(resolver
!= nameResolutions
.end(),
626 "cannot resolve type `%s'; it's not among "
627 "the datatypes being defined", name
.c_str());
628 // We will instruct the Datatype to substitute "*i" (the
629 // unresolved SortType used as a placeholder in complex types)
630 // with "(*resolver).second" (the DatatypeType we created in the
631 // first step, above).
632 if( (*i
).isSort() ) {
633 placeholders
.push_back(*i
);
634 replacements
.push_back( (*resolver
).second
);
636 Assert( (*i
).isSortConstructor() );
637 paramTypes
.push_back( SortConstructorType(*i
) );
638 paramReplacements
.push_back( (*resolver
).second
);
642 // Lastly, perform the final resolutions and checks.
643 for(std::vector
<DatatypeType
>::iterator i
= dtts
.begin(),
647 const Datatype
& dt
= (*i
).getDatatype();
648 if(!dt
.isResolved()) {
649 const_cast<Datatype
&>(dt
).resolve(this, nameResolutions
,
650 placeholders
, replacements
,
651 paramTypes
, paramReplacements
);
654 // Now run some checks, including a check to make sure that no
655 // selector is function-valued.
656 checkResolvedDatatype(*i
);
659 for(std::vector
<NodeManagerListener
*>::iterator i
= d_nodeManager
->d_listeners
.begin(); i
!= d_nodeManager
->d_listeners
.end(); ++i
) {
660 (*i
)->nmNotifyNewDatatypes(dtts
);
666 void ExprManager::checkResolvedDatatype(DatatypeType dtt
) const {
667 const Datatype
& dt
= dtt
.getDatatype();
669 AssertArgument(dt
.isResolved(), dtt
, "datatype should have been resolved");
671 // for all constructors...
672 for(Datatype::const_iterator i
= dt
.begin(), i_end
= dt
.end();
675 const DatatypeConstructor
& c
= *i
;
676 Type testerType CVC4_UNUSED
= c
.getTester().getType();
677 Assert(c
.isResolved() &&
678 testerType
.isTester() &&
679 TesterType(testerType
).getDomain() == dtt
&&
680 TesterType(testerType
).getRangeType() == booleanType(),
681 "malformed tester in datatype post-resolution");
682 Type ctorType CVC4_UNUSED
= c
.getConstructor().getType();
683 Assert(ctorType
.isConstructor() &&
684 ConstructorType(ctorType
).getArity() == c
.getNumArgs() &&
685 ConstructorType(ctorType
).getRangeType() == dtt
,
686 "malformed constructor in datatype post-resolution");
687 // for all selectors...
688 for(DatatypeConstructor::const_iterator j
= c
.begin(), j_end
= c
.end();
691 const DatatypeConstructorArg
& a
= *j
;
692 Type selectorType
= a
.getSelector().getType();
693 Assert(a
.isResolved() &&
694 selectorType
.isSelector() &&
695 SelectorType(selectorType
).getDomain() == dtt
,
696 "malformed selector in datatype post-resolution");
697 // This next one's a "hard" check, performed in non-debug builds
698 // as well; the other ones should all be guaranteed by the
699 // CVC4::Datatype class, but this actually needs to be checked.
700 AlwaysAssert(!SelectorType(selectorType
).getRangeType().d_typeNode
->isFunctionLike(),
701 "cannot put function-like things in datatypes");
706 ConstructorType
ExprManager::mkConstructorType(const DatatypeConstructor
& constructor
, Type range
) const {
707 NodeManagerScope
nms(d_nodeManager
);
708 return Type(d_nodeManager
, new TypeNode(d_nodeManager
->mkConstructorType(constructor
, *range
.d_typeNode
)));
711 SelectorType
ExprManager::mkSelectorType(Type domain
, Type range
) const {
712 NodeManagerScope
nms(d_nodeManager
);
713 return Type(d_nodeManager
, new TypeNode(d_nodeManager
->mkSelectorType(*domain
.d_typeNode
, *range
.d_typeNode
)));
716 TesterType
ExprManager::mkTesterType(Type domain
) const {
717 NodeManagerScope
nms(d_nodeManager
);
718 return Type(d_nodeManager
, new TypeNode(d_nodeManager
->mkTesterType(*domain
.d_typeNode
)));
721 SortType
ExprManager::mkSort(const std::string
& name
) const {
722 NodeManagerScope
nms(d_nodeManager
);
723 return SortType(Type(d_nodeManager
, new TypeNode(d_nodeManager
->mkSort(name
))));
726 SortConstructorType
ExprManager::mkSortConstructor(const std::string
& name
,
727 size_t arity
) const {
728 NodeManagerScope
nms(d_nodeManager
);
729 return SortConstructorType(Type(d_nodeManager
,
730 new TypeNode(d_nodeManager
->mkSortConstructor(name
, arity
))));
733 /* - not in release 1.0
734 Type ExprManager::mkPredicateSubtype(Expr lambda)
735 throw(TypeCheckingException) {
736 NodeManagerScope nms(d_nodeManager);
738 return PredicateSubtype(Type(d_nodeManager,
739 new TypeNode(d_nodeManager->mkPredicateSubtype(lambda))));
740 } catch (const TypeCheckingExceptionPrivate& e) {
741 throw TypeCheckingException(this, &e);
746 /* - not in release 1.0
747 Type ExprManager::mkPredicateSubtype(Expr lambda, Expr witness)
748 throw(TypeCheckingException) {
749 NodeManagerScope nms(d_nodeManager);
751 return PredicateSubtype(Type(d_nodeManager,
752 new TypeNode(d_nodeManager->mkPredicateSubtype(lambda, witness))));
753 } catch (const TypeCheckingExceptionPrivate& e) {
754 throw TypeCheckingException(this, &e);
759 Type
ExprManager::mkSubrangeType(const SubrangeBounds
& bounds
)
760 throw(TypeCheckingException
) {
761 NodeManagerScope
nms(d_nodeManager
);
763 return SubrangeType(Type(d_nodeManager
,
764 new TypeNode(d_nodeManager
->mkSubrangeType(bounds
))));
765 } catch (const TypeCheckingExceptionPrivate
& e
) {
766 throw TypeCheckingException(this, &e
);
771 * Get the type for the given Expr and optionally do type checking.
773 * Initial type computation will be near-constant time if
774 * type checking is not requested. Results are memoized, so that
775 * subsequent calls to getType() without type checking will be
778 * Initial type checking is linear in the size of the expression.
779 * Again, the results are memoized, so that subsequent calls to
780 * getType(), with or without type checking, will be constant
783 * NOTE: A TypeCheckingException can be thrown even when type
784 * checking is not requested. getType() will always return a
785 * valid and correct type and, thus, an exception will be thrown
786 * when no valid or correct type can be computed (e.g., if the
787 * arguments to a bit-vector operation aren't bit-vectors). When
788 * type checking is not requested, getType() will do the minimum
789 * amount of checking required to return a valid result.
791 * @param e the Expr for which we want a type
792 * @param check whether we should check the type as we compute it
795 Type
ExprManager::getType(Expr e
, bool check
) throw (TypeCheckingException
) {
796 NodeManagerScope
nms(d_nodeManager
);
799 t
= Type(d_nodeManager
,
800 new TypeNode(d_nodeManager
->getType(e
.getNode(), check
)));
801 } catch (const TypeCheckingExceptionPrivate
& e
) {
802 throw TypeCheckingException(this, &e
);
807 Expr
ExprManager::mkVar(const std::string
& name
, Type type
, uint32_t flags
) {
808 Assert(NodeManager::currentNM() == NULL
, "ExprManager::mkVar() should only be called externally, not from within CVC4 code. Please use mkSkolem().");
809 NodeManagerScope
nms(d_nodeManager
);
810 Node
* n
= d_nodeManager
->mkVarPtr(name
, *type
.d_typeNode
, flags
);
811 Debug("nm") << "set " << name
<< " on " << *n
<< std::endl
;
812 INC_STAT_VAR(type
, false);
813 return Expr(this, n
);
816 Expr
ExprManager::mkVar(Type type
, uint32_t flags
) {
817 Assert(NodeManager::currentNM() == NULL
, "ExprManager::mkVar() should only be called externally, not from within CVC4 code. Please use mkSkolem().");
818 NodeManagerScope
nms(d_nodeManager
);
819 INC_STAT_VAR(type
, false);
820 return Expr(this, d_nodeManager
->mkVarPtr(*type
.d_typeNode
, flags
));
823 Expr
ExprManager::mkBoundVar(const std::string
& name
, Type type
) {
824 NodeManagerScope
nms(d_nodeManager
);
825 Node
* n
= d_nodeManager
->mkBoundVarPtr(name
, *type
.d_typeNode
);
826 Debug("nm") << "set " << name
<< " on " << *n
<< std::endl
;
827 INC_STAT_VAR(type
, true);
828 return Expr(this, n
);
831 Expr
ExprManager::mkBoundVar(Type type
) {
832 NodeManagerScope
nms(d_nodeManager
);
833 INC_STAT_VAR(type
, true);
834 return Expr(this, d_nodeManager
->mkBoundVarPtr(*type
.d_typeNode
));
837 Expr
ExprManager::mkAssociative(Kind kind
,
838 const std::vector
<Expr
>& children
) {
839 CheckArgument( kind::isAssociative(kind
), kind
,
840 "Illegal kind in mkAssociative: %s",
841 kind::kindToString(kind
).c_str());
843 NodeManagerScope
nms(d_nodeManager
);
844 const unsigned int max
= maxArity(kind
);
845 const unsigned int min
= minArity(kind
);
846 unsigned int numChildren
= children
.size();
848 /* If the number of children is within bounds, then there's nothing to do. */
849 if( numChildren
<= max
) {
850 return mkExpr(kind
,children
);
853 std::vector
<Expr
>::const_iterator it
= children
.begin() ;
854 std::vector
<Expr
>::const_iterator end
= children
.end() ;
856 /* The new top-level children and the children of each sub node */
857 std::vector
<Node
> newChildren
;
858 std::vector
<Node
> subChildren
;
860 while( it
!= end
&& numChildren
> max
) {
861 /* Grab the next max children and make a node for them. */
862 for( std::vector
<Expr
>::const_iterator next
= it
+ max
;
864 ++it
, --numChildren
) {
865 subChildren
.push_back(it
->getNode());
867 Node subNode
= d_nodeManager
->mkNode(kind
,subChildren
);
868 newChildren
.push_back(subNode
);
873 /* If there's children left, "top off" the Expr. */
874 if(numChildren
> 0) {
875 /* If the leftovers are too few, just copy them into newChildren;
876 * otherwise make a new sub-node */
877 if(numChildren
< min
) {
878 for(; it
!= end
; ++it
) {
879 newChildren
.push_back(it
->getNode());
882 for(; it
!= end
; ++it
) {
883 subChildren
.push_back(it
->getNode());
885 Node subNode
= d_nodeManager
->mkNode(kind
, subChildren
);
886 newChildren
.push_back(subNode
);
890 /* It's inconceivable we could have enough children for this to fail
891 * (more than 2^32, in most cases?). */
892 AlwaysAssert( newChildren
.size() <= max
,
893 "Too many new children in mkAssociative" );
895 /* It would be really weird if this happened (it would require
896 * min > 2, for one thing), but let's make sure. */
897 AlwaysAssert( newChildren
.size() >= min
,
898 "Too few new children in mkAssociative" );
900 return Expr(this, d_nodeManager
->mkNodePtr(kind
,newChildren
) );
903 unsigned ExprManager::minArity(Kind kind
) {
904 return metakind::getLowerBoundForKind(kind
);
907 unsigned ExprManager::maxArity(Kind kind
) {
908 return metakind::getUpperBoundForKind(kind
);
911 NodeManager
* ExprManager::getNodeManager() const {
912 return d_nodeManager
;
915 Context
* ExprManager::getContext() const {
919 Statistics
ExprManager::getStatistics() const throw() {
920 return Statistics(*d_nodeManager
->getStatisticsRegistry());
923 SExpr
ExprManager::getStatistic(const std::string
& name
) const throw() {
924 return d_nodeManager
->getStatisticsRegistry()->getStatistic(name
);
929 Node
exportInternal(TNode n
, ExprManager
* from
, ExprManager
* to
, ExprManagerMapCollection
& vmap
);
931 TypeNode
exportTypeInternal(TypeNode n
, NodeManager
* from
, NodeManager
* to
, ExprManagerMapCollection
& vmap
) {
932 Debug("export") << "type: " << n
<< std::endl
;
933 if(theory::kindToTheoryId(n
.getKind()) == theory::THEORY_DATATYPES
) {
934 throw ExportUnsupportedException
935 ("export of types belonging to theory of DATATYPES kinds unsupported");
937 if(n
.getMetaKind() == kind::metakind::PARAMETERIZED
&&
938 n
.getKind() != kind::SORT_TYPE
) {
939 throw ExportUnsupportedException
940 ("export of PARAMETERIZED-kinded types (other than SORT_KIND) not supported");
942 if(n
.getKind() == kind::TYPE_CONSTANT
) {
943 return to
->mkTypeConst(n
.getConst
<TypeConstant
>());
944 } else if(n
.getKind() == kind::BITVECTOR_TYPE
) {
945 return to
->mkBitVectorType(n
.getConst
<BitVectorSize
>());
946 } else if(n
.getKind() == kind::SUBRANGE_TYPE
) {
947 return to
->mkSubrangeType(n
.getSubrangeBounds());
949 Type from_t
= from
->toType(n
);
950 Type
& to_t
= vmap
.d_typeMap
[from_t
];
951 if(! to_t
.isNull()) {
952 Debug("export") << "+ mapped `" << from_t
<< "' to `" << to_t
<< "'" << std::endl
;
953 return *Type::getTypeNode(to_t
);
955 NodeBuilder
<> children(to
, n
.getKind());
956 if(n
.getKind() == kind::SORT_TYPE
) {
957 Debug("export") << "type: operator: " << n
.getOperator() << std::endl
;
958 // make a new sort tag in target node manager
959 Node sortTag
= NodeBuilder
<0>(to
, kind::SORT_TAG
);
962 for(TypeNode::iterator i
= n
.begin(), i_end
= n
.end(); i
!= i_end
; ++i
) {
963 Debug("export") << "type: child: " << *i
<< std::endl
;
964 children
<< exportTypeInternal(*i
, from
, to
, vmap
);
966 TypeNode out
= children
.constructTypeNode();// FIXME thread safety
967 to_t
= to
->toType(out
);
969 }/* exportTypeInternal() */
971 }/* CVC4::expr namespace */
973 Type
ExprManager::exportType(const Type
& t
, ExprManager
* em
, ExprManagerMapCollection
& vmap
) {
974 Assert(t
.d_nodeManager
!= em
->d_nodeManager
,
975 "Can't export a Type to the same ExprManager");
976 NodeManagerScope
ems(t
.d_nodeManager
);
977 return Type(em
->d_nodeManager
,
978 new TypeNode(expr::exportTypeInternal(*t
.d_typeNode
, t
.d_nodeManager
, em
->d_nodeManager
, vmap
)));
981 $
{mkConst_implementations
}
983 }/* CVC4 namespace */