From: Morgan Deters Date: Tue, 13 Jan 2015 00:10:03 +0000 (-0500) Subject: Remove old .orig files that were added to the repository. X-Git-Tag: cvc5-1.0.0~6447 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9921d8baa2ec51a4bac8a8c87c5cad7b1abb140e;p=cvc5.git Remove old .orig files that were added to the repository. --- diff --git a/src/expr/expr_manager_template.cpp.orig b/src/expr/expr_manager_template.cpp.orig deleted file mode 100644 index c5249075b..000000000 --- a/src/expr/expr_manager_template.cpp.orig +++ /dev/null @@ -1,1027 +0,0 @@ -/********************* */ -/*! \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 - -${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() : 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& 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 nodes; - vector::const_iterator it = children.begin(); - vector::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& 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 nodes; - nodes.push_back(child1.getNode()); - - vector::const_iterator it = otherChildren.begin(); - vector::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& 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 nodes; - vector::const_iterator it = children.begin(); - vector::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& argTypes, Type range) { - NodeManagerScope nms(d_nodeManager); - Assert( argTypes.size() >= 1 ); - std::vector 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& sorts) { - NodeManagerScope nms(d_nodeManager); - Assert( sorts.size() >= 2 ); - std::vector 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& sorts) { - NodeManagerScope nms(d_nodeManager); - Assert( sorts.size() >= 1 ); - std::vector 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& types) { - NodeManagerScope nms(d_nodeManager); - std::vector 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& types) { - NodeManagerScope nms(d_nodeManager); - std::vector 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 datatypes; - datatypes.push_back(datatype); - vector result = mkMutualDatatypeTypes(datatypes); - Assert(result.size() == 1); - return result.front(); -} - -std::vector -ExprManager::mkMutualDatatypeTypes(const std::vector& datatypes) { - return mkMutualDatatypeTypes(datatypes, set()); -} - -std::vector -ExprManager::mkMutualDatatypeTypes(const std::vector& datatypes, - const std::set& unresolvedTypes) { - NodeManagerScope nms(d_nodeManager); - std::map nameResolutions; - std::vector 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::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 placeholders;// to hold the "unresolved placeholders" - std::vector replacements;// to hold our final, resolved types - for(std::set::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::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::iterator i = dtts.begin(), - i_end = dtts.end(); - i != i_end; - ++i) { - const Datatype& dt = (*i).getDatatype(); - if(!dt.isResolved()) { - const_cast(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::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& 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::const_iterator it = children.begin() ; - std::vector::const_iterator end = children.end() ; - - /* The new top-level children and the children of each sub node */ - std::vector newChildren; - std::vector subChildren; - - while( it != end && numChildren > max ) { - /* Grab the next max children and make a node for them. */ - for( std::vector::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()); - } else if(n.getKind() == kind::BITVECTOR_TYPE) { - return to->mkBitVectorType(n.getConst()); - } 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 */ diff --git a/src/expr/expr_manager_template.h.orig b/src/expr/expr_manager_template.h.orig deleted file mode 100644 index 2fabea0ff..000000000 --- a/src/expr/expr_manager_template.h.orig +++ /dev/null @@ -1,572 +0,0 @@ -/********************* */ -/*! \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 - -#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& 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& 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& children); - - /** Create a constant of type T */ - template - Expr mkConst(const T&); - - /** - * Create an Expr by applying an associative operator to the children. - * If children.size() is greater than the max arity for - * kind, then the expression will be broken up into - * suitably-sized chunks, taking advantage of the associativity of - * kind. For example, if kind FOO has max arity - * 2, then calling mkAssociative(FOO,a,b,c) will return - * (FOO (FOO a b) c) or (FOO a (FOO b c)). - * 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& 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() 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. - * argTypes must have at least one element. - */ - FunctionType mkFunctionType(const std::vector& argTypes, Type range); - - /** - * Make a function type with input types from - * sorts[0..sorts.size()-2] and result type - * sorts[sorts.size()-1]. sorts must have - * at least 2 elements. - */ - FunctionType mkFunctionType(const std::vector& sorts); - - /** - * Make a predicate type with input types from - * sorts. The result with be a function type with range - * BOOLEAN. sorts must have at least one - * element. - */ - FunctionType mkPredicateType(const std::vector& sorts); - - /** - * Make a tuple type with types from - * types[0..types.size()-1]. types must - * have at least one element. - */ - TupleType mkTupleType(const std::vector& types); - - /** - * Make a record type with types from the rec parameter. - */ - RecordType mkRecordType(const Record& rec); - - /** - * Make a symbolic expressiontype with types from - * types[0..types.size()-1]. types may - * have any number of elements. - */ - SExprType mkSExprType(const std::vector& 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 - mkMutualDatatypeTypes(const std::vector& 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 - mkMutualDatatypeTypes(const std::vector& datatypes, - const std::set& 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 */ diff --git a/src/expr/node_manager.h.orig b/src/expr/node_manager.h.orig deleted file mode 100644 index f4c3a1999..000000000 --- a/src/expr/node_manager.h.orig +++ /dev/null @@ -1,1498 +0,0 @@ -/********************* */ -/*! \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 -#include -#include - -#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& 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 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 ExprManager::mkMutualDatatypeTypes(const std::vector&, const std::set&); - - /** Predicate for use with STL algorithms */ - struct NodeValueReferenceCountNonZero { - bool operator()(expr::NodeValue* nv) { return nv->d_rc > 0; } - }; - - typedef __gnu_cxx::hash_set NodeValuePool; - typedef __gnu_cxx::hash_set 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(), you get kind::PLUS back. - */ - Node d_operators[kind::LAST_KIND]; - - /** - * A list of subscribers for NodeManager events. - */ - std::vector d_listeners; - - /** - * A map of tuple and record types to their corresponding datatype. - */ - std::hash_map 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(nvStorage); - * - * ...and then you can use nvStack as a NodeValue that you know has - * room for 4 children. - */ - template - struct NVStorage { - expr::NodeValue nv; - expr::NodeValue* child[N]; - };/* struct NodeManager::NVStorage */ - - /* 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::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 - Node mkNode(Kind kind, const std::vector >& children); - template - Node* mkNodePtr(Kind kind, const std::vector >& 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 - Node mkNode(TNode opNode, const std::vector >& children); - template - Node* mkNodePtr(TNode opNode, const std::vector >& 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 - Node mkConst(const T&); - - template - TypeNode mkTypeConst(const T&); - - template - 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& 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() 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 - * AttrKind::value_type if not. - */ - template - 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 true iff attr is set for - * nv. - */ - template - 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. - * value will be set to the value of the attribute, if it is - * set for nv; otherwise, it will be set to the default - * value of the attribute. - * @returns true iff attr is set for - * nv. - */ - template - 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 attr for nv - */ - template - 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 - * AttrKind::value_type if not. - */ - template - 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 true iff attr is set for n. - */ - template - 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. - * value will be set to the value of the attribute, if it is - * set for nv; otherwise, it will be set to the default value of - * the attribute. - * @returns true iff attr is set for n. - */ - template - 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 attr for n - */ - template - 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 - * AttrKind::value_type if not. - */ - template - 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 true iff attr is set for n. - */ - template - 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. - * value will be set to the value of the attribute, if it is - * set for nv; otherwise, it will be set to the default value of - * the attribute. - * @returns true iff attr is set for n. - */ - template - 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 attr for n - */ - template - 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. argTypes 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& argTypes, - const TypeNode& range); - - /** - * Make a function type with input types from - * sorts[0..sorts.size()-2] and result type - * sorts[sorts.size()-1]. sorts must have - * at least 2 elements. - */ - inline TypeNode mkFunctionType(const std::vector& sorts); - - /** - * Make a predicate type with input types from - * sorts. The result with be a function type with range - * BOOLEAN. sorts must have at least one - * element. - */ - inline TypeNode mkPredicateType(const std::vector& sorts); - - /** - * Make a tuple type with types from - * types. types 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& 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 - * types. types 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& types); - - /** Make the type of bitvectors of size size */ - 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& 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 - * NodeManager when it is created and reinstates the - * previous thread-global NodeManager when it is - * destroyed, effectively maintaining a set of nested - * NodeManager scopes. This is especially useful on - * public-interface calls into the CVC4 library, where CVC4's notion - * of the "current" NodeManager should be set to match - * the calling context. See, for example, the implementations of - * public calls in the ExprManager and - * SmtEngine classes. - * - * The client must be careful to create and destroy - * NodeManagerScope objects in a well-nested manner (such - * as on the stack). You may create a NodeManagerScope - * with new and destroy it with delete, or - * place it as a data member of an object that is, but if the scope of - * these new/delete pairs isn't properly - * maintained, the incorrect "current" NodeManager - * 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(BOOLEAN_TYPE)); -} - -/** Get the (singleton) type for integers. */ -inline TypeNode NodeManager::integerType() { - return TypeNode(mkTypeConst(INTEGER_TYPE)); -} - -/** Get the (singleton) type for reals. */ -inline TypeNode NodeManager::realType() { - return TypeNode(mkTypeConst(REAL_TYPE)); -} - -/** Get the (singleton) type for strings. */ -inline TypeNode NodeManager::stringType() { - return TypeNode(mkTypeConst(STRING_TYPE)); -} - -/** Get the (singleton) type for regexps. */ -inline TypeNode NodeManager::regexpType() { - return TypeNode(mkTypeConst(REGEXP_TYPE)); -} - -/** Get the bound var list type. */ -inline TypeNode NodeManager::boundVarListType() { - return TypeNode(mkTypeConst(BOUND_VAR_LIST_TYPE)); -} - -/** Get the instantiation pattern type. */ -inline TypeNode NodeManager::instPatternType() { - return TypeNode(mkTypeConst(INST_PATTERN_TYPE)); -} - -/** Get the instantiation pattern type. */ -inline TypeNode NodeManager::instPatternListType() { - return TypeNode(mkTypeConst(INST_PATTERN_LIST_TYPE)); -} - -/** Get the (singleton) type for builtin operators. */ -inline TypeNode NodeManager::builtinOperatorType() { - return TypeNode(mkTypeConst(BUILTIN_OPERATOR_TYPE)); -} - -/** Make a function type from domain to range. */ -inline TypeNode NodeManager::mkFunctionType(const TypeNode& domain, const TypeNode& range) { - std::vector sorts; - sorts.push_back(domain); - sorts.push_back(range); - return mkFunctionType(sorts); -} - -inline TypeNode NodeManager::mkFunctionType(const std::vector& argTypes, const TypeNode& range) { - Assert(argTypes.size() >= 1); - std::vector sorts(argTypes); - sorts.push_back(range); - return mkFunctionType(sorts); -} - -inline TypeNode -NodeManager::mkFunctionType(const std::vector& sorts) { - Assert(sorts.size() >= 2); - std::vector 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& sorts) { - Assert(sorts.size() >= 1); - std::vector 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& types) { - std::vector 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& types) { - std::vector 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(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 -inline Node NodeManager::mkNode(Kind kind, - const std::vector >& - children) { - NodeBuilder<> nb(this, kind); - nb.append(children); - return nb.constructNode(); -} - -template -inline Node* NodeManager::mkNodePtr(Kind kind, - const std::vector >& - 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 -inline Node NodeManager::mkNode(TNode opNode, - const std::vector >& - children) { - NodeBuilder<> nb(this, operatorToKind(opNode)); - if(opNode.getKind() != kind::BUILTIN) { - nb << opNode; - } - nb.append(children); - return nb.constructNode(); -} - -template -inline Node* NodeManager::mkNodePtr(TNode opNode, - const std::vector >& - 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& children) { - return NodeBuilder<>(this, kind).append(children).constructTypeNode(); -} - -template -Node NodeManager::mkConst(const T& val) { - return mkConstInternal(val); -} - -template -TypeNode NodeManager::mkTypeConst(const T& val) { - return mkConstInternal(val); -} - -template -NodeClass NodeManager::mkConstInternal(const T& val) { - - // typedef typename kind::metakind::constantMap::OwningTheory theory_t; - NVStorage<1> nvStorage; - expr::NodeValue& nvStack = reinterpret_cast(nvStorage); - - nvStack.d_id = 0; - nvStack.d_kind = kind::metakind::ConstantMap::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(reinterpret_cast(&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::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 */