From: Mathias Preiner Date: Fri, 30 Apr 2021 22:15:44 +0000 (-0700) Subject: bv: Refactor ppAssert and move to TheoryBV. (#6470) X-Git-Tag: cvc5-1.0.0~1806 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=839f64ea1f065415268bdb2bfe518ad727ed2a40;p=cvc5.git bv: Refactor ppAssert and move to TheoryBV. (#6470) This PR refactors ppAssert from the lazy BV solver and moves it to TheoryBV. --- diff --git a/src/theory/bv/bv_solver.h b/src/theory/bv/bv_solver.h index 282be6bfc..8ff4318c0 100644 --- a/src/theory/bv/bv_solver.h +++ b/src/theory/bv/bv_solver.h @@ -86,9 +86,6 @@ class BVSolver virtual std::string identify() const = 0; - virtual Theory::PPAssertStatus ppAssert( - TrustNode in, TrustSubstitutionMap& outSubstitutions) = 0; - virtual TrustNode ppRewrite(TNode t) { return TrustNode::null(); }; virtual void ppStaticLearn(TNode in, NodeBuilder& learned){}; diff --git a/src/theory/bv/bv_solver_bitblast.h b/src/theory/bv/bv_solver_bitblast.h index 8d6b8304e..384017f5f 100644 --- a/src/theory/bv/bv_solver_bitblast.h +++ b/src/theory/bv/bv_solver_bitblast.h @@ -60,12 +60,6 @@ class BVSolverBitblast : public BVSolver std::string identify() const override { return "BVSolverBitblast"; }; - Theory::PPAssertStatus ppAssert( - TrustNode in, TrustSubstitutionMap& outSubstitutions) override - { - return Theory::PPAssertStatus::PP_ASSERT_STATUS_UNSOLVED; - } - EqualityStatus getEqualityStatus(TNode a, TNode b) override; bool collectModelValues(TheoryModel* m, diff --git a/src/theory/bv/bv_solver_lazy.cpp b/src/theory/bv/bv_solver_lazy.cpp index a8670e1a6..06ecea701 100644 --- a/src/theory/bv/bv_solver_lazy.cpp +++ b/src/theory/bv/bv_solver_lazy.cpp @@ -30,7 +30,6 @@ #include "theory/bv/theory_bv_rewriter.h" #include "theory/bv/theory_bv_utils.h" #include "theory/theory_model.h" -#include "theory/trust_substitutions.h" using namespace cvc5::theory::bv::utils; @@ -126,8 +125,6 @@ void BVSolverLazy::spendResource(Resource r) BVSolverLazy::Statistics::Statistics() : d_avgConflictSize(smtStatisticsRegistry().registerAverage( "theory::bv::lazy::AvgBVConflictSize")), - d_solveSubstitutions(smtStatisticsRegistry().registerInt( - "theory::bv::lazy::NumSolveSubstitutions")), d_solveTimer(smtStatisticsRegistry().registerTimer( "theory::bv::lazy::solveTimer")), d_numCallsToCheckFullEffort(smtStatisticsRegistry().registerInt( @@ -428,89 +425,6 @@ void BVSolverLazy::propagate(Theory::Effort e) } } -Theory::PPAssertStatus BVSolverLazy::ppAssert( - TrustNode tin, TrustSubstitutionMap& outSubstitutions) -{ - TNode in = tin.getNode(); - switch (in.getKind()) - { - case kind::EQUAL: - { - if (in[0].isVar() && d_bv.isLegalElimination(in[0], in[1])) - { - ++(d_statistics.d_solveSubstitutions); - outSubstitutions.addSubstitutionSolved(in[0], in[1], tin); - return Theory::PP_ASSERT_STATUS_SOLVED; - } - if (in[1].isVar() && d_bv.isLegalElimination(in[1], in[0])) - { - ++(d_statistics.d_solveSubstitutions); - outSubstitutions.addSubstitutionSolved(in[1], in[0], tin); - return Theory::PP_ASSERT_STATUS_SOLVED; - } - Node node = Rewriter::rewrite(in); - if ((node[0].getKind() == kind::BITVECTOR_EXTRACT && node[1].isConst()) - || (node[1].getKind() == kind::BITVECTOR_EXTRACT - && node[0].isConst())) - { - Node extract = node[0].isConst() ? node[1] : node[0]; - if (extract[0].isVar()) - { - Node c = node[0].isConst() ? node[0] : node[1]; - - unsigned high = utils::getExtractHigh(extract); - unsigned low = utils::getExtractLow(extract); - unsigned var_bitwidth = utils::getSize(extract[0]); - std::vector children; - - if (low == 0) - { - Assert(high != var_bitwidth - 1); - unsigned skolem_size = var_bitwidth - high - 1; - Node skolem = utils::mkVar(skolem_size); - children.push_back(skolem); - children.push_back(c); - } - else if (high == var_bitwidth - 1) - { - unsigned skolem_size = low; - Node skolem = utils::mkVar(skolem_size); - children.push_back(c); - children.push_back(skolem); - } - else - { - unsigned skolem1_size = low; - unsigned skolem2_size = var_bitwidth - high - 1; - Node skolem1 = utils::mkVar(skolem1_size); - Node skolem2 = utils::mkVar(skolem2_size); - children.push_back(skolem2); - children.push_back(c); - children.push_back(skolem1); - } - Node concat = utils::mkConcat(children); - Assert(utils::getSize(concat) == utils::getSize(extract[0])); - if (d_bv.isLegalElimination(extract[0], concat)) - { - outSubstitutions.addSubstitutionSolved(extract[0], concat, tin); - return Theory::PP_ASSERT_STATUS_SOLVED; - } - } - } - } - break; - case kind::BITVECTOR_ULT: - case kind::BITVECTOR_SLT: - case kind::BITVECTOR_ULE: - case kind::BITVECTOR_SLE: - - default: - // TODO other predicates - break; - } - return Theory::PP_ASSERT_STATUS_UNSOLVED; -} - TrustNode BVSolverLazy::ppRewrite(TNode t) { Debug("bv-pp-rewrite") << "BVSolverLazy::ppRewrite " << t << "\n"; diff --git a/src/theory/bv/bv_solver_lazy.h b/src/theory/bv/bv_solver_lazy.h index e11f525f3..57b3e0a08 100644 --- a/src/theory/bv/bv_solver_lazy.h +++ b/src/theory/bv/bv_solver_lazy.h @@ -93,9 +93,6 @@ class BVSolverLazy : public BVSolver std::string identify() const override { return std::string("BVSolverLazy"); } - Theory::PPAssertStatus ppAssert( - TrustNode tin, TrustSubstitutionMap& outSubstitutions) override; - TrustNode ppRewrite(TNode t) override; void ppStaticLearn(TNode in, NodeBuilder& learned) override; @@ -112,7 +109,6 @@ class BVSolverLazy : public BVSolver { public: AverageStat d_avgConflictSize; - IntStat d_solveSubstitutions; TimerStat d_solveTimer; IntStat d_numCallsToCheckFullEffort; IntStat d_numCallsToCheckStandardEffort; diff --git a/src/theory/bv/bv_solver_simple.h b/src/theory/bv/bv_solver_simple.h index 106a473d9..2c23189db 100644 --- a/src/theory/bv/bv_solver_simple.h +++ b/src/theory/bv/bv_solver_simple.h @@ -54,12 +54,6 @@ class BVSolverSimple : public BVSolver std::string identify() const override { return "BVSolverSimple"; }; - Theory::PPAssertStatus ppAssert( - TrustNode in, TrustSubstitutionMap& outSubstitutions) override - { - return Theory::PPAssertStatus::PP_ASSERT_STATUS_UNSOLVED; - } - bool collectModelValues(TheoryModel* m, const std::set& termSet) override; diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index a0f3f28f7..296fca2c0 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -18,11 +18,13 @@ #include "expr/proof_checker.h" #include "options/bv_options.h" #include "options/smt_options.h" +#include "smt/smt_statistics_registry.h" #include "theory/bv/bv_solver_bitblast.h" #include "theory/bv/bv_solver_lazy.h" #include "theory/bv/bv_solver_simple.h" #include "theory/bv/theory_bv_utils.h" #include "theory/ee_setup_info.h" +#include "theory/trust_substitutions.h" namespace cvc5 { namespace theory { @@ -40,7 +42,8 @@ TheoryBV::TheoryBV(context::Context* c, d_rewriter(), d_state(c, u, valuation), d_im(*this, d_state, nullptr, "theory::bv::"), - d_notify(d_im) + d_notify(d_im), + d_stats("theory::bv::") { switch (options::bvSolver()) { @@ -182,7 +185,80 @@ void TheoryBV::propagate(Effort e) { return d_internal->propagate(e); } Theory::PPAssertStatus TheoryBV::ppAssert( TrustNode tin, TrustSubstitutionMap& outSubstitutions) { - return d_internal->ppAssert(tin, outSubstitutions); + TNode in = tin.getNode(); + Kind k = in.getKind(); + if (k == kind::EQUAL) + { + // Substitute variables + if (in[0].isVar() && isLegalElimination(in[0], in[1])) + { + ++d_stats.d_solveSubstitutions; + outSubstitutions.addSubstitutionSolved(in[0], in[1], tin); + return Theory::PP_ASSERT_STATUS_SOLVED; + } + if (in[1].isVar() && isLegalElimination(in[1], in[0])) + { + ++d_stats.d_solveSubstitutions; + outSubstitutions.addSubstitutionSolved(in[1], in[0], tin); + return Theory::PP_ASSERT_STATUS_SOLVED; + } + /** + * Eliminate extract over bit-vector variables. + * + * Given x[h:l] = c, where c is a constant and x is a variable. + * + * We rewrite to: + * + * x = sk1::c if l == 0, where bw(sk1) = bw(x)-1-h + * x = c::sk2 if h == bw(x)-1, where bw(sk2) = l + * x = sk1::c::sk2 otherwise, where bw(sk1) = bw(x)-1-h and bw(sk2) = l + */ + Node node = Rewriter::rewrite(in); + if ((node[0].getKind() == kind::BITVECTOR_EXTRACT && node[1].isConst()) + || (node[1].getKind() == kind::BITVECTOR_EXTRACT + && node[0].isConst())) + { + Node extract = node[0].isConst() ? node[1] : node[0]; + if (extract[0].isVar()) + { + Node c = node[0].isConst() ? node[0] : node[1]; + + uint32_t high = utils::getExtractHigh(extract); + uint32_t low = utils::getExtractLow(extract); + uint32_t var_bw = utils::getSize(extract[0]); + std::vector children; + + // create sk1 with size bw(x)-1-h + if (low == 0 || high != var_bw - 1) + { + Assert(high != var_bw - 1); + uint32_t skolem_size = var_bw - high - 1; + Node skolem = utils::mkVar(skolem_size); + children.push_back(skolem); + } + + children.push_back(c); + + // create sk2 with size l + if (high == var_bw - 1 || low != 0) + { + Assert(low != 0); + uint32_t skolem_size = low; + Node skolem = utils::mkVar(skolem_size); + children.push_back(skolem); + } + + Node concat = utils::mkConcat(children); + Assert(utils::getSize(concat) == utils::getSize(extract[0])); + if (isLegalElimination(extract[0], concat)) + { + outSubstitutions.addSubstitutionSolved(extract[0], concat, tin); + return Theory::PP_ASSERT_STATUS_SOLVED; + } + } + } + } + return Theory::PP_ASSERT_STATUS_UNSOLVED; } TrustNode TheoryBV::ppRewrite(TNode t, std::vector& lems) @@ -221,6 +297,12 @@ bool TheoryBV::applyAbstraction(const std::vector& assertions, return d_internal->applyAbstraction(assertions, new_assertions); } +TheoryBV::Statistics::Statistics(const std::string& name) + : d_solveSubstitutions( + smtStatisticsRegistry().registerInt(name + "NumSolveSubstitutions")) +{ +} + } // namespace bv } // namespace theory } // namespace cvc5 diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 1f14f05b0..4b3a1f3b2 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -122,6 +122,13 @@ class TheoryBV : public Theory /** The notify class for equality engine. */ TheoryEqNotifyClass d_notify; + /** TheoryBV statistics. */ + struct Statistics + { + Statistics(const std::string& name); + IntStat d_solveSubstitutions; + } d_stats; + }; /* class TheoryBV */ } // namespace bv