diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/fp/theory_fp.cpp | 355 | ||||
| -rw-r--r-- | src/theory/fp/theory_fp.h | 5 |
2 files changed, 148 insertions, 212 deletions
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<TypeNode> 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<TypeNode> 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<SkolemLemma>& lems) { Trace("fp-ppRewrite") << "TheoryFp::ppRewrite(): " << node << std::endl; @@ -226,53 +158,6 @@ TrustNode TheoryFp::ppRewrite(TNode node, std::vector<SkolemLemma>& 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<FloatingPointSize>(), 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<FloatingPointSize>(); + 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<FloatingPointSize>(); - 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<FloatingPointSize>(), 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<TNode> visited; - std::stack<TNode> working; + std::vector<TNode> working; std::set<TNode> relevantVariables; - for (std::set<Node>::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<TNode>::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. */ |