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 Assert( types
.size() >= 1 );
513 std::vector
<TypeNode
> typeNodes
;
514 for (unsigned i
= 0, i_end
= types
.size(); i
< i_end
; ++ i
) {
515 typeNodes
.push_back(*types
[i
].d_typeNode
);
517 return TupleType(Type(d_nodeManager
, new TypeNode(d_nodeManager
->mkTupleType(typeNodes
))));
520 RecordType
ExprManager::mkRecordType(const Record
& rec
) {
521 NodeManagerScope
nms(d_nodeManager
);
522 return RecordType(Type(d_nodeManager
, new TypeNode(d_nodeManager
->mkRecordType(rec
))));
525 SExprType
ExprManager::mkSExprType(const std::vector
<Type
>& types
) {
526 NodeManagerScope
nms(d_nodeManager
);
527 std::vector
<TypeNode
> typeNodes
;
528 for (unsigned i
= 0, i_end
= types
.size(); i
< i_end
; ++ i
) {
529 typeNodes
.push_back(*types
[i
].d_typeNode
);
531 return SExprType(Type(d_nodeManager
, new TypeNode(d_nodeManager
->mkSExprType(typeNodes
))));
534 BitVectorType
ExprManager::mkBitVectorType(unsigned size
) const {
535 NodeManagerScope
nms(d_nodeManager
);
536 return BitVectorType(Type(d_nodeManager
, new TypeNode(d_nodeManager
->mkBitVectorType(size
))));
539 ArrayType
ExprManager::mkArrayType(Type indexType
, Type constituentType
) const {
540 NodeManagerScope
nms(d_nodeManager
);
541 return ArrayType(Type(d_nodeManager
, new TypeNode(d_nodeManager
->mkArrayType(*indexType
.d_typeNode
, *constituentType
.d_typeNode
))));
544 DatatypeType
ExprManager::mkDatatypeType(const Datatype
& datatype
) {
545 // Not worth a special implementation; this doesn't need to be fast
547 vector
<Datatype
> datatypes
;
548 datatypes
.push_back(datatype
);
549 vector
<DatatypeType
> result
= mkMutualDatatypeTypes(datatypes
);
550 Assert(result
.size() == 1);
551 return result
.front();
554 std::vector
<DatatypeType
>
555 ExprManager::mkMutualDatatypeTypes(const std::vector
<Datatype
>& datatypes
) {
556 return mkMutualDatatypeTypes(datatypes
, set
<Type
>());
559 std::vector
<DatatypeType
>
560 ExprManager::mkMutualDatatypeTypes(const std::vector
<Datatype
>& datatypes
,
561 const std::set
<Type
>& unresolvedTypes
) {
562 NodeManagerScope
nms(d_nodeManager
);
563 std::map
<std::string
, DatatypeType
> nameResolutions
;
564 std::vector
<DatatypeType
> dtts
;
566 // First do some sanity checks, set up the final Type to be used for
567 // each datatype, and set up the "named resolutions" used to handle
568 // simple self- and mutual-recursion, for example in the definition
569 // "nat = succ(pred:nat) | zero", a named resolution can handle the
571 for(std::vector
<Datatype
>::const_iterator i
= datatypes
.begin(),
572 i_end
= datatypes
.end();
576 if( (*i
).getNumParameters() == 0 ) {
577 typeNode
= new TypeNode(d_nodeManager
->mkTypeConst(*i
));
579 TypeNode cons
= d_nodeManager
->mkTypeConst(*i
);
580 std::vector
< TypeNode
> params
;
581 params
.push_back( cons
);
582 for( unsigned int ip
= 0; ip
< (*i
).getNumParameters(); ++ip
) {
583 params
.push_back( TypeNode::fromType( (*i
).getParameter( ip
) ) );
586 typeNode
= new TypeNode(d_nodeManager
->mkTypeNode(kind::PARAMETRIC_DATATYPE
, params
));
588 Type
type(d_nodeManager
, typeNode
);
589 DatatypeType
dtt(type
);
590 CheckArgument(nameResolutions
.find((*i
).getName()) == nameResolutions
.end(),
592 "cannot construct two datatypes at the same time "
593 "with the same name `%s'",
594 (*i
).getName().c_str());
595 nameResolutions
.insert(std::make_pair((*i
).getName(), dtt
));
599 // Second, set up the type substitution map for complex type
600 // resolution (e.g. if "list" is the type we're defining, and it has
601 // a selector of type "ARRAY INT OF list", this can't be taken care
602 // of using the named resolutions that we set up above. A
603 // preliminary array type was set up, and now needs to have "list"
604 // substituted in it for the correct type.
606 // @TODO get rid of named resolutions altogether and handle
607 // everything with these resolutions?
608 std::vector
< SortConstructorType
> paramTypes
;
609 std::vector
< DatatypeType
> paramReplacements
;
610 std::vector
<Type
> placeholders
;// to hold the "unresolved placeholders"
611 std::vector
<Type
> replacements
;// to hold our final, resolved types
612 for(std::set
<Type
>::const_iterator i
= unresolvedTypes
.begin(),
613 i_end
= unresolvedTypes
.end();
617 if( (*i
).isSort() ) {
618 name
= SortType(*i
).getName();
620 Assert( (*i
).isSortConstructor() );
621 name
= SortConstructorType(*i
).getName();
623 std::map
<std::string
, DatatypeType
>::const_iterator resolver
=
624 nameResolutions
.find(name
);
625 CheckArgument(resolver
!= nameResolutions
.end(),
627 "cannot resolve type `%s'; it's not among "
628 "the datatypes being defined", name
.c_str());
629 // We will instruct the Datatype to substitute "*i" (the
630 // unresolved SortType used as a placeholder in complex types)
631 // with "(*resolver).second" (the DatatypeType we created in the
632 // first step, above).
633 if( (*i
).isSort() ) {
634 placeholders
.push_back(*i
);
635 replacements
.push_back( (*resolver
).second
);
637 Assert( (*i
).isSortConstructor() );
638 paramTypes
.push_back( SortConstructorType(*i
) );
639 paramReplacements
.push_back( (*resolver
).second
);
643 // Lastly, perform the final resolutions and checks.
644 for(std::vector
<DatatypeType
>::iterator i
= dtts
.begin(),
648 const Datatype
& dt
= (*i
).getDatatype();
649 if(!dt
.isResolved()) {
650 const_cast<Datatype
&>(dt
).resolve(this, nameResolutions
,
651 placeholders
, replacements
,
652 paramTypes
, paramReplacements
);
655 // Now run some checks, including a check to make sure that no
656 // selector is function-valued.
657 checkResolvedDatatype(*i
);
660 for(std::vector
<NodeManagerListener
*>::iterator i
= d_nodeManager
->d_listeners
.begin(); i
!= d_nodeManager
->d_listeners
.end(); ++i
) {
661 (*i
)->nmNotifyNewDatatypes(dtts
);
667 void ExprManager::checkResolvedDatatype(DatatypeType dtt
) const {
668 const Datatype
& dt
= dtt
.getDatatype();
670 AssertArgument(dt
.isResolved(), dtt
, "datatype should have been resolved");
672 // for all constructors...
673 for(Datatype::const_iterator i
= dt
.begin(), i_end
= dt
.end();
676 const DatatypeConstructor
& c
= *i
;
677 Type testerType CVC4_UNUSED
= c
.getTester().getType();
678 Assert(c
.isResolved() &&
679 testerType
.isTester() &&
680 TesterType(testerType
).getDomain() == dtt
&&
681 TesterType(testerType
).getRangeType() == booleanType(),
682 "malformed tester in datatype post-resolution");
683 Type ctorType CVC4_UNUSED
= c
.getConstructor().getType();
684 Assert(ctorType
.isConstructor() &&
685 ConstructorType(ctorType
).getArity() == c
.getNumArgs() &&
686 ConstructorType(ctorType
).getRangeType() == dtt
,
687 "malformed constructor in datatype post-resolution");
688 // for all selectors...
689 for(DatatypeConstructor::const_iterator j
= c
.begin(), j_end
= c
.end();
692 const DatatypeConstructorArg
& a
= *j
;
693 Type selectorType
= a
.getSelector().getType();
694 Assert(a
.isResolved() &&
695 selectorType
.isSelector() &&
696 SelectorType(selectorType
).getDomain() == dtt
,
697 "malformed selector in datatype post-resolution");
698 // This next one's a "hard" check, performed in non-debug builds
699 // as well; the other ones should all be guaranteed by the
700 // CVC4::Datatype class, but this actually needs to be checked.
701 AlwaysAssert(!SelectorType(selectorType
).getRangeType().d_typeNode
->isFunctionLike(),
702 "cannot put function-like things in datatypes");
707 ConstructorType
ExprManager::mkConstructorType(const DatatypeConstructor
& constructor
, Type range
) const {
708 NodeManagerScope
nms(d_nodeManager
);
709 return Type(d_nodeManager
, new TypeNode(d_nodeManager
->mkConstructorType(constructor
, *range
.d_typeNode
)));
712 SelectorType
ExprManager::mkSelectorType(Type domain
, Type range
) const {
713 NodeManagerScope
nms(d_nodeManager
);
714 return Type(d_nodeManager
, new TypeNode(d_nodeManager
->mkSelectorType(*domain
.d_typeNode
, *range
.d_typeNode
)));
717 TesterType
ExprManager::mkTesterType(Type domain
) const {
718 NodeManagerScope
nms(d_nodeManager
);
719 return Type(d_nodeManager
, new TypeNode(d_nodeManager
->mkTesterType(*domain
.d_typeNode
)));
722 SortType
ExprManager::mkSort(const std::string
& name
) const {
723 NodeManagerScope
nms(d_nodeManager
);
724 return SortType(Type(d_nodeManager
, new TypeNode(d_nodeManager
->mkSort(name
))));
727 SortConstructorType
ExprManager::mkSortConstructor(const std::string
& name
,
728 size_t arity
) const {
729 NodeManagerScope
nms(d_nodeManager
);
730 return SortConstructorType(Type(d_nodeManager
,
731 new TypeNode(d_nodeManager
->mkSortConstructor(name
, arity
))));
734 /* - not in release 1.0
735 Type ExprManager::mkPredicateSubtype(Expr lambda)
736 throw(TypeCheckingException) {
737 NodeManagerScope nms(d_nodeManager);
739 return PredicateSubtype(Type(d_nodeManager,
740 new TypeNode(d_nodeManager->mkPredicateSubtype(lambda))));
741 } catch (const TypeCheckingExceptionPrivate& e) {
742 throw TypeCheckingException(this, &e);
747 /* - not in release 1.0
748 Type ExprManager::mkPredicateSubtype(Expr lambda, Expr witness)
749 throw(TypeCheckingException) {
750 NodeManagerScope nms(d_nodeManager);
752 return PredicateSubtype(Type(d_nodeManager,
753 new TypeNode(d_nodeManager->mkPredicateSubtype(lambda, witness))));
754 } catch (const TypeCheckingExceptionPrivate& e) {
755 throw TypeCheckingException(this, &e);
760 Type
ExprManager::mkSubrangeType(const SubrangeBounds
& bounds
)
761 throw(TypeCheckingException
) {
762 NodeManagerScope
nms(d_nodeManager
);
764 return SubrangeType(Type(d_nodeManager
,
765 new TypeNode(d_nodeManager
->mkSubrangeType(bounds
))));
766 } catch (const TypeCheckingExceptionPrivate
& e
) {
767 throw TypeCheckingException(this, &e
);
772 * Get the type for the given Expr and optionally do type checking.
774 * Initial type computation will be near-constant time if
775 * type checking is not requested. Results are memoized, so that
776 * subsequent calls to getType() without type checking will be
779 * Initial type checking is linear in the size of the expression.
780 * Again, the results are memoized, so that subsequent calls to
781 * getType(), with or without type checking, will be constant
784 * NOTE: A TypeCheckingException can be thrown even when type
785 * checking is not requested. getType() will always return a
786 * valid and correct type and, thus, an exception will be thrown
787 * when no valid or correct type can be computed (e.g., if the
788 * arguments to a bit-vector operation aren't bit-vectors). When
789 * type checking is not requested, getType() will do the minimum
790 * amount of checking required to return a valid result.
792 * @param e the Expr for which we want a type
793 * @param check whether we should check the type as we compute it
796 Type
ExprManager::getType(Expr e
, bool check
) throw (TypeCheckingException
) {
797 NodeManagerScope
nms(d_nodeManager
);
800 t
= Type(d_nodeManager
,
801 new TypeNode(d_nodeManager
->getType(e
.getNode(), check
)));
802 } catch (const TypeCheckingExceptionPrivate
& e
) {
803 throw TypeCheckingException(this, &e
);
808 Expr
ExprManager::mkVar(const std::string
& name
, Type type
, uint32_t flags
) {
809 Assert(NodeManager::currentNM() == NULL
, "ExprManager::mkVar() should only be called externally, not from within CVC4 code. Please use mkSkolem().");
810 NodeManagerScope
nms(d_nodeManager
);
811 Node
* n
= d_nodeManager
->mkVarPtr(name
, *type
.d_typeNode
, flags
);
812 Debug("nm") << "set " << name
<< " on " << *n
<< std::endl
;
813 INC_STAT_VAR(type
, false);
814 return Expr(this, n
);
817 Expr
ExprManager::mkVar(Type type
, uint32_t flags
) {
818 Assert(NodeManager::currentNM() == NULL
, "ExprManager::mkVar() should only be called externally, not from within CVC4 code. Please use mkSkolem().");
819 NodeManagerScope
nms(d_nodeManager
);
820 INC_STAT_VAR(type
, false);
821 return Expr(this, d_nodeManager
->mkVarPtr(*type
.d_typeNode
, flags
));
824 Expr
ExprManager::mkBoundVar(const std::string
& name
, Type type
) {
825 NodeManagerScope
nms(d_nodeManager
);
826 Node
* n
= d_nodeManager
->mkBoundVarPtr(name
, *type
.d_typeNode
);
827 Debug("nm") << "set " << name
<< " on " << *n
<< std::endl
;
828 INC_STAT_VAR(type
, true);
829 return Expr(this, n
);
832 Expr
ExprManager::mkBoundVar(Type type
) {
833 NodeManagerScope
nms(d_nodeManager
);
834 INC_STAT_VAR(type
, true);
835 return Expr(this, d_nodeManager
->mkBoundVarPtr(*type
.d_typeNode
));
838 Expr
ExprManager::mkAssociative(Kind kind
,
839 const std::vector
<Expr
>& children
) {
840 CheckArgument( kind::isAssociative(kind
), kind
,
841 "Illegal kind in mkAssociative: %s",
842 kind::kindToString(kind
).c_str());
844 NodeManagerScope
nms(d_nodeManager
);
845 const unsigned int max
= maxArity(kind
);
846 const unsigned int min
= minArity(kind
);
847 unsigned int numChildren
= children
.size();
849 /* If the number of children is within bounds, then there's nothing to do. */
850 if( numChildren
<= max
) {
851 return mkExpr(kind
,children
);
854 std::vector
<Expr
>::const_iterator it
= children
.begin() ;
855 std::vector
<Expr
>::const_iterator end
= children
.end() ;
857 /* The new top-level children and the children of each sub node */
858 std::vector
<Node
> newChildren
;
859 std::vector
<Node
> subChildren
;
861 while( it
!= end
&& numChildren
> max
) {
862 /* Grab the next max children and make a node for them. */
863 for( std::vector
<Expr
>::const_iterator next
= it
+ max
;
865 ++it
, --numChildren
) {
866 subChildren
.push_back(it
->getNode());
868 Node subNode
= d_nodeManager
->mkNode(kind
,subChildren
);
869 newChildren
.push_back(subNode
);
874 /* If there's children left, "top off" the Expr. */
875 if(numChildren
> 0) {
876 /* If the leftovers are too few, just copy them into newChildren;
877 * otherwise make a new sub-node */
878 if(numChildren
< min
) {
879 for(; it
!= end
; ++it
) {
880 newChildren
.push_back(it
->getNode());
883 for(; it
!= end
; ++it
) {
884 subChildren
.push_back(it
->getNode());
886 Node subNode
= d_nodeManager
->mkNode(kind
, subChildren
);
887 newChildren
.push_back(subNode
);
891 /* It's inconceivable we could have enough children for this to fail
892 * (more than 2^32, in most cases?). */
893 AlwaysAssert( newChildren
.size() <= max
,
894 "Too many new children in mkAssociative" );
896 /* It would be really weird if this happened (it would require
897 * min > 2, for one thing), but let's make sure. */
898 AlwaysAssert( newChildren
.size() >= min
,
899 "Too few new children in mkAssociative" );
901 return Expr(this, d_nodeManager
->mkNodePtr(kind
,newChildren
) );
904 unsigned ExprManager::minArity(Kind kind
) {
905 return metakind::getLowerBoundForKind(kind
);
908 unsigned ExprManager::maxArity(Kind kind
) {
909 return metakind::getUpperBoundForKind(kind
);
912 NodeManager
* ExprManager::getNodeManager() const {
913 return d_nodeManager
;
916 Context
* ExprManager::getContext() const {
920 Statistics
ExprManager::getStatistics() const throw() {
921 return Statistics(*d_nodeManager
->getStatisticsRegistry());
924 SExpr
ExprManager::getStatistic(const std::string
& name
) const throw() {
925 return d_nodeManager
->getStatisticsRegistry()->getStatistic(name
);
930 Node
exportInternal(TNode n
, ExprManager
* from
, ExprManager
* to
, ExprManagerMapCollection
& vmap
);
932 TypeNode
exportTypeInternal(TypeNode n
, NodeManager
* from
, NodeManager
* to
, ExprManagerMapCollection
& vmap
) {
933 Debug("export") << "type: " << n
<< std::endl
;
934 if(theory::kindToTheoryId(n
.getKind()) == theory::THEORY_DATATYPES
) {
935 throw ExportUnsupportedException
936 ("export of types belonging to theory of DATATYPES kinds unsupported");
938 if(n
.getMetaKind() == kind::metakind::PARAMETERIZED
&&
939 n
.getKind() != kind::SORT_TYPE
) {
940 throw ExportUnsupportedException
941 ("export of PARAMETERIZED-kinded types (other than SORT_KIND) not supported");
943 if(n
.getKind() == kind::TYPE_CONSTANT
) {
944 return to
->mkTypeConst(n
.getConst
<TypeConstant
>());
945 } else if(n
.getKind() == kind::BITVECTOR_TYPE
) {
946 return to
->mkBitVectorType(n
.getConst
<BitVectorSize
>());
947 } else if(n
.getKind() == kind::SUBRANGE_TYPE
) {
948 return to
->mkSubrangeType(n
.getSubrangeBounds());
950 Type from_t
= from
->toType(n
);
951 Type
& to_t
= vmap
.d_typeMap
[from_t
];
952 if(! to_t
.isNull()) {
953 Debug("export") << "+ mapped `" << from_t
<< "' to `" << to_t
<< "'" << std::endl
;
954 return *Type::getTypeNode(to_t
);
956 NodeBuilder
<> children(to
, n
.getKind());
957 if(n
.getKind() == kind::SORT_TYPE
) {
958 Debug("export") << "type: operator: " << n
.getOperator() << std::endl
;
959 // make a new sort tag in target node manager
960 Node sortTag
= NodeBuilder
<0>(to
, kind::SORT_TAG
);
963 for(TypeNode::iterator i
= n
.begin(), i_end
= n
.end(); i
!= i_end
; ++i
) {
964 Debug("export") << "type: child: " << *i
<< std::endl
;
965 children
<< exportTypeInternal(*i
, from
, to
, vmap
);
967 TypeNode out
= children
.constructTypeNode();// FIXME thread safety
968 to_t
= to
->toType(out
);
970 }/* exportTypeInternal() */
972 }/* CVC4::expr namespace */
974 Type
ExprManager::exportType(const Type
& t
, ExprManager
* em
, ExprManagerMapCollection
& vmap
) {
975 Assert(t
.d_nodeManager
!= em
->d_nodeManager
,
976 "Can't export a Type to the same ExprManager");
977 NodeManagerScope
ems(t
.d_nodeManager
);
978 return Type(em
->d_nodeManager
,
979 new TypeNode(expr::exportTypeInternal(*t
.d_typeNode
, t
.d_nodeManager
, em
->d_nodeManager
, vmap
)));
982 $
{mkConst_implementations
}
984 }/* CVC4 namespace */