From: Andres Noetzli Date: Tue, 21 Sep 2021 00:10:46 +0000 (-0700) Subject: Fix handling of conversions between FP and reals (#7149) X-Git-Tag: cvc5-1.0.0~1190 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3a0fc2e7f21d797b4f9f7f43a7f4331fec97e05d;p=cvc5.git 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. --- 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. */ diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 90ad99e70..301e26bf9 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1595,6 +1595,7 @@ set(regress_1_tests regress1/decision/wishue160.smt2 regress1/error.cvc regress1/errorcrash.smt2 + regress1/fp/fp_to_real.smt2 regress1/fp/rti_3_5_bug_report.smt2 regress1/fmf-fun-dbu.smt2 regress1/fmf/ALG008-1.smt2 @@ -2492,6 +2493,7 @@ set(regress_2_tests regress2/bv_to_int_mask_array_3.smt2 regress2/bv_to_int_shifts.smt2 regress2/error1.smtv1.smt2 + regress2/fp/issue7056.smt2 regress2/fuzz_2.smtv1.smt2 regress2/hash_sat_06_19.smt2 regress2/hash_sat_07_17.smt2 diff --git a/test/regress/regress1/fp/fp_to_real.smt2 b/test/regress/regress1/fp/fp_to_real.smt2 new file mode 100644 index 000000000..a24ae4cdc --- /dev/null +++ b/test/regress/regress1/fp/fp_to_real.smt2 @@ -0,0 +1,10 @@ +(set-logic QF_FPLRA) +(declare-const c1 Bool) +(declare-const c2 Bool) +(declare-const x Float32) +(declare-const y Float32) +(assert (= x ((_ to_fp 8 24) RNE (ite c1 4.0 2.0)))) +(assert (= y ((_ to_fp 8 24) RNE (ite c1 6.0 8.0)))) +(assert (= 2.0 (fp.to_real (ite c2 x y)))) +(set-info :status sat) +(check-sat) diff --git a/test/regress/regress2/fp/issue7056.smt2 b/test/regress/regress2/fp/issue7056.smt2 new file mode 100644 index 000000000..4defecd66 --- /dev/null +++ b/test/regress/regress2/fp/issue7056.smt2 @@ -0,0 +1,26 @@ +; COMMAND-LINE: --no-check-proofs --no-check-unsat-cores +(set-logic ALL) +(set-info :smt-lib-version 2.6) +(define-fun fp.isFinite32 ((x Float32)) Bool (not (or (fp.isInfinite x) (fp.isNaN x)))) +(define-fun fp.isIntegral32 ((x Float32)) Bool (or (fp.isZero x) (and (fp.isNormal x) (= x (fp.roundToIntegral RNE x))))) + +(declare-sort t 0) +(declare-const a t) +(declare-fun first (t) Int) +(declare-fun last (t) Int) +(define-fun length ((b t)) Int (ite (<= (first b) (last b)) (+ (- (last b) (first b)) 1) 0)) + +(define-fun contained ((x Float32)) Bool (and + (fp.leq x (fp #b0 #b01111111 #b00000000000000000000000)) + (fp.leq (fp #b0 #b00000000 #b00000000000000000000000) x))) + + +(declare-const i Int) +(declare-const x Float32) +(assert (and (<= (length a) 1000) (< 0 (length a)))) +(assert (= i (first a))) +(assert (contained x)) +(assert (not (fp.isFinite32 (fp.mul RNE (fp.mul RNE (fp #b0 #b10010010 #b11101000010010000000000) ((_ to_fp 8 24) RNE (to_real (length a)))) + x)))) +(set-info :status unsat) +(check-sat)