From 3a0fc2e7f21d797b4f9f7f43a7f4331fec97e05d Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 20 Sep 2021 17:10:46 -0700 Subject: Fix handling of conversions between FP and reals (#7149) Fixes #7056. Currently, we introduce a UF for conversions between FP numbers and reals. This is done as part of `ppRewrite()`. The problem is that terms sent to `ppRewrite()` are not fully preprocessed yet and the FP theory solver was storing terms that were not fully preprocessed in a map for later lookup. For the issue at hand, the conversion term contained an `ite`, which was later removed. As a result, the theory solver did not consider the term to be relevant when refining abstractions. This commit changes the handling of conversion functions to instead adding purification lemmas for conversion terms when they are registered. The purification lemmas are needed, because otherwise, we can't retrieve the model values for the term without the rewriter interferring. --- src/theory/fp/theory_fp.cpp | 355 ++++++++++++++++++-------------------------- src/theory/fp/theory_fp.h | 5 - 2 files changed, 148 insertions(+), 212 deletions(-) (limited to 'src') diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index 5ee5fd7d8..d38b6d0fa 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -65,8 +65,6 @@ TheoryFp::TheoryFp(Env& env, OutputChannel& out, Valuation valuation) d_registeredTerms(userContext()), d_wordBlaster(new FpWordBlaster(userContext())), d_expansionRequested(false), - d_realToFloatMap(userContext()), - d_floatToRealMap(userContext()), d_abstractionMap(userContext()), d_rewriter(userContext()), d_state(env, valuation), @@ -148,72 +146,6 @@ void TheoryFp::finishInit() d_equalityEngine->addFunctionKind(kind::ROUNDINGMODE_BITBLAST); } -Node TheoryFp::abstractRealToFloat(Node node) -{ - Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_REAL); - TypeNode t(node.getType()); - Assert(t.getKind() == kind::FLOATINGPOINT_TYPE); - - NodeManager *nm = NodeManager::currentNM(); - SkolemManager* sm = nm->getSkolemManager(); - ConversionAbstractionMap::const_iterator i(d_realToFloatMap.find(t)); - - Node fun; - if (i == d_realToFloatMap.end()) - { - std::vector args(2); - args[0] = node[0].getType(); - args[1] = node[1].getType(); - fun = sm->mkDummySkolem("floatingpoint_abstract_real_to_float", - nm->mkFunctionType(args, node.getType()), - "floatingpoint_abstract_real_to_float", - NodeManager::SKOLEM_EXACT_NAME); - d_realToFloatMap.insert(t, fun); - } - else - { - fun = (*i).second; - } - Node uf = nm->mkNode(kind::APPLY_UF, fun, node[0], node[1]); - - d_abstractionMap.insert(uf, node); - - return uf; -} - -Node TheoryFp::abstractFloatToReal(Node node) -{ - Assert(node.getKind() == kind::FLOATINGPOINT_TO_REAL_TOTAL); - TypeNode t(node[0].getType()); - Assert(t.getKind() == kind::FLOATINGPOINT_TYPE); - - NodeManager *nm = NodeManager::currentNM(); - SkolemManager* sm = nm->getSkolemManager(); - ConversionAbstractionMap::const_iterator i(d_floatToRealMap.find(t)); - - Node fun; - if (i == d_floatToRealMap.end()) - { - std::vector args(2); - args[0] = t; - args[1] = nm->realType(); - fun = sm->mkDummySkolem("floatingpoint_abstract_float_to_real", - nm->mkFunctionType(args, nm->realType()), - "floatingpoint_abstract_float_to_real", - NodeManager::SKOLEM_EXACT_NAME); - d_floatToRealMap.insert(t, fun); - } - else - { - fun = (*i).second; - } - Node uf = nm->mkNode(kind::APPLY_UF, fun, node[0], node[1]); - - d_abstractionMap.insert(uf, node); - - return uf; -} - TrustNode TheoryFp::ppRewrite(TNode node, std::vector& lems) { Trace("fp-ppRewrite") << "TheoryFp::ppRewrite(): " << node << std::endl; @@ -226,53 +158,6 @@ TrustNode TheoryFp::ppRewrite(TNode node, std::vector& lems) Node res = node; - // Abstract conversion functions - if (node.getKind() == kind::FLOATINGPOINT_TO_REAL_TOTAL) - { - res = abstractFloatToReal(node); - - // Generate some lemmas - NodeManager *nm = NodeManager::currentNM(); - - Node pd = - nm->mkNode(kind::IMPLIES, - nm->mkNode(kind::OR, - nm->mkNode(kind::FLOATINGPOINT_ISNAN, node[0]), - nm->mkNode(kind::FLOATINGPOINT_ISINF, node[0])), - nm->mkNode(kind::EQUAL, res, node[1])); - handleLemma(pd, InferenceId::FP_PREPROCESS); - - Node z = - nm->mkNode(kind::IMPLIES, - nm->mkNode(kind::FLOATINGPOINT_ISZ, node[0]), - nm->mkNode(kind::EQUAL, res, nm->mkConst(Rational(0U)))); - handleLemma(z, InferenceId::FP_PREPROCESS); - - // TODO : bounds on the output from largest floats, #1914 - } - else if (node.getKind() == kind::FLOATINGPOINT_TO_FP_REAL) - { - res = abstractRealToFloat(node); - - // Generate some lemmas - NodeManager *nm = NodeManager::currentNM(); - - Node nnan = - nm->mkNode(kind::NOT, nm->mkNode(kind::FLOATINGPOINT_ISNAN, res)); - handleLemma(nnan, InferenceId::FP_PREPROCESS); - - Node z = nm->mkNode( - kind::IMPLIES, - nm->mkNode(kind::EQUAL, node[1], nm->mkConst(Rational(0U))), - nm->mkNode(kind::EQUAL, - res, - nm->mkConst(FloatingPoint::makeZero( - res.getType().getConst(), false)))); - handleLemma(z, InferenceId::FP_PREPROCESS); - - // TODO : rounding-mode specific bounds on floats that don't give infinity - // BEWARE of directed rounding! #1914 - } if (res != node) { @@ -591,80 +476,132 @@ void TheoryFp::registerTerm(TNode node) { Trace("fp-registerTerm") << "TheoryFp::registerTerm(): " << node << std::endl; - if (!isRegistered(node)) + if (isRegistered(node)) + { + return; + } + + Kind k = node.getKind(); + Assert(k != kind::FLOATINGPOINT_TO_FP_GENERIC && k != kind::FLOATINGPOINT_SUB + && k != kind::FLOATINGPOINT_EQ && k != kind::FLOATINGPOINT_GEQ + && k != kind::FLOATINGPOINT_GT); + + CVC5_UNUSED bool success = d_registeredTerms.insert(node); + Assert(success); + + // Add to the equality engine + if (k == kind::EQUAL) + { + d_equalityEngine->addTriggerPredicate(node); + } + else { - Kind k = node.getKind(); - Assert(k != kind::FLOATINGPOINT_TO_FP_GENERIC - && k != kind::FLOATINGPOINT_SUB && k != kind::FLOATINGPOINT_EQ - && k != kind::FLOATINGPOINT_GEQ && k != kind::FLOATINGPOINT_GT); + d_equalityEngine->addTerm(node); + } - bool success = d_registeredTerms.insert(node); - (void)success; // Only used for assertion - Assert(success); + // Give the expansion of classifications in terms of equalities + // This should make equality reasoning slightly more powerful. + if ((k == kind::FLOATINGPOINT_ISNAN) || (k == kind::FLOATINGPOINT_ISZ) + || (k == kind::FLOATINGPOINT_ISINF)) + { + NodeManager* nm = NodeManager::currentNM(); + FloatingPointSize s = node[0].getType().getConst(); + Node equalityAlias = Node::null(); - // Add to the equality engine - if (k == kind::EQUAL) + if (k == kind::FLOATINGPOINT_ISNAN) { - d_equalityEngine->addTriggerPredicate(node); + equalityAlias = nm->mkNode( + kind::EQUAL, node[0], nm->mkConst(FloatingPoint::makeNaN(s))); + } + else if (k == kind::FLOATINGPOINT_ISZ) + { + equalityAlias = nm->mkNode( + kind::OR, + nm->mkNode(kind::EQUAL, + node[0], + nm->mkConst(FloatingPoint::makeZero(s, true))), + nm->mkNode(kind::EQUAL, + node[0], + nm->mkConst(FloatingPoint::makeZero(s, false)))); + } + else if (k == kind::FLOATINGPOINT_ISINF) + { + equalityAlias = + nm->mkNode(kind::OR, + nm->mkNode(kind::EQUAL, + node[0], + nm->mkConst(FloatingPoint::makeInf(s, true))), + nm->mkNode(kind::EQUAL, + node[0], + nm->mkConst(FloatingPoint::makeInf(s, false)))); } else { - d_equalityEngine->addTerm(node); + Unreachable() << "Only isNaN, isInf and isZero have aliases"; } - // Give the expansion of classifications in terms of equalities - // This should make equality reasoning slightly more powerful. - if ((k == kind::FLOATINGPOINT_ISNAN) || (k == kind::FLOATINGPOINT_ISZ) - || (k == kind::FLOATINGPOINT_ISINF)) - { - NodeManager *nm = NodeManager::currentNM(); - FloatingPointSize s = node[0].getType().getConst(); - Node equalityAlias = Node::null(); + handleLemma(nm->mkNode(kind::EQUAL, node, equalityAlias), + InferenceId::FP_REGISTER_TERM); + } + else if (k == kind::FLOATINGPOINT_TO_REAL_TOTAL) + { + // Purify (fp.to_real x) + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); + Node sk = sm->mkPurifySkolem(node, "to_real", "fp purify skolem"); + handleLemma(node.eqNode(sk), InferenceId::FP_REGISTER_TERM); + d_abstractionMap.insert(sk, node); - if (k == kind::FLOATINGPOINT_ISNAN) - { - equalityAlias = nm->mkNode( - kind::EQUAL, node[0], nm->mkConst(FloatingPoint::makeNaN(s))); - } - else if (k == kind::FLOATINGPOINT_ISZ) - { - equalityAlias = nm->mkNode( - kind::OR, - nm->mkNode(kind::EQUAL, - node[0], - nm->mkConst(FloatingPoint::makeZero(s, true))), - nm->mkNode(kind::EQUAL, - node[0], - nm->mkConst(FloatingPoint::makeZero(s, false)))); - } - else if (k == kind::FLOATINGPOINT_ISINF) - { - equalityAlias = nm->mkNode( - kind::OR, - nm->mkNode(kind::EQUAL, - node[0], - nm->mkConst(FloatingPoint::makeInf(s, true))), - nm->mkNode(kind::EQUAL, - node[0], - nm->mkConst(FloatingPoint::makeInf(s, false)))); - } - else - { - Unreachable() << "Only isNaN, isInf and isZero have aliases"; - } + Node pd = + nm->mkNode(kind::IMPLIES, + nm->mkNode(kind::OR, + nm->mkNode(kind::FLOATINGPOINT_ISNAN, node[0]), + nm->mkNode(kind::FLOATINGPOINT_ISINF, node[0])), + nm->mkNode(kind::EQUAL, node, node[1])); + handleLemma(pd, InferenceId::FP_REGISTER_TERM); - handleLemma(nm->mkNode(kind::EQUAL, node, equalityAlias), - InferenceId::FP_REGISTER_TERM); - } + Node z = + nm->mkNode(kind::IMPLIES, + nm->mkNode(kind::FLOATINGPOINT_ISZ, node[0]), + nm->mkNode(kind::EQUAL, node, nm->mkConst(Rational(0U)))); + handleLemma(z, InferenceId::FP_REGISTER_TERM); + return; - /* When not word-blasting lazier, we word-blast every term on - * registration. */ - if (!options().fp.fpLazyWb) - { - wordBlastAndEquateTerm(node); - } + // TODO : bounds on the output from largest floats, #1914 + } + else if (k == kind::FLOATINGPOINT_TO_FP_REAL) + { + // Purify ((_ to_fp eb sb) rm x) + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); + Node sk = sm->mkPurifySkolem(node, "to_real_fp", "fp purify skolem"); + handleLemma(node.eqNode(sk), InferenceId::FP_REGISTER_TERM); + d_abstractionMap.insert(sk, node); + + Node nnan = + nm->mkNode(kind::NOT, nm->mkNode(kind::FLOATINGPOINT_ISNAN, node)); + handleLemma(nnan, InferenceId::FP_REGISTER_TERM); + + Node z = nm->mkNode( + kind::IMPLIES, + nm->mkNode(kind::EQUAL, node[1], nm->mkConst(Rational(0U))), + nm->mkNode(kind::EQUAL, + node, + nm->mkConst(FloatingPoint::makeZero( + node.getType().getConst(), false)))); + handleLemma(z, InferenceId::FP_REGISTER_TERM); + return; + + // TODO : rounding-mode specific bounds on floats that don't give infinity + // BEWARE of directed rounding! #1914 + } + + /* When not word-blasting lazier, we word-blast every term on + * registration. */ + if (!options().fp.fpLazyWb) + { + wordBlastAndEquateTerm(node); } - return; } bool TheoryFp::isRegistered(TNode node) @@ -703,8 +640,6 @@ void TheoryFp::preRegisterTerm(TNode node) void TheoryFp::handleLemma(Node node, InferenceId id) { Trace("fp") << "TheoryFp::handleLemma(): asserting " << node << std::endl; - // will be preprocessed when sent, which is important because it contains - // embedded ITEs if (rewrite(node) != d_true) { /* We only send non-trivial lemmas. */ @@ -737,17 +672,25 @@ void TheoryFp::postCheck(Effort level) /* Resolve the abstractions for the conversion lemmas */ if (level == EFFORT_LAST_CALL) { - Trace("fp") << "TheoryFp::check(): checking abstractions" << std::endl; + Trace("fp-abstraction") + << "TheoryFp::check(): checking abstractions" << std::endl; TheoryModel* m = getValuation().getModel(); bool lemmaAdded = false; - for (AbstractionMap::const_iterator i = d_abstractionMap.begin(); - i != d_abstractionMap.end(); - ++i) + for (const auto& [abstract, concrete] : d_abstractionMap) { - if (m->hasTerm((*i).first)) + Trace("fp-abstraction") + << "TheoryFp::check(): Abstraction: " << abstract << std::endl; + if (m->hasTerm(abstract)) { // Is actually used in the model - lemmaAdded |= refineAbstraction(m, (*i).first, (*i).second); + Trace("fp-abstraction") + << "TheoryFp::check(): ... relevant" << std::endl; + lemmaAdded |= refineAbstraction(m, abstract, concrete); + } + else + { + Trace("fp-abstraction") + << "TheoryFp::check(): ... not relevant" << std::endl; } } } @@ -846,40 +789,36 @@ bool TheoryFp::collectModelValues(TheoryModel* m, } std::unordered_set visited; - std::stack working; + std::vector working; std::set relevantVariables; - for (std::set::const_iterator i(relevantTerms.begin()); - i != relevantTerms.end(); ++i) { - working.push(*i); + for (const Node& n : relevantTerms) + { + working.emplace_back(n); } while (!working.empty()) { - TNode current = working.top(); - working.pop(); - - // Ignore things that have already been explored - if (visited.find(current) == visited.end()) { - visited.insert(current); + TNode current = working.back(); + working.pop_back(); - TypeNode t(current.getType()); + if (visited.find(current) != visited.end()) + { + // Ignore things that have already been explored + continue; + } + visited.insert(current); - if ((t.isRoundingMode() || t.isFloatingPoint()) && - this->isLeaf(current)) { - relevantVariables.insert(current); - } + TypeNode t = current.getType(); - for (size_t i = 0; i < current.getNumChildren(); ++i) { - working.push(current[i]); - } + if ((t.isRoundingMode() || t.isFloatingPoint()) && this->isLeaf(current)) + { + relevantVariables.insert(current); } + + working.insert(working.end(), current.begin(), current.end()); } - for (std::set::const_iterator i(relevantVariables.begin()); - i != relevantVariables.end(); - ++i) + for (const TNode& node : relevantVariables) { - TNode node = *i; - Trace("fp-collectModelInfo") << "TheoryFp::collectModelInfo(): relevantVariable " << node << std::endl; @@ -889,6 +828,8 @@ bool TheoryFp::collectModelValues(TheoryModel* m, // if FpWordBlaster::getValue() does not return a null node. if (!wordBlasted.isNull() && !m->assertEquality(node, wordBlasted, true)) { + Trace("fp-collectModelInfo") + << "TheoryFp::collectModelInfo(): ... not converted" << std::endl; return false; } diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h index 9dd532a5d..807756c5b 100644 --- a/src/theory/fp/theory_fp.h +++ b/src/theory/fp/theory_fp.h @@ -141,12 +141,7 @@ class TheoryFp : public Theory bool refineAbstraction(TheoryModel* m, TNode abstract, TNode concrete); - Node abstractRealToFloat(Node); - Node abstractFloatToReal(Node); - private: - ConversionAbstractionMap d_realToFloatMap; - ConversionAbstractionMap d_floatToRealMap; AbstractionMap d_abstractionMap; // abstract -> original /** The theory rewriter for this theory. */ -- cgit v1.2.3