AM_CXXFLAGS = -Wall -Wno-unknown-pragmas -Wno-parentheses $(FLAG_VISIBILITY_HIDDEN)
SUBDIRS = lib options expr util prop/minisat prop/bvminisat . parser compat bindings main
-THEORIES = builtin booleans uf arith bv arrays datatypes sets strings quantifiers idl
+THEORIES = builtin booleans uf arith bv fp arrays datatypes sets strings quantifiers idl
lib_LTLIBRARIES = libcvc4.la
theory/booleans/circuit_propagator.cpp \
theory/booleans/boolean_term_conversion_mode.h \
theory/booleans/boolean_term_conversion_mode.cpp \
- theory/booleans/options_handlers.h
+ theory/booleans/options_handlers.h \
+ theory/fp/theory_fp.h \
+ theory/fp/theory_fp.cpp \
+ theory/fp/theory_fp_rewriter.h \
+ theory/fp/theory_fp_rewriter.cpp \
+ theory/fp/theory_fp_type_rules.h
nodist_libcvc4_la_SOURCES = \
smt/smt_options.cpp \
theory/example/ecdata.h \
theory/example/ecdata.cpp \
theory/example/theory_uf_tim.h \
- theory/example/theory_uf_tim.cpp
+ theory/example/theory_uf_tim.cpp \
+ theory/fp/kinds \
+ theory/fp/options_handlers.h
svn_versioninfo.cpp: svninfo
$(AM_V_GEN)( \
%include "util/unsafe_interrupt_exception.i"
%include "util/integer.i"
%include "util/rational.i"
+//%include "util/floatingpoint.i"
%include "util/language.i"
%include "util/cardinality.i"
%include "util/bool.i"
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);
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))));
--- /dev/null
+/********************* */
+/*! \file expr_manager_template.cpp
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: Dejan Jovanovic, Christopher L. Conway
+ ** Minor contributors (to current version): Kshitij Bansal, Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Public-facing expression manager interface, implementation
+ **
+ ** Public-facing expression manager interface, implementation.
+ **/
+
+#include "expr/node_manager.h"
+#include "expr/expr_manager.h"
+#include "expr/variable_type_map.h"
+#include "options/options.h"
+#include "util/statistics_registry.h"
+
+#include <map>
+
+${includes}
+
+// This is a hack, but an important one: if there's an error, the
+// compiler directs the user to the template file instead of the
+// generated one. We don't want the user to modify the generated one,
+// since it'll get overwritten on a later build.
+#line 32 "${template}"
+
+#ifdef CVC4_STATISTICS_ON
+ #define INC_STAT(kind) \
+ { \
+ if (d_exprStatistics[kind] == NULL) { \
+ stringstream statName; \
+ statName << "expr::ExprManager::" << kind; \
+ d_exprStatistics[kind] = new IntStat(statName.str(), 0); \
+ d_nodeManager->getStatisticsRegistry()->registerStat_(d_exprStatistics[kind]); \
+ } \
+ ++ *(d_exprStatistics[kind]); \
+ }
+ #define INC_STAT_VAR(type, bound_var) \
+ { \
+ TypeNode* typeNode = Type::getTypeNode(type); \
+ TypeConstant type = typeNode->getKind() == kind::TYPE_CONSTANT ? typeNode->getConst<TypeConstant>() : LAST_TYPE; \
+ if (d_exprStatisticsVars[type] == NULL) { \
+ stringstream statName; \
+ if (type == LAST_TYPE) { \
+ statName << "expr::ExprManager::" << ((bound_var) ? "BOUND_VARIABLE" : "VARIABLE") << ":Parameterized type"; \
+ } else { \
+ statName << "expr::ExprManager::" << ((bound_var) ? "BOUND_VARIABLE" : "VARIABLE") << ":" << type; \
+ } \
+ d_exprStatisticsVars[type] = new IntStat(statName.str(), 0); \
+ d_nodeManager->getStatisticsRegistry()->registerStat_(d_exprStatisticsVars[type]); \
+ } \
+ ++ *(d_exprStatisticsVars[type]); \
+ }
+#else
+ #define INC_STAT(kind)
+ #define INC_STAT_VAR(type, bound_var)
+#endif
+
+using namespace std;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+
+ExprManager::ExprManager() :
+ d_nodeManager(new NodeManager(this)) {
+#ifdef CVC4_STATISTICS_ON
+ for (unsigned i = 0; i < kind::LAST_KIND; ++ i) {
+ d_exprStatistics[i] = NULL;
+ }
+ for (unsigned i = 0; i < LAST_TYPE; ++ i) {
+ d_exprStatisticsVars[i] = NULL;
+ }
+#endif
+}
+
+ExprManager::ExprManager(const Options& options) :
+ d_nodeManager(new NodeManager(this, options)) {
+#ifdef CVC4_STATISTICS_ON
+ for (unsigned i = 0; i < LAST_TYPE; ++ i) {
+ d_exprStatisticsVars[i] = NULL;
+ }
+ for (unsigned i = 0; i < kind::LAST_KIND; ++ i) {
+ d_exprStatistics[i] = NULL;
+ }
+#endif
+}
+
+ExprManager::~ExprManager() throw() {
+ NodeManagerScope nms(d_nodeManager);
+
+ try {
+
+#ifdef CVC4_STATISTICS_ON
+ for (unsigned i = 0; i < kind::LAST_KIND; ++ i) {
+ if (d_exprStatistics[i] != NULL) {
+ d_nodeManager->getStatisticsRegistry()->unregisterStat_(d_exprStatistics[i]);
+ delete d_exprStatistics[i];
+ d_exprStatistics[i] = NULL;
+ }
+ }
+ for (unsigned i = 0; i < LAST_TYPE; ++ i) {
+ if (d_exprStatisticsVars[i] != NULL) {
+ d_nodeManager->getStatisticsRegistry()->unregisterStat_(d_exprStatisticsVars[i]);
+ delete d_exprStatisticsVars[i];
+ d_exprStatisticsVars[i] = NULL;
+ }
+ }
+#endif
+
+ delete d_nodeManager;
+ d_nodeManager = NULL;
+
+ } catch(Exception& e) {
+ Warning() << "CVC4 threw an exception during cleanup." << std::endl
+ << e << std::endl;
+ }
+}
+
+StatisticsRegistry* ExprManager::getStatisticsRegistry() throw() {
+ return d_nodeManager->getStatisticsRegistry();
+}
+
+const Options& ExprManager::getOptions() const {
+ return d_nodeManager->getOptions();
+}
+
+ResourceManager* ExprManager::getResourceManager() throw() {
+ return d_nodeManager->getResourceManager();
+}
+
+BooleanType ExprManager::booleanType() const {
+ NodeManagerScope nms(d_nodeManager);
+ return BooleanType(Type(d_nodeManager, new TypeNode(d_nodeManager->booleanType())));
+}
+
+StringType ExprManager::stringType() const {
+ NodeManagerScope nms(d_nodeManager);
+ return StringType(Type(d_nodeManager, new TypeNode(d_nodeManager->stringType())));
+}
+
+RealType ExprManager::realType() const {
+ NodeManagerScope nms(d_nodeManager);
+ return RealType(Type(d_nodeManager, new TypeNode(d_nodeManager->realType())));
+}
+
+IntegerType ExprManager::integerType() const {
+ NodeManagerScope nms(d_nodeManager);
+ return IntegerType(Type(d_nodeManager, new TypeNode(d_nodeManager->integerType())));
+}
+
+Expr ExprManager::mkExpr(Kind kind, Expr child1) {
+ const kind::MetaKind mk = kind::metaKindOf(kind);
+ const unsigned n = 1 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0);
+ CheckArgument(mk == kind::metakind::PARAMETERIZED ||
+ mk == kind::metakind::OPERATOR, kind,
+ "Only operator-style expressions are made with mkExpr(); "
+ "to make variables and constants, see mkVar(), mkBoundVar(), "
+ "and mkConst().");
+ CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
+ "Exprs with kind %s must have at least %u children and "
+ "at most %u children (the one under construction has %u)",
+ kind::kindToString(kind).c_str(),
+ minArity(kind), maxArity(kind), n);
+ NodeManagerScope nms(d_nodeManager);
+ try {
+ INC_STAT(kind);
+ return Expr(this, d_nodeManager->mkNodePtr(kind, child1.getNode()));
+ } catch (const TypeCheckingExceptionPrivate& e) {
+ throw TypeCheckingException(this, &e);
+ }
+}
+
+Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2) {
+ const kind::MetaKind mk = kind::metaKindOf(kind);
+ const unsigned n = 2 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0);
+ CheckArgument(mk == kind::metakind::PARAMETERIZED ||
+ mk == kind::metakind::OPERATOR, kind,
+ "Only operator-style expressions are made with mkExpr(); "
+ "to make variables and constants, see mkVar(), mkBoundVar(), "
+ "and mkConst().");
+ CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
+ "Exprs with kind %s must have at least %u children and "
+ "at most %u children (the one under construction has %u)",
+ kind::kindToString(kind).c_str(),
+ minArity(kind), maxArity(kind), n);
+ NodeManagerScope nms(d_nodeManager);
+ try {
+ INC_STAT(kind);
+ return Expr(this, d_nodeManager->mkNodePtr(kind,
+ child1.getNode(),
+ child2.getNode()));
+ } catch (const TypeCheckingExceptionPrivate& e) {
+ throw TypeCheckingException(this, &e);
+ }
+}
+
+Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3) {
+ const kind::MetaKind mk = kind::metaKindOf(kind);
+ const unsigned n = 3 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0);
+ CheckArgument(mk == kind::metakind::PARAMETERIZED ||
+ mk == kind::metakind::OPERATOR, kind,
+ "Only operator-style expressions are made with mkExpr(); "
+ "to make variables and constants, see mkVar(), mkBoundVar(), "
+ "and mkConst().");
+ CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
+ "Exprs with kind %s must have at least %u children and "
+ "at most %u children (the one under construction has %u)",
+ kind::kindToString(kind).c_str(),
+ minArity(kind), maxArity(kind), n);
+ NodeManagerScope nms(d_nodeManager);
+ try {
+ INC_STAT(kind);
+ return Expr(this, d_nodeManager->mkNodePtr(kind,
+ child1.getNode(),
+ child2.getNode(),
+ child3.getNode()));
+ } catch (const TypeCheckingExceptionPrivate& e) {
+ throw TypeCheckingException(this, &e);
+ }
+}
+
+Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3,
+ Expr child4) {
+ const kind::MetaKind mk = kind::metaKindOf(kind);
+ const unsigned n = 4 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0);
+ CheckArgument(mk == kind::metakind::PARAMETERIZED ||
+ mk == kind::metakind::OPERATOR, kind,
+ "Only operator-style expressions are made with mkExpr(); "
+ "to make variables and constants, see mkVar(), mkBoundVar(), "
+ "and mkConst().");
+ CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
+ "Exprs with kind %s must have at least %u children and "
+ "at most %u children (the one under construction has %u)",
+ kind::kindToString(kind).c_str(),
+ minArity(kind), maxArity(kind), n);
+ NodeManagerScope nms(d_nodeManager);
+ try {
+ INC_STAT(kind);
+ return Expr(this, d_nodeManager->mkNodePtr(kind,
+ child1.getNode(),
+ child2.getNode(),
+ child3.getNode(),
+ child4.getNode()));
+ } catch (const TypeCheckingExceptionPrivate& e) {
+ throw TypeCheckingException(this, &e);
+ }
+}
+
+Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3,
+ Expr child4, Expr child5) {
+ const kind::MetaKind mk = kind::metaKindOf(kind);
+ const unsigned n = 5 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0);
+ CheckArgument(mk == kind::metakind::PARAMETERIZED ||
+ mk == kind::metakind::OPERATOR, kind,
+ "Only operator-style expressions are made with mkExpr(); "
+ "to make variables and constants, see mkVar(), mkBoundVar(), "
+ "and mkConst().");
+ CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
+ "Exprs with kind %s must have at least %u children and "
+ "at most %u children (the one under construction has %u)",
+ kind::kindToString(kind).c_str(),
+ minArity(kind), maxArity(kind), n);
+ NodeManagerScope nms(d_nodeManager);
+ try {
+ INC_STAT(kind);
+ return Expr(this, d_nodeManager->mkNodePtr(kind,
+ child1.getNode(),
+ child2.getNode(),
+ child3.getNode(),
+ child4.getNode(),
+ child5.getNode()));
+ } catch (const TypeCheckingExceptionPrivate& e) {
+ throw TypeCheckingException(this, &e);
+ }
+}
+
+Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) {
+ const kind::MetaKind mk = kind::metaKindOf(kind);
+ const unsigned n = children.size() - (mk == kind::metakind::PARAMETERIZED ? 1 : 0);
+ CheckArgument(mk == kind::metakind::PARAMETERIZED ||
+ mk == kind::metakind::OPERATOR, kind,
+ "Only operator-style expressions are made with mkExpr(); "
+ "to make variables and constants, see mkVar(), mkBoundVar(), "
+ "and mkConst().");
+ CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
+ "Exprs with kind %s must have at least %u children and "
+ "at most %u children (the one under construction has %u)",
+ kind::kindToString(kind).c_str(),
+ minArity(kind), maxArity(kind), n);
+
+ NodeManagerScope nms(d_nodeManager);
+
+ vector<Node> nodes;
+ vector<Expr>::const_iterator it = children.begin();
+ vector<Expr>::const_iterator it_end = children.end();
+ while(it != it_end) {
+ nodes.push_back(it->getNode());
+ ++it;
+ }
+ try {
+ INC_STAT(kind);
+ return Expr(this, d_nodeManager->mkNodePtr(kind, nodes));
+ } catch (const TypeCheckingExceptionPrivate& e) {
+ throw TypeCheckingException(this, &e);
+ }
+}
+
+Expr ExprManager::mkExpr(Kind kind, Expr child1,
+ const std::vector<Expr>& otherChildren) {
+ const kind::MetaKind mk = kind::metaKindOf(kind);
+ const unsigned n = otherChildren.size() - (mk == kind::metakind::PARAMETERIZED ? 1 : 0) + 1;
+ CheckArgument(mk == kind::metakind::PARAMETERIZED ||
+ mk == kind::metakind::OPERATOR, kind,
+ "Only operator-style expressions are made with mkExpr(); "
+ "to make variables and constants, see mkVar(), mkBoundVar(), "
+ "and mkConst().");
+ CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
+ "Exprs with kind %s must have at least %u children and "
+ "at most %u children (the one under construction has %u)",
+ kind::kindToString(kind).c_str(),
+ minArity(kind), maxArity(kind), n);
+
+ NodeManagerScope nms(d_nodeManager);
+
+ vector<Node> nodes;
+ nodes.push_back(child1.getNode());
+
+ vector<Expr>::const_iterator it = otherChildren.begin();
+ vector<Expr>::const_iterator it_end = otherChildren.end();
+ while(it != it_end) {
+ nodes.push_back(it->getNode());
+ ++it;
+ }
+ try {
+ INC_STAT(kind);
+ return Expr(this, d_nodeManager->mkNodePtr(kind, nodes));
+ } catch (const TypeCheckingExceptionPrivate& e) {
+ throw TypeCheckingException(this, &e);
+ }
+}
+
+Expr ExprManager::mkExpr(Expr opExpr) {
+ const unsigned n = 0;
+ Kind kind = NodeManager::operatorToKind(opExpr.getNode());
+ CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+ "This Expr constructor is for parameterized kinds only");
+ CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
+ "Exprs with kind %s must have at least %u children and "
+ "at most %u children (the one under construction has %u)",
+ kind::kindToString(kind).c_str(),
+ minArity(kind), maxArity(kind), n);
+ NodeManagerScope nms(d_nodeManager);
+ try {
+ INC_STAT(kind);
+ return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode()));
+ } catch (const TypeCheckingExceptionPrivate& e) {
+ throw TypeCheckingException(this, &e);
+ }
+}
+
+Expr ExprManager::mkExpr(Expr opExpr, Expr child1) {
+ const unsigned n = 1;
+ Kind kind = NodeManager::operatorToKind(opExpr.getNode());
+ CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+ "This Expr constructor is for parameterized kinds only");
+ CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
+ "Exprs with kind %s must have at least %u children and "
+ "at most %u children (the one under construction has %u)",
+ kind::kindToString(kind).c_str(),
+ minArity(kind), maxArity(kind), n);
+ NodeManagerScope nms(d_nodeManager);
+ try {
+ INC_STAT(kind);
+ return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(), child1.getNode()));
+ } catch (const TypeCheckingExceptionPrivate& e) {
+ throw TypeCheckingException(this, &e);
+ }
+}
+
+Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2) {
+ const unsigned n = 2;
+ Kind kind = NodeManager::operatorToKind(opExpr.getNode());
+ CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+ "This Expr constructor is for parameterized kinds only");
+ CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
+ "Exprs with kind %s must have at least %u children and "
+ "at most %u children (the one under construction has %u)",
+ kind::kindToString(kind).c_str(),
+ minArity(kind), maxArity(kind), n);
+ NodeManagerScope nms(d_nodeManager);
+ try {
+ INC_STAT(kind);
+ return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(),
+ child1.getNode(),
+ child2.getNode()));
+ } catch (const TypeCheckingExceptionPrivate& e) {
+ throw TypeCheckingException(this, &e);
+ }
+}
+
+Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3) {
+ const unsigned n = 3;
+ Kind kind = NodeManager::operatorToKind(opExpr.getNode());
+ CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+ "This Expr constructor is for parameterized kinds only");
+ CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
+ "Exprs with kind %s must have at least %u children and "
+ "at most %u children (the one under construction has %u)",
+ kind::kindToString(kind).c_str(),
+ minArity(kind), maxArity(kind), n);
+ NodeManagerScope nms(d_nodeManager);
+ try {
+ INC_STAT(kind);
+ return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(),
+ child1.getNode(),
+ child2.getNode(),
+ child3.getNode()));
+ } catch (const TypeCheckingExceptionPrivate& e) {
+ throw TypeCheckingException(this, &e);
+ }
+}
+
+Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3,
+ Expr child4) {
+ const unsigned n = 4;
+ Kind kind = NodeManager::operatorToKind(opExpr.getNode());
+ CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+ "This Expr constructor is for parameterized kinds only");
+ CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
+ "Exprs with kind %s must have at least %u children and "
+ "at most %u children (the one under construction has %u)",
+ kind::kindToString(kind).c_str(),
+ minArity(kind), maxArity(kind), n);
+ NodeManagerScope nms(d_nodeManager);
+ try {
+ INC_STAT(kind);
+ return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(),
+ child1.getNode(),
+ child2.getNode(),
+ child3.getNode(),
+ child4.getNode()));
+ } catch (const TypeCheckingExceptionPrivate& e) {
+ throw TypeCheckingException(this, &e);
+ }
+}
+
+Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3,
+ Expr child4, Expr child5) {
+ const unsigned n = 5;
+ Kind kind = NodeManager::operatorToKind(opExpr.getNode());
+ CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+ "This Expr constructor is for parameterized kinds only");
+ CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
+ "Exprs with kind %s must have at least %u children and "
+ "at most %u children (the one under construction has %u)",
+ kind::kindToString(kind).c_str(),
+ minArity(kind), maxArity(kind), n);
+ NodeManagerScope nms(d_nodeManager);
+ try {
+ INC_STAT(kind);
+ return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(),
+ child1.getNode(),
+ child2.getNode(),
+ child3.getNode(),
+ child4.getNode(),
+ child5.getNode()));
+ } catch (const TypeCheckingExceptionPrivate& e) {
+ throw TypeCheckingException(this, &e);
+ }
+}
+
+Expr ExprManager::mkExpr(Expr opExpr, const std::vector<Expr>& children) {
+ const unsigned n = children.size();
+ Kind kind = NodeManager::operatorToKind(opExpr.getNode());
+ CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+ "This Expr constructor is for parameterized kinds only");
+ CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
+ "Exprs with kind %s must have at least %u children and "
+ "at most %u children (the one under construction has %u)",
+ kind::kindToString(kind).c_str(),
+ minArity(kind), maxArity(kind), n);
+
+ NodeManagerScope nms(d_nodeManager);
+
+ vector<Node> nodes;
+ vector<Expr>::const_iterator it = children.begin();
+ vector<Expr>::const_iterator it_end = children.end();
+ while(it != it_end) {
+ nodes.push_back(it->getNode());
+ ++it;
+ }
+ try {
+ INC_STAT(kind);
+ return Expr(this,d_nodeManager->mkNodePtr(opExpr.getNode(), nodes));
+ } catch (const TypeCheckingExceptionPrivate& e) {
+ throw TypeCheckingException(this, &e);
+ }
+}
+
+bool ExprManager::hasOperator(Kind k) {
+ return NodeManager::hasOperator(k);
+}
+
+Expr ExprManager::operatorOf(Kind k) {
+ NodeManagerScope nms(d_nodeManager);
+
+ return d_nodeManager->operatorOf(k).toExpr();
+}
+
+/** Make a function type from domain to range. */
+FunctionType ExprManager::mkFunctionType(Type domain, Type range) {
+ NodeManagerScope nms(d_nodeManager);
+ return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(*domain.d_typeNode, *range.d_typeNode))));
+}
+
+/** Make a function type with input types from argTypes. */
+FunctionType ExprManager::mkFunctionType(const std::vector<Type>& argTypes, Type range) {
+ NodeManagerScope nms(d_nodeManager);
+ Assert( argTypes.size() >= 1 );
+ std::vector<TypeNode> argTypeNodes;
+ for (unsigned i = 0, i_end = argTypes.size(); i < i_end; ++ i) {
+ argTypeNodes.push_back(*argTypes[i].d_typeNode);
+ }
+ return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(argTypeNodes, *range.d_typeNode))));
+}
+
+FunctionType ExprManager::mkFunctionType(const std::vector<Type>& sorts) {
+ NodeManagerScope nms(d_nodeManager);
+ Assert( sorts.size() >= 2 );
+ std::vector<TypeNode> sortNodes;
+ for (unsigned i = 0, i_end = sorts.size(); i < i_end; ++ i) {
+ sortNodes.push_back(*sorts[i].d_typeNode);
+ }
+ return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(sortNodes))));
+}
+
+FunctionType ExprManager::mkPredicateType(const std::vector<Type>& sorts) {
+ NodeManagerScope nms(d_nodeManager);
+ Assert( sorts.size() >= 1 );
+ std::vector<TypeNode> sortNodes;
+ for (unsigned i = 0, i_end = sorts.size(); i < i_end; ++ i) {
+ sortNodes.push_back(*sorts[i].d_typeNode);
+ }
+ return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkPredicateType(sortNodes))));
+}
+
+TupleType ExprManager::mkTupleType(const std::vector<Type>& types) {
+ NodeManagerScope nms(d_nodeManager);
+ std::vector<TypeNode> typeNodes;
+ for (unsigned i = 0, i_end = types.size(); i < i_end; ++ i) {
+ typeNodes.push_back(*types[i].d_typeNode);
+ }
+ return TupleType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkTupleType(typeNodes))));
+}
+
+RecordType ExprManager::mkRecordType(const Record& rec) {
+ NodeManagerScope nms(d_nodeManager);
+ return RecordType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkRecordType(rec))));
+}
+
+SExprType ExprManager::mkSExprType(const std::vector<Type>& types) {
+ NodeManagerScope nms(d_nodeManager);
+ std::vector<TypeNode> typeNodes;
+ for (unsigned i = 0, i_end = types.size(); i < i_end; ++ i) {
+ typeNodes.push_back(*types[i].d_typeNode);
+ }
+ return SExprType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSExprType(typeNodes))));
+}
+
+BitVectorType ExprManager::mkBitVectorType(unsigned size) const {
+ NodeManagerScope nms(d_nodeManager);
+ return BitVectorType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkBitVectorType(size))));
+}
+
+ArrayType ExprManager::mkArrayType(Type indexType, Type constituentType) const {
+ NodeManagerScope nms(d_nodeManager);
+ return ArrayType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkArrayType(*indexType.d_typeNode, *constituentType.d_typeNode))));
+}
+
+SetType ExprManager::mkSetType(Type elementType) const {
+ NodeManagerScope nms(d_nodeManager);
+ return SetType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSetType(*elementType.d_typeNode))));
+}
+
+DatatypeType ExprManager::mkDatatypeType(const Datatype& datatype) {
+ // Not worth a special implementation; this doesn't need to be fast
+ // code anyway.
+ vector<Datatype> datatypes;
+ datatypes.push_back(datatype);
+ vector<DatatypeType> result = mkMutualDatatypeTypes(datatypes);
+ Assert(result.size() == 1);
+ return result.front();
+}
+
+std::vector<DatatypeType>
+ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
+ return mkMutualDatatypeTypes(datatypes, set<Type>());
+}
+
+std::vector<DatatypeType>
+ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
+ const std::set<Type>& unresolvedTypes) {
+ NodeManagerScope nms(d_nodeManager);
+ std::map<std::string, DatatypeType> nameResolutions;
+ std::vector<DatatypeType> dtts;
+
+ // First do some sanity checks, set up the final Type to be used for
+ // each datatype, and set up the "named resolutions" used to handle
+ // simple self- and mutual-recursion, for example in the definition
+ // "nat = succ(pred:nat) | zero", a named resolution can handle the
+ // pred selector.
+ for(std::vector<Datatype>::const_iterator i = datatypes.begin(),
+ i_end = datatypes.end();
+ i != i_end;
+ ++i) {
+ TypeNode* typeNode;
+ if( (*i).getNumParameters() == 0 ) {
+ typeNode = new TypeNode(d_nodeManager->mkTypeConst(*i));
+ } else {
+ TypeNode cons = d_nodeManager->mkTypeConst(*i);
+ std::vector< TypeNode > params;
+ params.push_back( cons );
+ for( unsigned int ip = 0; ip < (*i).getNumParameters(); ++ip ) {
+ params.push_back( TypeNode::fromType( (*i).getParameter( ip ) ) );
+ }
+
+ typeNode = new TypeNode(d_nodeManager->mkTypeNode(kind::PARAMETRIC_DATATYPE, params));
+ }
+ Type type(d_nodeManager, typeNode);
+ DatatypeType dtt(type);
+ CheckArgument(nameResolutions.find((*i).getName()) == nameResolutions.end(),
+ datatypes,
+ "cannot construct two datatypes at the same time "
+ "with the same name `%s'",
+ (*i).getName().c_str());
+ nameResolutions.insert(std::make_pair((*i).getName(), dtt));
+ dtts.push_back(dtt);
+ }
+
+ // Second, set up the type substitution map for complex type
+ // resolution (e.g. if "list" is the type we're defining, and it has
+ // a selector of type "ARRAY INT OF list", this can't be taken care
+ // of using the named resolutions that we set up above. A
+ // preliminary array type was set up, and now needs to have "list"
+ // substituted in it for the correct type.
+ //
+ // @TODO get rid of named resolutions altogether and handle
+ // everything with these resolutions?
+ std::vector< SortConstructorType > paramTypes;
+ std::vector< DatatypeType > paramReplacements;
+ std::vector<Type> placeholders;// to hold the "unresolved placeholders"
+ std::vector<Type> replacements;// to hold our final, resolved types
+ for(std::set<Type>::const_iterator i = unresolvedTypes.begin(),
+ i_end = unresolvedTypes.end();
+ i != i_end;
+ ++i) {
+ std::string name;
+ if( (*i).isSort() ) {
+ name = SortType(*i).getName();
+ } else {
+ Assert( (*i).isSortConstructor() );
+ name = SortConstructorType(*i).getName();
+ }
+ std::map<std::string, DatatypeType>::const_iterator resolver =
+ nameResolutions.find(name);
+ CheckArgument(resolver != nameResolutions.end(),
+ unresolvedTypes,
+ "cannot resolve type `%s'; it's not among "
+ "the datatypes being defined", name.c_str());
+ // We will instruct the Datatype to substitute "*i" (the
+ // unresolved SortType used as a placeholder in complex types)
+ // with "(*resolver).second" (the DatatypeType we created in the
+ // first step, above).
+ if( (*i).isSort() ) {
+ placeholders.push_back(*i);
+ replacements.push_back( (*resolver).second );
+ } else {
+ Assert( (*i).isSortConstructor() );
+ paramTypes.push_back( SortConstructorType(*i) );
+ paramReplacements.push_back( (*resolver).second );
+ }
+ }
+
+ // Lastly, perform the final resolutions and checks.
+ for(std::vector<DatatypeType>::iterator i = dtts.begin(),
+ i_end = dtts.end();
+ i != i_end;
+ ++i) {
+ const Datatype& dt = (*i).getDatatype();
+ if(!dt.isResolved()) {
+ const_cast<Datatype&>(dt).resolve(this, nameResolutions,
+ placeholders, replacements,
+ paramTypes, paramReplacements);
+ }
+
+ // Now run some checks, including a check to make sure that no
+ // selector is function-valued.
+ checkResolvedDatatype(*i);
+ }
+
+ for(std::vector<NodeManagerListener*>::iterator i = d_nodeManager->d_listeners.begin(); i != d_nodeManager->d_listeners.end(); ++i) {
+ (*i)->nmNotifyNewDatatypes(dtts);
+ }
+
+ return dtts;
+}
+
+void ExprManager::checkResolvedDatatype(DatatypeType dtt) const {
+ const Datatype& dt = dtt.getDatatype();
+
+ AssertArgument(dt.isResolved(), dtt, "datatype should have been resolved");
+
+ // for all constructors...
+ for(Datatype::const_iterator i = dt.begin(), i_end = dt.end();
+ i != i_end;
+ ++i) {
+ const DatatypeConstructor& c = *i;
+ Type testerType CVC4_UNUSED = c.getTester().getType();
+ Assert(c.isResolved() &&
+ testerType.isTester() &&
+ TesterType(testerType).getDomain() == dtt &&
+ TesterType(testerType).getRangeType() == booleanType(),
+ "malformed tester in datatype post-resolution");
+ Type ctorType CVC4_UNUSED = c.getConstructor().getType();
+ Assert(ctorType.isConstructor() &&
+ ConstructorType(ctorType).getArity() == c.getNumArgs() &&
+ ConstructorType(ctorType).getRangeType() == dtt,
+ "malformed constructor in datatype post-resolution");
+ // for all selectors...
+ for(DatatypeConstructor::const_iterator j = c.begin(), j_end = c.end();
+ j != j_end;
+ ++j) {
+ const DatatypeConstructorArg& a = *j;
+ Type selectorType = a.getSelector().getType();
+ Assert(a.isResolved() &&
+ selectorType.isSelector() &&
+ SelectorType(selectorType).getDomain() == dtt,
+ "malformed selector in datatype post-resolution");
+ // This next one's a "hard" check, performed in non-debug builds
+ // as well; the other ones should all be guaranteed by the
+ // CVC4::Datatype class, but this actually needs to be checked.
+ AlwaysAssert(!SelectorType(selectorType).getRangeType().d_typeNode->isFunctionLike(),
+ "cannot put function-like things in datatypes");
+ }
+ }
+}
+
+ConstructorType ExprManager::mkConstructorType(const DatatypeConstructor& constructor, Type range) const {
+ NodeManagerScope nms(d_nodeManager);
+ return Type(d_nodeManager, new TypeNode(d_nodeManager->mkConstructorType(constructor, *range.d_typeNode)));
+}
+
+SelectorType ExprManager::mkSelectorType(Type domain, Type range) const {
+ NodeManagerScope nms(d_nodeManager);
+ return Type(d_nodeManager, new TypeNode(d_nodeManager->mkSelectorType(*domain.d_typeNode, *range.d_typeNode)));
+}
+
+TesterType ExprManager::mkTesterType(Type domain) const {
+ NodeManagerScope nms(d_nodeManager);
+ return Type(d_nodeManager, new TypeNode(d_nodeManager->mkTesterType(*domain.d_typeNode)));
+}
+
+SortType ExprManager::mkSort(const std::string& name, uint32_t flags) const {
+ NodeManagerScope nms(d_nodeManager);
+ return SortType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name, flags))));
+}
+
+SortConstructorType ExprManager::mkSortConstructor(const std::string& name,
+ size_t arity) const {
+ NodeManagerScope nms(d_nodeManager);
+ return SortConstructorType(Type(d_nodeManager,
+ new TypeNode(d_nodeManager->mkSortConstructor(name, arity))));
+}
+
+/* - not in release 1.0
+Type ExprManager::mkPredicateSubtype(Expr lambda)
+ throw(TypeCheckingException) {
+ NodeManagerScope nms(d_nodeManager);
+ try {
+ return PredicateSubtype(Type(d_nodeManager,
+ new TypeNode(d_nodeManager->mkPredicateSubtype(lambda))));
+ } catch (const TypeCheckingExceptionPrivate& e) {
+ throw TypeCheckingException(this, &e);
+ }
+}
+*/
+
+/* - not in release 1.0
+Type ExprManager::mkPredicateSubtype(Expr lambda, Expr witness)
+ throw(TypeCheckingException) {
+ NodeManagerScope nms(d_nodeManager);
+ try {
+ return PredicateSubtype(Type(d_nodeManager,
+ new TypeNode(d_nodeManager->mkPredicateSubtype(lambda, witness))));
+ } catch (const TypeCheckingExceptionPrivate& e) {
+ throw TypeCheckingException(this, &e);
+ }
+}
+*/
+
+Type ExprManager::mkSubrangeType(const SubrangeBounds& bounds)
+ throw(TypeCheckingException) {
+ NodeManagerScope nms(d_nodeManager);
+ try {
+ return SubrangeType(Type(d_nodeManager,
+ new TypeNode(d_nodeManager->mkSubrangeType(bounds))));
+ } catch (const TypeCheckingExceptionPrivate& e) {
+ throw TypeCheckingException(this, &e);
+ }
+}
+
+/**
+ * Get the type for the given Expr and optionally do type checking.
+ *
+ * Initial type computation will be near-constant time if
+ * type checking is not requested. Results are memoized, so that
+ * subsequent calls to getType() without type checking will be
+ * constant time.
+ *
+ * Initial type checking is linear in the size of the expression.
+ * Again, the results are memoized, so that subsequent calls to
+ * getType(), with or without type checking, will be constant
+ * time.
+ *
+ * NOTE: A TypeCheckingException can be thrown even when type
+ * checking is not requested. getType() will always return a
+ * valid and correct type and, thus, an exception will be thrown
+ * when no valid or correct type can be computed (e.g., if the
+ * arguments to a bit-vector operation aren't bit-vectors). When
+ * type checking is not requested, getType() will do the minimum
+ * amount of checking required to return a valid result.
+ *
+ * @param e the Expr for which we want a type
+ * @param check whether we should check the type as we compute it
+ * (default: false)
+ */
+Type ExprManager::getType(Expr e, bool check) throw (TypeCheckingException) {
+ NodeManagerScope nms(d_nodeManager);
+ Type t;
+ try {
+ t = Type(d_nodeManager,
+ new TypeNode(d_nodeManager->getType(e.getNode(), check)));
+ } catch (const TypeCheckingExceptionPrivate& e) {
+ throw TypeCheckingException(this, &e);
+ }
+ return t;
+}
+
+Expr ExprManager::mkVar(const std::string& name, Type type, uint32_t flags) {
+ Assert(NodeManager::currentNM() == NULL, "ExprManager::mkVar() should only be called externally, not from within CVC4 code. Please use mkSkolem().");
+ NodeManagerScope nms(d_nodeManager);
+ Node* n = d_nodeManager->mkVarPtr(name, *type.d_typeNode, flags);
+ Debug("nm") << "set " << name << " on " << *n << std::endl;
+ INC_STAT_VAR(type, false);
+ return Expr(this, n);
+}
+
+Expr ExprManager::mkVar(Type type, uint32_t flags) {
+ Assert(NodeManager::currentNM() == NULL, "ExprManager::mkVar() should only be called externally, not from within CVC4 code. Please use mkSkolem().");
+ NodeManagerScope nms(d_nodeManager);
+ INC_STAT_VAR(type, false);
+ return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode, flags));
+}
+
+Expr ExprManager::mkBoundVar(const std::string& name, Type type) {
+ NodeManagerScope nms(d_nodeManager);
+ Node* n = d_nodeManager->mkBoundVarPtr(name, *type.d_typeNode);
+ Debug("nm") << "set " << name << " on " << *n << std::endl;
+ INC_STAT_VAR(type, true);
+ return Expr(this, n);
+}
+
+Expr ExprManager::mkBoundVar(Type type) {
+ NodeManagerScope nms(d_nodeManager);
+ INC_STAT_VAR(type, true);
+ return Expr(this, d_nodeManager->mkBoundVarPtr(*type.d_typeNode));
+}
+
+Expr ExprManager::mkAssociative(Kind kind,
+ const std::vector<Expr>& children) {
+ CheckArgument( kind::isAssociative(kind), kind,
+ "Illegal kind in mkAssociative: %s",
+ kind::kindToString(kind).c_str());
+
+ NodeManagerScope nms(d_nodeManager);
+ const unsigned int max = maxArity(kind);
+ const unsigned int min = minArity(kind);
+ unsigned int numChildren = children.size();
+
+ /* If the number of children is within bounds, then there's nothing to do. */
+ if( numChildren <= max ) {
+ return mkExpr(kind,children);
+ }
+
+ std::vector<Expr>::const_iterator it = children.begin() ;
+ std::vector<Expr>::const_iterator end = children.end() ;
+
+ /* The new top-level children and the children of each sub node */
+ std::vector<Node> newChildren;
+ std::vector<Node> subChildren;
+
+ while( it != end && numChildren > max ) {
+ /* Grab the next max children and make a node for them. */
+ for( std::vector<Expr>::const_iterator next = it + max;
+ it != next;
+ ++it, --numChildren ) {
+ subChildren.push_back(it->getNode());
+ }
+ Node subNode = d_nodeManager->mkNode(kind,subChildren);
+ newChildren.push_back(subNode);
+
+ subChildren.clear();
+ }
+
+ /* If there's children left, "top off" the Expr. */
+ if(numChildren > 0) {
+ /* If the leftovers are too few, just copy them into newChildren;
+ * otherwise make a new sub-node */
+ if(numChildren < min) {
+ for(; it != end; ++it) {
+ newChildren.push_back(it->getNode());
+ }
+ } else {
+ for(; it != end; ++it) {
+ subChildren.push_back(it->getNode());
+ }
+ Node subNode = d_nodeManager->mkNode(kind, subChildren);
+ newChildren.push_back(subNode);
+ }
+ }
+
+ /* It's inconceivable we could have enough children for this to fail
+ * (more than 2^32, in most cases?). */
+ AlwaysAssert( newChildren.size() <= max,
+ "Too many new children in mkAssociative" );
+
+ /* It would be really weird if this happened (it would require
+ * min > 2, for one thing), but let's make sure. */
+ AlwaysAssert( newChildren.size() >= min,
+ "Too few new children in mkAssociative" );
+
+ return Expr(this, d_nodeManager->mkNodePtr(kind,newChildren) );
+}
+
+unsigned ExprManager::minArity(Kind kind) {
+ return metakind::getLowerBoundForKind(kind);
+}
+
+unsigned ExprManager::maxArity(Kind kind) {
+ return metakind::getUpperBoundForKind(kind);
+}
+
+NodeManager* ExprManager::getNodeManager() const {
+ return d_nodeManager;
+}
+
+Statistics ExprManager::getStatistics() const throw() {
+ return Statistics(*d_nodeManager->getStatisticsRegistry());
+}
+
+SExpr ExprManager::getStatistic(const std::string& name) const throw() {
+ return d_nodeManager->getStatisticsRegistry()->getStatistic(name);
+}
+
+namespace expr {
+
+Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap);
+
+TypeNode exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* to, ExprManagerMapCollection& vmap) {
+ Debug("export") << "type: " << n << " " << n.getId() << std::endl;
+ if(theory::kindToTheoryId(n.getKind()) == theory::THEORY_DATATYPES) {
+ throw ExportUnsupportedException
+ ("export of types belonging to theory of DATATYPES kinds unsupported");
+ }
+ if(n.getMetaKind() == kind::metakind::PARAMETERIZED &&
+ n.getKind() != kind::SORT_TYPE) {
+ throw ExportUnsupportedException
+ ("export of PARAMETERIZED-kinded types (other than SORT_KIND) not supported");
+ }
+ if(n.getKind() == kind::TYPE_CONSTANT) {
+ return to->mkTypeConst(n.getConst<TypeConstant>());
+ } else if(n.getKind() == kind::BITVECTOR_TYPE) {
+ return to->mkBitVectorType(n.getConst<BitVectorSize>());
+ } else if(n.getKind() == kind::SUBRANGE_TYPE) {
+ return to->mkSubrangeType(n.getSubrangeBounds());
+ }
+ Type from_t = from->toType(n);
+ Type& to_t = vmap.d_typeMap[from_t];
+ if(! to_t.isNull()) {
+ Debug("export") << "+ mapped `" << from_t << "' to `" << to_t << "'" << std::endl;
+ return *Type::getTypeNode(to_t);
+ }
+ NodeBuilder<> children(to, n.getKind());
+ if(n.getKind() == kind::SORT_TYPE) {
+ Debug("export") << "type: operator: " << n.getOperator() << std::endl;
+ // make a new sort tag in target node manager
+ Node sortTag = NodeBuilder<0>(to, kind::SORT_TAG);
+ children << sortTag;
+ }
+ for(TypeNode::iterator i = n.begin(), i_end = n.end(); i != i_end; ++i) {
+ Debug("export") << "type: child: " << *i << std::endl;
+ children << exportTypeInternal(*i, from, to, vmap);
+ }
+ TypeNode out = children.constructTypeNode();// FIXME thread safety
+ to_t = to->toType(out);
+ return out;
+}/* exportTypeInternal() */
+
+}/* CVC4::expr namespace */
+
+Type ExprManager::exportType(const Type& t, ExprManager* em, ExprManagerMapCollection& vmap) {
+ Assert(t.d_nodeManager != em->d_nodeManager,
+ "Can't export a Type to the same ExprManager");
+ NodeManagerScope ems(t.d_nodeManager);
+ return Type(em->d_nodeManager,
+ new TypeNode(expr::exportTypeInternal(*t.d_typeNode, t.d_nodeManager, em->d_nodeManager, vmap)));
+}
+
+${mkConst_implementations}
+
+}/* CVC4 namespace */
/** 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
*/
SExprType mkSExprType(const std::vector<Type>& 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;
--- /dev/null
+/********************* */
+/*! \file expr_manager_template.h
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: Dejan Jovanovic
+ ** Minor contributors (to current version): Andrew Reynolds, Kshitij Bansal, Tim King, Christopher L. Conway
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Public-facing expression manager interface
+ **
+ ** Public-facing expression manager interface.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__EXPR_MANAGER_H
+#define __CVC4__EXPR_MANAGER_H
+
+#include <vector>
+
+#include "expr/kind.h"
+#include "expr/type.h"
+#include "expr/expr.h"
+#include "util/subrange_bound.h"
+#include "util/statistics.h"
+#include "util/sexpr.h"
+
+${includes}
+
+// This is a hack, but an important one: if there's an error, the
+// compiler directs the user to the template file instead of the
+// generated one. We don't want the user to modify the generated one,
+// since it'll get overwritten on a later build.
+#line 38 "${template}"
+
+namespace CVC4 {
+
+class Expr;
+class SmtEngine;
+class NodeManager;
+class Options;
+class IntStat;
+struct ExprManagerMapCollection;
+class StatisticsRegistry;
+class ResourceManager;
+
+namespace expr {
+ namespace pickle {
+ class Pickler;
+ }/* CVC4::expr::pickle namespace */
+}/* CVC4::expr namespace */
+
+namespace stats {
+ StatisticsRegistry* getStatisticsRegistry(ExprManager*);
+}/* CVC4::stats namespace */
+
+class CVC4_PUBLIC ExprManager {
+private:
+ /** The internal node manager */
+ NodeManager* d_nodeManager;
+
+ /** Counts of expressions and variables created of a given kind */
+ IntStat* d_exprStatisticsVars[LAST_TYPE];
+ IntStat* d_exprStatistics[kind::LAST_KIND];
+
+ /**
+ * Returns the internal node manager. This should only be used by
+ * internal users, i.e. the friend classes.
+ */
+ NodeManager* getNodeManager() const;
+
+ /**
+ * Check some things about a newly-created DatatypeType.
+ */
+ void checkResolvedDatatype(DatatypeType dtt) const;
+
+ /**
+ * SmtEngine will use all the internals, so it will grab the
+ * NodeManager.
+ */
+ friend class SmtEngine;
+
+ /** ExprManagerScope reaches in to get the NodeManager */
+ friend class ExprManagerScope;
+
+ /** NodeManager reaches in to get the NodeManager */
+ friend class NodeManager;
+
+ /** Statistics reach in to get the StatisticsRegistry */
+ friend ::CVC4::StatisticsRegistry* ::CVC4::stats::getStatisticsRegistry(ExprManager*);
+
+ /** Get the underlying statistics registry. */
+ StatisticsRegistry* getStatisticsRegistry() throw();
+
+ // undefined, private copy constructor and assignment op (disallow copy)
+ ExprManager(const ExprManager&) CVC4_UNDEFINED;
+ ExprManager& operator=(const ExprManager&) CVC4_UNDEFINED;
+
+public:
+
+ /**
+ * Creates an expression manager with default options.
+ */
+ ExprManager();
+
+ /**
+ * Creates an expression manager.
+ *
+ * @param options the earlyTypeChecking field is used to configure
+ * whether to do at Expr creation time.
+ */
+ explicit ExprManager(const Options& options);
+
+ /**
+ * Destroys the expression manager. No will be deallocated at this point, so
+ * any expression references that used to be managed by this expression
+ * manager and are left-over are bad.
+ */
+ ~ExprManager() throw();
+
+ /** Get this expr manager's options */
+ const Options& getOptions() const;
+
+ /** Get this expr manager's resource manager */
+ ResourceManager* getResourceManager() throw();
+
+ /** Get the type for booleans */
+ BooleanType booleanType() const;
+
+ /** Get the type for strings. */
+ StringType stringType() const;
+
+ /** Get the type for reals. */
+ RealType realType() const;
+
+ /** Get the type for integers */
+ IntegerType integerType() const;
+
+ /**
+ * Make a unary expression of a given kind (NOT, BVNOT, ...).
+ * @param kind the kind of expression
+ * @param child1 kind the kind of expression
+ * @return the expression
+ */
+ Expr mkExpr(Kind kind, Expr child1);
+
+ /**
+ * Make a binary expression of a given kind (AND, PLUS, ...).
+ * @param kind the kind of expression
+ * @param child1 the first child of the new expression
+ * @param child2 the second child of the new expression
+ * @return the expression
+ */
+ Expr mkExpr(Kind kind, Expr child1, Expr child2);
+
+ /**
+ * Make a 3-ary expression of a given kind (AND, PLUS, ...).
+ * @param kind the kind of expression
+ * @param child1 the first child of the new expression
+ * @param child2 the second child of the new expression
+ * @param child3 the third child of the new expression
+ * @return the expression
+ */
+ Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3);
+
+ /**
+ * Make a 4-ary expression of a given kind (AND, PLUS, ...).
+ * @param kind the kind of expression
+ * @param child1 the first child of the new expression
+ * @param child2 the second child of the new expression
+ * @param child3 the third child of the new expression
+ * @param child4 the fourth child of the new expression
+ * @return the expression
+ */
+ Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4);
+
+ /**
+ * Make a 5-ary expression of a given kind (AND, PLUS, ...).
+ * @param kind the kind of expression
+ * @param child1 the first child of the new expression
+ * @param child2 the second child of the new expression
+ * @param child3 the third child of the new expression
+ * @param child4 the fourth child of the new expression
+ * @param child5 the fifth child of the new expression
+ * @return the expression
+ */
+ Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4,
+ Expr child5);
+
+ /**
+ * Make an n-ary expression of given kind given a vector of its
+ * children
+ *
+ * @param kind the kind of expression to build
+ * @param children the subexpressions
+ * @return the n-ary expression
+ */
+ Expr mkExpr(Kind kind, const std::vector<Expr>& children);
+
+ /**
+ * Make an n-ary expression of given kind given a first arg and
+ * a vector of its remaining children (this can be useful where the
+ * kind is parameterized operator, so the first arg is really an
+ * arg to the kind to construct an operator)
+ *
+ * @param kind the kind of expression to build
+ * @param child1 the first subexpression
+ * @param otherChildren the remaining subexpressions
+ * @return the n-ary expression
+ */
+ Expr mkExpr(Kind kind, Expr child1, const std::vector<Expr>& otherChildren);
+
+ /**
+ * Make a nullary parameterized expression with the given operator.
+ *
+ * @param opExpr the operator expression
+ * @return the nullary expression
+ */
+ Expr mkExpr(Expr opExpr);
+
+ /**
+ * Make a unary parameterized expression with the given operator.
+ *
+ * @param opExpr the operator expression
+ * @param child1 the subexpression
+ * @return the unary expression
+ */
+ Expr mkExpr(Expr opExpr, Expr child1);
+
+ /**
+ * Make a binary parameterized expression with the given operator.
+ *
+ * @param opExpr the operator expression
+ * @param child1 the first subexpression
+ * @param child2 the second subexpression
+ * @return the binary expression
+ */
+ Expr mkExpr(Expr opExpr, Expr child1, Expr child2);
+
+ /**
+ * Make a ternary parameterized expression with the given operator.
+ *
+ * @param opExpr the operator expression
+ * @param child1 the first subexpression
+ * @param child2 the second subexpression
+ * @param child3 the third subexpression
+ * @return the ternary expression
+ */
+ Expr mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3);
+
+ /**
+ * Make a quaternary parameterized expression with the given operator.
+ *
+ * @param opExpr the operator expression
+ * @param child1 the first subexpression
+ * @param child2 the second subexpression
+ * @param child3 the third subexpression
+ * @param child4 the fourth subexpression
+ * @return the quaternary expression
+ */
+ Expr mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3, Expr child4);
+
+ /**
+ * Make a quinary parameterized expression with the given operator.
+ *
+ * @param opExpr the operator expression
+ * @param child1 the first subexpression
+ * @param child2 the second subexpression
+ * @param child3 the third subexpression
+ * @param child4 the fourth subexpression
+ * @param child5 the fifth subexpression
+ * @return the quinary expression
+ */
+ Expr mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3, Expr child4,
+ Expr child5);
+
+ /**
+ * Make an n-ary expression of given operator to apply and a vector
+ * of its children
+ *
+ * @param opExpr the operator expression
+ * @param children the subexpressions
+ * @return the n-ary expression
+ */
+ Expr mkExpr(Expr opExpr, const std::vector<Expr>& children);
+
+ /** Create a constant of type T */
+ template <class T>
+ Expr mkConst(const T&);
+
+ /**
+ * Create an Expr by applying an associative operator to the children.
+ * If <code>children.size()</code> is greater than the max arity for
+ * <code>kind</code>, then the expression will be broken up into
+ * suitably-sized chunks, taking advantage of the associativity of
+ * <code>kind</code>. For example, if kind <code>FOO</code> has max arity
+ * 2, then calling <code>mkAssociative(FOO,a,b,c)</code> will return
+ * <code>(FOO (FOO a b) c)</code> or <code>(FOO a (FOO b c))</code>.
+ * The order of the arguments will be preserved in a left-to-right
+ * traversal of the resulting tree.
+ */
+ Expr mkAssociative(Kind kind, const std::vector<Expr>& children);
+
+ /**
+ * Determine whether Exprs of a particular Kind have operators.
+ * @returns true if Exprs of Kind k have operators.
+ */
+ static bool hasOperator(Kind k);
+
+ /**
+ * Get the (singleton) operator of an OPERATOR-kinded kind. The
+ * returned Expr e will have kind BUILTIN, and calling
+ * e.getConst<CVC4::Kind>() will yield k.
+ */
+ Expr operatorOf(Kind k);
+
+ /** Make a function type from domain to range. */
+ FunctionType mkFunctionType(Type domain, Type range);
+
+ /**
+ * Make a function type with input types from argTypes.
+ * <code>argTypes</code> must have at least one element.
+ */
+ FunctionType mkFunctionType(const std::vector<Type>& argTypes, Type range);
+
+ /**
+ * Make a function type with input types from
+ * <code>sorts[0..sorts.size()-2]</code> and result type
+ * <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have
+ * at least 2 elements.
+ */
+ FunctionType mkFunctionType(const std::vector<Type>& sorts);
+
+ /**
+ * Make a predicate type with input types from
+ * <code>sorts</code>. The result with be a function type with range
+ * <code>BOOLEAN</code>. <code>sorts</code> must have at least one
+ * element.
+ */
+ FunctionType mkPredicateType(const std::vector<Type>& sorts);
+
+ /**
+ * Make a tuple type with types from
+ * <code>types[0..types.size()-1]</code>. <code>types</code> must
+ * have at least one element.
+ */
+ TupleType mkTupleType(const std::vector<Type>& types);
+
+ /**
+ * Make a record type with types from the rec parameter.
+ */
+ RecordType mkRecordType(const Record& rec);
+
+ /**
+ * Make a symbolic expressiontype with types from
+ * <code>types[0..types.size()-1]</code>. <code>types</code> may
+ * have any number of elements.
+ */
+ SExprType mkSExprType(const std::vector<Type>& types);
+
+ /** Make a type representing a bit-vector of the given size. */
+ BitVectorType mkBitVectorType(unsigned size) const;
+
+ /** Make the type of arrays with the given parameterization. */
+ ArrayType mkArrayType(Type indexType, Type constituentType) const;
+
+ /** Make the type of set with the given parameterization. */
+ SetType mkSetType(Type elementType) const;
+
+ /** Make a type representing the given datatype. */
+ DatatypeType mkDatatypeType(const Datatype& datatype);
+
+ /**
+ * Make a set of types representing the given datatypes, which may be
+ * mutually recursive.
+ */
+ std::vector<DatatypeType>
+ mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes);
+
+ /**
+ * Make a set of types representing the given datatypes, which may
+ * be mutually recursive. unresolvedTypes is a set of SortTypes
+ * that were used as placeholders in the Datatypes for the Datatypes
+ * of the same name. This is just a more complicated version of the
+ * above mkMutualDatatypeTypes() function, but is required to handle
+ * complex types.
+ *
+ * For example, unresolvedTypes might contain the single sort "list"
+ * (with that name reported from SortType::getName()). The
+ * datatypes list might have the single datatype
+ *
+ * DATATYPE
+ * list = cons(car:ARRAY INT OF list, cdr:list) | nil;
+ * END;
+ *
+ * To represent the Type of the array, the user had to create a
+ * placeholder type (an uninterpreted sort) to stand for "list" in
+ * the type of "car". It is this placeholder sort that should be
+ * passed in unresolvedTypes. If the datatype was of the simpler
+ * form:
+ *
+ * DATATYPE
+ * list = cons(car:list, cdr:list) | nil;
+ * END;
+ *
+ * then no complicated Type needs to be created, and the above,
+ * simpler form of mkMutualDatatypeTypes() is enough.
+ */
+ std::vector<DatatypeType>
+ mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
+ const std::set<Type>& unresolvedTypes);
+
+ /**
+ * Make a type representing a constructor with the given parameterization.
+ */
+ ConstructorType mkConstructorType(const DatatypeConstructor& constructor, Type range) const;
+
+ /** Make a type representing a selector with the given parameterization. */
+ SelectorType mkSelectorType(Type domain, Type range) const;
+
+ /** Make a type representing a tester with the given parameterization. */
+ TesterType mkTesterType(Type domain) const;
+
+ /** Bits for use in mkSort() flags. */
+ enum {
+ SORT_FLAG_NONE = 0,
+ SORT_FLAG_PLACEHOLDER = 1
+ };/* enum */
+
+ /** Make a new sort with the given name. */
+ SortType mkSort(const std::string& name, uint32_t flags = SORT_FLAG_NONE) const;
+
+ /** Make a sort constructor from a name and arity. */
+ SortConstructorType mkSortConstructor(const std::string& name,
+ size_t arity) const;
+
+ /**
+ * Make a predicate subtype type defined by the given LAMBDA
+ * expression. A TypeCheckingException can be thrown if lambda is
+ * not a LAMBDA, or is ill-typed, or if CVC4 fails at proving that
+ * the resulting predicate subtype is inhabited.
+ */
+ // not in release 1.0
+ //Type mkPredicateSubtype(Expr lambda)
+ // throw(TypeCheckingException);
+
+ /**
+ * Make a predicate subtype type defined by the given LAMBDA
+ * expression and whose non-emptiness is witnessed by the given
+ * witness. A TypeCheckingException can be thrown if lambda is not
+ * a LAMBDA, or is ill-typed, or if the witness is not a witness or
+ * ill-typed.
+ */
+ // not in release 1.0
+ //Type mkPredicateSubtype(Expr lambda, Expr witness)
+ // throw(TypeCheckingException);
+
+ /**
+ * Make an integer subrange type as defined by the argument.
+ */
+ Type mkSubrangeType(const SubrangeBounds& bounds)
+ throw(TypeCheckingException);
+
+ /** Get the type of an expression */
+ Type getType(Expr e, bool check = false)
+ throw(TypeCheckingException);
+
+ /** Bits for use in mkVar() flags. */
+ enum {
+ VAR_FLAG_NONE = 0,
+ VAR_FLAG_GLOBAL = 1,
+ VAR_FLAG_DEFINED = 2
+ };/* enum */
+
+ /**
+ * Create a new, fresh variable. This variable is guaranteed to be
+ * distinct from every variable thus far in the ExprManager, even
+ * if it shares a name with another; this is to support any kind of
+ * scoping policy on top of ExprManager. The SymbolTable class
+ * can be used to store and lookup symbols by name, if desired.
+ *
+ * @param name a name to associate to the fresh new variable
+ * @param type the type for the new variable
+ * @param flags - VAR_FLAG_NONE - no flags;
+ * VAR_FLAG_GLOBAL - whether this variable is to be
+ * considered "global" or not. Note that this information isn't
+ * used by the ExprManager, but is passed on to the ExprManager's
+ * event subscribers like the model-building service; if isGlobal
+ * is true, this newly-created variable will still available in
+ * models generated after an intervening pop.
+ * VAR_FLAG_DEFINED - if this is to be a "defined" symbol, e.g., for
+ * use with SmtEngine::defineFunction(). This keeps a declaration
+ * from being emitted in API dumps (since a subsequent definition is
+ * expected to be dumped instead).
+ */
+ Expr mkVar(const std::string& name, Type type, uint32_t flags = VAR_FLAG_NONE);
+
+ /**
+ * Create a (nameless) new, fresh variable. This variable is guaranteed
+ * to be distinct from every variable thus far in the ExprManager.
+ *
+ * @param type the type for the new variable
+ * @param flags - VAR_FLAG_GLOBAL - whether this variable is to be considered "global"
+ * or not. Note that this information isn't used by the ExprManager,
+ * but is passed on to the ExprManager's event subscribers like the
+ * model-building service; if isGlobal is true, this newly-created
+ * variable will still available in models generated after an
+ * intervening pop.
+ */
+ Expr mkVar(Type type, uint32_t flags = VAR_FLAG_NONE);
+
+ /**
+ * Create a new, fresh variable for use in a binder expression
+ * (the BOUND_VAR_LIST of a FORALL, EXISTS, or LAMBDA). It is
+ * an error for this bound variable to exist outside of a binder,
+ * and it should also only be used in a single binder expression.
+ * That is, two distinct FORALL expressions should use entirely
+ * disjoint sets of bound variables (however, a single FORALL
+ * expression can be used in multiple places in a formula without
+ * a problem). This newly-created bound variable is guaranteed to
+ * be distinct from every variable thus far in the ExprManager, even
+ * if it shares a name with another; this is to support any kind of
+ * scoping policy on top of ExprManager. The SymbolTable class
+ * can be used to store and lookup symbols by name, if desired.
+ *
+ * @param name a name to associate to the fresh new bound variable
+ * @param type the type for the new bound variable
+ */
+ Expr mkBoundVar(const std::string& name, Type type);
+
+ /**
+ * Create a (nameless) new, fresh variable for use in a binder
+ * expression (the BOUND_VAR_LIST of a FORALL, EXISTS, or LAMBDA).
+ * It is an error for this bound variable to exist outside of a
+ * binder, and it should also only be used in a single binder
+ * expression. That is, two distinct FORALL expressions should use
+ * entirely disjoint sets of bound variables (however, a single FORALL
+ * expression can be used in multiple places in a formula without
+ * a problem). This newly-created bound variable is guaranteed to
+ * be distinct from every variable thus far in the ExprManager.
+ *
+ * @param type the type for the new bound variable
+ */
+ Expr mkBoundVar(Type type);
+
+ /** Get a reference to the statistics registry for this ExprManager */
+ Statistics getStatistics() const throw();
+
+ /** Get a reference to the statistics registry for this ExprManager */
+ SExpr getStatistic(const std::string& name) const throw();
+
+ /** Export an expr to a different ExprManager */
+ //static Expr exportExpr(const Expr& e, ExprManager* em);
+ /** Export a type to a different ExprManager */
+ static Type exportType(const Type& t, ExprManager* em, ExprManagerMapCollection& vmap);
+
+ /** Returns the minimum arity of the given kind. */
+ static unsigned minArity(Kind kind);
+
+ /** Returns the maximum arity of the given kind. */
+ static unsigned maxArity(Kind kind);
+
+};/* class ExprManager */
+
+${mkConst_instantiations}
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__EXPR_MANAGER_H */
/** 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();
*/
inline TypeNode mkSExprType(const std::vector<TypeNode>& types);
+ /** Make the type of floating-point with <code>exp</code> bit exponent and
+ <code>sig</code> bit significand */
+ inline TypeNode mkFloatingPointType(unsigned exp, unsigned sig);
+ inline TypeNode mkFloatingPointType(FloatingPointSize fs);
+
/** Make the type of bitvectors of size <code>size</code> */
inline TypeNode mkBitVectorType(unsigned size);
return TypeNode(mkTypeConst<TypeConstant>(REGEXP_TYPE));
}
+/** Get the (singleton) type for rounding modes. */
+inline TypeNode NodeManager::roundingModeType() {
+ return TypeNode(mkTypeConst<TypeConstant>(ROUNDINGMODE_TYPE));
+}
+
/** Get the bound var list type. */
inline TypeNode NodeManager::boundVarListType() {
return TypeNode(mkTypeConst<TypeConstant>(BOUND_VAR_LIST_TYPE));
return TypeNode(mkTypeConst<BitVectorSize>(BitVectorSize(size)));
}
+inline TypeNode NodeManager::mkFloatingPointType(unsigned exp, unsigned sig) {
+ return TypeNode(mkTypeConst<FloatingPointSize>(FloatingPointSize(exp,sig)));
+}
+
+inline TypeNode NodeManager::mkFloatingPointType(FloatingPointSize fs) {
+ return TypeNode(mkTypeConst<FloatingPointSize>(fs));
+}
+
inline TypeNode NodeManager::mkArrayType(TypeNode indexType,
TypeNode constituentType) {
CheckArgument(!indexType.isNull(), indexType,
--- /dev/null
+/********************* */
+/*! \file node_manager.h
+ ** \verbatim
+ ** Original author: Dejan Jovanovic
+ ** Major contributors: Christopher L. Conway, Morgan Deters
+ ** Minor contributors (to current version): ACSYS, Tianyi Liang, Kshitij Bansal, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief A manager for Nodes
+ **
+ ** A manager for Nodes.
+ **
+ ** Reviewed by Chris Conway, Apr 5 2010 (bug #65).
+ **/
+
+#include "cvc4_private.h"
+
+/* circular dependency; force node.h first */
+//#include "expr/attribute.h"
+#include "expr/node.h"
+#include "expr/type_node.h"
+#include "expr/expr.h"
+#include "expr/expr_manager.h"
+
+#ifndef __CVC4__NODE_MANAGER_H
+#define __CVC4__NODE_MANAGER_H
+
+#include <vector>
+#include <string>
+#include <ext/hash_set>
+
+#include "expr/kind.h"
+#include "expr/metakind.h"
+#include "expr/node_value.h"
+#include "util/subrange_bound.h"
+#include "util/tls.h"
+#include "options/options.h"
+
+namespace CVC4 {
+
+class StatisticsRegistry;
+class ResourceManager;
+
+namespace expr {
+ namespace attr {
+ class AttributeUniqueId;
+ class AttributeManager;
+ }/* CVC4::expr::attr namespace */
+
+ class TypeChecker;
+}/* CVC4::expr namespace */
+
+/**
+ * An interface that an interested party can implement and then subscribe
+ * to NodeManager events via NodeManager::subscribeEvents(this).
+ */
+class NodeManagerListener {
+public:
+ virtual ~NodeManagerListener() { }
+ virtual void nmNotifyNewSort(TypeNode tn, uint32_t flags) { }
+ virtual void nmNotifyNewSortConstructor(TypeNode tn) { }
+ virtual void nmNotifyInstantiateSortConstructor(TypeNode ctor, TypeNode sort, uint32_t flags) { }
+ virtual void nmNotifyNewDatatypes(const std::vector<DatatypeType>& datatypes) { }
+ virtual void nmNotifyNewVar(TNode n, uint32_t flags) { }
+ virtual void nmNotifyNewSkolem(TNode n, const std::string& comment, uint32_t flags) { }
+ /**
+ * Notify a listener of a Node that's being GCed. If this function stores a reference
+ * to the Node somewhere, very bad things will happen.
+ */
+ virtual void nmNotifyDeleteNode(TNode n) { }
+};/* class NodeManagerListener */
+
+class NodeManager {
+ template <unsigned nchild_thresh> friend class CVC4::NodeBuilder;
+ friend class NodeManagerScope;
+ friend class expr::NodeValue;
+ friend class expr::TypeChecker;
+
+ // friends so they can access mkVar() here, which is private
+ friend Expr ExprManager::mkVar(const std::string&, Type, uint32_t flags);
+ friend Expr ExprManager::mkVar(Type, uint32_t flags);
+
+ // friend so it can access NodeManager's d_listeners and notify clients
+ friend std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>&, const std::set<Type>&);
+
+ /** Predicate for use with STL algorithms */
+ struct NodeValueReferenceCountNonZero {
+ bool operator()(expr::NodeValue* nv) { return nv->d_rc > 0; }
+ };
+
+ typedef __gnu_cxx::hash_set<expr::NodeValue*,
+ expr::NodeValuePoolHashFunction,
+ expr::NodeValuePoolEq> NodeValuePool;
+ typedef __gnu_cxx::hash_set<expr::NodeValue*,
+ expr::NodeValueIDHashFunction,
+ expr::NodeValueEq> ZombieSet;
+
+ static CVC4_THREADLOCAL(NodeManager*) s_current;
+
+ Options* d_options;
+ StatisticsRegistry* d_statisticsRegistry;
+ ResourceManager* d_resourceManager;
+
+ NodeValuePool d_nodeValuePool;
+
+ size_t next_id;
+
+ expr::attr::AttributeManager* d_attrManager;
+
+ /** The associated ExprManager */
+ ExprManager* d_exprManager;
+
+ /**
+ * The node value we're currently freeing. This unique node value
+ * is permitted to have outstanding TNodes to it (in "soft"
+ * contexts, like as a key in attribute tables), even though
+ * normally it's an error to have a TNode to a node value with a
+ * reference count of 0. Being "under deletion" also enables
+ * assertions that inc() is not called on it. (A poorly-behaving
+ * attribute cleanup function could otherwise create a "Node" that
+ * points to the node value that is in the process of being deleted,
+ * springing it back to life.)
+ */
+ expr::NodeValue* d_nodeUnderDeletion;
+
+ /**
+ * True iff we are in reclaimZombies(). This avoids unnecessary
+ * recursion; a NodeValue being deleted might zombify other
+ * NodeValues, but these shouldn't trigger a (recursive) call to
+ * reclaimZombies().
+ */
+ bool d_inReclaimZombies;
+
+ /**
+ * The set of zombie nodes. We may want to revisit this design, as
+ * we might like to delete nodes in least-recently-used order. But
+ * we also need to avoid processing a zombie twice.
+ */
+ ZombieSet d_zombies;
+
+ /**
+ * A set of operator singletons (w.r.t. to this NodeManager
+ * instance) for operators. Conceptually, Nodes with kind, say,
+ * PLUS, are APPLYs of a PLUS operator to arguments. This array
+ * holds the set of operators for these things. A PLUS operator is
+ * a Node with kind "BUILTIN", and if you call
+ * plusOperator->getConst<CVC4::Kind>(), you get kind::PLUS back.
+ */
+ Node d_operators[kind::LAST_KIND];
+
+ /**
+ * A list of subscribers for NodeManager events.
+ */
+ std::vector<NodeManagerListener*> d_listeners;
+
+ /**
+ * A map of tuple and record types to their corresponding datatype.
+ */
+ std::hash_map<TypeNode, TypeNode, TypeNodeHashFunction> d_tupleAndRecordTypes;
+
+ /**
+ * Keep a count of all abstract values produced by this NodeManager.
+ * Abstract values have a type attribute, so if multiple SmtEngines
+ * are attached to this NodeManager, we don't want their abstract
+ * values to overlap.
+ */
+ unsigned d_abstractValueCount;
+
+ /**
+ * A counter used to produce unique skolem names.
+ *
+ * Note that it is NOT incremented when skolems are created using
+ * SKOLEM_EXACT_NAME, so it is NOT a count of the skolems produced
+ * by this node manager.
+ */
+ unsigned d_skolemCounter;
+
+ /**
+ * Look up a NodeValue in the pool associated to this NodeManager.
+ * The NodeValue argument need not be a "completely-constructed"
+ * NodeValue. In particular, "non-inlined" constants are permitted
+ * (see below).
+ *
+ * For non-CONSTANT metakinds, nv's d_kind and d_nchildren should be
+ * correctly set, and d_children[0..n-1] should be valid (extant)
+ * NodeValues for lookup.
+ *
+ * For CONSTANT metakinds, nv's d_kind should be set correctly.
+ * Normally a CONSTANT would have d_nchildren == 0 and the constant
+ * value inlined in the d_children space. However, here we permit
+ * "non-inlined" NodeValues to avoid unnecessary copying. For
+ * these, d_nchildren == 1, and d_nchildren is a pointer to the
+ * constant value.
+ *
+ * The point of this complex design is to permit efficient lookups
+ * (without fully constructing a NodeValue). In the case that the
+ * argument is not fully constructed, and this function returns
+ * NULL, the caller should fully construct an equivalent one before
+ * calling poolInsert(). NON-FULLY-CONSTRUCTED NODEVALUES are not
+ * permitted in the pool!
+ */
+ inline expr::NodeValue* poolLookup(expr::NodeValue* nv) const;
+
+ /**
+ * Insert a NodeValue into the NodeManager's pool.
+ *
+ * It is an error to insert a NodeValue already in the pool.
+ * Enquire first with poolLookup().
+ */
+ inline void poolInsert(expr::NodeValue* nv);
+
+ /**
+ * Remove a NodeValue from the NodeManager's pool.
+ *
+ * It is an error to request the removal of a NodeValue from the
+ * pool that is not in the pool.
+ */
+ inline void poolRemove(expr::NodeValue* nv);
+
+ /**
+ * Determine if nv is currently being deleted by the NodeManager.
+ */
+ inline bool isCurrentlyDeleting(const expr::NodeValue* nv) const {
+ return d_nodeUnderDeletion == nv;
+ }
+
+ /**
+ * Register a NodeValue as a zombie.
+ */
+ inline void markForDeletion(expr::NodeValue* nv) {
+ Assert(nv->d_rc == 0);
+
+ // if d_reclaiming is set, make sure we don't call
+ // reclaimZombies(), because it's already running.
+ if(Debug.isOn("gc")) {
+ Debug("gc") << "zombifying node value " << nv
+ << " [" << nv->d_id << "]: ";
+ nv->printAst(Debug("gc"));
+ Debug("gc") << (d_inReclaimZombies ? " [CURRENTLY-RECLAIMING]" : "")
+ << std::endl;
+ }
+ d_zombies.insert(nv);// FIXME multithreading
+
+ if(safeToReclaimZombies()) {
+ if(d_zombies.size() > 5000) {
+ reclaimZombies();
+ }
+ }
+ }
+
+ /**
+ * Reclaim all zombies.
+ */
+ void reclaimZombies();
+
+ /**
+ * It is safe to collect zombies.
+ */
+ bool safeToReclaimZombies() const;
+
+ /**
+ * This template gives a mechanism to stack-allocate a NodeValue
+ * with enough space for N children (where N is a compile-time
+ * constant). You use it like this:
+ *
+ * NVStorage<4> nvStorage;
+ * NodeValue& nvStack = reinterpret_cast<NodeValue&>(nvStorage);
+ *
+ * ...and then you can use nvStack as a NodeValue that you know has
+ * room for 4 children.
+ */
+ template <size_t N>
+ struct NVStorage {
+ expr::NodeValue nv;
+ expr::NodeValue* child[N];
+ };/* struct NodeManager::NVStorage<N> */
+
+ /* A note on isAtomic() and isAtomicFormula() (in CVC3 parlance)..
+ *
+ * It has been decided for now to hold off on implementations of
+ * these functions, as they may only be needed in CNF conversion,
+ * where it's pointless to do a lazy isAtomic determination by
+ * searching through the DAG, and storing it, since the result will
+ * only be used once. For more details see the 4/27/2010 CVC4
+ * developer's meeting notes at:
+ *
+ * http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_April_27,_2010#isAtomic.28.29_and_isAtomicFormula.28.29
+ */
+ // bool containsDecision(TNode); // is "atomic"
+ // bool properlyContainsDecision(TNode); // all children are atomic
+
+ // undefined private copy constructor (disallow copy)
+ NodeManager(const NodeManager&) CVC4_UNDEFINED;
+
+ void init();
+
+ /**
+ * Create a variable with the given name and type. NOTE that no
+ * lookup is done on the name. If you mkVar("a", type) and then
+ * mkVar("a", type) again, you have two variables. The NodeManager
+ * version of this is private to avoid internal uses of mkVar() from
+ * within CVC4. Such uses should employ mkSkolem() instead.
+ */
+ Node mkVar(const std::string& name, const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
+ Node* mkVarPtr(const std::string& name, const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
+
+ /** Create a variable with the given type. */
+ Node mkVar(const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
+ Node* mkVarPtr(const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
+
+public:
+
+ explicit NodeManager(ExprManager* exprManager);
+ explicit NodeManager(ExprManager* exprManager, const Options& options);
+ ~NodeManager();
+
+ /** The node manager in the current public-facing CVC4 library context */
+ static NodeManager* currentNM() { return s_current; }
+ /** The resource manager associated with the current node manager */
+ static ResourceManager* currentResourceManager() { return s_current->d_resourceManager; }
+
+ /** Get this node manager's options (const version) */
+ const Options& getOptions() const {
+ return *d_options;
+ }
+
+ /** Get this node manager's options (non-const version) */
+ Options& getOptions() {
+ return *d_options;
+ }
+
+ /** Get this node manager's resource manager */
+ ResourceManager* getResourceManager() throw() { return d_resourceManager; }
+
+ /** Get this node manager's statistics registry */
+ StatisticsRegistry* getStatisticsRegistry() const throw() {
+ return d_statisticsRegistry;
+ }
+
+ /** Subscribe to NodeManager events */
+ void subscribeEvents(NodeManagerListener* listener) {
+ Assert(std::find(d_listeners.begin(), d_listeners.end(), listener) == d_listeners.end(), "listener already subscribed");
+ d_listeners.push_back(listener);
+ }
+
+ /** Unsubscribe from NodeManager events */
+ void unsubscribeEvents(NodeManagerListener* listener) {
+ std::vector<NodeManagerListener*>::iterator elt = std::find(d_listeners.begin(), d_listeners.end(), listener);
+ Assert(elt != d_listeners.end(), "listener not subscribed");
+ d_listeners.erase(elt);
+ }
+
+ /** Get a Kind from an operator expression */
+ static inline Kind operatorToKind(TNode n);
+
+ // general expression-builders
+
+ /** Create a node with one child. */
+ Node mkNode(Kind kind, TNode child1);
+ Node* mkNodePtr(Kind kind, TNode child1);
+
+ /** Create a node with two children. */
+ Node mkNode(Kind kind, TNode child1, TNode child2);
+ Node* mkNodePtr(Kind kind, TNode child1, TNode child2);
+
+ /** Create a node with three children. */
+ Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3);
+ Node* mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3);
+
+ /** Create a node with four children. */
+ Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3,
+ TNode child4);
+ Node* mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3,
+ TNode child4);
+
+ /** Create a node with five children. */
+ Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3,
+ TNode child4, TNode child5);
+ Node* mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3,
+ TNode child4, TNode child5);
+
+ /** Create a node with an arbitrary number of children. */
+ template <bool ref_count>
+ Node mkNode(Kind kind, const std::vector<NodeTemplate<ref_count> >& children);
+ template <bool ref_count>
+ Node* mkNodePtr(Kind kind, const std::vector<NodeTemplate<ref_count> >& children);
+
+ /** Create a node (with no children) by operator. */
+ Node mkNode(TNode opNode);
+ Node* mkNodePtr(TNode opNode);
+
+ /** Create a node with one child by operator. */
+ Node mkNode(TNode opNode, TNode child1);
+ Node* mkNodePtr(TNode opNode, TNode child1);
+
+ /** Create a node with two children by operator. */
+ Node mkNode(TNode opNode, TNode child1, TNode child2);
+ Node* mkNodePtr(TNode opNode, TNode child1, TNode child2);
+
+ /** Create a node with three children by operator. */
+ Node mkNode(TNode opNode, TNode child1, TNode child2, TNode child3);
+ Node* mkNodePtr(TNode opNode, TNode child1, TNode child2, TNode child3);
+
+ /** Create a node with four children by operator. */
+ Node mkNode(TNode opNode, TNode child1, TNode child2, TNode child3,
+ TNode child4);
+ Node* mkNodePtr(TNode opNode, TNode child1, TNode child2, TNode child3,
+ TNode child4);
+
+ /** Create a node with five children by operator. */
+ Node mkNode(TNode opNode, TNode child1, TNode child2, TNode child3,
+ TNode child4, TNode child5);
+ Node* mkNodePtr(TNode opNode, TNode child1, TNode child2, TNode child3,
+ TNode child4, TNode child5);
+
+ /** Create a node by applying an operator to the children. */
+ template <bool ref_count>
+ Node mkNode(TNode opNode, const std::vector<NodeTemplate<ref_count> >& children);
+ template <bool ref_count>
+ Node* mkNodePtr(TNode opNode, const std::vector<NodeTemplate<ref_count> >& children);
+
+ Node mkBoundVar(const std::string& name, const TypeNode& type);
+ Node* mkBoundVarPtr(const std::string& name, const TypeNode& type);
+
+ Node mkBoundVar(const TypeNode& type);
+ Node* mkBoundVarPtr(const TypeNode& type);
+
+ /**
+ * Optional flags used to control behavior of NodeManager::mkSkolem().
+ * They should be composed with a bitwise OR (e.g.,
+ * "SKOLEM_NO_NOTIFY | SKOLEM_EXACT_NAME"). Of course, SKOLEM_DEFAULT
+ * cannot be composed in such a manner.
+ */
+ enum SkolemFlags {
+ SKOLEM_DEFAULT = 0, /**< default behavior */
+ SKOLEM_NO_NOTIFY = 1, /**< do not notify subscribers */
+ SKOLEM_EXACT_NAME = 2,/**< do not make the name unique by adding the id */
+ SKOLEM_IS_GLOBAL = 4 /**< global vars appear in models even after a pop */
+ };/* enum SkolemFlags */
+
+ /**
+ * Create a skolem constant with the given name, type, and comment.
+ *
+ * @param prefix the name of the new skolem variable is the prefix
+ * appended with a unique ID. This way a family of skolem variables
+ * can be made with unique identifiers, used in dump, tracing, and
+ * debugging output. Use SKOLEM_EXECT_NAME flag if you don't want
+ * a unique ID appended and use prefix as the name.
+ *
+ * @param type the type of the skolem variable to create
+ *
+ * @param comment a comment for dumping output; if declarations are
+ * being dumped, this is included in a comment before the declaration
+ * and can be quite useful for debugging
+ *
+ * @param flags an optional mask of bits from SkolemFlags to control
+ * mkSkolem() behavior
+ */
+ Node mkSkolem(const std::string& prefix, const TypeNode& type,
+ const std::string& comment = "", int flags = SKOLEM_DEFAULT);
+
+ /** Create a instantiation constant with the given type. */
+ Node mkInstConstant(const TypeNode& type);
+
+ /** Make a new abstract value with the given type. */
+ Node mkAbstractValue(const TypeNode& type);
+
+ /**
+ * Create a constant of type T. It will have the appropriate
+ * CONST_* kind defined for T.
+ */
+ template <class T>
+ Node mkConst(const T&);
+
+ template <class T>
+ TypeNode mkTypeConst(const T&);
+
+ template <class NodeClass, class T>
+ NodeClass mkConstInternal(const T&);
+
+ /** Create a node with children. */
+ TypeNode mkTypeNode(Kind kind, TypeNode child1);
+ TypeNode mkTypeNode(Kind kind, TypeNode child1, TypeNode child2);
+ TypeNode mkTypeNode(Kind kind, TypeNode child1, TypeNode child2,
+ TypeNode child3);
+ TypeNode mkTypeNode(Kind kind, const std::vector<TypeNode>& children);
+
+ /**
+ * Determine whether Nodes of a particular Kind have operators.
+ * @returns true if Nodes of Kind k have operators.
+ */
+ static inline bool hasOperator(Kind k);
+
+ /**
+ * Get the (singleton) operator of an OPERATOR-kinded kind. The
+ * returned node n will have kind BUILTIN, and calling
+ * n.getConst<CVC4::Kind>() will yield k.
+ */
+ inline TNode operatorOf(Kind k) {
+ AssertArgument( kind::metaKindOf(k) == kind::metakind::OPERATOR, k,
+ "Kind is not an OPERATOR-kinded kind "
+ "in NodeManager::operatorOf()" );
+ return d_operators[k];
+ }
+
+ /**
+ * Retrieve an attribute for a node.
+ *
+ * @param nv the node value
+ * @param attr an instance of the attribute kind to retrieve.
+ * @returns the attribute, if set, or a default-constructed
+ * <code>AttrKind::value_type</code> if not.
+ */
+ template <class AttrKind>
+ inline typename AttrKind::value_type getAttribute(expr::NodeValue* nv,
+ const AttrKind& attr) const;
+
+ /**
+ * Check whether an attribute is set for a node.
+ *
+ * @param nv the node value
+ * @param attr an instance of the attribute kind to check
+ * @returns <code>true</code> iff <code>attr</code> is set for
+ * <code>nv</code>.
+ */
+ template <class AttrKind>
+ inline bool hasAttribute(expr::NodeValue* nv,
+ const AttrKind& attr) const;
+
+ /**
+ * Check whether an attribute is set for a node, and, if so,
+ * retrieve it.
+ *
+ * @param nv the node value
+ * @param attr an instance of the attribute kind to check
+ * @param value a reference to an object of the attribute's value type.
+ * <code>value</code> will be set to the value of the attribute, if it is
+ * set for <code>nv</code>; otherwise, it will be set to the default
+ * value of the attribute.
+ * @returns <code>true</code> iff <code>attr</code> is set for
+ * <code>nv</code>.
+ */
+ template <class AttrKind>
+ inline bool getAttribute(expr::NodeValue* nv,
+ const AttrKind& attr,
+ typename AttrKind::value_type& value) const;
+
+ /**
+ * Set an attribute for a node. If the node doesn't have the
+ * attribute, this function assigns one. If the node has one, this
+ * overwrites it.
+ *
+ * @param nv the node value
+ * @param attr an instance of the attribute kind to set
+ * @param value the value of <code>attr</code> for <code>nv</code>
+ */
+ template <class AttrKind>
+ inline void setAttribute(expr::NodeValue* nv,
+ const AttrKind& attr,
+ const typename AttrKind::value_type& value);
+
+ /**
+ * Retrieve an attribute for a TNode.
+ *
+ * @param n the node
+ * @param attr an instance of the attribute kind to retrieve.
+ * @returns the attribute, if set, or a default-constructed
+ * <code>AttrKind::value_type</code> if not.
+ */
+ template <class AttrKind>
+ inline typename AttrKind::value_type
+ getAttribute(TNode n, const AttrKind& attr) const;
+
+ /**
+ * Check whether an attribute is set for a TNode.
+ *
+ * @param n the node
+ * @param attr an instance of the attribute kind to check
+ * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
+ */
+ template <class AttrKind>
+ inline bool hasAttribute(TNode n,
+ const AttrKind& attr) const;
+
+ /**
+ * Check whether an attribute is set for a TNode and, if so, retieve
+ * it.
+ *
+ * @param n the node
+ * @param attr an instance of the attribute kind to check
+ * @param value a reference to an object of the attribute's value type.
+ * <code>value</code> will be set to the value of the attribute, if it is
+ * set for <code>nv</code>; otherwise, it will be set to the default value of
+ * the attribute.
+ * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
+ */
+ template <class AttrKind>
+ inline bool getAttribute(TNode n,
+ const AttrKind& attr,
+ typename AttrKind::value_type& value) const;
+
+ /**
+ * Set an attribute for a node. If the node doesn't have the
+ * attribute, this function assigns one. If the node has one, this
+ * overwrites it.
+ *
+ * @param n the node
+ * @param attr an instance of the attribute kind to set
+ * @param value the value of <code>attr</code> for <code>n</code>
+ */
+ template <class AttrKind>
+ inline void setAttribute(TNode n,
+ const AttrKind& attr,
+ const typename AttrKind::value_type& value);
+
+ /**
+ * Retrieve an attribute for a TypeNode.
+ *
+ * @param n the type node
+ * @param attr an instance of the attribute kind to retrieve.
+ * @returns the attribute, if set, or a default-constructed
+ * <code>AttrKind::value_type</code> if not.
+ */
+ template <class AttrKind>
+ inline typename AttrKind::value_type
+ getAttribute(TypeNode n, const AttrKind& attr) const;
+
+ /**
+ * Check whether an attribute is set for a TypeNode.
+ *
+ * @param n the type node
+ * @param attr an instance of the attribute kind to check
+ * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
+ */
+ template <class AttrKind>
+ inline bool hasAttribute(TypeNode n,
+ const AttrKind& attr) const;
+
+ /**
+ * Check whether an attribute is set for a TypeNode and, if so, retieve
+ * it.
+ *
+ * @param n the type node
+ * @param attr an instance of the attribute kind to check
+ * @param value a reference to an object of the attribute's value type.
+ * <code>value</code> will be set to the value of the attribute, if it is
+ * set for <code>nv</code>; otherwise, it will be set to the default value of
+ * the attribute.
+ * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
+ */
+ template <class AttrKind>
+ inline bool getAttribute(TypeNode n,
+ const AttrKind& attr,
+ typename AttrKind::value_type& value) const;
+
+ /**
+ * Set an attribute for a type node. If the node doesn't have the
+ * attribute, this function assigns one. If the type node has one,
+ * this overwrites it.
+ *
+ * @param n the type node
+ * @param attr an instance of the attribute kind to set
+ * @param value the value of <code>attr</code> for <code>n</code>
+ */
+ template <class AttrKind>
+ inline void setAttribute(TypeNode n,
+ const AttrKind& attr,
+ const typename AttrKind::value_type& value);
+
+ /** Get the (singleton) type for Booleans. */
+ inline TypeNode booleanType();
+
+ /** Get the (singleton) type for integers. */
+ inline TypeNode integerType();
+
+ /** Get the (singleton) type for reals. */
+ inline TypeNode realType();
+
+ /** Get the (singleton) type for strings. */
+ inline TypeNode stringType();
+
+ /** Get the (singleton) type for RegExp. */
+ inline TypeNode regexpType();
+
+ /** Get the bound var list type. */
+ inline TypeNode boundVarListType();
+
+ /** Get the instantiation pattern type. */
+ inline TypeNode instPatternType();
+
+ /** Get the instantiation pattern type. */
+ inline TypeNode instPatternListType();
+
+ /**
+ * Get the (singleton) type for builtin operators (that is, the type
+ * of the Node returned from Node::getOperator() when the operator
+ * is built-in, like EQUAL). */
+ inline TypeNode builtinOperatorType();
+
+ /**
+ * Make a function type from domain to range.
+ *
+ * @param domain the domain type
+ * @param range the range type
+ * @returns the functional type domain -> range
+ */
+ inline TypeNode mkFunctionType(const TypeNode& domain, const TypeNode& range);
+
+ /**
+ * Make a function type with input types from
+ * argTypes. <code>argTypes</code> must have at least one element.
+ *
+ * @param argTypes the domain is a tuple (argTypes[0], ..., argTypes[n])
+ * @param range the range type
+ * @returns the functional type (argTypes[0], ..., argTypes[n]) -> range
+ */
+ inline TypeNode mkFunctionType(const std::vector<TypeNode>& argTypes,
+ const TypeNode& range);
+
+ /**
+ * Make a function type with input types from
+ * <code>sorts[0..sorts.size()-2]</code> and result type
+ * <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have
+ * at least 2 elements.
+ */
+ inline TypeNode mkFunctionType(const std::vector<TypeNode>& sorts);
+
+ /**
+ * Make a predicate type with input types from
+ * <code>sorts</code>. The result with be a function type with range
+ * <code>BOOLEAN</code>. <code>sorts</code> must have at least one
+ * element.
+ */
+ inline TypeNode mkPredicateType(const std::vector<TypeNode>& sorts);
+
+ /**
+ * Make a tuple type with types from
+ * <code>types</code>. <code>types</code> must have at least one
+ * element.
+ *
+ * @param types a vector of types
+ * @returns the tuple type (types[0], ..., types[n])
+ */
+ inline TypeNode mkTupleType(const std::vector<TypeNode>& types);
+
+ /**
+ * Make a record type with the description from rec.
+ *
+ * @param rec a description of the record
+ * @returns the record type
+ */
+ inline TypeNode mkRecordType(const Record& rec);
+
+ /**
+ * Make a symbolic expression type with types from
+ * <code>types</code>. <code>types</code> may have any number of
+ * elements.
+ *
+ * @param types a vector of types
+ * @returns the symbolic expression type (types[0], ..., types[n])
+ */
+ inline TypeNode mkSExprType(const std::vector<TypeNode>& types);
+
+ /** Make the type of bitvectors of size <code>size</code> */
+ inline TypeNode mkBitVectorType(unsigned size);
+
+ /** Make the type of arrays with the given parameterization */
+ inline TypeNode mkArrayType(TypeNode indexType, TypeNode constituentType);
+
+ /** Make the type of arrays with the given parameterization */
+ inline TypeNode mkSetType(TypeNode elementType);
+
+ /** Make a type representing a constructor with the given parameterization */
+ TypeNode mkConstructorType(const DatatypeConstructor& constructor, TypeNode range);
+
+ /** Make a type representing a selector with the given parameterization */
+ inline TypeNode mkSelectorType(TypeNode domain, TypeNode range);
+
+ /** Make a type representing a tester with given parameterization */
+ inline TypeNode mkTesterType(TypeNode domain);
+
+ /** Make a new (anonymous) sort of arity 0. */
+ TypeNode mkSort(uint32_t flags = ExprManager::SORT_FLAG_NONE);
+
+ /** Make a new sort with the given name of arity 0. */
+ TypeNode mkSort(const std::string& name, uint32_t flags = ExprManager::SORT_FLAG_NONE);
+
+ /** Make a new sort by parameterizing the given sort constructor. */
+ TypeNode mkSort(TypeNode constructor,
+ const std::vector<TypeNode>& children,
+ uint32_t flags = ExprManager::SORT_FLAG_NONE);
+
+ /** Make a new sort with the given name and arity. */
+ TypeNode mkSortConstructor(const std::string& name, size_t arity);
+
+ /**
+ * Make a predicate subtype type defined by the given LAMBDA
+ * expression. A TypeCheckingExceptionPrivate can be thrown if
+ * lambda is not a LAMBDA, or is ill-typed, or if CVC4 fails at
+ * proving that the resulting predicate subtype is inhabited.
+ */
+ TypeNode mkPredicateSubtype(Expr lambda)
+ throw(TypeCheckingExceptionPrivate);
+
+ /**
+ * Make a predicate subtype type defined by the given LAMBDA
+ * expression and whose non-emptiness is witnessed by the given
+ * witness. A TypeCheckingExceptionPrivate can be thrown if lambda
+ * is not a LAMBDA, or is ill-typed, or if the witness is not a
+ * witness or ill-typed.
+ */
+ TypeNode mkPredicateSubtype(Expr lambda, Expr witness)
+ throw(TypeCheckingExceptionPrivate);
+
+ /**
+ * Make an integer subrange type as defined by the argument.
+ */
+ TypeNode mkSubrangeType(const SubrangeBounds& bounds)
+ throw(TypeCheckingExceptionPrivate);
+
+ /**
+ * Given a tuple or record type, get the internal datatype used for
+ * it. Makes the DatatypeType if necessary.
+ */
+ TypeNode getDatatypeForTupleRecord(TypeNode tupleRecordType);
+
+ /**
+ * Get the type for the given node and optionally do type checking.
+ *
+ * Initial type computation will be near-constant time if
+ * type checking is not requested. Results are memoized, so that
+ * subsequent calls to getType() without type checking will be
+ * constant time.
+ *
+ * Initial type checking is linear in the size of the expression.
+ * Again, the results are memoized, so that subsequent calls to
+ * getType(), with or without type checking, will be constant
+ * time.
+ *
+ * NOTE: A TypeCheckingException can be thrown even when type
+ * checking is not requested. getType() will always return a
+ * valid and correct type and, thus, an exception will be thrown
+ * when no valid or correct type can be computed (e.g., if the
+ * arguments to a bit-vector operation aren't bit-vectors). When
+ * type checking is not requested, getType() will do the minimum
+ * amount of checking required to return a valid result.
+ *
+ * @param n the Node for which we want a type
+ * @param check whether we should check the type as we compute it
+ * (default: false)
+ */
+ TypeNode getType(TNode n, bool check = false)
+ throw(TypeCheckingExceptionPrivate, AssertionException);
+
+ /**
+ * Convert a node to an expression. Uses the ExprManager
+ * associated to this NodeManager.
+ */
+ inline Expr toExpr(TNode n);
+
+ /**
+ * Convert an expression to a node.
+ */
+ static inline Node fromExpr(const Expr& e);
+
+ /**
+ * Convert a node manager to an expression manager.
+ */
+ inline ExprManager* toExprManager();
+
+ /**
+ * Convert an expression manager to a node manager.
+ */
+ static inline NodeManager* fromExprManager(ExprManager* exprManager);
+
+ /**
+ * Convert a type node to a type.
+ */
+ inline Type toType(TypeNode tn);
+
+ /**
+ * Convert a type to a type node.
+ */
+ static inline TypeNode fromType(Type t);
+
+ /** Reclaim zombies while there are more than k nodes in the pool (if possible).*/
+ void reclaimZombiesUntil(uint32_t k);
+
+ /** Reclaims all zombies (if possible).*/
+ void reclaimAllZombies();
+
+ /** Size of the node pool. */
+ size_t poolSize() const;
+
+ /** Deletes a list of attributes from the NM's AttributeManager.*/
+ void deleteAttributes(const std::vector< const expr::attr::AttributeUniqueId* >& ids);
+
+ /**
+ * This function gives developers a hook into the NodeManager.
+ * This can be changed in node_manager.cpp without recompiling most of cvc4.
+ *
+ * debugHook is a debugging only function, and should not be present in
+ * any published code!
+ */
+ void debugHook(int debugFlag);
+};/* class NodeManager */
+
+/**
+ * This class changes the "current" thread-global
+ * <code>NodeManager</code> when it is created and reinstates the
+ * previous thread-global <code>NodeManager</code> when it is
+ * destroyed, effectively maintaining a set of nested
+ * <code>NodeManager</code> scopes. This is especially useful on
+ * public-interface calls into the CVC4 library, where CVC4's notion
+ * of the "current" <code>NodeManager</code> should be set to match
+ * the calling context. See, for example, the implementations of
+ * public calls in the <code>ExprManager</code> and
+ * <code>SmtEngine</code> classes.
+ *
+ * The client must be careful to create and destroy
+ * <code>NodeManagerScope</code> objects in a well-nested manner (such
+ * as on the stack). You may create a <code>NodeManagerScope</code>
+ * with <code>new</code> and destroy it with <code>delete</code>, or
+ * place it as a data member of an object that is, but if the scope of
+ * these <code>new</code>/<code>delete</code> pairs isn't properly
+ * maintained, the incorrect "current" <code>NodeManager</code>
+ * pointer may be restored after a delete.
+ */
+class NodeManagerScope {
+ /** The old NodeManager, to be restored on destruction. */
+ NodeManager* d_oldNodeManager;
+
+public:
+
+ NodeManagerScope(NodeManager* nm) :
+ d_oldNodeManager(NodeManager::s_current) {
+ // There are corner cases where nm can be NULL and it's ok.
+ // For example, if you write { Expr e; }, then when the null
+ // Expr is destructed, there's no active node manager.
+ //Assert(nm != NULL);
+ NodeManager::s_current = nm;
+ Options::s_current = nm ? nm->d_options : NULL;
+ Debug("current") << "node manager scope: "
+ << NodeManager::s_current << "\n";
+ }
+
+ ~NodeManagerScope() {
+ NodeManager::s_current = d_oldNodeManager;
+ Options::s_current = d_oldNodeManager ? d_oldNodeManager->d_options : NULL;
+ Debug("current") << "node manager scope: "
+ << "returning to " << NodeManager::s_current << "\n";
+ }
+};/* class NodeManagerScope */
+
+/** Get the (singleton) type for booleans. */
+inline TypeNode NodeManager::booleanType() {
+ return TypeNode(mkTypeConst<TypeConstant>(BOOLEAN_TYPE));
+}
+
+/** Get the (singleton) type for integers. */
+inline TypeNode NodeManager::integerType() {
+ return TypeNode(mkTypeConst<TypeConstant>(INTEGER_TYPE));
+}
+
+/** Get the (singleton) type for reals. */
+inline TypeNode NodeManager::realType() {
+ return TypeNode(mkTypeConst<TypeConstant>(REAL_TYPE));
+}
+
+/** Get the (singleton) type for strings. */
+inline TypeNode NodeManager::stringType() {
+ return TypeNode(mkTypeConst<TypeConstant>(STRING_TYPE));
+}
+
+/** Get the (singleton) type for regexps. */
+inline TypeNode NodeManager::regexpType() {
+ return TypeNode(mkTypeConst<TypeConstant>(REGEXP_TYPE));
+}
+
+/** Get the bound var list type. */
+inline TypeNode NodeManager::boundVarListType() {
+ return TypeNode(mkTypeConst<TypeConstant>(BOUND_VAR_LIST_TYPE));
+}
+
+/** Get the instantiation pattern type. */
+inline TypeNode NodeManager::instPatternType() {
+ return TypeNode(mkTypeConst<TypeConstant>(INST_PATTERN_TYPE));
+}
+
+/** Get the instantiation pattern type. */
+inline TypeNode NodeManager::instPatternListType() {
+ return TypeNode(mkTypeConst<TypeConstant>(INST_PATTERN_LIST_TYPE));
+}
+
+/** Get the (singleton) type for builtin operators. */
+inline TypeNode NodeManager::builtinOperatorType() {
+ return TypeNode(mkTypeConst<TypeConstant>(BUILTIN_OPERATOR_TYPE));
+}
+
+/** Make a function type from domain to range. */
+inline TypeNode NodeManager::mkFunctionType(const TypeNode& domain, const TypeNode& range) {
+ std::vector<TypeNode> sorts;
+ sorts.push_back(domain);
+ sorts.push_back(range);
+ return mkFunctionType(sorts);
+}
+
+inline TypeNode NodeManager::mkFunctionType(const std::vector<TypeNode>& argTypes, const TypeNode& range) {
+ Assert(argTypes.size() >= 1);
+ std::vector<TypeNode> sorts(argTypes);
+ sorts.push_back(range);
+ return mkFunctionType(sorts);
+}
+
+inline TypeNode
+NodeManager::mkFunctionType(const std::vector<TypeNode>& sorts) {
+ Assert(sorts.size() >= 2);
+ std::vector<TypeNode> sortNodes;
+ for (unsigned i = 0; i < sorts.size(); ++ i) {
+ CheckArgument(!sorts[i].isFunctionLike(), sorts,
+ "cannot create higher-order function types");
+ sortNodes.push_back(sorts[i]);
+ }
+ return mkTypeNode(kind::FUNCTION_TYPE, sortNodes);
+}
+
+inline TypeNode
+NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts) {
+ Assert(sorts.size() >= 1);
+ std::vector<TypeNode> sortNodes;
+ for (unsigned i = 0; i < sorts.size(); ++ i) {
+ CheckArgument(!sorts[i].isFunctionLike(), sorts,
+ "cannot create higher-order function types");
+ sortNodes.push_back(sorts[i]);
+ }
+ sortNodes.push_back(booleanType());
+ return mkTypeNode(kind::FUNCTION_TYPE, sortNodes);
+}
+
+inline TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) {
+ std::vector<TypeNode> typeNodes;
+ for (unsigned i = 0; i < types.size(); ++ i) {
+ CheckArgument(!types[i].isFunctionLike(), types,
+ "cannot put function-like types in tuples");
+ typeNodes.push_back(types[i]);
+ }
+ return mkTypeNode(kind::TUPLE_TYPE, typeNodes);
+}
+
+inline TypeNode NodeManager::mkRecordType(const Record& rec) {
+ return mkTypeConst(rec);
+}
+
+inline TypeNode NodeManager::mkSExprType(const std::vector<TypeNode>& types) {
+ std::vector<TypeNode> typeNodes;
+ for (unsigned i = 0; i < types.size(); ++ i) {
+ typeNodes.push_back(types[i]);
+ }
+ return mkTypeNode(kind::SEXPR_TYPE, typeNodes);
+}
+
+inline TypeNode NodeManager::mkBitVectorType(unsigned size) {
+ return TypeNode(mkTypeConst<BitVectorSize>(BitVectorSize(size)));
+}
+
+inline TypeNode NodeManager::mkArrayType(TypeNode indexType,
+ TypeNode constituentType) {
+ CheckArgument(!indexType.isNull(), indexType,
+ "unexpected NULL index type");
+ CheckArgument(!constituentType.isNull(), constituentType,
+ "unexpected NULL constituent type");
+ CheckArgument(!indexType.isFunctionLike(), indexType,
+ "cannot index arrays by a function-like type");
+ CheckArgument(!constituentType.isFunctionLike(), constituentType,
+ "cannot store function-like types in arrays");
+ Debug("arrays") << "making array type " << indexType << " " << constituentType << std::endl;
+ return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType);
+}
+
+inline TypeNode NodeManager::mkSetType(TypeNode elementType) {
+ CheckArgument(!elementType.isNull(), elementType,
+ "unexpected NULL element type");
+ // TODO: Confirm meaning of isFunctionLike(). --K
+ CheckArgument(!elementType.isFunctionLike(), elementType,
+ "cannot store function-like types in sets");
+ Debug("sets") << "making sets type " << elementType << std::endl;
+ return mkTypeNode(kind::SET_TYPE, elementType);
+}
+
+inline TypeNode NodeManager::mkSelectorType(TypeNode domain, TypeNode range) {
+ CheckArgument(!domain.isFunctionLike(), domain,
+ "cannot create higher-order function types");
+ CheckArgument(!range.isFunctionLike(), range,
+ "cannot create higher-order function types");
+ return mkTypeNode(kind::SELECTOR_TYPE, domain, range);
+}
+
+inline TypeNode NodeManager::mkTesterType(TypeNode domain) {
+ CheckArgument(!domain.isFunctionLike(), domain,
+ "cannot create higher-order function types");
+ return mkTypeNode(kind::TESTER_TYPE, domain );
+}
+
+inline expr::NodeValue* NodeManager::poolLookup(expr::NodeValue* nv) const {
+ NodeValuePool::const_iterator find = d_nodeValuePool.find(nv);
+ if(find == d_nodeValuePool.end()) {
+ return NULL;
+ } else {
+ return *find;
+ }
+}
+
+inline void NodeManager::poolInsert(expr::NodeValue* nv) {
+ Assert(d_nodeValuePool.find(nv) == d_nodeValuePool.end(),
+ "NodeValue already in the pool!");
+ d_nodeValuePool.insert(nv);// FIXME multithreading
+}
+
+inline void NodeManager::poolRemove(expr::NodeValue* nv) {
+ Assert(d_nodeValuePool.find(nv) != d_nodeValuePool.end(),
+ "NodeValue is not in the pool!");
+
+ d_nodeValuePool.erase(nv);// FIXME multithreading
+}
+
+inline Expr NodeManager::toExpr(TNode n) {
+ return Expr(d_exprManager, new Node(n));
+}
+
+inline Node NodeManager::fromExpr(const Expr& e) {
+ return e.getNode();
+}
+
+inline ExprManager* NodeManager::toExprManager() {
+ return d_exprManager;
+}
+
+inline NodeManager* NodeManager::fromExprManager(ExprManager* exprManager) {
+ return exprManager->getNodeManager();
+}
+
+inline Type NodeManager::toType(TypeNode tn) {
+ return Type(this, new TypeNode(tn));
+}
+
+inline TypeNode NodeManager::fromType(Type t) {
+ return *Type::getTypeNode(t);
+}
+
+}/* CVC4 namespace */
+
+#define __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
+#include "expr/metakind.h"
+#undef __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
+
+#include "expr/node_builder.h"
+
+namespace CVC4 {
+
+// general expression-builders
+
+inline bool NodeManager::hasOperator(Kind k) {
+ switch(kind::MetaKind mk = kind::metaKindOf(k)) {
+
+ case kind::metakind::INVALID:
+ case kind::metakind::VARIABLE:
+ return false;
+
+ case kind::metakind::OPERATOR:
+ case kind::metakind::PARAMETERIZED:
+ return true;
+
+ case kind::metakind::CONSTANT:
+ return false;
+
+ default:
+ Unhandled(mk);
+ }
+}
+
+inline Kind NodeManager::operatorToKind(TNode n) {
+ return kind::operatorToKind(n.d_nv);
+}
+
+inline Node NodeManager::mkNode(Kind kind, TNode child1) {
+ NodeBuilder<1> nb(this, kind);
+ nb << child1;
+ return nb.constructNode();
+}
+
+inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1) {
+ NodeBuilder<1> nb(this, kind);
+ nb << child1;
+ return nb.constructNodePtr();
+}
+
+inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2) {
+ NodeBuilder<2> nb(this, kind);
+ nb << child1 << child2;
+ return nb.constructNode();
+}
+
+inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2) {
+ NodeBuilder<2> nb(this, kind);
+ nb << child1 << child2;
+ return nb.constructNodePtr();
+}
+
+inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
+ TNode child3) {
+ NodeBuilder<3> nb(this, kind);
+ nb << child1 << child2 << child3;
+ return nb.constructNode();
+}
+
+inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2,
+ TNode child3) {
+ NodeBuilder<3> nb(this, kind);
+ nb << child1 << child2 << child3;
+ return nb.constructNodePtr();
+}
+
+inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
+ TNode child3, TNode child4) {
+ NodeBuilder<4> nb(this, kind);
+ nb << child1 << child2 << child3 << child4;
+ return nb.constructNode();
+}
+
+inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2,
+ TNode child3, TNode child4) {
+ NodeBuilder<4> nb(this, kind);
+ nb << child1 << child2 << child3 << child4;
+ return nb.constructNodePtr();
+}
+
+inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
+ TNode child3, TNode child4, TNode child5) {
+ NodeBuilder<5> nb(this, kind);
+ nb << child1 << child2 << child3 << child4 << child5;
+ return nb.constructNode();
+}
+
+inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2,
+ TNode child3, TNode child4, TNode child5) {
+ NodeBuilder<5> nb(this, kind);
+ nb << child1 << child2 << child3 << child4 << child5;
+ return nb.constructNodePtr();
+}
+
+// N-ary version
+template <bool ref_count>
+inline Node NodeManager::mkNode(Kind kind,
+ const std::vector<NodeTemplate<ref_count> >&
+ children) {
+ NodeBuilder<> nb(this, kind);
+ nb.append(children);
+ return nb.constructNode();
+}
+
+template <bool ref_count>
+inline Node* NodeManager::mkNodePtr(Kind kind,
+ const std::vector<NodeTemplate<ref_count> >&
+ children) {
+ NodeBuilder<> nb(this, kind);
+ nb.append(children);
+ return nb.constructNodePtr();
+}
+
+// for operators
+inline Node NodeManager::mkNode(TNode opNode) {
+ NodeBuilder<1> nb(this, operatorToKind(opNode));
+ if(opNode.getKind() != kind::BUILTIN) {
+ nb << opNode;
+ }
+ return nb.constructNode();
+}
+
+inline Node* NodeManager::mkNodePtr(TNode opNode) {
+ NodeBuilder<1> nb(this, operatorToKind(opNode));
+ if(opNode.getKind() != kind::BUILTIN) {
+ nb << opNode;
+ }
+ return nb.constructNodePtr();
+}
+
+inline Node NodeManager::mkNode(TNode opNode, TNode child1) {
+ NodeBuilder<2> nb(this, operatorToKind(opNode));
+ if(opNode.getKind() != kind::BUILTIN) {
+ nb << opNode;
+ }
+ nb << child1;
+ return nb.constructNode();
+}
+
+inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1) {
+ NodeBuilder<2> nb(this, operatorToKind(opNode));
+ if(opNode.getKind() != kind::BUILTIN) {
+ nb << opNode;
+ }
+ nb << child1;
+ return nb.constructNodePtr();
+}
+
+inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2) {
+ NodeBuilder<3> nb(this, operatorToKind(opNode));
+ if(opNode.getKind() != kind::BUILTIN) {
+ nb << opNode;
+ }
+ nb << child1 << child2;
+ return nb.constructNode();
+}
+
+inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2) {
+ NodeBuilder<3> nb(this, operatorToKind(opNode));
+ if(opNode.getKind() != kind::BUILTIN) {
+ nb << opNode;
+ }
+ nb << child1 << child2;
+ return nb.constructNodePtr();
+}
+
+inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
+ TNode child3) {
+ NodeBuilder<4> nb(this, operatorToKind(opNode));
+ if(opNode.getKind() != kind::BUILTIN) {
+ nb << opNode;
+ }
+ nb << child1 << child2 << child3;
+ return nb.constructNode();
+}
+
+inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
+ TNode child3) {
+ NodeBuilder<4> nb(this, operatorToKind(opNode));
+ if(opNode.getKind() != kind::BUILTIN) {
+ nb << opNode;
+ }
+ nb << child1 << child2 << child3;
+ return nb.constructNodePtr();
+}
+
+inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
+ TNode child3, TNode child4) {
+ NodeBuilder<5> nb(this, operatorToKind(opNode));
+ if(opNode.getKind() != kind::BUILTIN) {
+ nb << opNode;
+ }
+ nb << child1 << child2 << child3 << child4;
+ return nb.constructNode();
+}
+
+inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
+ TNode child3, TNode child4) {
+ NodeBuilder<5> nb(this, operatorToKind(opNode));
+ if(opNode.getKind() != kind::BUILTIN) {
+ nb << opNode;
+ }
+ nb << child1 << child2 << child3 << child4;
+ return nb.constructNodePtr();
+}
+
+inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
+ TNode child3, TNode child4, TNode child5) {
+ NodeBuilder<6> nb(this, operatorToKind(opNode));
+ if(opNode.getKind() != kind::BUILTIN) {
+ nb << opNode;
+ }
+ nb << child1 << child2 << child3 << child4 << child5;
+ return nb.constructNode();
+}
+
+inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
+ TNode child3, TNode child4, TNode child5) {
+ NodeBuilder<6> nb(this, operatorToKind(opNode));
+ if(opNode.getKind() != kind::BUILTIN) {
+ nb << opNode;
+ }
+ nb << child1 << child2 << child3 << child4 << child5;
+ return nb.constructNodePtr();
+}
+
+// N-ary version for operators
+template <bool ref_count>
+inline Node NodeManager::mkNode(TNode opNode,
+ const std::vector<NodeTemplate<ref_count> >&
+ children) {
+ NodeBuilder<> nb(this, operatorToKind(opNode));
+ if(opNode.getKind() != kind::BUILTIN) {
+ nb << opNode;
+ }
+ nb.append(children);
+ return nb.constructNode();
+}
+
+template <bool ref_count>
+inline Node* NodeManager::mkNodePtr(TNode opNode,
+ const std::vector<NodeTemplate<ref_count> >&
+ children) {
+ NodeBuilder<> nb(this, operatorToKind(opNode));
+ if(opNode.getKind() != kind::BUILTIN) {
+ nb << opNode;
+ }
+ nb.append(children);
+ return nb.constructNodePtr();
+}
+
+
+inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1) {
+ return (NodeBuilder<1>(this, kind) << child1).constructTypeNode();
+}
+
+inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1,
+ TypeNode child2) {
+ return (NodeBuilder<2>(this, kind) << child1 << child2).constructTypeNode();
+}
+
+inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1,
+ TypeNode child2, TypeNode child3) {
+ return (NodeBuilder<3>(this, kind) << child1 << child2 << child3).constructTypeNode();
+}
+
+// N-ary version for types
+inline TypeNode NodeManager::mkTypeNode(Kind kind,
+ const std::vector<TypeNode>& children) {
+ return NodeBuilder<>(this, kind).append(children).constructTypeNode();
+}
+
+template <class T>
+Node NodeManager::mkConst(const T& val) {
+ return mkConstInternal<Node, T>(val);
+}
+
+template <class T>
+TypeNode NodeManager::mkTypeConst(const T& val) {
+ return mkConstInternal<TypeNode, T>(val);
+}
+
+template <class NodeClass, class T>
+NodeClass NodeManager::mkConstInternal(const T& val) {
+
+ // typedef typename kind::metakind::constantMap<T>::OwningTheory theory_t;
+ NVStorage<1> nvStorage;
+ expr::NodeValue& nvStack = reinterpret_cast<expr::NodeValue&>(nvStorage);
+
+ nvStack.d_id = 0;
+ nvStack.d_kind = kind::metakind::ConstantMap<T>::kind;
+ nvStack.d_rc = 0;
+ nvStack.d_nchildren = 1;
+
+#if defined(__GNUC__) && (__GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ >= 6))
+#pragma GCC diagnostic push
+#pragma GCC diagnostic ignored "-Warray-bounds"
+#endif
+
+ nvStack.d_children[0] =
+ const_cast<expr::NodeValue*>(reinterpret_cast<const expr::NodeValue*>(&val));
+ expr::NodeValue* nv = poolLookup(&nvStack);
+
+#if defined(__GNUC__) && (__GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ >= 6))
+#pragma GCC diagnostic pop
+#endif
+
+ if(nv != NULL) {
+ return NodeClass(nv);
+ }
+
+ nv = (expr::NodeValue*)
+ std::malloc(sizeof(expr::NodeValue) + sizeof(T));
+ if(nv == NULL) {
+ throw std::bad_alloc();
+ }
+
+ nv->d_nchildren = 0;
+ nv->d_kind = kind::metakind::ConstantMap<T>::kind;
+ nv->d_id = next_id++;// FIXME multithreading
+ nv->d_rc = 0;
+
+ //OwningTheory::mkConst(val);
+ new (&nv->d_children) T(val);
+
+ poolInsert(nv);
+ if(Debug.isOn("gc")) {
+ Debug("gc") << "creating node value " << nv
+ << " [" << nv->d_id << "]: ";
+ nv->printAst(Debug("gc"));
+ Debug("gc") << std::endl;
+ }
+
+ return NodeClass(nv);
+}
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__NODE_MANAGER_H */
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);
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);
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());
}
class IntegerType;
class RealType;
class StringType;
+class RoundingModeType;
class BitVectorType;
class ArrayType;
class SetType;
*/
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
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.
*/
};/* 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
*/
/** 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;
/** 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 <code>exp</code> exponent bits
+ and <code>sig</code> significand bits */
+ bool isFloatingPoint(unsigned exp, unsigned sig) const;
+
/** Is this a bit-vector type */
bool isBitVector() const;
/** 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;
inline bool TypeNode::isRegExp() const {
return getKind() == kind::TYPE_CONSTANT &&
getConst<TypeConstant>() == REGEXP_TYPE;
+ }
+
+inline bool TypeNode::isRoundingMode() const {
+ return getKind() == kind::TYPE_CONSTANT &&
+ getConst<TypeConstant>() == ROUNDINGMODE_TYPE;
}
inline bool TypeNode::isArray() 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 ||
return getKind() == kind::TESTER_TYPE;
}
+/** Is this a floating-point type of with <code>exp</code> exponent bits
+ and <code>sig</code> significand bits */
+inline bool TypeNode::isFloatingPoint(unsigned exp, unsigned sig) const {
+ return
+ ( getKind() == kind::FLOATINGPOINT_TYPE &&
+ getConst<FloatingPointSize>().exponent() == exp &&
+ getConst<FloatingPointSize>().significand() == sig ) ||
+ ( isPredicateSubtype() && getSubtypeParentType().isFloatingPoint(exp,sig) );
+}
+
/** Is this a bit-vector type of size <code>size</code> */
inline bool TypeNode::isBitVector(unsigned size) const {
return
}
}
+/** Get the exponent size of this floating-point type */
+inline unsigned TypeNode::getFloatingPointExponentSize() const {
+ Assert(isFloatingPoint());
+ return getConst<FloatingPointSize>().exponent();
+}
+
+/** Get the significand size of this floating-point type */
+inline unsigned TypeNode::getFloatingPointSignificandSize() const {
+ Assert(isFloatingPoint());
+ return getConst<FloatingPointSize>().significand();
+}
+
/** Get the size of this bit-vector type */
inline unsigned TypeNode::getBitVectorSize() const {
Assert(isBitVector());
../theory/idl/options.cpp \
../theory/idl/options.h \
../theory/sets/options.cpp \
- ../theory/sets/options.h
+ ../theory/sets/options.h \
+ ../theory/fp/options.cpp \
+ ../theory/fp/options.h
OPTIONS_FILES = \
$(patsubst %.cpp,%,$(filter %.cpp,$(OPTIONS_FILES_SRCS)))
../theory/idl/options.cpp \
../theory/idl/options.h \
../theory/sets/options.cpp \
- ../theory/sets/options.h
+ ../theory/sets/options.h \
+ ../theory/fp/options.cpp \
+ ../theory/fp/options.h
BUILT_SOURCES = \
exprs-builts \
#include "util/output.h"
#include "util/rational.h"
#include "util/hash.h"
+#include "util/floatingpoint.h"
#include <vector>
#include <set>
#include <string>
#include <sstream>
+// \todo Review the need for this header
+#include "math.h"
using namespace CVC4;
using namespace CVC4::parser;
std::string name;
std::vector<Expr> args;
std::vector< std::pair<std::string, Type> > sortedVarNames;
- Expr f, f2;
+ Expr f, f2, f3, f4;
std::string attr;
Expr attexpr;
std::vector<Expr> patexprs;
// valid GMP rational string
expr = MK_CONST( AntlrInput::tokenToRational($DECIMAL_LITERAL) ); }
- | LPAREN_TOK INDEX_TOK bvLit=SIMPLE_SYMBOL size=INTEGER_LITERAL RPAREN_TOK
- { if(AntlrInput::tokenText($bvLit).find("bv") == 0) {
- expr = MK_CONST( AntlrInput::tokenToBitvector($bvLit, $size) );
- } else {
- PARSER_STATE->parseError("Unexpected symbol `" + AntlrInput::tokenText($bvLit) + "'");
+ | LPAREN_TOK INDEX_TOK
+ ( bvLit=SIMPLE_SYMBOL size=INTEGER_LITERAL
+ { if(AntlrInput::tokenText($bvLit).find("bv") == 0) {
+ expr = MK_CONST( AntlrInput::tokenToBitvector($bvLit, $size) );
+ } else {
+ PARSER_STATE->parseError("Unexpected symbol `" + AntlrInput::tokenText($bvLit) + "'");
+ }
}
- }
+ | FP_PINF_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
+ { expr = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb),
+ AntlrInput::tokenToUnsigned($sb),
+ +INFINITY)); }
+ | FP_NINF_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
+ { expr = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb),
+ AntlrInput::tokenToUnsigned($sb),
+ -INFINITY)); }
+ | FP_NAN_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
+ { expr = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb),
+ AntlrInput::tokenToUnsigned($sb),
+ NAN)); }
+ // NOTE: Theory parametric constants go here
+
+ )
+ RPAREN_TOK
| HEX_LITERAL
{ assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 );
| str[s,false]
{ expr = MK_CONST( ::CVC4::String(s) ); }
+ | FP_RNE_TOK { expr = MK_CONST(roundNearestTiesToEven); }
+ | FP_RNA_TOK { expr = MK_CONST(roundNearestTiesToAway); }
+ | FP_RTP_TOK { expr = MK_CONST(roundTowardPositive); }
+ | FP_RTN_TOK { expr = MK_CONST(roundTowardNegative); }
+ | FP_RTZ_TOK { expr = MK_CONST(roundTowardZero); }
+ | FP_RNE_FULL_TOK { expr = MK_CONST(roundNearestTiesToEven); }
+ | FP_RNA_FULL_TOK { expr = MK_CONST(roundNearestTiesToAway); }
+ | FP_RTP_FULL_TOK { expr = MK_CONST(roundTowardPositive); }
+ | FP_RTN_FULL_TOK { expr = MK_CONST(roundTowardNegative); }
+ | FP_RTZ_FULL_TOK { expr = MK_CONST(roundTowardZero); }
| RENOSTR_TOK
{ std::vector< Expr > nvec; expr = MK_EXPR( CVC4::kind::REGEXP_EMPTY, nvec ); }
if(PARSER_STATE->strictModeEnabled()) {
PARSER_STATE->parseError("bv2nat and int2bv are not part of SMT-LIB, and aren't available in SMT-LIB strict compliance mode");
} }
+ | FP_PINF_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
+ { op = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb),
+ AntlrInput::tokenToUnsigned($sb),
+ +INFINITY)); }
+ | FP_NINF_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
+ { op = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb),
+ AntlrInput::tokenToUnsigned($sb),
+ -INFINITY)); }
+ | FP_NAN_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
+ { op = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb),
+ AntlrInput::tokenToUnsigned($sb),
+ NAN)); }
+ | FP_PZERO_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
+ { op = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb),
+ AntlrInput::tokenToUnsigned($sb),
+ +0.0)); }
+ | FP_NZERO_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
+ { op = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb),
+ AntlrInput::tokenToUnsigned($sb),
+ -0.0)); }
+ | FP_TO_FP_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
+ { op = MK_CONST(FloatingPointToFPGeneric(AntlrInput::tokenToUnsigned($eb),
+ AntlrInput::tokenToUnsigned($sb))); }
+ | FP_TO_FPBV_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
+ { op = MK_CONST(FloatingPointToFPIEEEBitVector(AntlrInput::tokenToUnsigned($eb),
+ AntlrInput::tokenToUnsigned($sb))); }
+ | FP_TO_FPFP_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
+ { op = MK_CONST(FloatingPointToFPFloatingPoint(AntlrInput::tokenToUnsigned($eb),
+ AntlrInput::tokenToUnsigned($sb))); }
+ | FP_TO_FPR_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
+ { op = MK_CONST(FloatingPointToFPReal(AntlrInput::tokenToUnsigned($eb),
+ AntlrInput::tokenToUnsigned($sb))); }
+ | FP_TO_FPS_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
+ { op = MK_CONST(FloatingPointToFPSignedBitVector(AntlrInput::tokenToUnsigned($eb),
+ AntlrInput::tokenToUnsigned($sb))); }
+ | FP_TO_FPU_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
+ { op = MK_CONST(FloatingPointToFPUnsignedBitVector(AntlrInput::tokenToUnsigned($eb),
+ AntlrInput::tokenToUnsigned($sb))); }
+ | FP_TO_UBV_TOK m=INTEGER_LITERAL
+ { op = MK_CONST(FloatingPointToUBV(AntlrInput::tokenToUnsigned($m))); }
+ | FP_TO_SBV_TOK m=INTEGER_LITERAL
+ { op = MK_CONST(FloatingPointToSBV(AntlrInput::tokenToUnsigned($m))); }
| badIndexedFunctionName
- )
+ )
RPAREN_TOK
;
| INST_CLOSURE_TOK { $kind = CVC4::kind::INST_CLOSURE; }
+ | FP_TOK { $kind = CVC4::kind::FLOATINGPOINT_FP; }
+ | FP_EQ_TOK { $kind = CVC4::kind::FLOATINGPOINT_EQ; }
+ | FP_ABS_TOK { $kind = CVC4::kind::FLOATINGPOINT_ABS; }
+ | FP_NEG_TOK { $kind = CVC4::kind::FLOATINGPOINT_NEG; }
+ | FP_PLUS_TOK { $kind = CVC4::kind::FLOATINGPOINT_PLUS; }
+ | FP_SUB_TOK { $kind = CVC4::kind::FLOATINGPOINT_SUB; }
+ | FP_MUL_TOK { $kind = CVC4::kind::FLOATINGPOINT_MULT; }
+ | FP_DIV_TOK { $kind = CVC4::kind::FLOATINGPOINT_DIV; }
+ | FP_FMA_TOK { $kind = CVC4::kind::FLOATINGPOINT_FMA; }
+ | FP_SQRT_TOK { $kind = CVC4::kind::FLOATINGPOINT_SQRT; }
+ | FP_REM_TOK { $kind = CVC4::kind::FLOATINGPOINT_REM; }
+ | FP_RTI_TOK { $kind = CVC4::kind::FLOATINGPOINT_RTI; }
+ | FP_MIN_TOK { $kind = CVC4::kind::FLOATINGPOINT_MIN; }
+ | FP_MAX_TOK { $kind = CVC4::kind::FLOATINGPOINT_MAX; }
+ | FP_LEQ_TOK { $kind = CVC4::kind::FLOATINGPOINT_LEQ; }
+ | FP_LT_TOK { $kind = CVC4::kind::FLOATINGPOINT_LT; }
+ | FP_GEQ_TOK { $kind = CVC4::kind::FLOATINGPOINT_GEQ; }
+ | FP_GT_TOK { $kind = CVC4::kind::FLOATINGPOINT_GT; }
+ | FP_ISN_TOK { $kind = CVC4::kind::FLOATINGPOINT_ISN; }
+ | FP_ISSN_TOK { $kind = CVC4::kind::FLOATINGPOINT_ISSN; }
+ | FP_ISZ_TOK { $kind = CVC4::kind::FLOATINGPOINT_ISZ; }
+ | FP_ISINF_TOK { $kind = CVC4::kind::FLOATINGPOINT_ISINF; }
+ | FP_ISNAN_TOK { $kind = CVC4::kind::FLOATINGPOINT_ISNAN; }
+ | FP_ISNEG_TOK { $kind = CVC4::kind::FLOATINGPOINT_ISNEG; }
+ | FP_ISPOS_TOK { $kind = CVC4::kind::FLOATINGPOINT_ISPOS; }
+ | FP_TO_REAL_TOK {$kind = CVC4::kind::FLOATINGPOINT_TO_REAL; }
// NOTE: Theory operators go here
;
PARSER_STATE->parseError("Illegal bitvector size: 0");
}
t = EXPR_MANAGER->mkBitVectorType(numerals.front());
+ } else if ( name == "FloatingPoint" ) {
+ if( numerals.size() != 2 ) {
+ PARSER_STATE->parseError("Illegal floating-point type.");
+ }
+ if(!validExponentSize(numerals[0])) {
+ PARSER_STATE->parseError("Illegal floating-point exponent size");
+ }
+ if(!validSignificandSize(numerals[1])) {
+ PARSER_STATE->parseError("Illegal floating-point significand size");
+ }
+ t = EXPR_MANAGER->mkFloatingPointType(numerals[0],numerals[1]);
} else {
std::stringstream ss;
ss << "unknown indexed symbol `" << name << "'";
// tokenized and handled directly when
// processing a term
+FP_TOK : 'fp';
+FP_PINF_TOK : '+oo';
+FP_NINF_TOK : '-oo';
+FP_PZERO_TOK : '+zero';
+FP_NZERO_TOK : '-zero';
+FP_NAN_TOK : 'NaN';
+FP_EQ_TOK : 'fp.eq';
+FP_ABS_TOK : 'fp.abs';
+FP_NEG_TOK : 'fp.neg';
+FP_PLUS_TOK : 'fp.add';
+FP_SUB_TOK : 'fp.sub';
+FP_MUL_TOK : 'fp.mul';
+FP_DIV_TOK : 'fp.div';
+FP_FMA_TOK : 'fp.fma';
+FP_SQRT_TOK : 'fp.sqrt';
+FP_REM_TOK : 'fp.rem';
+FP_RTI_TOK : 'fp.roundToIntegral';
+FP_MIN_TOK : 'fp.min';
+FP_MAX_TOK : 'fp.max';
+FP_LEQ_TOK : 'fp.leq';
+FP_LT_TOK : 'fp.lt';
+FP_GEQ_TOK : 'fp.geq';
+FP_GT_TOK : 'fp.gt';
+FP_ISN_TOK : 'fp.isNormal';
+FP_ISSN_TOK : 'fp.isSubnormal';
+FP_ISZ_TOK : 'fp.isZero';
+FP_ISINF_TOK : 'fp.isInfinite';
+FP_ISNAN_TOK : 'fp.isNaN';
+FP_ISNEG_TOK : 'fp.isNegative';
+FP_ISPOS_TOK : 'fp.isPositive';
+FP_TO_FP_TOK : 'to_fp';
+FP_TO_FPBV_TOK : 'to_fp_bv';
+FP_TO_FPFP_TOK : 'to_fp_fp';
+FP_TO_FPR_TOK : 'to_fp_real';
+FP_TO_FPS_TOK : 'to_fp_signed';
+FP_TO_FPU_TOK : 'to_fp_unsigned';
+FP_TO_UBV_TOK : 'fp.to_ubv';
+FP_TO_SBV_TOK : 'fp.to_sbv';
+FP_TO_REAL_TOK : 'fp.to_real';
+FP_RNE_TOK : 'RNE';
+FP_RNA_TOK : 'RNA';
+FP_RTP_TOK : 'RTP';
+FP_RTN_TOK : 'RTN';
+FP_RTZ_TOK : 'RTZ';
+FP_RNE_FULL_TOK : 'roundNearestTiesToEven';
+FP_RNA_FULL_TOK : 'roundNearestTiesToAway';
+FP_RTP_FULL_TOK : 'roundTowardPositive';
+FP_RTN_FULL_TOK : 'roundTowardNegative';
+FP_RTZ_FULL_TOK : 'roundTowardZero';
+
/**
* A sequence of printable ASCII characters (except backslash) that starts
* and ends with | and does not otherwise contain |.
Parser::addOperator(kind::STRING_LENGTH);
}
+void Smt2::addFloatingPointOperators() {
+ Parser::addOperator(kind::FLOATINGPOINT_FP);
+ Parser::addOperator(kind::FLOATINGPOINT_EQ);
+ Parser::addOperator(kind::FLOATINGPOINT_ABS);
+ Parser::addOperator(kind::FLOATINGPOINT_NEG);
+ Parser::addOperator(kind::FLOATINGPOINT_PLUS);
+ Parser::addOperator(kind::FLOATINGPOINT_SUB);
+ Parser::addOperator(kind::FLOATINGPOINT_MULT);
+ Parser::addOperator(kind::FLOATINGPOINT_DIV);
+ Parser::addOperator(kind::FLOATINGPOINT_FMA);
+ Parser::addOperator(kind::FLOATINGPOINT_SQRT);
+ Parser::addOperator(kind::FLOATINGPOINT_REM);
+ Parser::addOperator(kind::FLOATINGPOINT_RTI);
+ Parser::addOperator(kind::FLOATINGPOINT_MIN);
+ Parser::addOperator(kind::FLOATINGPOINT_MAX);
+ Parser::addOperator(kind::FLOATINGPOINT_LEQ);
+ Parser::addOperator(kind::FLOATINGPOINT_LT);
+ Parser::addOperator(kind::FLOATINGPOINT_GEQ);
+ Parser::addOperator(kind::FLOATINGPOINT_GT);
+ Parser::addOperator(kind::FLOATINGPOINT_ISN);
+ Parser::addOperator(kind::FLOATINGPOINT_ISSN);
+ Parser::addOperator(kind::FLOATINGPOINT_ISZ);
+ Parser::addOperator(kind::FLOATINGPOINT_ISINF);
+ Parser::addOperator(kind::FLOATINGPOINT_ISNAN);
+ Parser::addOperator(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR);
+ Parser::addOperator(kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT);
+ Parser::addOperator(kind::FLOATINGPOINT_TO_FP_REAL);
+ Parser::addOperator(kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR);
+ Parser::addOperator(kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR);
+ Parser::addOperator(kind::FLOATINGPOINT_TO_UBV);
+ Parser::addOperator(kind::FLOATINGPOINT_TO_SBV);
+ Parser::addOperator(kind::FLOATINGPOINT_TO_REAL);
+}
+
+
void Smt2::addTheory(Theory theory) {
switch(theory) {
case THEORY_ARRAYS:
Parser::addOperator(kind::APPLY_UF);
break;
+ case THEORY_FP:
+ defineType("RoundingMode", getExprManager()->roundingModeType());
+ defineType("Float16", getExprManager()->mkFloatingPointType(5, 11));
+ defineType("Float32", getExprManager()->mkFloatingPointType(8, 24));
+ defineType("Float64", getExprManager()->mkFloatingPointType(11, 53));
+ defineType("Float128", getExprManager()->mkFloatingPointType(15, 113));
+ addFloatingPointOperators();
+ break;
+
default:
std::stringstream ss;
ss << "internal error: unsupported theory " << theory;
return d_logic.isTheoryEnabled(theory::THEORY_STRINGS);
case THEORY_UF:
return d_logic.isTheoryEnabled(theory::THEORY_UF);
+ case THEORY_FP:
+ return d_logic.isTheoryEnabled(theory::THEORY_FP);
default:
std::stringstream ss;
ss << "internal error: unsupported theory " << theory;
if(d_logic.isQuantified()) {
addTheory(THEORY_QUANTIFIERS);
}
+
+ if (d_logic.isTheoryEnabled(theory::THEORY_FP)) {
+ addTheory(THEORY_FP);
+ }
+
}/* Smt2::setLogic() */
void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) {
THEORY_QUANTIFIERS,
THEORY_SETS,
THEORY_STRINGS,
- THEORY_UF
+ THEORY_UF,
+ THEORY_FP
};
private:
void addStringOperators();
+ void addFloatingPointOperators();
+
};/* class Smt2 */
}/* CVC4::parser namespace */
static string smtKindString(Kind k) throw();
static void printBvParameterizedOp(std::ostream& out, TNode n) throw();
+static void printFpParameterizedOp(std::ostream& out, TNode n) throw();
void Smt2Printer::toStream(std::ostream& out, TNode n,
int toDepth, bool types, size_t dag) const throw() {
case REAL_TYPE: out << "Real"; break;
case INTEGER_TYPE: out << "Int"; break;
case STRING_TYPE: out << "String"; break;
+ case ROUNDINGMODE_TYPE: out << "RoundingMode"; break;
default:
// fall back on whatever operator<< does on underlying type; we
// might luck out and be SMT-LIB v2 compliant
case kind::BITVECTOR_TYPE:
out << "(_ BitVec " << n.getConst<BitVectorSize>().size << ")";
break;
+ case kind::FLOATINGPOINT_TYPE:
+ out << "(_ FloatingPoint "
+ << n.getConst<FloatingPointSize>().exponent() << " "
+ << n.getConst<FloatingPointSize>().significand()
+ << ")";
+ break;
case kind::CONST_BITVECTOR: {
const BitVector& bv = n.getConst<BitVector>();
const Integer& x = bv.getValue();
// }
break;
}
+ case kind::CONST_FLOATINGPOINT:
+ out << n.getConst<FloatingPoint>().getLiteral();
+ break;
+ case kind::CONST_ROUNDINGMODE:
+ switch (n.getConst<RoundingMode>()) {
+ case roundNearestTiesToEven : out << "roundNearestTiesToEven"; break;
+ case roundNearestTiesToAway : out << "roundNearestTiesToAway"; break;
+ case roundTowardPositive : out << "roundTowardPositive"; break;
+ case roundTowardNegative : out << "roundTowardNegative"; break;
+ case roundTowardZero : out << "roundTowardZero"; break;
+ default :
+ Unreachable("Invalid value of rounding mode constant (%d)",n.getConst<RoundingMode>());
+ }
+ break;
case kind::CONST_BOOLEAN:
// the default would print "1" or "0" for bool, that's not correct
// for our purposes
case kind::SET_TYPE:
case kind::SINGLETON: out << smtKindString(k) << " "; break;
- // datatypes
+ // fp theory
+ case kind::FLOATINGPOINT_FP:
+ case kind::FLOATINGPOINT_EQ:
+ case kind::FLOATINGPOINT_ABS:
+ case kind::FLOATINGPOINT_NEG:
+ case kind::FLOATINGPOINT_PLUS:
+ case kind::FLOATINGPOINT_SUB:
+ case kind::FLOATINGPOINT_MULT:
+ case kind::FLOATINGPOINT_DIV:
+ case kind::FLOATINGPOINT_FMA:
+ case kind::FLOATINGPOINT_SQRT:
+ case kind::FLOATINGPOINT_REM:
+ case kind::FLOATINGPOINT_RTI:
+ case kind::FLOATINGPOINT_MIN:
+ case kind::FLOATINGPOINT_MAX:
+ case kind::FLOATINGPOINT_LEQ:
+ case kind::FLOATINGPOINT_LT:
+ case kind::FLOATINGPOINT_GEQ:
+ case kind::FLOATINGPOINT_GT:
+ case kind::FLOATINGPOINT_ISN:
+ case kind::FLOATINGPOINT_ISSN:
+ case kind::FLOATINGPOINT_ISZ:
+ case kind::FLOATINGPOINT_ISINF:
+ case kind::FLOATINGPOINT_ISNAN:
+ case kind::FLOATINGPOINT_ISNEG:
+ case kind::FLOATINGPOINT_ISPOS:
+ case kind::FLOATINGPOINT_TO_REAL:
+ out << smtKindString(k) << ' '; break;
+
+ case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR:
+ case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT:
+ case kind::FLOATINGPOINT_TO_FP_REAL:
+ case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR:
+ case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR:
+ case kind::FLOATINGPOINT_TO_FP_GENERIC:
+ case kind::FLOATINGPOINT_TO_UBV:
+ case kind::FLOATINGPOINT_TO_SBV:
+ printFpParameterizedOp(out, n);
+ out << ' ';
+ stillNeedToPrintParams = false;
+ break;
+
+ // datatypes
case kind::APPLY_TYPE_ASCRIPTION: {
TypeNode t = TypeNode::fromType(n.getOperator().getConst<AscriptionType>().getType());
if(t.getKind() == kind::TYPE_CONSTANT &&
case kind::SET_TYPE: return "Set";
case kind::SINGLETON: return "singleton";
case kind::INSERT: return "insert";
+
+ // fp theory
+ case kind::FLOATINGPOINT_FP: return "fp";
+ case kind::FLOATINGPOINT_EQ: return "fp.eq";
+ case kind::FLOATINGPOINT_ABS: return "fp.abs";
+ case kind::FLOATINGPOINT_NEG: return "fp.neg";
+ case kind::FLOATINGPOINT_PLUS: return "fp.add";
+ case kind::FLOATINGPOINT_SUB: return "fp.sub";
+ case kind::FLOATINGPOINT_MULT: return "fp.mul";
+ case kind::FLOATINGPOINT_DIV: return "fp.div";
+ case kind::FLOATINGPOINT_FMA: return "fp.fma";
+ case kind::FLOATINGPOINT_SQRT: return "fp.sqrt";
+ case kind::FLOATINGPOINT_REM: return "fp.rem";
+ case kind::FLOATINGPOINT_RTI: return "fp.roundToIntegral";
+ case kind::FLOATINGPOINT_MIN: return "fp.min";
+ case kind::FLOATINGPOINT_MAX: return "fp.max";
+
+ case kind::FLOATINGPOINT_LEQ: return "fp.leq";
+ case kind::FLOATINGPOINT_LT: return "fp.lt";
+ case kind::FLOATINGPOINT_GEQ: return "fp.geq";
+ case kind::FLOATINGPOINT_GT: return "fp.gt";
+
+ case kind::FLOATINGPOINT_ISN: return "fp.isNormal";
+ case kind::FLOATINGPOINT_ISSN: return "fp.isSubnormal";
+ case kind::FLOATINGPOINT_ISZ: return "fp.isZero";
+ case kind::FLOATINGPOINT_ISINF: return "fp.isInfinite";
+ case kind::FLOATINGPOINT_ISNAN: return "fp.isNaN";
+ case kind::FLOATINGPOINT_ISNEG: return "fp.isNegative";
+ case kind::FLOATINGPOINT_ISPOS: return "fp.isPositive";
+
+ case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: return "to_fp";
+ case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT: return "to_fp";
+ case kind::FLOATINGPOINT_TO_FP_REAL: return "to_fp";
+ case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: return "to_fp";
+ case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: return "to_fp_unsigned";
+ case kind::FLOATINGPOINT_TO_FP_GENERIC: return "to_fp_unsigned";
+ case kind::FLOATINGPOINT_TO_UBV: return "fp.to_ubv";
+ case kind::FLOATINGPOINT_TO_SBV: return "fp.to_sbv";
+ case kind::FLOATINGPOINT_TO_REAL: return "fp.to_real";
+
default:
; /* fall through */
}
out << ")";
}
+static void printFpParameterizedOp(std::ostream& out, TNode n) throw() {
+ out << "(_ ";
+ switch(n.getKind()) {
+ case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR:
+ //out << "to_fp_bv "
+ out << "to_fp "
+ << n.getOperator().getConst<FloatingPointToFPIEEEBitVector>().t.exponent() << ' '
+ << n.getOperator().getConst<FloatingPointToFPIEEEBitVector>().t.significand();
+ break;
+ case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT:
+ //out << "to_fp_fp "
+ out << "to_fp "
+ << n.getOperator().getConst<FloatingPointToFPFloatingPoint>().t.exponent() << ' '
+ << n.getOperator().getConst<FloatingPointToFPFloatingPoint>().t.significand();
+ break;
+ case kind::FLOATINGPOINT_TO_FP_REAL:
+ //out << "to_fp_real "
+ out << "to_fp "
+ << n.getOperator().getConst<FloatingPointToFPReal>().t.exponent() << ' '
+ << n.getOperator().getConst<FloatingPointToFPReal>().t.significand();
+ break;
+ case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR:
+ //out << "to_fp_signed "
+ out << "to_fp "
+ << n.getOperator().getConst<FloatingPointToFPSignedBitVector>().t.exponent() << ' '
+ << n.getOperator().getConst<FloatingPointToFPSignedBitVector>().t.significand();
+ break;
+ case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR:
+ out << "to_fp_unsigned "
+ << n.getOperator().getConst<FloatingPointToFPUnsignedBitVector>().t.exponent() << ' '
+ << n.getOperator().getConst<FloatingPointToFPUnsignedBitVector>().t.significand();
+ break;
+ case kind::FLOATINGPOINT_TO_FP_GENERIC:
+ out << "to_fp "
+ << n.getOperator().getConst<FloatingPointToFPGeneric>().t.exponent() << ' '
+ << n.getOperator().getConst<FloatingPointToFPGeneric>().t.significand();
+ break;
+ case kind::FLOATINGPOINT_TO_UBV:
+ out << "fp.to_ubv "
+ << n.getOperator().getConst<FloatingPointToUBV>().bvs.size;
+ break;
+ case kind::FLOATINGPOINT_TO_SBV:
+ out << "fp.to_sbv "
+ << n.getOperator().getConst<FloatingPointToSBV>().bvs.size;
+ break;
+ default:
+ out << n.getKind();
+ }
+ out << ")";
+}
+
+
template <class T>
static bool tryToStream(std::ostream& out, const Command* c) throw();
template <class T>
k != kind::TUPLE_UPDATE &&
k != kind::RECORD_SELECT &&
k != kind::RECORD_UPDATE &&
- k != kind::DIVISIBLE) {
+ k != kind::DIVISIBLE &&
+ // Theory parametric functions go here
+ k != kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR &&
+ k != kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT &&
+ k != kind::FLOATINGPOINT_TO_FP_REAL &&
+ k != kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR &&
+ k != kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR &&
+ k != kind::FLOATINGPOINT_TO_UBV &&
+ k != kind::FLOATINGPOINT_TO_SBV &&
+ k != kind::FLOATINGPOINT_TO_REAL
+ ) {
Debug("bt") << "rewriting: " << top.getOperator() << endl;
result.top() << rewriteBooleanTermsRec(top.getOperator(), theory::THEORY_BUILTIN, quantBoolVars);
Debug("bt") << "got: " << result.top().getOperator() << endl;
--- /dev/null
+# kinds -*- sh -*-
+#
+# For documentation on this file format, please refer to
+# src/theory/builtin/kinds.
+#
+
+theory THEORY_FP ::CVC4::theory::fp::TheoryFp "theory/fp/theory_fp.h"
+typechecker "theory/fp/theory_fp_type_rules.h"
+rewriter ::CVC4::theory::fp::TheoryFpRewriter "theory/fp/theory_fp_rewriter.h"
+
+properties check
+
+# Theory content goes here.
+
+# constants...
+constant CONST_FLOATINGPOINT \
+ ::CVC4::FloatingPoint \
+ ::CVC4::FloatingPointHashFunction \
+ "util/floatingpoint.h" \
+ "a floating-point literal"
+typerule CONST_FLOATINGPOINT ::CVC4::theory::fp::FloatingPointConstantTypeRule
+
+
+constant CONST_ROUNDINGMODE \
+ ::CVC4::RoundingMode \
+ ::CVC4::RoundingModeHashFunction \
+ "util/floatingpoint.h" \
+ "a floating-point rounding mode"
+typerule CONST_ROUNDINGMODE ::CVC4::theory::fp::RoundingModeConstantTypeRule
+
+
+
+# types...
+sort ROUNDINGMODE_TYPE \
+ 5 \
+ well-founded \
+ "NodeManager::currentNM()->mkConst<RoundingMode>(RoundingMode())" \
+ "expr/node_manager.h" \
+ "floating-point rounding mode"
+
+constant FLOATINGPOINT_TYPE \
+ ::CVC4::FloatingPointSize \
+ ::CVC4::FloatingPointSizeHashFunction \
+ "util/floatingpoint.h" \
+ "floating-point type"
+#cardinality FLOATINGPOINT_TYPE "function" "header"
+#enumerator FLOATINGPOINT_TYPE "function" "header"
+#well-founded FLOATINGPOINT_TYPE true "function" "header"
+
+
+# operators...
+operator FLOATINGPOINT_FP 3 "construct a floating-point literal from bit vectors"
+typerule FLOATINGPOINT_FP ::CVC4::theory::fp::FloatingPointFPTypeRule
+
+
+
+operator FLOATINGPOINT_EQ 2: "floating-point equality"
+typerule FLOATINGPOINT_EQ ::CVC4::theory::fp::FloatingPointTestTypeRule
+
+operator FLOATINGPOINT_ABS 1 "floating-point absolute value"
+typerule FLOATINGPOINT_ABS ::CVC4::theory::fp::FloatingPointOperationTypeRule
+
+operator FLOATINGPOINT_NEG 1 "floating-point negation"
+typerule FLOATINGPOINT_NEG ::CVC4::theory::fp::FloatingPointOperationTypeRule
+
+operator FLOATINGPOINT_PLUS 3 "floating-point addition"
+typerule FLOATINGPOINT_PLUS ::CVC4::theory::fp::FloatingPointRoundingOperationTypeRule
+
+operator FLOATINGPOINT_SUB 3 "floating-point sutraction"
+typerule FLOATINGPOINT_SUB ::CVC4::theory::fp::FloatingPointRoundingOperationTypeRule
+
+operator FLOATINGPOINT_MULT 3 "floating-point multiply"
+typerule FLOATINGPOINT_MULT ::CVC4::theory::fp::FloatingPointRoundingOperationTypeRule
+
+operator FLOATINGPOINT_DIV 3 "floating-point division"
+typerule FLOATINGPOINT_DIV ::CVC4::theory::fp::FloatingPointRoundingOperationTypeRule
+
+operator FLOATINGPOINT_FMA 4 "floating-point fused multiply and add"
+typerule FLOATINGPOINT_FMA ::CVC4::theory::fp::FloatingPointRoundingOperationTypeRule
+
+operator FLOATINGPOINT_SQRT 2 "floating-point square root"
+typerule FLOATINGPOINT_SQRT ::CVC4::theory::fp::FloatingPointRoundingOperationTypeRule
+
+operator FLOATINGPOINT_REM 2 "floating-point remainder"
+typerule FLOATINGPOINT_REM ::CVC4::theory::fp::FloatingPointOperationTypeRule
+
+operator FLOATINGPOINT_RTI 2 "floating-point round to integral"
+typerule FLOATINGPOINT_RTI ::CVC4::theory::fp::FloatingPointRoundingOperationTypeRule
+
+operator FLOATINGPOINT_MIN 2 "floating-point minimum"
+typerule FLOATINGPOINT_MIN ::CVC4::theory::fp::FloatingPointOperationTypeRule
+
+operator FLOATINGPOINT_MAX 2 "floating-point maximum"
+typerule FLOATINGPOINT_MAX ::CVC4::theory::fp::FloatingPointOperationTypeRule
+
+
+operator FLOATINGPOINT_LEQ 2 "floating-point less than or equal"
+typerule FLOATINGPOINT_LEQ ::CVC4::theory::fp::FloatingPointTestTypeRule
+
+operator FLOATINGPOINT_LT 2 "floating-point less than"
+typerule FLOATINGPOINT_LT ::CVC4::theory::fp::FloatingPointTestTypeRule
+
+operator FLOATINGPOINT_GEQ 2 "floating-point greater than or equal"
+typerule FLOATINGPOINT_GEQ ::CVC4::theory::fp::FloatingPointTestTypeRule
+
+operator FLOATINGPOINT_GT 2 "floating-point greater than"
+typerule FLOATINGPOINT_GT ::CVC4::theory::fp::FloatingPointTestTypeRule
+
+
+
+operator FLOATINGPOINT_ISN 1 "floating-point is normal"
+typerule FLOATINGPOINT_ISN ::CVC4::theory::fp::FloatingPointTestTypeRule
+
+operator FLOATINGPOINT_ISSN 1 "floating-point is sub-normal"
+typerule FLOATINGPOINT_ISSN ::CVC4::theory::fp::FloatingPointTestTypeRule
+
+operator FLOATINGPOINT_ISZ 1 "floating-point is zero"
+typerule FLOATINGPOINT_ISZ ::CVC4::theory::fp::FloatingPointTestTypeRule
+
+operator FLOATINGPOINT_ISINF 1 "floating-point is infinite"
+typerule FLOATINGPOINT_ISINF ::CVC4::theory::fp::FloatingPointTestTypeRule
+
+operator FLOATINGPOINT_ISNAN 1 "floating-point is NaN"
+typerule FLOATINGPOINT_ISNAN ::CVC4::theory::fp::FloatingPointTestTypeRule
+
+operator FLOATINGPOINT_ISNEG 1 "floating-point is negative"
+typerule FLOATINGPOINT_ISNEG ::CVC4::theory::fp::FloatingPointTestTypeRule
+
+operator FLOATINGPOINT_ISPOS 1 "floating-point is positive"
+typerule FLOATINGPOINT_ISPOS ::CVC4::theory::fp::FloatingPointTestTypeRule
+
+
+
+constant FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP \
+ ::CVC4::FloatingPointToFPIEEEBitVector \
+ "::CVC4::FloatingPointConvertSortHashFunction<0x1>" \
+ "util/floatingpoint.h" \
+ "operator for to_fp from bit vector"
+typerule FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP ::CVC4::theory::fp::FloatingPointParametricOpTypeRule
+
+parameterized FLOATINGPOINT_TO_FP_IEEE_BITVECTOR FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP 1 "convert an IEEE-754 bit vector to floating-point"
+typerule FLOATINGPOINT_TO_FP_IEEE_BITVECTOR ::CVC4::theory::fp::FloatingPointToFPIEEEBitVectorTypeRule
+
+
+
+constant FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP \
+ ::CVC4::FloatingPointToFPFloatingPoint \
+ "::CVC4::FloatingPointConvertSortHashFunction<0x2>" \
+ "util/floatingpoint.h" \
+ "operator for to_fp from floating point"
+typerule FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP ::CVC4::theory::fp::FloatingPointParametricOpTypeRule
+
+parameterized FLOATINGPOINT_TO_FP_FLOATINGPOINT FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP 2 "convert between floating-point sorts"
+typerule FLOATINGPOINT_TO_FP_FLOATINGPOINT ::CVC4::theory::fp::FloatingPointToFPFloatingPointTypeRule
+
+
+
+
+constant FLOATINGPOINT_TO_FP_REAL_OP \
+ ::CVC4::FloatingPointToFPReal \
+ "::CVC4::FloatingPointConvertSortHashFunction<0x4>" \
+ "util/floatingpoint.h" \
+ "operator for to_fp from real"
+typerule FLOATINGPOINT_TO_FP_REAL_OP ::CVC4::theory::fp::FloatingPointParametricOpTypeRule
+
+parameterized FLOATINGPOINT_TO_FP_REAL FLOATINGPOINT_TO_FP_REAL_OP 2 "convert a real to floating-point"
+typerule FLOATINGPOINT_TO_FP_REAL ::CVC4::theory::fp::FloatingPointToFPRealTypeRule
+
+
+
+constant FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP \
+ ::CVC4::FloatingPointToFPSignedBitVector \
+ "::CVC4::FloatingPointConvertSortHashFunction<0x8>" \
+ "util/floatingpoint.h" \
+ "operator for to_fp from signed bit vector"
+typerule FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP ::CVC4::theory::fp::FloatingPointParametricOpTypeRule
+
+parameterized FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP 2 "convert a signed bit vector to floating-point"
+typerule FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR ::CVC4::theory::fp::FloatingPointToFPSignedBitVectorTypeRule
+
+
+
+constant FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP \
+ ::CVC4::FloatingPointToFPUnsignedBitVector \
+ "::CVC4::FloatingPointConvertSortHashFunction<0x10>" \
+ "util/floatingpoint.h" \
+ "operator for to_fp from unsigned bit vector"
+typerule FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP ::CVC4::theory::fp::FloatingPointParametricOpTypeRule
+
+
+parameterized FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP 2 "convert an unsigned bit vector to floating-point"
+typerule FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR ::CVC4::theory::fp::FloatingPointToFPUnsignedBitVectorTypeRule
+
+
+
+constant FLOATINGPOINT_TO_FP_GENERIC_OP \
+ ::CVC4::FloatingPointToFPGeneric \
+ "::CVC4::FloatingPointConvertSortHashFunction<0x11>" \
+ "util/floatingpoint.h" \
+ "operator for a generic to_fp"
+typerule FLOATINGPOINT_TO_FP_GENERIC_OP ::CVC4::theory::fp::FloatingPointParametricOpTypeRule
+
+
+parameterized FLOATINGPOINT_TO_FP_GENERIC FLOATINGPOINT_TO_FP_GENERIC_OP 1:2 "a generic conversion to floating-point, used in parsing only"
+typerule FLOATINGPOINT_TO_FP_GENERIC ::CVC4::theory::fp::FloatingPointToFPGenericTypeRule
+
+
+
+
+
+constant FLOATINGPOINT_TO_UBV_OP \
+ ::CVC4::FloatingPointToUBV \
+ "::CVC4::FloatingPointToBVHashFunction<0x1>" \
+ "util/floatingpoint.h" \
+ "operator for to_ubv"
+typerule FLOATINGPOINT_TO_UBV_OP ::CVC4::theory::fp::FloatingPointParametricOpTypeRule
+
+parameterized FLOATINGPOINT_TO_UBV FLOATINGPOINT_TO_UBV_OP 2 "convert a floating-point value to an unsigned bit vector"
+typerule FLOATINGPOINT_TO_UBV ::CVC4::theory::fp::FloatingPointToUBVTypeRule
+
+
+
+constant FLOATINGPOINT_TO_SBV_OP \
+ ::CVC4::FloatingPointToSBV \
+ "::CVC4::FloatingPointToBVHashFunction<0x2>" \
+ "util/floatingpoint.h" \
+ "operator for to_sbv"
+typerule FLOATINGPOINT_TO_SBV_OP ::CVC4::theory::fp::FloatingPointParametricOpTypeRule
+
+parameterized FLOATINGPOINT_TO_SBV FLOATINGPOINT_TO_SBV_OP 2 "convert a floating-point value to a signed bit vector"
+typerule FLOATINGPOINT_TO_SBV ::CVC4::theory::fp::FloatingPointToSBVTypeRule
+
+
+operator FLOATINGPOINT_TO_REAL 1 "floating-point to real"
+typerule FLOATINGPOINT_TO_REAL ::CVC4::theory::fp::FloatingPointToRealTypeRule
+
+
+endtheory
--- /dev/null
+#
+# Option specification file for CVC4
+# See src/options/base_options for a description of this file format
+#
+
+module FP "theory/fp/options.h" Fp
+
+endmodule
--- /dev/null
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__FP__OPTIONS_HANDLERS_H
+#define __CVC4__THEORY__FP__OPTIONS_HANDLERS_H
+
+namespace CVC4 {
+namespace theory {
+namespace fp {
+
+}/* CVC4::theory::fp namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__FP__OPTIONS_HANDLERS_H */
--- /dev/null
+#include "theory/fp/theory_fp.h"
+
+using namespace std;
+
+namespace CVC4 {
+namespace theory {
+namespace fp {
+
+namespace removeToFPGeneric {
+
+ Node removeToFPGeneric (TNode node) {
+ Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_GENERIC);
+
+ FloatingPointToFPGeneric info = node.getOperator().getConst<FloatingPointToFPGeneric>();
+
+ size_t children = node.getNumChildren();
+
+ Node op;
+
+ if (children == 1) {
+ op = NodeManager::currentNM()->mkConst(FloatingPointToFPIEEEBitVector(info.t.exponent(),
+ info.t.significand()));
+ return NodeManager::currentNM()->mkNode(op, node[0]);
+
+ } else {
+ Assert(children == 2);
+ Assert(node[0].getType().isRoundingMode());
+
+ TypeNode t = node[1].getType();
+
+ if (t.isFloatingPoint()) {
+ op = NodeManager::currentNM()->mkConst(FloatingPointToFPFloatingPoint(info.t.exponent(),
+ info.t.significand()));
+ } else if (t.isReal()) {
+ op = NodeManager::currentNM()->mkConst(FloatingPointToFPReal(info.t.exponent(),
+ info.t.significand()));
+ } else if (t.isBitVector()) {
+ op = NodeManager::currentNM()->mkConst(FloatingPointToFPSignedBitVector(info.t.exponent(),
+ info.t.significand()));
+
+ } else {
+ throw TypeCheckingExceptionPrivate(node, "cannot rewrite to_fp generic due to incorrect type of second argument");
+ }
+
+ return NodeManager::currentNM()->mkNode(op, node[0], node[1]);
+ }
+
+ Unreachable("to_fp generic not rewritten");
+ }
+}
+
+
+/** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */
+TheoryFp::TheoryFp(context::Context* c,
+ context::UserContext* u,
+ OutputChannel& out,
+ Valuation valuation,
+ const LogicInfo& logicInfo) :
+ Theory(THEORY_FP, c, u, out, valuation, logicInfo) {
+}/* TheoryFp::TheoryFp() */
+
+
+Node TheoryFp::expandDefinition(LogicRequest &, Node node) {
+ Trace("fp-expandDefinition") << "TheoryFp::expandDefinition(): " << node << std::endl;
+
+ if (node.getKind() == kind::FLOATINGPOINT_TO_FP_GENERIC) {
+ Node res(removeToFPGeneric::removeToFPGeneric(node));
+
+ Trace("fp-expandDefinition") << "TO_FP_GENERIC rewritten to " << res << std::endl;
+
+ return res;
+ } else {
+ return node;
+ }
+}
+
+
+void TheoryFp::check(Effort level) {
+ if (done() && !fullEffort(level)) {
+ return;
+ }
+
+ while(!done()) {
+ // Get all the assertions
+ Assertion assertion = get();
+ TNode fact = assertion.assertion;
+
+ Debug("fp") << "TheoryFp::check(): processing " << fact << std::endl;
+
+ // Do the work
+ switch(fact.getKind()) {
+
+ /* cases for all the theory's kinds go here... */
+
+ default:
+ Unhandled(fact.getKind());
+ }
+ }
+
+}/* TheoryFp::check() */
+
+}/* CVC4::theory::fp namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
--- /dev/null
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__FP__THEORY_FP_H
+#define __CVC4__THEORY__FP__THEORY_FP_H
+
+#include "theory/theory.h"
+
+namespace CVC4 {
+namespace theory {
+namespace fp {
+
+class TheoryFp : public Theory {
+public:
+
+ /** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */
+ TheoryFp(context::Context* c,
+ context::UserContext* u,
+ OutputChannel& out,
+ Valuation valuation,
+ const LogicInfo& logicInfo);
+
+ Node expandDefinition(LogicRequest &, Node node);
+
+ void check(Effort);
+
+ std::string identify() const {
+ return "THEORY_FP";
+ }
+
+};/* class TheoryFp */
+
+}/* CVC4::theory::fp namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__FP__THEORY_FP_H */
--- /dev/null
+/********************* */
+/*! \file theory_fp_rewriter.cpp
+ ** \verbatim
+ ** Original author: Martin Brain
+ ** Major contributors:
+ ** Minor contributors (to current version):
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2013 University of Oxford
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Rewrite rules for floating point theories. ]]
+ **
+ ** \todo [[ Constant folding
+ ** Push negations up through arithmetic operators (include max and min? maybe not due to +0/-0)
+ ** classifications to normal tests (maybe)
+ ** (= x (fp.neg x)) --> (isNaN x)
+ ** (fp.eq x (fp.neg x)) --> (isZero x) (previous and reorganise should be sufficient)
+ ** (fp.eq x const) --> various = depending on const
+ ** (fp.abs (fp.neg x)) --> (fp.abs x)
+ ** (fp.isPositive (fp.neg x)) --> (fp.isNegative x)
+ ** (fp.isNegative (fp.neg x)) --> (fp.isPositive x)
+ ** (fp.isPositive (fp.abs x)) --> (not (isNaN x))
+ ** (fp.isNegative (fp.abs x)) --> false
+ ** ]]
+ **/
+
+#include "theory/fp/theory_fp_rewriter.h"
+
+#include "util/cvc4_assert.h"
+
+#include <algorithm>
+
+namespace CVC4 {
+namespace theory {
+namespace fp {
+
+namespace rewrite {
+ /** Rewrite rules **/
+
+ RewriteResponse notFP (TNode node, bool) {
+ Unreachable("non floating-point kind (%d) in floating point rewrite?",node.getKind());
+ }
+
+ RewriteResponse identity (TNode node, bool) {
+ return RewriteResponse(REWRITE_DONE, node);
+ }
+
+ RewriteResponse type (TNode node, bool) {
+ Unreachable("sort kind (%d) found in expression?",node.getKind());
+ return RewriteResponse(REWRITE_DONE, node);
+ }
+
+ RewriteResponse removeDoubleNegation (TNode node, bool) {
+ Assert(node.getKind() == kind::FLOATINGPOINT_NEG);
+ if (node[0].getKind() == kind::FLOATINGPOINT_NEG) {
+ RewriteResponse(REWRITE_AGAIN, node[0][0]);
+ }
+
+ return RewriteResponse(REWRITE_DONE, node);
+ }
+
+ RewriteResponse convertSubtractionToAddition (TNode node, bool) {
+ Assert(node.getKind() == kind::FLOATINGPOINT_SUB);
+ Node negation = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_NEG,node[2]);
+ Node addition = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_PLUS,node[0],node[1],negation);
+ return RewriteResponse(REWRITE_DONE, addition);
+ }
+
+
+ /* Implies (fp.eq x x) --> (not (isNaN x))
+ */
+
+ RewriteResponse ieeeEqToEq (TNode node, bool) {
+ Assert(node.getKind() == kind::FLOATINGPOINT_EQ);
+ NodeManager *nm = NodeManager::currentNM();
+
+ return RewriteResponse(REWRITE_DONE,
+ nm->mkNode(kind::AND,
+ nm->mkNode(kind::AND,
+ nm->mkNode(kind::NOT, nm->mkNode(kind::FLOATINGPOINT_ISNAN, node[0])),
+ nm->mkNode(kind::NOT, nm->mkNode(kind::FLOATINGPOINT_ISNAN, node[1]))),
+ nm->mkNode(kind::OR,
+ nm->mkNode(kind::EQUAL, node[0], node[1]),
+ nm->mkNode(kind::AND,
+ nm->mkNode(kind::FLOATINGPOINT_ISZ, node[0]),
+ nm->mkNode(kind::FLOATINGPOINT_ISZ, node[1])))));
+ }
+
+
+ RewriteResponse geqToleq (TNode node, bool) {
+ Assert(node.getKind() == kind::FLOATINGPOINT_GEQ);
+ return RewriteResponse(REWRITE_DONE,NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_LEQ,node[1],node[0]));
+ }
+
+ RewriteResponse gtTolt (TNode node, bool) {
+ Assert(node.getKind() == kind::FLOATINGPOINT_GT);
+ return RewriteResponse(REWRITE_DONE,NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_LT,node[1],node[0]));
+ }
+
+ RewriteResponse removed (TNode node, bool) {
+ Unreachable("kind (%d) should have been removed?",node.getKind());
+ return RewriteResponse(REWRITE_DONE, node);
+ }
+
+ RewriteResponse variable (TNode node, bool) {
+ // We should only get floating point and rounding mode variables to rewrite.
+ TypeNode tn = node.getType(true);
+ Assert(tn.isFloatingPoint() || tn.isRoundingMode());
+
+ // Not that we do anything with them...
+ return RewriteResponse(REWRITE_DONE, node);
+ }
+
+ RewriteResponse equal (TNode node, bool isPreRewrite) {
+ // We should only get equalities of floating point or rounding mode types.
+ Assert(node.getKind() == kind::EQUAL);
+
+ TypeNode tn = node[0].getType(true);
+
+ Assert(tn.isFloatingPoint() || tn.isRoundingMode());
+ Assert(tn == node[1].getType(true)); // Should be ensured by the typing rules
+
+ if (node[0] == node[1]) {
+ return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
+ } else if (!isPreRewrite && (node[0] > node[1])) {
+ Node normal = NodeManager::currentNM()->mkNode(kind::EQUAL,node[1],node[0]);
+ return RewriteResponse(REWRITE_DONE, normal);
+ } else {
+ return RewriteResponse(REWRITE_DONE, node);
+ }
+ }
+
+ RewriteResponse convertFromRealLiteral (TNode node, bool) {
+ Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_REAL);
+
+ // \todo Honour the rounding mode and work for something other than doubles!
+
+ if (node[1].getKind() == kind::CONST_RATIONAL) {
+ TNode op = node.getOperator();
+ const FloatingPointToFPReal ¶m = op.getConst<FloatingPointToFPReal>();
+ Node lit =
+ NodeManager::currentNM()->mkConst(FloatingPoint(param.t.exponent(),
+ param.t.significand(),
+ node[1].getConst<Rational>().getDouble()));
+
+ return RewriteResponse(REWRITE_DONE, lit);
+ } else {
+ return RewriteResponse(REWRITE_DONE, node);
+ }
+ }
+
+ RewriteResponse convertFromIEEEBitVectorLiteral (TNode node, bool) {
+ Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR);
+
+ // \todo Handle arbitrary length bit vectors without using strings!
+
+ if (node[0].getKind() == kind::CONST_BITVECTOR) {
+ TNode op = node.getOperator();
+ const FloatingPointToFPIEEEBitVector ¶m = op.getConst<FloatingPointToFPIEEEBitVector>();
+ const BitVector &bv = node[0].getConst<BitVector>();
+ std::string bitString(bv.toString());
+
+ Node lit =
+ NodeManager::currentNM()->mkConst(FloatingPoint(param.t.exponent(),
+ param.t.significand(),
+ bitString));
+
+ return RewriteResponse(REWRITE_DONE, lit);
+ } else {
+ return RewriteResponse(REWRITE_DONE, node);
+ }
+ }
+
+ RewriteResponse convertFromLiteral (TNode node, bool) {
+ Assert(node.getKind() == kind::FLOATINGPOINT_FP);
+
+ // \todo Handle arbitrary length bit vectors without using strings!
+
+ if ((node[0].getKind() == kind::CONST_BITVECTOR) &&
+ (node[1].getKind() == kind::CONST_BITVECTOR) &&
+ (node[2].getKind() == kind::CONST_BITVECTOR)) {
+
+ BitVector bv(node[0].getConst<BitVector>());
+ bv = bv.concat(node[1].getConst<BitVector>());
+ bv = bv.concat(node[2].getConst<BitVector>());
+
+ std::string bitString(bv.toString());
+ std::reverse(bitString.begin(), bitString.end());
+
+ // +1 to support the hidden bit
+ Node lit =
+ NodeManager::currentNM()->mkConst(FloatingPoint(node[1].getConst<BitVector>().getSize(),
+ node[2].getConst<BitVector>().getSize() + 1,
+ bitString));
+
+ return RewriteResponse(REWRITE_DONE, lit);
+ } else {
+ return RewriteResponse(REWRITE_DONE, node);
+ }
+ }
+
+ // Note these cannot be assumed to be symmetric for +0/-0, thus no symmetry reorder
+ RewriteResponse compactMinMax (TNode node, bool isPreRewrite) {
+ Kind k = node.getKind();
+
+ Assert((k == kind::FLOATINGPOINT_MIN) || (k == kind::FLOATINGPOINT_MAX));
+
+ if (node[0] == node[1]) {
+ return RewriteResponse(REWRITE_DONE, node[0]);
+ } else {
+ return RewriteResponse(REWRITE_DONE, node);
+ }
+ }
+
+
+ RewriteResponse reorderFPEquality (TNode node, bool isPreRewrite) {
+ Assert(node.getKind() == kind::FLOATINGPOINT_EQ);
+ Assert(!isPreRewrite); // Likely redundant in pre-rewrite
+
+ if (node[0] > node[1]) {
+ Node normal = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_EQ,node[1],node[0]);
+ return RewriteResponse(REWRITE_DONE, normal);
+ } else {
+ return RewriteResponse(REWRITE_DONE, node);
+ }
+ }
+
+ RewriteResponse reorderBinaryOperation (TNode node, bool isPreRewrite) {
+ Kind k = node.getKind();
+ Assert((k == kind::FLOATINGPOINT_PLUS) || (k == kind::FLOATINGPOINT_MULT));
+ Assert(!isPreRewrite); // Likely redundant in pre-rewrite
+
+ if (node[1] > node[2]) {
+ Node normal = NodeManager::currentNM()->mkNode(k,node[0],node[2],node[1]);
+ return RewriteResponse(REWRITE_DONE, normal);
+ } else {
+ return RewriteResponse(REWRITE_DONE, node);
+ }
+ }
+
+ RewriteResponse reorderFMA (TNode node, bool isPreRewrite) {
+ Assert(node.getKind() == kind::FLOATINGPOINT_FMA);
+ Assert(!isPreRewrite); // Likely redundant in pre-rewrite
+
+ if (node[1] > node[2]) {
+ Node normal = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_FMA,node[0],node[2],node[1],node[3]);
+ return RewriteResponse(REWRITE_DONE, normal);
+ } else {
+ return RewriteResponse(REWRITE_DONE, node);
+ }
+ }
+
+ RewriteResponse removeSignOperations (TNode node, bool isPreRewrite) {
+ Assert(node.getKind() == kind::FLOATINGPOINT_ISN ||
+ node.getKind() == kind::FLOATINGPOINT_ISSN ||
+ node.getKind() == kind::FLOATINGPOINT_ISZ ||
+ node.getKind() == kind::FLOATINGPOINT_ISINF ||
+ node.getKind() == kind::FLOATINGPOINT_ISNAN);
+ Assert(node.getNumChildren() == 1);
+
+ Kind childKind(node[0].getKind());
+
+ if ((childKind == kind::FLOATINGPOINT_NEG) ||
+ (childKind == kind::FLOATINGPOINT_ABS)) {
+
+ Node rewritten = NodeManager::currentNM()->mkNode(node.getKind(),node[0][0]);
+ return RewriteResponse(REWRITE_AGAIN, rewritten);
+ } else {
+ return RewriteResponse(REWRITE_DONE, node);
+ }
+ }
+
+
+}; /* CVC4::theory::fp::rewrite */
+
+RewriteFunction TheoryFpRewriter::preRewriteTable[kind::LAST_KIND];
+RewriteFunction TheoryFpRewriter::postRewriteTable[kind::LAST_KIND];
+
+
+ /**
+ * Initialize the rewriter.
+ */
+ void TheoryFpRewriter::init() {
+
+ /* Set up the pre-rewrite dispatch table */
+ for (unsigned i = 0; i < kind::LAST_KIND; ++i) {
+ preRewriteTable[i] = rewrite::notFP;
+ }
+
+ /******** Constants ********/
+ /* No rewriting possible for constants */
+ preRewriteTable[kind::CONST_FLOATINGPOINT] = rewrite::identity;
+ preRewriteTable[kind::CONST_ROUNDINGMODE] = rewrite::identity;
+
+ /******** Sorts(?) ********/
+ /* These kinds should only appear in types */
+ //preRewriteTable[kind::ROUNDINGMODE_TYPE] = rewrite::type;
+ preRewriteTable[kind::FLOATINGPOINT_TYPE] = rewrite::type;
+
+ /******** Operations ********/
+ preRewriteTable[kind::FLOATINGPOINT_FP] = rewrite::identity;
+ preRewriteTable[kind::FLOATINGPOINT_ABS] = rewrite::identity;
+ preRewriteTable[kind::FLOATINGPOINT_NEG] = rewrite::removeDoubleNegation;
+ preRewriteTable[kind::FLOATINGPOINT_PLUS] = rewrite::identity;
+ preRewriteTable[kind::FLOATINGPOINT_SUB] = rewrite::convertSubtractionToAddition;
+ preRewriteTable[kind::FLOATINGPOINT_MULT] = rewrite::identity;
+ preRewriteTable[kind::FLOATINGPOINT_DIV] = rewrite::identity;
+ preRewriteTable[kind::FLOATINGPOINT_FMA] = rewrite::identity;
+ preRewriteTable[kind::FLOATINGPOINT_SQRT] = rewrite::identity;
+ preRewriteTable[kind::FLOATINGPOINT_REM] = rewrite::identity;
+ preRewriteTable[kind::FLOATINGPOINT_RTI] = rewrite::identity;
+ preRewriteTable[kind::FLOATINGPOINT_MIN] = rewrite::compactMinMax;
+ preRewriteTable[kind::FLOATINGPOINT_MAX] = rewrite::compactMinMax;
+
+ /******** Comparisons ********/
+ preRewriteTable[kind::FLOATINGPOINT_EQ] = rewrite::ieeeEqToEq;
+ preRewriteTable[kind::FLOATINGPOINT_LEQ] = rewrite::identity;
+ preRewriteTable[kind::FLOATINGPOINT_LT] = rewrite::identity;
+ preRewriteTable[kind::FLOATINGPOINT_GEQ] = rewrite::geqToleq;
+ preRewriteTable[kind::FLOATINGPOINT_GT] = rewrite::gtTolt;
+
+ /******** Classifications ********/
+ preRewriteTable[kind::FLOATINGPOINT_ISN] = rewrite::identity;
+ preRewriteTable[kind::FLOATINGPOINT_ISSN] = rewrite::identity;
+ preRewriteTable[kind::FLOATINGPOINT_ISZ] = rewrite::identity;
+ preRewriteTable[kind::FLOATINGPOINT_ISINF] = rewrite::identity;
+ preRewriteTable[kind::FLOATINGPOINT_ISNAN] = rewrite::identity;
+ preRewriteTable[kind::FLOATINGPOINT_ISNEG] = rewrite::identity;
+ preRewriteTable[kind::FLOATINGPOINT_ISPOS] = rewrite::identity;
+
+ /******** Conversions ********/
+ preRewriteTable[kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR] = rewrite::identity;
+ preRewriteTable[kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT] = rewrite::identity;
+ preRewriteTable[kind::FLOATINGPOINT_TO_FP_REAL] = rewrite::identity;
+ preRewriteTable[kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR] = rewrite::identity;
+ preRewriteTable[kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR] = rewrite::identity;
+ preRewriteTable[kind::FLOATINGPOINT_TO_FP_GENERIC] = rewrite::removed;
+ preRewriteTable[kind::FLOATINGPOINT_TO_UBV] = rewrite::identity;
+ preRewriteTable[kind::FLOATINGPOINT_TO_SBV] = rewrite::identity;
+ preRewriteTable[kind::FLOATINGPOINT_TO_REAL] = rewrite::identity;
+
+ /******** Variables ********/
+ preRewriteTable[kind::VARIABLE] = rewrite::variable;
+ preRewriteTable[kind::BOUND_VARIABLE] = rewrite::variable;
+
+ preRewriteTable[kind::EQUAL] = rewrite::equal;
+
+
+
+
+ /* Set up the post-rewrite dispatch table */
+ for (unsigned i = 0; i < kind::LAST_KIND; ++i) {
+ postRewriteTable[i] = rewrite::notFP;
+ }
+
+ /******** Constants ********/
+ /* No rewriting possible for constants */
+ postRewriteTable[kind::CONST_FLOATINGPOINT] = rewrite::identity;
+ postRewriteTable[kind::CONST_ROUNDINGMODE] = rewrite::identity;
+
+ /******** Sorts(?) ********/
+ /* These kinds should only appear in types */
+ //postRewriteTable[kind::ROUNDINGMODE_TYPE] = rewrite::type;
+ postRewriteTable[kind::FLOATINGPOINT_TYPE] = rewrite::type;
+
+ /******** Operations ********/
+ postRewriteTable[kind::FLOATINGPOINT_FP] = rewrite::convertFromLiteral;
+ postRewriteTable[kind::FLOATINGPOINT_ABS] = rewrite::identity;
+ postRewriteTable[kind::FLOATINGPOINT_NEG] = rewrite::removeDoubleNegation;
+ postRewriteTable[kind::FLOATINGPOINT_PLUS] = rewrite::reorderBinaryOperation;
+ postRewriteTable[kind::FLOATINGPOINT_SUB] = rewrite::removed;
+ postRewriteTable[kind::FLOATINGPOINT_MULT] = rewrite::reorderBinaryOperation;
+ postRewriteTable[kind::FLOATINGPOINT_DIV] = rewrite::identity;
+ postRewriteTable[kind::FLOATINGPOINT_FMA] = rewrite::reorderFMA;
+ postRewriteTable[kind::FLOATINGPOINT_SQRT] = rewrite::identity;
+ postRewriteTable[kind::FLOATINGPOINT_REM] = rewrite::identity;
+ postRewriteTable[kind::FLOATINGPOINT_RTI] = rewrite::identity;
+ postRewriteTable[kind::FLOATINGPOINT_MIN] = rewrite::compactMinMax;
+ postRewriteTable[kind::FLOATINGPOINT_MAX] = rewrite::compactMinMax;
+
+ /******** Comparisons ********/
+ postRewriteTable[kind::FLOATINGPOINT_EQ] = rewrite::removed;
+ postRewriteTable[kind::FLOATINGPOINT_LEQ] = rewrite::identity;
+ postRewriteTable[kind::FLOATINGPOINT_LT] = rewrite::identity;
+ postRewriteTable[kind::FLOATINGPOINT_GEQ] = rewrite::removed;
+ postRewriteTable[kind::FLOATINGPOINT_GT] = rewrite::removed;
+
+ /******** Classifications ********/
+ postRewriteTable[kind::FLOATINGPOINT_ISN] = rewrite::removeSignOperations;
+ postRewriteTable[kind::FLOATINGPOINT_ISSN] = rewrite::removeSignOperations;
+ postRewriteTable[kind::FLOATINGPOINT_ISZ] = rewrite::removeSignOperations;
+ postRewriteTable[kind::FLOATINGPOINT_ISINF] = rewrite::removeSignOperations;
+ postRewriteTable[kind::FLOATINGPOINT_ISNAN] = rewrite::removeSignOperations;
+ postRewriteTable[kind::FLOATINGPOINT_ISNEG] = rewrite::identity;
+ postRewriteTable[kind::FLOATINGPOINT_ISPOS] = rewrite::identity;
+
+ /******** Conversions ********/
+ postRewriteTable[kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR] = rewrite::convertFromIEEEBitVectorLiteral;
+ postRewriteTable[kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT] = rewrite::identity;
+ postRewriteTable[kind::FLOATINGPOINT_TO_FP_REAL] = rewrite::convertFromRealLiteral;
+ postRewriteTable[kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR] = rewrite::identity;
+ postRewriteTable[kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR] = rewrite::identity;
+ postRewriteTable[kind::FLOATINGPOINT_TO_FP_GENERIC] = rewrite::removed;
+ postRewriteTable[kind::FLOATINGPOINT_TO_UBV] = rewrite::identity;
+ postRewriteTable[kind::FLOATINGPOINT_TO_SBV] = rewrite::identity;
+ postRewriteTable[kind::FLOATINGPOINT_TO_REAL] = rewrite::identity;
+
+ /******** Variables ********/
+ postRewriteTable[kind::VARIABLE] = rewrite::variable;
+ postRewriteTable[kind::BOUND_VARIABLE] = rewrite::variable;
+
+ postRewriteTable[kind::EQUAL] = rewrite::equal;
+
+
+ }
+
+
+
+
+ /**
+ * Rewrite a node into the normal form for the theory of fp
+ * in pre-order (really topological order)---meaning that the
+ * children may not be in the normal form. This is an optimization
+ * for theories with cancelling terms (e.g., 0 * (big-nasty-expression)
+ * in arithmetic rewrites to 0 without the need to look at the big
+ * nasty expression). Since it's only an optimization, the
+ * implementation here can do nothing.
+ */
+
+ RewriteResponse TheoryFpRewriter::preRewrite(TNode node) {
+ Trace("fp-rewrite") << "TheoryFpRewriter::preRewrite(): " << node << std::endl;
+ RewriteResponse res = preRewriteTable [node.getKind()] (node, true);
+ if (res.node != node) {
+ Debug("fp-rewrite") << "TheoryFpRewriter::preRewrite(): before " << node << std::endl;
+ Debug("fp-rewrite") << "TheoryFpRewriter::preRewrite(): after " << res.node << std::endl;
+ }
+ return res;
+ }
+
+
+ /**
+ * Rewrite a node into the normal form for the theory of fp.
+ * Called in post-order (really reverse-topological order) when
+ * traversing the expression DAG during rewriting. This is the
+ * main function of the rewriter, and because of the ordering,
+ * it can assume its children are all rewritten already.
+ *
+ * This function can return one of three rewrite response codes
+ * along with the rewritten node:
+ *
+ * REWRITE_DONE indicates that no more rewriting is needed.
+ * REWRITE_AGAIN means that the top-level expression should be
+ * rewritten again, but that its children are in final form.
+ * REWRITE_AGAIN_FULL means that the entire returned expression
+ * should be rewritten again (top-down with preRewrite(), then
+ * bottom-up with postRewrite()).
+ *
+ * Even if this function returns REWRITE_DONE, if the returned
+ * expression belongs to a different theory, it will be fully
+ * rewritten by that theory's rewriter.
+ */
+
+ RewriteResponse TheoryFpRewriter::postRewrite(TNode node) {
+ Trace("fp-rewrite") << "TheoryFpRewriter::postRewrite(): " << node << std::endl;
+ RewriteResponse res = postRewriteTable [node.getKind()] (node, false);
+ if (res.node != node) {
+ Debug("fp-rewrite") << "TheoryFpRewriter::postRewrite(): before " << node << std::endl;
+ Debug("fp-rewrite") << "TheoryFpRewriter::postRewrite(): after " << res.node << std::endl;
+ }
+ return res;
+ }
+
+
+}/* CVC4::theory::fp namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
--- /dev/null
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__FP__THEORY_FP_REWRITER_H
+#define __CVC4__THEORY__FP__THEORY_FP_REWRITER_H
+
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+namespace theory {
+namespace fp {
+
+typedef RewriteResponse (*RewriteFunction) (TNode, bool);
+
+class TheoryFpRewriter {
+ protected :
+ static RewriteFunction preRewriteTable[kind::LAST_KIND];
+ static RewriteFunction postRewriteTable[kind::LAST_KIND];
+
+ public:
+
+ static RewriteResponse preRewrite(TNode node);
+ static RewriteResponse postRewrite(TNode node);
+
+
+ /**
+ * Rewrite an equality, in case special handling is required.
+ */
+ static Node rewriteEquality(TNode equality) {
+ // often this will suffice
+ return postRewrite(equality).node;
+ }
+
+ static void init();
+
+ /**
+ * Shut down the rewriter.
+ */
+ static inline void shutdown() {
+ // nothing to do
+ }
+
+};/* class TheoryFpRewriter */
+
+}/* CVC4::theory::fp namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__FP__THEORY_FP_REWRITER_H */
--- /dev/null
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__FP__THEORY_FP_TYPE_RULES_H
+#define __CVC4__THEORY__FP__THEORY_FP_TYPE_RULES_H
+
+namespace CVC4 {
+namespace theory {
+namespace fp {
+
+#define TRACE(FUNCTION) Trace("fp-type") << FUNCTION "::computeType(" << check << "): " << n << std::endl
+
+
+class FloatingPointConstantTypeRule {
+public:
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ TRACE("FloatingPointConstantTypeRule");
+
+ const FloatingPoint &f = n.getConst<FloatingPoint>();
+
+ if (check) {
+ if (!(validExponentSize(f.t.exponent()))) {
+ throw TypeCheckingExceptionPrivate(n, "constant with invalid exponent size");
+ }
+ if (!(validSignificandSize(f.t.significand()))) {
+ throw TypeCheckingExceptionPrivate(n, "constant with invalid significand size");
+ }
+ }
+ return nodeManager->mkFloatingPointType(f.t);
+ }
+};
+
+
+class RoundingModeConstantTypeRule {
+public:
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ TRACE("RoundingModeConstantTypeRule");
+
+ // Nothing to check!
+ return nodeManager->roundingModeType();
+ }
+};
+
+
+
+class FloatingPointFPTypeRule {
+public:
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ TRACE("FloatingPointFPTypeRule");
+
+ TypeNode signType = n[0].getType(check);
+ TypeNode exponentType = n[1].getType(check);
+ TypeNode significandType = n[2].getType(check);
+
+ if (!signType.isBitVector() ||
+ !exponentType.isBitVector() ||
+ !significandType.isBitVector()) {
+ throw TypeCheckingExceptionPrivate(n, "arguments to fp must be bit vectors");
+ }
+
+ unsigned signBits = signType.getBitVectorSize();
+ unsigned exponentBits = exponentType.getBitVectorSize();
+ unsigned significandBits = significandType.getBitVectorSize();
+
+ if (check) {
+
+ if (signBits != 1) {
+ throw TypeCheckingExceptionPrivate(n, "sign bit vector in fp must be 1 bit long");
+ } else if (!(validExponentSize(exponentBits))) {
+ throw TypeCheckingExceptionPrivate(n, "exponent bit vector in fp is an invalid size");
+ } else if (!(validSignificandSize(significandBits))) {
+ throw TypeCheckingExceptionPrivate(n, "significand bit vector in fp is an invalid size");
+ }
+ }
+
+ // The +1 is for the implicit hidden bit
+ return nodeManager->mkFloatingPointType(exponentBits,significandBits + 1);
+ }
+
+};
+
+
+class FloatingPointTestTypeRule {
+public:
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ TRACE("FloatingPointTestTypeRule");
+
+ if (check) {
+ TypeNode firstOperand = n[0].getType(check);
+
+ if (!firstOperand.isFloatingPoint()) {
+ throw TypeCheckingExceptionPrivate(n, "floating-point test applied to a non floating-point sort");
+ }
+
+ size_t children = n.getNumChildren();
+ for (size_t i = 1; i < children; ++i) {
+ if (!(n[i].getType(check) == firstOperand)) {
+ throw TypeCheckingExceptionPrivate(n, "floating-point test applied to mixed sorts");
+ }
+ }
+ }
+
+ return nodeManager->booleanType();
+ }
+};
+
+
+class FloatingPointOperationTypeRule {
+public :
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ TRACE("FloatingPointOperationTypeRule");
+
+ TypeNode firstOperand = n[0].getType(check);
+
+ if (check) {
+ if (!firstOperand.isFloatingPoint()) {
+ throw TypeCheckingExceptionPrivate(n, "floating-point operation applied to a non floating-point sort");
+ }
+
+ size_t children = n.getNumChildren();
+ for (size_t i = 1; i < children; ++i) {
+ if (!(n[i].getType(check) == firstOperand)) {
+ throw TypeCheckingExceptionPrivate(n, "floating-point test applied to mixed sorts");
+ }
+ }
+ }
+
+ return firstOperand;
+ }
+};
+
+
+class FloatingPointRoundingOperationTypeRule {
+public :
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ TRACE("FloatingPointRoundingOperationTypeRule");
+
+ if (check) {
+ TypeNode roundingModeType = n[0].getType(check);
+
+ if (!roundingModeType.isRoundingMode()) {
+ throw TypeCheckingExceptionPrivate(n, "first argument must be a rounding mode");
+ }
+ }
+
+
+ TypeNode firstOperand = n[1].getType(check);
+
+ if (check) {
+ if (!firstOperand.isFloatingPoint()) {
+ throw TypeCheckingExceptionPrivate(n, "floating-point operation applied to a non floating-point sort");
+ }
+
+ size_t children = n.getNumChildren();
+ for (size_t i = 2; i < children; ++i) {
+ if (!(n[i].getType(check) == firstOperand)) {
+ throw TypeCheckingExceptionPrivate(n, "floating-point test applied to mixed sorts");
+ }
+ }
+ }
+
+ return firstOperand;
+ }
+};
+
+class FloatingPointParametricOpTypeRule {
+public :
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ TRACE("FloatingPointParametricOpTypeRule");
+
+ return nodeManager->builtinOperatorType();
+ }
+};
+
+class FloatingPointToFPIEEEBitVectorTypeRule {
+public :
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ TRACE("FloatingPointToFPIEEEBitVectorTypeRule");
+
+ FloatingPointToFPIEEEBitVector info = n.getOperator().getConst<FloatingPointToFPIEEEBitVector>();
+
+ if (check) {
+ TypeNode operandType = n[0].getType(check);
+
+ if (!(operandType.isBitVector())) {
+ throw TypeCheckingExceptionPrivate(n, "conversion to floating-point from bit vector used with sort other than bit vector");
+ } else if (!(operandType.getBitVectorSize() == info.t.exponent() + info.t.significand())) {
+ throw TypeCheckingExceptionPrivate(n, "conversion to floating-point from bit vector used with bit vector length that does not match floating point parameters");
+ }
+ }
+
+ return nodeManager->mkFloatingPointType(info.t);
+ }
+};
+
+
+class FloatingPointToFPFloatingPointTypeRule {
+public :
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ TRACE("FloatingPointToFPFloatingPointTypeRule");
+
+ FloatingPointToFPFloatingPoint info = n.getOperator().getConst<FloatingPointToFPFloatingPoint>();
+
+ if (check) {
+ TypeNode roundingModeType = n[0].getType(check);
+
+ if (!roundingModeType.isRoundingMode()) {
+ throw TypeCheckingExceptionPrivate(n, "first argument must be a rounding mode");
+ }
+
+
+ TypeNode operandType = n[1].getType(check);
+
+ if (!(operandType.isFloatingPoint())) {
+ throw TypeCheckingExceptionPrivate(n, "conversion to floating-point from floating-point used with sort other than floating-point");
+ }
+ }
+
+ return nodeManager->mkFloatingPointType(info.t);
+ }
+};
+
+
+class FloatingPointToFPRealTypeRule {
+public :
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ TRACE("FloatingPointToFPRealTypeRule");
+
+ FloatingPointToFPReal info = n.getOperator().getConst<FloatingPointToFPReal>();
+
+ if (check) {
+ TypeNode roundingModeType = n[0].getType(check);
+
+ if (!roundingModeType.isRoundingMode()) {
+ throw TypeCheckingExceptionPrivate(n, "first argument must be a rounding mode");
+ }
+
+
+ TypeNode operandType = n[1].getType(check);
+
+ if (!(operandType.isReal())) {
+ throw TypeCheckingExceptionPrivate(n, "conversion to floating-point from real used with sort other than real");
+ }
+ }
+
+ return nodeManager->mkFloatingPointType(info.t);
+ }
+};
+
+
+class FloatingPointToFPSignedBitVectorTypeRule {
+public :
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ TRACE("FloatingPointToFPSignedBitVectorTypeRule");
+
+ FloatingPointToFPSignedBitVector info = n.getOperator().getConst<FloatingPointToFPSignedBitVector>();
+
+ if (check) {
+ TypeNode roundingModeType = n[0].getType(check);
+
+ if (!roundingModeType.isRoundingMode()) {
+ throw TypeCheckingExceptionPrivate(n, "first argument must be a rounding mode");
+ }
+
+
+ TypeNode operandType = n[1].getType(check);
+
+ if (!(operandType.isBitVector())) {
+ throw TypeCheckingExceptionPrivate(n, "conversion to floating-point from signed bit vector used with sort other than bit vector");
+ }
+ }
+
+ return nodeManager->mkFloatingPointType(info.t);
+ }
+};
+
+
+class FloatingPointToFPUnsignedBitVectorTypeRule {
+public :
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ TRACE("FloatingPointToFPUnsignedBitVectorTypeRule");
+
+ FloatingPointToFPUnsignedBitVector info = n.getOperator().getConst<FloatingPointToFPUnsignedBitVector>();
+
+ if (check) {
+ TypeNode roundingModeType = n[0].getType(check);
+
+ if (!roundingModeType.isRoundingMode()) {
+ throw TypeCheckingExceptionPrivate(n, "first argument must be a rounding mode");
+ }
+
+
+ TypeNode operandType = n[1].getType(check);
+
+ if (!(operandType.isBitVector())) {
+ throw TypeCheckingExceptionPrivate(n, "conversion to floating-point from unsigned bit vector used with sort other than bit vector");
+ }
+ }
+
+ return nodeManager->mkFloatingPointType(info.t);
+ }
+};
+
+
+
+class FloatingPointToFPGenericTypeRule {
+public :
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ TRACE("FloatingPointToFPGenericTypeRule");
+
+ FloatingPointToFPGeneric info = n.getOperator().getConst<FloatingPointToFPGeneric>();
+
+ if (check) {
+ /* As this is a generic kind intended only for parsing,
+ * the checking here is light. For better checking, use
+ * expandDefinitions first.
+ */
+
+ size_t children = n.getNumChildren();
+ for (size_t i = 0; i < children; ++i) {
+ n[i].getType(check);
+ }
+ }
+
+ return nodeManager->mkFloatingPointType(info.t);
+ }
+};
+
+
+
+class FloatingPointToUBVTypeRule {
+public :
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ TRACE("FloatingPointToUBVTypeRule");
+
+ FloatingPointToUBV info = n.getOperator().getConst<FloatingPointToUBV>();
+
+ if (check) {
+ TypeNode roundingModeType = n[0].getType(check);
+
+ if (!roundingModeType.isRoundingMode()) {
+ throw TypeCheckingExceptionPrivate(n, "first argument must be a rounding mode");
+ }
+
+
+ TypeNode operandType = n[1].getType(check);
+
+ if (!(operandType.isFloatingPoint())) {
+ throw TypeCheckingExceptionPrivate(n, "conversion to unsigned bit vector used with a sort other than floating-point");
+ }
+ }
+
+ return nodeManager->mkBitVectorType(info.bvs);
+ }
+};
+
+
+class FloatingPointToSBVTypeRule {
+public :
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ TRACE("FloatingPointToSBVTypeRule");
+
+ FloatingPointToSBV info = n.getOperator().getConst<FloatingPointToSBV>();
+
+ if (check) {
+ TypeNode roundingModeType = n[0].getType(check);
+
+ if (!roundingModeType.isRoundingMode()) {
+ throw TypeCheckingExceptionPrivate(n, "first argument must be a rounding mode");
+ }
+
+
+ TypeNode operandType = n[1].getType(check);
+
+ if (!(operandType.isFloatingPoint())) {
+ throw TypeCheckingExceptionPrivate(n, "conversion to signed bit vector used with a sort other than floating-point");
+ }
+ }
+
+ return nodeManager->mkBitVectorType(info.bvs);
+ }
+};
+
+
+
+class FloatingPointToRealTypeRule {
+public :
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ TRACE("FloatingPointToRealTypeRule");
+
+ if (check) {
+ TypeNode roundingModeType = n[0].getType(check);
+
+ if (!roundingModeType.isRoundingMode()) {
+ throw TypeCheckingExceptionPrivate(n, "first argument must be a rounding mode");
+ }
+
+ TypeNode operand = n[1].getType(check);
+
+ if (!operand.isFloatingPoint()) {
+ throw TypeCheckingExceptionPrivate(n, "floating-point to real applied to a non floating-point sort");
+ }
+ }
+
+ return nodeManager->realType();
+ }
+};
+
+
+
+}/* CVC4::theory::fp namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__FP__THEORY_FP_TYPE_RULES_H */
ss << "BV";
++seen;
}
+ if(d_theories[THEORY_FP]) {
+ ss << "FP";
+ ++seen;
+ }
if(d_theories[THEORY_DATATYPES]) {
ss << "DT";
++seen;
enableTheory(THEORY_BV);
p += 2;
}
+ if(!strncmp(p, "FP", 2)) {
+ enableTheory(THEORY_FP);
+ p += 2;
+ }
if(!strncmp(p, "DT", 2)) {
enableTheory(THEORY_DATATYPES);
p += 2;
didyoumean.cpp \
unsat_core.h \
unsat_core.cpp \
+ floatingpoint.h \
+ floatingpoint.cpp \
resource_manager.h \
resource_manager.cpp \
unsafe_interrupt_exception.h
resource_manager.i \
unsafe_interrupt_exception.i \
proof.i \
- unsat_core.i
+ unsat_core.i \
+ floatingpoint.i
DISTCLEANFILES = \
integer.h.tmp \
--- /dev/null
+/********************* */
+/*! \file floatingpoint.cpp
+ ** \verbatim
+ ** Original author: Martin Brain
+ ** Major contributors:
+ ** Minor contributors (to current version):
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2013 University of Oxford
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Implementations of the utility functions for working with floating point theories. ]]
+ **
+ **/
+
+#include "util/cvc4_assert.h"
+#include "util/floatingpoint.h"
+
+namespace CVC4 {
+
+ FloatingPointSize::FloatingPointSize (unsigned _e, unsigned _s) : e(_e), s(_s)
+ {
+ CheckArgument(validExponentSize(_e),_e,"Invalid exponent size : %d",_e);
+ CheckArgument(validSignificandSize(_s),_s,"Invalid significand size : %d",_s);
+ }
+
+ FloatingPointSize::FloatingPointSize (const FloatingPointSize &old) : e(old.e), s(old.s)
+ {
+ CheckArgument(validExponentSize(e),e,"Invalid exponent size : %d",e);
+ CheckArgument(validSignificandSize(s),s,"Invalid significand size : %d",s);
+ }
+
+ void FloatingPointLiteral::unfinished (void) const {
+ Unimplemented("Floating-point literals not yet implemented.");
+ }
+
+}/* CVC4 namespace */
+
--- /dev/null
+/********************* */
+/*! \file floatingpoint.h
+ ** \verbatim
+ ** Original author: Martin Brain
+ ** Major contributors:
+ ** Minor contributors (to current version):
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2013 University of Oxford
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Utility functions for working with floating point theories. ]]
+ **
+ ** [[ This file contains the data structures used by the constant and
+ ** parametric types of the floating point theory. ]]
+ **/
+
+#include <fenv.h>
+
+#include "cvc4_public.h"
+
+#include "util/bitvector.h"
+
+
+#ifndef __CVC4__FLOATINGPOINT_H
+#define __CVC4__FLOATINGPOINT_H
+
+
+
+namespace CVC4 {
+
+
+ // Inline these!
+ inline bool CVC4_PUBLIC validExponentSize (unsigned e) { return e >= 2; }
+ inline bool CVC4_PUBLIC validSignificandSize (unsigned s) { return s >= 2; }
+
+ /**
+ * Floating point sorts are parameterised by two non-zero constants
+ * giving the width (in bits) of the exponent and significand
+ * (including the hidden bit).
+ */
+ class CVC4_PUBLIC FloatingPointSize {
+ /*
+ Class invariants:
+ * VALIDEXPONENTSIZE(e)
+ * VALIDSIGNIFCANDSIZE(s)
+ */
+
+ private :
+ unsigned e;
+ unsigned s;
+
+ public :
+ FloatingPointSize (unsigned _e, unsigned _s);
+ FloatingPointSize (const FloatingPointSize &old);
+
+ inline unsigned exponent (void) const {
+ return this->e;
+ }
+
+ inline unsigned significand (void) const {
+ return this->s;
+ }
+
+ bool operator ==(const FloatingPointSize& fps) const {
+ return (e == fps.e) && (s == fps.s);
+ }
+
+ }; /* class FloatingPointSize */
+
+
+
+#define ROLL(X,N) (((X) << (N)) | ((X) >> (8*sizeof((X)) - (N)) ))
+
+ struct CVC4_PUBLIC FloatingPointSizeHashFunction {
+ inline size_t operator() (const FloatingPointSize& fpt) const {
+ return size_t(ROLL(fpt.exponent(), 4*sizeof(unsigned)) |
+ fpt.significand());
+ }
+ }; /* struct FloatingPointSizeHashFunction */
+
+
+
+
+
+
+
+
+
+
+ /**
+ * A concrete instance of the rounding mode sort
+ */
+ enum CVC4_PUBLIC RoundingMode {
+ roundNearestTiesToEven = FE_TONEAREST,
+ roundNearestTiesToAway,
+ roundTowardPositive = FE_UPWARD,
+ roundTowardNegative = FE_DOWNWARD,
+ roundTowardZero = FE_TOWARDZERO
+ }; /* enum RoundingMode */
+
+ struct CVC4_PUBLIC RoundingModeHashFunction {
+ inline size_t operator() (const RoundingMode& rm) const {
+ return size_t(rm);
+ }
+ }; /* struct RoundingModeHashFunction */
+
+
+
+
+
+
+
+
+
+
+ /**
+ * A concrete floating point number
+ */
+
+ class CVC4_PUBLIC FloatingPointLiteral {
+ public :
+ // This intentional left unfinished as the choice of literal
+ // representation is solver specific.
+ void unfinished (void) const;
+
+ FloatingPointLiteral(unsigned, unsigned, double) { unfinished(); }
+ FloatingPointLiteral(unsigned, unsigned, const std::string &) { unfinished(); }
+ FloatingPointLiteral(const FloatingPointLiteral &) { unfinished(); }
+
+ bool operator == (const FloatingPointLiteral &op) const {
+ unfinished();
+ return false;
+ }
+
+ size_t hash (void) const {
+ unfinished();
+ return 23;
+ }
+ };
+
+ class CVC4_PUBLIC FloatingPoint {
+ protected :
+ FloatingPointLiteral fpl;
+
+ public :
+ FloatingPointSize t;
+
+ FloatingPoint (unsigned e, unsigned s, double d) : fpl(e,s,d), t(e,s) {}
+ FloatingPoint (unsigned e, unsigned s, const std::string &bitString) : fpl(e,s,bitString), t(e,s) {}
+ FloatingPoint (const FloatingPoint &fp) : fpl(fp.fpl), t(fp.t) {}
+
+ bool operator ==(const FloatingPoint& fp) const {
+ return ( (t == fp.t) && fpl == fp.fpl );
+ }
+
+ const FloatingPointLiteral & getLiteral (void) const {
+ return this->fpl;
+ }
+
+ }; /* class FloatingPoint */
+
+
+ struct CVC4_PUBLIC FloatingPointHashFunction {
+ inline size_t operator() (const FloatingPoint& fp) const {
+ FloatingPointSizeHashFunction h;
+ return h(fp.t) ^ fp.getLiteral().hash();
+ }
+ }; /* struct FloatingPointHashFunction */
+
+
+
+
+
+
+
+ /**
+ * The parameter type for the conversions to floating point.
+ */
+ class CVC4_PUBLIC FloatingPointConvertSort {
+ public :
+ FloatingPointSize t;
+
+ FloatingPointConvertSort (unsigned _e, unsigned _s)
+ : t(_e,_s) {}
+
+ bool operator ==(const FloatingPointConvertSort& fpcs) const {
+ return t == fpcs.t;
+ }
+
+ };
+
+ /**
+ * As different conversions are different parameterised kinds, there
+ * is a need for different (C++) types for each one.
+ */
+
+ class CVC4_PUBLIC FloatingPointToFPIEEEBitVector : public FloatingPointConvertSort {
+ public : FloatingPointToFPIEEEBitVector (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {}
+ };
+ class CVC4_PUBLIC FloatingPointToFPFloatingPoint : public FloatingPointConvertSort {
+ public : FloatingPointToFPFloatingPoint (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {}
+ };
+ class CVC4_PUBLIC FloatingPointToFPReal : public FloatingPointConvertSort {
+ public : FloatingPointToFPReal (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {}
+ };
+ class CVC4_PUBLIC FloatingPointToFPSignedBitVector : public FloatingPointConvertSort {
+ public : FloatingPointToFPSignedBitVector (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {}
+ };
+ class CVC4_PUBLIC FloatingPointToFPUnsignedBitVector : public FloatingPointConvertSort {
+ public : FloatingPointToFPUnsignedBitVector (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {}
+ };
+ class CVC4_PUBLIC FloatingPointToFPGeneric : public FloatingPointConvertSort {
+ public : FloatingPointToFPGeneric (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {}
+ };
+
+
+
+ template <unsigned key>
+ struct CVC4_PUBLIC FloatingPointConvertSortHashFunction {
+ inline size_t operator() (const FloatingPointConvertSort& fpcs) const {
+ FloatingPointSizeHashFunction f;
+ return f(fpcs.t) ^ (0x00005300 | (key << 24));
+ }
+ }; /* struct FloatingPointConvertSortHashFunction */
+
+
+
+
+
+
+
+
+ /**
+ * The parameter type for the conversion to bit vector.
+ */
+ class CVC4_PUBLIC FloatingPointToBV {
+ public :
+ BitVectorSize bvs;
+
+ FloatingPointToBV (unsigned s)
+ : bvs(s) {}
+ operator unsigned () const { return bvs; }
+ };
+
+ class CVC4_PUBLIC FloatingPointToUBV : public FloatingPointToBV {
+ public : FloatingPointToUBV (unsigned _s) : FloatingPointToBV(_s) {}
+ };
+ class CVC4_PUBLIC FloatingPointToSBV : public FloatingPointToBV {
+ public : FloatingPointToSBV (unsigned _s) : FloatingPointToBV(_s) {}
+ };
+
+
+ template <unsigned key>
+ struct CVC4_PUBLIC FloatingPointToBVHashFunction {
+ inline size_t operator() (const FloatingPointToBV& fptbv) const {
+ UnsignedHashFunction< ::CVC4::BitVectorSize > f;
+ return (key ^ 0x46504256) ^ f(fptbv.bvs);
+ }
+ }; /* struct FloatingPointToBVHashFunction */
+
+
+
+
+
+
+ inline std::ostream& operator <<(std::ostream& os, const FloatingPointLiteral& fp) CVC4_PUBLIC;
+ inline std::ostream& operator <<(std::ostream& os, const FloatingPointLiteral& fp) {
+ fp.unfinished();
+ return os;
+ }
+
+ inline std::ostream& operator <<(std::ostream& os, const FloatingPoint& fp) CVC4_PUBLIC;
+ inline std::ostream& operator <<(std::ostream& os, const FloatingPoint& fp) {
+ return os << fp.getLiteral();
+ }
+
+ inline std::ostream& operator <<(std::ostream& os, const FloatingPointSize& fps) CVC4_PUBLIC;
+ inline std::ostream& operator <<(std::ostream& os, const FloatingPointSize& fps) {
+ return os << "(_ FloatingPoint " << fps.exponent() << " " << fps.significand() << ")";
+ }
+
+ inline std::ostream& operator <<(std::ostream& os, const FloatingPointConvertSort& fpcs) CVC4_PUBLIC;
+ inline std::ostream& operator <<(std::ostream& os, const FloatingPointConvertSort& fpcs) {
+ return os << "(_ to_fp " << fpcs.t.exponent() << " " << fpcs.t.significand() << ")";
+ }
+
+
+
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__FLOATINGPOINT_H */
--- /dev/null
+%{
+#include "util/floatingpoint.h"
+%}
+
+%include "util/floatingpoint.h"
info.arithOnlyLinear();
info.disableIntegers();
info.lock();
- TS_ASSERT_EQUALS( info.getLogicString(), "AUFBVDTLRA" );
+ TS_ASSERT_EQUALS( info.getLogicString(), "AUFBVFPDTLRA" );
info = info.getUnlockedCopy();
TS_ASSERT( !info.isLocked() );
info.disableQuantifiers();
info.lock();
- TS_ASSERT_EQUALS( info.getLogicString(), "QF_AUFBVDTLRA" );
+ TS_ASSERT_EQUALS( info.getLogicString(), "QF_AUFBVFPDTLRA" );
info = info.getUnlockedCopy();
TS_ASSERT( !info.isLocked() );
info.enableIntegers();
info.disableReals();
info.lock();
- TS_ASSERT_EQUALS( info.getLogicString(), "QF_AUFLIA" );
+ TS_ASSERT_EQUALS( info.getLogicString(), "QF_AUFFPLIA" );
info = info.getUnlockedCopy();
TS_ASSERT( !info.isLocked() );
info.disableTheory(THEORY_ARITH);
info.disableTheory(THEORY_UF);
+ info.disableTheory(THEORY_FP);
info.lock();
TS_ASSERT_EQUALS( info.getLogicString(), "QF_AX" );
TS_ASSERT( info.isPure( THEORY_ARRAY ) );
projects / cvc5.git / commitdiff