From 6931c8b3d078e9f5386837955dde2d786fcb1547 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Fri, 23 Jul 2021 10:51:22 -0700 Subject: [PATCH] FP: Add option to word-blast more lazily. (#6904) When enabled, this does not word-blast when registering term but at preNotifyFact (= more lazily) instead. This is enabled via option --fp-lazy-wb. --- src/options/fp_options.toml | 8 +++ src/theory/bv/bv_solver_bitblast.h | 2 +- src/theory/fp/fp_converter.cpp | 15 +++-- src/theory/fp/fp_converter.h | 5 +- src/theory/fp/theory_fp.cpp | 71 ++++++++++++++++++------ src/theory/fp/theory_fp.h | 11 ++-- test/regress/CMakeLists.txt | 1 + test/regress/regress0/fp/word-blast.smt2 | 15 +++++ 8 files changed, 99 insertions(+), 29 deletions(-) create mode 100644 test/regress/regress0/fp/word-blast.smt2 diff --git a/src/options/fp_options.toml b/src/options/fp_options.toml index 6fd632a7c..be40b49e2 100644 --- a/src/options/fp_options.toml +++ b/src/options/fp_options.toml @@ -8,3 +8,11 @@ name = "Floating-Point" type = "bool" default = "false" help = "Allow floating-point sorts of all sizes, rather than only Float32 (8/24) or Float64 (11/53) (experimental)" + +[[option]] + name = "fpLazyWb" + category = "experimental" + long = "fp-lazy-wb" + type = "bool" + default = "false" + help = "Enable lazier word-blasting (on preNotifyFact instead of registerTerm)" diff --git a/src/theory/bv/bv_solver_bitblast.h b/src/theory/bv/bv_solver_bitblast.h index 87f3f25cd..8dee3c2c4 100644 --- a/src/theory/bv/bv_solver_bitblast.h +++ b/src/theory/bv/bv_solver_bitblast.h @@ -120,7 +120,7 @@ class BVSolverBitblast : public BVSolver /** * Bit-blast queue for facts sent to this solver. * - * Get populated on preNotifyFact(). + * Gets populated on preNotifyFact(). */ context::CDQueue d_bbFacts; diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp index e309ab2e4..f6f1f3bb3 100644 --- a/src/theory/fp/fp_converter.cpp +++ b/src/theory/fp/fp_converter.cpp @@ -1296,15 +1296,18 @@ Node FpConverter::getValue(Valuation &val, TNode var) if (t.isRoundingMode()) { rmMap::const_iterator i(d_rmMap.find(var)); - - Assert(i != d_rmMap.end()) - << "Asking for the value of an unregistered expression"; + if (i == d_rmMap.end()) + { + return Node::null(); + } return rmToNode((*i).second); } - fpMap::const_iterator i(d_fpMap.find(var)); - Assert(i != d_fpMap.end()) - << "Asking for the value of an unregistered expression"; + fpMap::const_iterator i(d_fpMap.find(var)); + if (i == d_fpMap.end()) + { + return Node::null(); + } return ufToNode(fpt(t), (*i).second); } diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h index 9900c2987..d589eff60 100644 --- a/src/theory/fp/fp_converter.h +++ b/src/theory/fp/fp_converter.h @@ -300,7 +300,10 @@ class FpConverter /** Adds a node to the conversion, returns the converted node */ Node convert(TNode); - /** Gives the node representing the value of a given variable */ + /** + * Gives the node representing the value of a word-blasted variable. + * Returns a null node if it has not been word-blasted. + */ Node getValue(Valuation&, TNode); context::CDList d_additionalAssertions; diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index 1c8f10f77..9b5ac66d3 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -76,12 +76,13 @@ TheoryFp::TheoryFp(context::Context* c, d_abstractionMap(u), d_rewriter(u), d_state(c, u, valuation), - d_im(*this, d_state, pnm, "theory::fp::", false) + d_im(*this, d_state, pnm, "theory::fp::", false), + d_wbFactsCache(u) { // indicate we are using the default theory state and inference manager d_theoryState = &d_state; d_inferManager = &d_im; -} /* TheoryFp::TheoryFp() */ +} TheoryRewriter* TheoryFp::getTheoryRewriter() { return &d_rewriter; } @@ -304,6 +305,9 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete) Node floatValue = m->getValue(concrete[0]); Node undefValue = m->getValue(concrete[1]); + Assert(!abstractValue.isNull()); + Assert(!floatValue.isNull()); + Assert(!undefValue.isNull()); Assert(abstractValue.isConst()); Assert(floatValue.isConst()); Assert(undefValue.isConst()); @@ -413,6 +417,9 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete) Node rmValue = m->getValue(concrete[0]); Node realValue = m->getValue(concrete[1]); + Assert(!abstractValue.isNull()); + Assert(!rmValue.isNull()); + Assert(!realValue.isNull()); Assert(abstractValue.isConst()); Assert(rmValue.isConst()); Assert(realValue.isConst()); @@ -509,12 +516,16 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete) return false; } -void TheoryFp::convertAndEquateTerm(TNode node) { +void TheoryFp::convertAndEquateTerm(TNode node) +{ Trace("fp-convertTerm") << "TheoryFp::convertTerm(): " << node << std::endl; - size_t oldAdditionalAssertions = d_conv->d_additionalAssertions.size(); + + size_t oldSize = d_conv->d_additionalAssertions.size(); Node converted(d_conv->convert(node)); + size_t newSize = d_conv->d_additionalAssertions.size(); + if (converted != node) { Debug("fp-convertTerm") << "TheoryFp::convertTerm(): before " << node << std::endl; @@ -522,12 +533,11 @@ void TheoryFp::convertAndEquateTerm(TNode node) { << "TheoryFp::convertTerm(): after " << converted << std::endl; } - size_t newAdditionalAssertions = d_conv->d_additionalAssertions.size(); - Assert(oldAdditionalAssertions <= newAdditionalAssertions); + Assert(oldSize <= newSize); - while (oldAdditionalAssertions < newAdditionalAssertions) + while (oldSize < newSize) { - Node addA = d_conv->d_additionalAssertions[oldAdditionalAssertions]; + Node addA = d_conv->d_additionalAssertions[oldSize]; Debug("fp-convertTerm") << "TheoryFp::convertTerm(): additional assertion " << addA << std::endl; @@ -538,7 +548,7 @@ void TheoryFp::convertAndEquateTerm(TNode node) { nm->mkNode(kind::EQUAL, addA, nm->mkConst(::cvc5::BitVector(1U, 1U))), InferenceId::FP_EQUATE_TERM); - ++oldAdditionalAssertions; + ++oldSize; } // Equate the floating-point atom and the converted one. @@ -578,10 +588,12 @@ void TheoryFp::convertAndEquateTerm(TNode node) { return; } -void TheoryFp::registerTerm(TNode node) { +void TheoryFp::registerTerm(TNode node) +{ Trace("fp-registerTerm") << "TheoryFp::registerTerm(): " << node << std::endl; - if (!isRegistered(node)) { + if (!isRegistered(node)) + { Kind k = node.getKind(); Assert(k != kind::FLOATINGPOINT_TO_FP_GENERIC && k != kind::FLOATINGPOINT_SUB && k != kind::FLOATINGPOINT_EQ @@ -646,14 +658,19 @@ void TheoryFp::registerTerm(TNode node) { InferenceId::FP_REGISTER_TERM); } - // Use symfpu to produce an equivalent bit-vector statement - convertAndEquateTerm(node); + /* When not word-blasting lazier, we word-blast every term on + * registration. */ + if (!options::fpLazyWb()) + { + convertAndEquateTerm(node); + } } return; } -bool TheoryFp::isRegistered(TNode node) { - return !(d_registeredTerms.find(node) == d_registeredTerms.end()); +bool TheoryFp::isRegistered(TNode node) +{ + return d_registeredTerms.find(node) != d_registeredTerms.end(); } void TheoryFp::preRegisterTerm(TNode node) @@ -714,7 +731,7 @@ bool TheoryFp::needsCheckLastEffort() void TheoryFp::postCheck(Effort level) { - // Resolve the abstractions for the conversion lemmas + /* Resolve the abstractions for the conversion lemmas */ if (level == EFFORT_LAST_CALL) { Trace("fp") << "TheoryFp::check(): checking abstractions" << std::endl; @@ -739,6 +756,13 @@ void TheoryFp::postCheck(Effort level) bool TheoryFp::preNotifyFact( TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal) { + /* Word-blast lazier if configured. */ + if (options::fpLazyWb() && d_wbFactsCache.find(atom) == d_wbFactsCache.end()) + { + d_wbFactsCache.insert(atom); + convertAndEquateTerm(atom); + } + if (atom.getKind() == kind::EQUAL) { Assert(!(atom[0].getType().isFloatingPoint() @@ -763,6 +787,16 @@ bool TheoryFp::preNotifyFact( return false; } +void TheoryFp::notifySharedTerm(TNode n) +{ + /* Word-blast lazier if configured. */ + if (options::fpLazyWb() && d_wbFactsCache.find(n) == d_wbFactsCache.end()) + { + d_wbFactsCache.insert(n); + convertAndEquateTerm(n); + } +} + TrustNode TheoryFp::explain(TNode n) { Trace("fp") << "TheoryFp::explain(): explain " << n << std::endl; @@ -846,7 +880,10 @@ bool TheoryFp::collectModelValues(TheoryModel* m, << "TheoryFp::collectModelInfo(): relevantVariable " << node << std::endl; - if (!m->assertEquality(node, d_conv->getValue(d_valuation, node), true)) + Node converted = d_conv->getValue(d_valuation, node); + // We only assign the value if the FpConverter actually has one, that is, + // if FpConverter::getValue() does not return a null node. + if (!converted.isNull() && !m->assertEquality(node, converted, true)) { return false; } diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h index ada9b39d0..14779cc3d 100644 --- a/src/theory/fp/theory_fp.h +++ b/src/theory/fp/theory_fp.h @@ -114,6 +114,8 @@ class TheoryFp : public Theory }; friend NotifyClass; + void notifySharedTerm(TNode n) override; + NotifyClass d_notification; /** General utility. */ @@ -148,18 +150,19 @@ class TheoryFp : public Theory Node abstractFloatToReal(Node); private: - ConversionAbstractionMap d_realToFloatMap; ConversionAbstractionMap d_floatToRealMap; AbstractionMap d_abstractionMap; // abstract -> original /** The theory rewriter for this theory. */ TheoryFpRewriter d_rewriter; - /** A (default) theory state object */ + /** A (default) theory state object. */ TheoryState d_state; - /** A (default) inference manager */ + /** A (default) inference manager. */ TheoryInferenceManager d_im; -}; /* class TheoryFp */ + /** Cache of word-blasted facts. */ + context::CDHashSet d_wbFactsCache; +}; } // namespace fp } // namespace theory diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 6ebb91f9e..22a222369 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -604,6 +604,7 @@ set(regress_0_tests regress0/fp/issue6164.smt2 regress0/fp/rti_3_5_bug.smt2 regress0/fp/simple.smt2 + regress0/fp/word-blast.smt2 regress0/fp/wrong-model.smt2 regress0/fuzz_1.smtv1.smt2 regress0/fuzz_3.smtv1.smt2 diff --git a/test/regress/regress0/fp/word-blast.smt2 b/test/regress/regress0/fp/word-blast.smt2 new file mode 100644 index 000000000..65290a3b3 --- /dev/null +++ b/test/regress/regress0/fp/word-blast.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --fp-lazy-wb +; EXPECT: unsat +(set-logic QF_BVFP) +(declare-fun meters_ackermann!0 () (_ BitVec 64)) +(assert + (let ((?x8 ((_ to_fp 11 53) meters_ackermann!0))) + (fp.geq ?x8 ((_ to_fp 11 53) (_ bv0 64))))) +(assert + (let ((?x8 ((_ to_fp 11 53) meters_ackermann!0))) + (fp.leq ?x8 ((_ to_fp 11 53) (_ bv4652007308841189376 64))))) +(assert + (let ((?x19 ((_ sign_extend 32) ((_ fp.to_sbv 32) roundTowardZero (fp.abs ((_ to_fp 11 53) meters_ackermann!0)))))) +(not (not (bvult (_ bv9223372036854775807 64) ?x19))))) +(check-sat) +(exit) -- 2.30.2