From cf6bc6c57dd579b8f75b7d20922eda0eaa92b2f7 Mon Sep 17 00:00:00 2001 From: Martin Brain Date: Wed, 3 Dec 2014 21:29:43 -0500 Subject: Floating point infrastructure. Signed-off-by: Morgan Deters --- src/expr/expr_manager_template.cpp | 11 + src/expr/expr_manager_template.cpp.orig | 1027 +++++++++++++++++++++ src/expr/expr_manager_template.h | 6 + src/expr/expr_manager_template.h.orig | 572 ++++++++++++ src/expr/node_manager.h | 21 + src/expr/node_manager.h.orig | 1498 +++++++++++++++++++++++++++++++ src/expr/type.cpp | 30 + src/expr/type.h | 51 ++ src/expr/type_node.h | 49 + 9 files changed, 3265 insertions(+) create mode 100644 src/expr/expr_manager_template.cpp.orig create mode 100644 src/expr/expr_manager_template.h.orig create mode 100644 src/expr/node_manager.h.orig (limited to 'src/expr') diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index c5249075b..7eb93b8ff 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -154,6 +154,12 @@ IntegerType ExprManager::integerType() const { return IntegerType(Type(d_nodeManager, new TypeNode(d_nodeManager->integerType()))); } +RoundingModeType ExprManager::roundingModeType() const { + NodeManagerScope nms(d_nodeManager); + return RoundingModeType(Type(d_nodeManager, new TypeNode(d_nodeManager->roundingModeType()))); +} + + Expr ExprManager::mkExpr(Kind kind, Expr child1) { const kind::MetaKind mk = kind::metaKindOf(kind); const unsigned n = 1 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0); @@ -573,6 +579,11 @@ SExprType ExprManager::mkSExprType(const std::vector& types) { return SExprType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSExprType(typeNodes)))); } +FloatingPointType ExprManager::mkFloatingPointType(unsigned exp, unsigned sig) const { + NodeManagerScope nms(d_nodeManager); + return FloatingPointType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkFloatingPointType(exp,sig)))); +} + BitVectorType ExprManager::mkBitVectorType(unsigned size) const { NodeManagerScope nms(d_nodeManager); return BitVectorType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkBitVectorType(size)))); diff --git a/src/expr/expr_manager_template.cpp.orig b/src/expr/expr_manager_template.cpp.orig new file mode 100644 index 000000000..c5249075b --- /dev/null +++ b/src/expr/expr_manager_template.cpp.orig @@ -0,0 +1,1027 @@ +/********************* */ +/*! \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 b/src/expr/expr_manager_template.h index 2fabea0ff..8acb7489f 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -139,6 +139,9 @@ public: /** Get the type for integers */ IntegerType integerType() const; + /** Get the type for rounding modes */ + RoundingModeType roundingModeType() const; + /** * Make a unary expression of a given kind (NOT, BVNOT, ...). * @param kind the kind of expression @@ -361,6 +364,9 @@ public: */ SExprType mkSExprType(const std::vector& types); + /** Make a type representing a floating-point type with the given parameters. */ + FloatingPointType mkFloatingPointType(unsigned exp, unsigned sig) const; + /** Make a type representing a bit-vector of the given size. */ BitVectorType mkBitVectorType(unsigned size) const; diff --git a/src/expr/expr_manager_template.h.orig b/src/expr/expr_manager_template.h.orig new file mode 100644 index 000000000..2fabea0ff --- /dev/null +++ b/src/expr/expr_manager_template.h.orig @@ -0,0 +1,572 @@ +/********************* */ +/*! \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 b/src/expr/node_manager.h index f4c3a1999..f52c7732f 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -685,6 +685,9 @@ public: /** Get the (singleton) type for RegExp. */ inline TypeNode regexpType(); + /** Get the (singleton) type for rounding modes. */ + inline TypeNode roundingModeType(); + /** Get the bound var list type. */ inline TypeNode boundVarListType(); @@ -764,6 +767,11 @@ public: */ inline TypeNode mkSExprType(const std::vector& types); + /** Make the type of floating-point with exp bit exponent and + sig bit significand */ + inline TypeNode mkFloatingPointType(unsigned exp, unsigned sig); + inline TypeNode mkFloatingPointType(FloatingPointSize fs); + /** Make the type of bitvectors of size size */ inline TypeNode mkBitVectorType(unsigned size); @@ -980,6 +988,11 @@ inline TypeNode NodeManager::regexpType() { return TypeNode(mkTypeConst(REGEXP_TYPE)); } +/** Get the (singleton) type for rounding modes. */ +inline TypeNode NodeManager::roundingModeType() { + return TypeNode(mkTypeConst(ROUNDINGMODE_TYPE)); +} + /** Get the bound var list type. */ inline TypeNode NodeManager::boundVarListType() { return TypeNode(mkTypeConst(BOUND_VAR_LIST_TYPE)); @@ -1066,6 +1079,14 @@ inline TypeNode NodeManager::mkBitVectorType(unsigned size) { return TypeNode(mkTypeConst(BitVectorSize(size))); } +inline TypeNode NodeManager::mkFloatingPointType(unsigned exp, unsigned sig) { + return TypeNode(mkTypeConst(FloatingPointSize(exp,sig))); +} + +inline TypeNode NodeManager::mkFloatingPointType(FloatingPointSize fs) { + return TypeNode(mkTypeConst(fs)); +} + inline TypeNode NodeManager::mkArrayType(TypeNode indexType, TypeNode constituentType) { CheckArgument(!indexType.isNull(), indexType, diff --git a/src/expr/node_manager.h.orig b/src/expr/node_manager.h.orig new file mode 100644 index 000000000..f4c3a1999 --- /dev/null +++ b/src/expr/node_manager.h.orig @@ -0,0 +1,1498 @@ +/********************* */ +/*! \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 */ diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 5810e1f4f..46705a849 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -223,12 +223,24 @@ bool Type::isString() const { return d_typeNode->isString(); } +/** Is this the rounding mode type? */ +bool Type::isRoundingMode() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->isRoundingMode(); +} + /** Is this the bit-vector type? */ bool Type::isBitVector() const { NodeManagerScope nms(d_nodeManager); return d_typeNode->isBitVector(); } +/** Is this the floating-point type? */ +bool Type::isFloatingPoint() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->isFloatingPoint(); +} + /** Is this a datatype type? */ bool Type::isDatatype() const { NodeManagerScope nms(d_nodeManager); @@ -436,11 +448,21 @@ StringType::StringType(const Type& t) throw(IllegalArgumentException) : CheckArgument(isNull() || isString(), this); } +RoundingModeType::RoundingModeType(const Type& t) throw(IllegalArgumentException) : + Type(t) { + CheckArgument(isNull() || isRoundingMode(), this); +} + BitVectorType::BitVectorType(const Type& t) throw(IllegalArgumentException) : Type(t) { CheckArgument(isNull() || isBitVector(), this); } +FloatingPointType::FloatingPointType(const Type& t) throw(IllegalArgumentException) : + Type(t) { + CheckArgument(isNull() || isFloatingPoint(), this); +} + DatatypeType::DatatypeType(const Type& t) throw(IllegalArgumentException) : Type(t) { CheckArgument(isNull() || isDatatype(), this); @@ -520,6 +542,14 @@ unsigned BitVectorType::getSize() const { return d_typeNode->getBitVectorSize(); } +unsigned FloatingPointType::getExponentSize() const { + return d_typeNode->getFloatingPointExponentSize(); +} + +unsigned FloatingPointType::getSignificandSize() const { + return d_typeNode->getFloatingPointSignificandSize(); +} + Type ArrayType::getIndexType() const { return makeType(d_typeNode->getArrayIndexType()); } diff --git a/src/expr/type.h b/src/expr/type.h index 7674ff9d0..8a5a987d5 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -47,6 +47,7 @@ class BooleanType; class IntegerType; class RealType; class StringType; +class RoundingModeType; class BitVectorType; class ArrayType; class SetType; @@ -258,12 +259,24 @@ public: */ bool isString() const; + /** + * Is this the rounding mode type? + * @return true if the type is the rounding mode type + */ + bool isRoundingMode() const; + /** * Is this the bit-vector type? * @return true if the type is a bit-vector type */ bool isBitVector() const; + /** + * Is this the floating-point type? + * @return true if the type is a floating-point type + */ + bool isFloatingPoint() const; + /** * Is this a function type? * @return true if the type is a function type @@ -412,6 +425,19 @@ public: StringType(const Type& type) throw(IllegalArgumentException); };/* class StringType */ +/** + * Singleton class encapsulating the rounding mode type. + */ +class CVC4_PUBLIC RoundingModeType : public Type { + +public: + + /** Construct from the base type */ + RoundingModeType(const Type& type = Type()) throw(IllegalArgumentException); +};/* class RoundingModeType */ + + + /** * Class encapsulating a function type. */ @@ -609,6 +635,31 @@ public: };/* class BitVectorType */ +/** + * Class encapsulating the floating point type. + */ +class CVC4_PUBLIC FloatingPointType : public Type { + +public: + + /** Construct from the base type */ + FloatingPointType(const Type& type = Type()) throw(IllegalArgumentException); + + /** + * Returns the size of the floating-point exponent type. + * @return the width of the floating-point exponent type (> 0) + */ + unsigned getExponentSize() const; + + /** + * Returns the size of the floating-point significand type. + * @return the width of the floating-point significand type (> 0) + */ + unsigned getSignificandSize() const; + +};/* class FloatingPointType */ + + /** * Class encapsulating the datatype type */ diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 289395a34..5129b7581 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -463,6 +463,9 @@ public: /** Is this the String type? */ bool isString() const; + /** Is this the Rounding Mode type? */ + bool isRoundingMode() const; + /** Is this an array type? */ bool isArray() const; @@ -560,6 +563,13 @@ public: /** Is this a regexp type */ bool isRegExp() const; + /** Is this a floating-point type */ + bool isFloatingPoint() const; + + /** Is this a floating-point type of with exp exponent bits + and sig significand bits */ + bool isFloatingPoint(unsigned exp, unsigned sig) const; + /** Is this a bit-vector type */ bool isBitVector() const; @@ -590,6 +600,12 @@ public: /** Get the Datatype specification from a datatype type */ const Datatype& getDatatype() const; + /** Get the exponent size of this floating-point type */ + unsigned getFloatingPointExponentSize() const; + + /** Get the significand size of this floating-point type */ + unsigned getFloatingPointSignificandSize() const; + /** Get the size of this bit-vector type */ unsigned getBitVectorSize() const; @@ -852,6 +868,11 @@ inline bool TypeNode::isString() const { inline bool TypeNode::isRegExp() const { return getKind() == kind::TYPE_CONSTANT && getConst() == REGEXP_TYPE; + } + +inline bool TypeNode::isRoundingMode() const { + return getKind() == kind::TYPE_CONSTANT && + getConst() == ROUNDINGMODE_TYPE; } inline bool TypeNode::isArray() const { @@ -939,6 +960,12 @@ inline bool TypeNode::isSubrange() const { ( isPredicateSubtype() && getSubtypeParentType().isSubrange() ); } +/** Is this a floating-point type */ +inline bool TypeNode::isFloatingPoint() const { + return getKind() == kind::FLOATINGPOINT_TYPE || + ( isPredicateSubtype() && getSubtypeParentType().isFloatingPoint() ); +} + /** Is this a bit-vector type */ inline bool TypeNode::isBitVector() const { return getKind() == kind::BITVECTOR_TYPE || @@ -973,6 +1000,16 @@ inline bool TypeNode::isTester() const { return getKind() == kind::TESTER_TYPE; } +/** Is this a floating-point type of with exp exponent bits + and sig significand bits */ +inline bool TypeNode::isFloatingPoint(unsigned exp, unsigned sig) const { + return + ( getKind() == kind::FLOATINGPOINT_TYPE && + getConst().exponent() == exp && + getConst().significand() == sig ) || + ( isPredicateSubtype() && getSubtypeParentType().isFloatingPoint(exp,sig) ); +} + /** Is this a bit-vector type of size size */ inline bool TypeNode::isBitVector(unsigned size) const { return @@ -990,6 +1027,18 @@ inline const Datatype& TypeNode::getDatatype() const { } } +/** Get the exponent size of this floating-point type */ +inline unsigned TypeNode::getFloatingPointExponentSize() const { + Assert(isFloatingPoint()); + return getConst().exponent(); +} + +/** Get the significand size of this floating-point type */ +inline unsigned TypeNode::getFloatingPointSignificandSize() const { + Assert(isFloatingPoint()); + return getConst().significand(); +} + /** Get the size of this bit-vector type */ inline unsigned TypeNode::getBitVectorSize() const { Assert(isBitVector()); -- cgit v1.2.3