From: Andrew Reynolds Date: Tue, 20 Apr 2021 23:53:56 +0000 (-0500) Subject: Split FP expand definitions to own module (#6392) X-Git-Tag: cvc5-1.0.0~1873 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=eada674106422d800c86797ebccdd59010cf36b2;p=cvc5.git Split FP expand definitions to own module (#6392) This moves the code for expanding definitions in floating point to its own module, which lives in the rewriter. This is work towards moving Theory::expandDefinitions to Rewriter::expandDefinitions. The code was only moved, not modified in this PR. --- 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(); + + 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 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 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 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 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 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 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 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(); + 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(); + 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; + /** Uninterpreted functions for undefined cases of non-total operators. */ + using ComparisonUFMap = + context::CDHashMap; + /** Uninterpreted functions for lazy handling of conversions. */ + using ConversionUFMap = context:: + CDHashMap, 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(); - - 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 &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 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 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 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 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 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 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 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(); - 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(); - 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& 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& lems) override; //--------------------------------- standard check @@ -95,17 +93,8 @@ class TheoryFp : public Theory TrustNode explain(TNode n) override; protected: - using PairTypeNodeHashFunction = PairHashFunction; - /** Uninterpreted functions for undefined cases of non-total operators. */ - using ComparisonUFMap = + using ConversionAbstractionMap = context::CDHashMap; - /** Uninterpreted functions for lazy handling of conversions. */ - using ConversionUFMap = context:: - CDHashMap, Node, PairTypeNodeHashFunction>; - using ConversionAbstractionMap = ComparisonUFMap; using AbstractionMap = context::CDHashMap; /** 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