summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/CMakeLists.txt2
-rw-r--r--src/theory/fp/fp_expand_defs.cpp323
-rw-r--r--src/theory/fp/fp_expand_defs.h70
-rw-r--r--src/theory/fp/theory_fp.cpp259
-rw-r--r--src/theory/fp/theory_fp.h28
-rw-r--r--src/theory/fp/theory_fp_rewriter.cpp6
-rw-r--r--src/theory/fp/theory_fp_rewriter.h8
7 files changed, 418 insertions, 278 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 662df7254..9e340a31c 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -608,6 +608,8 @@ libcvc4_add_sources(
theory/ext_theory.h
theory/fp/fp_converter.cpp
theory/fp/fp_converter.h
+ theory/fp/fp_expand_defs.cpp
+ theory/fp/fp_expand_defs.h
theory/fp/theory_fp.cpp
theory/fp/theory_fp.h
theory/fp/theory_fp_rewriter.cpp
diff --git a/src/theory/fp/fp_expand_defs.cpp b/src/theory/fp/fp_expand_defs.cpp
new file mode 100644
index 000000000..4e9803bf7
--- /dev/null
+++ b/src/theory/fp/fp_expand_defs.cpp
@@ -0,0 +1,323 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Expand definitions for floating-point arithmetic.
+ */
+
+#include "theory/fp/fp_expand_defs.h"
+
+#include "expr/skolem_manager.h"
+
+namespace cvc5 {
+namespace theory {
+namespace fp {
+
+namespace removeToFPGeneric {
+
+Node removeToFPGeneric(TNode node)
+{
+ Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_GENERIC);
+
+ FloatingPointToFPGeneric info =
+ node.getOperator().getConst<FloatingPointToFPGeneric>();
+
+ size_t children = node.getNumChildren();
+
+ Node op;
+ NodeManager* nm = NodeManager::currentNM();
+
+ if (children == 1)
+ {
+ op = nm->mkConst(FloatingPointToFPIEEEBitVector(info));
+ return nm->mkNode(op, node[0]);
+ }
+ else
+ {
+ Assert(children == 2);
+ Assert(node[0].getType().isRoundingMode());
+
+ TypeNode t = node[1].getType();
+
+ if (t.isFloatingPoint())
+ {
+ op = nm->mkConst(FloatingPointToFPFloatingPoint(info));
+ }
+ else if (t.isReal())
+ {
+ op = nm->mkConst(FloatingPointToFPReal(info));
+ }
+ else if (t.isBitVector())
+ {
+ op = nm->mkConst(FloatingPointToFPSignedBitVector(info));
+ }
+ else
+ {
+ throw TypeCheckingExceptionPrivate(
+ node,
+ "cannot rewrite to_fp generic due to incorrect type of second "
+ "argument");
+ }
+
+ return nm->mkNode(op, node[0], node[1]);
+ }
+
+ Unreachable() << "to_fp generic not rewritten";
+}
+} // namespace removeToFPGeneric
+
+FpExpandDefs::FpExpandDefs(context::UserContext* u)
+ :
+
+ d_minMap(u),
+ d_maxMap(u),
+ d_toUBVMap(u),
+ d_toSBVMap(u),
+ d_toRealMap(u)
+{
+}
+
+Node FpExpandDefs::minUF(Node node)
+{
+ Assert(node.getKind() == kind::FLOATINGPOINT_MIN);
+ TypeNode t(node.getType());
+ Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
+
+ NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
+ ComparisonUFMap::const_iterator i(d_minMap.find(t));
+
+ Node fun;
+ if (i == d_minMap.end())
+ {
+ std::vector<TypeNode> args(2);
+ args[0] = t;
+ args[1] = t;
+ fun = sm->mkDummySkolem("floatingpoint_min_zero_case",
+ nm->mkFunctionType(args,
+#ifdef SYMFPUPROPISBOOL
+ nm->booleanType()
+#else
+ nm->mkBitVectorType(1U)
+#endif
+ ),
+ "floatingpoint_min_zero_case",
+ NodeManager::SKOLEM_EXACT_NAME);
+ d_minMap.insert(t, fun);
+ }
+ else
+ {
+ fun = (*i).second;
+ }
+ return nm->mkNode(kind::APPLY_UF,
+ fun,
+ node[1],
+ node[0]); // Application reverses the order or arguments
+}
+
+Node FpExpandDefs::maxUF(Node node)
+{
+ Assert(node.getKind() == kind::FLOATINGPOINT_MAX);
+ TypeNode t(node.getType());
+ Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
+
+ NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
+ ComparisonUFMap::const_iterator i(d_maxMap.find(t));
+
+ Node fun;
+ if (i == d_maxMap.end())
+ {
+ std::vector<TypeNode> args(2);
+ args[0] = t;
+ args[1] = t;
+ fun = sm->mkDummySkolem("floatingpoint_max_zero_case",
+ nm->mkFunctionType(args,
+#ifdef SYMFPUPROPISBOOL
+ nm->booleanType()
+#else
+ nm->mkBitVectorType(1U)
+#endif
+ ),
+ "floatingpoint_max_zero_case",
+ NodeManager::SKOLEM_EXACT_NAME);
+ d_maxMap.insert(t, fun);
+ }
+ else
+ {
+ fun = (*i).second;
+ }
+ return nm->mkNode(kind::APPLY_UF, fun, node[1], node[0]);
+}
+
+Node FpExpandDefs::toUBVUF(Node node)
+{
+ Assert(node.getKind() == kind::FLOATINGPOINT_TO_UBV);
+
+ TypeNode target(node.getType());
+ Assert(target.getKind() == kind::BITVECTOR_TYPE);
+
+ TypeNode source(node[1].getType());
+ Assert(source.getKind() == kind::FLOATINGPOINT_TYPE);
+
+ std::pair<TypeNode, TypeNode> p(source, target);
+ NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
+ ConversionUFMap::const_iterator i(d_toUBVMap.find(p));
+
+ Node fun;
+ if (i == d_toUBVMap.end())
+ {
+ std::vector<TypeNode> args(2);
+ args[0] = nm->roundingModeType();
+ args[1] = source;
+ fun = sm->mkDummySkolem("floatingpoint_to_ubv_out_of_range_case",
+ nm->mkFunctionType(args, target),
+ "floatingpoint_to_ubv_out_of_range_case",
+ NodeManager::SKOLEM_EXACT_NAME);
+ d_toUBVMap.insert(p, fun);
+ }
+ else
+ {
+ fun = (*i).second;
+ }
+ return nm->mkNode(kind::APPLY_UF, fun, node[0], node[1]);
+}
+
+Node FpExpandDefs::toSBVUF(Node node)
+{
+ Assert(node.getKind() == kind::FLOATINGPOINT_TO_SBV);
+
+ TypeNode target(node.getType());
+ Assert(target.getKind() == kind::BITVECTOR_TYPE);
+
+ TypeNode source(node[1].getType());
+ Assert(source.getKind() == kind::FLOATINGPOINT_TYPE);
+
+ std::pair<TypeNode, TypeNode> p(source, target);
+ NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
+ ConversionUFMap::const_iterator i(d_toSBVMap.find(p));
+
+ Node fun;
+ if (i == d_toSBVMap.end())
+ {
+ std::vector<TypeNode> args(2);
+ args[0] = nm->roundingModeType();
+ args[1] = source;
+ fun = sm->mkDummySkolem("floatingpoint_to_sbv_out_of_range_case",
+ nm->mkFunctionType(args, target),
+ "floatingpoint_to_sbv_out_of_range_case",
+ NodeManager::SKOLEM_EXACT_NAME);
+ d_toSBVMap.insert(p, fun);
+ }
+ else
+ {
+ fun = (*i).second;
+ }
+ return nm->mkNode(kind::APPLY_UF, fun, node[0], node[1]);
+}
+
+Node FpExpandDefs::toRealUF(Node node)
+{
+ Assert(node.getKind() == kind::FLOATINGPOINT_TO_REAL);
+ TypeNode t(node[0].getType());
+ Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
+
+ NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
+ ComparisonUFMap::const_iterator i(d_toRealMap.find(t));
+
+ Node fun;
+ if (i == d_toRealMap.end())
+ {
+ std::vector<TypeNode> args(1);
+ args[0] = t;
+ fun = sm->mkDummySkolem("floatingpoint_to_real_infinity_and_NaN_case",
+ nm->mkFunctionType(args, nm->realType()),
+ "floatingpoint_to_real_infinity_and_NaN_case",
+ NodeManager::SKOLEM_EXACT_NAME);
+ d_toRealMap.insert(t, fun);
+ }
+ else
+ {
+ fun = (*i).second;
+ }
+ return nm->mkNode(kind::APPLY_UF, fun, node[0]);
+}
+
+TrustNode FpExpandDefs::expandDefinition(Node node)
+{
+ Trace("fp-expandDefinition")
+ << "FpExpandDefs::expandDefinition(): " << node << std::endl;
+
+ Node res = node;
+
+ if (node.getKind() == kind::FLOATINGPOINT_TO_FP_GENERIC)
+ {
+ res = removeToFPGeneric::removeToFPGeneric(node);
+ }
+ else if (node.getKind() == kind::FLOATINGPOINT_MIN)
+ {
+ res = NodeManager::currentNM()->mkNode(
+ kind::FLOATINGPOINT_MIN_TOTAL, node[0], node[1], minUF(node));
+ }
+ else if (node.getKind() == kind::FLOATINGPOINT_MAX)
+ {
+ res = NodeManager::currentNM()->mkNode(
+ kind::FLOATINGPOINT_MAX_TOTAL, node[0], node[1], maxUF(node));
+ }
+ else if (node.getKind() == kind::FLOATINGPOINT_TO_UBV)
+ {
+ FloatingPointToUBV info = node.getOperator().getConst<FloatingPointToUBV>();
+ FloatingPointToUBVTotal newInfo(info);
+
+ res =
+ NodeManager::currentNM()->mkNode( // kind::FLOATINGPOINT_TO_UBV_TOTAL,
+ NodeManager::currentNM()->mkConst(newInfo),
+ node[0],
+ node[1],
+ toUBVUF(node));
+ }
+ else if (node.getKind() == kind::FLOATINGPOINT_TO_SBV)
+ {
+ FloatingPointToSBV info = node.getOperator().getConst<FloatingPointToSBV>();
+ FloatingPointToSBVTotal newInfo(info);
+
+ res =
+ NodeManager::currentNM()->mkNode( // kind::FLOATINGPOINT_TO_SBV_TOTAL,
+ NodeManager::currentNM()->mkConst(newInfo),
+ node[0],
+ node[1],
+ toSBVUF(node));
+ }
+ else if (node.getKind() == kind::FLOATINGPOINT_TO_REAL)
+ {
+ res = NodeManager::currentNM()->mkNode(
+ kind::FLOATINGPOINT_TO_REAL_TOTAL, node[0], toRealUF(node));
+ }
+ else
+ {
+ // Do nothing
+ }
+
+ if (res != node)
+ {
+ Trace("fp-expandDefinition") << "FpExpandDefs::expandDefinition(): " << node
+ << " rewritten to " << res << std::endl;
+ return TrustNode::mkTrustRewrite(node, res, nullptr);
+ }
+ return TrustNode::null();
+}
+
+} // namespace fp
+} // namespace theory
+} // namespace cvc5
diff --git a/src/theory/fp/fp_expand_defs.h b/src/theory/fp/fp_expand_defs.h
new file mode 100644
index 000000000..674d79331
--- /dev/null
+++ b/src/theory/fp/fp_expand_defs.h
@@ -0,0 +1,70 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Expand definitions for floating-point arithmetic.
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__THEORY__FP__FP_EXPAND_DEFS_H
+#define CVC5__THEORY__FP__FP_EXPAND_DEFS_H
+
+#include "context/cdhashmap.h"
+#include "expr/node.h"
+#include "theory/trust_node.h"
+
+namespace cvc5 {
+namespace theory {
+namespace fp {
+
+/**
+ * Module responsibile for expanding definitions for the FP theory.
+ */
+class FpExpandDefs
+{
+ using PairTypeNodeHashFunction = PairHashFunction<TypeNode,
+ TypeNode,
+ TypeNodeHashFunction,
+ TypeNodeHashFunction>;
+ /** Uninterpreted functions for undefined cases of non-total operators. */
+ using ComparisonUFMap =
+ context::CDHashMap<TypeNode, Node, TypeNodeHashFunction>;
+ /** Uninterpreted functions for lazy handling of conversions. */
+ using ConversionUFMap = context::
+ CDHashMap<std::pair<TypeNode, TypeNode>, Node, PairTypeNodeHashFunction>;
+
+ public:
+ FpExpandDefs(context::UserContext* u);
+ /** expand definitions in node */
+ TrustNode expandDefinition(Node node);
+
+ private:
+ /** TODO: document (projects issue #265) */
+ Node minUF(Node);
+ Node maxUF(Node);
+ Node toUBVUF(Node);
+ Node toSBVUF(Node);
+ Node toRealUF(Node);
+ Node abstractRealToFloat(Node);
+ Node abstractFloatToReal(Node);
+ ComparisonUFMap d_minMap;
+ ComparisonUFMap d_maxMap;
+ ConversionUFMap d_toUBVMap;
+ ConversionUFMap d_toSBVMap;
+ ComparisonUFMap d_toRealMap;
+}; /* class TheoryFp */
+
+} // namespace fp
+} // namespace theory
+} // namespace cvc5
+
+#endif /* CVC5__THEORY__FP__THEORY_FP_H */
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 4bcb761a5..6629a839d 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -36,49 +36,6 @@ namespace cvc5 {
namespace theory {
namespace fp {
-namespace removeToFPGeneric {
-
-Node removeToFPGeneric(TNode node) {
- Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_GENERIC);
-
- FloatingPointToFPGeneric info =
- node.getOperator().getConst<FloatingPointToFPGeneric>();
-
- size_t children = node.getNumChildren();
-
- Node op;
- NodeManager *nm = NodeManager::currentNM();
-
- if (children == 1) {
- op = nm->mkConst(FloatingPointToFPIEEEBitVector(info));
- return nm->mkNode(op, node[0]);
-
- } else {
- Assert(children == 2);
- Assert(node[0].getType().isRoundingMode());
-
- TypeNode t = node[1].getType();
-
- if (t.isFloatingPoint()) {
- op = nm->mkConst(FloatingPointToFPFloatingPoint(info));
- } else if (t.isReal()) {
- op = nm->mkConst(FloatingPointToFPReal(info));
- } else if (t.isBitVector()) {
- op = nm->mkConst(FloatingPointToFPSignedBitVector(info));
- } else {
- throw TypeCheckingExceptionPrivate(
- node,
- "cannot rewrite to_fp generic due to incorrect type of second "
- "argument");
- }
-
- return nm->mkNode(op, node[0], node[1]);
- }
-
- Unreachable() << "to_fp generic not rewritten";
-}
-} // namespace removeToFPGeneric
-
namespace helper {
Node buildConjunct(const std::vector<TNode> &assumptions) {
if (assumptions.size() == 0) {
@@ -113,14 +70,10 @@ TheoryFp::TheoryFp(context::Context* c,
d_registeredTerms(u),
d_conv(new FpConverter(u)),
d_expansionRequested(false),
- d_minMap(u),
- d_maxMap(u),
- d_toUBVMap(u),
- d_toSBVMap(u),
- d_toRealMap(u),
d_realToFloatMap(u),
d_floatToRealMap(u),
d_abstractionMap(u),
+ d_rewriter(u),
d_state(c, u, valuation),
d_im(*this, d_state, pnm, "theory::fp::", false)
{
@@ -198,153 +151,6 @@ void TheoryFp::finishInit()
d_equalityEngine->addFunctionKind(kind::ROUNDINGMODE_BITBLAST);
}
-Node TheoryFp::minUF(Node node) {
- Assert(node.getKind() == kind::FLOATINGPOINT_MIN);
- TypeNode t(node.getType());
- Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
-
- NodeManager *nm = NodeManager::currentNM();
- SkolemManager* sm = nm->getSkolemManager();
- ComparisonUFMap::const_iterator i(d_minMap.find(t));
-
- Node fun;
- if (i == d_minMap.end()) {
- std::vector<TypeNode> args(2);
- args[0] = t;
- args[1] = t;
- fun = sm->mkDummySkolem("floatingpoint_min_zero_case",
- nm->mkFunctionType(args,
-#ifdef SYMFPUPROPISBOOL
- nm->booleanType()
-#else
- nm->mkBitVectorType(1U)
-#endif
- ),
- "floatingpoint_min_zero_case",
- NodeManager::SKOLEM_EXACT_NAME);
- d_minMap.insert(t, fun);
- } else {
- fun = (*i).second;
- }
- return nm->mkNode(kind::APPLY_UF, fun, node[1],
- node[0]); // Application reverses the order or arguments
-}
-
-Node TheoryFp::maxUF(Node node) {
- Assert(node.getKind() == kind::FLOATINGPOINT_MAX);
- TypeNode t(node.getType());
- Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
-
- NodeManager *nm = NodeManager::currentNM();
- SkolemManager* sm = nm->getSkolemManager();
- ComparisonUFMap::const_iterator i(d_maxMap.find(t));
-
- Node fun;
- if (i == d_maxMap.end()) {
- std::vector<TypeNode> args(2);
- args[0] = t;
- args[1] = t;
- fun = sm->mkDummySkolem("floatingpoint_max_zero_case",
- nm->mkFunctionType(args,
-#ifdef SYMFPUPROPISBOOL
- nm->booleanType()
-#else
- nm->mkBitVectorType(1U)
-#endif
- ),
- "floatingpoint_max_zero_case",
- NodeManager::SKOLEM_EXACT_NAME);
- d_maxMap.insert(t, fun);
- } else {
- fun = (*i).second;
- }
- return nm->mkNode(kind::APPLY_UF, fun, node[1], node[0]);
-}
-
-Node TheoryFp::toUBVUF(Node node) {
- Assert(node.getKind() == kind::FLOATINGPOINT_TO_UBV);
-
- TypeNode target(node.getType());
- Assert(target.getKind() == kind::BITVECTOR_TYPE);
-
- TypeNode source(node[1].getType());
- Assert(source.getKind() == kind::FLOATINGPOINT_TYPE);
-
- std::pair<TypeNode, TypeNode> p(source, target);
- NodeManager *nm = NodeManager::currentNM();
- SkolemManager* sm = nm->getSkolemManager();
- ConversionUFMap::const_iterator i(d_toUBVMap.find(p));
-
- Node fun;
- if (i == d_toUBVMap.end()) {
- std::vector<TypeNode> args(2);
- args[0] = nm->roundingModeType();
- args[1] = source;
- fun = sm->mkDummySkolem("floatingpoint_to_ubv_out_of_range_case",
- nm->mkFunctionType(args, target),
- "floatingpoint_to_ubv_out_of_range_case",
- NodeManager::SKOLEM_EXACT_NAME);
- d_toUBVMap.insert(p, fun);
- } else {
- fun = (*i).second;
- }
- return nm->mkNode(kind::APPLY_UF, fun, node[0], node[1]);
-}
-
-Node TheoryFp::toSBVUF(Node node) {
- Assert(node.getKind() == kind::FLOATINGPOINT_TO_SBV);
-
- TypeNode target(node.getType());
- Assert(target.getKind() == kind::BITVECTOR_TYPE);
-
- TypeNode source(node[1].getType());
- Assert(source.getKind() == kind::FLOATINGPOINT_TYPE);
-
- std::pair<TypeNode, TypeNode> p(source, target);
- NodeManager *nm = NodeManager::currentNM();
- SkolemManager* sm = nm->getSkolemManager();
- ConversionUFMap::const_iterator i(d_toSBVMap.find(p));
-
- Node fun;
- if (i == d_toSBVMap.end()) {
- std::vector<TypeNode> args(2);
- args[0] = nm->roundingModeType();
- args[1] = source;
- fun = sm->mkDummySkolem("floatingpoint_to_sbv_out_of_range_case",
- nm->mkFunctionType(args, target),
- "floatingpoint_to_sbv_out_of_range_case",
- NodeManager::SKOLEM_EXACT_NAME);
- d_toSBVMap.insert(p, fun);
- } else {
- fun = (*i).second;
- }
- return nm->mkNode(kind::APPLY_UF, fun, node[0], node[1]);
-}
-
-Node TheoryFp::toRealUF(Node node) {
- Assert(node.getKind() == kind::FLOATINGPOINT_TO_REAL);
- TypeNode t(node[0].getType());
- Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
-
- NodeManager *nm = NodeManager::currentNM();
- SkolemManager* sm = nm->getSkolemManager();
- ComparisonUFMap::const_iterator i(d_toRealMap.find(t));
-
- Node fun;
- if (i == d_toRealMap.end()) {
- std::vector<TypeNode> args(1);
- args[0] = t;
- fun = sm->mkDummySkolem("floatingpoint_to_real_infinity_and_NaN_case",
- nm->mkFunctionType(args, nm->realType()),
- "floatingpoint_to_real_infinity_and_NaN_case",
- NodeManager::SKOLEM_EXACT_NAME);
- d_toRealMap.insert(t, fun);
- } else {
- fun = (*i).second;
- }
- return nm->mkNode(kind::APPLY_UF, fun, node[0]);
-}
-
Node TheoryFp::abstractRealToFloat(Node node)
{
Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_REAL);
@@ -353,7 +159,7 @@ Node TheoryFp::abstractRealToFloat(Node node)
NodeManager *nm = NodeManager::currentNM();
SkolemManager* sm = nm->getSkolemManager();
- ComparisonUFMap::const_iterator i(d_realToFloatMap.find(t));
+ ConversionAbstractionMap::const_iterator i(d_realToFloatMap.find(t));
Node fun;
if (i == d_realToFloatMap.end())
@@ -386,7 +192,7 @@ Node TheoryFp::abstractFloatToReal(Node node)
NodeManager *nm = NodeManager::currentNM();
SkolemManager* sm = nm->getSkolemManager();
- ComparisonUFMap::const_iterator i(d_floatToRealMap.find(t));
+ ConversionAbstractionMap::const_iterator i(d_floatToRealMap.find(t));
Node fun;
if (i == d_floatToRealMap.end())
@@ -411,63 +217,11 @@ Node TheoryFp::abstractFloatToReal(Node node)
return uf;
}
-TrustNode TheoryFp::expandDefinition(Node node)
-{
- Trace("fp-expandDefinition") << "TheoryFp::expandDefinition(): " << node
- << std::endl;
-
- Node res = node;
-
- if (node.getKind() == kind::FLOATINGPOINT_TO_FP_GENERIC) {
- res = removeToFPGeneric::removeToFPGeneric(node);
-
- } else if (node.getKind() == kind::FLOATINGPOINT_MIN) {
- res = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_MIN_TOTAL,
- node[0], node[1], minUF(node));
-
- } else if (node.getKind() == kind::FLOATINGPOINT_MAX) {
- res = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_MAX_TOTAL,
- node[0], node[1], maxUF(node));
-
- } else if (node.getKind() == kind::FLOATINGPOINT_TO_UBV) {
- FloatingPointToUBV info = node.getOperator().getConst<FloatingPointToUBV>();
- FloatingPointToUBVTotal newInfo(info);
-
- res =
- NodeManager::currentNM()->mkNode( // kind::FLOATINGPOINT_TO_UBV_TOTAL,
- NodeManager::currentNM()->mkConst(newInfo), node[0], node[1],
- toUBVUF(node));
-
- } else if (node.getKind() == kind::FLOATINGPOINT_TO_SBV) {
- FloatingPointToSBV info = node.getOperator().getConst<FloatingPointToSBV>();
- FloatingPointToSBVTotal newInfo(info);
-
- res =
- NodeManager::currentNM()->mkNode( // kind::FLOATINGPOINT_TO_SBV_TOTAL,
- NodeManager::currentNM()->mkConst(newInfo), node[0], node[1],
- toSBVUF(node));
-
- } else if (node.getKind() == kind::FLOATINGPOINT_TO_REAL) {
- res = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_TO_REAL_TOTAL,
- node[0], toRealUF(node));
-
- } else {
- // Do nothing
- }
-
- if (res != node) {
- Trace("fp-expandDefinition") << "TheoryFp::expandDefinition(): " << node
- << " rewritten to " << res << std::endl;
- return TrustNode::mkTrustRewrite(node, res, nullptr);
- }
- return TrustNode::null();
-}
-
TrustNode TheoryFp::ppRewrite(TNode node, std::vector<SkolemLemma>& lems)
{
Trace("fp-ppRewrite") << "TheoryFp::ppRewrite(): " << node << std::endl;
// first, see if we need to expand definitions
- TrustNode texp = expandDefinition(node);
+ TrustNode texp = d_rewriter.expandDefinition(node);
if (!texp.isNull())
{
return texp;
@@ -927,6 +681,11 @@ void TheoryFp::preRegisterTerm(TNode node)
return;
}
+TrustNode TheoryFp::expandDefinition(Node node)
+{
+ return d_rewriter.expandDefinition(node);
+}
+
void TheoryFp::handleLemma(Node node, InferenceId id)
{
Trace("fp") << "TheoryFp::handleLemma(): asserting " << node << std::endl;
diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h
index af53a50c6..78791b9b4 100644
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -61,10 +61,8 @@ class TheoryFp : public Theory
void finishInit() override;
//--------------------------------- end initialization
- TrustNode expandDefinition(Node node) override;
-
void preRegisterTerm(TNode node) override;
-
+ TrustNode expandDefinition(Node node) override;
TrustNode ppRewrite(TNode node, std::vector<SkolemLemma>& lems) override;
//--------------------------------- standard check
@@ -95,17 +93,8 @@ class TheoryFp : public Theory
TrustNode explain(TNode n) override;
protected:
- using PairTypeNodeHashFunction = PairHashFunction<TypeNode,
- TypeNode,
- TypeNodeHashFunction,
- TypeNodeHashFunction>;
- /** Uninterpreted functions for undefined cases of non-total operators. */
- using ComparisonUFMap =
+ using ConversionAbstractionMap =
context::CDHashMap<TypeNode, Node, TypeNodeHashFunction>;
- /** Uninterpreted functions for lazy handling of conversions. */
- using ConversionUFMap = context::
- CDHashMap<std::pair<TypeNode, TypeNode>, Node, PairTypeNodeHashFunction>;
- using ConversionAbstractionMap = ComparisonUFMap;
using AbstractionMap = context::CDHashMap<Node, Node, NodeHashFunction>;
/** Equality engine. */
@@ -157,24 +146,11 @@ class TheoryFp : public Theory
bool refineAbstraction(TheoryModel* m, TNode abstract, TNode concrete);
- Node minUF(Node);
- Node maxUF(Node);
-
- Node toUBVUF(Node);
- Node toSBVUF(Node);
-
- Node toRealUF(Node);
-
Node abstractRealToFloat(Node);
Node abstractFloatToReal(Node);
private:
- ComparisonUFMap d_minMap;
- ComparisonUFMap d_maxMap;
- ConversionUFMap d_toUBVMap;
- ConversionUFMap d_toSBVMap;
- ComparisonUFMap d_toRealMap;
ConversionAbstractionMap d_realToFloatMap;
ConversionAbstractionMap d_floatToRealMap;
AbstractionMap d_abstractionMap; // abstract -> original
diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp
index 64b89913a..07fde6a88 100644
--- a/src/theory/fp/theory_fp_rewriter.cpp
+++ b/src/theory/fp/theory_fp_rewriter.cpp
@@ -982,7 +982,7 @@ namespace constantFold {
/**
* Initialize the rewriter.
*/
-TheoryFpRewriter::TheoryFpRewriter()
+TheoryFpRewriter::TheoryFpRewriter(context::UserContext* u) : d_fpExpDef(u)
{
/* Set up the pre-rewrite dispatch table */
for (unsigned i = 0; i < kind::LAST_KIND; ++i)
@@ -1418,6 +1418,10 @@ TheoryFpRewriter::TheoryFpRewriter()
return res;
}
+ TrustNode TheoryFpRewriter::expandDefinition(Node node)
+ {
+ return d_fpExpDef.expandDefinition(node);
+ }
} // namespace fp
} // namespace theory
diff --git a/src/theory/fp/theory_fp_rewriter.h b/src/theory/fp/theory_fp_rewriter.h
index cc76d4dee..97c0e216b 100644
--- a/src/theory/fp/theory_fp_rewriter.h
+++ b/src/theory/fp/theory_fp_rewriter.h
@@ -21,6 +21,7 @@
#ifndef CVC5__THEORY__FP__THEORY_FP_REWRITER_H
#define CVC5__THEORY__FP__THEORY_FP_REWRITER_H
+#include "theory/fp/fp_expand_defs.h"
#include "theory/theory_rewriter.h"
namespace cvc5 {
@@ -32,7 +33,7 @@ typedef RewriteResponse (*RewriteFunction) (TNode, bool);
class TheoryFpRewriter : public TheoryRewriter
{
public:
- TheoryFpRewriter();
+ TheoryFpRewriter(context::UserContext* u);
RewriteResponse preRewrite(TNode node) override;
RewriteResponse postRewrite(TNode node) override;
@@ -45,11 +46,16 @@ class TheoryFpRewriter : public TheoryRewriter
// often this will suffice
return postRewrite(equality).d_node;
}
+ /** Expand definitions in node. */
+ TrustNode expandDefinition(Node node);
protected:
+ /** TODO: document (projects issue #265) */
RewriteFunction d_preRewriteTable[kind::LAST_KIND];
RewriteFunction d_postRewriteTable[kind::LAST_KIND];
RewriteFunction d_constantFoldTable[kind::LAST_KIND];
+ /** The expand definitions module. */
+ FpExpandDefs d_fpExpDef;
}; /* class TheoryFpRewriter */
} // namespace fp
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback