From cf6bc6c57dd579b8f75b7d20922eda0eaa92b2f7 Mon Sep 17 00:00:00 2001 From: Martin Brain Date: Wed, 3 Dec 2014 21:29:43 -0500 Subject: [PATCH] Floating point infrastructure. Signed-off-by: Morgan Deters --- src/Makefile.am | 13 +- src/cvc4.i | 1 + src/expr/expr_manager_template.cpp | 11 + src/expr/expr_manager_template.cpp.orig | 1027 ++++++++++++++++ src/expr/expr_manager_template.h | 6 + src/expr/expr_manager_template.h.orig | 572 +++++++++ src/expr/node_manager.h | 21 + src/expr/node_manager.h.orig | 1498 +++++++++++++++++++++++ src/expr/type.cpp | 30 + src/expr/type.h | 51 + src/expr/type_node.h | 49 + src/options/Makefile.am | 8 +- src/parser/smt2/Smt2.g | 175 ++- src/parser/smt2/smt2.cpp | 51 + src/parser/smt2/smt2.h | 5 +- src/printer/smt2/smt2_printer.cpp | 158 ++- src/smt/boolean_terms.cpp | 12 +- src/theory/fp/kinds | 238 ++++ src/theory/fp/options | 8 + src/theory/fp/options_handlers.h | 14 + src/theory/fp/theory_fp.cpp | 104 ++ src/theory/fp/theory_fp.h | 36 + src/theory/fp/theory_fp_rewriter.cpp | 478 ++++++++ src/theory/fp/theory_fp_rewriter.h | 48 + src/theory/fp/theory_fp_type_rules.h | 430 +++++++ src/theory/logic_info.cpp | 8 + src/util/Makefile.am | 5 +- src/util/floatingpoint.cpp | 38 + src/util/floatingpoint.h | 293 +++++ src/util/floatingpoint.i | 5 + test/unit/theory/logic_info_white.h | 7 +- 31 files changed, 5380 insertions(+), 20 deletions(-) create mode 100644 src/expr/expr_manager_template.cpp.orig create mode 100644 src/expr/expr_manager_template.h.orig create mode 100644 src/expr/node_manager.h.orig create mode 100644 src/theory/fp/kinds create mode 100644 src/theory/fp/options create mode 100644 src/theory/fp/options_handlers.h create mode 100644 src/theory/fp/theory_fp.cpp create mode 100644 src/theory/fp/theory_fp.h create mode 100644 src/theory/fp/theory_fp_rewriter.cpp create mode 100644 src/theory/fp/theory_fp_rewriter.h create mode 100644 src/theory/fp/theory_fp_type_rules.h create mode 100644 src/util/floatingpoint.cpp create mode 100644 src/util/floatingpoint.h create mode 100644 src/util/floatingpoint.i diff --git a/src/Makefile.am b/src/Makefile.am index f88dcb3a9..e66d590dc 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -20,7 +20,7 @@ AM_CPPFLAGS = \ 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 @@ -407,7 +407,12 @@ libcvc4_la_SOURCES = \ 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 \ @@ -491,7 +496,9 @@ EXTRA_DIST = \ 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)( \ diff --git a/src/cvc4.i b/src/cvc4.i index 3ad08660c..56404ee65 100644 --- a/src/cvc4.i +++ b/src/cvc4.i @@ -297,6 +297,7 @@ std::set CVC4::JavaInputStreamAdapter::s_adapters; %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" diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index c5249075b..7eb93b8ff 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -154,6 +154,12 @@ IntegerType ExprManager::integerType() const { return IntegerType(Type(d_nodeManager, new TypeNode(d_nodeManager->integerType()))); } +RoundingModeType ExprManager::roundingModeType() const { + NodeManagerScope nms(d_nodeManager); + return RoundingModeType(Type(d_nodeManager, new TypeNode(d_nodeManager->roundingModeType()))); +} + + Expr ExprManager::mkExpr(Kind kind, Expr child1) { const kind::MetaKind mk = kind::metaKindOf(kind); const unsigned n = 1 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0); @@ -573,6 +579,11 @@ SExprType ExprManager::mkSExprType(const std::vector& types) { return SExprType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSExprType(typeNodes)))); } +FloatingPointType ExprManager::mkFloatingPointType(unsigned exp, unsigned sig) const { + NodeManagerScope nms(d_nodeManager); + return FloatingPointType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkFloatingPointType(exp,sig)))); +} + BitVectorType ExprManager::mkBitVectorType(unsigned size) const { NodeManagerScope nms(d_nodeManager); return BitVectorType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkBitVectorType(size)))); diff --git a/src/expr/expr_manager_template.cpp.orig b/src/expr/expr_manager_template.cpp.orig new file mode 100644 index 000000000..c5249075b --- /dev/null +++ b/src/expr/expr_manager_template.cpp.orig @@ -0,0 +1,1027 @@ +/********************* */ +/*! \file expr_manager_template.cpp + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: Dejan Jovanovic, Christopher L. Conway + ** Minor contributors (to current version): Kshitij Bansal, Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Public-facing expression manager interface, implementation + ** + ** Public-facing expression manager interface, implementation. + **/ + +#include "expr/node_manager.h" +#include "expr/expr_manager.h" +#include "expr/variable_type_map.h" +#include "options/options.h" +#include "util/statistics_registry.h" + +#include + +${includes} + +// This is a hack, but an important one: if there's an error, the +// compiler directs the user to the template file instead of the +// generated one. We don't want the user to modify the generated one, +// since it'll get overwritten on a later build. +#line 32 "${template}" + +#ifdef CVC4_STATISTICS_ON + #define INC_STAT(kind) \ + { \ + if (d_exprStatistics[kind] == NULL) { \ + stringstream statName; \ + statName << "expr::ExprManager::" << kind; \ + d_exprStatistics[kind] = new IntStat(statName.str(), 0); \ + d_nodeManager->getStatisticsRegistry()->registerStat_(d_exprStatistics[kind]); \ + } \ + ++ *(d_exprStatistics[kind]); \ + } + #define INC_STAT_VAR(type, bound_var) \ + { \ + TypeNode* typeNode = Type::getTypeNode(type); \ + TypeConstant type = typeNode->getKind() == kind::TYPE_CONSTANT ? typeNode->getConst() : LAST_TYPE; \ + if (d_exprStatisticsVars[type] == NULL) { \ + stringstream statName; \ + if (type == LAST_TYPE) { \ + statName << "expr::ExprManager::" << ((bound_var) ? "BOUND_VARIABLE" : "VARIABLE") << ":Parameterized type"; \ + } else { \ + statName << "expr::ExprManager::" << ((bound_var) ? "BOUND_VARIABLE" : "VARIABLE") << ":" << type; \ + } \ + d_exprStatisticsVars[type] = new IntStat(statName.str(), 0); \ + d_nodeManager->getStatisticsRegistry()->registerStat_(d_exprStatisticsVars[type]); \ + } \ + ++ *(d_exprStatisticsVars[type]); \ + } +#else + #define INC_STAT(kind) + #define INC_STAT_VAR(type, bound_var) +#endif + +using namespace std; +using namespace CVC4::kind; + +namespace CVC4 { + +ExprManager::ExprManager() : + d_nodeManager(new NodeManager(this)) { +#ifdef CVC4_STATISTICS_ON + for (unsigned i = 0; i < kind::LAST_KIND; ++ i) { + d_exprStatistics[i] = NULL; + } + for (unsigned i = 0; i < LAST_TYPE; ++ i) { + d_exprStatisticsVars[i] = NULL; + } +#endif +} + +ExprManager::ExprManager(const Options& options) : + d_nodeManager(new NodeManager(this, options)) { +#ifdef CVC4_STATISTICS_ON + for (unsigned i = 0; i < LAST_TYPE; ++ i) { + d_exprStatisticsVars[i] = NULL; + } + for (unsigned i = 0; i < kind::LAST_KIND; ++ i) { + d_exprStatistics[i] = NULL; + } +#endif +} + +ExprManager::~ExprManager() throw() { + NodeManagerScope nms(d_nodeManager); + + try { + +#ifdef CVC4_STATISTICS_ON + for (unsigned i = 0; i < kind::LAST_KIND; ++ i) { + if (d_exprStatistics[i] != NULL) { + d_nodeManager->getStatisticsRegistry()->unregisterStat_(d_exprStatistics[i]); + delete d_exprStatistics[i]; + d_exprStatistics[i] = NULL; + } + } + for (unsigned i = 0; i < LAST_TYPE; ++ i) { + if (d_exprStatisticsVars[i] != NULL) { + d_nodeManager->getStatisticsRegistry()->unregisterStat_(d_exprStatisticsVars[i]); + delete d_exprStatisticsVars[i]; + d_exprStatisticsVars[i] = NULL; + } + } +#endif + + delete d_nodeManager; + d_nodeManager = NULL; + + } catch(Exception& e) { + Warning() << "CVC4 threw an exception during cleanup." << std::endl + << e << std::endl; + } +} + +StatisticsRegistry* ExprManager::getStatisticsRegistry() throw() { + return d_nodeManager->getStatisticsRegistry(); +} + +const Options& ExprManager::getOptions() const { + return d_nodeManager->getOptions(); +} + +ResourceManager* ExprManager::getResourceManager() throw() { + return d_nodeManager->getResourceManager(); +} + +BooleanType ExprManager::booleanType() const { + NodeManagerScope nms(d_nodeManager); + return BooleanType(Type(d_nodeManager, new TypeNode(d_nodeManager->booleanType()))); +} + +StringType ExprManager::stringType() const { + NodeManagerScope nms(d_nodeManager); + return StringType(Type(d_nodeManager, new TypeNode(d_nodeManager->stringType()))); +} + +RealType ExprManager::realType() const { + NodeManagerScope nms(d_nodeManager); + return RealType(Type(d_nodeManager, new TypeNode(d_nodeManager->realType()))); +} + +IntegerType ExprManager::integerType() const { + NodeManagerScope nms(d_nodeManager); + return IntegerType(Type(d_nodeManager, new TypeNode(d_nodeManager->integerType()))); +} + +Expr ExprManager::mkExpr(Kind kind, Expr child1) { + const kind::MetaKind mk = kind::metaKindOf(kind); + const unsigned n = 1 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0); + CheckArgument(mk == kind::metakind::PARAMETERIZED || + mk == kind::metakind::OPERATOR, kind, + "Only operator-style expressions are made with mkExpr(); " + "to make variables and constants, see mkVar(), mkBoundVar(), " + "and mkConst()."); + CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, + "Exprs with kind %s must have at least %u children and " + "at most %u children (the one under construction has %u)", + kind::kindToString(kind).c_str(), + minArity(kind), maxArity(kind), n); + NodeManagerScope nms(d_nodeManager); + try { + INC_STAT(kind); + return Expr(this, d_nodeManager->mkNodePtr(kind, child1.getNode())); + } catch (const TypeCheckingExceptionPrivate& e) { + throw TypeCheckingException(this, &e); + } +} + +Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2) { + const kind::MetaKind mk = kind::metaKindOf(kind); + const unsigned n = 2 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0); + CheckArgument(mk == kind::metakind::PARAMETERIZED || + mk == kind::metakind::OPERATOR, kind, + "Only operator-style expressions are made with mkExpr(); " + "to make variables and constants, see mkVar(), mkBoundVar(), " + "and mkConst()."); + CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, + "Exprs with kind %s must have at least %u children and " + "at most %u children (the one under construction has %u)", + kind::kindToString(kind).c_str(), + minArity(kind), maxArity(kind), n); + NodeManagerScope nms(d_nodeManager); + try { + INC_STAT(kind); + return Expr(this, d_nodeManager->mkNodePtr(kind, + child1.getNode(), + child2.getNode())); + } catch (const TypeCheckingExceptionPrivate& e) { + throw TypeCheckingException(this, &e); + } +} + +Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3) { + const kind::MetaKind mk = kind::metaKindOf(kind); + const unsigned n = 3 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0); + CheckArgument(mk == kind::metakind::PARAMETERIZED || + mk == kind::metakind::OPERATOR, kind, + "Only operator-style expressions are made with mkExpr(); " + "to make variables and constants, see mkVar(), mkBoundVar(), " + "and mkConst()."); + CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, + "Exprs with kind %s must have at least %u children and " + "at most %u children (the one under construction has %u)", + kind::kindToString(kind).c_str(), + minArity(kind), maxArity(kind), n); + NodeManagerScope nms(d_nodeManager); + try { + INC_STAT(kind); + return Expr(this, d_nodeManager->mkNodePtr(kind, + child1.getNode(), + child2.getNode(), + child3.getNode())); + } catch (const TypeCheckingExceptionPrivate& e) { + throw TypeCheckingException(this, &e); + } +} + +Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, + Expr child4) { + const kind::MetaKind mk = kind::metaKindOf(kind); + const unsigned n = 4 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0); + CheckArgument(mk == kind::metakind::PARAMETERIZED || + mk == kind::metakind::OPERATOR, kind, + "Only operator-style expressions are made with mkExpr(); " + "to make variables and constants, see mkVar(), mkBoundVar(), " + "and mkConst()."); + CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, + "Exprs with kind %s must have at least %u children and " + "at most %u children (the one under construction has %u)", + kind::kindToString(kind).c_str(), + minArity(kind), maxArity(kind), n); + NodeManagerScope nms(d_nodeManager); + try { + INC_STAT(kind); + return Expr(this, d_nodeManager->mkNodePtr(kind, + child1.getNode(), + child2.getNode(), + child3.getNode(), + child4.getNode())); + } catch (const TypeCheckingExceptionPrivate& e) { + throw TypeCheckingException(this, &e); + } +} + +Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, + Expr child4, Expr child5) { + const kind::MetaKind mk = kind::metaKindOf(kind); + const unsigned n = 5 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0); + CheckArgument(mk == kind::metakind::PARAMETERIZED || + mk == kind::metakind::OPERATOR, kind, + "Only operator-style expressions are made with mkExpr(); " + "to make variables and constants, see mkVar(), mkBoundVar(), " + "and mkConst()."); + CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, + "Exprs with kind %s must have at least %u children and " + "at most %u children (the one under construction has %u)", + kind::kindToString(kind).c_str(), + minArity(kind), maxArity(kind), n); + NodeManagerScope nms(d_nodeManager); + try { + INC_STAT(kind); + return Expr(this, d_nodeManager->mkNodePtr(kind, + child1.getNode(), + child2.getNode(), + child3.getNode(), + child4.getNode(), + child5.getNode())); + } catch (const TypeCheckingExceptionPrivate& e) { + throw TypeCheckingException(this, &e); + } +} + +Expr ExprManager::mkExpr(Kind kind, const std::vector& children) { + const kind::MetaKind mk = kind::metaKindOf(kind); + const unsigned n = children.size() - (mk == kind::metakind::PARAMETERIZED ? 1 : 0); + CheckArgument(mk == kind::metakind::PARAMETERIZED || + mk == kind::metakind::OPERATOR, kind, + "Only operator-style expressions are made with mkExpr(); " + "to make variables and constants, see mkVar(), mkBoundVar(), " + "and mkConst()."); + CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, + "Exprs with kind %s must have at least %u children and " + "at most %u children (the one under construction has %u)", + kind::kindToString(kind).c_str(), + minArity(kind), maxArity(kind), n); + + NodeManagerScope nms(d_nodeManager); + + vector nodes; + vector::const_iterator it = children.begin(); + vector::const_iterator it_end = children.end(); + while(it != it_end) { + nodes.push_back(it->getNode()); + ++it; + } + try { + INC_STAT(kind); + return Expr(this, d_nodeManager->mkNodePtr(kind, nodes)); + } catch (const TypeCheckingExceptionPrivate& e) { + throw TypeCheckingException(this, &e); + } +} + +Expr ExprManager::mkExpr(Kind kind, Expr child1, + const std::vector& otherChildren) { + const kind::MetaKind mk = kind::metaKindOf(kind); + const unsigned n = otherChildren.size() - (mk == kind::metakind::PARAMETERIZED ? 1 : 0) + 1; + CheckArgument(mk == kind::metakind::PARAMETERIZED || + mk == kind::metakind::OPERATOR, kind, + "Only operator-style expressions are made with mkExpr(); " + "to make variables and constants, see mkVar(), mkBoundVar(), " + "and mkConst()."); + CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, + "Exprs with kind %s must have at least %u children and " + "at most %u children (the one under construction has %u)", + kind::kindToString(kind).c_str(), + minArity(kind), maxArity(kind), n); + + NodeManagerScope nms(d_nodeManager); + + vector nodes; + nodes.push_back(child1.getNode()); + + vector::const_iterator it = otherChildren.begin(); + vector::const_iterator it_end = otherChildren.end(); + while(it != it_end) { + nodes.push_back(it->getNode()); + ++it; + } + try { + INC_STAT(kind); + return Expr(this, d_nodeManager->mkNodePtr(kind, nodes)); + } catch (const TypeCheckingExceptionPrivate& e) { + throw TypeCheckingException(this, &e); + } +} + +Expr ExprManager::mkExpr(Expr opExpr) { + const unsigned n = 0; + Kind kind = NodeManager::operatorToKind(opExpr.getNode()); + CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr, + "This Expr constructor is for parameterized kinds only"); + CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, + "Exprs with kind %s must have at least %u children and " + "at most %u children (the one under construction has %u)", + kind::kindToString(kind).c_str(), + minArity(kind), maxArity(kind), n); + NodeManagerScope nms(d_nodeManager); + try { + INC_STAT(kind); + return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode())); + } catch (const TypeCheckingExceptionPrivate& e) { + throw TypeCheckingException(this, &e); + } +} + +Expr ExprManager::mkExpr(Expr opExpr, Expr child1) { + const unsigned n = 1; + Kind kind = NodeManager::operatorToKind(opExpr.getNode()); + CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr, + "This Expr constructor is for parameterized kinds only"); + CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, + "Exprs with kind %s must have at least %u children and " + "at most %u children (the one under construction has %u)", + kind::kindToString(kind).c_str(), + minArity(kind), maxArity(kind), n); + NodeManagerScope nms(d_nodeManager); + try { + INC_STAT(kind); + return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(), child1.getNode())); + } catch (const TypeCheckingExceptionPrivate& e) { + throw TypeCheckingException(this, &e); + } +} + +Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2) { + const unsigned n = 2; + Kind kind = NodeManager::operatorToKind(opExpr.getNode()); + CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr, + "This Expr constructor is for parameterized kinds only"); + CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, + "Exprs with kind %s must have at least %u children and " + "at most %u children (the one under construction has %u)", + kind::kindToString(kind).c_str(), + minArity(kind), maxArity(kind), n); + NodeManagerScope nms(d_nodeManager); + try { + INC_STAT(kind); + return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(), + child1.getNode(), + child2.getNode())); + } catch (const TypeCheckingExceptionPrivate& e) { + throw TypeCheckingException(this, &e); + } +} + +Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3) { + const unsigned n = 3; + Kind kind = NodeManager::operatorToKind(opExpr.getNode()); + CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr, + "This Expr constructor is for parameterized kinds only"); + CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, + "Exprs with kind %s must have at least %u children and " + "at most %u children (the one under construction has %u)", + kind::kindToString(kind).c_str(), + minArity(kind), maxArity(kind), n); + NodeManagerScope nms(d_nodeManager); + try { + INC_STAT(kind); + return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(), + child1.getNode(), + child2.getNode(), + child3.getNode())); + } catch (const TypeCheckingExceptionPrivate& e) { + throw TypeCheckingException(this, &e); + } +} + +Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3, + Expr child4) { + const unsigned n = 4; + Kind kind = NodeManager::operatorToKind(opExpr.getNode()); + CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr, + "This Expr constructor is for parameterized kinds only"); + CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, + "Exprs with kind %s must have at least %u children and " + "at most %u children (the one under construction has %u)", + kind::kindToString(kind).c_str(), + minArity(kind), maxArity(kind), n); + NodeManagerScope nms(d_nodeManager); + try { + INC_STAT(kind); + return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(), + child1.getNode(), + child2.getNode(), + child3.getNode(), + child4.getNode())); + } catch (const TypeCheckingExceptionPrivate& e) { + throw TypeCheckingException(this, &e); + } +} + +Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3, + Expr child4, Expr child5) { + const unsigned n = 5; + Kind kind = NodeManager::operatorToKind(opExpr.getNode()); + CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr, + "This Expr constructor is for parameterized kinds only"); + CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, + "Exprs with kind %s must have at least %u children and " + "at most %u children (the one under construction has %u)", + kind::kindToString(kind).c_str(), + minArity(kind), maxArity(kind), n); + NodeManagerScope nms(d_nodeManager); + try { + INC_STAT(kind); + return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(), + child1.getNode(), + child2.getNode(), + child3.getNode(), + child4.getNode(), + child5.getNode())); + } catch (const TypeCheckingExceptionPrivate& e) { + throw TypeCheckingException(this, &e); + } +} + +Expr ExprManager::mkExpr(Expr opExpr, const std::vector& children) { + const unsigned n = children.size(); + Kind kind = NodeManager::operatorToKind(opExpr.getNode()); + CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr, + "This Expr constructor is for parameterized kinds only"); + CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, + "Exprs with kind %s must have at least %u children and " + "at most %u children (the one under construction has %u)", + kind::kindToString(kind).c_str(), + minArity(kind), maxArity(kind), n); + + NodeManagerScope nms(d_nodeManager); + + vector nodes; + vector::const_iterator it = children.begin(); + vector::const_iterator it_end = children.end(); + while(it != it_end) { + nodes.push_back(it->getNode()); + ++it; + } + try { + INC_STAT(kind); + return Expr(this,d_nodeManager->mkNodePtr(opExpr.getNode(), nodes)); + } catch (const TypeCheckingExceptionPrivate& e) { + throw TypeCheckingException(this, &e); + } +} + +bool ExprManager::hasOperator(Kind k) { + return NodeManager::hasOperator(k); +} + +Expr ExprManager::operatorOf(Kind k) { + NodeManagerScope nms(d_nodeManager); + + return d_nodeManager->operatorOf(k).toExpr(); +} + +/** Make a function type from domain to range. */ +FunctionType ExprManager::mkFunctionType(Type domain, Type range) { + NodeManagerScope nms(d_nodeManager); + return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(*domain.d_typeNode, *range.d_typeNode)))); +} + +/** Make a function type with input types from argTypes. */ +FunctionType ExprManager::mkFunctionType(const std::vector& argTypes, Type range) { + NodeManagerScope nms(d_nodeManager); + Assert( argTypes.size() >= 1 ); + std::vector argTypeNodes; + for (unsigned i = 0, i_end = argTypes.size(); i < i_end; ++ i) { + argTypeNodes.push_back(*argTypes[i].d_typeNode); + } + return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(argTypeNodes, *range.d_typeNode)))); +} + +FunctionType ExprManager::mkFunctionType(const std::vector& sorts) { + NodeManagerScope nms(d_nodeManager); + Assert( sorts.size() >= 2 ); + std::vector sortNodes; + for (unsigned i = 0, i_end = sorts.size(); i < i_end; ++ i) { + sortNodes.push_back(*sorts[i].d_typeNode); + } + return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(sortNodes)))); +} + +FunctionType ExprManager::mkPredicateType(const std::vector& sorts) { + NodeManagerScope nms(d_nodeManager); + Assert( sorts.size() >= 1 ); + std::vector sortNodes; + for (unsigned i = 0, i_end = sorts.size(); i < i_end; ++ i) { + sortNodes.push_back(*sorts[i].d_typeNode); + } + return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkPredicateType(sortNodes)))); +} + +TupleType ExprManager::mkTupleType(const std::vector& types) { + NodeManagerScope nms(d_nodeManager); + std::vector typeNodes; + for (unsigned i = 0, i_end = types.size(); i < i_end; ++ i) { + typeNodes.push_back(*types[i].d_typeNode); + } + return TupleType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkTupleType(typeNodes)))); +} + +RecordType ExprManager::mkRecordType(const Record& rec) { + NodeManagerScope nms(d_nodeManager); + return RecordType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkRecordType(rec)))); +} + +SExprType ExprManager::mkSExprType(const std::vector& types) { + NodeManagerScope nms(d_nodeManager); + std::vector typeNodes; + for (unsigned i = 0, i_end = types.size(); i < i_end; ++ i) { + typeNodes.push_back(*types[i].d_typeNode); + } + return SExprType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSExprType(typeNodes)))); +} + +BitVectorType ExprManager::mkBitVectorType(unsigned size) const { + NodeManagerScope nms(d_nodeManager); + return BitVectorType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkBitVectorType(size)))); +} + +ArrayType ExprManager::mkArrayType(Type indexType, Type constituentType) const { + NodeManagerScope nms(d_nodeManager); + return ArrayType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkArrayType(*indexType.d_typeNode, *constituentType.d_typeNode)))); +} + +SetType ExprManager::mkSetType(Type elementType) const { + NodeManagerScope nms(d_nodeManager); + return SetType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSetType(*elementType.d_typeNode)))); +} + +DatatypeType ExprManager::mkDatatypeType(const Datatype& datatype) { + // Not worth a special implementation; this doesn't need to be fast + // code anyway. + vector datatypes; + datatypes.push_back(datatype); + vector result = mkMutualDatatypeTypes(datatypes); + Assert(result.size() == 1); + return result.front(); +} + +std::vector +ExprManager::mkMutualDatatypeTypes(const std::vector& datatypes) { + return mkMutualDatatypeTypes(datatypes, set()); +} + +std::vector +ExprManager::mkMutualDatatypeTypes(const std::vector& datatypes, + const std::set& unresolvedTypes) { + NodeManagerScope nms(d_nodeManager); + std::map nameResolutions; + std::vector dtts; + + // First do some sanity checks, set up the final Type to be used for + // each datatype, and set up the "named resolutions" used to handle + // simple self- and mutual-recursion, for example in the definition + // "nat = succ(pred:nat) | zero", a named resolution can handle the + // pred selector. + for(std::vector::const_iterator i = datatypes.begin(), + i_end = datatypes.end(); + i != i_end; + ++i) { + TypeNode* typeNode; + if( (*i).getNumParameters() == 0 ) { + typeNode = new TypeNode(d_nodeManager->mkTypeConst(*i)); + } else { + TypeNode cons = d_nodeManager->mkTypeConst(*i); + std::vector< TypeNode > params; + params.push_back( cons ); + for( unsigned int ip = 0; ip < (*i).getNumParameters(); ++ip ) { + params.push_back( TypeNode::fromType( (*i).getParameter( ip ) ) ); + } + + typeNode = new TypeNode(d_nodeManager->mkTypeNode(kind::PARAMETRIC_DATATYPE, params)); + } + Type type(d_nodeManager, typeNode); + DatatypeType dtt(type); + CheckArgument(nameResolutions.find((*i).getName()) == nameResolutions.end(), + datatypes, + "cannot construct two datatypes at the same time " + "with the same name `%s'", + (*i).getName().c_str()); + nameResolutions.insert(std::make_pair((*i).getName(), dtt)); + dtts.push_back(dtt); + } + + // Second, set up the type substitution map for complex type + // resolution (e.g. if "list" is the type we're defining, and it has + // a selector of type "ARRAY INT OF list", this can't be taken care + // of using the named resolutions that we set up above. A + // preliminary array type was set up, and now needs to have "list" + // substituted in it for the correct type. + // + // @TODO get rid of named resolutions altogether and handle + // everything with these resolutions? + std::vector< SortConstructorType > paramTypes; + std::vector< DatatypeType > paramReplacements; + std::vector placeholders;// to hold the "unresolved placeholders" + std::vector replacements;// to hold our final, resolved types + for(std::set::const_iterator i = unresolvedTypes.begin(), + i_end = unresolvedTypes.end(); + i != i_end; + ++i) { + std::string name; + if( (*i).isSort() ) { + name = SortType(*i).getName(); + } else { + Assert( (*i).isSortConstructor() ); + name = SortConstructorType(*i).getName(); + } + std::map::const_iterator resolver = + nameResolutions.find(name); + CheckArgument(resolver != nameResolutions.end(), + unresolvedTypes, + "cannot resolve type `%s'; it's not among " + "the datatypes being defined", name.c_str()); + // We will instruct the Datatype to substitute "*i" (the + // unresolved SortType used as a placeholder in complex types) + // with "(*resolver).second" (the DatatypeType we created in the + // first step, above). + if( (*i).isSort() ) { + placeholders.push_back(*i); + replacements.push_back( (*resolver).second ); + } else { + Assert( (*i).isSortConstructor() ); + paramTypes.push_back( SortConstructorType(*i) ); + paramReplacements.push_back( (*resolver).second ); + } + } + + // Lastly, perform the final resolutions and checks. + for(std::vector::iterator i = dtts.begin(), + i_end = dtts.end(); + i != i_end; + ++i) { + const Datatype& dt = (*i).getDatatype(); + if(!dt.isResolved()) { + const_cast(dt).resolve(this, nameResolutions, + placeholders, replacements, + paramTypes, paramReplacements); + } + + // Now run some checks, including a check to make sure that no + // selector is function-valued. + checkResolvedDatatype(*i); + } + + for(std::vector::iterator i = d_nodeManager->d_listeners.begin(); i != d_nodeManager->d_listeners.end(); ++i) { + (*i)->nmNotifyNewDatatypes(dtts); + } + + return dtts; +} + +void ExprManager::checkResolvedDatatype(DatatypeType dtt) const { + const Datatype& dt = dtt.getDatatype(); + + AssertArgument(dt.isResolved(), dtt, "datatype should have been resolved"); + + // for all constructors... + for(Datatype::const_iterator i = dt.begin(), i_end = dt.end(); + i != i_end; + ++i) { + const DatatypeConstructor& c = *i; + Type testerType CVC4_UNUSED = c.getTester().getType(); + Assert(c.isResolved() && + testerType.isTester() && + TesterType(testerType).getDomain() == dtt && + TesterType(testerType).getRangeType() == booleanType(), + "malformed tester in datatype post-resolution"); + Type ctorType CVC4_UNUSED = c.getConstructor().getType(); + Assert(ctorType.isConstructor() && + ConstructorType(ctorType).getArity() == c.getNumArgs() && + ConstructorType(ctorType).getRangeType() == dtt, + "malformed constructor in datatype post-resolution"); + // for all selectors... + for(DatatypeConstructor::const_iterator j = c.begin(), j_end = c.end(); + j != j_end; + ++j) { + const DatatypeConstructorArg& a = *j; + Type selectorType = a.getSelector().getType(); + Assert(a.isResolved() && + selectorType.isSelector() && + SelectorType(selectorType).getDomain() == dtt, + "malformed selector in datatype post-resolution"); + // This next one's a "hard" check, performed in non-debug builds + // as well; the other ones should all be guaranteed by the + // CVC4::Datatype class, but this actually needs to be checked. + AlwaysAssert(!SelectorType(selectorType).getRangeType().d_typeNode->isFunctionLike(), + "cannot put function-like things in datatypes"); + } + } +} + +ConstructorType ExprManager::mkConstructorType(const DatatypeConstructor& constructor, Type range) const { + NodeManagerScope nms(d_nodeManager); + return Type(d_nodeManager, new TypeNode(d_nodeManager->mkConstructorType(constructor, *range.d_typeNode))); +} + +SelectorType ExprManager::mkSelectorType(Type domain, Type range) const { + NodeManagerScope nms(d_nodeManager); + return Type(d_nodeManager, new TypeNode(d_nodeManager->mkSelectorType(*domain.d_typeNode, *range.d_typeNode))); +} + +TesterType ExprManager::mkTesterType(Type domain) const { + NodeManagerScope nms(d_nodeManager); + return Type(d_nodeManager, new TypeNode(d_nodeManager->mkTesterType(*domain.d_typeNode))); +} + +SortType ExprManager::mkSort(const std::string& name, uint32_t flags) const { + NodeManagerScope nms(d_nodeManager); + return SortType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name, flags)))); +} + +SortConstructorType ExprManager::mkSortConstructor(const std::string& name, + size_t arity) const { + NodeManagerScope nms(d_nodeManager); + return SortConstructorType(Type(d_nodeManager, + new TypeNode(d_nodeManager->mkSortConstructor(name, arity)))); +} + +/* - not in release 1.0 +Type ExprManager::mkPredicateSubtype(Expr lambda) + throw(TypeCheckingException) { + NodeManagerScope nms(d_nodeManager); + try { + return PredicateSubtype(Type(d_nodeManager, + new TypeNode(d_nodeManager->mkPredicateSubtype(lambda)))); + } catch (const TypeCheckingExceptionPrivate& e) { + throw TypeCheckingException(this, &e); + } +} +*/ + +/* - not in release 1.0 +Type ExprManager::mkPredicateSubtype(Expr lambda, Expr witness) + throw(TypeCheckingException) { + NodeManagerScope nms(d_nodeManager); + try { + return PredicateSubtype(Type(d_nodeManager, + new TypeNode(d_nodeManager->mkPredicateSubtype(lambda, witness)))); + } catch (const TypeCheckingExceptionPrivate& e) { + throw TypeCheckingException(this, &e); + } +} +*/ + +Type ExprManager::mkSubrangeType(const SubrangeBounds& bounds) + throw(TypeCheckingException) { + NodeManagerScope nms(d_nodeManager); + try { + return SubrangeType(Type(d_nodeManager, + new TypeNode(d_nodeManager->mkSubrangeType(bounds)))); + } catch (const TypeCheckingExceptionPrivate& e) { + throw TypeCheckingException(this, &e); + } +} + +/** + * Get the type for the given Expr and optionally do type checking. + * + * Initial type computation will be near-constant time if + * type checking is not requested. Results are memoized, so that + * subsequent calls to getType() without type checking will be + * constant time. + * + * Initial type checking is linear in the size of the expression. + * Again, the results are memoized, so that subsequent calls to + * getType(), with or without type checking, will be constant + * time. + * + * NOTE: A TypeCheckingException can be thrown even when type + * checking is not requested. getType() will always return a + * valid and correct type and, thus, an exception will be thrown + * when no valid or correct type can be computed (e.g., if the + * arguments to a bit-vector operation aren't bit-vectors). When + * type checking is not requested, getType() will do the minimum + * amount of checking required to return a valid result. + * + * @param e the Expr for which we want a type + * @param check whether we should check the type as we compute it + * (default: false) + */ +Type ExprManager::getType(Expr e, bool check) throw (TypeCheckingException) { + NodeManagerScope nms(d_nodeManager); + Type t; + try { + t = Type(d_nodeManager, + new TypeNode(d_nodeManager->getType(e.getNode(), check))); + } catch (const TypeCheckingExceptionPrivate& e) { + throw TypeCheckingException(this, &e); + } + return t; +} + +Expr ExprManager::mkVar(const std::string& name, Type type, uint32_t flags) { + Assert(NodeManager::currentNM() == NULL, "ExprManager::mkVar() should only be called externally, not from within CVC4 code. Please use mkSkolem()."); + NodeManagerScope nms(d_nodeManager); + Node* n = d_nodeManager->mkVarPtr(name, *type.d_typeNode, flags); + Debug("nm") << "set " << name << " on " << *n << std::endl; + INC_STAT_VAR(type, false); + return Expr(this, n); +} + +Expr ExprManager::mkVar(Type type, uint32_t flags) { + Assert(NodeManager::currentNM() == NULL, "ExprManager::mkVar() should only be called externally, not from within CVC4 code. Please use mkSkolem()."); + NodeManagerScope nms(d_nodeManager); + INC_STAT_VAR(type, false); + return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode, flags)); +} + +Expr ExprManager::mkBoundVar(const std::string& name, Type type) { + NodeManagerScope nms(d_nodeManager); + Node* n = d_nodeManager->mkBoundVarPtr(name, *type.d_typeNode); + Debug("nm") << "set " << name << " on " << *n << std::endl; + INC_STAT_VAR(type, true); + return Expr(this, n); +} + +Expr ExprManager::mkBoundVar(Type type) { + NodeManagerScope nms(d_nodeManager); + INC_STAT_VAR(type, true); + return Expr(this, d_nodeManager->mkBoundVarPtr(*type.d_typeNode)); +} + +Expr ExprManager::mkAssociative(Kind kind, + const std::vector& children) { + CheckArgument( kind::isAssociative(kind), kind, + "Illegal kind in mkAssociative: %s", + kind::kindToString(kind).c_str()); + + NodeManagerScope nms(d_nodeManager); + const unsigned int max = maxArity(kind); + const unsigned int min = minArity(kind); + unsigned int numChildren = children.size(); + + /* If the number of children is within bounds, then there's nothing to do. */ + if( numChildren <= max ) { + return mkExpr(kind,children); + } + + std::vector::const_iterator it = children.begin() ; + std::vector::const_iterator end = children.end() ; + + /* The new top-level children and the children of each sub node */ + std::vector newChildren; + std::vector subChildren; + + while( it != end && numChildren > max ) { + /* Grab the next max children and make a node for them. */ + for( std::vector::const_iterator next = it + max; + it != next; + ++it, --numChildren ) { + subChildren.push_back(it->getNode()); + } + Node subNode = d_nodeManager->mkNode(kind,subChildren); + newChildren.push_back(subNode); + + subChildren.clear(); + } + + /* If there's children left, "top off" the Expr. */ + if(numChildren > 0) { + /* If the leftovers are too few, just copy them into newChildren; + * otherwise make a new sub-node */ + if(numChildren < min) { + for(; it != end; ++it) { + newChildren.push_back(it->getNode()); + } + } else { + for(; it != end; ++it) { + subChildren.push_back(it->getNode()); + } + Node subNode = d_nodeManager->mkNode(kind, subChildren); + newChildren.push_back(subNode); + } + } + + /* It's inconceivable we could have enough children for this to fail + * (more than 2^32, in most cases?). */ + AlwaysAssert( newChildren.size() <= max, + "Too many new children in mkAssociative" ); + + /* It would be really weird if this happened (it would require + * min > 2, for one thing), but let's make sure. */ + AlwaysAssert( newChildren.size() >= min, + "Too few new children in mkAssociative" ); + + return Expr(this, d_nodeManager->mkNodePtr(kind,newChildren) ); +} + +unsigned ExprManager::minArity(Kind kind) { + return metakind::getLowerBoundForKind(kind); +} + +unsigned ExprManager::maxArity(Kind kind) { + return metakind::getUpperBoundForKind(kind); +} + +NodeManager* ExprManager::getNodeManager() const { + return d_nodeManager; +} + +Statistics ExprManager::getStatistics() const throw() { + return Statistics(*d_nodeManager->getStatisticsRegistry()); +} + +SExpr ExprManager::getStatistic(const std::string& name) const throw() { + return d_nodeManager->getStatisticsRegistry()->getStatistic(name); +} + +namespace expr { + +Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap); + +TypeNode exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* to, ExprManagerMapCollection& vmap) { + Debug("export") << "type: " << n << " " << n.getId() << std::endl; + if(theory::kindToTheoryId(n.getKind()) == theory::THEORY_DATATYPES) { + throw ExportUnsupportedException + ("export of types belonging to theory of DATATYPES kinds unsupported"); + } + if(n.getMetaKind() == kind::metakind::PARAMETERIZED && + n.getKind() != kind::SORT_TYPE) { + throw ExportUnsupportedException + ("export of PARAMETERIZED-kinded types (other than SORT_KIND) not supported"); + } + if(n.getKind() == kind::TYPE_CONSTANT) { + return to->mkTypeConst(n.getConst()); + } else if(n.getKind() == kind::BITVECTOR_TYPE) { + return to->mkBitVectorType(n.getConst()); + } else if(n.getKind() == kind::SUBRANGE_TYPE) { + return to->mkSubrangeType(n.getSubrangeBounds()); + } + Type from_t = from->toType(n); + Type& to_t = vmap.d_typeMap[from_t]; + if(! to_t.isNull()) { + Debug("export") << "+ mapped `" << from_t << "' to `" << to_t << "'" << std::endl; + return *Type::getTypeNode(to_t); + } + NodeBuilder<> children(to, n.getKind()); + if(n.getKind() == kind::SORT_TYPE) { + Debug("export") << "type: operator: " << n.getOperator() << std::endl; + // make a new sort tag in target node manager + Node sortTag = NodeBuilder<0>(to, kind::SORT_TAG); + children << sortTag; + } + for(TypeNode::iterator i = n.begin(), i_end = n.end(); i != i_end; ++i) { + Debug("export") << "type: child: " << *i << std::endl; + children << exportTypeInternal(*i, from, to, vmap); + } + TypeNode out = children.constructTypeNode();// FIXME thread safety + to_t = to->toType(out); + return out; +}/* exportTypeInternal() */ + +}/* CVC4::expr namespace */ + +Type ExprManager::exportType(const Type& t, ExprManager* em, ExprManagerMapCollection& vmap) { + Assert(t.d_nodeManager != em->d_nodeManager, + "Can't export a Type to the same ExprManager"); + NodeManagerScope ems(t.d_nodeManager); + return Type(em->d_nodeManager, + new TypeNode(expr::exportTypeInternal(*t.d_typeNode, t.d_nodeManager, em->d_nodeManager, vmap))); +} + +${mkConst_implementations} + +}/* CVC4 namespace */ diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 2fabea0ff..8acb7489f 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -139,6 +139,9 @@ public: /** Get the type for integers */ IntegerType integerType() const; + /** Get the type for rounding modes */ + RoundingModeType roundingModeType() const; + /** * Make a unary expression of a given kind (NOT, BVNOT, ...). * @param kind the kind of expression @@ -361,6 +364,9 @@ public: */ SExprType mkSExprType(const std::vector& types); + /** Make a type representing a floating-point type with the given parameters. */ + FloatingPointType mkFloatingPointType(unsigned exp, unsigned sig) const; + /** Make a type representing a bit-vector of the given size. */ BitVectorType mkBitVectorType(unsigned size) const; diff --git a/src/expr/expr_manager_template.h.orig b/src/expr/expr_manager_template.h.orig new file mode 100644 index 000000000..2fabea0ff --- /dev/null +++ b/src/expr/expr_manager_template.h.orig @@ -0,0 +1,572 @@ +/********************* */ +/*! \file expr_manager_template.h + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: Dejan Jovanovic + ** Minor contributors (to current version): Andrew Reynolds, Kshitij Bansal, Tim King, Christopher L. Conway + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Public-facing expression manager interface + ** + ** Public-facing expression manager interface. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__EXPR_MANAGER_H +#define __CVC4__EXPR_MANAGER_H + +#include + +#include "expr/kind.h" +#include "expr/type.h" +#include "expr/expr.h" +#include "util/subrange_bound.h" +#include "util/statistics.h" +#include "util/sexpr.h" + +${includes} + +// This is a hack, but an important one: if there's an error, the +// compiler directs the user to the template file instead of the +// generated one. We don't want the user to modify the generated one, +// since it'll get overwritten on a later build. +#line 38 "${template}" + +namespace CVC4 { + +class Expr; +class SmtEngine; +class NodeManager; +class Options; +class IntStat; +struct ExprManagerMapCollection; +class StatisticsRegistry; +class ResourceManager; + +namespace expr { + namespace pickle { + class Pickler; + }/* CVC4::expr::pickle namespace */ +}/* CVC4::expr namespace */ + +namespace stats { + StatisticsRegistry* getStatisticsRegistry(ExprManager*); +}/* CVC4::stats namespace */ + +class CVC4_PUBLIC ExprManager { +private: + /** The internal node manager */ + NodeManager* d_nodeManager; + + /** Counts of expressions and variables created of a given kind */ + IntStat* d_exprStatisticsVars[LAST_TYPE]; + IntStat* d_exprStatistics[kind::LAST_KIND]; + + /** + * Returns the internal node manager. This should only be used by + * internal users, i.e. the friend classes. + */ + NodeManager* getNodeManager() const; + + /** + * Check some things about a newly-created DatatypeType. + */ + void checkResolvedDatatype(DatatypeType dtt) const; + + /** + * SmtEngine will use all the internals, so it will grab the + * NodeManager. + */ + friend class SmtEngine; + + /** ExprManagerScope reaches in to get the NodeManager */ + friend class ExprManagerScope; + + /** NodeManager reaches in to get the NodeManager */ + friend class NodeManager; + + /** Statistics reach in to get the StatisticsRegistry */ + friend ::CVC4::StatisticsRegistry* ::CVC4::stats::getStatisticsRegistry(ExprManager*); + + /** Get the underlying statistics registry. */ + StatisticsRegistry* getStatisticsRegistry() throw(); + + // undefined, private copy constructor and assignment op (disallow copy) + ExprManager(const ExprManager&) CVC4_UNDEFINED; + ExprManager& operator=(const ExprManager&) CVC4_UNDEFINED; + +public: + + /** + * Creates an expression manager with default options. + */ + ExprManager(); + + /** + * Creates an expression manager. + * + * @param options the earlyTypeChecking field is used to configure + * whether to do at Expr creation time. + */ + explicit ExprManager(const Options& options); + + /** + * Destroys the expression manager. No will be deallocated at this point, so + * any expression references that used to be managed by this expression + * manager and are left-over are bad. + */ + ~ExprManager() throw(); + + /** Get this expr manager's options */ + const Options& getOptions() const; + + /** Get this expr manager's resource manager */ + ResourceManager* getResourceManager() throw(); + + /** Get the type for booleans */ + BooleanType booleanType() const; + + /** Get the type for strings. */ + StringType stringType() const; + + /** Get the type for reals. */ + RealType realType() const; + + /** Get the type for integers */ + IntegerType integerType() const; + + /** + * Make a unary expression of a given kind (NOT, BVNOT, ...). + * @param kind the kind of expression + * @param child1 kind the kind of expression + * @return the expression + */ + Expr mkExpr(Kind kind, Expr child1); + + /** + * Make a binary expression of a given kind (AND, PLUS, ...). + * @param kind the kind of expression + * @param child1 the first child of the new expression + * @param child2 the second child of the new expression + * @return the expression + */ + Expr mkExpr(Kind kind, Expr child1, Expr child2); + + /** + * Make a 3-ary expression of a given kind (AND, PLUS, ...). + * @param kind the kind of expression + * @param child1 the first child of the new expression + * @param child2 the second child of the new expression + * @param child3 the third child of the new expression + * @return the expression + */ + Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3); + + /** + * Make a 4-ary expression of a given kind (AND, PLUS, ...). + * @param kind the kind of expression + * @param child1 the first child of the new expression + * @param child2 the second child of the new expression + * @param child3 the third child of the new expression + * @param child4 the fourth child of the new expression + * @return the expression + */ + Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4); + + /** + * Make a 5-ary expression of a given kind (AND, PLUS, ...). + * @param kind the kind of expression + * @param child1 the first child of the new expression + * @param child2 the second child of the new expression + * @param child3 the third child of the new expression + * @param child4 the fourth child of the new expression + * @param child5 the fifth child of the new expression + * @return the expression + */ + Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, + Expr child5); + + /** + * Make an n-ary expression of given kind given a vector of its + * children + * + * @param kind the kind of expression to build + * @param children the subexpressions + * @return the n-ary expression + */ + Expr mkExpr(Kind kind, const std::vector& children); + + /** + * Make an n-ary expression of given kind given a first arg and + * a vector of its remaining children (this can be useful where the + * kind is parameterized operator, so the first arg is really an + * arg to the kind to construct an operator) + * + * @param kind the kind of expression to build + * @param child1 the first subexpression + * @param otherChildren the remaining subexpressions + * @return the n-ary expression + */ + Expr mkExpr(Kind kind, Expr child1, const std::vector& otherChildren); + + /** + * Make a nullary parameterized expression with the given operator. + * + * @param opExpr the operator expression + * @return the nullary expression + */ + Expr mkExpr(Expr opExpr); + + /** + * Make a unary parameterized expression with the given operator. + * + * @param opExpr the operator expression + * @param child1 the subexpression + * @return the unary expression + */ + Expr mkExpr(Expr opExpr, Expr child1); + + /** + * Make a binary parameterized expression with the given operator. + * + * @param opExpr the operator expression + * @param child1 the first subexpression + * @param child2 the second subexpression + * @return the binary expression + */ + Expr mkExpr(Expr opExpr, Expr child1, Expr child2); + + /** + * Make a ternary parameterized expression with the given operator. + * + * @param opExpr the operator expression + * @param child1 the first subexpression + * @param child2 the second subexpression + * @param child3 the third subexpression + * @return the ternary expression + */ + Expr mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3); + + /** + * Make a quaternary parameterized expression with the given operator. + * + * @param opExpr the operator expression + * @param child1 the first subexpression + * @param child2 the second subexpression + * @param child3 the third subexpression + * @param child4 the fourth subexpression + * @return the quaternary expression + */ + Expr mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3, Expr child4); + + /** + * Make a quinary parameterized expression with the given operator. + * + * @param opExpr the operator expression + * @param child1 the first subexpression + * @param child2 the second subexpression + * @param child3 the third subexpression + * @param child4 the fourth subexpression + * @param child5 the fifth subexpression + * @return the quinary expression + */ + Expr mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3, Expr child4, + Expr child5); + + /** + * Make an n-ary expression of given operator to apply and a vector + * of its children + * + * @param opExpr the operator expression + * @param children the subexpressions + * @return the n-ary expression + */ + Expr mkExpr(Expr opExpr, const std::vector& children); + + /** Create a constant of type T */ + template + Expr mkConst(const T&); + + /** + * Create an Expr by applying an associative operator to the children. + * If children.size() is greater than the max arity for + * kind, then the expression will be broken up into + * suitably-sized chunks, taking advantage of the associativity of + * kind. For example, if kind FOO has max arity + * 2, then calling mkAssociative(FOO,a,b,c) will return + * (FOO (FOO a b) c) or (FOO a (FOO b c)). + * The order of the arguments will be preserved in a left-to-right + * traversal of the resulting tree. + */ + Expr mkAssociative(Kind kind, const std::vector& children); + + /** + * Determine whether Exprs of a particular Kind have operators. + * @returns true if Exprs of Kind k have operators. + */ + static bool hasOperator(Kind k); + + /** + * Get the (singleton) operator of an OPERATOR-kinded kind. The + * returned Expr e will have kind BUILTIN, and calling + * e.getConst() will yield k. + */ + Expr operatorOf(Kind k); + + /** Make a function type from domain to range. */ + FunctionType mkFunctionType(Type domain, Type range); + + /** + * Make a function type with input types from argTypes. + * argTypes must have at least one element. + */ + FunctionType mkFunctionType(const std::vector& argTypes, Type range); + + /** + * Make a function type with input types from + * sorts[0..sorts.size()-2] and result type + * sorts[sorts.size()-1]. sorts must have + * at least 2 elements. + */ + FunctionType mkFunctionType(const std::vector& sorts); + + /** + * Make a predicate type with input types from + * sorts. The result with be a function type with range + * BOOLEAN. sorts must have at least one + * element. + */ + FunctionType mkPredicateType(const std::vector& sorts); + + /** + * Make a tuple type with types from + * types[0..types.size()-1]. types must + * have at least one element. + */ + TupleType mkTupleType(const std::vector& types); + + /** + * Make a record type with types from the rec parameter. + */ + RecordType mkRecordType(const Record& rec); + + /** + * Make a symbolic expressiontype with types from + * types[0..types.size()-1]. types may + * have any number of elements. + */ + SExprType mkSExprType(const std::vector& types); + + /** Make a type representing a bit-vector of the given size. */ + BitVectorType mkBitVectorType(unsigned size) const; + + /** Make the type of arrays with the given parameterization. */ + ArrayType mkArrayType(Type indexType, Type constituentType) const; + + /** Make the type of set with the given parameterization. */ + SetType mkSetType(Type elementType) const; + + /** Make a type representing the given datatype. */ + DatatypeType mkDatatypeType(const Datatype& datatype); + + /** + * Make a set of types representing the given datatypes, which may be + * mutually recursive. + */ + std::vector + mkMutualDatatypeTypes(const std::vector& datatypes); + + /** + * Make a set of types representing the given datatypes, which may + * be mutually recursive. unresolvedTypes is a set of SortTypes + * that were used as placeholders in the Datatypes for the Datatypes + * of the same name. This is just a more complicated version of the + * above mkMutualDatatypeTypes() function, but is required to handle + * complex types. + * + * For example, unresolvedTypes might contain the single sort "list" + * (with that name reported from SortType::getName()). The + * datatypes list might have the single datatype + * + * DATATYPE + * list = cons(car:ARRAY INT OF list, cdr:list) | nil; + * END; + * + * To represent the Type of the array, the user had to create a + * placeholder type (an uninterpreted sort) to stand for "list" in + * the type of "car". It is this placeholder sort that should be + * passed in unresolvedTypes. If the datatype was of the simpler + * form: + * + * DATATYPE + * list = cons(car:list, cdr:list) | nil; + * END; + * + * then no complicated Type needs to be created, and the above, + * simpler form of mkMutualDatatypeTypes() is enough. + */ + std::vector + mkMutualDatatypeTypes(const std::vector& datatypes, + const std::set& unresolvedTypes); + + /** + * Make a type representing a constructor with the given parameterization. + */ + ConstructorType mkConstructorType(const DatatypeConstructor& constructor, Type range) const; + + /** Make a type representing a selector with the given parameterization. */ + SelectorType mkSelectorType(Type domain, Type range) const; + + /** Make a type representing a tester with the given parameterization. */ + TesterType mkTesterType(Type domain) const; + + /** Bits for use in mkSort() flags. */ + enum { + SORT_FLAG_NONE = 0, + SORT_FLAG_PLACEHOLDER = 1 + };/* enum */ + + /** Make a new sort with the given name. */ + SortType mkSort(const std::string& name, uint32_t flags = SORT_FLAG_NONE) const; + + /** Make a sort constructor from a name and arity. */ + SortConstructorType mkSortConstructor(const std::string& name, + size_t arity) const; + + /** + * Make a predicate subtype type defined by the given LAMBDA + * expression. A TypeCheckingException can be thrown if lambda is + * not a LAMBDA, or is ill-typed, or if CVC4 fails at proving that + * the resulting predicate subtype is inhabited. + */ + // not in release 1.0 + //Type mkPredicateSubtype(Expr lambda) + // throw(TypeCheckingException); + + /** + * Make a predicate subtype type defined by the given LAMBDA + * expression and whose non-emptiness is witnessed by the given + * witness. A TypeCheckingException can be thrown if lambda is not + * a LAMBDA, or is ill-typed, or if the witness is not a witness or + * ill-typed. + */ + // not in release 1.0 + //Type mkPredicateSubtype(Expr lambda, Expr witness) + // throw(TypeCheckingException); + + /** + * Make an integer subrange type as defined by the argument. + */ + Type mkSubrangeType(const SubrangeBounds& bounds) + throw(TypeCheckingException); + + /** Get the type of an expression */ + Type getType(Expr e, bool check = false) + throw(TypeCheckingException); + + /** Bits for use in mkVar() flags. */ + enum { + VAR_FLAG_NONE = 0, + VAR_FLAG_GLOBAL = 1, + VAR_FLAG_DEFINED = 2 + };/* enum */ + + /** + * Create a new, fresh variable. This variable is guaranteed to be + * distinct from every variable thus far in the ExprManager, even + * if it shares a name with another; this is to support any kind of + * scoping policy on top of ExprManager. The SymbolTable class + * can be used to store and lookup symbols by name, if desired. + * + * @param name a name to associate to the fresh new variable + * @param type the type for the new variable + * @param flags - VAR_FLAG_NONE - no flags; + * VAR_FLAG_GLOBAL - whether this variable is to be + * considered "global" or not. Note that this information isn't + * used by the ExprManager, but is passed on to the ExprManager's + * event subscribers like the model-building service; if isGlobal + * is true, this newly-created variable will still available in + * models generated after an intervening pop. + * VAR_FLAG_DEFINED - if this is to be a "defined" symbol, e.g., for + * use with SmtEngine::defineFunction(). This keeps a declaration + * from being emitted in API dumps (since a subsequent definition is + * expected to be dumped instead). + */ + Expr mkVar(const std::string& name, Type type, uint32_t flags = VAR_FLAG_NONE); + + /** + * Create a (nameless) new, fresh variable. This variable is guaranteed + * to be distinct from every variable thus far in the ExprManager. + * + * @param type the type for the new variable + * @param flags - VAR_FLAG_GLOBAL - whether this variable is to be considered "global" + * or not. Note that this information isn't used by the ExprManager, + * but is passed on to the ExprManager's event subscribers like the + * model-building service; if isGlobal is true, this newly-created + * variable will still available in models generated after an + * intervening pop. + */ + Expr mkVar(Type type, uint32_t flags = VAR_FLAG_NONE); + + /** + * Create a new, fresh variable for use in a binder expression + * (the BOUND_VAR_LIST of a FORALL, EXISTS, or LAMBDA). It is + * an error for this bound variable to exist outside of a binder, + * and it should also only be used in a single binder expression. + * That is, two distinct FORALL expressions should use entirely + * disjoint sets of bound variables (however, a single FORALL + * expression can be used in multiple places in a formula without + * a problem). This newly-created bound variable is guaranteed to + * be distinct from every variable thus far in the ExprManager, even + * if it shares a name with another; this is to support any kind of + * scoping policy on top of ExprManager. The SymbolTable class + * can be used to store and lookup symbols by name, if desired. + * + * @param name a name to associate to the fresh new bound variable + * @param type the type for the new bound variable + */ + Expr mkBoundVar(const std::string& name, Type type); + + /** + * Create a (nameless) new, fresh variable for use in a binder + * expression (the BOUND_VAR_LIST of a FORALL, EXISTS, or LAMBDA). + * It is an error for this bound variable to exist outside of a + * binder, and it should also only be used in a single binder + * expression. That is, two distinct FORALL expressions should use + * entirely disjoint sets of bound variables (however, a single FORALL + * expression can be used in multiple places in a formula without + * a problem). This newly-created bound variable is guaranteed to + * be distinct from every variable thus far in the ExprManager. + * + * @param type the type for the new bound variable + */ + Expr mkBoundVar(Type type); + + /** Get a reference to the statistics registry for this ExprManager */ + Statistics getStatistics() const throw(); + + /** Get a reference to the statistics registry for this ExprManager */ + SExpr getStatistic(const std::string& name) const throw(); + + /** Export an expr to a different ExprManager */ + //static Expr exportExpr(const Expr& e, ExprManager* em); + /** Export a type to a different ExprManager */ + static Type exportType(const Type& t, ExprManager* em, ExprManagerMapCollection& vmap); + + /** Returns the minimum arity of the given kind. */ + static unsigned minArity(Kind kind); + + /** Returns the maximum arity of the given kind. */ + static unsigned maxArity(Kind kind); + +};/* class ExprManager */ + +${mkConst_instantiations} + +}/* CVC4 namespace */ + +#endif /* __CVC4__EXPR_MANAGER_H */ diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index f4c3a1999..f52c7732f 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -685,6 +685,9 @@ public: /** Get the (singleton) type for RegExp. */ inline TypeNode regexpType(); + /** Get the (singleton) type for rounding modes. */ + inline TypeNode roundingModeType(); + /** Get the bound var list type. */ inline TypeNode boundVarListType(); @@ -764,6 +767,11 @@ public: */ inline TypeNode mkSExprType(const std::vector& types); + /** Make the type of floating-point with exp bit exponent and + sig bit significand */ + inline TypeNode mkFloatingPointType(unsigned exp, unsigned sig); + inline TypeNode mkFloatingPointType(FloatingPointSize fs); + /** Make the type of bitvectors of size size */ inline TypeNode mkBitVectorType(unsigned size); @@ -980,6 +988,11 @@ inline TypeNode NodeManager::regexpType() { return TypeNode(mkTypeConst(REGEXP_TYPE)); } +/** Get the (singleton) type for rounding modes. */ +inline TypeNode NodeManager::roundingModeType() { + return TypeNode(mkTypeConst(ROUNDINGMODE_TYPE)); +} + /** Get the bound var list type. */ inline TypeNode NodeManager::boundVarListType() { return TypeNode(mkTypeConst(BOUND_VAR_LIST_TYPE)); @@ -1066,6 +1079,14 @@ inline TypeNode NodeManager::mkBitVectorType(unsigned size) { return TypeNode(mkTypeConst(BitVectorSize(size))); } +inline TypeNode NodeManager::mkFloatingPointType(unsigned exp, unsigned sig) { + return TypeNode(mkTypeConst(FloatingPointSize(exp,sig))); +} + +inline TypeNode NodeManager::mkFloatingPointType(FloatingPointSize fs) { + return TypeNode(mkTypeConst(fs)); +} + inline TypeNode NodeManager::mkArrayType(TypeNode indexType, TypeNode constituentType) { CheckArgument(!indexType.isNull(), indexType, diff --git a/src/expr/node_manager.h.orig b/src/expr/node_manager.h.orig new file mode 100644 index 000000000..f4c3a1999 --- /dev/null +++ b/src/expr/node_manager.h.orig @@ -0,0 +1,1498 @@ +/********************* */ +/*! \file node_manager.h + ** \verbatim + ** Original author: Dejan Jovanovic + ** Major contributors: Christopher L. Conway, Morgan Deters + ** Minor contributors (to current version): ACSYS, Tianyi Liang, Kshitij Bansal, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief A manager for Nodes + ** + ** A manager for Nodes. + ** + ** Reviewed by Chris Conway, Apr 5 2010 (bug #65). + **/ + +#include "cvc4_private.h" + +/* circular dependency; force node.h first */ +//#include "expr/attribute.h" +#include "expr/node.h" +#include "expr/type_node.h" +#include "expr/expr.h" +#include "expr/expr_manager.h" + +#ifndef __CVC4__NODE_MANAGER_H +#define __CVC4__NODE_MANAGER_H + +#include +#include +#include + +#include "expr/kind.h" +#include "expr/metakind.h" +#include "expr/node_value.h" +#include "util/subrange_bound.h" +#include "util/tls.h" +#include "options/options.h" + +namespace CVC4 { + +class StatisticsRegistry; +class ResourceManager; + +namespace expr { + namespace attr { + class AttributeUniqueId; + class AttributeManager; + }/* CVC4::expr::attr namespace */ + + class TypeChecker; +}/* CVC4::expr namespace */ + +/** + * An interface that an interested party can implement and then subscribe + * to NodeManager events via NodeManager::subscribeEvents(this). + */ +class NodeManagerListener { +public: + virtual ~NodeManagerListener() { } + virtual void nmNotifyNewSort(TypeNode tn, uint32_t flags) { } + virtual void nmNotifyNewSortConstructor(TypeNode tn) { } + virtual void nmNotifyInstantiateSortConstructor(TypeNode ctor, TypeNode sort, uint32_t flags) { } + virtual void nmNotifyNewDatatypes(const std::vector& datatypes) { } + virtual void nmNotifyNewVar(TNode n, uint32_t flags) { } + virtual void nmNotifyNewSkolem(TNode n, const std::string& comment, uint32_t flags) { } + /** + * Notify a listener of a Node that's being GCed. If this function stores a reference + * to the Node somewhere, very bad things will happen. + */ + virtual void nmNotifyDeleteNode(TNode n) { } +};/* class NodeManagerListener */ + +class NodeManager { + template friend class CVC4::NodeBuilder; + friend class NodeManagerScope; + friend class expr::NodeValue; + friend class expr::TypeChecker; + + // friends so they can access mkVar() here, which is private + friend Expr ExprManager::mkVar(const std::string&, Type, uint32_t flags); + friend Expr ExprManager::mkVar(Type, uint32_t flags); + + // friend so it can access NodeManager's d_listeners and notify clients + friend std::vector ExprManager::mkMutualDatatypeTypes(const std::vector&, const std::set&); + + /** Predicate for use with STL algorithms */ + struct NodeValueReferenceCountNonZero { + bool operator()(expr::NodeValue* nv) { return nv->d_rc > 0; } + }; + + typedef __gnu_cxx::hash_set NodeValuePool; + typedef __gnu_cxx::hash_set ZombieSet; + + static CVC4_THREADLOCAL(NodeManager*) s_current; + + Options* d_options; + StatisticsRegistry* d_statisticsRegistry; + ResourceManager* d_resourceManager; + + NodeValuePool d_nodeValuePool; + + size_t next_id; + + expr::attr::AttributeManager* d_attrManager; + + /** The associated ExprManager */ + ExprManager* d_exprManager; + + /** + * The node value we're currently freeing. This unique node value + * is permitted to have outstanding TNodes to it (in "soft" + * contexts, like as a key in attribute tables), even though + * normally it's an error to have a TNode to a node value with a + * reference count of 0. Being "under deletion" also enables + * assertions that inc() is not called on it. (A poorly-behaving + * attribute cleanup function could otherwise create a "Node" that + * points to the node value that is in the process of being deleted, + * springing it back to life.) + */ + expr::NodeValue* d_nodeUnderDeletion; + + /** + * True iff we are in reclaimZombies(). This avoids unnecessary + * recursion; a NodeValue being deleted might zombify other + * NodeValues, but these shouldn't trigger a (recursive) call to + * reclaimZombies(). + */ + bool d_inReclaimZombies; + + /** + * The set of zombie nodes. We may want to revisit this design, as + * we might like to delete nodes in least-recently-used order. But + * we also need to avoid processing a zombie twice. + */ + ZombieSet d_zombies; + + /** + * A set of operator singletons (w.r.t. to this NodeManager + * instance) for operators. Conceptually, Nodes with kind, say, + * PLUS, are APPLYs of a PLUS operator to arguments. This array + * holds the set of operators for these things. A PLUS operator is + * a Node with kind "BUILTIN", and if you call + * plusOperator->getConst(), you get kind::PLUS back. + */ + Node d_operators[kind::LAST_KIND]; + + /** + * A list of subscribers for NodeManager events. + */ + std::vector d_listeners; + + /** + * A map of tuple and record types to their corresponding datatype. + */ + std::hash_map d_tupleAndRecordTypes; + + /** + * Keep a count of all abstract values produced by this NodeManager. + * Abstract values have a type attribute, so if multiple SmtEngines + * are attached to this NodeManager, we don't want their abstract + * values to overlap. + */ + unsigned d_abstractValueCount; + + /** + * A counter used to produce unique skolem names. + * + * Note that it is NOT incremented when skolems are created using + * SKOLEM_EXACT_NAME, so it is NOT a count of the skolems produced + * by this node manager. + */ + unsigned d_skolemCounter; + + /** + * Look up a NodeValue in the pool associated to this NodeManager. + * The NodeValue argument need not be a "completely-constructed" + * NodeValue. In particular, "non-inlined" constants are permitted + * (see below). + * + * For non-CONSTANT metakinds, nv's d_kind and d_nchildren should be + * correctly set, and d_children[0..n-1] should be valid (extant) + * NodeValues for lookup. + * + * For CONSTANT metakinds, nv's d_kind should be set correctly. + * Normally a CONSTANT would have d_nchildren == 0 and the constant + * value inlined in the d_children space. However, here we permit + * "non-inlined" NodeValues to avoid unnecessary copying. For + * these, d_nchildren == 1, and d_nchildren is a pointer to the + * constant value. + * + * The point of this complex design is to permit efficient lookups + * (without fully constructing a NodeValue). In the case that the + * argument is not fully constructed, and this function returns + * NULL, the caller should fully construct an equivalent one before + * calling poolInsert(). NON-FULLY-CONSTRUCTED NODEVALUES are not + * permitted in the pool! + */ + inline expr::NodeValue* poolLookup(expr::NodeValue* nv) const; + + /** + * Insert a NodeValue into the NodeManager's pool. + * + * It is an error to insert a NodeValue already in the pool. + * Enquire first with poolLookup(). + */ + inline void poolInsert(expr::NodeValue* nv); + + /** + * Remove a NodeValue from the NodeManager's pool. + * + * It is an error to request the removal of a NodeValue from the + * pool that is not in the pool. + */ + inline void poolRemove(expr::NodeValue* nv); + + /** + * Determine if nv is currently being deleted by the NodeManager. + */ + inline bool isCurrentlyDeleting(const expr::NodeValue* nv) const { + return d_nodeUnderDeletion == nv; + } + + /** + * Register a NodeValue as a zombie. + */ + inline void markForDeletion(expr::NodeValue* nv) { + Assert(nv->d_rc == 0); + + // if d_reclaiming is set, make sure we don't call + // reclaimZombies(), because it's already running. + if(Debug.isOn("gc")) { + Debug("gc") << "zombifying node value " << nv + << " [" << nv->d_id << "]: "; + nv->printAst(Debug("gc")); + Debug("gc") << (d_inReclaimZombies ? " [CURRENTLY-RECLAIMING]" : "") + << std::endl; + } + d_zombies.insert(nv);// FIXME multithreading + + if(safeToReclaimZombies()) { + if(d_zombies.size() > 5000) { + reclaimZombies(); + } + } + } + + /** + * Reclaim all zombies. + */ + void reclaimZombies(); + + /** + * It is safe to collect zombies. + */ + bool safeToReclaimZombies() const; + + /** + * This template gives a mechanism to stack-allocate a NodeValue + * with enough space for N children (where N is a compile-time + * constant). You use it like this: + * + * NVStorage<4> nvStorage; + * NodeValue& nvStack = reinterpret_cast(nvStorage); + * + * ...and then you can use nvStack as a NodeValue that you know has + * room for 4 children. + */ + template + struct NVStorage { + expr::NodeValue nv; + expr::NodeValue* child[N]; + };/* struct NodeManager::NVStorage */ + + /* A note on isAtomic() and isAtomicFormula() (in CVC3 parlance).. + * + * It has been decided for now to hold off on implementations of + * these functions, as they may only be needed in CNF conversion, + * where it's pointless to do a lazy isAtomic determination by + * searching through the DAG, and storing it, since the result will + * only be used once. For more details see the 4/27/2010 CVC4 + * developer's meeting notes at: + * + * http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_April_27,_2010#isAtomic.28.29_and_isAtomicFormula.28.29 + */ + // bool containsDecision(TNode); // is "atomic" + // bool properlyContainsDecision(TNode); // all children are atomic + + // undefined private copy constructor (disallow copy) + NodeManager(const NodeManager&) CVC4_UNDEFINED; + + void init(); + + /** + * Create a variable with the given name and type. NOTE that no + * lookup is done on the name. If you mkVar("a", type) and then + * mkVar("a", type) again, you have two variables. The NodeManager + * version of this is private to avoid internal uses of mkVar() from + * within CVC4. Such uses should employ mkSkolem() instead. + */ + Node mkVar(const std::string& name, const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE); + Node* mkVarPtr(const std::string& name, const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE); + + /** Create a variable with the given type. */ + Node mkVar(const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE); + Node* mkVarPtr(const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE); + +public: + + explicit NodeManager(ExprManager* exprManager); + explicit NodeManager(ExprManager* exprManager, const Options& options); + ~NodeManager(); + + /** The node manager in the current public-facing CVC4 library context */ + static NodeManager* currentNM() { return s_current; } + /** The resource manager associated with the current node manager */ + static ResourceManager* currentResourceManager() { return s_current->d_resourceManager; } + + /** Get this node manager's options (const version) */ + const Options& getOptions() const { + return *d_options; + } + + /** Get this node manager's options (non-const version) */ + Options& getOptions() { + return *d_options; + } + + /** Get this node manager's resource manager */ + ResourceManager* getResourceManager() throw() { return d_resourceManager; } + + /** Get this node manager's statistics registry */ + StatisticsRegistry* getStatisticsRegistry() const throw() { + return d_statisticsRegistry; + } + + /** Subscribe to NodeManager events */ + void subscribeEvents(NodeManagerListener* listener) { + Assert(std::find(d_listeners.begin(), d_listeners.end(), listener) == d_listeners.end(), "listener already subscribed"); + d_listeners.push_back(listener); + } + + /** Unsubscribe from NodeManager events */ + void unsubscribeEvents(NodeManagerListener* listener) { + std::vector::iterator elt = std::find(d_listeners.begin(), d_listeners.end(), listener); + Assert(elt != d_listeners.end(), "listener not subscribed"); + d_listeners.erase(elt); + } + + /** Get a Kind from an operator expression */ + static inline Kind operatorToKind(TNode n); + + // general expression-builders + + /** Create a node with one child. */ + Node mkNode(Kind kind, TNode child1); + Node* mkNodePtr(Kind kind, TNode child1); + + /** Create a node with two children. */ + Node mkNode(Kind kind, TNode child1, TNode child2); + Node* mkNodePtr(Kind kind, TNode child1, TNode child2); + + /** Create a node with three children. */ + Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3); + Node* mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3); + + /** Create a node with four children. */ + Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3, + TNode child4); + Node* mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3, + TNode child4); + + /** Create a node with five children. */ + Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3, + TNode child4, TNode child5); + Node* mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3, + TNode child4, TNode child5); + + /** Create a node with an arbitrary number of children. */ + template + Node mkNode(Kind kind, const std::vector >& children); + template + Node* mkNodePtr(Kind kind, const std::vector >& children); + + /** Create a node (with no children) by operator. */ + Node mkNode(TNode opNode); + Node* mkNodePtr(TNode opNode); + + /** Create a node with one child by operator. */ + Node mkNode(TNode opNode, TNode child1); + Node* mkNodePtr(TNode opNode, TNode child1); + + /** Create a node with two children by operator. */ + Node mkNode(TNode opNode, TNode child1, TNode child2); + Node* mkNodePtr(TNode opNode, TNode child1, TNode child2); + + /** Create a node with three children by operator. */ + Node mkNode(TNode opNode, TNode child1, TNode child2, TNode child3); + Node* mkNodePtr(TNode opNode, TNode child1, TNode child2, TNode child3); + + /** Create a node with four children by operator. */ + Node mkNode(TNode opNode, TNode child1, TNode child2, TNode child3, + TNode child4); + Node* mkNodePtr(TNode opNode, TNode child1, TNode child2, TNode child3, + TNode child4); + + /** Create a node with five children by operator. */ + Node mkNode(TNode opNode, TNode child1, TNode child2, TNode child3, + TNode child4, TNode child5); + Node* mkNodePtr(TNode opNode, TNode child1, TNode child2, TNode child3, + TNode child4, TNode child5); + + /** Create a node by applying an operator to the children. */ + template + Node mkNode(TNode opNode, const std::vector >& children); + template + Node* mkNodePtr(TNode opNode, const std::vector >& children); + + Node mkBoundVar(const std::string& name, const TypeNode& type); + Node* mkBoundVarPtr(const std::string& name, const TypeNode& type); + + Node mkBoundVar(const TypeNode& type); + Node* mkBoundVarPtr(const TypeNode& type); + + /** + * Optional flags used to control behavior of NodeManager::mkSkolem(). + * They should be composed with a bitwise OR (e.g., + * "SKOLEM_NO_NOTIFY | SKOLEM_EXACT_NAME"). Of course, SKOLEM_DEFAULT + * cannot be composed in such a manner. + */ + enum SkolemFlags { + SKOLEM_DEFAULT = 0, /**< default behavior */ + SKOLEM_NO_NOTIFY = 1, /**< do not notify subscribers */ + SKOLEM_EXACT_NAME = 2,/**< do not make the name unique by adding the id */ + SKOLEM_IS_GLOBAL = 4 /**< global vars appear in models even after a pop */ + };/* enum SkolemFlags */ + + /** + * Create a skolem constant with the given name, type, and comment. + * + * @param prefix the name of the new skolem variable is the prefix + * appended with a unique ID. This way a family of skolem variables + * can be made with unique identifiers, used in dump, tracing, and + * debugging output. Use SKOLEM_EXECT_NAME flag if you don't want + * a unique ID appended and use prefix as the name. + * + * @param type the type of the skolem variable to create + * + * @param comment a comment for dumping output; if declarations are + * being dumped, this is included in a comment before the declaration + * and can be quite useful for debugging + * + * @param flags an optional mask of bits from SkolemFlags to control + * mkSkolem() behavior + */ + Node mkSkolem(const std::string& prefix, const TypeNode& type, + const std::string& comment = "", int flags = SKOLEM_DEFAULT); + + /** Create a instantiation constant with the given type. */ + Node mkInstConstant(const TypeNode& type); + + /** Make a new abstract value with the given type. */ + Node mkAbstractValue(const TypeNode& type); + + /** + * Create a constant of type T. It will have the appropriate + * CONST_* kind defined for T. + */ + template + Node mkConst(const T&); + + template + TypeNode mkTypeConst(const T&); + + template + NodeClass mkConstInternal(const T&); + + /** Create a node with children. */ + TypeNode mkTypeNode(Kind kind, TypeNode child1); + TypeNode mkTypeNode(Kind kind, TypeNode child1, TypeNode child2); + TypeNode mkTypeNode(Kind kind, TypeNode child1, TypeNode child2, + TypeNode child3); + TypeNode mkTypeNode(Kind kind, const std::vector& children); + + /** + * Determine whether Nodes of a particular Kind have operators. + * @returns true if Nodes of Kind k have operators. + */ + static inline bool hasOperator(Kind k); + + /** + * Get the (singleton) operator of an OPERATOR-kinded kind. The + * returned node n will have kind BUILTIN, and calling + * n.getConst() will yield k. + */ + inline TNode operatorOf(Kind k) { + AssertArgument( kind::metaKindOf(k) == kind::metakind::OPERATOR, k, + "Kind is not an OPERATOR-kinded kind " + "in NodeManager::operatorOf()" ); + return d_operators[k]; + } + + /** + * Retrieve an attribute for a node. + * + * @param nv the node value + * @param attr an instance of the attribute kind to retrieve. + * @returns the attribute, if set, or a default-constructed + * AttrKind::value_type if not. + */ + template + inline typename AttrKind::value_type getAttribute(expr::NodeValue* nv, + const AttrKind& attr) const; + + /** + * Check whether an attribute is set for a node. + * + * @param nv the node value + * @param attr an instance of the attribute kind to check + * @returns true iff attr is set for + * nv. + */ + template + inline bool hasAttribute(expr::NodeValue* nv, + const AttrKind& attr) const; + + /** + * Check whether an attribute is set for a node, and, if so, + * retrieve it. + * + * @param nv the node value + * @param attr an instance of the attribute kind to check + * @param value a reference to an object of the attribute's value type. + * value will be set to the value of the attribute, if it is + * set for nv; otherwise, it will be set to the default + * value of the attribute. + * @returns true iff attr is set for + * nv. + */ + template + inline bool getAttribute(expr::NodeValue* nv, + const AttrKind& attr, + typename AttrKind::value_type& value) const; + + /** + * Set an attribute for a node. If the node doesn't have the + * attribute, this function assigns one. If the node has one, this + * overwrites it. + * + * @param nv the node value + * @param attr an instance of the attribute kind to set + * @param value the value of attr for nv + */ + template + inline void setAttribute(expr::NodeValue* nv, + const AttrKind& attr, + const typename AttrKind::value_type& value); + + /** + * Retrieve an attribute for a TNode. + * + * @param n the node + * @param attr an instance of the attribute kind to retrieve. + * @returns the attribute, if set, or a default-constructed + * AttrKind::value_type if not. + */ + template + inline typename AttrKind::value_type + getAttribute(TNode n, const AttrKind& attr) const; + + /** + * Check whether an attribute is set for a TNode. + * + * @param n the node + * @param attr an instance of the attribute kind to check + * @returns true iff attr is set for n. + */ + template + inline bool hasAttribute(TNode n, + const AttrKind& attr) const; + + /** + * Check whether an attribute is set for a TNode and, if so, retieve + * it. + * + * @param n the node + * @param attr an instance of the attribute kind to check + * @param value a reference to an object of the attribute's value type. + * value will be set to the value of the attribute, if it is + * set for nv; otherwise, it will be set to the default value of + * the attribute. + * @returns true iff attr is set for n. + */ + template + inline bool getAttribute(TNode n, + const AttrKind& attr, + typename AttrKind::value_type& value) const; + + /** + * Set an attribute for a node. If the node doesn't have the + * attribute, this function assigns one. If the node has one, this + * overwrites it. + * + * @param n the node + * @param attr an instance of the attribute kind to set + * @param value the value of attr for n + */ + template + inline void setAttribute(TNode n, + const AttrKind& attr, + const typename AttrKind::value_type& value); + + /** + * Retrieve an attribute for a TypeNode. + * + * @param n the type node + * @param attr an instance of the attribute kind to retrieve. + * @returns the attribute, if set, or a default-constructed + * AttrKind::value_type if not. + */ + template + inline typename AttrKind::value_type + getAttribute(TypeNode n, const AttrKind& attr) const; + + /** + * Check whether an attribute is set for a TypeNode. + * + * @param n the type node + * @param attr an instance of the attribute kind to check + * @returns true iff attr is set for n. + */ + template + inline bool hasAttribute(TypeNode n, + const AttrKind& attr) const; + + /** + * Check whether an attribute is set for a TypeNode and, if so, retieve + * it. + * + * @param n the type node + * @param attr an instance of the attribute kind to check + * @param value a reference to an object of the attribute's value type. + * value will be set to the value of the attribute, if it is + * set for nv; otherwise, it will be set to the default value of + * the attribute. + * @returns true iff attr is set for n. + */ + template + inline bool getAttribute(TypeNode n, + const AttrKind& attr, + typename AttrKind::value_type& value) const; + + /** + * Set an attribute for a type node. If the node doesn't have the + * attribute, this function assigns one. If the type node has one, + * this overwrites it. + * + * @param n the type node + * @param attr an instance of the attribute kind to set + * @param value the value of attr for n + */ + template + inline void setAttribute(TypeNode n, + const AttrKind& attr, + const typename AttrKind::value_type& value); + + /** Get the (singleton) type for Booleans. */ + inline TypeNode booleanType(); + + /** Get the (singleton) type for integers. */ + inline TypeNode integerType(); + + /** Get the (singleton) type for reals. */ + inline TypeNode realType(); + + /** Get the (singleton) type for strings. */ + inline TypeNode stringType(); + + /** Get the (singleton) type for RegExp. */ + inline TypeNode regexpType(); + + /** Get the bound var list type. */ + inline TypeNode boundVarListType(); + + /** Get the instantiation pattern type. */ + inline TypeNode instPatternType(); + + /** Get the instantiation pattern type. */ + inline TypeNode instPatternListType(); + + /** + * Get the (singleton) type for builtin operators (that is, the type + * of the Node returned from Node::getOperator() when the operator + * is built-in, like EQUAL). */ + inline TypeNode builtinOperatorType(); + + /** + * Make a function type from domain to range. + * + * @param domain the domain type + * @param range the range type + * @returns the functional type domain -> range + */ + inline TypeNode mkFunctionType(const TypeNode& domain, const TypeNode& range); + + /** + * Make a function type with input types from + * argTypes. argTypes must have at least one element. + * + * @param argTypes the domain is a tuple (argTypes[0], ..., argTypes[n]) + * @param range the range type + * @returns the functional type (argTypes[0], ..., argTypes[n]) -> range + */ + inline TypeNode mkFunctionType(const std::vector& argTypes, + const TypeNode& range); + + /** + * Make a function type with input types from + * sorts[0..sorts.size()-2] and result type + * sorts[sorts.size()-1]. sorts must have + * at least 2 elements. + */ + inline TypeNode mkFunctionType(const std::vector& sorts); + + /** + * Make a predicate type with input types from + * sorts. The result with be a function type with range + * BOOLEAN. sorts must have at least one + * element. + */ + inline TypeNode mkPredicateType(const std::vector& sorts); + + /** + * Make a tuple type with types from + * types. types must have at least one + * element. + * + * @param types a vector of types + * @returns the tuple type (types[0], ..., types[n]) + */ + inline TypeNode mkTupleType(const std::vector& types); + + /** + * Make a record type with the description from rec. + * + * @param rec a description of the record + * @returns the record type + */ + inline TypeNode mkRecordType(const Record& rec); + + /** + * Make a symbolic expression type with types from + * types. types may have any number of + * elements. + * + * @param types a vector of types + * @returns the symbolic expression type (types[0], ..., types[n]) + */ + inline TypeNode mkSExprType(const std::vector& types); + + /** Make the type of bitvectors of size size */ + inline TypeNode mkBitVectorType(unsigned size); + + /** Make the type of arrays with the given parameterization */ + inline TypeNode mkArrayType(TypeNode indexType, TypeNode constituentType); + + /** Make the type of arrays with the given parameterization */ + inline TypeNode mkSetType(TypeNode elementType); + + /** Make a type representing a constructor with the given parameterization */ + TypeNode mkConstructorType(const DatatypeConstructor& constructor, TypeNode range); + + /** Make a type representing a selector with the given parameterization */ + inline TypeNode mkSelectorType(TypeNode domain, TypeNode range); + + /** Make a type representing a tester with given parameterization */ + inline TypeNode mkTesterType(TypeNode domain); + + /** Make a new (anonymous) sort of arity 0. */ + TypeNode mkSort(uint32_t flags = ExprManager::SORT_FLAG_NONE); + + /** Make a new sort with the given name of arity 0. */ + TypeNode mkSort(const std::string& name, uint32_t flags = ExprManager::SORT_FLAG_NONE); + + /** Make a new sort by parameterizing the given sort constructor. */ + TypeNode mkSort(TypeNode constructor, + const std::vector& children, + uint32_t flags = ExprManager::SORT_FLAG_NONE); + + /** Make a new sort with the given name and arity. */ + TypeNode mkSortConstructor(const std::string& name, size_t arity); + + /** + * Make a predicate subtype type defined by the given LAMBDA + * expression. A TypeCheckingExceptionPrivate can be thrown if + * lambda is not a LAMBDA, or is ill-typed, or if CVC4 fails at + * proving that the resulting predicate subtype is inhabited. + */ + TypeNode mkPredicateSubtype(Expr lambda) + throw(TypeCheckingExceptionPrivate); + + /** + * Make a predicate subtype type defined by the given LAMBDA + * expression and whose non-emptiness is witnessed by the given + * witness. A TypeCheckingExceptionPrivate can be thrown if lambda + * is not a LAMBDA, or is ill-typed, or if the witness is not a + * witness or ill-typed. + */ + TypeNode mkPredicateSubtype(Expr lambda, Expr witness) + throw(TypeCheckingExceptionPrivate); + + /** + * Make an integer subrange type as defined by the argument. + */ + TypeNode mkSubrangeType(const SubrangeBounds& bounds) + throw(TypeCheckingExceptionPrivate); + + /** + * Given a tuple or record type, get the internal datatype used for + * it. Makes the DatatypeType if necessary. + */ + TypeNode getDatatypeForTupleRecord(TypeNode tupleRecordType); + + /** + * Get the type for the given node and optionally do type checking. + * + * Initial type computation will be near-constant time if + * type checking is not requested. Results are memoized, so that + * subsequent calls to getType() without type checking will be + * constant time. + * + * Initial type checking is linear in the size of the expression. + * Again, the results are memoized, so that subsequent calls to + * getType(), with or without type checking, will be constant + * time. + * + * NOTE: A TypeCheckingException can be thrown even when type + * checking is not requested. getType() will always return a + * valid and correct type and, thus, an exception will be thrown + * when no valid or correct type can be computed (e.g., if the + * arguments to a bit-vector operation aren't bit-vectors). When + * type checking is not requested, getType() will do the minimum + * amount of checking required to return a valid result. + * + * @param n the Node for which we want a type + * @param check whether we should check the type as we compute it + * (default: false) + */ + TypeNode getType(TNode n, bool check = false) + throw(TypeCheckingExceptionPrivate, AssertionException); + + /** + * Convert a node to an expression. Uses the ExprManager + * associated to this NodeManager. + */ + inline Expr toExpr(TNode n); + + /** + * Convert an expression to a node. + */ + static inline Node fromExpr(const Expr& e); + + /** + * Convert a node manager to an expression manager. + */ + inline ExprManager* toExprManager(); + + /** + * Convert an expression manager to a node manager. + */ + static inline NodeManager* fromExprManager(ExprManager* exprManager); + + /** + * Convert a type node to a type. + */ + inline Type toType(TypeNode tn); + + /** + * Convert a type to a type node. + */ + static inline TypeNode fromType(Type t); + + /** Reclaim zombies while there are more than k nodes in the pool (if possible).*/ + void reclaimZombiesUntil(uint32_t k); + + /** Reclaims all zombies (if possible).*/ + void reclaimAllZombies(); + + /** Size of the node pool. */ + size_t poolSize() const; + + /** Deletes a list of attributes from the NM's AttributeManager.*/ + void deleteAttributes(const std::vector< const expr::attr::AttributeUniqueId* >& ids); + + /** + * This function gives developers a hook into the NodeManager. + * This can be changed in node_manager.cpp without recompiling most of cvc4. + * + * debugHook is a debugging only function, and should not be present in + * any published code! + */ + void debugHook(int debugFlag); +};/* class NodeManager */ + +/** + * This class changes the "current" thread-global + * NodeManager when it is created and reinstates the + * previous thread-global NodeManager when it is + * destroyed, effectively maintaining a set of nested + * NodeManager scopes. This is especially useful on + * public-interface calls into the CVC4 library, where CVC4's notion + * of the "current" NodeManager should be set to match + * the calling context. See, for example, the implementations of + * public calls in the ExprManager and + * SmtEngine classes. + * + * The client must be careful to create and destroy + * NodeManagerScope objects in a well-nested manner (such + * as on the stack). You may create a NodeManagerScope + * with new and destroy it with delete, or + * place it as a data member of an object that is, but if the scope of + * these new/delete pairs isn't properly + * maintained, the incorrect "current" NodeManager + * pointer may be restored after a delete. + */ +class NodeManagerScope { + /** The old NodeManager, to be restored on destruction. */ + NodeManager* d_oldNodeManager; + +public: + + NodeManagerScope(NodeManager* nm) : + d_oldNodeManager(NodeManager::s_current) { + // There are corner cases where nm can be NULL and it's ok. + // For example, if you write { Expr e; }, then when the null + // Expr is destructed, there's no active node manager. + //Assert(nm != NULL); + NodeManager::s_current = nm; + Options::s_current = nm ? nm->d_options : NULL; + Debug("current") << "node manager scope: " + << NodeManager::s_current << "\n"; + } + + ~NodeManagerScope() { + NodeManager::s_current = d_oldNodeManager; + Options::s_current = d_oldNodeManager ? d_oldNodeManager->d_options : NULL; + Debug("current") << "node manager scope: " + << "returning to " << NodeManager::s_current << "\n"; + } +};/* class NodeManagerScope */ + +/** Get the (singleton) type for booleans. */ +inline TypeNode NodeManager::booleanType() { + return TypeNode(mkTypeConst(BOOLEAN_TYPE)); +} + +/** Get the (singleton) type for integers. */ +inline TypeNode NodeManager::integerType() { + return TypeNode(mkTypeConst(INTEGER_TYPE)); +} + +/** Get the (singleton) type for reals. */ +inline TypeNode NodeManager::realType() { + return TypeNode(mkTypeConst(REAL_TYPE)); +} + +/** Get the (singleton) type for strings. */ +inline TypeNode NodeManager::stringType() { + return TypeNode(mkTypeConst(STRING_TYPE)); +} + +/** Get the (singleton) type for regexps. */ +inline TypeNode NodeManager::regexpType() { + return TypeNode(mkTypeConst(REGEXP_TYPE)); +} + +/** Get the bound var list type. */ +inline TypeNode NodeManager::boundVarListType() { + return TypeNode(mkTypeConst(BOUND_VAR_LIST_TYPE)); +} + +/** Get the instantiation pattern type. */ +inline TypeNode NodeManager::instPatternType() { + return TypeNode(mkTypeConst(INST_PATTERN_TYPE)); +} + +/** Get the instantiation pattern type. */ +inline TypeNode NodeManager::instPatternListType() { + return TypeNode(mkTypeConst(INST_PATTERN_LIST_TYPE)); +} + +/** Get the (singleton) type for builtin operators. */ +inline TypeNode NodeManager::builtinOperatorType() { + return TypeNode(mkTypeConst(BUILTIN_OPERATOR_TYPE)); +} + +/** Make a function type from domain to range. */ +inline TypeNode NodeManager::mkFunctionType(const TypeNode& domain, const TypeNode& range) { + std::vector sorts; + sorts.push_back(domain); + sorts.push_back(range); + return mkFunctionType(sorts); +} + +inline TypeNode NodeManager::mkFunctionType(const std::vector& argTypes, const TypeNode& range) { + Assert(argTypes.size() >= 1); + std::vector sorts(argTypes); + sorts.push_back(range); + return mkFunctionType(sorts); +} + +inline TypeNode +NodeManager::mkFunctionType(const std::vector& sorts) { + Assert(sorts.size() >= 2); + std::vector sortNodes; + for (unsigned i = 0; i < sorts.size(); ++ i) { + CheckArgument(!sorts[i].isFunctionLike(), sorts, + "cannot create higher-order function types"); + sortNodes.push_back(sorts[i]); + } + return mkTypeNode(kind::FUNCTION_TYPE, sortNodes); +} + +inline TypeNode +NodeManager::mkPredicateType(const std::vector& sorts) { + Assert(sorts.size() >= 1); + std::vector sortNodes; + for (unsigned i = 0; i < sorts.size(); ++ i) { + CheckArgument(!sorts[i].isFunctionLike(), sorts, + "cannot create higher-order function types"); + sortNodes.push_back(sorts[i]); + } + sortNodes.push_back(booleanType()); + return mkTypeNode(kind::FUNCTION_TYPE, sortNodes); +} + +inline TypeNode NodeManager::mkTupleType(const std::vector& types) { + std::vector typeNodes; + for (unsigned i = 0; i < types.size(); ++ i) { + CheckArgument(!types[i].isFunctionLike(), types, + "cannot put function-like types in tuples"); + typeNodes.push_back(types[i]); + } + return mkTypeNode(kind::TUPLE_TYPE, typeNodes); +} + +inline TypeNode NodeManager::mkRecordType(const Record& rec) { + return mkTypeConst(rec); +} + +inline TypeNode NodeManager::mkSExprType(const std::vector& types) { + std::vector typeNodes; + for (unsigned i = 0; i < types.size(); ++ i) { + typeNodes.push_back(types[i]); + } + return mkTypeNode(kind::SEXPR_TYPE, typeNodes); +} + +inline TypeNode NodeManager::mkBitVectorType(unsigned size) { + return TypeNode(mkTypeConst(BitVectorSize(size))); +} + +inline TypeNode NodeManager::mkArrayType(TypeNode indexType, + TypeNode constituentType) { + CheckArgument(!indexType.isNull(), indexType, + "unexpected NULL index type"); + CheckArgument(!constituentType.isNull(), constituentType, + "unexpected NULL constituent type"); + CheckArgument(!indexType.isFunctionLike(), indexType, + "cannot index arrays by a function-like type"); + CheckArgument(!constituentType.isFunctionLike(), constituentType, + "cannot store function-like types in arrays"); + Debug("arrays") << "making array type " << indexType << " " << constituentType << std::endl; + return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType); +} + +inline TypeNode NodeManager::mkSetType(TypeNode elementType) { + CheckArgument(!elementType.isNull(), elementType, + "unexpected NULL element type"); + // TODO: Confirm meaning of isFunctionLike(). --K + CheckArgument(!elementType.isFunctionLike(), elementType, + "cannot store function-like types in sets"); + Debug("sets") << "making sets type " << elementType << std::endl; + return mkTypeNode(kind::SET_TYPE, elementType); +} + +inline TypeNode NodeManager::mkSelectorType(TypeNode domain, TypeNode range) { + CheckArgument(!domain.isFunctionLike(), domain, + "cannot create higher-order function types"); + CheckArgument(!range.isFunctionLike(), range, + "cannot create higher-order function types"); + return mkTypeNode(kind::SELECTOR_TYPE, domain, range); +} + +inline TypeNode NodeManager::mkTesterType(TypeNode domain) { + CheckArgument(!domain.isFunctionLike(), domain, + "cannot create higher-order function types"); + return mkTypeNode(kind::TESTER_TYPE, domain ); +} + +inline expr::NodeValue* NodeManager::poolLookup(expr::NodeValue* nv) const { + NodeValuePool::const_iterator find = d_nodeValuePool.find(nv); + if(find == d_nodeValuePool.end()) { + return NULL; + } else { + return *find; + } +} + +inline void NodeManager::poolInsert(expr::NodeValue* nv) { + Assert(d_nodeValuePool.find(nv) == d_nodeValuePool.end(), + "NodeValue already in the pool!"); + d_nodeValuePool.insert(nv);// FIXME multithreading +} + +inline void NodeManager::poolRemove(expr::NodeValue* nv) { + Assert(d_nodeValuePool.find(nv) != d_nodeValuePool.end(), + "NodeValue is not in the pool!"); + + d_nodeValuePool.erase(nv);// FIXME multithreading +} + +inline Expr NodeManager::toExpr(TNode n) { + return Expr(d_exprManager, new Node(n)); +} + +inline Node NodeManager::fromExpr(const Expr& e) { + return e.getNode(); +} + +inline ExprManager* NodeManager::toExprManager() { + return d_exprManager; +} + +inline NodeManager* NodeManager::fromExprManager(ExprManager* exprManager) { + return exprManager->getNodeManager(); +} + +inline Type NodeManager::toType(TypeNode tn) { + return Type(this, new TypeNode(tn)); +} + +inline TypeNode NodeManager::fromType(Type t) { + return *Type::getTypeNode(t); +} + +}/* CVC4 namespace */ + +#define __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP +#include "expr/metakind.h" +#undef __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP + +#include "expr/node_builder.h" + +namespace CVC4 { + +// general expression-builders + +inline bool NodeManager::hasOperator(Kind k) { + switch(kind::MetaKind mk = kind::metaKindOf(k)) { + + case kind::metakind::INVALID: + case kind::metakind::VARIABLE: + return false; + + case kind::metakind::OPERATOR: + case kind::metakind::PARAMETERIZED: + return true; + + case kind::metakind::CONSTANT: + return false; + + default: + Unhandled(mk); + } +} + +inline Kind NodeManager::operatorToKind(TNode n) { + return kind::operatorToKind(n.d_nv); +} + +inline Node NodeManager::mkNode(Kind kind, TNode child1) { + NodeBuilder<1> nb(this, kind); + nb << child1; + return nb.constructNode(); +} + +inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1) { + NodeBuilder<1> nb(this, kind); + nb << child1; + return nb.constructNodePtr(); +} + +inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2) { + NodeBuilder<2> nb(this, kind); + nb << child1 << child2; + return nb.constructNode(); +} + +inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2) { + NodeBuilder<2> nb(this, kind); + nb << child1 << child2; + return nb.constructNodePtr(); +} + +inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2, + TNode child3) { + NodeBuilder<3> nb(this, kind); + nb << child1 << child2 << child3; + return nb.constructNode(); +} + +inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2, + TNode child3) { + NodeBuilder<3> nb(this, kind); + nb << child1 << child2 << child3; + return nb.constructNodePtr(); +} + +inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2, + TNode child3, TNode child4) { + NodeBuilder<4> nb(this, kind); + nb << child1 << child2 << child3 << child4; + return nb.constructNode(); +} + +inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2, + TNode child3, TNode child4) { + NodeBuilder<4> nb(this, kind); + nb << child1 << child2 << child3 << child4; + return nb.constructNodePtr(); +} + +inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2, + TNode child3, TNode child4, TNode child5) { + NodeBuilder<5> nb(this, kind); + nb << child1 << child2 << child3 << child4 << child5; + return nb.constructNode(); +} + +inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2, + TNode child3, TNode child4, TNode child5) { + NodeBuilder<5> nb(this, kind); + nb << child1 << child2 << child3 << child4 << child5; + return nb.constructNodePtr(); +} + +// N-ary version +template +inline Node NodeManager::mkNode(Kind kind, + const std::vector >& + children) { + NodeBuilder<> nb(this, kind); + nb.append(children); + return nb.constructNode(); +} + +template +inline Node* NodeManager::mkNodePtr(Kind kind, + const std::vector >& + children) { + NodeBuilder<> nb(this, kind); + nb.append(children); + return nb.constructNodePtr(); +} + +// for operators +inline Node NodeManager::mkNode(TNode opNode) { + NodeBuilder<1> nb(this, operatorToKind(opNode)); + if(opNode.getKind() != kind::BUILTIN) { + nb << opNode; + } + return nb.constructNode(); +} + +inline Node* NodeManager::mkNodePtr(TNode opNode) { + NodeBuilder<1> nb(this, operatorToKind(opNode)); + if(opNode.getKind() != kind::BUILTIN) { + nb << opNode; + } + return nb.constructNodePtr(); +} + +inline Node NodeManager::mkNode(TNode opNode, TNode child1) { + NodeBuilder<2> nb(this, operatorToKind(opNode)); + if(opNode.getKind() != kind::BUILTIN) { + nb << opNode; + } + nb << child1; + return nb.constructNode(); +} + +inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1) { + NodeBuilder<2> nb(this, operatorToKind(opNode)); + if(opNode.getKind() != kind::BUILTIN) { + nb << opNode; + } + nb << child1; + return nb.constructNodePtr(); +} + +inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2) { + NodeBuilder<3> nb(this, operatorToKind(opNode)); + if(opNode.getKind() != kind::BUILTIN) { + nb << opNode; + } + nb << child1 << child2; + return nb.constructNode(); +} + +inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2) { + NodeBuilder<3> nb(this, operatorToKind(opNode)); + if(opNode.getKind() != kind::BUILTIN) { + nb << opNode; + } + nb << child1 << child2; + return nb.constructNodePtr(); +} + +inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2, + TNode child3) { + NodeBuilder<4> nb(this, operatorToKind(opNode)); + if(opNode.getKind() != kind::BUILTIN) { + nb << opNode; + } + nb << child1 << child2 << child3; + return nb.constructNode(); +} + +inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2, + TNode child3) { + NodeBuilder<4> nb(this, operatorToKind(opNode)); + if(opNode.getKind() != kind::BUILTIN) { + nb << opNode; + } + nb << child1 << child2 << child3; + return nb.constructNodePtr(); +} + +inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2, + TNode child3, TNode child4) { + NodeBuilder<5> nb(this, operatorToKind(opNode)); + if(opNode.getKind() != kind::BUILTIN) { + nb << opNode; + } + nb << child1 << child2 << child3 << child4; + return nb.constructNode(); +} + +inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2, + TNode child3, TNode child4) { + NodeBuilder<5> nb(this, operatorToKind(opNode)); + if(opNode.getKind() != kind::BUILTIN) { + nb << opNode; + } + nb << child1 << child2 << child3 << child4; + return nb.constructNodePtr(); +} + +inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2, + TNode child3, TNode child4, TNode child5) { + NodeBuilder<6> nb(this, operatorToKind(opNode)); + if(opNode.getKind() != kind::BUILTIN) { + nb << opNode; + } + nb << child1 << child2 << child3 << child4 << child5; + return nb.constructNode(); +} + +inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2, + TNode child3, TNode child4, TNode child5) { + NodeBuilder<6> nb(this, operatorToKind(opNode)); + if(opNode.getKind() != kind::BUILTIN) { + nb << opNode; + } + nb << child1 << child2 << child3 << child4 << child5; + return nb.constructNodePtr(); +} + +// N-ary version for operators +template +inline Node NodeManager::mkNode(TNode opNode, + const std::vector >& + children) { + NodeBuilder<> nb(this, operatorToKind(opNode)); + if(opNode.getKind() != kind::BUILTIN) { + nb << opNode; + } + nb.append(children); + return nb.constructNode(); +} + +template +inline Node* NodeManager::mkNodePtr(TNode opNode, + const std::vector >& + children) { + NodeBuilder<> nb(this, operatorToKind(opNode)); + if(opNode.getKind() != kind::BUILTIN) { + nb << opNode; + } + nb.append(children); + return nb.constructNodePtr(); +} + + +inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1) { + return (NodeBuilder<1>(this, kind) << child1).constructTypeNode(); +} + +inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1, + TypeNode child2) { + return (NodeBuilder<2>(this, kind) << child1 << child2).constructTypeNode(); +} + +inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1, + TypeNode child2, TypeNode child3) { + return (NodeBuilder<3>(this, kind) << child1 << child2 << child3).constructTypeNode(); +} + +// N-ary version for types +inline TypeNode NodeManager::mkTypeNode(Kind kind, + const std::vector& children) { + return NodeBuilder<>(this, kind).append(children).constructTypeNode(); +} + +template +Node NodeManager::mkConst(const T& val) { + return mkConstInternal(val); +} + +template +TypeNode NodeManager::mkTypeConst(const T& val) { + return mkConstInternal(val); +} + +template +NodeClass NodeManager::mkConstInternal(const T& val) { + + // typedef typename kind::metakind::constantMap::OwningTheory theory_t; + NVStorage<1> nvStorage; + expr::NodeValue& nvStack = reinterpret_cast(nvStorage); + + nvStack.d_id = 0; + nvStack.d_kind = kind::metakind::ConstantMap::kind; + nvStack.d_rc = 0; + nvStack.d_nchildren = 1; + +#if defined(__GNUC__) && (__GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ >= 6)) +#pragma GCC diagnostic push +#pragma GCC diagnostic ignored "-Warray-bounds" +#endif + + nvStack.d_children[0] = + const_cast(reinterpret_cast(&val)); + expr::NodeValue* nv = poolLookup(&nvStack); + +#if defined(__GNUC__) && (__GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ >= 6)) +#pragma GCC diagnostic pop +#endif + + if(nv != NULL) { + return NodeClass(nv); + } + + nv = (expr::NodeValue*) + std::malloc(sizeof(expr::NodeValue) + sizeof(T)); + if(nv == NULL) { + throw std::bad_alloc(); + } + + nv->d_nchildren = 0; + nv->d_kind = kind::metakind::ConstantMap::kind; + nv->d_id = next_id++;// FIXME multithreading + nv->d_rc = 0; + + //OwningTheory::mkConst(val); + new (&nv->d_children) T(val); + + poolInsert(nv); + if(Debug.isOn("gc")) { + Debug("gc") << "creating node value " << nv + << " [" << nv->d_id << "]: "; + nv->printAst(Debug("gc")); + Debug("gc") << std::endl; + } + + return NodeClass(nv); +} + +}/* CVC4 namespace */ + +#endif /* __CVC4__NODE_MANAGER_H */ diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 5810e1f4f..46705a849 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -223,12 +223,24 @@ bool Type::isString() const { return d_typeNode->isString(); } +/** Is this the rounding mode type? */ +bool Type::isRoundingMode() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->isRoundingMode(); +} + /** Is this the bit-vector type? */ bool Type::isBitVector() const { NodeManagerScope nms(d_nodeManager); return d_typeNode->isBitVector(); } +/** Is this the floating-point type? */ +bool Type::isFloatingPoint() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->isFloatingPoint(); +} + /** Is this a datatype type? */ bool Type::isDatatype() const { NodeManagerScope nms(d_nodeManager); @@ -436,11 +448,21 @@ StringType::StringType(const Type& t) throw(IllegalArgumentException) : CheckArgument(isNull() || isString(), this); } +RoundingModeType::RoundingModeType(const Type& t) throw(IllegalArgumentException) : + Type(t) { + CheckArgument(isNull() || isRoundingMode(), this); +} + BitVectorType::BitVectorType(const Type& t) throw(IllegalArgumentException) : Type(t) { CheckArgument(isNull() || isBitVector(), this); } +FloatingPointType::FloatingPointType(const Type& t) throw(IllegalArgumentException) : + Type(t) { + CheckArgument(isNull() || isFloatingPoint(), this); +} + DatatypeType::DatatypeType(const Type& t) throw(IllegalArgumentException) : Type(t) { CheckArgument(isNull() || isDatatype(), this); @@ -520,6 +542,14 @@ unsigned BitVectorType::getSize() const { return d_typeNode->getBitVectorSize(); } +unsigned FloatingPointType::getExponentSize() const { + return d_typeNode->getFloatingPointExponentSize(); +} + +unsigned FloatingPointType::getSignificandSize() const { + return d_typeNode->getFloatingPointSignificandSize(); +} + Type ArrayType::getIndexType() const { return makeType(d_typeNode->getArrayIndexType()); } diff --git a/src/expr/type.h b/src/expr/type.h index 7674ff9d0..8a5a987d5 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -47,6 +47,7 @@ class BooleanType; class IntegerType; class RealType; class StringType; +class RoundingModeType; class BitVectorType; class ArrayType; class SetType; @@ -258,12 +259,24 @@ public: */ bool isString() const; + /** + * Is this the rounding mode type? + * @return true if the type is the rounding mode type + */ + bool isRoundingMode() const; + /** * Is this the bit-vector type? * @return true if the type is a bit-vector type */ bool isBitVector() const; + /** + * Is this the floating-point type? + * @return true if the type is a floating-point type + */ + bool isFloatingPoint() const; + /** * Is this a function type? * @return true if the type is a function type @@ -412,6 +425,19 @@ public: StringType(const Type& type) throw(IllegalArgumentException); };/* class StringType */ +/** + * Singleton class encapsulating the rounding mode type. + */ +class CVC4_PUBLIC RoundingModeType : public Type { + +public: + + /** Construct from the base type */ + RoundingModeType(const Type& type = Type()) throw(IllegalArgumentException); +};/* class RoundingModeType */ + + + /** * Class encapsulating a function type. */ @@ -609,6 +635,31 @@ public: };/* class BitVectorType */ +/** + * Class encapsulating the floating point type. + */ +class CVC4_PUBLIC FloatingPointType : public Type { + +public: + + /** Construct from the base type */ + FloatingPointType(const Type& type = Type()) throw(IllegalArgumentException); + + /** + * Returns the size of the floating-point exponent type. + * @return the width of the floating-point exponent type (> 0) + */ + unsigned getExponentSize() const; + + /** + * Returns the size of the floating-point significand type. + * @return the width of the floating-point significand type (> 0) + */ + unsigned getSignificandSize() const; + +};/* class FloatingPointType */ + + /** * Class encapsulating the datatype type */ diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 289395a34..5129b7581 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -463,6 +463,9 @@ public: /** Is this the String type? */ bool isString() const; + /** Is this the Rounding Mode type? */ + bool isRoundingMode() const; + /** Is this an array type? */ bool isArray() const; @@ -560,6 +563,13 @@ public: /** Is this a regexp type */ bool isRegExp() const; + /** Is this a floating-point type */ + bool isFloatingPoint() const; + + /** Is this a floating-point type of with exp exponent bits + and sig significand bits */ + bool isFloatingPoint(unsigned exp, unsigned sig) const; + /** Is this a bit-vector type */ bool isBitVector() const; @@ -590,6 +600,12 @@ public: /** Get the Datatype specification from a datatype type */ const Datatype& getDatatype() const; + /** Get the exponent size of this floating-point type */ + unsigned getFloatingPointExponentSize() const; + + /** Get the significand size of this floating-point type */ + unsigned getFloatingPointSignificandSize() const; + /** Get the size of this bit-vector type */ unsigned getBitVectorSize() const; @@ -852,6 +868,11 @@ inline bool TypeNode::isString() const { inline bool TypeNode::isRegExp() const { return getKind() == kind::TYPE_CONSTANT && getConst() == REGEXP_TYPE; + } + +inline bool TypeNode::isRoundingMode() const { + return getKind() == kind::TYPE_CONSTANT && + getConst() == ROUNDINGMODE_TYPE; } inline bool TypeNode::isArray() const { @@ -939,6 +960,12 @@ inline bool TypeNode::isSubrange() const { ( isPredicateSubtype() && getSubtypeParentType().isSubrange() ); } +/** Is this a floating-point type */ +inline bool TypeNode::isFloatingPoint() const { + return getKind() == kind::FLOATINGPOINT_TYPE || + ( isPredicateSubtype() && getSubtypeParentType().isFloatingPoint() ); +} + /** Is this a bit-vector type */ inline bool TypeNode::isBitVector() const { return getKind() == kind::BITVECTOR_TYPE || @@ -973,6 +1000,16 @@ inline bool TypeNode::isTester() const { return getKind() == kind::TESTER_TYPE; } +/** Is this a floating-point type of with exp exponent bits + and sig significand bits */ +inline bool TypeNode::isFloatingPoint(unsigned exp, unsigned sig) const { + return + ( getKind() == kind::FLOATINGPOINT_TYPE && + getConst().exponent() == exp && + getConst().significand() == sig ) || + ( isPredicateSubtype() && getSubtypeParentType().isFloatingPoint(exp,sig) ); +} + /** Is this a bit-vector type of size size */ inline bool TypeNode::isBitVector(unsigned size) const { return @@ -990,6 +1027,18 @@ inline const Datatype& TypeNode::getDatatype() const { } } +/** Get the exponent size of this floating-point type */ +inline unsigned TypeNode::getFloatingPointExponentSize() const { + Assert(isFloatingPoint()); + return getConst().exponent(); +} + +/** Get the significand size of this floating-point type */ +inline unsigned TypeNode::getFloatingPointSignificandSize() const { + Assert(isFloatingPoint()); + return getConst().significand(); +} + /** Get the size of this bit-vector type */ inline unsigned TypeNode::getBitVectorSize() const { Assert(isBitVector()); diff --git a/src/options/Makefile.am b/src/options/Makefile.am index 2be82469e..24b78836a 100644 --- a/src/options/Makefile.am +++ b/src/options/Makefile.am @@ -40,7 +40,9 @@ 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 OPTIONS_FILES = \ $(patsubst %.cpp,%,$(filter %.cpp,$(OPTIONS_FILES_SRCS))) @@ -101,7 +103,9 @@ nodist_liboptions_la_SOURCES = \ ../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 \ diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 511b67997..1a5442419 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -112,10 +112,13 @@ namespace CVC4 { #include "util/output.h" #include "util/rational.h" #include "util/hash.h" +#include "util/floatingpoint.h" #include #include #include #include +// \todo Review the need for this header +#include "math.h" using namespace CVC4; using namespace CVC4::parser; @@ -949,7 +952,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] std::string name; std::vector args; std::vector< std::pair > sortedVarNames; - Expr f, f2; + Expr f, f2, f3, f4; std::string attr; Expr attexpr; std::vector patexprs; @@ -1243,13 +1246,30 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] // 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 ); @@ -1263,6 +1283,16 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] | 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 ); } @@ -1427,8 +1457,50 @@ indexedFunctionName[CVC4::Expr& op] 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 ; @@ -1623,6 +1695,32 @@ builtinOp[CVC4::Kind& kind] | 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 ; @@ -1706,6 +1804,17 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check] 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 << "'"; @@ -2035,6 +2144,56 @@ EMPTYSET_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }? 'emptyset'; // 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 |. diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 62814ca25..7740d0b94 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -95,6 +95,41 @@ void Smt2::addStringOperators() { 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: @@ -172,6 +207,15 @@ void Smt2::addTheory(Theory theory) { 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; @@ -222,6 +266,8 @@ bool Smt2::isTheoryEnabled(Theory theory) const { 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; @@ -301,6 +347,11 @@ void Smt2::setLogic(const std::string& name) { 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) { diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 8c23c8657..82498b624 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -51,7 +51,8 @@ public: THEORY_QUANTIFIERS, THEORY_SETS, THEORY_STRINGS, - THEORY_UF + THEORY_UF, + THEORY_FP }; private: @@ -219,6 +220,8 @@ private: void addStringOperators(); + void addFloatingPointOperators(); + };/* class Smt2 */ }/* CVC4::parser namespace */ diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 4f12ed012..b3b548450 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -42,6 +42,7 @@ namespace smt2 { 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() { @@ -140,6 +141,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, 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 @@ -149,6 +151,12 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::BITVECTOR_TYPE: out << "(_ BitVec " << n.getConst().size << ")"; break; + case kind::FLOATINGPOINT_TYPE: + out << "(_ FloatingPoint " + << n.getConst().exponent() << " " + << n.getConst().significand() + << ")"; + break; case kind::CONST_BITVECTOR: { const BitVector& bv = n.getConst(); const Integer& x = bv.getValue(); @@ -163,6 +171,20 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, // } break; } + case kind::CONST_FLOATINGPOINT: + out << n.getConst().getLiteral(); + break; + case kind::CONST_ROUNDINGMODE: + switch (n.getConst()) { + 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()); + } + break; case kind::CONST_BOOLEAN: // the default would print "1" or "0" for bool, that's not correct // for our purposes @@ -448,7 +470,49 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, 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().getType()); if(t.getKind() == kind::TYPE_CONSTANT && @@ -657,6 +721,46 @@ static string smtKindString(Kind k) throw() { 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 */ } @@ -703,6 +807,58 @@ static void printBvParameterizedOp(std::ostream& out, TNode n) throw() { 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().t.exponent() << ' ' + << n.getOperator().getConst().t.significand(); + break; + case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT: + //out << "to_fp_fp " + out << "to_fp " + << n.getOperator().getConst().t.exponent() << ' ' + << n.getOperator().getConst().t.significand(); + break; + case kind::FLOATINGPOINT_TO_FP_REAL: + //out << "to_fp_real " + out << "to_fp " + << n.getOperator().getConst().t.exponent() << ' ' + << n.getOperator().getConst().t.significand(); + break; + case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: + //out << "to_fp_signed " + out << "to_fp " + << n.getOperator().getConst().t.exponent() << ' ' + << n.getOperator().getConst().t.significand(); + break; + case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: + out << "to_fp_unsigned " + << n.getOperator().getConst().t.exponent() << ' ' + << n.getOperator().getConst().t.significand(); + break; + case kind::FLOATINGPOINT_TO_FP_GENERIC: + out << "to_fp " + << n.getOperator().getConst().t.exponent() << ' ' + << n.getOperator().getConst().t.significand(); + break; + case kind::FLOATINGPOINT_TO_UBV: + out << "fp.to_ubv " + << n.getOperator().getConst().bvs.size; + break; + case kind::FLOATINGPOINT_TO_SBV: + out << "fp.to_sbv " + << n.getOperator().getConst().bvs.size; + break; + default: + out << n.getKind(); + } + out << ")"; +} + + template static bool tryToStream(std::ostream& out, const Command* c) throw(); template diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index ba3845d7a..7ab590d89 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -846,7 +846,17 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa 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; diff --git a/src/theory/fp/kinds b/src/theory/fp/kinds new file mode 100644 index 000000000..983d5aa5c --- /dev/null +++ b/src/theory/fp/kinds @@ -0,0 +1,238 @@ +# 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())" \ + "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 diff --git a/src/theory/fp/options b/src/theory/fp/options new file mode 100644 index 000000000..3fee94d1d --- /dev/null +++ b/src/theory/fp/options @@ -0,0 +1,8 @@ +# +# 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 diff --git a/src/theory/fp/options_handlers.h b/src/theory/fp/options_handlers.h new file mode 100644 index 000000000..f1a86e396 --- /dev/null +++ b/src/theory/fp/options_handlers.h @@ -0,0 +1,14 @@ +#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 */ diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp new file mode 100644 index 000000000..6400fec38 --- /dev/null +++ b/src/theory/fp/theory_fp.cpp @@ -0,0 +1,104 @@ +#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(); + + 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 */ diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h new file mode 100644 index 000000000..6fb41685f --- /dev/null +++ b/src/theory/fp/theory_fp.h @@ -0,0 +1,36 @@ +#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 */ diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp new file mode 100644 index 000000000..0c41e8ff7 --- /dev/null +++ b/src/theory/fp/theory_fp_rewriter.cpp @@ -0,0 +1,478 @@ +/********************* */ +/*! \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 + +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(); + Node lit = + NodeManager::currentNM()->mkConst(FloatingPoint(param.t.exponent(), + param.t.significand(), + node[1].getConst().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(); + const BitVector &bv = node[0].getConst(); + 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()); + bv = bv.concat(node[1].getConst()); + bv = bv.concat(node[2].getConst()); + + 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().getSize(), + node[2].getConst().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 */ + diff --git a/src/theory/fp/theory_fp_rewriter.h b/src/theory/fp/theory_fp_rewriter.h new file mode 100644 index 000000000..8a8f1c933 --- /dev/null +++ b/src/theory/fp/theory_fp_rewriter.h @@ -0,0 +1,48 @@ +#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 */ diff --git a/src/theory/fp/theory_fp_type_rules.h b/src/theory/fp/theory_fp_type_rules.h new file mode 100644 index 000000000..2c9a67984 --- /dev/null +++ b/src/theory/fp/theory_fp_type_rules.h @@ -0,0 +1,430 @@ +#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(); + + 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(); + + 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(); + + 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(); + + 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(); + + 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(); + + 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(); + + 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(); + + 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(); + + 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 */ diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index 4ea30d5c9..635262a1e 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -107,6 +107,10 @@ std::string LogicInfo::getLogicString() const { ss << "BV"; ++seen; } + if(d_theories[THEORY_FP]) { + ss << "FP"; + ++seen; + } if(d_theories[THEORY_DATATYPES]) { ss << "DT"; ++seen; @@ -206,6 +210,10 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc 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; diff --git a/src/util/Makefile.am b/src/util/Makefile.am index cca98db60..df787d049 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -100,6 +100,8 @@ libutil_la_SOURCES = \ didyoumean.cpp \ unsat_core.h \ unsat_core.cpp \ + floatingpoint.h \ + floatingpoint.cpp \ resource_manager.h \ resource_manager.cpp \ unsafe_interrupt_exception.h @@ -164,7 +166,8 @@ EXTRA_DIST = \ resource_manager.i \ unsafe_interrupt_exception.i \ proof.i \ - unsat_core.i + unsat_core.i \ + floatingpoint.i DISTCLEANFILES = \ integer.h.tmp \ diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp new file mode 100644 index 000000000..1aed6331e --- /dev/null +++ b/src/util/floatingpoint.cpp @@ -0,0 +1,38 @@ +/********************* */ +/*! \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 */ + diff --git a/src/util/floatingpoint.h b/src/util/floatingpoint.h new file mode 100644 index 000000000..e0678d389 --- /dev/null +++ b/src/util/floatingpoint.h @@ -0,0 +1,293 @@ +/********************* */ +/*! \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 + +#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 + 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 + 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 */ diff --git a/src/util/floatingpoint.i b/src/util/floatingpoint.i new file mode 100644 index 000000000..c66cc311d --- /dev/null +++ b/src/util/floatingpoint.i @@ -0,0 +1,5 @@ +%{ +#include "util/floatingpoint.h" +%} + +%include "util/floatingpoint.h" diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h index 007378528..efc7c5582 100644 --- a/test/unit/theory/logic_info_white.h +++ b/test/unit/theory/logic_info_white.h @@ -512,13 +512,13 @@ public: 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() ); @@ -527,12 +527,13 @@ public: 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 ) ); -- 2.30.2