From c9e23f66383a4d490aca6d082d40117fe799ee4b Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Thu, 3 Sep 2020 18:34:19 -0700 Subject: [PATCH] Split lazy bit-vector solver from TheoryBV (#5009) This commit separates the lazy bit-vector solver from TheoryBV, which is now a thin wrapper around a bit-vector solver d_internal . This will allow us to easily swap out the bit-vector solver in the future. --- src/CMakeLists.txt | 3 + src/theory/bv/bitblast/eager_bitblaster.cpp | 6 +- src/theory/bv/bitblast/eager_bitblaster.h | 6 +- src/theory/bv/bitblast/lazy_bitblaster.cpp | 20 +- src/theory/bv/bitblast/lazy_bitblaster.h | 10 +- src/theory/bv/bv_eager_solver.cpp | 2 +- src/theory/bv/bv_eager_solver.h | 6 +- src/theory/bv/bv_quick_check.cpp | 12 +- src/theory/bv/bv_quick_check.h | 137 ++-- src/theory/bv/bv_solver.h | 119 +++ src/theory/bv/bv_solver_lazy.cpp | 835 ++++++++++++++++++++ src/theory/bv/bv_solver_lazy.h | 240 ++++++ src/theory/bv/bv_subtheory.h | 13 +- src/theory/bv/bv_subtheory_algebraic.cpp | 7 +- src/theory/bv/bv_subtheory_algebraic.h | 149 ++-- src/theory/bv/bv_subtheory_bitblast.cpp | 5 +- src/theory/bv/bv_subtheory_bitblast.h | 17 +- src/theory/bv/bv_subtheory_core.cpp | 23 +- src/theory/bv/bv_subtheory_core.h | 4 +- src/theory/bv/bv_subtheory_inequality.cpp | 2 +- src/theory/bv/bv_subtheory_inequality.h | 39 +- src/theory/bv/theory_bv.cpp | 830 +++---------------- src/theory/bv/theory_bv.h | 180 +---- src/theory/theory_inference_manager.cpp | 10 + src/theory/theory_inference_manager.h | 11 + src/theory/theory_state.cpp | 5 + src/theory/theory_state.h | 3 + test/unit/theory/theory_bv_white.h | 25 +- 28 files changed, 1606 insertions(+), 1113 deletions(-) create mode 100644 src/theory/bv/bv_solver.h create mode 100644 src/theory/bv/bv_solver_lazy.cpp create mode 100644 src/theory/bv/bv_solver_lazy.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index a0fd277f8..6cd2c24d1 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -406,6 +406,9 @@ libcvc4_add_sources( theory/bv/bv_inequality_graph.h theory/bv/bv_quick_check.cpp theory/bv/bv_quick_check.h + theory/bv/bv_solver.h + theory/bv/bv_solver_lazy.cpp + theory/bv/bv_solver_lazy.h theory/bv/bv_subtheory.h theory/bv/bv_subtheory_algebraic.cpp theory/bv/bv_subtheory_algebraic.h diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp index 627a17bc5..6417740fd 100644 --- a/src/theory/bv/bitblast/eager_bitblaster.cpp +++ b/src/theory/bv/bitblast/eager_bitblaster.cpp @@ -14,14 +14,14 @@ ** Bitblaster for the eager bv solver. **/ -#include "cvc4_private.h" - #include "theory/bv/bitblast/eager_bitblaster.h" +#include "cvc4_private.h" #include "options/bv_options.h" #include "prop/cnf_stream.h" #include "prop/sat_solver_factory.h" #include "smt/smt_statistics_registry.h" +#include "theory/bv/bv_solver_lazy.h" #include "theory/bv/theory_bv.h" #include "theory/theory_model.h" @@ -29,7 +29,7 @@ namespace CVC4 { namespace theory { namespace bv { -EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv, context::Context* c) +EagerBitblaster::EagerBitblaster(BVSolverLazy* theory_bv, context::Context* c) : TBitblaster(), d_context(c), d_satSolver(), diff --git a/src/theory/bv/bitblast/eager_bitblaster.h b/src/theory/bv/bitblast/eager_bitblaster.h index da9488d43..b57f1ee0b 100644 --- a/src/theory/bv/bitblast/eager_bitblaster.h +++ b/src/theory/bv/bitblast/eager_bitblaster.h @@ -31,12 +31,12 @@ namespace theory { namespace bv { class BitblastingRegistrar; -class TheoryBV; +class BVSolverLazy; class EagerBitblaster : public TBitblaster { public: - EagerBitblaster(TheoryBV* theory_bv, context::Context* context); + EagerBitblaster(BVSolverLazy* theory_bv, context::Context* context); ~EagerBitblaster(); void addAtom(TNode atom); @@ -61,7 +61,7 @@ class EagerBitblaster : public TBitblaster std::unique_ptr d_satSolver; std::unique_ptr d_bitblastingRegistrar; - TheoryBV* d_bv; + BVSolverLazy* d_bv; TNodeSet d_bbAtoms; TNodeSet d_variables; diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp index 3109d6ed7..3e32b4cc3 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.cpp +++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp @@ -14,16 +14,16 @@ ** Bitblaster for the lazy bv solver. **/ -#include "cvc4_private.h" - #include "theory/bv/bitblast/lazy_bitblaster.h" +#include "cvc4_private.h" #include "options/bv_options.h" #include "prop/cnf_stream.h" #include "prop/sat_solver.h" #include "prop/sat_solver_factory.h" #include "smt/smt_statistics_registry.h" #include "theory/bv/abstraction.h" +#include "theory/bv/bv_solver_lazy.h" #include "theory/bv/theory_bv.h" #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" @@ -58,7 +58,7 @@ uint64_t numNodes(TNode node, utils::NodeSet& seen) } TLazyBitblaster::TLazyBitblaster(context::Context* c, - bv::TheoryBV* bv, + bv::BVSolverLazy* bv, const std::string name, bool emptyNotify) : TBitblaster(), @@ -292,8 +292,12 @@ bool TLazyBitblaster::assertToSat(TNode lit, bool propagate) { markerLit = ~markerLit; } - Debug("bitvector-bb") << "TheoryBV::TLazyBitblaster::assertToSat asserting node: " << atom <<"\n"; - Debug("bitvector-bb") << "TheoryBV::TLazyBitblaster::assertToSat with literal: " << markerLit << "\n"; + Debug("bitvector-bb") + << "BVSolverLazy::TLazyBitblaster::assertToSat asserting node: " << atom + << "\n"; + Debug("bitvector-bb") + << "BVSolverLazy::TLazyBitblaster::assertToSat with literal: " + << markerLit << "\n"; prop::SatValue ret = d_satSolver->assertAssumption(markerLit, propagate); @@ -410,9 +414,9 @@ void TLazyBitblaster::MinisatNotify::notify(prop::SatClause& clause) { lemmab << d_cnf->getNode(clause[i]); } Node lemma = lemmab; - d_bv->d_out->lemma(lemma); + d_bv->d_inferManager.lemma(lemma); } else { - d_bv->d_out->lemma(d_cnf->getNode(clause[0])); + d_bv->d_inferManager.lemma(d_cnf->getNode(clause[0])); } } @@ -423,7 +427,7 @@ void TLazyBitblaster::MinisatNotify::spendResource(ResourceManager::Resource r) void TLazyBitblaster::MinisatNotify::safePoint(ResourceManager::Resource r) { - d_bv->d_out->safePoint(r); + d_bv->d_inferManager.safePoint(r); } EqualityStatus TLazyBitblaster::getEqualityStatus(TNode a, TNode b) diff --git a/src/theory/bv/bitblast/lazy_bitblaster.h b/src/theory/bv/bitblast/lazy_bitblaster.h index bc930aec4..e53f1697d 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.h +++ b/src/theory/bv/bitblast/lazy_bitblaster.h @@ -32,7 +32,7 @@ namespace CVC4 { namespace theory { namespace bv { -class TheoryBV; +class BVSolverLazy; class TLazyBitblaster : public TBitblaster { @@ -45,7 +45,7 @@ class TLazyBitblaster : public TBitblaster bool hasBBAtom(TNode atom) const override; TLazyBitblaster(context::Context* c, - TheoryBV* bv, + BVSolverLazy* bv, const std::string name = "", bool emptyNotify = false); ~TLazyBitblaster(); @@ -108,11 +108,11 @@ class TLazyBitblaster : public TBitblaster class MinisatNotify : public prop::BVSatSolverNotify { prop::CnfStream* d_cnf; - TheoryBV* d_bv; + BVSolverLazy* d_bv; TLazyBitblaster* d_lazyBB; public: - MinisatNotify(prop::CnfStream* cnf, TheoryBV* bv, TLazyBitblaster* lbv) + MinisatNotify(prop::CnfStream* cnf, BVSolverLazy* bv, TLazyBitblaster* lbv) : d_cnf(cnf), d_bv(bv), d_lazyBB(lbv) { } @@ -123,7 +123,7 @@ class TLazyBitblaster : public TBitblaster void safePoint(ResourceManager::Resource r) override; }; - TheoryBV* d_bv; + BVSolverLazy* d_bv; context::Context* d_ctx; std::unique_ptr d_nullRegistrar; diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp index d1490374d..fcb678987 100644 --- a/src/theory/bv/bv_eager_solver.cpp +++ b/src/theory/bv/bv_eager_solver.cpp @@ -26,7 +26,7 @@ namespace CVC4 { namespace theory { namespace bv { -EagerBitblastSolver::EagerBitblastSolver(context::Context* c, TheoryBV* bv) +EagerBitblastSolver::EagerBitblastSolver(context::Context* c, BVSolverLazy* bv) : d_assertionSet(c), d_assumptionSet(c), d_context(c), diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h index e0b55c23b..eef824af4 100644 --- a/src/theory/bv/bv_eager_solver.h +++ b/src/theory/bv/bv_eager_solver.h @@ -23,7 +23,7 @@ #include #include "expr/node.h" -#include "theory/bv/theory_bv.h" +#include "theory/bv/bv_solver_lazy.h" #include "theory/theory_model.h" namespace CVC4 { @@ -38,7 +38,7 @@ class AigBitblaster; */ class EagerBitblastSolver { public: - EagerBitblastSolver(context::Context* c, theory::bv::TheoryBV* bv); + EagerBitblastSolver(context::Context* c, theory::bv::BVSolverLazy* bv); ~EagerBitblastSolver(); bool checkSat(); void assertFormula(TNode formula); @@ -58,7 +58,7 @@ class EagerBitblastSolver { std::unique_ptr d_aigBitblaster; bool d_useAig; - TheoryBV* d_bv; + BVSolverLazy* d_bv; }; // class EagerBitblastSolver } // namespace bv diff --git a/src/theory/bv/bv_quick_check.cpp b/src/theory/bv/bv_quick_check.cpp index ed445eb33..f8e30247f 100644 --- a/src/theory/bv/bv_quick_check.cpp +++ b/src/theory/bv/bv_quick_check.cpp @@ -18,6 +18,7 @@ #include "smt/smt_statistics_registry.h" #include "theory/bv/bitblast/lazy_bitblaster.h" +#include "theory/bv/bv_solver_lazy.h" #include "theory/bv/theory_bv_utils.h" using namespace CVC4::prop; @@ -26,11 +27,12 @@ namespace CVC4 { namespace theory { namespace bv { -BVQuickCheck::BVQuickCheck(const std::string& name, theory::bv::TheoryBV* bv) - : d_ctx() - , d_bitblaster(new TLazyBitblaster(&d_ctx, bv, name, true)) - , d_conflict() - , d_inConflict(&d_ctx, false) +BVQuickCheck::BVQuickCheck(const std::string& name, + theory::bv::BVSolverLazy* bv) + : d_ctx(), + d_bitblaster(new TLazyBitblaster(&d_ctx, bv, name, true)), + d_conflict(), + d_inConflict(&d_ctx, false) {} diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h index 03a62e41b..c1d9e333e 100644 --- a/src/theory/bv/bv_quick_check.h +++ b/src/theory/bv/bv_quick_check.h @@ -19,8 +19,8 @@ #ifndef CVC4__BV_QUICK_CHECK_H #define CVC4__BV_QUICK_CHECK_H -#include #include +#include #include "context/cdo.h" #include "expr/node.h" @@ -36,43 +36,44 @@ class TheoryModel; namespace bv { class TLazyBitblaster; -class TheoryBV; +class BVSolverLazy; -class BVQuickCheck { +class BVQuickCheck +{ context::Context d_ctx; std::unique_ptr d_bitblaster; Node d_conflict; context::CDO d_inConflict; void setConflict(); -public: - BVQuickCheck(const std::string& name, theory::bv::TheoryBV* bv); + public: + BVQuickCheck(const std::string& name, theory::bv::BVSolverLazy* bv); ~BVQuickCheck(); bool inConflict(); Node getConflict() { return d_conflict; } - /** + /** * Checks the satisfiability for a given set of assumptions. - * + * * @param assumptions literals assumed true * @param budget max number of conflicts - * - * @return + * + * @return */ prop::SatValue checkSat(std::vector& assumptions, unsigned long budget); - /** + /** * Checks the satisfiability of given assertions. - * + * * @param budget max number of conflicts - * - * @return + * + * @return */ prop::SatValue checkSat(unsigned long budget); - - /** + + /** * Convert to CNF and assert the given literal. - * + * * @param assumption bv literal - * + * * @return false if a conflict has been found via bcp. */ bool addAssertion(TNode assumption); @@ -80,36 +81,37 @@ public: void push(); void pop(); void popToZero(); - /** + /** * Deletes the SAT solver and CNF stream, but maintains the - * bit-blasting term cache. - * + * bit-blasting term cache. + * */ - void clearSolver(); + void clearSolver(); - /** + /** * Computes the size of the circuit required to bit-blast - * atom, by not recounting the nodes in seen. - * - * @param node - * @param seen - * - * @return + * atom, by not recounting the nodes in seen. + * + * @param node + * @param seen + * + * @return */ uint64_t computeAtomWeight(TNode atom, NodeSet& seen); bool collectModelInfo(theory::TheoryModel* model, bool fullModel); - typedef std::unordered_set::const_iterator vars_iterator; - vars_iterator beginVars(); - vars_iterator endVars(); - - Node getVarValue(TNode var, bool fullModel); + typedef std::unordered_set::const_iterator + vars_iterator; + vars_iterator beginVars(); + vars_iterator endVars(); + Node getVarValue(TNode var, bool fullModel); }; - -class QuickXPlain { - struct Statistics { +class QuickXPlain +{ + struct Statistics + { TimerStat d_xplainTime; IntStat d_numSolved; IntStat d_numUnknown; @@ -124,52 +126,59 @@ class QuickXPlain { unsigned long d_budget; // crazy heuristic variables - unsigned d_numCalled; // number of times called - double d_minRatioSum; // sum of minimization ratio for computing average min ratio - unsigned d_numConflicts; // number of conflicts (including when minimization not applied) + unsigned d_numCalled; // number of times called + double d_minRatioSum; // sum of minimization ratio for computing average min + // ratio + unsigned d_numConflicts; // number of conflicts (including when minimization + // not applied) // unsigned d_period; // after how many conflicts to try minimizing again // double d_thresh; // if minimization ratio is less, increase period - // double d_hardThresh; // decrease period if minimization ratio is greater than this - - + // double d_hardThresh; // decrease period if minimization ratio is greater + // than this + Statistics d_statistics; - /** + /** * Uses solve with assumptions unsat core feature to * further minimize a conflict. The minimized conflict * will be between low and the returned value in conflict. - * - * @param low - * @param high - * @param conflict - * - * @return + * + * @param low + * @param high + * @param conflict + * + * @return */ - unsigned selectUnsatCore(unsigned low, unsigned high, + unsigned selectUnsatCore(unsigned low, + unsigned high, std::vector& conflict); - /** + /** * Internal conflict minimization, attempts to minimize * literals in conflict between low and high and adds the - * result in new_conflict. - * - * @param low - * @param high - * @param conflict - * @param new_conflict + * result in new_conflict. + * + * @param low + * @param high + * @param conflict + * @param new_conflict */ - void minimizeConflictInternal(unsigned low, unsigned high, + void minimizeConflictInternal(unsigned low, + unsigned high, std::vector& conflict, std::vector& new_conflict); bool useHeuristic(); -public: - QuickXPlain(const std::string& name, BVQuickCheck* solver, unsigned long budged = 10000); + + public: + QuickXPlain(const std::string& name, + BVQuickCheck* solver, + unsigned long budged = 10000); ~QuickXPlain(); - Node minimizeConflict(TNode conflict); + Node minimizeConflict(TNode conflict); }; -} /* bv namespace */ -} /* theory namespace */ -} /* CVC4 namespace */ +} // namespace bv +} // namespace theory +} // namespace CVC4 #endif /* CVC4__BV_QUICK_CHECK_H */ diff --git a/src/theory/bv/bv_solver.h b/src/theory/bv/bv_solver.h new file mode 100644 index 000000000..fef95ceef --- /dev/null +++ b/src/theory/bv/bv_solver.h @@ -0,0 +1,119 @@ +/********************* */ +/*! \file bv_solver.h + ** \verbatim + ** Top contributors (to current version): + ** Mathias Preiner + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Bit-vector solver interface. + ** + ** Describes the interface for the internal bit-vector solver of TheoryBV. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__BV__BV_SOLVER_H +#define CVC4__THEORY__BV__BV_SOLVER_H + +#include "theory/theory.h" + +namespace CVC4 { +namespace theory { +namespace bv { + +class BVSolver +{ + public: + BVSolver(TheoryState& state, TheoryInferenceManager& inferMgr) + : d_state(state), d_inferManager(inferMgr){}; + + virtual ~BVSolver(){}; + + /** + * Returns true if we need an equality engine. If so, we initialize the + * information regarding how it should be setup. For details, see the + * documentation in Theory::needsEqualityEngine. + */ + virtual bool needsEqualityEngine(EeSetupInfo& esi) { return false; } + + virtual void finishInit(){}; + + virtual void preRegisterTerm(TNode n) = 0; + + /** + * Forwarded from TheoryBV::preCheck(). + */ + virtual bool preCheck(Theory::Effort level = Theory::Effort::EFFORT_FULL) + { + return false; + } + /** + * Forwarded from TheoryBV::postCheck(). + */ + virtual void postCheck(Theory::Effort level = Theory::Effort::EFFORT_FULL){}; + /** + * Forwarded from TheoryBV:preNotifyFact(). + */ + virtual bool preNotifyFact( + TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal) + { + return false; + } + /** + * Forwarded from TheoryBV::notifyFact(). + */ + virtual void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) {} + + virtual bool needsCheckLastEffort() = 0; + + virtual void propagate(Theory::Effort e){}; + + virtual TrustNode explain(TNode n) + { + Unimplemented() << "BVSolver propagated a node but doesn't implement the " + "BVSolver::explain() interface!"; + return TrustNode::null(); + }; + + /** + * This is temporary only and will be deprecated soon in favor of + * Theory::collectModelValues. + */ + virtual bool collectModelInfo(TheoryModel* m) = 0; + + virtual std::string identify() const = 0; + + virtual Theory::PPAssertStatus ppAssert( + TNode in, SubstitutionMap& outSubstitutions) = 0; + + virtual TrustNode ppRewrite(TNode t) { return TrustNode::null(); }; + + virtual void ppStaticLearn(TNode in, NodeBuilder<>& learned){}; + + virtual void presolve(){}; + + virtual void notifySharedTerm(TNode t) = 0; + + virtual EqualityStatus getEqualityStatus(TNode a, TNode b) + { + return EqualityStatus::EQUALITY_UNKNOWN; + } + + /** Called by abstraction preprocessing pass. */ + virtual bool applyAbstraction(const std::vector& assertions, + std::vector& new_assertions) = 0; + + protected: + TheoryState& d_state; + TheoryInferenceManager& d_inferManager; +}; + +} // namespace bv +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__BV__BV_SOLVER_H */ diff --git a/src/theory/bv/bv_solver_lazy.cpp b/src/theory/bv/bv_solver_lazy.cpp new file mode 100644 index 000000000..ad673b402 --- /dev/null +++ b/src/theory/bv/bv_solver_lazy.cpp @@ -0,0 +1,835 @@ +/********************* */ +/*! \file theory_bv_lazy.cpp + ** \verbatim + ** Top contributors (to current version): + ** Liana Hadarean, Andrew Reynolds, Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "theory/bv/bv_solver_lazy.h" + +#include "expr/node_algorithm.h" +#include "options/bv_options.h" +#include "options/smt_options.h" +#include "smt/smt_statistics_registry.h" +#include "theory/bv/abstraction.h" +#include "theory/bv/bv_eager_solver.h" +#include "theory/bv/bv_subtheory_algebraic.h" +#include "theory/bv/bv_subtheory_bitblast.h" +#include "theory/bv/bv_subtheory_core.h" +#include "theory/bv/bv_subtheory_inequality.h" +#include "theory/bv/theory_bv_rewrite_rules_normalization.h" +#include "theory/bv/theory_bv_rewrite_rules_simplification.h" +#include "theory/bv/theory_bv_rewriter.h" +#include "theory/bv/theory_bv_utils.h" +#include "theory/theory_model.h" + +using namespace CVC4::theory::bv::utils; + +namespace CVC4 { +namespace theory { +namespace bv { + +BVSolverLazy::BVSolverLazy(TheoryBV& bv, + context::Context* c, + context::UserContext* u, + ProofNodeManager* pnm, + std::string name) + : BVSolver(bv.d_state, bv.d_inferMgr), + d_bv(bv), + d_context(c), + d_alreadyPropagatedSet(c), + d_sharedTermsSet(c), + d_subtheories(), + d_subtheoryMap(), + d_statistics(), + d_staticLearnCache(), + d_lemmasAdded(c, false), + d_conflict(c, false), + d_invalidateModelCache(c, true), + d_literalsToPropagate(c), + d_literalsToPropagateIndex(c, 0), + d_propagatedBy(c), + d_eagerSolver(), + d_abstractionModule(new AbstractionModule(getStatsPrefix(THEORY_BV))), + d_calledPreregister(false) +{ + if (options::bitblastMode() == options::BitblastMode::EAGER) + { + d_eagerSolver.reset(new EagerBitblastSolver(c, this)); + return; + } + + if (options::bitvectorEqualitySolver()) + { + d_subtheories.emplace_back(new CoreSolver(c, this)); + d_subtheoryMap[SUB_CORE] = d_subtheories.back().get(); + } + + if (options::bitvectorInequalitySolver()) + { + d_subtheories.emplace_back(new InequalitySolver(c, u, this)); + d_subtheoryMap[SUB_INEQUALITY] = d_subtheories.back().get(); + } + + if (options::bitvectorAlgebraicSolver()) + { + d_subtheories.emplace_back(new AlgebraicSolver(c, this)); + d_subtheoryMap[SUB_ALGEBRAIC] = d_subtheories.back().get(); + } + + BitblastSolver* bb_solver = new BitblastSolver(c, this); + if (options::bvAbstraction()) + { + bb_solver->setAbstraction(d_abstractionModule.get()); + } + d_subtheories.emplace_back(bb_solver); + d_subtheoryMap[SUB_BITBLAST] = bb_solver; +} + +BVSolverLazy::~BVSolverLazy() {} + +bool BVSolverLazy::needsEqualityEngine(EeSetupInfo& esi) +{ + CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE]; + if (core) + { + return core->needsEqualityEngine(esi); + } + // otherwise we don't use an equality engine + return false; +} + +void BVSolverLazy::finishInit() +{ + CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE]; + if (core) + { + // must finish initialization in the core solver + core->finishInit(); + } +} + +void BVSolverLazy::spendResource(ResourceManager::Resource r) +{ + d_inferManager.spendResource(r); +} + +BVSolverLazy::Statistics::Statistics() + : d_avgConflictSize("theory::bv::lazy::AvgBVConflictSize"), + d_solveSubstitutions("theory::bv::lazy::NumSolveSubstitutions", 0), + d_solveTimer("theory::bv::lazy::solveTimer"), + d_numCallsToCheckFullEffort("theory::bv::lazy::NumFullCheckCalls", 0), + d_numCallsToCheckStandardEffort("theory::bv::lazy::NumStandardCheckCalls", + 0), + d_weightComputationTimer("theory::bv::lazy::weightComputationTimer"), + d_numMultSlice("theory::bv::lazy::NumMultSliceApplied", 0) +{ + smtStatisticsRegistry()->registerStat(&d_avgConflictSize); + smtStatisticsRegistry()->registerStat(&d_solveSubstitutions); + smtStatisticsRegistry()->registerStat(&d_solveTimer); + smtStatisticsRegistry()->registerStat(&d_numCallsToCheckFullEffort); + smtStatisticsRegistry()->registerStat(&d_numCallsToCheckStandardEffort); + smtStatisticsRegistry()->registerStat(&d_weightComputationTimer); + smtStatisticsRegistry()->registerStat(&d_numMultSlice); +} + +BVSolverLazy::Statistics::~Statistics() +{ + smtStatisticsRegistry()->unregisterStat(&d_avgConflictSize); + smtStatisticsRegistry()->unregisterStat(&d_solveSubstitutions); + smtStatisticsRegistry()->unregisterStat(&d_solveTimer); + smtStatisticsRegistry()->unregisterStat(&d_numCallsToCheckFullEffort); + smtStatisticsRegistry()->unregisterStat(&d_numCallsToCheckStandardEffort); + smtStatisticsRegistry()->unregisterStat(&d_weightComputationTimer); + smtStatisticsRegistry()->unregisterStat(&d_numMultSlice); +} + +void BVSolverLazy::preRegisterTerm(TNode node) +{ + d_calledPreregister = true; + Debug("bitvector-preregister") + << "BVSolverLazy::preRegister(" << node << ")" << std::endl; + + if (options::bitblastMode() == options::BitblastMode::EAGER) + { + // the aig bit-blaster option is set heuristically + // if bv abstraction is used + if (!d_eagerSolver->isInitialized()) + { + d_eagerSolver->initialize(); + } + + if (node.getKind() == kind::BITVECTOR_EAGER_ATOM) + { + Node formula = node[0]; + d_eagerSolver->assertFormula(formula); + } + return; + } + + for (unsigned i = 0; i < d_subtheories.size(); ++i) + { + d_subtheories[i]->preRegister(node); + } + + // AJR : equality solver currently registers all terms to ExtTheory, if we + // want a lazy reduction without the bv equality solver, need to call this + // d_bv.d_extTheory->registerTermRec( node ); +} + +void BVSolverLazy::sendConflict() +{ + Assert(d_conflict); + if (d_conflictNode.isNull()) + { + return; + } + else + { + Debug("bitvector") << indent() << "BVSolverLazy::check(): conflict " + << d_conflictNode << std::endl; + d_inferManager.conflict(d_conflictNode); + d_statistics.d_avgConflictSize.addEntry(d_conflictNode.getNumChildren()); + d_conflictNode = Node::null(); + } +} + +void BVSolverLazy::checkForLemma(TNode fact) +{ + if (fact.getKind() == kind::EQUAL) + { + NodeManager* nm = NodeManager::currentNM(); + if (fact[0].getKind() == kind::BITVECTOR_UREM_TOTAL) + { + TNode urem = fact[0]; + TNode result = fact[1]; + TNode divisor = urem[1]; + Node result_ult_div = nm->mkNode(kind::BITVECTOR_ULT, result, divisor); + Node divisor_eq_0 = + nm->mkNode(kind::EQUAL, divisor, mkZero(getSize(divisor))); + Node split = nm->mkNode( + kind::OR, divisor_eq_0, nm->mkNode(kind::NOT, fact), result_ult_div); + lemma(split); + } + if (fact[1].getKind() == kind::BITVECTOR_UREM_TOTAL) + { + TNode urem = fact[1]; + TNode result = fact[0]; + TNode divisor = urem[1]; + Node result_ult_div = nm->mkNode(kind::BITVECTOR_ULT, result, divisor); + Node divisor_eq_0 = + nm->mkNode(kind::EQUAL, divisor, mkZero(getSize(divisor))); + Node split = nm->mkNode( + kind::OR, divisor_eq_0, nm->mkNode(kind::NOT, fact), result_ult_div); + lemma(split); + } + } +} + +bool BVSolverLazy::preCheck(Theory::Effort e) +{ + check(e); + return true; +} + +void BVSolverLazy::check(Theory::Effort e) +{ + if (done() && e < Theory::EFFORT_FULL) + { + 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 + d_invalidateModelCache.set(true); + // if we are using the eager solver + if (options::bitblastMode() == options::BitblastMode::EAGER) + { + // this can only happen on an empty benchmark + if (!d_eagerSolver->isInitialized()) + { + d_eagerSolver->initialize(); + } + if (!Theory::fullEffort(e)) return; + + std::vector assertions; + while (!done()) + { + TNode fact = get().d_assertion; + Assert(fact.getKind() == kind::BITVECTOR_EAGER_ATOM); + assertions.push_back(fact); + d_eagerSolver->assertFormula(fact[0]); + } + + bool ok = d_eagerSolver->checkSat(); + if (!ok) + { + if (assertions.size() == 1) + { + d_inferManager.conflict(assertions[0]); + return; + } + Node conflict = utils::mkAnd(assertions); + d_inferManager.conflict(conflict); + return; + } + return; + } + + if (Theory::fullEffort(e)) + { + ++(d_statistics.d_numCallsToCheckFullEffort); + } + else + { + ++(d_statistics.d_numCallsToCheckStandardEffort); + } + // if we are already in conflict just return the conflict + if (inConflict()) + { + sendConflict(); + return; + } + + while (!done()) + { + TNode fact = get().d_assertion; + + checkForLemma(fact); + + for (unsigned i = 0; i < d_subtheories.size(); ++i) + { + d_subtheories[i]->assertFact(fact); + } + } + + bool ok = true; + bool complete = false; + for (unsigned i = 0; i < d_subtheories.size(); ++i) + { + Assert(!inConflict()); + ok = d_subtheories[i]->check(e); + complete = d_subtheories[i]->isComplete(); + + if (!ok) + { + // if we are in a conflict no need to check with other theories + Assert(inConflict()); + sendConflict(); + return; + } + if (complete) + { + // if the last subtheory was complete we stop + 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::collectModelInfo(TheoryModel* m) +{ + Assert(!inConflict()); + if (options::bitblastMode() == options::BitblastMode::EAGER) + { + if (!d_eagerSolver->collectModelInfo(m, true)) + { + return false; + } + } + for (unsigned i = 0; i < d_subtheories.size(); ++i) + { + if (d_subtheories[i]->isComplete()) + { + return d_subtheories[i]->collectModelInfo(m, true); + } + } + return true; +} + +Node BVSolverLazy::getModelValue(TNode var) +{ + Assert(!inConflict()); + for (unsigned i = 0; i < d_subtheories.size(); ++i) + { + if (d_subtheories[i]->isComplete()) + { + return d_subtheories[i]->getModelValue(var); + } + } + Unreachable(); +} + +void BVSolverLazy::propagate(Theory::Effort e) +{ + Debug("bitvector") << indent() << "BVSolverLazy::propagate()" << std::endl; + if (options::bitblastMode() == options::BitblastMode::EAGER) + { + return; + } + + if (inConflict()) + { + return; + } + + // go through stored propagations + bool ok = true; + for (; d_literalsToPropagateIndex < d_literalsToPropagate.size() && ok; + d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) + { + TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex]; + // temporary fix for incremental bit-blasting + if (d_state.isSatLiteral(literal)) + { + Debug("bitvector::propagate") + << "BVSolverLazy:: propagating " << literal << "\n"; + ok = d_inferManager.propagateLit(literal); + } + } + + if (!ok) + { + Debug("bitvector::propagate") + << indent() << "BVSolverLazy::propagate(): conflict from theory engine" + << std::endl; + setConflict(); + } +} + +Theory::PPAssertStatus BVSolverLazy::ppAssert(TNode in, + SubstitutionMap& outSubstitutions) +{ + switch (in.getKind()) + { + case kind::EQUAL: + { + if (in[0].isVar() && d_bv.isLegalElimination(in[0], in[1])) + { + ++(d_statistics.d_solveSubstitutions); + outSubstitutions.addSubstitution(in[0], in[1]); + return Theory::PP_ASSERT_STATUS_SOLVED; + } + if (in[1].isVar() && d_bv.isLegalElimination(in[1], in[0])) + { + ++(d_statistics.d_solveSubstitutions); + outSubstitutions.addSubstitution(in[1], in[0]); + 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.addSubstitution(extract[0], concat); + 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"; + Node res = t; + if (options::bitwiseEq() && RewriteRule::applies(t)) + { + Node result = RewriteRule::run(t); + res = Rewriter::rewrite(result); + } + else if (RewriteRule::applies(t)) + { + Node result = RewriteRule::run(t); + res = Rewriter::rewrite(result); + } + else if (res.getKind() == kind::EQUAL + && ((res[0].getKind() == kind::BITVECTOR_PLUS + && RewriteRule::applies(res[1])) + || (res[1].getKind() == kind::BITVECTOR_PLUS + && RewriteRule::applies(res[0])))) + { + Node mult = RewriteRule::applies(res[0]) + ? RewriteRule::run(res[0]) + : RewriteRule::run(res[1]); + Node factor = mult[0]; + Node sum = RewriteRule::applies(res[0]) ? res[1] : res[0]; + Node new_eq = NodeManager::currentNM()->mkNode(kind::EQUAL, sum, mult); + Node rewr_eq = RewriteRule::run(new_eq); + if (rewr_eq[0].isVar() || rewr_eq[1].isVar()) + { + res = Rewriter::rewrite(rewr_eq); + } + else + { + res = t; + } + } + else if (RewriteRule::applies(t)) + { + res = RewriteRule::run(t); + } + else if (RewriteRule::applies(t)) + { + res = RewriteRule::run(t); + } + else if (RewriteRule::applies(t)) + { + res = RewriteRule::run(t); + } + + // if(t.getKind() == kind::EQUAL && + // ((t[0].getKind() == kind::BITVECTOR_MULT && t[1].getKind() == + // kind::BITVECTOR_PLUS) || + // (t[1].getKind() == kind::BITVECTOR_MULT && t[0].getKind() == + // kind::BITVECTOR_PLUS))) { + // // if we have an equality between a multiplication and addition + // // try to express multiplication in terms of addition + // Node mult = t[0].getKind() == kind::BITVECTOR_MULT? t[0] : t[1]; + // Node add = t[0].getKind() == kind::BITVECTOR_PLUS? t[0] : t[1]; + // if (RewriteRule::applies(mult)) { + // Node new_mult = RewriteRule::run(mult); + // Node new_eq = + // Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL, + // new_mult, add)); + + // // the simplification can cause the formula to blow up + // // only apply if formula reduced + // if (d_subtheoryMap.find(SUB_BITBLAST) != d_subtheoryMap.end()) { + // BitblastSolver* bv = (BitblastSolver*)d_subtheoryMap[SUB_BITBLAST]; + // uint64_t old_size = bv->computeAtomWeight(t); + // Assert (old_size); + // uint64_t new_size = bv->computeAtomWeight(new_eq); + // double ratio = ((double)new_size)/old_size; + // if (ratio <= 0.4) { + // ++(d_statistics.d_numMultSlice); + // return new_eq; + // } + // } + + // if (new_eq.getKind() == kind::CONST_BOOLEAN) { + // ++(d_statistics.d_numMultSlice); + // return new_eq; + // } + // } + // } + + if (options::bvAbstraction() && t.getType().isBoolean()) + { + d_abstractionModule->addInputAtom(res); + } + Debug("bv-pp-rewrite") << "to " << res << "\n"; + if (res != t) + { + return TrustNode::mkTrustRewrite(t, res, nullptr); + } + return TrustNode::null(); +} + +void BVSolverLazy::presolve() +{ + Debug("bitvector") << "BVSolverLazy::presolve" << std::endl; +} + +static int prop_count = 0; + +bool BVSolverLazy::storePropagation(TNode literal, SubTheory subtheory) +{ + Debug("bitvector::propagate") << indent() << d_context->getLevel() << " " + << "BVSolverLazy::storePropagation(" << literal + << ", " << subtheory << ")" << std::endl; + prop_count++; + + // If already in conflict, no more propagation + if (d_conflict) + { + Debug("bitvector::propagate") + << indent() << "BVSolverLazy::storePropagation(" << literal << ", " + << subtheory << "): already in conflict" << std::endl; + return false; + } + + // If propagated already, just skip + PropagatedMap::const_iterator find = d_propagatedBy.find(literal); + if (find != d_propagatedBy.end()) + { + return true; + } + else + { + bool polarity = literal.getKind() != kind::NOT; + Node negatedLiteral = polarity ? literal.notNode() : (Node)literal[0]; + find = d_propagatedBy.find(negatedLiteral); + if (find != d_propagatedBy.end() && (*find).second != subtheory) + { + // Safe to ignore this one, subtheory should produce a conflict + return true; + } + + d_propagatedBy[literal] = subtheory; + } + + // Propagate differs depending on the subtheory + // * bitblaster needs to be left alone until it's done, otherwise it doesn't + // know how to explain + // * equality engine can propagate eagerly + // TODO(2348): Determine if ok should be set by propagate. If not, remove ok. + constexpr bool ok = true; + if (subtheory == SUB_CORE) + { + d_inferManager.propagateLit(literal); + if (!ok) + { + setConflict(); + } + } + else + { + d_literalsToPropagate.push_back(literal); + } + return ok; + +} /* BVSolverLazy::propagate(TNode) */ + +void BVSolverLazy::explain(TNode literal, std::vector& assumptions) +{ + Assert(wasPropagatedBySubtheory(literal)); + SubTheory sub = getPropagatingSubtheory(literal); + d_subtheoryMap[sub]->explain(literal, assumptions); +} + +TrustNode BVSolverLazy::explain(TNode node) +{ + Debug("bitvector::explain") + << "BVSolverLazy::explain(" << node << ")" << std::endl; + std::vector assumptions; + + // Ask for the explanation + explain(node, assumptions); + // this means that it is something true at level 0 + Node explanation; + if (assumptions.size() == 0) + { + explanation = utils::mkTrue(); + } + else + { + // return the explanation + explanation = utils::mkAnd(assumptions); + } + Debug("bitvector::explain") << "BVSolverLazy::explain(" << node << ") => " + << explanation << std::endl; + Debug("bitvector::explain") << "BVSolverLazy::explain done. \n"; + return TrustNode::mkTrustPropExp(node, explanation, nullptr); +} + +void BVSolverLazy::notifySharedTerm(TNode t) +{ + Debug("bitvector::sharing") + << indent() << "BVSolverLazy::notifySharedTerm(" << t << ")" << std::endl; + d_sharedTermsSet.insert(t); + if (options::bitvectorEqualitySolver()) + { + for (unsigned i = 0; i < d_subtheories.size(); ++i) + { + d_subtheories[i]->addSharedTerm(t); + } + } +} + +EqualityStatus BVSolverLazy::getEqualityStatus(TNode a, TNode b) +{ + if (options::bitblastMode() == options::BitblastMode::EAGER) + return EQUALITY_UNKNOWN; + Assert(options::bitblastMode() == options::BitblastMode::LAZY); + for (unsigned i = 0; i < d_subtheories.size(); ++i) + { + EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b); + if (status != EQUALITY_UNKNOWN) + { + return status; + } + } + return EQUALITY_UNKNOWN; + ; +} + +void BVSolverLazy::ppStaticLearn(TNode in, NodeBuilder<>& learned) +{ + if (d_staticLearnCache.find(in) != d_staticLearnCache.end()) + { + return; + } + d_staticLearnCache.insert(in); + + if (in.getKind() == kind::EQUAL) + { + if ((in[0].getKind() == kind::BITVECTOR_PLUS + && in[1].getKind() == kind::BITVECTOR_SHL) + || (in[1].getKind() == kind::BITVECTOR_PLUS + && in[0].getKind() == kind::BITVECTOR_SHL)) + { + TNode p = in[0].getKind() == kind::BITVECTOR_PLUS ? in[0] : in[1]; + TNode s = in[0].getKind() == kind::BITVECTOR_PLUS ? in[1] : in[0]; + + if (p.getNumChildren() == 2 && p[0].getKind() == kind::BITVECTOR_SHL + && p[1].getKind() == kind::BITVECTOR_SHL) + { + unsigned size = utils::getSize(s); + Node one = utils::mkConst(size, 1u); + if (s[0] == one && p[0][0] == one && p[1][0] == one) + { + Node zero = utils::mkConst(size, 0u); + TNode b = p[0]; + TNode c = p[1]; + // (s : 1 << S) = (b : 1 << B) + (c : 1 << C) + Node b_eq_0 = b.eqNode(zero); + Node c_eq_0 = c.eqNode(zero); + Node b_eq_c = b.eqNode(c); + + Node dis = NodeManager::currentNM()->mkNode( + kind::OR, b_eq_0, c_eq_0, b_eq_c); + Node imp = in.impNode(dis); + learned << imp; + } + } + } + } + else if (in.getKind() == kind::AND) + { + for (size_t i = 0, N = in.getNumChildren(); i < N; ++i) + { + ppStaticLearn(in[i], learned); + } + } +} + +bool BVSolverLazy::applyAbstraction(const std::vector& assertions, + std::vector& new_assertions) +{ + bool changed = + d_abstractionModule->applyAbstraction(assertions, new_assertions); + if (changed && options::bitblastMode() == options::BitblastMode::EAGER + && options::bitvectorAig()) + { + // disable AIG mode + AlwaysAssert(!d_eagerSolver->isInitialized()); + d_eagerSolver->turnOffAig(); + d_eagerSolver->initialize(); + } + return changed; +} + +void BVSolverLazy::setConflict(Node conflict) +{ + if (options::bvAbstraction()) + { + NodeManager* const nm = NodeManager::currentNM(); + Node new_conflict = d_abstractionModule->simplifyConflict(conflict); + + std::vector lemmas; + lemmas.push_back(new_conflict); + d_abstractionModule->generalizeConflict(new_conflict, lemmas); + for (unsigned i = 0; i < lemmas.size(); ++i) + { + lemma(nm->mkNode(kind::NOT, lemmas[i])); + } + } + d_conflict = true; + d_conflictNode = conflict; +} + +} // namespace bv +} // namespace theory +} /* namespace CVC4 */ diff --git a/src/theory/bv/bv_solver_lazy.h b/src/theory/bv/bv_solver_lazy.h new file mode 100644 index 000000000..81f40340e --- /dev/null +++ b/src/theory/bv/bv_solver_lazy.h @@ -0,0 +1,240 @@ +/********************* */ +/*! \file bv_solver_lazy.h + ** \verbatim + ** Top contributors (to current version): + ** Liana Hadarean, Andrew Reynolds, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Lazy bit-vector solver. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__BV__BV_SOLVER_LAZY_H +#define CVC4__THEORY__BV__BV_SOLVER_LAZY_H + +#include +#include + +#include "context/cdhashset.h" +#include "context/cdlist.h" +#include "context/context.h" +#include "theory/bv/bv_solver.h" +#include "theory/bv/bv_subtheory.h" +#include "theory/bv/theory_bv.h" +#include "util/hash.h" + +namespace CVC4 { +namespace theory { +namespace bv { + +class CoreSolver; +class InequalitySolver; +class AlgebraicSolver; +class BitblastSolver; +class EagerBitblastSolver; +class AbstractionModule; + +class BVSolverLazy : public BVSolver +{ + /** Back reference to TheoryBV */ + TheoryBV& d_bv; + + /** The context we are using */ + context::Context* d_context; + + /** Context dependent set of atoms we already propagated */ + context::CDHashSet d_alreadyPropagatedSet; + context::CDHashSet d_sharedTermsSet; + + std::vector> d_subtheories; + std::unordered_map> + d_subtheoryMap; + + public: + BVSolverLazy(TheoryBV& bv, + context::Context* c, + context::UserContext* u, + ProofNodeManager* pnm = nullptr, + std::string name = ""); + + ~BVSolverLazy(); + + //--------------------------------- initialization + + /** + * Returns true if we need an equality engine. If so, we initialize the + * information regarding how it should be setup. For details, see the + * documentation in Theory::needsEqualityEngine. + */ + bool needsEqualityEngine(EeSetupInfo& esi) override; + + /** finish initialization */ + void finishInit() override; + //--------------------------------- end initialization + + void preRegisterTerm(TNode n) override; + + bool preCheck(Theory::Effort e) override; + + bool needsCheckLastEffort() override; + + void propagate(Theory::Effort e) override; + + TrustNode explain(TNode n) override; + + bool collectModelInfo(TheoryModel* m) override; + + std::string identify() const override { return std::string("BVSolverLazy"); } + + Theory::PPAssertStatus ppAssert(TNode in, + SubstitutionMap& outSubstitutions) override; + + TrustNode ppRewrite(TNode t) override; + + void ppStaticLearn(TNode in, NodeBuilder<>& learned) override; + + void presolve() override; + + bool applyAbstraction(const std::vector& assertions, + std::vector& new_assertions) override; + + bool isLeaf(TNode node) { return d_bv.isLeaf(node); } + + private: + class Statistics + { + public: + AverageStat d_avgConflictSize; + IntStat d_solveSubstitutions; + TimerStat d_solveTimer; + IntStat d_numCallsToCheckFullEffort; + IntStat d_numCallsToCheckStandardEffort; + TimerStat d_weightComputationTimer; + IntStat d_numMultSlice; + Statistics(); + ~Statistics(); + }; + + Statistics d_statistics; + + void check(Theory::Effort e); + void spendResource(ResourceManager::Resource r); + + typedef std::unordered_set TNodeSet; + typedef std::unordered_set NodeSet; + NodeSet d_staticLearnCache; + + typedef std::unordered_map NodeToNode; + + context::CDO d_lemmasAdded; + + // Are we in conflict? + context::CDO d_conflict; + + // Invalidate the model cache if check was called + context::CDO d_invalidateModelCache; + + /** The conflict node */ + Node d_conflictNode; + + /** Literals to propagate */ + context::CDList d_literalsToPropagate; + + /** Index of the next literal to propagate */ + context::CDO d_literalsToPropagateIndex; + + /** + * Keeps a map from nodes to the subtheory that propagated it so that we can + * explain it properly. + */ + typedef context::CDHashMap PropagatedMap; + PropagatedMap d_propagatedBy; + + std::unique_ptr d_eagerSolver; + std::unique_ptr d_abstractionModule; + bool d_calledPreregister; + + bool wasPropagatedBySubtheory(TNode literal) const + { + return d_propagatedBy.find(literal) != d_propagatedBy.end(); + } + + SubTheory getPropagatingSubtheory(TNode literal) const + { + Assert(wasPropagatedBySubtheory(literal)); + PropagatedMap::const_iterator find = d_propagatedBy.find(literal); + return (*find).second; + } + + /** Should be called to propagate the literal. */ + bool storePropagation(TNode literal, SubTheory subtheory); + + /** + * Explains why this literal (propagated by subtheory) is true by adding + * assumptions. + */ + void explain(TNode literal, std::vector& assumptions); + + void notifySharedTerm(TNode t) override; + + bool isSharedTerm(TNode t) { return d_sharedTermsSet.contains(t); } + + EqualityStatus getEqualityStatus(TNode a, TNode b) override; + + Node getModelValue(TNode var); + + inline std::string indent() + { + std::string indentStr(d_context->getLevel(), ' '); + return indentStr; + } + + void setConflict(Node conflict = Node::null()); + + bool inConflict() { return d_conflict; } + + void sendConflict(); + + void lemma(TNode node) + { + d_inferManager.lemma(node); + d_lemmasAdded = true; + } + + void checkForLemma(TNode node); + + void computeAssertedTerms(std::set& termSet, + const std::set& irrKinds, + bool includeShared) const + { + return d_bv.computeAssertedTerms(termSet, irrKinds, includeShared); + } + + size_t numAssertions() { return d_bv.numAssertions(); } + + theory::Assertion get() { return d_bv.get(); } + + bool done() { return d_bv.done(); } + + friend class LazyBitblaster; + friend class TLazyBitblaster; + friend class EagerBitblaster; + friend class BitblastSolver; + friend class EqualitySolver; + friend class CoreSolver; + friend class InequalitySolver; + friend class AlgebraicSolver; + friend class EagerBitblastSolver; +}; /* class BVSolverLazy */ + +} // namespace bv +} // namespace theory + +} // namespace CVC4 + +#endif /* CVC4__THEORY__BV__BV_SOLVER_LAZY_H */ diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h index f4b88b719..1244ae828 100644 --- a/src/theory/bv/bv_subtheory.h +++ b/src/theory/bv/bv_subtheory.h @@ -55,7 +55,7 @@ inline std::ostream& operator<<(std::ostream& out, SubTheory subtheory) { } // forward declaration -class TheoryBV; +class BVSolverLazy; using AssertionQueue = context::CDQueue; @@ -65,11 +65,10 @@ using AssertionQueue = context::CDQueue; */ class SubtheorySolver { public: - SubtheorySolver(context::Context* c, TheoryBV* bv) - : d_context(c), - d_bv(bv), - d_assertionQueue(c), - d_assertionIndex(c, 0) {} + SubtheorySolver(context::Context* c, BVSolverLazy* bv) + : d_context(c), d_bv(bv), d_assertionQueue(c), d_assertionIndex(c, 0) + { + } virtual ~SubtheorySolver() {} virtual bool check(Theory::Effort e) = 0; virtual void explain(TNode literal, std::vector& assumptions) = 0; @@ -101,7 +100,7 @@ class SubtheorySolver { context::Context* d_context; /** The bit-vector theory */ - TheoryBV* d_bv; + BVSolverLazy* d_bv; AssertionQueue d_assertionQueue; context::CDO d_assertionIndex; }; /* class SubtheorySolver */ diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp index 80a6aeb86..49043b445 100644 --- a/src/theory/bv/bv_subtheory_algebraic.cpp +++ b/src/theory/bv/bv_subtheory_algebraic.cpp @@ -22,7 +22,7 @@ #include "smt/smt_statistics_registry.h" #include "smt_util/boolean_simplification.h" #include "theory/bv/bv_quick_check.h" -#include "theory/bv/theory_bv.h" +#include "theory/bv/bv_solver_lazy.h" #include "theory/bv/theory_bv_utils.h" #include "theory/theory_model.h" @@ -227,7 +227,7 @@ void SubstitutionEx::storeCache(TNode from, TNode to, Node reason) { d_cache[from] = SubstitutionElement(to, reason); } -AlgebraicSolver::AlgebraicSolver(context::Context* c, TheoryBV* bv) +AlgebraicSolver::AlgebraicSolver(context::Context* c, BVSolverLazy* bv) : SubtheorySolver(c, bv), d_modelMap(), d_quickSolver(new BVQuickCheck("theory::bv::algebraic", bv)), @@ -345,7 +345,8 @@ bool AlgebraicSolver::check(Theory::Effort e) Debug("bv-subtheory-algebraic") << " UNSAT: assertion simplfies to false with conflict: "<< conflict << "\n"; if (Dump.isOn("bv-algebraic")) { - Dump("bv-algebraic") << EchoCommand("TheoryBV::AlgebraicSolver::conflict"); + Dump("bv-algebraic") + << EchoCommand("BVSolverLazy::AlgebraicSolver::conflict"); Dump("bv-algebraic") << PushCommand(); Dump("bv-algebraic") << AssertCommand(conflict.toExpr()); Dump("bv-algebraic") << CheckSatCommand(); diff --git a/src/theory/bv/bv_subtheory_algebraic.h b/src/theory/bv/bv_subtheory_algebraic.h index d9a9bce6f..a5d7b2db3 100644 --- a/src/theory/bv/bv_subtheory_algebraic.h +++ b/src/theory/bv/bv_subtheory_algebraic.h @@ -31,64 +31,60 @@ namespace bv { class AlgebraicSolver; - Node mergeExplanations(TNode expl1, TNode expl2); Node mergeExplanations(const std::vector& expls); - /** * Non-context dependent substitution with explanations. - * + * */ -class SubstitutionEx { - struct SubstitutionElement { +class SubstitutionEx +{ + struct SubstitutionElement + { Node to; Node reason; - SubstitutionElement() - : to() - , reason() - {} - - SubstitutionElement(TNode t, TNode r) - : to(t) - , reason(r) - {} + SubstitutionElement() : to(), reason() {} + + SubstitutionElement(TNode t, TNode r) : to(t), reason(r) {} }; - struct SubstitutionStackElement { + struct SubstitutionStackElement + { TNode node; bool childrenAdded; SubstitutionStackElement(TNode n, bool ca = false) - : node(n) - , childrenAdded(ca) - {} + : node(n), childrenAdded(ca) + { + } }; - typedef std::unordered_map Substitutions; - typedef std::unordered_map SubstitutionsCache; + typedef std::unordered_map + Substitutions; + typedef std::unordered_map + SubstitutionsCache; Substitutions d_substitutions; SubstitutionsCache d_cache; bool d_cacheInvalid; - theory::SubstitutionMap* d_modelMap; + theory::SubstitutionMap* d_modelMap; - Node getReason(TNode node) const; bool hasCache(TNode node) const; Node getCache(TNode node) const; void storeCache(TNode from, TNode to, Node rason); Node internalApply(TNode node); -public: + public: SubstitutionEx(theory::SubstitutionMap* modelMap); - /** - * Returnst true if the substitution map did not contain from. - * - * @param from - * @param to - * @param reason - * - * @return + /** + * Returnst true if the substitution map did not contain from. + * + * @param from + * @param to + * @param reason + * + * @return */ bool addSubstitution(TNode from, TNode to, TNode reason); Node apply(TNode node); @@ -97,37 +93,39 @@ public: /** * In-processing worklist element, id keeps track of - * original assertion. - * + * original assertion. + * */ -struct WorklistElement { +struct WorklistElement +{ Node node; unsigned id; WorklistElement(Node n, unsigned i) : node(n), id(i) {} WorklistElement() : node(), id(-1) {} -}; - +}; typedef std::unordered_map NodeNodeMap; typedef std::unordered_map NodeIdMap; typedef std::unordered_set TNodeSet; - -class ExtractSkolemizer { - struct Extract { +class ExtractSkolemizer +{ + struct Extract + { unsigned high; unsigned low; Extract(unsigned h, unsigned l) : high(h), low(l) {} }; - - struct ExtractList { + + struct ExtractList + { Base base; std::vector extracts; ExtractList(unsigned bitwidth) : base(bitwidth), extracts() {} ExtractList() : base(1), extracts() {} - void addExtract(Extract& e); + void addExtract(Extract& e); }; - typedef std::unordered_map VarExtractMap; + typedef std::unordered_map VarExtractMap; context::Context d_emptyContext; VarExtractMap d_varToExtract; theory::SubstitutionMap* d_modelMap; @@ -141,12 +139,13 @@ class ExtractSkolemizer { Node unSkolemize(TNode); Node mkSkolem(Node node); -public: - ExtractSkolemizer(theory::SubstitutionMap* modelMap); + + public: + ExtractSkolemizer(theory::SubstitutionMap* modelMap); void skolemize(std::vector&); void unSkolemize(std::vector&); ~ExtractSkolemizer(); -}; +}; class BVQuickCheck; class QuickXPlain; @@ -154,9 +153,10 @@ class QuickXPlain; /** * AlgebraicSolver */ -class AlgebraicSolver : public SubtheorySolver { - - struct Statistics { +class AlgebraicSolver : public SubtheorySolver +{ + struct Statistics + { IntStat d_numCallstoCheck; IntStat d_numSimplifiesToTrue; IntStat d_numSimplifiesToFalse; @@ -171,13 +171,17 @@ class AlgebraicSolver : public SubtheorySolver { std::unique_ptr d_modelMap; std::unique_ptr d_quickSolver; - context::CDO d_isComplete; - context::CDO d_isDifficult; /**< flag to indicate whether the current assertions contain expensive BV operators */ - + context::CDO d_isComplete; + context::CDO + d_isDifficult; /**< flag to indicate whether the current assertions + contain expensive BV operators */ + unsigned long d_budget; - std::vector d_explanations; /**< explanations for assertions indexed by assertion id */ - TNodeSet d_inputAssertions; /**< assertions in current context (for debugging purposes only) */ - NodeIdMap d_ids; /**< map from assertions to ids */ + std::vector d_explanations; /**< explanations for assertions indexed by + assertion id */ + TNodeSet d_inputAssertions; /**< assertions in current context (for debugging + purposes only) */ + NodeIdMap d_ids; /**< map from assertions to ids */ uint64_t d_numSolved; uint64_t d_numCalls; @@ -191,37 +195,38 @@ class AlgebraicSolver : public SubtheorySolver { bool checkExplanation(TNode expl); void storeExplanation(TNode expl); void storeExplanation(unsigned id, TNode expl); - /** + /** * Apply substitutions and rewriting to the worklist assertions to a fixpoint. - * Subsitutions learned store in subst. + * Subsitutions learned store in subst. * - * @param worklist - * @param subst + * @param worklist + * @param subst */ - void processAssertions(std::vector& worklist, SubstitutionEx& subst); - /** + void processAssertions(std::vector& worklist, + SubstitutionEx& subst); + /** * Attempt to solve the equation in fact, and if successful - * add a substitution to subst. - * + * add a substitution to subst. + * * @param fact equation we are trying to solve * @param reason the reason in terms of original assertions * @param subst substitution map - * + * * @return true if added a substitution to subst */ bool solve(TNode fact, TNode reason, SubstitutionEx& subst); - /** + /** * Run a SAT solver on the given facts with the given budget. - * Sets the isComplete flag and conflict accordingly. - * - * @param facts - * - * @return true if no conflict was detected. + * Sets the isComplete flag and conflict accordingly. + * + * @param facts + * + * @return true if no conflict was detected. */ bool quickCheck(std::vector& facts); -public: - AlgebraicSolver(context::Context* c, TheoryBV* bv); + public: + AlgebraicSolver(context::Context* c, BVSolverLazy* bv); ~AlgebraicSolver(); void preRegister(TNode node) override {} diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index 28c70a5b8..93ac87abe 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -15,6 +15,7 @@ **/ #include "theory/bv/bv_subtheory_bitblast.h" + #include "decision/decision_attributes.h" #include "options/bv_options.h" #include "options/decision_options.h" @@ -22,7 +23,7 @@ #include "theory/bv/abstraction.h" #include "theory/bv/bitblast/lazy_bitblaster.h" #include "theory/bv/bv_quick_check.h" -#include "theory/bv/theory_bv.h" +#include "theory/bv/bv_solver_lazy.h" #include "theory/bv/theory_bv_utils.h" using namespace std; @@ -32,7 +33,7 @@ namespace CVC4 { namespace theory { namespace bv { -BitblastSolver::BitblastSolver(context::Context* c, TheoryBV* bv) +BitblastSolver::BitblastSolver(context::Context* c, BVSolverLazy* bv) : SubtheorySolver(c, bv), d_bitblaster(new TLazyBitblaster(c, bv, "theory::bv::lazy")), d_bitblastQueue(c), diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h index 60ef08d93..0832b6772 100644 --- a/src/theory/bv/bv_subtheory_bitblast.h +++ b/src/theory/bv/bv_subtheory_bitblast.h @@ -35,8 +35,10 @@ class QuickXPlain; /** * BitblastSolver */ -class BitblastSolver : public SubtheorySolver { - struct Statistics { +class BitblastSolver : public SubtheorySolver +{ + struct Statistics + { IntStat d_numCallstoCheck; IntStat d_numBBLemmas; Statistics(); @@ -55,14 +57,15 @@ class BitblastSolver : public SubtheorySolver { /** Queue for bit-blasting lemma atoms only in full check if we are sat */ context::CDQueue d_lemmaAtomsQueue; - bool d_useSatPropagation; + bool d_useSatPropagation; AbstractionModule* d_abstractionModule; std::unique_ptr d_quickCheck; std::unique_ptr d_quickXplain; // Node getModelValueRec(TNode node); void setConflict(TNode conflict); -public: - BitblastSolver(context::Context* c, TheoryBV* bv); + + public: + BitblastSolver(context::Context* c, BVSolverLazy* bv); ~BitblastSolver(); void preRegister(TNode node) override; @@ -77,6 +80,6 @@ public: uint64_t computeAtomWeight(TNode atom); }; -} /* namespace CVC4::theory::bv */ -} /* namespace CVC4::theory */ +} // namespace bv +} // namespace theory } /* namespace CVC4 */ diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index b341b0671..5bb6a45e4 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -19,7 +19,7 @@ #include "options/bv_options.h" #include "options/smt_options.h" #include "smt/smt_statistics_registry.h" -#include "theory/bv/theory_bv.h" +#include "theory/bv/bv_solver_lazy.h" #include "theory/bv/theory_bv_utils.h" #include "theory/ext_theory.h" #include "theory/theory_model.h" @@ -89,7 +89,7 @@ bool CoreSolverExtTheoryCallback::getReduction(int effort, return false; } -CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv) +CoreSolver::CoreSolver(context::Context* c, BVSolverLazy* bv) : SubtheorySolver(c, bv), d_notify(*this), d_isComplete(c, true), @@ -99,13 +99,13 @@ CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv) d_bv(bv), d_extTheoryCb(), d_extTheory(new ExtTheory(d_extTheoryCb, - bv->getSatContext(), - bv->getUserContext(), - bv->getOutputChannel())), + bv->d_bv.getSatContext(), + bv->d_bv.getUserContext(), + bv->d_bv.getOutputChannel())), d_reasons(c), d_needsLastCallCheck(false), - d_extf_range_infer(bv->getUserContext()), - d_extf_collapse_infer(bv->getUserContext()) + d_extf_range_infer(bv->d_bv.getUserContext()), + d_extf_collapse_infer(bv->d_bv.getUserContext()) { d_extTheory->addFunctionKind(kind::BITVECTOR_TO_NAT); d_extTheory->addFunctionKind(kind::INT_TO_BITVECTOR); @@ -123,7 +123,7 @@ bool CoreSolver::needsEqualityEngine(EeSetupInfo& esi) void CoreSolver::finishInit() { // use the parent's equality engine, which may be the one we allocated above - d_equalityEngine = d_bv->getEqualityEngine(); + d_equalityEngine = d_bv->d_bv.getEqualityEngine(); // The kinds we are treating as function application in congruence d_equalityEngine->addFunctionKind(kind::BITVECTOR_CONCAT, true); @@ -188,7 +188,8 @@ void CoreSolver::explain(TNode literal, std::vector& assumptions) { bool CoreSolver::check(Theory::Effort e) { Trace("bitvector::core") << "CoreSolver::check \n"; - d_bv->spendResource(ResourceManager::Resource::TheoryCheckStep); + d_bv->d_inferManager.spendResource( + ResourceManager::Resource::TheoryCheckStep); d_checkCalled = true; Assert(!d_bv->inConflict()); @@ -566,7 +567,7 @@ bool CoreSolver::doExtfInferences(std::vector& terms) nm->mkNode(kind::LT, n, max)); Trace("bv-extf-lemma") << "BV extf lemma (range) : " << lem << std::endl; - d_bv->getOutputChannel().lemma(lem); + d_bv->d_inferManager.lemma(lem); sentLemma = true; } } @@ -615,7 +616,7 @@ bool CoreSolver::doExtfInferences(std::vector& terms) // (bv2nat ((_ int2bv w) x)) == x + k*2^w for some k Trace("bv-extf-lemma") << "BV extf lemma (collapse) : " << lem << std::endl; - d_bv->getOutputChannel().lemma(lem); + d_bv->d_inferManager.lemma(lem); sentLemma = true; } } diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h index 32bc36164..876daeabe 100644 --- a/src/theory/bv/bv_subtheory_core.h +++ b/src/theory/bv/bv_subtheory_core.h @@ -97,7 +97,7 @@ class CoreSolver : public SubtheorySolver { bool d_checkCalled; /** Pointer to the parent theory solver that owns this */ - TheoryBV* d_bv; + BVSolverLazy* d_bv; /** Pointer to the equality engine of the parent */ eq::EqualityEngine* d_equalityEngine; /** The extended theory callback */ @@ -146,7 +146,7 @@ class CoreSolver : public SubtheorySolver { bool doExtfReductions(std::vector& terms); public: - CoreSolver(context::Context* c, TheoryBV* bv); + CoreSolver(context::Context* c, BVSolverLazy* bv); ~CoreSolver(); bool needsEqualityEngine(EeSetupInfo& esi); void finishInit(); diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp index 1ff23c460..ffc354d8d 100644 --- a/src/theory/bv/bv_subtheory_inequality.cpp +++ b/src/theory/bv/bv_subtheory_inequality.cpp @@ -18,7 +18,7 @@ #include "options/smt_options.h" #include "smt/smt_statistics_registry.h" -#include "theory/bv/theory_bv.h" +#include "theory/bv/bv_solver_lazy.h" #include "theory/bv/theory_bv_utils.h" #include "theory/theory_model.h" diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h index abfb0d3cf..05c9c3d60 100644 --- a/src/theory/bv/bv_subtheory_inequality.h +++ b/src/theory/bv/bv_subtheory_inequality.h @@ -31,12 +31,17 @@ namespace theory { namespace bv { /** Cache for InequalitySolver::isInequalityOnly() */ -struct IneqOnlyAttributeId {}; +struct IneqOnlyAttributeId +{ +}; typedef expr::Attribute IneqOnlyAttribute; /** Whether the above has been computed yet or not for an expr */ -struct IneqOnlyComputedAttributeId {}; -typedef expr::Attribute IneqOnlyComputedAttribute; +struct IneqOnlyComputedAttributeId +{ +}; +typedef expr::Attribute + IneqOnlyComputedAttribute; class InequalitySolver : public SubtheorySolver { @@ -57,16 +62,18 @@ class InequalitySolver : public SubtheorySolver bool isInequalityOnly(TNode node); bool addInequality(TNode a, TNode b, bool strict, TNode fact); Statistics d_statistics; -public: - InequalitySolver(context::Context* c, context::Context* u, TheoryBV* bv) - : SubtheorySolver(c, bv), - d_assertionSet(c), - d_inequalityGraph(c, u), - d_explanations(c), - d_isComplete(c, true), - d_ineqTerms(), - d_statistics() - {} + + public: + InequalitySolver(context::Context* c, context::Context* u, BVSolverLazy* bv) + : SubtheorySolver(c, bv), + d_assertionSet(c), + d_inequalityGraph(c, u), + d_explanations(c), + d_isComplete(c, true), + d_ineqTerms(), + d_statistics() + { + } bool check(Theory::Effort e) override; void propagate(Theory::Effort e) override; @@ -79,8 +86,8 @@ public: void preRegister(TNode node) override; }; -} -} -} +} // namespace bv +} // namespace theory +} // namespace CVC4 #endif /* CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H */ diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 815656d8f..6f25d0843 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -15,26 +15,9 @@ #include "theory/bv/theory_bv.h" -#include "expr/node_algorithm.h" #include "options/bv_options.h" -#include "options/smt_options.h" -#include "smt/smt_statistics_registry.h" -#include "theory/bv/abstraction.h" -#include "theory/bv/bv_eager_solver.h" -#include "theory/bv/bv_subtheory_algebraic.h" -#include "theory/bv/bv_subtheory_bitblast.h" -#include "theory/bv/bv_subtheory_core.h" -#include "theory/bv/bv_subtheory_inequality.h" -#include "theory/bv/theory_bv_rewrite_rules_normalization.h" -#include "theory/bv/theory_bv_rewrite_rules_simplification.h" -#include "theory/bv/theory_bv_rewriter.h" +#include "theory/bv/bv_solver_lazy.h" #include "theory/bv/theory_bv_utils.h" -#include "theory/theory_model.h" -#include "theory/valuation.h" - -using namespace CVC4::context; -using namespace CVC4::theory::bv::utils; -using namespace std; namespace CVC4 { namespace theory { @@ -48,60 +31,16 @@ TheoryBV::TheoryBV(context::Context* c, ProofNodeManager* pnm, std::string name) : Theory(THEORY_BV, c, u, out, valuation, logicInfo, pnm, name), - d_context(c), - d_alreadyPropagatedSet(c), - d_sharedTermsSet(c), - d_subtheories(), - d_subtheoryMap(), - d_statistics(), - d_staticLearnCache(), - d_BVDivByZero(), - d_BVRemByZero(), - d_lemmasAdded(c, false), - d_conflict(c, false), - d_invalidateModelCache(c, true), - d_literalsToPropagate(c), - d_literalsToPropagateIndex(c, 0), - d_propagatedBy(c), - d_eagerSolver(), - d_abstractionModule(new AbstractionModule(getStatsPrefix(THEORY_BV))), - d_calledPreregister(false), - d_state(c, u, valuation) -{ - if (options::bitblastMode() == options::BitblastMode::EAGER) - { - d_eagerSolver.reset(new EagerBitblastSolver(c, this)); - return; - } - - if (options::bitvectorEqualitySolver()) - { - d_subtheories.emplace_back(new CoreSolver(c, this)); - d_subtheoryMap[SUB_CORE] = d_subtheories.back().get(); - } - - if (options::bitvectorInequalitySolver()) - { - d_subtheories.emplace_back(new InequalitySolver(c, u, this)); - d_subtheoryMap[SUB_INEQUALITY] = d_subtheories.back().get(); - } - - if (options::bitvectorAlgebraicSolver()) - { - d_subtheories.emplace_back(new AlgebraicSolver(c, this)); - d_subtheoryMap[SUB_ALGEBRAIC] = d_subtheories.back().get(); - } - - BitblastSolver* bb_solver = new BitblastSolver(c, this); - if (options::bvAbstraction()) - { - bb_solver->setAbstraction(d_abstractionModule.get()); - } - d_subtheories.emplace_back(bb_solver); - d_subtheoryMap[SUB_BITBLAST] = bb_solver; - - // indicate we are using the default theory state object + d_internal(nullptr), + d_ufDivByZero(), + d_ufRemByZero(), + d_rewriter(), + d_state(c, u, valuation), + d_inferMgr(*this, d_state, pnm) +{ + d_internal.reset(new BVSolverLazy(*this, c, u, pnm, name)); d_theoryState = &d_state; + d_inferManager = &d_inferMgr; } TheoryBV::~TheoryBV() {} @@ -110,87 +49,53 @@ TheoryRewriter* TheoryBV::getTheoryRewriter() { return &d_rewriter; } bool TheoryBV::needsEqualityEngine(EeSetupInfo& esi) { - CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE]; - if (core) - { - return core->needsEqualityEngine(esi); - } - // otherwise we don't use an equality engine - return false; + return d_internal->needsEqualityEngine(esi); } void TheoryBV::finishInit() { // these kinds are semi-evaluated in getModelValue (applications of this // kind are treated as variables) - d_valuation.setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UDIV); - d_valuation.setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UREM); - - CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE]; - if (core) - { - // must finish initialization in the core solver - core->finishInit(); - } -} - -void TheoryBV::spendResource(ResourceManager::Resource r) -{ - getOutputChannel().spendResource(r); + getValuation().setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UDIV); + getValuation().setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UREM); + d_internal->finishInit(); } -TheoryBV::Statistics::Statistics(): - d_avgConflictSize("theory::bv::AvgBVConflictSize"), - d_solveSubstitutions("theory::bv::NumSolveSubstitutions", 0), - d_solveTimer("theory::bv::solveTimer"), - d_numCallsToCheckFullEffort("theory::bv::NumFullCheckCalls", 0), - d_numCallsToCheckStandardEffort("theory::bv::NumStandardCheckCalls", 0), - d_weightComputationTimer("theory::bv::weightComputationTimer"), - d_numMultSlice("theory::bv::NumMultSliceApplied", 0) +Node TheoryBV::getUFDivByZero(Kind k, unsigned width) { - smtStatisticsRegistry()->registerStat(&d_avgConflictSize); - smtStatisticsRegistry()->registerStat(&d_solveSubstitutions); - smtStatisticsRegistry()->registerStat(&d_solveTimer); - smtStatisticsRegistry()->registerStat(&d_numCallsToCheckFullEffort); - smtStatisticsRegistry()->registerStat(&d_numCallsToCheckStandardEffort); - smtStatisticsRegistry()->registerStat(&d_weightComputationTimer); - smtStatisticsRegistry()->registerStat(&d_numMultSlice); -} - -TheoryBV::Statistics::~Statistics() { - smtStatisticsRegistry()->unregisterStat(&d_avgConflictSize); - smtStatisticsRegistry()->unregisterStat(&d_solveSubstitutions); - smtStatisticsRegistry()->unregisterStat(&d_solveTimer); - smtStatisticsRegistry()->unregisterStat(&d_numCallsToCheckFullEffort); - smtStatisticsRegistry()->unregisterStat(&d_numCallsToCheckStandardEffort); - smtStatisticsRegistry()->unregisterStat(&d_weightComputationTimer); - smtStatisticsRegistry()->unregisterStat(&d_numMultSlice); -} - -Node TheoryBV::getBVDivByZero(Kind k, unsigned width) { NodeManager* nm = NodeManager::currentNM(); - if (k == kind::BITVECTOR_UDIV) { - if (d_BVDivByZero.find(width) == d_BVDivByZero.end()) { + if (k == kind::BITVECTOR_UDIV) + { + if (d_ufDivByZero.find(width) == d_ufDivByZero.end()) + { // lazily create the function symbols - ostringstream os; + std::ostringstream os; os << "BVUDivByZero_" << width; - Node divByZero = nm->mkSkolem(os.str(), - nm->mkFunctionType(nm->mkBitVectorType(width), nm->mkBitVectorType(width)), - "partial bvudiv", NodeManager::SKOLEM_EXACT_NAME); - d_BVDivByZero[width] = divByZero; + Node divByZero = + nm->mkSkolem(os.str(), + nm->mkFunctionType(nm->mkBitVectorType(width), + nm->mkBitVectorType(width)), + "partial bvudiv", + NodeManager::SKOLEM_EXACT_NAME); + d_ufDivByZero[width] = divByZero; } - return d_BVDivByZero[width]; + return d_ufDivByZero[width]; } - else if (k == kind::BITVECTOR_UREM) { - if (d_BVRemByZero.find(width) == d_BVRemByZero.end()) { - ostringstream os; + else if (k == kind::BITVECTOR_UREM) + { + if (d_ufRemByZero.find(width) == d_ufRemByZero.end()) + { + std::ostringstream os; os << "BVURemByZero_" << width; - Node divByZero = nm->mkSkolem(os.str(), - nm->mkFunctionType(nm->mkBitVectorType(width), nm->mkBitVectorType(width)), - "partial bvurem", NodeManager::SKOLEM_EXACT_NAME); - d_BVRemByZero[width] = divByZero; + Node divByZero = + nm->mkSkolem(os.str(), + nm->mkFunctionType(nm->mkBitVectorType(width), + nm->mkBitVectorType(width)), + "partial bvurem", + NodeManager::SKOLEM_EXACT_NAME); + d_ufRemByZero[width] = divByZero; } - return d_BVRemByZero[width]; + return d_ufRemByZero[width]; } Unreachable(); @@ -198,42 +103,47 @@ Node TheoryBV::getBVDivByZero(Kind k, unsigned width) { TrustNode TheoryBV::expandDefinition(Node node) { - Debug("bitvector-expandDefinition") << "TheoryBV::expandDefinition(" << node << ")" << std::endl; + Debug("bitvector-expandDefinition") + << "TheoryBV::expandDefinition(" << node << ")" << std::endl; Node ret; - switch (node.getKind()) { - case kind::BITVECTOR_SDIV: - case kind::BITVECTOR_SREM: - case kind::BITVECTOR_SMOD: - ret = TheoryBVRewriter::eliminateBVSDiv(node); - break; + switch (node.getKind()) + { + case kind::BITVECTOR_SDIV: + case kind::BITVECTOR_SREM: + case kind::BITVECTOR_SMOD: + ret = TheoryBVRewriter::eliminateBVSDiv(node); + break; - case kind::BITVECTOR_UDIV: - case kind::BITVECTOR_UREM: { - NodeManager* nm = NodeManager::currentNM(); - unsigned width = node.getType().getBitVectorSize(); + case kind::BITVECTOR_UDIV: + case kind::BITVECTOR_UREM: + { + NodeManager* nm = NodeManager::currentNM(); + unsigned width = node.getType().getBitVectorSize(); - if (options::bitvectorDivByZeroConst()) { - Kind kind = node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_UDIV_TOTAL : kind::BITVECTOR_UREM_TOTAL; - ret = nm->mkNode(kind, node[0], node[1]); - break; - } + if (options::bitvectorDivByZeroConst()) + { + Kind kind = node.getKind() == kind::BITVECTOR_UDIV + ? kind::BITVECTOR_UDIV_TOTAL + : kind::BITVECTOR_UREM_TOTAL; + ret = nm->mkNode(kind, node[0], node[1]); + break; + } - TNode num = node[0], den = node[1]; - Node den_eq_0 = nm->mkNode(kind::EQUAL, den, utils::mkZero(width)); - Node divTotalNumDen = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV - ? kind::BITVECTOR_UDIV_TOTAL - : kind::BITVECTOR_UREM_TOTAL, - num, - den); - Node divByZero = getBVDivByZero(node.getKind(), width); - Node divByZeroNum = nm->mkNode(kind::APPLY_UF, divByZero, num); - ret = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen); - } + TNode num = node[0], den = node[1]; + Node den_eq_0 = nm->mkNode(kind::EQUAL, den, utils::mkZero(width)); + Node divTotalNumDen = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV + ? kind::BITVECTOR_UDIV_TOTAL + : kind::BITVECTOR_UREM_TOTAL, + num, + den); + Node divByZero = getUFDivByZero(node.getKind(), width); + Node divByZeroNum = nm->mkNode(kind::APPLY_UF, divByZero, num); + ret = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen); + } break; - default: - break; + default: break; } if (!ret.isNull() && node != ret) { @@ -242,600 +152,50 @@ TrustNode TheoryBV::expandDefinition(Node node) return TrustNode::null(); } -void TheoryBV::preRegisterTerm(TNode node) { - d_calledPreregister = true; - Debug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl; - - if (options::bitblastMode() == options::BitblastMode::EAGER) - { - // the aig bit-blaster option is set heuristically - // if bv abstraction is used - if (!d_eagerSolver->isInitialized()) - { - d_eagerSolver->initialize(); - } - - if (node.getKind() == kind::BITVECTOR_EAGER_ATOM) - { - Node formula = node[0]; - d_eagerSolver->assertFormula(formula); - } - return; - } - - for (unsigned i = 0; i < d_subtheories.size(); ++i) { - d_subtheories[i]->preRegister(node); - } - - // AJR : equality solver currently registers all terms to ExtTheory, if we - // want a lazy reduction without the bv equality solver, need to call this - // d_extTheory->registerTermRec( node ); -} - -void TheoryBV::sendConflict() { - Assert(d_conflict); - if (d_conflictNode.isNull()) { - return; - } else { - Debug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode << std::endl; - d_out->conflict(d_conflictNode); - d_statistics.d_avgConflictSize.addEntry(d_conflictNode.getNumChildren()); - d_conflictNode = Node::null(); - } -} - -void TheoryBV::checkForLemma(TNode fact) +void TheoryBV::preRegisterTerm(TNode node) { - if (fact.getKind() == kind::EQUAL) - { - NodeManager* nm = NodeManager::currentNM(); - if (fact[0].getKind() == kind::BITVECTOR_UREM_TOTAL) - { - TNode urem = fact[0]; - TNode result = fact[1]; - TNode divisor = urem[1]; - Node result_ult_div = nm->mkNode(kind::BITVECTOR_ULT, result, divisor); - Node divisor_eq_0 = - nm->mkNode(kind::EQUAL, divisor, mkZero(getSize(divisor))); - Node split = nm->mkNode( - kind::OR, divisor_eq_0, nm->mkNode(kind::NOT, fact), result_ult_div); - lemma(split); - } - if (fact[1].getKind() == kind::BITVECTOR_UREM_TOTAL) - { - TNode urem = fact[1]; - TNode result = fact[0]; - TNode divisor = urem[1]; - Node result_ult_div = nm->mkNode(kind::BITVECTOR_ULT, result, divisor); - Node divisor_eq_0 = - nm->mkNode(kind::EQUAL, divisor, mkZero(getSize(divisor))); - Node split = nm->mkNode( - kind::OR, divisor_eq_0, nm->mkNode(kind::NOT, fact), result_ult_div); - lemma(split); - } - } + d_internal->preRegisterTerm(node); } -void TheoryBV::check(Effort e) -{ - if (done() && echeckExtf(e); - } - return; - } - - TimerStat::CodeTimer checkTimer(d_checkTime); - Debug("bitvector") << "TheoryBV::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 - d_invalidateModelCache.set(true); - // if we are using the eager solver - if (options::bitblastMode() == options::BitblastMode::EAGER) - { - // this can only happen on an empty benchmark - if (!d_eagerSolver->isInitialized()) { - d_eagerSolver->initialize(); - } - if (!Theory::fullEffort(e)) - return; - - std::vector assertions; - while (!done()) { - TNode fact = get().d_assertion; - Assert(fact.getKind() == kind::BITVECTOR_EAGER_ATOM); - assertions.push_back(fact); - d_eagerSolver->assertFormula(fact[0]); - } - - bool ok = d_eagerSolver->checkSat(); - if (!ok) { - if (assertions.size() == 1) { - d_out->conflict(assertions[0]); - return; - } - Node conflict = utils::mkAnd(assertions); - d_out->conflict(conflict); - return; - } - return; - } - - if (Theory::fullEffort(e)) { - ++(d_statistics.d_numCallsToCheckFullEffort); - } else { - ++(d_statistics.d_numCallsToCheckStandardEffort); - } - // if we are already in conflict just return the conflict - if (inConflict()) { - sendConflict(); - return; - } - - while (!done()) { - TNode fact = get().d_assertion; - - checkForLemma(fact); - - for (unsigned i = 0; i < d_subtheories.size(); ++i) { - d_subtheories[i]->assertFact(fact); - } - } - - bool ok = true; - bool complete = false; - for (unsigned i = 0; i < d_subtheories.size(); ++i) { - Assert(!inConflict()); - ok = d_subtheories[i]->check(e); - complete = d_subtheories[i]->isComplete(); - - if (!ok) { - // if we are in a conflict no need to check with other theories - Assert(inConflict()); - sendConflict(); - return; - } - if (complete) { - // if the last subtheory was complete we stop - 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 TheoryBV::preCheck(Effort e) { return d_internal->preCheck(e); } bool TheoryBV::needsCheckLastEffort() { - CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE]; - if (core) - { - return core->needsCheckLastEffort(); - } - return false; + return d_internal->needsCheckLastEffort(); } + bool TheoryBV::collectModelInfo(TheoryModel* m) { - Assert(!inConflict()); - if (options::bitblastMode() == options::BitblastMode::EAGER) - { - if (!d_eagerSolver->collectModelInfo(m, true)) - { - return false; - } - } - for (unsigned i = 0; i < d_subtheories.size(); ++i) { - if (d_subtheories[i]->isComplete()) { - return d_subtheories[i]->collectModelInfo(m, true); - } - } - return true; + return d_internal->collectModelInfo(m); } -Node TheoryBV::getModelValue(TNode var) { - Assert(!inConflict()); - for (unsigned i = 0; i < d_subtheories.size(); ++i) { - if (d_subtheories[i]->isComplete()) { - return d_subtheories[i]->getModelValue(var); - } - } - Unreachable(); -} - -void TheoryBV::propagate(Effort e) { - Debug("bitvector") << indent() << "TheoryBV::propagate()" << std::endl; - if (options::bitblastMode() == options::BitblastMode::EAGER) - { - return; - } - - if (inConflict()) { - return; - } - - // go through stored propagations - bool ok = true; - for (; d_literalsToPropagateIndex < d_literalsToPropagate.size() && ok; d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) { - TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex]; - // temporary fix for incremental bit-blasting - if (d_valuation.isSatLiteral(literal)) { - Debug("bitvector::propagate") << "TheoryBV:: propagating " << literal <<"\n"; - ok = d_out->propagate(literal); - } - } - - if (!ok) { - Debug("bitvector::propagate") << indent() << "TheoryBV::propagate(): conflict from theory engine" << std::endl; - setConflict(); - } -} +void TheoryBV::propagate(Effort e) { return d_internal->propagate(e); } Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { - switch (in.getKind()) - { - case kind::EQUAL: - { - if (in[0].isVar() && isLegalElimination(in[0], in[1])) - { - ++(d_statistics.d_solveSubstitutions); - outSubstitutions.addSubstitution(in[0], in[1]); - return PP_ASSERT_STATUS_SOLVED; - } - if (in[1].isVar() && isLegalElimination(in[1], in[0])) - { - ++(d_statistics.d_solveSubstitutions); - outSubstitutions.addSubstitution(in[1], in[0]); - return 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 (isLegalElimination(extract[0], concat)) - { - outSubstitutions.addSubstitution(extract[0], concat); - return 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 PP_ASSERT_STATUS_UNSOLVED; -} - -TrustNode TheoryBV::ppRewrite(TNode t) -{ - Debug("bv-pp-rewrite") << "TheoryBV::ppRewrite " << t << "\n"; - Node res = t; - if (options::bitwiseEq() && RewriteRule::applies(t)) { - Node result = RewriteRule::run(t); - res = Rewriter::rewrite(result); - } else if (RewriteRule::applies(t)) { - Node result = RewriteRule::run(t); - res = Rewriter::rewrite(result); - } - else if (res.getKind() == kind::EQUAL - && ((res[0].getKind() == kind::BITVECTOR_PLUS - && RewriteRule::applies(res[1])) - || (res[1].getKind() == kind::BITVECTOR_PLUS - && RewriteRule::applies(res[0])))) - { - Node mult = RewriteRule::applies(res[0])? - RewriteRule::run(res[0]) : - RewriteRule::run(res[1]); - Node factor = mult[0]; - Node sum = RewriteRule::applies(res[0])? res[1] : res[0]; - Node new_eq = NodeManager::currentNM()->mkNode(kind::EQUAL, sum, mult); - Node rewr_eq = RewriteRule::run(new_eq); - if (rewr_eq[0].isVar() || rewr_eq[1].isVar()){ - res = Rewriter::rewrite(rewr_eq); - } else { - res = t; - } - } - else if (RewriteRule::applies(t)) - { - res = RewriteRule::run(t); - } - else if (RewriteRule::applies(t)) - { - res = RewriteRule::run(t); - } - else if (RewriteRule::applies(t)) - { - res = RewriteRule::run(t); - } - - // if(t.getKind() == kind::EQUAL && - // ((t[0].getKind() == kind::BITVECTOR_MULT && t[1].getKind() == - // kind::BITVECTOR_PLUS) || - // (t[1].getKind() == kind::BITVECTOR_MULT && t[0].getKind() == - // kind::BITVECTOR_PLUS))) { - // // if we have an equality between a multiplication and addition - // // try to express multiplication in terms of addition - // Node mult = t[0].getKind() == kind::BITVECTOR_MULT? t[0] : t[1]; - // Node add = t[0].getKind() == kind::BITVECTOR_PLUS? t[0] : t[1]; - // if (RewriteRule::applies(mult)) { - // Node new_mult = RewriteRule::run(mult); - // Node new_eq = - // Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL, - // new_mult, add)); - - // // the simplification can cause the formula to blow up - // // only apply if formula reduced - // if (d_subtheoryMap.find(SUB_BITBLAST) != d_subtheoryMap.end()) { - // BitblastSolver* bv = (BitblastSolver*)d_subtheoryMap[SUB_BITBLAST]; - // uint64_t old_size = bv->computeAtomWeight(t); - // Assert (old_size); - // uint64_t new_size = bv->computeAtomWeight(new_eq); - // double ratio = ((double)new_size)/old_size; - // if (ratio <= 0.4) { - // ++(d_statistics.d_numMultSlice); - // return new_eq; - // } - // } - - // if (new_eq.getKind() == kind::CONST_BOOLEAN) { - // ++(d_statistics.d_numMultSlice); - // return new_eq; - // } - // } - // } - - if (options::bvAbstraction() && t.getType().isBoolean()) { - d_abstractionModule->addInputAtom(res); - } - Debug("bv-pp-rewrite") << "to " << res << "\n"; - if (res != t) - { - return TrustNode::mkTrustRewrite(t, res, nullptr); - } - return TrustNode::null(); -} - -void TheoryBV::presolve() { - Debug("bitvector") << "TheoryBV::presolve" << endl; -} - -static int prop_count = 0; - -bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory) -{ - Debug("bitvector::propagate") << indent() << getSatContext()->getLevel() << " " << "TheoryBV::storePropagation(" << literal << ", " << subtheory << ")" << std::endl; - prop_count++; - - // If already in conflict, no more propagation - if (d_conflict) { - Debug("bitvector::propagate") << indent() << "TheoryBV::storePropagation(" << literal << ", " << subtheory << "): already in conflict" << std::endl; - return false; - } - - // If propagated already, just skip - PropagatedMap::const_iterator find = d_propagatedBy.find(literal); - if (find != d_propagatedBy.end()) { - return true; - } else { - bool polarity = literal.getKind() != kind::NOT; - Node negatedLiteral = polarity ? literal.notNode() : (Node) literal[0]; - find = d_propagatedBy.find(negatedLiteral); - if (find != d_propagatedBy.end() && (*find).second != subtheory) { - // Safe to ignore this one, subtheory should produce a conflict - return true; - } - - d_propagatedBy[literal] = subtheory; - } - - // Propagate differs depending on the subtheory - // * bitblaster needs to be left alone until it's done, otherwise it doesn't - // know how to explain - // * equality engine can propagate eagerly - // TODO(2348): Determine if ok should be set by propagate. If not, remove ok. - constexpr bool ok = true; - if (subtheory == SUB_CORE) { - d_out->propagate(literal); - if (!ok) { - setConflict(); - } - } else { - d_literalsToPropagate.push_back(literal); - } - return ok; - -}/* TheoryBV::propagate(TNode) */ - - -void TheoryBV::explain(TNode literal, std::vector& assumptions) { - Assert(wasPropagatedBySubtheory(literal)); - SubTheory sub = getPropagatingSubtheory(literal); - d_subtheoryMap[sub]->explain(literal, assumptions); + return d_internal->ppAssert(in, outSubstitutions); } -TrustNode TheoryBV::explain(TNode node) -{ - Debug("bitvector::explain") << "TheoryBV::explain(" << node << ")" << std::endl; - std::vector assumptions; +TrustNode TheoryBV::ppRewrite(TNode t) { return d_internal->ppRewrite(t); } - // Ask for the explanation - explain(node, assumptions); - // this means that it is something true at level 0 - Node explanation; - if (assumptions.size() == 0) { - explanation = utils::mkTrue(); - } - else - { - // return the explanation - explanation = utils::mkAnd(assumptions); - } - Debug("bitvector::explain") << "TheoryBV::explain(" << node << ") => " << explanation << std::endl; - Debug("bitvector::explain") << "TheoryBV::explain done. \n"; - return TrustNode::mkTrustPropExp(node, explanation, nullptr); -} +void TheoryBV::presolve() { d_internal->presolve(); } -void TheoryBV::notifySharedTerm(TNode t) -{ - Debug("bitvector::sharing") - << indent() << "TheoryBV::notifySharedTerm(" << t << ")" << std::endl; - d_sharedTermsSet.insert(t); - if (options::bitvectorEqualitySolver()) { - for (unsigned i = 0; i < d_subtheories.size(); ++i) { - d_subtheories[i]->addSharedTerm(t); - } - } -} +TrustNode TheoryBV::explain(TNode node) { return d_internal->explain(node); } +void TheoryBV::notifySharedTerm(TNode t) { d_internal->notifySharedTerm(t); }; -EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b) +void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned) { - if (options::bitblastMode() == options::BitblastMode::EAGER) - return EQUALITY_UNKNOWN; - Assert(options::bitblastMode() == options::BitblastMode::LAZY); - for (unsigned i = 0; i < d_subtheories.size(); ++i) { - EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b); - if (status != EQUALITY_UNKNOWN) { - return status; - } - } - return EQUALITY_UNKNOWN; ; -} - -void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned) { - if(d_staticLearnCache.find(in) != d_staticLearnCache.end()){ - return; - } - d_staticLearnCache.insert(in); - - if (in.getKind() == kind::EQUAL) { - if((in[0].getKind() == kind::BITVECTOR_PLUS && in[1].getKind() == kind::BITVECTOR_SHL) || - (in[1].getKind() == kind::BITVECTOR_PLUS && in[0].getKind() == kind::BITVECTOR_SHL)) { - TNode p = in[0].getKind() == kind::BITVECTOR_PLUS ? in[0] : in[1]; - TNode s = in[0].getKind() == kind::BITVECTOR_PLUS ? in[1] : in[0]; - - if(p.getNumChildren() == 2 - && p[0].getKind() == kind::BITVECTOR_SHL - && p[1].getKind() == kind::BITVECTOR_SHL ){ - unsigned size = utils::getSize(s); - Node one = utils::mkConst(size, 1u); - if(s[0] == one && p[0][0] == one && p[1][0] == one){ - Node zero = utils::mkConst(size, 0u); - TNode b = p[0]; - TNode c = p[1]; - // (s : 1 << S) = (b : 1 << B) + (c : 1 << C) - Node b_eq_0 = b.eqNode(zero); - Node c_eq_0 = c.eqNode(zero); - Node b_eq_c = b.eqNode(c); - - Node dis = NodeManager::currentNM()->mkNode( - kind::OR, b_eq_0, c_eq_0, b_eq_c); - Node imp = in.impNode(dis); - learned << imp; - } - } - } - }else if(in.getKind() == kind::AND){ - for(size_t i = 0, N = in.getNumChildren(); i < N; ++i){ - ppStaticLearn(in[i], learned); - } - } + d_internal->ppStaticLearn(in, learned); } -bool TheoryBV::applyAbstraction(const std::vector& assertions, std::vector& new_assertions) { - bool changed = d_abstractionModule->applyAbstraction(assertions, new_assertions); - if (changed && options::bitblastMode() == options::BitblastMode::EAGER - && options::bitvectorAig()) - { - // disable AIG mode - AlwaysAssert(!d_eagerSolver->isInitialized()); - d_eagerSolver->turnOffAig(); - d_eagerSolver->initialize(); - } - return changed; -} - -void TheoryBV::setConflict(Node conflict) +bool TheoryBV::applyAbstraction(const std::vector& assertions, + std::vector& new_assertions) { - if (options::bvAbstraction()) - { - NodeManager* const nm = NodeManager::currentNM(); - Node new_conflict = d_abstractionModule->simplifyConflict(conflict); - - std::vector lemmas; - lemmas.push_back(new_conflict); - d_abstractionModule->generalizeConflict(new_conflict, lemmas); - for (unsigned i = 0; i < lemmas.size(); ++i) - { - lemma(nm->mkNode(kind::NOT, lemmas[i])); - } - } - d_conflict = true; - d_conflictNode = conflict; + return d_internal->applyAbstraction(assertions, new_assertions); } -} /* namespace CVC4::theory::bv */ -} /* namespace CVC4::theory */ -} /* namespace CVC4 */ +} // namespace bv +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 7475feccc..d33ea1337 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -20,42 +20,21 @@ #define CVC4__THEORY__BV__THEORY_BV_H #include -#include -#include "context/cdhashset.h" -#include "context/cdlist.h" -#include "context/context.h" -#include "theory/bv/bv_subtheory.h" #include "theory/bv/theory_bv_rewriter.h" -#include "theory/bv/theory_bv_utils.h" #include "theory/theory.h" -#include "util/hash.h" -#include "util/statistics_registry.h" namespace CVC4 { namespace theory { namespace bv { -class CoreSolver; -class InequalitySolver; -class AlgebraicSolver; -class BitblastSolver; +class BVSolver; -class EagerBitblastSolver; - -class AbstractionModule; - -class TheoryBV : public Theory { - - /** The context we are using */ - context::Context* d_context; - - /** Context dependent set of atoms we already propagated */ - context::CDHashSet d_alreadyPropagatedSet; - context::CDHashSet d_sharedTermsSet; - - std::vector> d_subtheories; - std::unordered_map > d_subtheoryMap; +class TheoryBV : public Theory +{ + /* BVSolverLazy accesses methods from theory in a way that is deprecated and + * will be removed in the future. For now we allow direct access. */ + friend class BVSolverLazy; public: TheoryBV(context::Context* c, @@ -68,24 +47,23 @@ class TheoryBV : public Theory { ~TheoryBV(); - //--------------------------------- initialization /** get the official theory rewriter of this theory */ TheoryRewriter* getTheoryRewriter() override; + /** * Returns true if we need an equality engine. If so, we initialize the * information regarding how it should be setup. For details, see the * documentation in Theory::needsEqualityEngine. */ bool needsEqualityEngine(EeSetupInfo& esi) override; - /** finish initialization */ + void finishInit() override; - //--------------------------------- end initialization TrustNode expandDefinition(Node node) override; void preRegisterTerm(TNode n) override; - void check(Effort e) override; + bool preCheck(Effort e) override; bool needsCheckLastEffort() override; @@ -105,146 +83,44 @@ class TheoryBV : public Theory { void presolve() override; + /** Called by abstraction preprocessing pass. */ bool applyAbstraction(const std::vector& assertions, std::vector& new_assertions); private: - class Statistics - { - public: - AverageStat d_avgConflictSize; - IntStat d_solveSubstitutions; - TimerStat d_solveTimer; - IntStat d_numCallsToCheckFullEffort; - IntStat d_numCallsToCheckStandardEffort; - TimerStat d_weightComputationTimer; - IntStat d_numMultSlice; - Statistics(); - ~Statistics(); - }; - - Statistics d_statistics; - - void spendResource(ResourceManager::Resource r); + void notifySharedTerm(TNode t) override; /** - * Return the uninterpreted function symbol corresponding to division-by-zero - * for this particular bit-width + * Return the UF symbol corresponding to division-by-zero for this particular + * bit-width. * @param k should be UREM or UDIV - * @param width - * - * @return + * @param width bit-width */ - Node getBVDivByZero(Kind k, unsigned width); + Node getUFDivByZero(Kind k, unsigned width); - typedef std::unordered_set TNodeSet; - typedef std::unordered_set NodeSet; - NodeSet d_staticLearnCache; + /** Internal BV solver. */ + std::unique_ptr d_internal; /** * Maps from bit-vector width to division-by-zero uninterpreted * function symbols. */ - std::unordered_map d_BVDivByZero; - std::unordered_map d_BVRemByZero; - - typedef std::unordered_map NodeToNode; - - context::CDO d_lemmasAdded; - - // Are we in conflict? - context::CDO d_conflict; - - // Invalidate the model cache if check was called - context::CDO d_invalidateModelCache; - - /** The conflict node */ - Node d_conflictNode; - - /** Literals to propagate */ - context::CDList d_literalsToPropagate; - - /** Index of the next literal to propagate */ - context::CDO d_literalsToPropagateIndex; - - /** - * Keeps a map from nodes to the subtheory that propagated it so that we can explain it - * properly. - */ - typedef context::CDHashMap PropagatedMap; - PropagatedMap d_propagatedBy; - - std::unique_ptr d_eagerSolver; - std::unique_ptr d_abstractionModule; - bool d_calledPreregister; - - bool wasPropagatedBySubtheory(TNode literal) const { - return d_propagatedBy.find(literal) != d_propagatedBy.end(); - } - - SubTheory getPropagatingSubtheory(TNode literal) const { - Assert(wasPropagatedBySubtheory(literal)); - PropagatedMap::const_iterator find = d_propagatedBy.find(literal); - return (*find).second; - } - - /** Should be called to propagate the literal. */ - bool storePropagation(TNode literal, SubTheory subtheory); - - /** - * Explains why this literal (propagated by subtheory) is true by adding assumptions. - */ - void explain(TNode literal, std::vector& assumptions); - - void notifySharedTerm(TNode t) override; - - bool isSharedTerm(TNode t) { return d_sharedTermsSet.contains(t); } - - EqualityStatus getEqualityStatus(TNode a, TNode b) override; - - Node getModelValue(TNode var) override; - - inline std::string indent() - { - std::string indentStr(getSatContext()->getLevel(), ' '); - return indentStr; - } - - void setConflict(Node conflict = Node::null()); - - bool inConflict() { - return d_conflict; - } - - void sendConflict(); - - void lemma(TNode node) - { - d_out->lemma(node); - d_lemmasAdded = true; - } - - void checkForLemma(TNode node); + std::unordered_map d_ufDivByZero; + std::unordered_map d_ufRemByZero; /** The theory rewriter for this theory. */ TheoryBVRewriter d_rewriter; + /** A (default) theory state object */ TheoryState d_state; - friend class LazyBitblaster; - friend class TLazyBitblaster; - friend class EagerBitblaster; - friend class BitblastSolver; - friend class EqualitySolver; - friend class CoreSolver; - friend class InequalitySolver; - friend class AlgebraicSolver; - friend class EagerBitblastSolver; -};/* class TheoryBV */ - -}/* CVC4::theory::bv namespace */ -}/* CVC4::theory namespace */ - -}/* CVC4 namespace */ + /** A (default) theory inference manager. */ + TheoryInferenceManager d_inferMgr; + +}; /* class TheoryBV */ + +} // namespace bv +} // namespace theory +} // namespace CVC4 #endif /* CVC4__THEORY__BV__THEORY_BV_H */ diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp index 40fa9c5ae..570b878b4 100644 --- a/src/theory/theory_inference_manager.cpp +++ b/src/theory/theory_inference_manager.cpp @@ -449,5 +449,15 @@ void TheoryInferenceManager::requirePhase(TNode n, bool pol) return d_out.requirePhase(n, pol); } +void TheoryInferenceManager::spendResource(ResourceManager::Resource r) +{ + d_out.spendResource(r); +} + +void TheoryInferenceManager::safePoint(ResourceManager::Resource r) +{ + d_out.safePoint(r); +} + } // namespace theory } // namespace CVC4 diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h index 92116648e..7fecacf82 100644 --- a/src/theory/theory_inference_manager.h +++ b/src/theory/theory_inference_manager.h @@ -329,6 +329,17 @@ class TheoryInferenceManager * decided with polarity pol, for details see OutputChannel::requirePhase. */ void requirePhase(TNode n, bool pol); + + /** + * Forward to OutputChannel::spendResource() to spend resources. + */ + void spendResource(ResourceManager::Resource r); + + /** + * Forward to OutputChannel::safePoint() to spend resources. + */ + void safePoint(ResourceManager::Resource r); + protected: /** * Process internal fact. This is a common helper method for the diff --git a/src/theory/theory_state.cpp b/src/theory/theory_state.cpp index 8afe3be96..f22a652c0 100644 --- a/src/theory/theory_state.cpp +++ b/src/theory/theory_state.cpp @@ -125,5 +125,10 @@ void TheoryState::notifyInConflict() { d_conflict = true; } bool TheoryState::isInConflict() const { return d_conflict; } +bool TheoryState::isSatLiteral(TNode lit) const +{ + return d_valuation.isSatLiteral(lit); +} + } // namespace theory } // namespace CVC4 diff --git a/src/theory/theory_state.h b/src/theory/theory_state.h index de6e6d477..4ae381e78 100644 --- a/src/theory/theory_state.h +++ b/src/theory/theory_state.h @@ -72,6 +72,9 @@ class TheoryState /** Are we currently in conflict? */ virtual bool isInConflict() const; + /** Returns true if lit is a SAT literal. */ + virtual bool isSatLiteral(TNode lit) const; + protected: /** Pointer to the SAT context object used by the theory. */ context::Context* d_context; diff --git a/test/unit/theory/theory_bv_white.h b/test/unit/theory/theory_bv_white.h index 582a031c9..cacd92d41 100644 --- a/test/unit/theory/theory_bv_white.h +++ b/test/unit/theory/theory_bv_white.h @@ -15,22 +15,20 @@ ** \todo document this file **/ - #include -#include "theory/theory.h" +#include + +#include "context/context.h" +#include "expr/node.h" +#include "expr/node_manager.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" -#include "theory/bv/theory_bv.h" #include "theory/bv/bitblast/eager_bitblaster.h" -#include "expr/node.h" -#include "expr/node_manager.h" -#include "context/context.h" - +#include "theory/bv/bv_solver_lazy.h" +#include "theory/theory.h" #include "theory/theory_test_utils.h" -#include - using namespace CVC4; using namespace CVC4::theory; using namespace CVC4::theory::bv; @@ -76,10 +74,11 @@ public: // engine d_smt. We must ensure that d_smt is properly initialized via // the following call, which constructs its underlying theory engine. d_smt->finishInit(); - EagerBitblaster* bb = new EagerBitblaster( - dynamic_cast( - d_smt->getTheoryEngine()->d_theoryTable[THEORY_BV]), - d_smt->getContext()); + TheoryBV* tbv = dynamic_cast( + d_smt->getTheoryEngine()->d_theoryTable[THEORY_BV]); + BVSolverLazy* bvsl = dynamic_cast(tbv->d_internal.get()); + EagerBitblaster* bb = new EagerBitblaster(bvsl, d_smt->getContext()); + Node x = d_nm->mkVar("x", d_nm->mkBitVectorType(16)); Node y = d_nm->mkVar("y", d_nm->mkBitVectorType(16)); Node x_plus_y = d_nm->mkNode(kind::BITVECTOR_PLUS, x, y); -- 2.30.2