+++ /dev/null
-/********************* */
-/*! \file expr_manager_template.cpp
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Dejan Jovanovic, Christopher L. Conway
- ** Minor contributors (to current version): Kshitij Bansal, Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Public-facing expression manager interface, implementation
- **
- ** Public-facing expression manager interface, implementation.
- **/
-
-#include "expr/node_manager.h"
-#include "expr/expr_manager.h"
-#include "expr/variable_type_map.h"
-#include "options/options.h"
-#include "util/statistics_registry.h"
-
-#include <map>
-
-${includes}
-
-// This is a hack, but an important one: if there's an error, the
-// compiler directs the user to the template file instead of the
-// generated one. We don't want the user to modify the generated one,
-// since it'll get overwritten on a later build.
-#line 32 "${template}"
-
-#ifdef CVC4_STATISTICS_ON
- #define INC_STAT(kind) \
- { \
- if (d_exprStatistics[kind] == NULL) { \
- stringstream statName; \
- statName << "expr::ExprManager::" << kind; \
- d_exprStatistics[kind] = new IntStat(statName.str(), 0); \
- d_nodeManager->getStatisticsRegistry()->registerStat_(d_exprStatistics[kind]); \
- } \
- ++ *(d_exprStatistics[kind]); \
- }
- #define INC_STAT_VAR(type, bound_var) \
- { \
- TypeNode* typeNode = Type::getTypeNode(type); \
- TypeConstant type = typeNode->getKind() == kind::TYPE_CONSTANT ? typeNode->getConst<TypeConstant>() : LAST_TYPE; \
- if (d_exprStatisticsVars[type] == NULL) { \
- stringstream statName; \
- if (type == LAST_TYPE) { \
- statName << "expr::ExprManager::" << ((bound_var) ? "BOUND_VARIABLE" : "VARIABLE") << ":Parameterized type"; \
- } else { \
- statName << "expr::ExprManager::" << ((bound_var) ? "BOUND_VARIABLE" : "VARIABLE") << ":" << type; \
- } \
- d_exprStatisticsVars[type] = new IntStat(statName.str(), 0); \
- d_nodeManager->getStatisticsRegistry()->registerStat_(d_exprStatisticsVars[type]); \
- } \
- ++ *(d_exprStatisticsVars[type]); \
- }
-#else
- #define INC_STAT(kind)
- #define INC_STAT_VAR(type, bound_var)
-#endif
-
-using namespace std;
-using namespace CVC4::kind;
-
-namespace CVC4 {
-
-ExprManager::ExprManager() :
- d_nodeManager(new NodeManager(this)) {
-#ifdef CVC4_STATISTICS_ON
- for (unsigned i = 0; i < kind::LAST_KIND; ++ i) {
- d_exprStatistics[i] = NULL;
- }
- for (unsigned i = 0; i < LAST_TYPE; ++ i) {
- d_exprStatisticsVars[i] = NULL;
- }
-#endif
-}
-
-ExprManager::ExprManager(const Options& options) :
- d_nodeManager(new NodeManager(this, options)) {
-#ifdef CVC4_STATISTICS_ON
- for (unsigned i = 0; i < LAST_TYPE; ++ i) {
- d_exprStatisticsVars[i] = NULL;
- }
- for (unsigned i = 0; i < kind::LAST_KIND; ++ i) {
- d_exprStatistics[i] = NULL;
- }
-#endif
-}
-
-ExprManager::~ExprManager() throw() {
- NodeManagerScope nms(d_nodeManager);
-
- try {
-
-#ifdef CVC4_STATISTICS_ON
- for (unsigned i = 0; i < kind::LAST_KIND; ++ i) {
- if (d_exprStatistics[i] != NULL) {
- d_nodeManager->getStatisticsRegistry()->unregisterStat_(d_exprStatistics[i]);
- delete d_exprStatistics[i];
- d_exprStatistics[i] = NULL;
- }
- }
- for (unsigned i = 0; i < LAST_TYPE; ++ i) {
- if (d_exprStatisticsVars[i] != NULL) {
- d_nodeManager->getStatisticsRegistry()->unregisterStat_(d_exprStatisticsVars[i]);
- delete d_exprStatisticsVars[i];
- d_exprStatisticsVars[i] = NULL;
- }
- }
-#endif
-
- delete d_nodeManager;
- d_nodeManager = NULL;
-
- } catch(Exception& e) {
- Warning() << "CVC4 threw an exception during cleanup." << std::endl
- << e << std::endl;
- }
-}
-
-StatisticsRegistry* ExprManager::getStatisticsRegistry() throw() {
- return d_nodeManager->getStatisticsRegistry();
-}
-
-const Options& ExprManager::getOptions() const {
- return d_nodeManager->getOptions();
-}
-
-ResourceManager* ExprManager::getResourceManager() throw() {
- return d_nodeManager->getResourceManager();
-}
-
-BooleanType ExprManager::booleanType() const {
- NodeManagerScope nms(d_nodeManager);
- return BooleanType(Type(d_nodeManager, new TypeNode(d_nodeManager->booleanType())));
-}
-
-StringType ExprManager::stringType() const {
- NodeManagerScope nms(d_nodeManager);
- return StringType(Type(d_nodeManager, new TypeNode(d_nodeManager->stringType())));
-}
-
-RealType ExprManager::realType() const {
- NodeManagerScope nms(d_nodeManager);
- return RealType(Type(d_nodeManager, new TypeNode(d_nodeManager->realType())));
-}
-
-IntegerType ExprManager::integerType() const {
- NodeManagerScope nms(d_nodeManager);
- return IntegerType(Type(d_nodeManager, new TypeNode(d_nodeManager->integerType())));
-}
-
-Expr ExprManager::mkExpr(Kind kind, Expr child1) {
- const kind::MetaKind mk = kind::metaKindOf(kind);
- const unsigned n = 1 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0);
- CheckArgument(mk == kind::metakind::PARAMETERIZED ||
- mk == kind::metakind::OPERATOR, kind,
- "Only operator-style expressions are made with mkExpr(); "
- "to make variables and constants, see mkVar(), mkBoundVar(), "
- "and mkConst().");
- CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
- "Exprs with kind %s must have at least %u children and "
- "at most %u children (the one under construction has %u)",
- kind::kindToString(kind).c_str(),
- minArity(kind), maxArity(kind), n);
- NodeManagerScope nms(d_nodeManager);
- try {
- INC_STAT(kind);
- return Expr(this, d_nodeManager->mkNodePtr(kind, child1.getNode()));
- } catch (const TypeCheckingExceptionPrivate& e) {
- throw TypeCheckingException(this, &e);
- }
-}
-
-Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2) {
- const kind::MetaKind mk = kind::metaKindOf(kind);
- const unsigned n = 2 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0);
- CheckArgument(mk == kind::metakind::PARAMETERIZED ||
- mk == kind::metakind::OPERATOR, kind,
- "Only operator-style expressions are made with mkExpr(); "
- "to make variables and constants, see mkVar(), mkBoundVar(), "
- "and mkConst().");
- CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
- "Exprs with kind %s must have at least %u children and "
- "at most %u children (the one under construction has %u)",
- kind::kindToString(kind).c_str(),
- minArity(kind), maxArity(kind), n);
- NodeManagerScope nms(d_nodeManager);
- try {
- INC_STAT(kind);
- return Expr(this, d_nodeManager->mkNodePtr(kind,
- child1.getNode(),
- child2.getNode()));
- } catch (const TypeCheckingExceptionPrivate& e) {
- throw TypeCheckingException(this, &e);
- }
-}
-
-Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3) {
- const kind::MetaKind mk = kind::metaKindOf(kind);
- const unsigned n = 3 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0);
- CheckArgument(mk == kind::metakind::PARAMETERIZED ||
- mk == kind::metakind::OPERATOR, kind,
- "Only operator-style expressions are made with mkExpr(); "
- "to make variables and constants, see mkVar(), mkBoundVar(), "
- "and mkConst().");
- CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
- "Exprs with kind %s must have at least %u children and "
- "at most %u children (the one under construction has %u)",
- kind::kindToString(kind).c_str(),
- minArity(kind), maxArity(kind), n);
- NodeManagerScope nms(d_nodeManager);
- try {
- INC_STAT(kind);
- return Expr(this, d_nodeManager->mkNodePtr(kind,
- child1.getNode(),
- child2.getNode(),
- child3.getNode()));
- } catch (const TypeCheckingExceptionPrivate& e) {
- throw TypeCheckingException(this, &e);
- }
-}
-
-Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3,
- Expr child4) {
- const kind::MetaKind mk = kind::metaKindOf(kind);
- const unsigned n = 4 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0);
- CheckArgument(mk == kind::metakind::PARAMETERIZED ||
- mk == kind::metakind::OPERATOR, kind,
- "Only operator-style expressions are made with mkExpr(); "
- "to make variables and constants, see mkVar(), mkBoundVar(), "
- "and mkConst().");
- CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
- "Exprs with kind %s must have at least %u children and "
- "at most %u children (the one under construction has %u)",
- kind::kindToString(kind).c_str(),
- minArity(kind), maxArity(kind), n);
- NodeManagerScope nms(d_nodeManager);
- try {
- INC_STAT(kind);
- return Expr(this, d_nodeManager->mkNodePtr(kind,
- child1.getNode(),
- child2.getNode(),
- child3.getNode(),
- child4.getNode()));
- } catch (const TypeCheckingExceptionPrivate& e) {
- throw TypeCheckingException(this, &e);
- }
-}
-
-Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3,
- Expr child4, Expr child5) {
- const kind::MetaKind mk = kind::metaKindOf(kind);
- const unsigned n = 5 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0);
- CheckArgument(mk == kind::metakind::PARAMETERIZED ||
- mk == kind::metakind::OPERATOR, kind,
- "Only operator-style expressions are made with mkExpr(); "
- "to make variables and constants, see mkVar(), mkBoundVar(), "
- "and mkConst().");
- CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
- "Exprs with kind %s must have at least %u children and "
- "at most %u children (the one under construction has %u)",
- kind::kindToString(kind).c_str(),
- minArity(kind), maxArity(kind), n);
- NodeManagerScope nms(d_nodeManager);
- try {
- INC_STAT(kind);
- return Expr(this, d_nodeManager->mkNodePtr(kind,
- child1.getNode(),
- child2.getNode(),
- child3.getNode(),
- child4.getNode(),
- child5.getNode()));
- } catch (const TypeCheckingExceptionPrivate& e) {
- throw TypeCheckingException(this, &e);
- }
-}
-
-Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) {
- const kind::MetaKind mk = kind::metaKindOf(kind);
- const unsigned n = children.size() - (mk == kind::metakind::PARAMETERIZED ? 1 : 0);
- CheckArgument(mk == kind::metakind::PARAMETERIZED ||
- mk == kind::metakind::OPERATOR, kind,
- "Only operator-style expressions are made with mkExpr(); "
- "to make variables and constants, see mkVar(), mkBoundVar(), "
- "and mkConst().");
- CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
- "Exprs with kind %s must have at least %u children and "
- "at most %u children (the one under construction has %u)",
- kind::kindToString(kind).c_str(),
- minArity(kind), maxArity(kind), n);
-
- NodeManagerScope nms(d_nodeManager);
-
- vector<Node> nodes;
- vector<Expr>::const_iterator it = children.begin();
- vector<Expr>::const_iterator it_end = children.end();
- while(it != it_end) {
- nodes.push_back(it->getNode());
- ++it;
- }
- try {
- INC_STAT(kind);
- return Expr(this, d_nodeManager->mkNodePtr(kind, nodes));
- } catch (const TypeCheckingExceptionPrivate& e) {
- throw TypeCheckingException(this, &e);
- }
-}
-
-Expr ExprManager::mkExpr(Kind kind, Expr child1,
- const std::vector<Expr>& otherChildren) {
- const kind::MetaKind mk = kind::metaKindOf(kind);
- const unsigned n = otherChildren.size() - (mk == kind::metakind::PARAMETERIZED ? 1 : 0) + 1;
- CheckArgument(mk == kind::metakind::PARAMETERIZED ||
- mk == kind::metakind::OPERATOR, kind,
- "Only operator-style expressions are made with mkExpr(); "
- "to make variables and constants, see mkVar(), mkBoundVar(), "
- "and mkConst().");
- CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
- "Exprs with kind %s must have at least %u children and "
- "at most %u children (the one under construction has %u)",
- kind::kindToString(kind).c_str(),
- minArity(kind), maxArity(kind), n);
-
- NodeManagerScope nms(d_nodeManager);
-
- vector<Node> nodes;
- nodes.push_back(child1.getNode());
-
- vector<Expr>::const_iterator it = otherChildren.begin();
- vector<Expr>::const_iterator it_end = otherChildren.end();
- while(it != it_end) {
- nodes.push_back(it->getNode());
- ++it;
- }
- try {
- INC_STAT(kind);
- return Expr(this, d_nodeManager->mkNodePtr(kind, nodes));
- } catch (const TypeCheckingExceptionPrivate& e) {
- throw TypeCheckingException(this, &e);
- }
-}
-
-Expr ExprManager::mkExpr(Expr opExpr) {
- const unsigned n = 0;
- Kind kind = NodeManager::operatorToKind(opExpr.getNode());
- CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
- "This Expr constructor is for parameterized kinds only");
- CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
- "Exprs with kind %s must have at least %u children and "
- "at most %u children (the one under construction has %u)",
- kind::kindToString(kind).c_str(),
- minArity(kind), maxArity(kind), n);
- NodeManagerScope nms(d_nodeManager);
- try {
- INC_STAT(kind);
- return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode()));
- } catch (const TypeCheckingExceptionPrivate& e) {
- throw TypeCheckingException(this, &e);
- }
-}
-
-Expr ExprManager::mkExpr(Expr opExpr, Expr child1) {
- const unsigned n = 1;
- Kind kind = NodeManager::operatorToKind(opExpr.getNode());
- CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
- "This Expr constructor is for parameterized kinds only");
- CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
- "Exprs with kind %s must have at least %u children and "
- "at most %u children (the one under construction has %u)",
- kind::kindToString(kind).c_str(),
- minArity(kind), maxArity(kind), n);
- NodeManagerScope nms(d_nodeManager);
- try {
- INC_STAT(kind);
- return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(), child1.getNode()));
- } catch (const TypeCheckingExceptionPrivate& e) {
- throw TypeCheckingException(this, &e);
- }
-}
-
-Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2) {
- const unsigned n = 2;
- Kind kind = NodeManager::operatorToKind(opExpr.getNode());
- CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
- "This Expr constructor is for parameterized kinds only");
- CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
- "Exprs with kind %s must have at least %u children and "
- "at most %u children (the one under construction has %u)",
- kind::kindToString(kind).c_str(),
- minArity(kind), maxArity(kind), n);
- NodeManagerScope nms(d_nodeManager);
- try {
- INC_STAT(kind);
- return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(),
- child1.getNode(),
- child2.getNode()));
- } catch (const TypeCheckingExceptionPrivate& e) {
- throw TypeCheckingException(this, &e);
- }
-}
-
-Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3) {
- const unsigned n = 3;
- Kind kind = NodeManager::operatorToKind(opExpr.getNode());
- CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
- "This Expr constructor is for parameterized kinds only");
- CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
- "Exprs with kind %s must have at least %u children and "
- "at most %u children (the one under construction has %u)",
- kind::kindToString(kind).c_str(),
- minArity(kind), maxArity(kind), n);
- NodeManagerScope nms(d_nodeManager);
- try {
- INC_STAT(kind);
- return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(),
- child1.getNode(),
- child2.getNode(),
- child3.getNode()));
- } catch (const TypeCheckingExceptionPrivate& e) {
- throw TypeCheckingException(this, &e);
- }
-}
-
-Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3,
- Expr child4) {
- const unsigned n = 4;
- Kind kind = NodeManager::operatorToKind(opExpr.getNode());
- CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
- "This Expr constructor is for parameterized kinds only");
- CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
- "Exprs with kind %s must have at least %u children and "
- "at most %u children (the one under construction has %u)",
- kind::kindToString(kind).c_str(),
- minArity(kind), maxArity(kind), n);
- NodeManagerScope nms(d_nodeManager);
- try {
- INC_STAT(kind);
- return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(),
- child1.getNode(),
- child2.getNode(),
- child3.getNode(),
- child4.getNode()));
- } catch (const TypeCheckingExceptionPrivate& e) {
- throw TypeCheckingException(this, &e);
- }
-}
-
-Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3,
- Expr child4, Expr child5) {
- const unsigned n = 5;
- Kind kind = NodeManager::operatorToKind(opExpr.getNode());
- CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
- "This Expr constructor is for parameterized kinds only");
- CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
- "Exprs with kind %s must have at least %u children and "
- "at most %u children (the one under construction has %u)",
- kind::kindToString(kind).c_str(),
- minArity(kind), maxArity(kind), n);
- NodeManagerScope nms(d_nodeManager);
- try {
- INC_STAT(kind);
- return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(),
- child1.getNode(),
- child2.getNode(),
- child3.getNode(),
- child4.getNode(),
- child5.getNode()));
- } catch (const TypeCheckingExceptionPrivate& e) {
- throw TypeCheckingException(this, &e);
- }
-}
-
-Expr ExprManager::mkExpr(Expr opExpr, const std::vector<Expr>& children) {
- const unsigned n = children.size();
- Kind kind = NodeManager::operatorToKind(opExpr.getNode());
- CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
- "This Expr constructor is for parameterized kinds only");
- CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
- "Exprs with kind %s must have at least %u children and "
- "at most %u children (the one under construction has %u)",
- kind::kindToString(kind).c_str(),
- minArity(kind), maxArity(kind), n);
-
- NodeManagerScope nms(d_nodeManager);
-
- vector<Node> nodes;
- vector<Expr>::const_iterator it = children.begin();
- vector<Expr>::const_iterator it_end = children.end();
- while(it != it_end) {
- nodes.push_back(it->getNode());
- ++it;
- }
- try {
- INC_STAT(kind);
- return Expr(this,d_nodeManager->mkNodePtr(opExpr.getNode(), nodes));
- } catch (const TypeCheckingExceptionPrivate& e) {
- throw TypeCheckingException(this, &e);
- }
-}
-
-bool ExprManager::hasOperator(Kind k) {
- return NodeManager::hasOperator(k);
-}
-
-Expr ExprManager::operatorOf(Kind k) {
- NodeManagerScope nms(d_nodeManager);
-
- return d_nodeManager->operatorOf(k).toExpr();
-}
-
-/** Make a function type from domain to range. */
-FunctionType ExprManager::mkFunctionType(Type domain, Type range) {
- NodeManagerScope nms(d_nodeManager);
- return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(*domain.d_typeNode, *range.d_typeNode))));
-}
-
-/** Make a function type with input types from argTypes. */
-FunctionType ExprManager::mkFunctionType(const std::vector<Type>& argTypes, Type range) {
- NodeManagerScope nms(d_nodeManager);
- Assert( argTypes.size() >= 1 );
- std::vector<TypeNode> argTypeNodes;
- for (unsigned i = 0, i_end = argTypes.size(); i < i_end; ++ i) {
- argTypeNodes.push_back(*argTypes[i].d_typeNode);
- }
- return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(argTypeNodes, *range.d_typeNode))));
-}
-
-FunctionType ExprManager::mkFunctionType(const std::vector<Type>& sorts) {
- NodeManagerScope nms(d_nodeManager);
- Assert( sorts.size() >= 2 );
- std::vector<TypeNode> sortNodes;
- for (unsigned i = 0, i_end = sorts.size(); i < i_end; ++ i) {
- sortNodes.push_back(*sorts[i].d_typeNode);
- }
- return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(sortNodes))));
-}
-
-FunctionType ExprManager::mkPredicateType(const std::vector<Type>& sorts) {
- NodeManagerScope nms(d_nodeManager);
- Assert( sorts.size() >= 1 );
- std::vector<TypeNode> sortNodes;
- for (unsigned i = 0, i_end = sorts.size(); i < i_end; ++ i) {
- sortNodes.push_back(*sorts[i].d_typeNode);
- }
- return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkPredicateType(sortNodes))));
-}
-
-TupleType ExprManager::mkTupleType(const std::vector<Type>& types) {
- NodeManagerScope nms(d_nodeManager);
- std::vector<TypeNode> typeNodes;
- for (unsigned i = 0, i_end = types.size(); i < i_end; ++ i) {
- typeNodes.push_back(*types[i].d_typeNode);
- }
- return TupleType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkTupleType(typeNodes))));
-}
-
-RecordType ExprManager::mkRecordType(const Record& rec) {
- NodeManagerScope nms(d_nodeManager);
- return RecordType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkRecordType(rec))));
-}
-
-SExprType ExprManager::mkSExprType(const std::vector<Type>& types) {
- NodeManagerScope nms(d_nodeManager);
- std::vector<TypeNode> typeNodes;
- for (unsigned i = 0, i_end = types.size(); i < i_end; ++ i) {
- typeNodes.push_back(*types[i].d_typeNode);
- }
- return SExprType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSExprType(typeNodes))));
-}
-
-BitVectorType ExprManager::mkBitVectorType(unsigned size) const {
- NodeManagerScope nms(d_nodeManager);
- return BitVectorType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkBitVectorType(size))));
-}
-
-ArrayType ExprManager::mkArrayType(Type indexType, Type constituentType) const {
- NodeManagerScope nms(d_nodeManager);
- return ArrayType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkArrayType(*indexType.d_typeNode, *constituentType.d_typeNode))));
-}
-
-SetType ExprManager::mkSetType(Type elementType) const {
- NodeManagerScope nms(d_nodeManager);
- return SetType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSetType(*elementType.d_typeNode))));
-}
-
-DatatypeType ExprManager::mkDatatypeType(const Datatype& datatype) {
- // Not worth a special implementation; this doesn't need to be fast
- // code anyway.
- vector<Datatype> datatypes;
- datatypes.push_back(datatype);
- vector<DatatypeType> result = mkMutualDatatypeTypes(datatypes);
- Assert(result.size() == 1);
- return result.front();
-}
-
-std::vector<DatatypeType>
-ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
- return mkMutualDatatypeTypes(datatypes, set<Type>());
-}
-
-std::vector<DatatypeType>
-ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
- const std::set<Type>& unresolvedTypes) {
- NodeManagerScope nms(d_nodeManager);
- std::map<std::string, DatatypeType> nameResolutions;
- std::vector<DatatypeType> dtts;
-
- // First do some sanity checks, set up the final Type to be used for
- // each datatype, and set up the "named resolutions" used to handle
- // simple self- and mutual-recursion, for example in the definition
- // "nat = succ(pred:nat) | zero", a named resolution can handle the
- // pred selector.
- for(std::vector<Datatype>::const_iterator i = datatypes.begin(),
- i_end = datatypes.end();
- i != i_end;
- ++i) {
- TypeNode* typeNode;
- if( (*i).getNumParameters() == 0 ) {
- typeNode = new TypeNode(d_nodeManager->mkTypeConst(*i));
- } else {
- TypeNode cons = d_nodeManager->mkTypeConst(*i);
- std::vector< TypeNode > params;
- params.push_back( cons );
- for( unsigned int ip = 0; ip < (*i).getNumParameters(); ++ip ) {
- params.push_back( TypeNode::fromType( (*i).getParameter( ip ) ) );
- }
-
- typeNode = new TypeNode(d_nodeManager->mkTypeNode(kind::PARAMETRIC_DATATYPE, params));
- }
- Type type(d_nodeManager, typeNode);
- DatatypeType dtt(type);
- CheckArgument(nameResolutions.find((*i).getName()) == nameResolutions.end(),
- datatypes,
- "cannot construct two datatypes at the same time "
- "with the same name `%s'",
- (*i).getName().c_str());
- nameResolutions.insert(std::make_pair((*i).getName(), dtt));
- dtts.push_back(dtt);
- }
-
- // Second, set up the type substitution map for complex type
- // resolution (e.g. if "list" is the type we're defining, and it has
- // a selector of type "ARRAY INT OF list", this can't be taken care
- // of using the named resolutions that we set up above. A
- // preliminary array type was set up, and now needs to have "list"
- // substituted in it for the correct type.
- //
- // @TODO get rid of named resolutions altogether and handle
- // everything with these resolutions?
- std::vector< SortConstructorType > paramTypes;
- std::vector< DatatypeType > paramReplacements;
- std::vector<Type> placeholders;// to hold the "unresolved placeholders"
- std::vector<Type> replacements;// to hold our final, resolved types
- for(std::set<Type>::const_iterator i = unresolvedTypes.begin(),
- i_end = unresolvedTypes.end();
- i != i_end;
- ++i) {
- std::string name;
- if( (*i).isSort() ) {
- name = SortType(*i).getName();
- } else {
- Assert( (*i).isSortConstructor() );
- name = SortConstructorType(*i).getName();
- }
- std::map<std::string, DatatypeType>::const_iterator resolver =
- nameResolutions.find(name);
- CheckArgument(resolver != nameResolutions.end(),
- unresolvedTypes,
- "cannot resolve type `%s'; it's not among "
- "the datatypes being defined", name.c_str());
- // We will instruct the Datatype to substitute "*i" (the
- // unresolved SortType used as a placeholder in complex types)
- // with "(*resolver).second" (the DatatypeType we created in the
- // first step, above).
- if( (*i).isSort() ) {
- placeholders.push_back(*i);
- replacements.push_back( (*resolver).second );
- } else {
- Assert( (*i).isSortConstructor() );
- paramTypes.push_back( SortConstructorType(*i) );
- paramReplacements.push_back( (*resolver).second );
- }
- }
-
- // Lastly, perform the final resolutions and checks.
- for(std::vector<DatatypeType>::iterator i = dtts.begin(),
- i_end = dtts.end();
- i != i_end;
- ++i) {
- const Datatype& dt = (*i).getDatatype();
- if(!dt.isResolved()) {
- const_cast<Datatype&>(dt).resolve(this, nameResolutions,
- placeholders, replacements,
- paramTypes, paramReplacements);
- }
-
- // Now run some checks, including a check to make sure that no
- // selector is function-valued.
- checkResolvedDatatype(*i);
- }
-
- for(std::vector<NodeManagerListener*>::iterator i = d_nodeManager->d_listeners.begin(); i != d_nodeManager->d_listeners.end(); ++i) {
- (*i)->nmNotifyNewDatatypes(dtts);
- }
-
- return dtts;
-}
-
-void ExprManager::checkResolvedDatatype(DatatypeType dtt) const {
- const Datatype& dt = dtt.getDatatype();
-
- AssertArgument(dt.isResolved(), dtt, "datatype should have been resolved");
-
- // for all constructors...
- for(Datatype::const_iterator i = dt.begin(), i_end = dt.end();
- i != i_end;
- ++i) {
- const DatatypeConstructor& c = *i;
- Type testerType CVC4_UNUSED = c.getTester().getType();
- Assert(c.isResolved() &&
- testerType.isTester() &&
- TesterType(testerType).getDomain() == dtt &&
- TesterType(testerType).getRangeType() == booleanType(),
- "malformed tester in datatype post-resolution");
- Type ctorType CVC4_UNUSED = c.getConstructor().getType();
- Assert(ctorType.isConstructor() &&
- ConstructorType(ctorType).getArity() == c.getNumArgs() &&
- ConstructorType(ctorType).getRangeType() == dtt,
- "malformed constructor in datatype post-resolution");
- // for all selectors...
- for(DatatypeConstructor::const_iterator j = c.begin(), j_end = c.end();
- j != j_end;
- ++j) {
- const DatatypeConstructorArg& a = *j;
- Type selectorType = a.getSelector().getType();
- Assert(a.isResolved() &&
- selectorType.isSelector() &&
- SelectorType(selectorType).getDomain() == dtt,
- "malformed selector in datatype post-resolution");
- // This next one's a "hard" check, performed in non-debug builds
- // as well; the other ones should all be guaranteed by the
- // CVC4::Datatype class, but this actually needs to be checked.
- AlwaysAssert(!SelectorType(selectorType).getRangeType().d_typeNode->isFunctionLike(),
- "cannot put function-like things in datatypes");
- }
- }
-}
-
-ConstructorType ExprManager::mkConstructorType(const DatatypeConstructor& constructor, Type range) const {
- NodeManagerScope nms(d_nodeManager);
- return Type(d_nodeManager, new TypeNode(d_nodeManager->mkConstructorType(constructor, *range.d_typeNode)));
-}
-
-SelectorType ExprManager::mkSelectorType(Type domain, Type range) const {
- NodeManagerScope nms(d_nodeManager);
- return Type(d_nodeManager, new TypeNode(d_nodeManager->mkSelectorType(*domain.d_typeNode, *range.d_typeNode)));
-}
-
-TesterType ExprManager::mkTesterType(Type domain) const {
- NodeManagerScope nms(d_nodeManager);
- return Type(d_nodeManager, new TypeNode(d_nodeManager->mkTesterType(*domain.d_typeNode)));
-}
-
-SortType ExprManager::mkSort(const std::string& name, uint32_t flags) const {
- NodeManagerScope nms(d_nodeManager);
- return SortType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name, flags))));
-}
-
-SortConstructorType ExprManager::mkSortConstructor(const std::string& name,
- size_t arity) const {
- NodeManagerScope nms(d_nodeManager);
- return SortConstructorType(Type(d_nodeManager,
- new TypeNode(d_nodeManager->mkSortConstructor(name, arity))));
-}
-
-/* - not in release 1.0
-Type ExprManager::mkPredicateSubtype(Expr lambda)
- throw(TypeCheckingException) {
- NodeManagerScope nms(d_nodeManager);
- try {
- return PredicateSubtype(Type(d_nodeManager,
- new TypeNode(d_nodeManager->mkPredicateSubtype(lambda))));
- } catch (const TypeCheckingExceptionPrivate& e) {
- throw TypeCheckingException(this, &e);
- }
-}
-*/
-
-/* - not in release 1.0
-Type ExprManager::mkPredicateSubtype(Expr lambda, Expr witness)
- throw(TypeCheckingException) {
- NodeManagerScope nms(d_nodeManager);
- try {
- return PredicateSubtype(Type(d_nodeManager,
- new TypeNode(d_nodeManager->mkPredicateSubtype(lambda, witness))));
- } catch (const TypeCheckingExceptionPrivate& e) {
- throw TypeCheckingException(this, &e);
- }
-}
-*/
-
-Type ExprManager::mkSubrangeType(const SubrangeBounds& bounds)
- throw(TypeCheckingException) {
- NodeManagerScope nms(d_nodeManager);
- try {
- return SubrangeType(Type(d_nodeManager,
- new TypeNode(d_nodeManager->mkSubrangeType(bounds))));
- } catch (const TypeCheckingExceptionPrivate& e) {
- throw TypeCheckingException(this, &e);
- }
-}
-
-/**
- * Get the type for the given Expr and optionally do type checking.
- *
- * Initial type computation will be near-constant time if
- * type checking is not requested. Results are memoized, so that
- * subsequent calls to getType() without type checking will be
- * constant time.
- *
- * Initial type checking is linear in the size of the expression.
- * Again, the results are memoized, so that subsequent calls to
- * getType(), with or without type checking, will be constant
- * time.
- *
- * NOTE: A TypeCheckingException can be thrown even when type
- * checking is not requested. getType() will always return a
- * valid and correct type and, thus, an exception will be thrown
- * when no valid or correct type can be computed (e.g., if the
- * arguments to a bit-vector operation aren't bit-vectors). When
- * type checking is not requested, getType() will do the minimum
- * amount of checking required to return a valid result.
- *
- * @param e the Expr for which we want a type
- * @param check whether we should check the type as we compute it
- * (default: false)
- */
-Type ExprManager::getType(Expr e, bool check) throw (TypeCheckingException) {
- NodeManagerScope nms(d_nodeManager);
- Type t;
- try {
- t = Type(d_nodeManager,
- new TypeNode(d_nodeManager->getType(e.getNode(), check)));
- } catch (const TypeCheckingExceptionPrivate& e) {
- throw TypeCheckingException(this, &e);
- }
- return t;
-}
-
-Expr ExprManager::mkVar(const std::string& name, Type type, uint32_t flags) {
- Assert(NodeManager::currentNM() == NULL, "ExprManager::mkVar() should only be called externally, not from within CVC4 code. Please use mkSkolem().");
- NodeManagerScope nms(d_nodeManager);
- Node* n = d_nodeManager->mkVarPtr(name, *type.d_typeNode, flags);
- Debug("nm") << "set " << name << " on " << *n << std::endl;
- INC_STAT_VAR(type, false);
- return Expr(this, n);
-}
-
-Expr ExprManager::mkVar(Type type, uint32_t flags) {
- Assert(NodeManager::currentNM() == NULL, "ExprManager::mkVar() should only be called externally, not from within CVC4 code. Please use mkSkolem().");
- NodeManagerScope nms(d_nodeManager);
- INC_STAT_VAR(type, false);
- return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode, flags));
-}
-
-Expr ExprManager::mkBoundVar(const std::string& name, Type type) {
- NodeManagerScope nms(d_nodeManager);
- Node* n = d_nodeManager->mkBoundVarPtr(name, *type.d_typeNode);
- Debug("nm") << "set " << name << " on " << *n << std::endl;
- INC_STAT_VAR(type, true);
- return Expr(this, n);
-}
-
-Expr ExprManager::mkBoundVar(Type type) {
- NodeManagerScope nms(d_nodeManager);
- INC_STAT_VAR(type, true);
- return Expr(this, d_nodeManager->mkBoundVarPtr(*type.d_typeNode));
-}
-
-Expr ExprManager::mkAssociative(Kind kind,
- const std::vector<Expr>& children) {
- CheckArgument( kind::isAssociative(kind), kind,
- "Illegal kind in mkAssociative: %s",
- kind::kindToString(kind).c_str());
-
- NodeManagerScope nms(d_nodeManager);
- const unsigned int max = maxArity(kind);
- const unsigned int min = minArity(kind);
- unsigned int numChildren = children.size();
-
- /* If the number of children is within bounds, then there's nothing to do. */
- if( numChildren <= max ) {
- return mkExpr(kind,children);
- }
-
- std::vector<Expr>::const_iterator it = children.begin() ;
- std::vector<Expr>::const_iterator end = children.end() ;
-
- /* The new top-level children and the children of each sub node */
- std::vector<Node> newChildren;
- std::vector<Node> subChildren;
-
- while( it != end && numChildren > max ) {
- /* Grab the next max children and make a node for them. */
- for( std::vector<Expr>::const_iterator next = it + max;
- it != next;
- ++it, --numChildren ) {
- subChildren.push_back(it->getNode());
- }
- Node subNode = d_nodeManager->mkNode(kind,subChildren);
- newChildren.push_back(subNode);
-
- subChildren.clear();
- }
-
- /* If there's children left, "top off" the Expr. */
- if(numChildren > 0) {
- /* If the leftovers are too few, just copy them into newChildren;
- * otherwise make a new sub-node */
- if(numChildren < min) {
- for(; it != end; ++it) {
- newChildren.push_back(it->getNode());
- }
- } else {
- for(; it != end; ++it) {
- subChildren.push_back(it->getNode());
- }
- Node subNode = d_nodeManager->mkNode(kind, subChildren);
- newChildren.push_back(subNode);
- }
- }
-
- /* It's inconceivable we could have enough children for this to fail
- * (more than 2^32, in most cases?). */
- AlwaysAssert( newChildren.size() <= max,
- "Too many new children in mkAssociative" );
-
- /* It would be really weird if this happened (it would require
- * min > 2, for one thing), but let's make sure. */
- AlwaysAssert( newChildren.size() >= min,
- "Too few new children in mkAssociative" );
-
- return Expr(this, d_nodeManager->mkNodePtr(kind,newChildren) );
-}
-
-unsigned ExprManager::minArity(Kind kind) {
- return metakind::getLowerBoundForKind(kind);
-}
-
-unsigned ExprManager::maxArity(Kind kind) {
- return metakind::getUpperBoundForKind(kind);
-}
-
-NodeManager* ExprManager::getNodeManager() const {
- return d_nodeManager;
-}
-
-Statistics ExprManager::getStatistics() const throw() {
- return Statistics(*d_nodeManager->getStatisticsRegistry());
-}
-
-SExpr ExprManager::getStatistic(const std::string& name) const throw() {
- return d_nodeManager->getStatisticsRegistry()->getStatistic(name);
-}
-
-namespace expr {
-
-Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap);
-
-TypeNode exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* to, ExprManagerMapCollection& vmap) {
- Debug("export") << "type: " << n << " " << n.getId() << std::endl;
- if(theory::kindToTheoryId(n.getKind()) == theory::THEORY_DATATYPES) {
- throw ExportUnsupportedException
- ("export of types belonging to theory of DATATYPES kinds unsupported");
- }
- if(n.getMetaKind() == kind::metakind::PARAMETERIZED &&
- n.getKind() != kind::SORT_TYPE) {
- throw ExportUnsupportedException
- ("export of PARAMETERIZED-kinded types (other than SORT_KIND) not supported");
- }
- if(n.getKind() == kind::TYPE_CONSTANT) {
- return to->mkTypeConst(n.getConst<TypeConstant>());
- } else if(n.getKind() == kind::BITVECTOR_TYPE) {
- return to->mkBitVectorType(n.getConst<BitVectorSize>());
- } else if(n.getKind() == kind::SUBRANGE_TYPE) {
- return to->mkSubrangeType(n.getSubrangeBounds());
- }
- Type from_t = from->toType(n);
- Type& to_t = vmap.d_typeMap[from_t];
- if(! to_t.isNull()) {
- Debug("export") << "+ mapped `" << from_t << "' to `" << to_t << "'" << std::endl;
- return *Type::getTypeNode(to_t);
- }
- NodeBuilder<> children(to, n.getKind());
- if(n.getKind() == kind::SORT_TYPE) {
- Debug("export") << "type: operator: " << n.getOperator() << std::endl;
- // make a new sort tag in target node manager
- Node sortTag = NodeBuilder<0>(to, kind::SORT_TAG);
- children << sortTag;
- }
- for(TypeNode::iterator i = n.begin(), i_end = n.end(); i != i_end; ++i) {
- Debug("export") << "type: child: " << *i << std::endl;
- children << exportTypeInternal(*i, from, to, vmap);
- }
- TypeNode out = children.constructTypeNode();// FIXME thread safety
- to_t = to->toType(out);
- return out;
-}/* exportTypeInternal() */
-
-}/* CVC4::expr namespace */
-
-Type ExprManager::exportType(const Type& t, ExprManager* em, ExprManagerMapCollection& vmap) {
- Assert(t.d_nodeManager != em->d_nodeManager,
- "Can't export a Type to the same ExprManager");
- NodeManagerScope ems(t.d_nodeManager);
- return Type(em->d_nodeManager,
- new TypeNode(expr::exportTypeInternal(*t.d_typeNode, t.d_nodeManager, em->d_nodeManager, vmap)));
-}
-
-${mkConst_implementations}
-
-}/* CVC4 namespace */
+++ /dev/null
-/********************* */
-/*! \file expr_manager_template.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Dejan Jovanovic
- ** Minor contributors (to current version): Andrew Reynolds, Kshitij Bansal, Tim King, Christopher L. Conway
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Public-facing expression manager interface
- **
- ** Public-facing expression manager interface.
- **/
-
-#include "cvc4_public.h"
-
-#ifndef __CVC4__EXPR_MANAGER_H
-#define __CVC4__EXPR_MANAGER_H
-
-#include <vector>
-
-#include "expr/kind.h"
-#include "expr/type.h"
-#include "expr/expr.h"
-#include "util/subrange_bound.h"
-#include "util/statistics.h"
-#include "util/sexpr.h"
-
-${includes}
-
-// This is a hack, but an important one: if there's an error, the
-// compiler directs the user to the template file instead of the
-// generated one. We don't want the user to modify the generated one,
-// since it'll get overwritten on a later build.
-#line 38 "${template}"
-
-namespace CVC4 {
-
-class Expr;
-class SmtEngine;
-class NodeManager;
-class Options;
-class IntStat;
-struct ExprManagerMapCollection;
-class StatisticsRegistry;
-class ResourceManager;
-
-namespace expr {
- namespace pickle {
- class Pickler;
- }/* CVC4::expr::pickle namespace */
-}/* CVC4::expr namespace */
-
-namespace stats {
- StatisticsRegistry* getStatisticsRegistry(ExprManager*);
-}/* CVC4::stats namespace */
-
-class CVC4_PUBLIC ExprManager {
-private:
- /** The internal node manager */
- NodeManager* d_nodeManager;
-
- /** Counts of expressions and variables created of a given kind */
- IntStat* d_exprStatisticsVars[LAST_TYPE];
- IntStat* d_exprStatistics[kind::LAST_KIND];
-
- /**
- * Returns the internal node manager. This should only be used by
- * internal users, i.e. the friend classes.
- */
- NodeManager* getNodeManager() const;
-
- /**
- * Check some things about a newly-created DatatypeType.
- */
- void checkResolvedDatatype(DatatypeType dtt) const;
-
- /**
- * SmtEngine will use all the internals, so it will grab the
- * NodeManager.
- */
- friend class SmtEngine;
-
- /** ExprManagerScope reaches in to get the NodeManager */
- friend class ExprManagerScope;
-
- /** NodeManager reaches in to get the NodeManager */
- friend class NodeManager;
-
- /** Statistics reach in to get the StatisticsRegistry */
- friend ::CVC4::StatisticsRegistry* ::CVC4::stats::getStatisticsRegistry(ExprManager*);
-
- /** Get the underlying statistics registry. */
- StatisticsRegistry* getStatisticsRegistry() throw();
-
- // undefined, private copy constructor and assignment op (disallow copy)
- ExprManager(const ExprManager&) CVC4_UNDEFINED;
- ExprManager& operator=(const ExprManager&) CVC4_UNDEFINED;
-
-public:
-
- /**
- * Creates an expression manager with default options.
- */
- ExprManager();
-
- /**
- * Creates an expression manager.
- *
- * @param options the earlyTypeChecking field is used to configure
- * whether to do at Expr creation time.
- */
- explicit ExprManager(const Options& options);
-
- /**
- * Destroys the expression manager. No will be deallocated at this point, so
- * any expression references that used to be managed by this expression
- * manager and are left-over are bad.
- */
- ~ExprManager() throw();
-
- /** Get this expr manager's options */
- const Options& getOptions() const;
-
- /** Get this expr manager's resource manager */
- ResourceManager* getResourceManager() throw();
-
- /** Get the type for booleans */
- BooleanType booleanType() const;
-
- /** Get the type for strings. */
- StringType stringType() const;
-
- /** Get the type for reals. */
- RealType realType() const;
-
- /** Get the type for integers */
- IntegerType integerType() const;
-
- /**
- * Make a unary expression of a given kind (NOT, BVNOT, ...).
- * @param kind the kind of expression
- * @param child1 kind the kind of expression
- * @return the expression
- */
- Expr mkExpr(Kind kind, Expr child1);
-
- /**
- * Make a binary expression of a given kind (AND, PLUS, ...).
- * @param kind the kind of expression
- * @param child1 the first child of the new expression
- * @param child2 the second child of the new expression
- * @return the expression
- */
- Expr mkExpr(Kind kind, Expr child1, Expr child2);
-
- /**
- * Make a 3-ary expression of a given kind (AND, PLUS, ...).
- * @param kind the kind of expression
- * @param child1 the first child of the new expression
- * @param child2 the second child of the new expression
- * @param child3 the third child of the new expression
- * @return the expression
- */
- Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3);
-
- /**
- * Make a 4-ary expression of a given kind (AND, PLUS, ...).
- * @param kind the kind of expression
- * @param child1 the first child of the new expression
- * @param child2 the second child of the new expression
- * @param child3 the third child of the new expression
- * @param child4 the fourth child of the new expression
- * @return the expression
- */
- Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4);
-
- /**
- * Make a 5-ary expression of a given kind (AND, PLUS, ...).
- * @param kind the kind of expression
- * @param child1 the first child of the new expression
- * @param child2 the second child of the new expression
- * @param child3 the third child of the new expression
- * @param child4 the fourth child of the new expression
- * @param child5 the fifth child of the new expression
- * @return the expression
- */
- Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4,
- Expr child5);
-
- /**
- * Make an n-ary expression of given kind given a vector of its
- * children
- *
- * @param kind the kind of expression to build
- * @param children the subexpressions
- * @return the n-ary expression
- */
- Expr mkExpr(Kind kind, const std::vector<Expr>& children);
-
- /**
- * Make an n-ary expression of given kind given a first arg and
- * a vector of its remaining children (this can be useful where the
- * kind is parameterized operator, so the first arg is really an
- * arg to the kind to construct an operator)
- *
- * @param kind the kind of expression to build
- * @param child1 the first subexpression
- * @param otherChildren the remaining subexpressions
- * @return the n-ary expression
- */
- Expr mkExpr(Kind kind, Expr child1, const std::vector<Expr>& otherChildren);
-
- /**
- * Make a nullary parameterized expression with the given operator.
- *
- * @param opExpr the operator expression
- * @return the nullary expression
- */
- Expr mkExpr(Expr opExpr);
-
- /**
- * Make a unary parameterized expression with the given operator.
- *
- * @param opExpr the operator expression
- * @param child1 the subexpression
- * @return the unary expression
- */
- Expr mkExpr(Expr opExpr, Expr child1);
-
- /**
- * Make a binary parameterized expression with the given operator.
- *
- * @param opExpr the operator expression
- * @param child1 the first subexpression
- * @param child2 the second subexpression
- * @return the binary expression
- */
- Expr mkExpr(Expr opExpr, Expr child1, Expr child2);
-
- /**
- * Make a ternary parameterized expression with the given operator.
- *
- * @param opExpr the operator expression
- * @param child1 the first subexpression
- * @param child2 the second subexpression
- * @param child3 the third subexpression
- * @return the ternary expression
- */
- Expr mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3);
-
- /**
- * Make a quaternary parameterized expression with the given operator.
- *
- * @param opExpr the operator expression
- * @param child1 the first subexpression
- * @param child2 the second subexpression
- * @param child3 the third subexpression
- * @param child4 the fourth subexpression
- * @return the quaternary expression
- */
- Expr mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3, Expr child4);
-
- /**
- * Make a quinary parameterized expression with the given operator.
- *
- * @param opExpr the operator expression
- * @param child1 the first subexpression
- * @param child2 the second subexpression
- * @param child3 the third subexpression
- * @param child4 the fourth subexpression
- * @param child5 the fifth subexpression
- * @return the quinary expression
- */
- Expr mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3, Expr child4,
- Expr child5);
-
- /**
- * Make an n-ary expression of given operator to apply and a vector
- * of its children
- *
- * @param opExpr the operator expression
- * @param children the subexpressions
- * @return the n-ary expression
- */
- Expr mkExpr(Expr opExpr, const std::vector<Expr>& children);
-
- /** Create a constant of type T */
- template <class T>
- Expr mkConst(const T&);
-
- /**
- * Create an Expr by applying an associative operator to the children.
- * If <code>children.size()</code> is greater than the max arity for
- * <code>kind</code>, then the expression will be broken up into
- * suitably-sized chunks, taking advantage of the associativity of
- * <code>kind</code>. For example, if kind <code>FOO</code> has max arity
- * 2, then calling <code>mkAssociative(FOO,a,b,c)</code> will return
- * <code>(FOO (FOO a b) c)</code> or <code>(FOO a (FOO b c))</code>.
- * The order of the arguments will be preserved in a left-to-right
- * traversal of the resulting tree.
- */
- Expr mkAssociative(Kind kind, const std::vector<Expr>& children);
-
- /**
- * Determine whether Exprs of a particular Kind have operators.
- * @returns true if Exprs of Kind k have operators.
- */
- static bool hasOperator(Kind k);
-
- /**
- * Get the (singleton) operator of an OPERATOR-kinded kind. The
- * returned Expr e will have kind BUILTIN, and calling
- * e.getConst<CVC4::Kind>() will yield k.
- */
- Expr operatorOf(Kind k);
-
- /** Make a function type from domain to range. */
- FunctionType mkFunctionType(Type domain, Type range);
-
- /**
- * Make a function type with input types from argTypes.
- * <code>argTypes</code> must have at least one element.
- */
- FunctionType mkFunctionType(const std::vector<Type>& argTypes, Type range);
-
- /**
- * Make a function type with input types from
- * <code>sorts[0..sorts.size()-2]</code> and result type
- * <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have
- * at least 2 elements.
- */
- FunctionType mkFunctionType(const std::vector<Type>& sorts);
-
- /**
- * Make a predicate type with input types from
- * <code>sorts</code>. The result with be a function type with range
- * <code>BOOLEAN</code>. <code>sorts</code> must have at least one
- * element.
- */
- FunctionType mkPredicateType(const std::vector<Type>& sorts);
-
- /**
- * Make a tuple type with types from
- * <code>types[0..types.size()-1]</code>. <code>types</code> must
- * have at least one element.
- */
- TupleType mkTupleType(const std::vector<Type>& types);
-
- /**
- * Make a record type with types from the rec parameter.
- */
- RecordType mkRecordType(const Record& rec);
-
- /**
- * Make a symbolic expressiontype with types from
- * <code>types[0..types.size()-1]</code>. <code>types</code> may
- * have any number of elements.
- */
- SExprType mkSExprType(const std::vector<Type>& types);
-
- /** Make a type representing a bit-vector of the given size. */
- BitVectorType mkBitVectorType(unsigned size) const;
-
- /** Make the type of arrays with the given parameterization. */
- ArrayType mkArrayType(Type indexType, Type constituentType) const;
-
- /** Make the type of set with the given parameterization. */
- SetType mkSetType(Type elementType) const;
-
- /** Make a type representing the given datatype. */
- DatatypeType mkDatatypeType(const Datatype& datatype);
-
- /**
- * Make a set of types representing the given datatypes, which may be
- * mutually recursive.
- */
- std::vector<DatatypeType>
- mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes);
-
- /**
- * Make a set of types representing the given datatypes, which may
- * be mutually recursive. unresolvedTypes is a set of SortTypes
- * that were used as placeholders in the Datatypes for the Datatypes
- * of the same name. This is just a more complicated version of the
- * above mkMutualDatatypeTypes() function, but is required to handle
- * complex types.
- *
- * For example, unresolvedTypes might contain the single sort "list"
- * (with that name reported from SortType::getName()). The
- * datatypes list might have the single datatype
- *
- * DATATYPE
- * list = cons(car:ARRAY INT OF list, cdr:list) | nil;
- * END;
- *
- * To represent the Type of the array, the user had to create a
- * placeholder type (an uninterpreted sort) to stand for "list" in
- * the type of "car". It is this placeholder sort that should be
- * passed in unresolvedTypes. If the datatype was of the simpler
- * form:
- *
- * DATATYPE
- * list = cons(car:list, cdr:list) | nil;
- * END;
- *
- * then no complicated Type needs to be created, and the above,
- * simpler form of mkMutualDatatypeTypes() is enough.
- */
- std::vector<DatatypeType>
- mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
- const std::set<Type>& unresolvedTypes);
-
- /**
- * Make a type representing a constructor with the given parameterization.
- */
- ConstructorType mkConstructorType(const DatatypeConstructor& constructor, Type range) const;
-
- /** Make a type representing a selector with the given parameterization. */
- SelectorType mkSelectorType(Type domain, Type range) const;
-
- /** Make a type representing a tester with the given parameterization. */
- TesterType mkTesterType(Type domain) const;
-
- /** Bits for use in mkSort() flags. */
- enum {
- SORT_FLAG_NONE = 0,
- SORT_FLAG_PLACEHOLDER = 1
- };/* enum */
-
- /** Make a new sort with the given name. */
- SortType mkSort(const std::string& name, uint32_t flags = SORT_FLAG_NONE) const;
-
- /** Make a sort constructor from a name and arity. */
- SortConstructorType mkSortConstructor(const std::string& name,
- size_t arity) const;
-
- /**
- * Make a predicate subtype type defined by the given LAMBDA
- * expression. A TypeCheckingException can be thrown if lambda is
- * not a LAMBDA, or is ill-typed, or if CVC4 fails at proving that
- * the resulting predicate subtype is inhabited.
- */
- // not in release 1.0
- //Type mkPredicateSubtype(Expr lambda)
- // throw(TypeCheckingException);
-
- /**
- * Make a predicate subtype type defined by the given LAMBDA
- * expression and whose non-emptiness is witnessed by the given
- * witness. A TypeCheckingException can be thrown if lambda is not
- * a LAMBDA, or is ill-typed, or if the witness is not a witness or
- * ill-typed.
- */
- // not in release 1.0
- //Type mkPredicateSubtype(Expr lambda, Expr witness)
- // throw(TypeCheckingException);
-
- /**
- * Make an integer subrange type as defined by the argument.
- */
- Type mkSubrangeType(const SubrangeBounds& bounds)
- throw(TypeCheckingException);
-
- /** Get the type of an expression */
- Type getType(Expr e, bool check = false)
- throw(TypeCheckingException);
-
- /** Bits for use in mkVar() flags. */
- enum {
- VAR_FLAG_NONE = 0,
- VAR_FLAG_GLOBAL = 1,
- VAR_FLAG_DEFINED = 2
- };/* enum */
-
- /**
- * Create a new, fresh variable. This variable is guaranteed to be
- * distinct from every variable thus far in the ExprManager, even
- * if it shares a name with another; this is to support any kind of
- * scoping policy on top of ExprManager. The SymbolTable class
- * can be used to store and lookup symbols by name, if desired.
- *
- * @param name a name to associate to the fresh new variable
- * @param type the type for the new variable
- * @param flags - VAR_FLAG_NONE - no flags;
- * VAR_FLAG_GLOBAL - whether this variable is to be
- * considered "global" or not. Note that this information isn't
- * used by the ExprManager, but is passed on to the ExprManager's
- * event subscribers like the model-building service; if isGlobal
- * is true, this newly-created variable will still available in
- * models generated after an intervening pop.
- * VAR_FLAG_DEFINED - if this is to be a "defined" symbol, e.g., for
- * use with SmtEngine::defineFunction(). This keeps a declaration
- * from being emitted in API dumps (since a subsequent definition is
- * expected to be dumped instead).
- */
- Expr mkVar(const std::string& name, Type type, uint32_t flags = VAR_FLAG_NONE);
-
- /**
- * Create a (nameless) new, fresh variable. This variable is guaranteed
- * to be distinct from every variable thus far in the ExprManager.
- *
- * @param type the type for the new variable
- * @param flags - VAR_FLAG_GLOBAL - whether this variable is to be considered "global"
- * or not. Note that this information isn't used by the ExprManager,
- * but is passed on to the ExprManager's event subscribers like the
- * model-building service; if isGlobal is true, this newly-created
- * variable will still available in models generated after an
- * intervening pop.
- */
- Expr mkVar(Type type, uint32_t flags = VAR_FLAG_NONE);
-
- /**
- * Create a new, fresh variable for use in a binder expression
- * (the BOUND_VAR_LIST of a FORALL, EXISTS, or LAMBDA). It is
- * an error for this bound variable to exist outside of a binder,
- * and it should also only be used in a single binder expression.
- * That is, two distinct FORALL expressions should use entirely
- * disjoint sets of bound variables (however, a single FORALL
- * expression can be used in multiple places in a formula without
- * a problem). This newly-created bound variable is guaranteed to
- * be distinct from every variable thus far in the ExprManager, even
- * if it shares a name with another; this is to support any kind of
- * scoping policy on top of ExprManager. The SymbolTable class
- * can be used to store and lookup symbols by name, if desired.
- *
- * @param name a name to associate to the fresh new bound variable
- * @param type the type for the new bound variable
- */
- Expr mkBoundVar(const std::string& name, Type type);
-
- /**
- * Create a (nameless) new, fresh variable for use in a binder
- * expression (the BOUND_VAR_LIST of a FORALL, EXISTS, or LAMBDA).
- * It is an error for this bound variable to exist outside of a
- * binder, and it should also only be used in a single binder
- * expression. That is, two distinct FORALL expressions should use
- * entirely disjoint sets of bound variables (however, a single FORALL
- * expression can be used in multiple places in a formula without
- * a problem). This newly-created bound variable is guaranteed to
- * be distinct from every variable thus far in the ExprManager.
- *
- * @param type the type for the new bound variable
- */
- Expr mkBoundVar(Type type);
-
- /** Get a reference to the statistics registry for this ExprManager */
- Statistics getStatistics() const throw();
-
- /** Get a reference to the statistics registry for this ExprManager */
- SExpr getStatistic(const std::string& name) const throw();
-
- /** Export an expr to a different ExprManager */
- //static Expr exportExpr(const Expr& e, ExprManager* em);
- /** Export a type to a different ExprManager */
- static Type exportType(const Type& t, ExprManager* em, ExprManagerMapCollection& vmap);
-
- /** Returns the minimum arity of the given kind. */
- static unsigned minArity(Kind kind);
-
- /** Returns the maximum arity of the given kind. */
- static unsigned maxArity(Kind kind);
-
-};/* class ExprManager */
-
-${mkConst_instantiations}
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__EXPR_MANAGER_H */
+++ /dev/null
-/********************* */
-/*! \file node_manager.h
- ** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: Christopher L. Conway, Morgan Deters
- ** Minor contributors (to current version): ACSYS, Tianyi Liang, Kshitij Bansal, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief A manager for Nodes
- **
- ** A manager for Nodes.
- **
- ** Reviewed by Chris Conway, Apr 5 2010 (bug #65).
- **/
-
-#include "cvc4_private.h"
-
-/* circular dependency; force node.h first */
-//#include "expr/attribute.h"
-#include "expr/node.h"
-#include "expr/type_node.h"
-#include "expr/expr.h"
-#include "expr/expr_manager.h"
-
-#ifndef __CVC4__NODE_MANAGER_H
-#define __CVC4__NODE_MANAGER_H
-
-#include <vector>
-#include <string>
-#include <ext/hash_set>
-
-#include "expr/kind.h"
-#include "expr/metakind.h"
-#include "expr/node_value.h"
-#include "util/subrange_bound.h"
-#include "util/tls.h"
-#include "options/options.h"
-
-namespace CVC4 {
-
-class StatisticsRegistry;
-class ResourceManager;
-
-namespace expr {
- namespace attr {
- class AttributeUniqueId;
- class AttributeManager;
- }/* CVC4::expr::attr namespace */
-
- class TypeChecker;
-}/* CVC4::expr namespace */
-
-/**
- * An interface that an interested party can implement and then subscribe
- * to NodeManager events via NodeManager::subscribeEvents(this).
- */
-class NodeManagerListener {
-public:
- virtual ~NodeManagerListener() { }
- virtual void nmNotifyNewSort(TypeNode tn, uint32_t flags) { }
- virtual void nmNotifyNewSortConstructor(TypeNode tn) { }
- virtual void nmNotifyInstantiateSortConstructor(TypeNode ctor, TypeNode sort, uint32_t flags) { }
- virtual void nmNotifyNewDatatypes(const std::vector<DatatypeType>& datatypes) { }
- virtual void nmNotifyNewVar(TNode n, uint32_t flags) { }
- virtual void nmNotifyNewSkolem(TNode n, const std::string& comment, uint32_t flags) { }
- /**
- * Notify a listener of a Node that's being GCed. If this function stores a reference
- * to the Node somewhere, very bad things will happen.
- */
- virtual void nmNotifyDeleteNode(TNode n) { }
-};/* class NodeManagerListener */
-
-class NodeManager {
- template <unsigned nchild_thresh> friend class CVC4::NodeBuilder;
- friend class NodeManagerScope;
- friend class expr::NodeValue;
- friend class expr::TypeChecker;
-
- // friends so they can access mkVar() here, which is private
- friend Expr ExprManager::mkVar(const std::string&, Type, uint32_t flags);
- friend Expr ExprManager::mkVar(Type, uint32_t flags);
-
- // friend so it can access NodeManager's d_listeners and notify clients
- friend std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>&, const std::set<Type>&);
-
- /** Predicate for use with STL algorithms */
- struct NodeValueReferenceCountNonZero {
- bool operator()(expr::NodeValue* nv) { return nv->d_rc > 0; }
- };
-
- typedef __gnu_cxx::hash_set<expr::NodeValue*,
- expr::NodeValuePoolHashFunction,
- expr::NodeValuePoolEq> NodeValuePool;
- typedef __gnu_cxx::hash_set<expr::NodeValue*,
- expr::NodeValueIDHashFunction,
- expr::NodeValueEq> ZombieSet;
-
- static CVC4_THREADLOCAL(NodeManager*) s_current;
-
- Options* d_options;
- StatisticsRegistry* d_statisticsRegistry;
- ResourceManager* d_resourceManager;
-
- NodeValuePool d_nodeValuePool;
-
- size_t next_id;
-
- expr::attr::AttributeManager* d_attrManager;
-
- /** The associated ExprManager */
- ExprManager* d_exprManager;
-
- /**
- * The node value we're currently freeing. This unique node value
- * is permitted to have outstanding TNodes to it (in "soft"
- * contexts, like as a key in attribute tables), even though
- * normally it's an error to have a TNode to a node value with a
- * reference count of 0. Being "under deletion" also enables
- * assertions that inc() is not called on it. (A poorly-behaving
- * attribute cleanup function could otherwise create a "Node" that
- * points to the node value that is in the process of being deleted,
- * springing it back to life.)
- */
- expr::NodeValue* d_nodeUnderDeletion;
-
- /**
- * True iff we are in reclaimZombies(). This avoids unnecessary
- * recursion; a NodeValue being deleted might zombify other
- * NodeValues, but these shouldn't trigger a (recursive) call to
- * reclaimZombies().
- */
- bool d_inReclaimZombies;
-
- /**
- * The set of zombie nodes. We may want to revisit this design, as
- * we might like to delete nodes in least-recently-used order. But
- * we also need to avoid processing a zombie twice.
- */
- ZombieSet d_zombies;
-
- /**
- * A set of operator singletons (w.r.t. to this NodeManager
- * instance) for operators. Conceptually, Nodes with kind, say,
- * PLUS, are APPLYs of a PLUS operator to arguments. This array
- * holds the set of operators for these things. A PLUS operator is
- * a Node with kind "BUILTIN", and if you call
- * plusOperator->getConst<CVC4::Kind>(), you get kind::PLUS back.
- */
- Node d_operators[kind::LAST_KIND];
-
- /**
- * A list of subscribers for NodeManager events.
- */
- std::vector<NodeManagerListener*> d_listeners;
-
- /**
- * A map of tuple and record types to their corresponding datatype.
- */
- std::hash_map<TypeNode, TypeNode, TypeNodeHashFunction> d_tupleAndRecordTypes;
-
- /**
- * Keep a count of all abstract values produced by this NodeManager.
- * Abstract values have a type attribute, so if multiple SmtEngines
- * are attached to this NodeManager, we don't want their abstract
- * values to overlap.
- */
- unsigned d_abstractValueCount;
-
- /**
- * A counter used to produce unique skolem names.
- *
- * Note that it is NOT incremented when skolems are created using
- * SKOLEM_EXACT_NAME, so it is NOT a count of the skolems produced
- * by this node manager.
- */
- unsigned d_skolemCounter;
-
- /**
- * Look up a NodeValue in the pool associated to this NodeManager.
- * The NodeValue argument need not be a "completely-constructed"
- * NodeValue. In particular, "non-inlined" constants are permitted
- * (see below).
- *
- * For non-CONSTANT metakinds, nv's d_kind and d_nchildren should be
- * correctly set, and d_children[0..n-1] should be valid (extant)
- * NodeValues for lookup.
- *
- * For CONSTANT metakinds, nv's d_kind should be set correctly.
- * Normally a CONSTANT would have d_nchildren == 0 and the constant
- * value inlined in the d_children space. However, here we permit
- * "non-inlined" NodeValues to avoid unnecessary copying. For
- * these, d_nchildren == 1, and d_nchildren is a pointer to the
- * constant value.
- *
- * The point of this complex design is to permit efficient lookups
- * (without fully constructing a NodeValue). In the case that the
- * argument is not fully constructed, and this function returns
- * NULL, the caller should fully construct an equivalent one before
- * calling poolInsert(). NON-FULLY-CONSTRUCTED NODEVALUES are not
- * permitted in the pool!
- */
- inline expr::NodeValue* poolLookup(expr::NodeValue* nv) const;
-
- /**
- * Insert a NodeValue into the NodeManager's pool.
- *
- * It is an error to insert a NodeValue already in the pool.
- * Enquire first with poolLookup().
- */
- inline void poolInsert(expr::NodeValue* nv);
-
- /**
- * Remove a NodeValue from the NodeManager's pool.
- *
- * It is an error to request the removal of a NodeValue from the
- * pool that is not in the pool.
- */
- inline void poolRemove(expr::NodeValue* nv);
-
- /**
- * Determine if nv is currently being deleted by the NodeManager.
- */
- inline bool isCurrentlyDeleting(const expr::NodeValue* nv) const {
- return d_nodeUnderDeletion == nv;
- }
-
- /**
- * Register a NodeValue as a zombie.
- */
- inline void markForDeletion(expr::NodeValue* nv) {
- Assert(nv->d_rc == 0);
-
- // if d_reclaiming is set, make sure we don't call
- // reclaimZombies(), because it's already running.
- if(Debug.isOn("gc")) {
- Debug("gc") << "zombifying node value " << nv
- << " [" << nv->d_id << "]: ";
- nv->printAst(Debug("gc"));
- Debug("gc") << (d_inReclaimZombies ? " [CURRENTLY-RECLAIMING]" : "")
- << std::endl;
- }
- d_zombies.insert(nv);// FIXME multithreading
-
- if(safeToReclaimZombies()) {
- if(d_zombies.size() > 5000) {
- reclaimZombies();
- }
- }
- }
-
- /**
- * Reclaim all zombies.
- */
- void reclaimZombies();
-
- /**
- * It is safe to collect zombies.
- */
- bool safeToReclaimZombies() const;
-
- /**
- * This template gives a mechanism to stack-allocate a NodeValue
- * with enough space for N children (where N is a compile-time
- * constant). You use it like this:
- *
- * NVStorage<4> nvStorage;
- * NodeValue& nvStack = reinterpret_cast<NodeValue&>(nvStorage);
- *
- * ...and then you can use nvStack as a NodeValue that you know has
- * room for 4 children.
- */
- template <size_t N>
- struct NVStorage {
- expr::NodeValue nv;
- expr::NodeValue* child[N];
- };/* struct NodeManager::NVStorage<N> */
-
- /* A note on isAtomic() and isAtomicFormula() (in CVC3 parlance)..
- *
- * It has been decided for now to hold off on implementations of
- * these functions, as they may only be needed in CNF conversion,
- * where it's pointless to do a lazy isAtomic determination by
- * searching through the DAG, and storing it, since the result will
- * only be used once. For more details see the 4/27/2010 CVC4
- * developer's meeting notes at:
- *
- * http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_April_27,_2010#isAtomic.28.29_and_isAtomicFormula.28.29
- */
- // bool containsDecision(TNode); // is "atomic"
- // bool properlyContainsDecision(TNode); // all children are atomic
-
- // undefined private copy constructor (disallow copy)
- NodeManager(const NodeManager&) CVC4_UNDEFINED;
-
- void init();
-
- /**
- * Create a variable with the given name and type. NOTE that no
- * lookup is done on the name. If you mkVar("a", type) and then
- * mkVar("a", type) again, you have two variables. The NodeManager
- * version of this is private to avoid internal uses of mkVar() from
- * within CVC4. Such uses should employ mkSkolem() instead.
- */
- Node mkVar(const std::string& name, const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
- Node* mkVarPtr(const std::string& name, const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
-
- /** Create a variable with the given type. */
- Node mkVar(const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
- Node* mkVarPtr(const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
-
-public:
-
- explicit NodeManager(ExprManager* exprManager);
- explicit NodeManager(ExprManager* exprManager, const Options& options);
- ~NodeManager();
-
- /** The node manager in the current public-facing CVC4 library context */
- static NodeManager* currentNM() { return s_current; }
- /** The resource manager associated with the current node manager */
- static ResourceManager* currentResourceManager() { return s_current->d_resourceManager; }
-
- /** Get this node manager's options (const version) */
- const Options& getOptions() const {
- return *d_options;
- }
-
- /** Get this node manager's options (non-const version) */
- Options& getOptions() {
- return *d_options;
- }
-
- /** Get this node manager's resource manager */
- ResourceManager* getResourceManager() throw() { return d_resourceManager; }
-
- /** Get this node manager's statistics registry */
- StatisticsRegistry* getStatisticsRegistry() const throw() {
- return d_statisticsRegistry;
- }
-
- /** Subscribe to NodeManager events */
- void subscribeEvents(NodeManagerListener* listener) {
- Assert(std::find(d_listeners.begin(), d_listeners.end(), listener) == d_listeners.end(), "listener already subscribed");
- d_listeners.push_back(listener);
- }
-
- /** Unsubscribe from NodeManager events */
- void unsubscribeEvents(NodeManagerListener* listener) {
- std::vector<NodeManagerListener*>::iterator elt = std::find(d_listeners.begin(), d_listeners.end(), listener);
- Assert(elt != d_listeners.end(), "listener not subscribed");
- d_listeners.erase(elt);
- }
-
- /** Get a Kind from an operator expression */
- static inline Kind operatorToKind(TNode n);
-
- // general expression-builders
-
- /** Create a node with one child. */
- Node mkNode(Kind kind, TNode child1);
- Node* mkNodePtr(Kind kind, TNode child1);
-
- /** Create a node with two children. */
- Node mkNode(Kind kind, TNode child1, TNode child2);
- Node* mkNodePtr(Kind kind, TNode child1, TNode child2);
-
- /** Create a node with three children. */
- Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3);
- Node* mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3);
-
- /** Create a node with four children. */
- Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3,
- TNode child4);
- Node* mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3,
- TNode child4);
-
- /** Create a node with five children. */
- Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3,
- TNode child4, TNode child5);
- Node* mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3,
- TNode child4, TNode child5);
-
- /** Create a node with an arbitrary number of children. */
- template <bool ref_count>
- Node mkNode(Kind kind, const std::vector<NodeTemplate<ref_count> >& children);
- template <bool ref_count>
- Node* mkNodePtr(Kind kind, const std::vector<NodeTemplate<ref_count> >& children);
-
- /** Create a node (with no children) by operator. */
- Node mkNode(TNode opNode);
- Node* mkNodePtr(TNode opNode);
-
- /** Create a node with one child by operator. */
- Node mkNode(TNode opNode, TNode child1);
- Node* mkNodePtr(TNode opNode, TNode child1);
-
- /** Create a node with two children by operator. */
- Node mkNode(TNode opNode, TNode child1, TNode child2);
- Node* mkNodePtr(TNode opNode, TNode child1, TNode child2);
-
- /** Create a node with three children by operator. */
- Node mkNode(TNode opNode, TNode child1, TNode child2, TNode child3);
- Node* mkNodePtr(TNode opNode, TNode child1, TNode child2, TNode child3);
-
- /** Create a node with four children by operator. */
- Node mkNode(TNode opNode, TNode child1, TNode child2, TNode child3,
- TNode child4);
- Node* mkNodePtr(TNode opNode, TNode child1, TNode child2, TNode child3,
- TNode child4);
-
- /** Create a node with five children by operator. */
- Node mkNode(TNode opNode, TNode child1, TNode child2, TNode child3,
- TNode child4, TNode child5);
- Node* mkNodePtr(TNode opNode, TNode child1, TNode child2, TNode child3,
- TNode child4, TNode child5);
-
- /** Create a node by applying an operator to the children. */
- template <bool ref_count>
- Node mkNode(TNode opNode, const std::vector<NodeTemplate<ref_count> >& children);
- template <bool ref_count>
- Node* mkNodePtr(TNode opNode, const std::vector<NodeTemplate<ref_count> >& children);
-
- Node mkBoundVar(const std::string& name, const TypeNode& type);
- Node* mkBoundVarPtr(const std::string& name, const TypeNode& type);
-
- Node mkBoundVar(const TypeNode& type);
- Node* mkBoundVarPtr(const TypeNode& type);
-
- /**
- * Optional flags used to control behavior of NodeManager::mkSkolem().
- * They should be composed with a bitwise OR (e.g.,
- * "SKOLEM_NO_NOTIFY | SKOLEM_EXACT_NAME"). Of course, SKOLEM_DEFAULT
- * cannot be composed in such a manner.
- */
- enum SkolemFlags {
- SKOLEM_DEFAULT = 0, /**< default behavior */
- SKOLEM_NO_NOTIFY = 1, /**< do not notify subscribers */
- SKOLEM_EXACT_NAME = 2,/**< do not make the name unique by adding the id */
- SKOLEM_IS_GLOBAL = 4 /**< global vars appear in models even after a pop */
- };/* enum SkolemFlags */
-
- /**
- * Create a skolem constant with the given name, type, and comment.
- *
- * @param prefix the name of the new skolem variable is the prefix
- * appended with a unique ID. This way a family of skolem variables
- * can be made with unique identifiers, used in dump, tracing, and
- * debugging output. Use SKOLEM_EXECT_NAME flag if you don't want
- * a unique ID appended and use prefix as the name.
- *
- * @param type the type of the skolem variable to create
- *
- * @param comment a comment for dumping output; if declarations are
- * being dumped, this is included in a comment before the declaration
- * and can be quite useful for debugging
- *
- * @param flags an optional mask of bits from SkolemFlags to control
- * mkSkolem() behavior
- */
- Node mkSkolem(const std::string& prefix, const TypeNode& type,
- const std::string& comment = "", int flags = SKOLEM_DEFAULT);
-
- /** Create a instantiation constant with the given type. */
- Node mkInstConstant(const TypeNode& type);
-
- /** Make a new abstract value with the given type. */
- Node mkAbstractValue(const TypeNode& type);
-
- /**
- * Create a constant of type T. It will have the appropriate
- * CONST_* kind defined for T.
- */
- template <class T>
- Node mkConst(const T&);
-
- template <class T>
- TypeNode mkTypeConst(const T&);
-
- template <class NodeClass, class T>
- NodeClass mkConstInternal(const T&);
-
- /** Create a node with children. */
- TypeNode mkTypeNode(Kind kind, TypeNode child1);
- TypeNode mkTypeNode(Kind kind, TypeNode child1, TypeNode child2);
- TypeNode mkTypeNode(Kind kind, TypeNode child1, TypeNode child2,
- TypeNode child3);
- TypeNode mkTypeNode(Kind kind, const std::vector<TypeNode>& children);
-
- /**
- * Determine whether Nodes of a particular Kind have operators.
- * @returns true if Nodes of Kind k have operators.
- */
- static inline bool hasOperator(Kind k);
-
- /**
- * Get the (singleton) operator of an OPERATOR-kinded kind. The
- * returned node n will have kind BUILTIN, and calling
- * n.getConst<CVC4::Kind>() will yield k.
- */
- inline TNode operatorOf(Kind k) {
- AssertArgument( kind::metaKindOf(k) == kind::metakind::OPERATOR, k,
- "Kind is not an OPERATOR-kinded kind "
- "in NodeManager::operatorOf()" );
- return d_operators[k];
- }
-
- /**
- * Retrieve an attribute for a node.
- *
- * @param nv the node value
- * @param attr an instance of the attribute kind to retrieve.
- * @returns the attribute, if set, or a default-constructed
- * <code>AttrKind::value_type</code> if not.
- */
- template <class AttrKind>
- inline typename AttrKind::value_type getAttribute(expr::NodeValue* nv,
- const AttrKind& attr) const;
-
- /**
- * Check whether an attribute is set for a node.
- *
- * @param nv the node value
- * @param attr an instance of the attribute kind to check
- * @returns <code>true</code> iff <code>attr</code> is set for
- * <code>nv</code>.
- */
- template <class AttrKind>
- inline bool hasAttribute(expr::NodeValue* nv,
- const AttrKind& attr) const;
-
- /**
- * Check whether an attribute is set for a node, and, if so,
- * retrieve it.
- *
- * @param nv the node value
- * @param attr an instance of the attribute kind to check
- * @param value a reference to an object of the attribute's value type.
- * <code>value</code> will be set to the value of the attribute, if it is
- * set for <code>nv</code>; otherwise, it will be set to the default
- * value of the attribute.
- * @returns <code>true</code> iff <code>attr</code> is set for
- * <code>nv</code>.
- */
- template <class AttrKind>
- inline bool getAttribute(expr::NodeValue* nv,
- const AttrKind& attr,
- typename AttrKind::value_type& value) const;
-
- /**
- * Set an attribute for a node. If the node doesn't have the
- * attribute, this function assigns one. If the node has one, this
- * overwrites it.
- *
- * @param nv the node value
- * @param attr an instance of the attribute kind to set
- * @param value the value of <code>attr</code> for <code>nv</code>
- */
- template <class AttrKind>
- inline void setAttribute(expr::NodeValue* nv,
- const AttrKind& attr,
- const typename AttrKind::value_type& value);
-
- /**
- * Retrieve an attribute for a TNode.
- *
- * @param n the node
- * @param attr an instance of the attribute kind to retrieve.
- * @returns the attribute, if set, or a default-constructed
- * <code>AttrKind::value_type</code> if not.
- */
- template <class AttrKind>
- inline typename AttrKind::value_type
- getAttribute(TNode n, const AttrKind& attr) const;
-
- /**
- * Check whether an attribute is set for a TNode.
- *
- * @param n the node
- * @param attr an instance of the attribute kind to check
- * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
- */
- template <class AttrKind>
- inline bool hasAttribute(TNode n,
- const AttrKind& attr) const;
-
- /**
- * Check whether an attribute is set for a TNode and, if so, retieve
- * it.
- *
- * @param n the node
- * @param attr an instance of the attribute kind to check
- * @param value a reference to an object of the attribute's value type.
- * <code>value</code> will be set to the value of the attribute, if it is
- * set for <code>nv</code>; otherwise, it will be set to the default value of
- * the attribute.
- * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
- */
- template <class AttrKind>
- inline bool getAttribute(TNode n,
- const AttrKind& attr,
- typename AttrKind::value_type& value) const;
-
- /**
- * Set an attribute for a node. If the node doesn't have the
- * attribute, this function assigns one. If the node has one, this
- * overwrites it.
- *
- * @param n the node
- * @param attr an instance of the attribute kind to set
- * @param value the value of <code>attr</code> for <code>n</code>
- */
- template <class AttrKind>
- inline void setAttribute(TNode n,
- const AttrKind& attr,
- const typename AttrKind::value_type& value);
-
- /**
- * Retrieve an attribute for a TypeNode.
- *
- * @param n the type node
- * @param attr an instance of the attribute kind to retrieve.
- * @returns the attribute, if set, or a default-constructed
- * <code>AttrKind::value_type</code> if not.
- */
- template <class AttrKind>
- inline typename AttrKind::value_type
- getAttribute(TypeNode n, const AttrKind& attr) const;
-
- /**
- * Check whether an attribute is set for a TypeNode.
- *
- * @param n the type node
- * @param attr an instance of the attribute kind to check
- * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
- */
- template <class AttrKind>
- inline bool hasAttribute(TypeNode n,
- const AttrKind& attr) const;
-
- /**
- * Check whether an attribute is set for a TypeNode and, if so, retieve
- * it.
- *
- * @param n the type node
- * @param attr an instance of the attribute kind to check
- * @param value a reference to an object of the attribute's value type.
- * <code>value</code> will be set to the value of the attribute, if it is
- * set for <code>nv</code>; otherwise, it will be set to the default value of
- * the attribute.
- * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
- */
- template <class AttrKind>
- inline bool getAttribute(TypeNode n,
- const AttrKind& attr,
- typename AttrKind::value_type& value) const;
-
- /**
- * Set an attribute for a type node. If the node doesn't have the
- * attribute, this function assigns one. If the type node has one,
- * this overwrites it.
- *
- * @param n the type node
- * @param attr an instance of the attribute kind to set
- * @param value the value of <code>attr</code> for <code>n</code>
- */
- template <class AttrKind>
- inline void setAttribute(TypeNode n,
- const AttrKind& attr,
- const typename AttrKind::value_type& value);
-
- /** Get the (singleton) type for Booleans. */
- inline TypeNode booleanType();
-
- /** Get the (singleton) type for integers. */
- inline TypeNode integerType();
-
- /** Get the (singleton) type for reals. */
- inline TypeNode realType();
-
- /** Get the (singleton) type for strings. */
- inline TypeNode stringType();
-
- /** Get the (singleton) type for RegExp. */
- inline TypeNode regexpType();
-
- /** Get the bound var list type. */
- inline TypeNode boundVarListType();
-
- /** Get the instantiation pattern type. */
- inline TypeNode instPatternType();
-
- /** Get the instantiation pattern type. */
- inline TypeNode instPatternListType();
-
- /**
- * Get the (singleton) type for builtin operators (that is, the type
- * of the Node returned from Node::getOperator() when the operator
- * is built-in, like EQUAL). */
- inline TypeNode builtinOperatorType();
-
- /**
- * Make a function type from domain to range.
- *
- * @param domain the domain type
- * @param range the range type
- * @returns the functional type domain -> range
- */
- inline TypeNode mkFunctionType(const TypeNode& domain, const TypeNode& range);
-
- /**
- * Make a function type with input types from
- * argTypes. <code>argTypes</code> must have at least one element.
- *
- * @param argTypes the domain is a tuple (argTypes[0], ..., argTypes[n])
- * @param range the range type
- * @returns the functional type (argTypes[0], ..., argTypes[n]) -> range
- */
- inline TypeNode mkFunctionType(const std::vector<TypeNode>& argTypes,
- const TypeNode& range);
-
- /**
- * Make a function type with input types from
- * <code>sorts[0..sorts.size()-2]</code> and result type
- * <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have
- * at least 2 elements.
- */
- inline TypeNode mkFunctionType(const std::vector<TypeNode>& sorts);
-
- /**
- * Make a predicate type with input types from
- * <code>sorts</code>. The result with be a function type with range
- * <code>BOOLEAN</code>. <code>sorts</code> must have at least one
- * element.
- */
- inline TypeNode mkPredicateType(const std::vector<TypeNode>& sorts);
-
- /**
- * Make a tuple type with types from
- * <code>types</code>. <code>types</code> must have at least one
- * element.
- *
- * @param types a vector of types
- * @returns the tuple type (types[0], ..., types[n])
- */
- inline TypeNode mkTupleType(const std::vector<TypeNode>& types);
-
- /**
- * Make a record type with the description from rec.
- *
- * @param rec a description of the record
- * @returns the record type
- */
- inline TypeNode mkRecordType(const Record& rec);
-
- /**
- * Make a symbolic expression type with types from
- * <code>types</code>. <code>types</code> may have any number of
- * elements.
- *
- * @param types a vector of types
- * @returns the symbolic expression type (types[0], ..., types[n])
- */
- inline TypeNode mkSExprType(const std::vector<TypeNode>& types);
-
- /** Make the type of bitvectors of size <code>size</code> */
- inline TypeNode mkBitVectorType(unsigned size);
-
- /** Make the type of arrays with the given parameterization */
- inline TypeNode mkArrayType(TypeNode indexType, TypeNode constituentType);
-
- /** Make the type of arrays with the given parameterization */
- inline TypeNode mkSetType(TypeNode elementType);
-
- /** Make a type representing a constructor with the given parameterization */
- TypeNode mkConstructorType(const DatatypeConstructor& constructor, TypeNode range);
-
- /** Make a type representing a selector with the given parameterization */
- inline TypeNode mkSelectorType(TypeNode domain, TypeNode range);
-
- /** Make a type representing a tester with given parameterization */
- inline TypeNode mkTesterType(TypeNode domain);
-
- /** Make a new (anonymous) sort of arity 0. */
- TypeNode mkSort(uint32_t flags = ExprManager::SORT_FLAG_NONE);
-
- /** Make a new sort with the given name of arity 0. */
- TypeNode mkSort(const std::string& name, uint32_t flags = ExprManager::SORT_FLAG_NONE);
-
- /** Make a new sort by parameterizing the given sort constructor. */
- TypeNode mkSort(TypeNode constructor,
- const std::vector<TypeNode>& children,
- uint32_t flags = ExprManager::SORT_FLAG_NONE);
-
- /** Make a new sort with the given name and arity. */
- TypeNode mkSortConstructor(const std::string& name, size_t arity);
-
- /**
- * Make a predicate subtype type defined by the given LAMBDA
- * expression. A TypeCheckingExceptionPrivate can be thrown if
- * lambda is not a LAMBDA, or is ill-typed, or if CVC4 fails at
- * proving that the resulting predicate subtype is inhabited.
- */
- TypeNode mkPredicateSubtype(Expr lambda)
- throw(TypeCheckingExceptionPrivate);
-
- /**
- * Make a predicate subtype type defined by the given LAMBDA
- * expression and whose non-emptiness is witnessed by the given
- * witness. A TypeCheckingExceptionPrivate can be thrown if lambda
- * is not a LAMBDA, or is ill-typed, or if the witness is not a
- * witness or ill-typed.
- */
- TypeNode mkPredicateSubtype(Expr lambda, Expr witness)
- throw(TypeCheckingExceptionPrivate);
-
- /**
- * Make an integer subrange type as defined by the argument.
- */
- TypeNode mkSubrangeType(const SubrangeBounds& bounds)
- throw(TypeCheckingExceptionPrivate);
-
- /**
- * Given a tuple or record type, get the internal datatype used for
- * it. Makes the DatatypeType if necessary.
- */
- TypeNode getDatatypeForTupleRecord(TypeNode tupleRecordType);
-
- /**
- * Get the type for the given node and optionally do type checking.
- *
- * Initial type computation will be near-constant time if
- * type checking is not requested. Results are memoized, so that
- * subsequent calls to getType() without type checking will be
- * constant time.
- *
- * Initial type checking is linear in the size of the expression.
- * Again, the results are memoized, so that subsequent calls to
- * getType(), with or without type checking, will be constant
- * time.
- *
- * NOTE: A TypeCheckingException can be thrown even when type
- * checking is not requested. getType() will always return a
- * valid and correct type and, thus, an exception will be thrown
- * when no valid or correct type can be computed (e.g., if the
- * arguments to a bit-vector operation aren't bit-vectors). When
- * type checking is not requested, getType() will do the minimum
- * amount of checking required to return a valid result.
- *
- * @param n the Node for which we want a type
- * @param check whether we should check the type as we compute it
- * (default: false)
- */
- TypeNode getType(TNode n, bool check = false)
- throw(TypeCheckingExceptionPrivate, AssertionException);
-
- /**
- * Convert a node to an expression. Uses the ExprManager
- * associated to this NodeManager.
- */
- inline Expr toExpr(TNode n);
-
- /**
- * Convert an expression to a node.
- */
- static inline Node fromExpr(const Expr& e);
-
- /**
- * Convert a node manager to an expression manager.
- */
- inline ExprManager* toExprManager();
-
- /**
- * Convert an expression manager to a node manager.
- */
- static inline NodeManager* fromExprManager(ExprManager* exprManager);
-
- /**
- * Convert a type node to a type.
- */
- inline Type toType(TypeNode tn);
-
- /**
- * Convert a type to a type node.
- */
- static inline TypeNode fromType(Type t);
-
- /** Reclaim zombies while there are more than k nodes in the pool (if possible).*/
- void reclaimZombiesUntil(uint32_t k);
-
- /** Reclaims all zombies (if possible).*/
- void reclaimAllZombies();
-
- /** Size of the node pool. */
- size_t poolSize() const;
-
- /** Deletes a list of attributes from the NM's AttributeManager.*/
- void deleteAttributes(const std::vector< const expr::attr::AttributeUniqueId* >& ids);
-
- /**
- * This function gives developers a hook into the NodeManager.
- * This can be changed in node_manager.cpp without recompiling most of cvc4.
- *
- * debugHook is a debugging only function, and should not be present in
- * any published code!
- */
- void debugHook(int debugFlag);
-};/* class NodeManager */
-
-/**
- * This class changes the "current" thread-global
- * <code>NodeManager</code> when it is created and reinstates the
- * previous thread-global <code>NodeManager</code> when it is
- * destroyed, effectively maintaining a set of nested
- * <code>NodeManager</code> scopes. This is especially useful on
- * public-interface calls into the CVC4 library, where CVC4's notion
- * of the "current" <code>NodeManager</code> should be set to match
- * the calling context. See, for example, the implementations of
- * public calls in the <code>ExprManager</code> and
- * <code>SmtEngine</code> classes.
- *
- * The client must be careful to create and destroy
- * <code>NodeManagerScope</code> objects in a well-nested manner (such
- * as on the stack). You may create a <code>NodeManagerScope</code>
- * with <code>new</code> and destroy it with <code>delete</code>, or
- * place it as a data member of an object that is, but if the scope of
- * these <code>new</code>/<code>delete</code> pairs isn't properly
- * maintained, the incorrect "current" <code>NodeManager</code>
- * pointer may be restored after a delete.
- */
-class NodeManagerScope {
- /** The old NodeManager, to be restored on destruction. */
- NodeManager* d_oldNodeManager;
-
-public:
-
- NodeManagerScope(NodeManager* nm) :
- d_oldNodeManager(NodeManager::s_current) {
- // There are corner cases where nm can be NULL and it's ok.
- // For example, if you write { Expr e; }, then when the null
- // Expr is destructed, there's no active node manager.
- //Assert(nm != NULL);
- NodeManager::s_current = nm;
- Options::s_current = nm ? nm->d_options : NULL;
- Debug("current") << "node manager scope: "
- << NodeManager::s_current << "\n";
- }
-
- ~NodeManagerScope() {
- NodeManager::s_current = d_oldNodeManager;
- Options::s_current = d_oldNodeManager ? d_oldNodeManager->d_options : NULL;
- Debug("current") << "node manager scope: "
- << "returning to " << NodeManager::s_current << "\n";
- }
-};/* class NodeManagerScope */
-
-/** Get the (singleton) type for booleans. */
-inline TypeNode NodeManager::booleanType() {
- return TypeNode(mkTypeConst<TypeConstant>(BOOLEAN_TYPE));
-}
-
-/** Get the (singleton) type for integers. */
-inline TypeNode NodeManager::integerType() {
- return TypeNode(mkTypeConst<TypeConstant>(INTEGER_TYPE));
-}
-
-/** Get the (singleton) type for reals. */
-inline TypeNode NodeManager::realType() {
- return TypeNode(mkTypeConst<TypeConstant>(REAL_TYPE));
-}
-
-/** Get the (singleton) type for strings. */
-inline TypeNode NodeManager::stringType() {
- return TypeNode(mkTypeConst<TypeConstant>(STRING_TYPE));
-}
-
-/** Get the (singleton) type for regexps. */
-inline TypeNode NodeManager::regexpType() {
- return TypeNode(mkTypeConst<TypeConstant>(REGEXP_TYPE));
-}
-
-/** Get the bound var list type. */
-inline TypeNode NodeManager::boundVarListType() {
- return TypeNode(mkTypeConst<TypeConstant>(BOUND_VAR_LIST_TYPE));
-}
-
-/** Get the instantiation pattern type. */
-inline TypeNode NodeManager::instPatternType() {
- return TypeNode(mkTypeConst<TypeConstant>(INST_PATTERN_TYPE));
-}
-
-/** Get the instantiation pattern type. */
-inline TypeNode NodeManager::instPatternListType() {
- return TypeNode(mkTypeConst<TypeConstant>(INST_PATTERN_LIST_TYPE));
-}
-
-/** Get the (singleton) type for builtin operators. */
-inline TypeNode NodeManager::builtinOperatorType() {
- return TypeNode(mkTypeConst<TypeConstant>(BUILTIN_OPERATOR_TYPE));
-}
-
-/** Make a function type from domain to range. */
-inline TypeNode NodeManager::mkFunctionType(const TypeNode& domain, const TypeNode& range) {
- std::vector<TypeNode> sorts;
- sorts.push_back(domain);
- sorts.push_back(range);
- return mkFunctionType(sorts);
-}
-
-inline TypeNode NodeManager::mkFunctionType(const std::vector<TypeNode>& argTypes, const TypeNode& range) {
- Assert(argTypes.size() >= 1);
- std::vector<TypeNode> sorts(argTypes);
- sorts.push_back(range);
- return mkFunctionType(sorts);
-}
-
-inline TypeNode
-NodeManager::mkFunctionType(const std::vector<TypeNode>& sorts) {
- Assert(sorts.size() >= 2);
- std::vector<TypeNode> sortNodes;
- for (unsigned i = 0; i < sorts.size(); ++ i) {
- CheckArgument(!sorts[i].isFunctionLike(), sorts,
- "cannot create higher-order function types");
- sortNodes.push_back(sorts[i]);
- }
- return mkTypeNode(kind::FUNCTION_TYPE, sortNodes);
-}
-
-inline TypeNode
-NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts) {
- Assert(sorts.size() >= 1);
- std::vector<TypeNode> sortNodes;
- for (unsigned i = 0; i < sorts.size(); ++ i) {
- CheckArgument(!sorts[i].isFunctionLike(), sorts,
- "cannot create higher-order function types");
- sortNodes.push_back(sorts[i]);
- }
- sortNodes.push_back(booleanType());
- return mkTypeNode(kind::FUNCTION_TYPE, sortNodes);
-}
-
-inline TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) {
- std::vector<TypeNode> typeNodes;
- for (unsigned i = 0; i < types.size(); ++ i) {
- CheckArgument(!types[i].isFunctionLike(), types,
- "cannot put function-like types in tuples");
- typeNodes.push_back(types[i]);
- }
- return mkTypeNode(kind::TUPLE_TYPE, typeNodes);
-}
-
-inline TypeNode NodeManager::mkRecordType(const Record& rec) {
- return mkTypeConst(rec);
-}
-
-inline TypeNode NodeManager::mkSExprType(const std::vector<TypeNode>& types) {
- std::vector<TypeNode> typeNodes;
- for (unsigned i = 0; i < types.size(); ++ i) {
- typeNodes.push_back(types[i]);
- }
- return mkTypeNode(kind::SEXPR_TYPE, typeNodes);
-}
-
-inline TypeNode NodeManager::mkBitVectorType(unsigned size) {
- return TypeNode(mkTypeConst<BitVectorSize>(BitVectorSize(size)));
-}
-
-inline TypeNode NodeManager::mkArrayType(TypeNode indexType,
- TypeNode constituentType) {
- CheckArgument(!indexType.isNull(), indexType,
- "unexpected NULL index type");
- CheckArgument(!constituentType.isNull(), constituentType,
- "unexpected NULL constituent type");
- CheckArgument(!indexType.isFunctionLike(), indexType,
- "cannot index arrays by a function-like type");
- CheckArgument(!constituentType.isFunctionLike(), constituentType,
- "cannot store function-like types in arrays");
- Debug("arrays") << "making array type " << indexType << " " << constituentType << std::endl;
- return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType);
-}
-
-inline TypeNode NodeManager::mkSetType(TypeNode elementType) {
- CheckArgument(!elementType.isNull(), elementType,
- "unexpected NULL element type");
- // TODO: Confirm meaning of isFunctionLike(). --K
- CheckArgument(!elementType.isFunctionLike(), elementType,
- "cannot store function-like types in sets");
- Debug("sets") << "making sets type " << elementType << std::endl;
- return mkTypeNode(kind::SET_TYPE, elementType);
-}
-
-inline TypeNode NodeManager::mkSelectorType(TypeNode domain, TypeNode range) {
- CheckArgument(!domain.isFunctionLike(), domain,
- "cannot create higher-order function types");
- CheckArgument(!range.isFunctionLike(), range,
- "cannot create higher-order function types");
- return mkTypeNode(kind::SELECTOR_TYPE, domain, range);
-}
-
-inline TypeNode NodeManager::mkTesterType(TypeNode domain) {
- CheckArgument(!domain.isFunctionLike(), domain,
- "cannot create higher-order function types");
- return mkTypeNode(kind::TESTER_TYPE, domain );
-}
-
-inline expr::NodeValue* NodeManager::poolLookup(expr::NodeValue* nv) const {
- NodeValuePool::const_iterator find = d_nodeValuePool.find(nv);
- if(find == d_nodeValuePool.end()) {
- return NULL;
- } else {
- return *find;
- }
-}
-
-inline void NodeManager::poolInsert(expr::NodeValue* nv) {
- Assert(d_nodeValuePool.find(nv) == d_nodeValuePool.end(),
- "NodeValue already in the pool!");
- d_nodeValuePool.insert(nv);// FIXME multithreading
-}
-
-inline void NodeManager::poolRemove(expr::NodeValue* nv) {
- Assert(d_nodeValuePool.find(nv) != d_nodeValuePool.end(),
- "NodeValue is not in the pool!");
-
- d_nodeValuePool.erase(nv);// FIXME multithreading
-}
-
-inline Expr NodeManager::toExpr(TNode n) {
- return Expr(d_exprManager, new Node(n));
-}
-
-inline Node NodeManager::fromExpr(const Expr& e) {
- return e.getNode();
-}
-
-inline ExprManager* NodeManager::toExprManager() {
- return d_exprManager;
-}
-
-inline NodeManager* NodeManager::fromExprManager(ExprManager* exprManager) {
- return exprManager->getNodeManager();
-}
-
-inline Type NodeManager::toType(TypeNode tn) {
- return Type(this, new TypeNode(tn));
-}
-
-inline TypeNode NodeManager::fromType(Type t) {
- return *Type::getTypeNode(t);
-}
-
-}/* CVC4 namespace */
-
-#define __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
-#include "expr/metakind.h"
-#undef __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
-
-#include "expr/node_builder.h"
-
-namespace CVC4 {
-
-// general expression-builders
-
-inline bool NodeManager::hasOperator(Kind k) {
- switch(kind::MetaKind mk = kind::metaKindOf(k)) {
-
- case kind::metakind::INVALID:
- case kind::metakind::VARIABLE:
- return false;
-
- case kind::metakind::OPERATOR:
- case kind::metakind::PARAMETERIZED:
- return true;
-
- case kind::metakind::CONSTANT:
- return false;
-
- default:
- Unhandled(mk);
- }
-}
-
-inline Kind NodeManager::operatorToKind(TNode n) {
- return kind::operatorToKind(n.d_nv);
-}
-
-inline Node NodeManager::mkNode(Kind kind, TNode child1) {
- NodeBuilder<1> nb(this, kind);
- nb << child1;
- return nb.constructNode();
-}
-
-inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1) {
- NodeBuilder<1> nb(this, kind);
- nb << child1;
- return nb.constructNodePtr();
-}
-
-inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2) {
- NodeBuilder<2> nb(this, kind);
- nb << child1 << child2;
- return nb.constructNode();
-}
-
-inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2) {
- NodeBuilder<2> nb(this, kind);
- nb << child1 << child2;
- return nb.constructNodePtr();
-}
-
-inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
- TNode child3) {
- NodeBuilder<3> nb(this, kind);
- nb << child1 << child2 << child3;
- return nb.constructNode();
-}
-
-inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2,
- TNode child3) {
- NodeBuilder<3> nb(this, kind);
- nb << child1 << child2 << child3;
- return nb.constructNodePtr();
-}
-
-inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
- TNode child3, TNode child4) {
- NodeBuilder<4> nb(this, kind);
- nb << child1 << child2 << child3 << child4;
- return nb.constructNode();
-}
-
-inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2,
- TNode child3, TNode child4) {
- NodeBuilder<4> nb(this, kind);
- nb << child1 << child2 << child3 << child4;
- return nb.constructNodePtr();
-}
-
-inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
- TNode child3, TNode child4, TNode child5) {
- NodeBuilder<5> nb(this, kind);
- nb << child1 << child2 << child3 << child4 << child5;
- return nb.constructNode();
-}
-
-inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2,
- TNode child3, TNode child4, TNode child5) {
- NodeBuilder<5> nb(this, kind);
- nb << child1 << child2 << child3 << child4 << child5;
- return nb.constructNodePtr();
-}
-
-// N-ary version
-template <bool ref_count>
-inline Node NodeManager::mkNode(Kind kind,
- const std::vector<NodeTemplate<ref_count> >&
- children) {
- NodeBuilder<> nb(this, kind);
- nb.append(children);
- return nb.constructNode();
-}
-
-template <bool ref_count>
-inline Node* NodeManager::mkNodePtr(Kind kind,
- const std::vector<NodeTemplate<ref_count> >&
- children) {
- NodeBuilder<> nb(this, kind);
- nb.append(children);
- return nb.constructNodePtr();
-}
-
-// for operators
-inline Node NodeManager::mkNode(TNode opNode) {
- NodeBuilder<1> nb(this, operatorToKind(opNode));
- if(opNode.getKind() != kind::BUILTIN) {
- nb << opNode;
- }
- return nb.constructNode();
-}
-
-inline Node* NodeManager::mkNodePtr(TNode opNode) {
- NodeBuilder<1> nb(this, operatorToKind(opNode));
- if(opNode.getKind() != kind::BUILTIN) {
- nb << opNode;
- }
- return nb.constructNodePtr();
-}
-
-inline Node NodeManager::mkNode(TNode opNode, TNode child1) {
- NodeBuilder<2> nb(this, operatorToKind(opNode));
- if(opNode.getKind() != kind::BUILTIN) {
- nb << opNode;
- }
- nb << child1;
- return nb.constructNode();
-}
-
-inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1) {
- NodeBuilder<2> nb(this, operatorToKind(opNode));
- if(opNode.getKind() != kind::BUILTIN) {
- nb << opNode;
- }
- nb << child1;
- return nb.constructNodePtr();
-}
-
-inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2) {
- NodeBuilder<3> nb(this, operatorToKind(opNode));
- if(opNode.getKind() != kind::BUILTIN) {
- nb << opNode;
- }
- nb << child1 << child2;
- return nb.constructNode();
-}
-
-inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2) {
- NodeBuilder<3> nb(this, operatorToKind(opNode));
- if(opNode.getKind() != kind::BUILTIN) {
- nb << opNode;
- }
- nb << child1 << child2;
- return nb.constructNodePtr();
-}
-
-inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
- TNode child3) {
- NodeBuilder<4> nb(this, operatorToKind(opNode));
- if(opNode.getKind() != kind::BUILTIN) {
- nb << opNode;
- }
- nb << child1 << child2 << child3;
- return nb.constructNode();
-}
-
-inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
- TNode child3) {
- NodeBuilder<4> nb(this, operatorToKind(opNode));
- if(opNode.getKind() != kind::BUILTIN) {
- nb << opNode;
- }
- nb << child1 << child2 << child3;
- return nb.constructNodePtr();
-}
-
-inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
- TNode child3, TNode child4) {
- NodeBuilder<5> nb(this, operatorToKind(opNode));
- if(opNode.getKind() != kind::BUILTIN) {
- nb << opNode;
- }
- nb << child1 << child2 << child3 << child4;
- return nb.constructNode();
-}
-
-inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
- TNode child3, TNode child4) {
- NodeBuilder<5> nb(this, operatorToKind(opNode));
- if(opNode.getKind() != kind::BUILTIN) {
- nb << opNode;
- }
- nb << child1 << child2 << child3 << child4;
- return nb.constructNodePtr();
-}
-
-inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
- TNode child3, TNode child4, TNode child5) {
- NodeBuilder<6> nb(this, operatorToKind(opNode));
- if(opNode.getKind() != kind::BUILTIN) {
- nb << opNode;
- }
- nb << child1 << child2 << child3 << child4 << child5;
- return nb.constructNode();
-}
-
-inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
- TNode child3, TNode child4, TNode child5) {
- NodeBuilder<6> nb(this, operatorToKind(opNode));
- if(opNode.getKind() != kind::BUILTIN) {
- nb << opNode;
- }
- nb << child1 << child2 << child3 << child4 << child5;
- return nb.constructNodePtr();
-}
-
-// N-ary version for operators
-template <bool ref_count>
-inline Node NodeManager::mkNode(TNode opNode,
- const std::vector<NodeTemplate<ref_count> >&
- children) {
- NodeBuilder<> nb(this, operatorToKind(opNode));
- if(opNode.getKind() != kind::BUILTIN) {
- nb << opNode;
- }
- nb.append(children);
- return nb.constructNode();
-}
-
-template <bool ref_count>
-inline Node* NodeManager::mkNodePtr(TNode opNode,
- const std::vector<NodeTemplate<ref_count> >&
- children) {
- NodeBuilder<> nb(this, operatorToKind(opNode));
- if(opNode.getKind() != kind::BUILTIN) {
- nb << opNode;
- }
- nb.append(children);
- return nb.constructNodePtr();
-}
-
-
-inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1) {
- return (NodeBuilder<1>(this, kind) << child1).constructTypeNode();
-}
-
-inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1,
- TypeNode child2) {
- return (NodeBuilder<2>(this, kind) << child1 << child2).constructTypeNode();
-}
-
-inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1,
- TypeNode child2, TypeNode child3) {
- return (NodeBuilder<3>(this, kind) << child1 << child2 << child3).constructTypeNode();
-}
-
-// N-ary version for types
-inline TypeNode NodeManager::mkTypeNode(Kind kind,
- const std::vector<TypeNode>& children) {
- return NodeBuilder<>(this, kind).append(children).constructTypeNode();
-}
-
-template <class T>
-Node NodeManager::mkConst(const T& val) {
- return mkConstInternal<Node, T>(val);
-}
-
-template <class T>
-TypeNode NodeManager::mkTypeConst(const T& val) {
- return mkConstInternal<TypeNode, T>(val);
-}
-
-template <class NodeClass, class T>
-NodeClass NodeManager::mkConstInternal(const T& val) {
-
- // typedef typename kind::metakind::constantMap<T>::OwningTheory theory_t;
- NVStorage<1> nvStorage;
- expr::NodeValue& nvStack = reinterpret_cast<expr::NodeValue&>(nvStorage);
-
- nvStack.d_id = 0;
- nvStack.d_kind = kind::metakind::ConstantMap<T>::kind;
- nvStack.d_rc = 0;
- nvStack.d_nchildren = 1;
-
-#if defined(__GNUC__) && (__GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ >= 6))
-#pragma GCC diagnostic push
-#pragma GCC diagnostic ignored "-Warray-bounds"
-#endif
-
- nvStack.d_children[0] =
- const_cast<expr::NodeValue*>(reinterpret_cast<const expr::NodeValue*>(&val));
- expr::NodeValue* nv = poolLookup(&nvStack);
-
-#if defined(__GNUC__) && (__GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ >= 6))
-#pragma GCC diagnostic pop
-#endif
-
- if(nv != NULL) {
- return NodeClass(nv);
- }
-
- nv = (expr::NodeValue*)
- std::malloc(sizeof(expr::NodeValue) + sizeof(T));
- if(nv == NULL) {
- throw std::bad_alloc();
- }
-
- nv->d_nchildren = 0;
- nv->d_kind = kind::metakind::ConstantMap<T>::kind;
- nv->d_id = next_id++;// FIXME multithreading
- nv->d_rc = 0;
-
- //OwningTheory::mkConst(val);
- new (&nv->d_children) T(val);
-
- poolInsert(nv);
- if(Debug.isOn("gc")) {
- Debug("gc") << "creating node value " << nv
- << " [" << nv->d_id << "]: ";
- nv->printAst(Debug("gc"));
- Debug("gc") << std::endl;
- }
-
- return NodeClass(nv);
-}
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__NODE_MANAGER_H */
projects / cvc5.git / commitdiff