diff options
Diffstat (limited to 'src/theory/fp')
-rw-r--r-- | src/theory/fp/fp_converter.cpp | 8 | ||||
-rw-r--r-- | src/theory/fp/fp_converter.h | 33 | ||||
-rw-r--r-- | src/theory/fp/theory_fp.cpp | 45 | ||||
-rw-r--r-- | src/theory/fp/theory_fp.h | 75 |
4 files changed, 86 insertions, 75 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 59e65c9e1..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" @@ -26,7 +28,7 @@ #include "context/cdlist.h" #include "expr/node.h" #include "expr/node_builder.h" -#include "expr/type.h" +#include "expr/type_node.h" #include "theory/valuation.h" #include "util/bitvector.h" #include "util/floatingpoint_size.h" @@ -49,10 +51,6 @@ namespace CVC4 { namespace theory { namespace fp { -typedef PairHashFunction<TypeNode, TypeNode, TypeNodeHashFunction, - TypeNodeHashFunction> - 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<Node> 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<Node> 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 <vector> #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<TypeNode> 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<TypeNode> 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<TNode>::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 <utility> #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<Node>& 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<Node>& relevantTerms) override; @@ -87,7 +92,20 @@ class TheoryFp : public Theory { TrustNode explain(TNode n) override; protected: - /** Equality engine */ + 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>; + using ConversionAbstractionMap = ComparisonUFMap; + using AbstractionMap = context::CDHashMap<Node, Node, NodeHashFunction>; + + /** 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<Node, NodeHashFunction> d_registeredTerms; - /** Bit-blasting conversion */ - FpConverter d_conv; + /** The word-blaster. Translates FP -> BV. */ + std::unique_ptr<FpConverter> 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<Node> d_conflictNode; - - typedef context::CDHashMap<TypeNode, Node, TypeNodeHashFunction> - ComparisonUFMap; - - ComparisonUFMap d_minMap; - ComparisonUFMap d_maxMap; + bool refineAbstraction(TheoryModel* m, TNode abstract, TNode concrete); Node minUF(Node); Node maxUF(Node); - typedef context::CDHashMap<std::pair<TypeNode, TypeNode>, 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<Node, Node, NodeHashFunction> abstractionMapType; - abstractionMapType abstractionMap; // abstract -> original + private: + context::CDO<Node> 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; |