From e7924fc22d220909c1b3eb0e41a1cdb624a69be7 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Mon, 30 Nov 2020 15:26:33 -0800 Subject: [PATCH] fp_converter: Properly separate out symbolic glue code. (#5501) File fp_converter.h encapsulates the symbolic glue code for symFPU and implements the actual word-blaster (class FpConverter). This header should not be included in any other headers in order to no pull in symFPU headers where it's not needed. However, it was included in src/theory/fp/theory_fp.h. This properly separates it out and does some clean up in TheoryFP, which still needs more love to conform to code style guidelines, and also more documentation. More love and documentation is postponed to future PRs to make reviewing easier. --- src/theory/fp/fp_converter.cpp | 8 ++-- src/theory/fp/fp_converter.h | 31 +++++++------- src/theory/fp/theory_fp.cpp | 45 ++++++++++---------- src/theory/fp/theory_fp.h | 75 ++++++++++++++++++---------------- 4 files changed, 85 insertions(+), 74 deletions(-) diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp index 85482bf6d..858710746 100644 --- a/src/theory/fp/fp_converter.cpp +++ b/src/theory/fp/fp_converter.cpp @@ -755,18 +755,20 @@ TypeNode floatingPointTypeInfo::getTypeNode(void) const } FpConverter::FpConverter(context::UserContext* user) - : + : d_additionalAssertions(user) #ifdef CVC4_USE_SYMFPU + , d_fpMap(user), d_rmMap(user), d_boolMap(user), d_ubvMap(user), - d_sbvMap(user), + d_sbvMap(user) #endif - d_additionalAssertions(user) { } +FpConverter::~FpConverter() {} + #ifdef CVC4_USE_SYMFPU Node FpConverter::ufToNode(const fpt &format, const uf &u) const { diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h index e48d651bd..6688e8607 100644 --- a/src/theory/fp/fp_converter.h +++ b/src/theory/fp/fp_converter.h @@ -14,6 +14,8 @@ ** Uses the symfpu library to convert from floating-point operations to ** bit-vectors and propositions allowing the theory to be solved by ** 'bit-blasting'. + ** + ** !!! This header is not to be included in any other headers !!! **/ #include "cvc4_private.h" @@ -49,10 +51,6 @@ namespace CVC4 { namespace theory { namespace fp { -typedef PairHashFunction - PairTypeNodeHashFunction; - /** * This is a symfpu symbolic "back-end". It allows the library to be used to * construct bit-vector expressions that compute floating-point operations. @@ -302,6 +300,20 @@ class floatingPointTypeInfo : public FloatingPointSize */ class FpConverter { + public: + /** Constructor. */ + FpConverter(context::UserContext*); + /** Destructor. */ + ~FpConverter(); + + /** Adds a node to the conversion, returns the converted node */ + Node convert(TNode); + + /** Gives the node representing the value of a given variable */ + Node getValue(Valuation&, TNode); + + context::CDList d_additionalAssertions; + protected: #ifdef CVC4_USE_SYMFPU typedef symfpuSymbolic::traits traits; @@ -338,17 +350,6 @@ class FpConverter /* Creates the relevant components for a variable */ uf buildComponents(TNode current); #endif - - public: - context::CDList d_additionalAssertions; - - FpConverter(context::UserContext *); - - /** Adds a node to the conversion, returns the converted node */ - Node convert(TNode); - - /** Gives the node representing the value of a given variable */ - Node getValue(Valuation &, TNode); }; } // namespace fp diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index 0b15486e2..01fab92c8 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -23,6 +23,7 @@ #include #include "options/fp_options.h" +#include "theory/fp/fp_converter.h" #include "theory/fp/theory_fp_rewriter.h" #include "theory/rewriter.h" #include "theory/theory_model.h" @@ -108,7 +109,7 @@ TheoryFp::TheoryFp(context::Context* c, : Theory(THEORY_FP, c, u, out, valuation, logicInfo, pnm), d_notification(*this), d_registeredTerms(u), - d_conv(u), + d_conv(new FpConverter(u)), d_expansionRequested(false), d_conflictNode(c, Node::null()), d_minMap(u), @@ -116,9 +117,9 @@ TheoryFp::TheoryFp(context::Context* c, d_toUBVMap(u), d_toSBVMap(u), d_toRealMap(u), - realToFloatMap(u), - floatToRealMap(u), - abstractionMap(u), + d_realToFloatMap(u), + d_floatToRealMap(u), + d_abstractionMap(u), d_state(c, u, valuation) { // indicate we are using the default theory state object @@ -341,10 +342,10 @@ Node TheoryFp::abstractRealToFloat(Node node) Assert(t.getKind() == kind::FLOATINGPOINT_TYPE); NodeManager *nm = NodeManager::currentNM(); - ComparisonUFMap::const_iterator i(realToFloatMap.find(t)); + ComparisonUFMap::const_iterator i(d_realToFloatMap.find(t)); Node fun; - if (i == realToFloatMap.end()) + if (i == d_realToFloatMap.end()) { std::vector args(2); args[0] = node[0].getType(); @@ -353,7 +354,7 @@ Node TheoryFp::abstractRealToFloat(Node node) nm->mkFunctionType(args, node.getType()), "floatingpoint_abstract_real_to_float", NodeManager::SKOLEM_EXACT_NAME); - realToFloatMap.insert(t, fun); + d_realToFloatMap.insert(t, fun); } else { @@ -361,7 +362,7 @@ Node TheoryFp::abstractRealToFloat(Node node) } Node uf = nm->mkNode(kind::APPLY_UF, fun, node[0], node[1]); - abstractionMap.insert(uf, node); + d_abstractionMap.insert(uf, node); return uf; } @@ -373,10 +374,10 @@ Node TheoryFp::abstractFloatToReal(Node node) Assert(t.getKind() == kind::FLOATINGPOINT_TYPE); NodeManager *nm = NodeManager::currentNM(); - ComparisonUFMap::const_iterator i(floatToRealMap.find(t)); + ComparisonUFMap::const_iterator i(d_floatToRealMap.find(t)); Node fun; - if (i == floatToRealMap.end()) + if (i == d_floatToRealMap.end()) { std::vector args(2); args[0] = t; @@ -385,7 +386,7 @@ Node TheoryFp::abstractFloatToReal(Node node) nm->mkFunctionType(args, nm->realType()), "floatingpoint_abstract_float_to_real", NodeManager::SKOLEM_EXACT_NAME); - floatToRealMap.insert(t, fun); + d_floatToRealMap.insert(t, fun); } else { @@ -393,7 +394,7 @@ Node TheoryFp::abstractFloatToReal(Node node) } Node uf = nm->mkNode(kind::APPLY_UF, fun, node[0], node[1]); - abstractionMap.insert(uf, node); + d_abstractionMap.insert(uf, node); return uf; } @@ -737,9 +738,9 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete) void TheoryFp::convertAndEquateTerm(TNode node) { Trace("fp-convertTerm") << "TheoryFp::convertTerm(): " << node << std::endl; - size_t oldAdditionalAssertions = d_conv.d_additionalAssertions.size(); + size_t oldAdditionalAssertions = d_conv->d_additionalAssertions.size(); - Node converted(d_conv.convert(node)); + Node converted(d_conv->convert(node)); if (converted != node) { Debug("fp-convertTerm") @@ -748,11 +749,11 @@ void TheoryFp::convertAndEquateTerm(TNode node) { << "TheoryFp::convertTerm(): after " << converted << std::endl; } - size_t newAdditionalAssertions = d_conv.d_additionalAssertions.size(); + size_t newAdditionalAssertions = d_conv->d_additionalAssertions.size(); Assert(oldAdditionalAssertions <= newAdditionalAssertions); while (oldAdditionalAssertions < newAdditionalAssertions) { - Node addA = d_conv.d_additionalAssertions[oldAdditionalAssertions]; + Node addA = d_conv->d_additionalAssertions[oldAdditionalAssertions]; Debug("fp-convertTerm") << "TheoryFp::convertTerm(): additional assertion " << addA << std::endl; @@ -953,8 +954,8 @@ void TheoryFp::postCheck(Effort level) TheoryModel* m = getValuation().getModel(); bool lemmaAdded = false; - for (abstractionMapType::const_iterator i = abstractionMap.begin(); - i != abstractionMap.end(); + for (AbstractionMap::const_iterator i = d_abstractionMap.begin(); + i != d_abstractionMap.end(); ++i) { if (m->hasTerm((*i).first)) @@ -1016,7 +1017,7 @@ TrustNode TheoryFp::explain(TNode n) } Node TheoryFp::getModelValue(TNode var) { - return d_conv.getValue(d_valuation, var); + return d_conv->getValue(d_valuation, var); } bool TheoryFp::collectModelInfo(TheoryModel* m, @@ -1069,14 +1070,16 @@ bool TheoryFp::collectModelValues(TheoryModel* m, } for (std::set::const_iterator i(relevantVariables.begin()); - i != relevantVariables.end(); ++i) { + i != relevantVariables.end(); + ++i) + { TNode node = *i; Trace("fp-collectModelInfo") << "TheoryFp::collectModelInfo(): relevantVariable " << node << std::endl; - if (!m->assertEquality(node, d_conv.getValue(d_valuation, node), true)) + if (!m->assertEquality(node, d_conv->getValue(d_valuation, node), true)) { return false; } diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h index 42c009893..fe91a39bd 100644 --- a/src/theory/fp/theory_fp.h +++ b/src/theory/fp/theory_fp.h @@ -24,7 +24,6 @@ #include #include "context/cdo.h" -#include "theory/fp/fp_converter.h" #include "theory/fp/theory_fp_rewriter.h" #include "theory/theory.h" #include "theory/uf/equality_engine.h" @@ -33,7 +32,10 @@ namespace CVC4 { namespace theory { namespace fp { -class TheoryFp : public Theory { +class FpConverter; + +class TheoryFp : public Theory +{ public: /** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */ TheoryFp(context::Context* c, @@ -42,8 +44,9 @@ class TheoryFp : public Theory { Valuation valuation, const LogicInfo& logicInfo, ProofNodeManager* pnm = nullptr); + //--------------------------------- initialization - /** get the official theory rewriter of this theory */ + /** Get the official theory rewriter of this theory. */ TheoryRewriter* getTheoryRewriter() override; /** * Returns true if we need an equality engine. If so, we initialize the @@ -51,7 +54,7 @@ class TheoryFp : public Theory { * documentation in Theory::needsEqualityEngine. */ bool needsEqualityEngine(EeSetupInfo& esi) override; - /** finish initialization */ + /** Finish initialization. */ void finishInit() override; //--------------------------------- end initialization @@ -77,8 +80,10 @@ class TheoryFp : public Theory { Node getModelValue(TNode var) override; bool collectModelInfo(TheoryModel* m, const std::set& relevantTerms) override; - /** Collect model values in m based on the relevant terms given by - * relevantTerms */ + /** + * Collect model values in m based on the relevant terms given by + * relevantTerms. + */ bool collectModelValues(TheoryModel* m, const std::set& relevantTerms) override; @@ -87,7 +92,20 @@ class TheoryFp : public Theory { TrustNode explain(TNode n) override; protected: - /** Equality engine */ + 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>; + using ConversionAbstractionMap = ComparisonUFMap; + using AbstractionMap = context::CDHashMap; + + /** Equality engine. */ class NotifyClass : public eq::EqualityEngineNotify { protected: TheoryFp& d_theorySolver; @@ -108,14 +126,15 @@ class TheoryFp : public Theory { NotifyClass d_notification; - /** General utility **/ + /** General utility. */ void registerTerm(TNode node); bool isRegistered(TNode node); context::CDHashSet d_registeredTerms; - /** Bit-blasting conversion */ - FpConverter d_conv; + /** The word-blaster. Translates FP -> BV. */ + std::unique_ptr d_conv; + bool d_expansionRequested; void convertAndEquateTerm(TNode node); @@ -133,44 +152,30 @@ class TheoryFp : public Theory { */ void conflictEqConstantMerge(TNode t1, TNode t2); - context::CDO d_conflictNode; - - typedef context::CDHashMap - ComparisonUFMap; - - ComparisonUFMap d_minMap; - ComparisonUFMap d_maxMap; + bool refineAbstraction(TheoryModel* m, TNode abstract, TNode concrete); Node minUF(Node); Node maxUF(Node); - typedef context::CDHashMap, Node, - PairTypeNodeHashFunction> - ConversionUFMap; - - ConversionUFMap d_toUBVMap; - ConversionUFMap d_toSBVMap; - Node toUBVUF(Node); Node toSBVUF(Node); - ComparisonUFMap d_toRealMap; - Node toRealUF(Node); - /** Uninterpretted functions for lazy handling of conversions */ - typedef ComparisonUFMap conversionAbstractionMap; - - conversionAbstractionMap realToFloatMap; - conversionAbstractionMap floatToRealMap; - Node abstractRealToFloat(Node); Node abstractFloatToReal(Node); - typedef context::CDHashMap abstractionMapType; - abstractionMapType abstractionMap; // abstract -> original + private: + context::CDO d_conflictNode; - bool refineAbstraction(TheoryModel* m, TNode abstract, TNode concrete); + 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 /** The theory rewriter for this theory. */ TheoryFpRewriter d_rewriter; -- 2.30.2