From 18aef1113bbdb5ce8e007d115f032e425ad10797 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 11 Jun 2021 08:54:32 -0500 Subject: [PATCH] Remove support for lazy BV extended function reductions and inferences (#6728) solve-int-as-bv is now the preferred method for solving these benchmarks. Adds solve-int-as-bv to a regression that became slow in my previous commit. --- src/options/bv_options.toml | 16 -- src/smt/set_defaults.cpp | 26 --- src/theory/bv/bv_solver_lazy.cpp | 33 --- src/theory/bv/bv_solver_lazy.h | 2 - src/theory/bv/bv_subtheory_core.cpp | 214 +----------------- src/theory/bv/bv_subtheory_core.h | 56 ----- src/theory/bv/theory_bv_rewriter.cpp | 18 +- .../regress1/bv/bv2nat-simp-range-sat.smt2 | 2 + 8 files changed, 11 insertions(+), 356 deletions(-) diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml index fcad51ceb..8d4c2b1de 100644 --- a/src/options/bv_options.toml +++ b/src/options/bv_options.toml @@ -190,22 +190,6 @@ name = "Bitvector Theory" default = "false" help = "simplify formula via Gaussian Elimination if applicable" -[[option]] - name = "bvLazyRewriteExtf" - category = "regular" - long = "bv-lazy-rewrite-extf" - type = "bool" - default = "true" - help = "lazily rewrite extended functions like bv2nat and int2bv" - -[[option]] - name = "bvLazyReduceExtf" - category = "regular" - long = "bv-lazy-reduce-extf" - type = "bool" - default = "false" - help = "reduce extended functions like bv2nat and int2bv at last call instead of full effort" - [[option]] name = "bvAlgExtf" category = "regular" diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 31d14c569..67c5c5647 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -189,8 +189,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) if (options::solveBVAsInt() != options::SolveBVAsIntMode::OFF) { - // do not rewrite bv2nat eagerly - opts.bv.bvLazyRewriteExtf = true; if (options::boolToBitvector() != options::BoolToBVMode::OFF) { throw OptionException( @@ -215,14 +213,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) logic.lock(); } } - else if (options::bvSolver() == options::BVSolver::SIMPLE - || options::bvSolver() == options::BVSolver::BITBLAST) - { - // Only BVSolver::LAZY natively supports int2bv and nat2bv, for other - // solvers we need to eagerly eliminate the operators. Note this is only - // applied if we are not eliminating BV (e.g. with solveBVAsInt). - opts.bv.bvLazyReduceExtf = false; - } // set options about ackermannization if (options::ackermann() && options::produceModels() @@ -1401,22 +1391,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.arrays.arraysOptimizeLinear = false; } - if (!options::bitvectorEqualitySolver()) - { - if (options::bvLazyRewriteExtf()) - { - if (opts.bv.bvLazyRewriteExtfWasSetByUser) - { - throw OptionException( - "--bv-lazy-rewrite-extf requires --bv-eq-solver to be set"); - } - } - Trace("smt") - << "disabling bvLazyRewriteExtf since equality solver is disabled" - << std::endl; - opts.bv.bvLazyRewriteExtf = false; - } - if (options::stringFMF() && !opts.strings.stringProcessLoopModeWasSetByUser) { Trace("smt") << "settting stringProcessLoopMode to 'simple' since " diff --git a/src/theory/bv/bv_solver_lazy.cpp b/src/theory/bv/bv_solver_lazy.cpp index fbd910bee..5210117b8 100644 --- a/src/theory/bv/bv_solver_lazy.cpp +++ b/src/theory/bv/bv_solver_lazy.cpp @@ -233,18 +233,6 @@ void BVSolverLazy::check(Theory::Effort e) return; } - // last call : do reductions on extended bitvector functions - if (e == Theory::EFFORT_LAST_CALL) - { - CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE]; - if (core) - { - // check extended functions at last call effort - core->checkExtf(e); - } - return; - } - Debug("bitvector") << "BVSolverLazy::check(" << e << ")" << std::endl; TimerStat::CodeTimer codeTimer(d_statistics.d_solveTimer); // we may be getting new assertions so the model cache may not be sound @@ -331,27 +319,6 @@ void BVSolverLazy::check(Theory::Effort e) break; } } - - // check extended functions - if (Theory::fullEffort(e)) - { - CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE]; - if (core) - { - // check extended functions at full effort - core->checkExtf(e); - } - } -} - -bool BVSolverLazy::needsCheckLastEffort() -{ - CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE]; - if (core) - { - return core->needsCheckLastEffort(); - } - return false; } bool BVSolverLazy::collectModelValues(TheoryModel* m, diff --git a/src/theory/bv/bv_solver_lazy.h b/src/theory/bv/bv_solver_lazy.h index 9b3a2f1fa..4f73354bc 100644 --- a/src/theory/bv/bv_solver_lazy.h +++ b/src/theory/bv/bv_solver_lazy.h @@ -82,8 +82,6 @@ class BVSolverLazy : public BVSolver bool preCheck(Theory::Effort e) override; - bool needsCheckLastEffort() override; - void propagate(Theory::Effort e) override; TrustNode explain(TNode n) override; diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index 2589418cc..fa71641ad 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -32,64 +32,6 @@ using namespace cvc5::theory; using namespace cvc5::theory::bv; using namespace cvc5::theory::bv::utils; -bool CoreSolverExtTheoryCallback::getCurrentSubstitution( - int effort, - const std::vector& vars, - std::vector& subs, - std::map >& exp) -{ - if (d_equalityEngine == nullptr) - { - return false; - } - // get the constant equivalence classes - bool retVal = false; - for (const Node& n : vars) - { - if (d_equalityEngine->hasTerm(n)) - { - Node nr = d_equalityEngine->getRepresentative(n); - if (nr.isConst()) - { - subs.push_back(nr); - exp[n].push_back(n.eqNode(nr)); - retVal = true; - } - else - { - subs.push_back(n); - } - } - else - { - subs.push_back(n); - } - } - // return true if the substitution is non-trivial - return retVal; -} - -bool CoreSolverExtTheoryCallback::getReduction(int effort, - Node n, - Node& nr, - bool& satDep) -{ - Trace("bv-ext") << "TheoryBV::checkExt : non-reduced : " << n << std::endl; - if (n.getKind() == kind::BITVECTOR_TO_NAT) - { - nr = utils::eliminateBv2Nat(n); - satDep = false; - return true; - } - else if (n.getKind() == kind::INT_TO_BITVECTOR) - { - nr = utils::eliminateInt2Bv(n); - satDep = false; - return true; - } - return false; -} - CoreSolver::CoreSolver(context::Context* c, BVSolverLazy* bv) : SubtheorySolver(c, bv), d_notify(*this), @@ -98,18 +40,8 @@ CoreSolver::CoreSolver(context::Context* c, BVSolverLazy* bv) d_preregisterCalled(false), d_checkCalled(false), d_bv(bv), - d_extTheoryCb(), - d_extTheory(new ExtTheory(d_extTheoryCb, - bv->d_bv.getSatContext(), - bv->d_bv.getUserContext(), - bv->d_bv.getOutputChannel())), - d_reasons(c), - d_needsLastCallCheck(false), - d_extf_range_infer(bv->d_bv.getUserContext()), - d_extf_collapse_infer(bv->d_bv.getUserContext()) + d_reasons(c) { - d_extTheory->addFunctionKind(kind::BITVECTOR_TO_NAT); - d_extTheory->addFunctionKind(kind::INT_TO_BITVECTOR); } CoreSolver::~CoreSolver() {} @@ -167,11 +99,6 @@ void CoreSolver::preRegister(TNode node) { d_equalityEngine->addTriggerPredicate(node); } else { d_equalityEngine->addTerm(node); - // Register with the extended theory, for context-dependent simplification. - // Notice we do this for registered terms but not internally generated - // equivalence classes. The two should roughly cooincide. Since ExtTheory is - // being used as a heuristic, it is good enough to be registered here. - d_extTheory->registerTerm(node); } } @@ -489,142 +416,3 @@ CoreSolver::Statistics::Statistics() "theory::bv::CoreSolver::NumCallsToCheck")) { } - -void CoreSolver::checkExtf(Theory::Effort e) -{ - if (e == Theory::EFFORT_LAST_CALL) - { - std::vector nred = d_extTheory->getActive(); - doExtfReductions(nred); - } - Assert(e == Theory::EFFORT_FULL); - // do inferences (adds external lemmas) TODO: this can be improved to add - // internal inferences - std::vector nred; - if (d_extTheory->doInferences(0, nred)) - { - return; - } - d_needsLastCallCheck = false; - if (!nred.empty()) - { - // other inferences involving bv2nat, int2bv - if (options::bvAlgExtf()) - { - if (doExtfInferences(nred)) - { - return; - } - } - if (!options::bvLazyReduceExtf()) - { - if (doExtfReductions(nred)) - { - return; - } - } - else - { - d_needsLastCallCheck = true; - } - } -} - -bool CoreSolver::needsCheckLastEffort() const { return d_needsLastCallCheck; } - -bool CoreSolver::doExtfInferences(std::vector& terms) -{ - NodeManager* nm = NodeManager::currentNM(); - SkolemManager* sm = nm->getSkolemManager(); - bool sentLemma = false; - eq::EqualityEngine* ee = d_equalityEngine; - std::map op_map; - for (unsigned j = 0; j < terms.size(); j++) - { - TNode n = terms[j]; - Assert(n.getKind() == kind::BITVECTOR_TO_NAT - || n.getKind() == kind::INT_TO_BITVECTOR); - if (n.getKind() == kind::BITVECTOR_TO_NAT) - { - // range lemmas - if (d_extf_range_infer.find(n) == d_extf_range_infer.end()) - { - d_extf_range_infer.insert(n); - unsigned bvs = n[0].getType().getBitVectorSize(); - Node min = nm->mkConst(Rational(0)); - Node max = nm->mkConst(Rational(Integer(1).multiplyByPow2(bvs))); - Node lem = nm->mkNode(kind::AND, - nm->mkNode(kind::GEQ, n, min), - nm->mkNode(kind::LT, n, max)); - Trace("bv-extf-lemma") - << "BV extf lemma (range) : " << lem << std::endl; - d_bv->d_im.lemma(lem, InferenceId::BV_EXTF_LEMMA); - sentLemma = true; - } - } - Node r = (ee && ee->hasTerm(n[0])) ? ee->getRepresentative(n[0]) : n[0]; - op_map[r] = n; - } - for (unsigned j = 0; j < terms.size(); j++) - { - TNode n = terms[j]; - Node r = (ee && ee->hasTerm(n[0])) ? ee->getRepresentative(n) : n; - std::map::iterator it = op_map.find(r); - if (it != op_map.end()) - { - Node parent = it->second; - // Node cterm = parent[0]==n ? parent : nm->mkNode( parent.getOperator(), - // n ); - Node cterm = parent[0].eqNode(n); - Trace("bv-extf-lemma-debug") - << "BV extf collapse based on : " << cterm << std::endl; - if (d_extf_collapse_infer.find(cterm) == d_extf_collapse_infer.end()) - { - d_extf_collapse_infer.insert(cterm); - - Node t = n[0]; - if (t.getType() == parent.getType()) - { - if (n.getKind() == kind::INT_TO_BITVECTOR) - { - Assert(t.getType().isInteger()); - // congruent modulo 2^( bv width ) - unsigned bvs = n.getType().getBitVectorSize(); - Node coeff = nm->mkConst(Rational(Integer(1).multiplyByPow2(bvs))); - Node k = sm->mkDummySkolem( - "int_bv_cong", t.getType(), "for int2bv/bv2nat congruence"); - t = nm->mkNode(kind::PLUS, t, nm->mkNode(kind::MULT, coeff, k)); - } - Node lem = parent.eqNode(t); - - if (parent[0] != n) - { - Assert(ee->areEqual(parent[0], n)); - lem = nm->mkNode(kind::IMPLIES, parent[0].eqNode(n), lem); - } - // this handles inferences of the form, e.g.: - // ((_ int2bv w) (bv2nat x)) == x (if x is bit-width w) - // (bv2nat ((_ int2bv w) x)) == x + k*2^w for some k - Trace("bv-extf-lemma") - << "BV extf lemma (collapse) : " << lem << std::endl; - d_bv->d_im.lemma(lem, InferenceId::BV_EXTF_COLLAPSE); - sentLemma = true; - } - } - Trace("bv-extf-lemma-debug") - << "BV extf f collapse based on : " << cterm << std::endl; - } - } - return sentLemma; -} - -bool CoreSolver::doExtfReductions(std::vector& terms) -{ - std::vector nredr; - if (d_extTheory->doReductions(0, terms, nredr)) - { - return true; - } - Assert(nredr.empty()); - return false; -} diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h index 0dfcfdde4..46c4559ea 100644 --- a/src/theory/bv/bv_subtheory_core.h +++ b/src/theory/bv/bv_subtheory_core.h @@ -22,30 +22,11 @@ #include "context/cdhashset.h" #include "theory/bv/bv_subtheory.h" -#include "theory/ext_theory.h" namespace cvc5 { namespace theory { namespace bv { -class Base; - -/** An extended theory callback used by the core solver */ -class CoreSolverExtTheoryCallback : public ExtTheoryCallback -{ - public: - CoreSolverExtTheoryCallback() : d_equalityEngine(nullptr) {} - /** Get current substitution based on the underlying equality engine. */ - bool getCurrentSubstitution(int effort, - const std::vector& vars, - std::vector& subs, - std::map >& exp) override; - /** Get reduction. */ - bool getReduction(int effort, Node n, Node& nr, bool& satDep) override; - /** The underlying equality engine */ - eq::EqualityEngine* d_equalityEngine; -}; - /** * Bitvector equality solver */ @@ -96,10 +77,6 @@ class CoreSolver : public SubtheorySolver { BVSolverLazy* d_bv; /** Pointer to the equality engine of the parent */ eq::EqualityEngine* d_equalityEngine; - /** The extended theory callback */ - CoreSolverExtTheoryCallback d_extTheoryCb; - /** Extended theory module, for context-dependent simplification. */ - std::unique_ptr d_extTheory; /** To make sure we keep the explanations */ context::CDHashSet d_reasons; @@ -109,36 +86,6 @@ class CoreSolver : public SubtheorySolver { bool isCompleteForTerm(TNode term, TNodeBoolMap& seen); Statistics d_statistics; - /** Whether we need a last call effort check */ - bool d_needsLastCallCheck; - /** For extended functions */ - context::CDHashSet d_extf_range_infer; - context::CDHashSet d_extf_collapse_infer; - - /** do extended function inferences - * - * This method adds lemmas on the output channel of TheoryBV based on - * reasoning about extended functions, such as bv2nat and int2bv. Examples - * of lemmas added by this method include: - * 0 <= ((_ int2bv w) x) < 2^w - * ((_ int2bv w) (bv2nat x)) = x - * (bv2nat ((_ int2bv w) x)) == x + k*2^w - * The purpose of these lemmas is to recognize easy conflicts before fully - * reducing extended functions based on their full semantics. - */ - bool doExtfInferences(std::vector& terms); - /** do extended function reductions - * - * This method adds lemmas on the output channel of TheoryBV based on - * reducing all extended function applications that are preregistered to - * this theory and have not already been reduced by context-dependent - * simplification (see theory/ext_theory.h). Examples of lemmas added by - * this method include: - * (bv2nat x) = (ite ((_ extract w w-1) x) 2^{w-1} 0) + ... + - * (ite ((_ extract 1 0) x) 1 0) - */ - bool doExtfReductions(std::vector& terms); - public: CoreSolver(context::Context* c, BVSolverLazy* bv); ~CoreSolver(); @@ -154,9 +101,6 @@ class CoreSolver : public SubtheorySolver { EqualityStatus getEqualityStatus(TNode a, TNode b) override; bool hasTerm(TNode node) const; void addTermToEqualityEngine(TNode node); - /** check extended functions at the given effort */ - void checkExtf(Theory::Effort e); - bool needsCheckLastEffort() const; }; } diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 4e1076763..97ca24437 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -65,16 +65,14 @@ TrustNode TheoryBVRewriter::expandDefinition(Node node) case kind::BITVECTOR_SREM: case kind::BITVECTOR_SMOD: ret = eliminateBVSDiv(node); break; case kind::BITVECTOR_TO_NAT: - if (!options::bvLazyReduceExtf()) - { + ret = utils::eliminateBv2Nat(node); - } + break; case kind::INT_TO_BITVECTOR: - if (!options::bvLazyReduceExtf()) - { + ret = utils::eliminateInt2Bv(node); - } + break; default: break; } @@ -646,8 +644,8 @@ RewriteResponse TheoryBVRewriter::RewriteRedand(TNode node, bool prerewrite){ } RewriteResponse TheoryBVRewriter::RewriteBVToNat(TNode node, bool prerewrite) { - //do not use lazy rewrite strategy if equality solver is disabled - if( node[0].isConst() || !options::bvLazyRewriteExtf() ){ + if (node[0].isConst()) + { Node resultNode = LinearRewriteStrategy < RewriteRule >::apply(node); @@ -658,8 +656,8 @@ RewriteResponse TheoryBVRewriter::RewriteBVToNat(TNode node, bool prerewrite) { } RewriteResponse TheoryBVRewriter::RewriteIntToBV(TNode node, bool prerewrite) { - //do not use lazy rewrite strategy if equality solver is disabled - if( node[0].isConst() || !options::bvLazyRewriteExtf() ){ + if (node[0].isConst()) + { Node resultNode = LinearRewriteStrategy < RewriteRule >::apply(node); diff --git a/test/regress/regress1/bv/bv2nat-simp-range-sat.smt2 b/test/regress/regress1/bv/bv2nat-simp-range-sat.smt2 index 9da8d4ca8..66b286da1 100644 --- a/test/regress/regress1/bv/bv2nat-simp-range-sat.smt2 +++ b/test/regress/regress1/bv/bv2nat-simp-range-sat.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --solve-bv-as-int=sum +; EXPECT: sat (set-logic ALL) (set-info :status sat) (declare-fun t () (_ BitVec 16)) -- 2.30.2