From a917cc2ab4956b542b1f565abf0e62b197692f8d Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Mon, 2 Apr 2018 12:48:44 -0700 Subject: [PATCH] Reorganize bitblaster code. (#1695) This splits bitblaster_template.h into the separate header files {aig,eager,lazy}_bitblaster.h and bitblaster.h (the template class TBitblaster). All the bitblaster related code is moved into the sub-directory bitblast/. --- src/Makefile.am | 15 +- src/proof/bitvector_proof.cpp | 2 +- .../bv/{ => bitblast}/aig_bitblaster.cpp | 102 ++-- src/theory/bv/bitblast/aig_bitblaster.h | 105 ++++ .../bitblast_strategies_template.h | 9 +- src/theory/bv/{ => bitblast}/bitblast_utils.h | 23 +- src/theory/bv/bitblast/bitblaster.h | 261 +++++++++ .../bv/{ => bitblast}/eager_bitblaster.cpp | 64 +-- src/theory/bv/bitblast/eager_bitblaster.h | 89 +++ .../bv/{ => bitblast}/lazy_bitblaster.cpp | 106 ++-- src/theory/bv/bitblast/lazy_bitblaster.h | 181 +++++++ src/theory/bv/bitblaster_template.h | 508 ------------------ src/theory/bv/bv_eager_solver.cpp | 4 +- src/theory/bv/bv_quick_check.cpp | 2 +- src/theory/bv/bv_subtheory_bitblast.cpp | 10 +- src/theory/bv/bv_subtheory_bitblast.h | 3 +- test/unit/theory/theory_bv_white.h | 2 +- 17 files changed, 803 insertions(+), 683 deletions(-) rename src/theory/bv/{ => bitblast}/aig_bitblaster.cpp (87%) create mode 100644 src/theory/bv/bitblast/aig_bitblaster.h rename src/theory/bv/{ => bitblast}/bitblast_strategies_template.h (99%) rename src/theory/bv/{ => bitblast}/bitblast_utils.h (96%) create mode 100644 src/theory/bv/bitblast/bitblaster.h rename src/theory/bv/{ => bitblast}/eager_bitblaster.cpp (84%) create mode 100644 src/theory/bv/bitblast/eager_bitblaster.h rename src/theory/bv/{ => bitblast}/lazy_bitblaster.cpp (88%) create mode 100644 src/theory/bv/bitblast/lazy_bitblaster.h delete mode 100644 src/theory/bv/bitblaster_template.h diff --git a/src/Makefile.am b/src/Makefile.am index 6693deaa5..2beb8274d 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -292,10 +292,15 @@ libcvc4_la_SOURCES = \ theory/builtin/type_enumerator.h \ theory/bv/abstraction.cpp \ theory/bv/abstraction.h \ - theory/bv/aig_bitblaster.cpp \ - theory/bv/bitblast_strategies_template.h \ - theory/bv/bitblast_utils.h \ - theory/bv/bitblaster_template.h \ + theory/bv/bitblast/aig_bitblaster.cpp \ + theory/bv/bitblast/aig_bitblaster.h \ + theory/bv/bitblast/bitblast_strategies_template.h \ + theory/bv/bitblast/bitblast_utils.h \ + theory/bv/bitblast/bitblaster.h \ + theory/bv/bitblast/eager_bitblaster.cpp \ + theory/bv/bitblast/eager_bitblaster.h \ + theory/bv/bitblast/lazy_bitblaster.cpp \ + theory/bv/bitblast/lazy_bitblaster.h \ theory/bv/bv_eager_solver.cpp \ theory/bv/bv_eager_solver.h \ theory/bv/bv_inequality_graph.cpp \ @@ -317,8 +322,6 @@ libcvc4_la_SOURCES = \ theory/bv/bvgauss.h \ theory/bv/bvintropow2.cpp \ theory/bv/bvintropow2.h \ - theory/bv/eager_bitblaster.cpp \ - theory/bv/lazy_bitblaster.cpp \ theory/bv/slicer.cpp \ theory/bv/slicer.h \ theory/bv/theory_bv.cpp \ diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp index 907c809dd..7a2faba37 100644 --- a/src/proof/bitvector_proof.cpp +++ b/src/proof/bitvector_proof.cpp @@ -24,7 +24,7 @@ #include "proof/proof_utils.h" #include "proof/sat_proof_implementation.h" #include "prop/bvminisat/bvminisat.h" -#include "theory/bv/bitblaster_template.h" +#include "theory/bv/bitblast/bitblaster.h" #include "theory/bv/theory_bv.h" #include "theory/bv/theory_bv_rewrite_rules.h" diff --git a/src/theory/bv/aig_bitblaster.cpp b/src/theory/bv/bitblast/aig_bitblaster.cpp similarity index 87% rename from src/theory/bv/aig_bitblaster.cpp rename to src/theory/bv/bitblast/aig_bitblaster.cpp index 010eaf4e5..7e666bcbf 100644 --- a/src/theory/bv/aig_bitblaster.cpp +++ b/src/theory/bv/bitblast/aig_bitblaster.cpp @@ -9,29 +9,35 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief + ** \brief AIG bitblaster. ** - ** Bitblaster for the lazy bv solver. + ** AIG bitblaster. **/ -#include "bitblaster_template.h" - #include "cvc4_private.h" +#include "theory/bv/bitblast/aig_bitblaster.h" + #include "base/cvc4_check.h" #include "options/bv_options.h" -#include "prop/cnf_stream.h" #include "prop/sat_solver_factory.h" #include "smt/smt_statistics_registry.h" #ifdef CVC4_USE_ABC -// Function is defined as static in ABC. Not sure how else to do this. -static inline int Cnf_Lit2Var( int Lit ) { return (Lit & 1)? -(Lit >> 1)-1 : (Lit >> 1)+1; } extern "C" { -extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); +#include "base/abc/abc.h" +#include "base/main/main.h" +#include "sat/cnf/cnf.h" + +extern Aig_Man_t* Abc_NtkToDar(Abc_Ntk_t* pNtk, int fExors, int fRegisters); } +// Function is defined as static in ABC. Not sure how else to do this. +static inline int Cnf_Lit2Var(int Lit) +{ + return (Lit & 1) ? -(Lit >> 1) - 1 : (Lit >> 1) + 1; +} namespace CVC4 { namespace theory { @@ -110,26 +116,17 @@ Abc_Obj_t* mkIte(Abc_Obj_t* cond, Abc_Obj_t* a, Abc_Obj_t* b) { return Abc_AigMux(AigBitblaster::currentAigM(), cond, a, b); } -} /* CVC4::theory::bv */ -} /* CVC4::theory */ -} /* CVC4 */ - -using namespace CVC4; -using namespace CVC4::theory; -using namespace CVC4::theory::bv; - - -Abc_Ntk_t* AigBitblaster::abcAigNetwork = NULL; +CVC4_THREAD_LOCAL Abc_Ntk_t* AigBitblaster::s_abcAigNetwork = nullptr; Abc_Ntk_t* AigBitblaster::currentAigNtk() { - if (!AigBitblaster::abcAigNetwork) { + if (!AigBitblaster::s_abcAigNetwork) { Abc_Start(); - abcAigNetwork = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1); + s_abcAigNetwork = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1); char pName[] = "CVC4::theory::bv::AigNetwork"; - abcAigNetwork->pName = Extra_UtilStrsav(pName); + s_abcAigNetwork->pName = Extra_UtilStrsav(pName); } - return abcAigNetwork; + return s_abcAigNetwork; } @@ -138,34 +135,39 @@ Abc_Aig_t* AigBitblaster::currentAigM() { } AigBitblaster::AigBitblaster() - : TBitblaster() - , d_aigCache() - , d_bbAtoms() - , d_aigOutputNode(NULL) + : TBitblaster(), + d_nullContext(new context::Context()), + d_aigCache(), + d_bbAtoms(), + d_aigOutputNode(NULL) { - d_nullContext = new context::Context(); - switch(options::bvSatSolver()) { - case SAT_SOLVER_MINISAT: { - prop::BVSatSolverInterface* minisat = prop::SatSolverFactory::createMinisat(d_nullContext, - smtStatisticsRegistry(), - "AigBitblaster"); - MinisatEmptyNotify* notify = new MinisatEmptyNotify(); - minisat->setNotify(notify); - d_satSolver = minisat; - break; - } - case SAT_SOLVER_CRYPTOMINISAT: - d_satSolver = prop::SatSolverFactory::createCryptoMinisat(smtStatisticsRegistry(), - "AigBitblaster"); - break; - default: CVC4_FATAL() << "Unknown SAT solver type"; + prop::SatSolver* solver = nullptr; + switch (options::bvSatSolver()) + { + case SAT_SOLVER_MINISAT: + { + prop::BVSatSolverInterface* minisat = + prop::SatSolverFactory::createMinisat( + d_nullContext.get(), smtStatisticsRegistry(), "AigBitblaster"); + MinisatEmptyNotify notify; + minisat->setNotify(¬ify); + solver = minisat; + break; + } + case SAT_SOLVER_CADICAL: + solver = prop::SatSolverFactory::createCadical(smtStatisticsRegistry(), + "AigBitblaster"); + break; + case SAT_SOLVER_CRYPTOMINISAT: + solver = prop::SatSolverFactory::createCryptoMinisat( + smtStatisticsRegistry(), "AigBitblaster"); + break; + default: CVC4_FATAL() << "Unknown SAT solver type"; } + d_satSolver.reset(solver); } -AigBitblaster::~AigBitblaster() { - Assert (abcAigNetwork == NULL); - delete d_nullContext; -} +AigBitblaster::~AigBitblaster() {} Abc_Obj_t* AigBitblaster::bbFormula(TNode node) { Assert (node.getType().isBoolean()); @@ -363,7 +365,7 @@ void AigBitblaster::simplifyAig() { fprintf( stdout, "Cannot execute command \"%s\".\n", command ); exit(-1); } - abcAigNetwork = Abc_FrameReadNtk(pAbc); + s_abcAigNetwork = Abc_FrameReadNtk(pAbc); } @@ -380,7 +382,7 @@ void AigBitblaster::convertToCnfAndAssert() { // // free old network // Abc_NtkDelete(currentAigNtk()); - // abcAigNetwork = NULL; + // s_abcAigNetwork = NULL; Assert (pMan != NULL); Assert (Aig_ManCheck(pMan)); @@ -485,4 +487,8 @@ AigBitblaster::Statistics::~Statistics() { smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime); smtStatisticsRegistry()->unregisterStat(&d_solveTime); } + +} // namespace bv +} // namespace theory +} // namespace CVC4 #endif // CVC4_USE_ABC diff --git a/src/theory/bv/bitblast/aig_bitblaster.h b/src/theory/bv/bitblast/aig_bitblaster.h new file mode 100644 index 000000000..30f1dd00b --- /dev/null +++ b/src/theory/bv/bitblast/aig_bitblaster.h @@ -0,0 +1,105 @@ +/********************* */ +/*! \file aig_bitblaster.h + ** \verbatim + ** Top contributors (to current version): + ** Liana Hadarean, Tim King, Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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 AIG bitblaster. + ** + ** AIG Bitblaster based on ABC. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H +#define __CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H + +#include "theory/bv/bitblast/bitblaster.h" + +#include "base/tls.h" + +class Abc_Obj_t_; +typedef Abc_Obj_t_ Abc_Obj_t; + +class Abc_Ntk_t_; +typedef Abc_Ntk_t_ Abc_Ntk_t; + +class Abc_Aig_t_; +typedef Abc_Aig_t_ Abc_Aig_t; + +class Cnf_Dat_t_; +typedef Cnf_Dat_t_ Cnf_Dat_t; + +namespace CVC4 { +namespace theory { +namespace bv { + +class AigBitblaster : public TBitblaster +{ + public: + AigBitblaster(); + ~AigBitblaster(); + + void makeVariable(TNode node, Bits& bits) override; + void bbTerm(TNode node, Bits& bits) override; + void bbAtom(TNode node) override; + Abc_Obj_t* bbFormula(TNode formula); + bool solve(TNode query); + static Abc_Aig_t* currentAigM(); + static Abc_Ntk_t* currentAigNtk(); + + private: + typedef std::unordered_map TNodeAigMap; + typedef std::unordered_map NodeAigMap; + + static CVC4_THREAD_LOCAL Abc_Ntk_t* s_abcAigNetwork; + std::unique_ptr d_nullContext; + std::unique_ptr d_satSolver; + TNodeAigMap d_aigCache; + NodeAigMap d_bbAtoms; + + NodeAigMap d_nodeToAigInput; + // the thing we are checking for sat + Abc_Obj_t* d_aigOutputNode; + + void addAtom(TNode atom); + void simplifyAig(); + void storeBBAtom(TNode atom, Abc_Obj_t* atom_bb) override; + Abc_Obj_t* getBBAtom(TNode atom) const override; + bool hasBBAtom(TNode atom) const override; + void cacheAig(TNode node, Abc_Obj_t* aig); + bool hasAig(TNode node); + Abc_Obj_t* getAig(TNode node); + Abc_Obj_t* mkInput(TNode input); + bool hasInput(TNode input); + void convertToCnfAndAssert(); + void assertToSatSolver(Cnf_Dat_t* pCnf); + Node getModelFromSatSolver(TNode a, bool fullModel) override + { + Unreachable(); + } + + class Statistics + { + public: + IntStat d_numClauses; + IntStat d_numVariables; + TimerStat d_simplificationTime; + TimerStat d_cnfConversionTime; + TimerStat d_solveTime; + Statistics(); + ~Statistics(); + }; + + Statistics d_statistics; +}; + +} // namespace bv +} // namespace theory +} // namespace CVC4 +#endif // __CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H diff --git a/src/theory/bv/bitblast_strategies_template.h b/src/theory/bv/bitblast/bitblast_strategies_template.h similarity index 99% rename from src/theory/bv/bitblast_strategies_template.h rename to src/theory/bv/bitblast/bitblast_strategies_template.h index 60e7fc051..3c8b7bddc 100644 --- a/src/theory/bv/bitblast_strategies_template.h +++ b/src/theory/bv/bitblast/bitblast_strategies_template.h @@ -14,15 +14,16 @@ ** Implementation of bitblasting functions for various operators. **/ -#ifndef __CVC4__BITBLAST__STRATEGIES_TEMPLATE_H -#define __CVC4__BITBLAST__STRATEGIES_TEMPLATE_H +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__BV__BITBLAST__BITBLAST_STRATEGIES_TEMPLATE_H +#define __CVC4__THEORY__BV__BITBLAST__BITBLAST_STRATEGIES_TEMPLATE_H #include #include -#include "cvc4_private.h" #include "expr/node.h" -#include "theory/bv/bitblast_utils.h" +#include "theory/bv/bitblast/bitblast_utils.h" #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" diff --git a/src/theory/bv/bitblast_utils.h b/src/theory/bv/bitblast/bitblast_utils.h similarity index 96% rename from src/theory/bv/bitblast_utils.h rename to src/theory/bv/bitblast/bitblast_utils.h index 1d6920007..a2991c529 100644 --- a/src/theory/bv/bitblast_utils.h +++ b/src/theory/bv/bitblast/bitblast_utils.h @@ -16,24 +16,14 @@ #include "cvc4_private.h" -#ifndef __CVC4__BITBLAST__UTILS_H -#define __CVC4__BITBLAST__UTILS_H +#ifndef __CVC4__THEORY__BV__BITBLAST__BITBLAST_UTILS_H +#define __CVC4__THEORY__BV__BITBLAST__BITBLAST_UTILS_H #include #include "expr/node.h" -#ifdef CVC4_USE_ABC -#include "base/main/main.h" -#include "base/abc/abc.h" - -extern "C" { -#include "sat/cnf/cnf.h" -} -#endif - namespace CVC4 { - namespace theory { namespace bv { @@ -275,9 +265,8 @@ T inline sLessThanBB(const std::vector&a, const std::vector& b, bool orEqu return res; } +} // namespace bv +} // namespace theory +} // namespace CVC4 -} -} -} - -#endif +#endif // __CVC4__THEORY__BV__BITBLAST__BITBLAST_UTILS_H diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h new file mode 100644 index 000000000..f9c444b45 --- /dev/null +++ b/src/theory/bv/bitblast/bitblaster.h @@ -0,0 +1,261 @@ +/********************* */ +/*! \file bitblaster.h + ** \verbatim + ** Top contributors (to current version): + ** Liana Hadarean, Tim King, Clark Barrett + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 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 Wrapper around the SAT solver used for bitblasting + ** + ** Wrapper around the SAT solver used for bitblasting. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__BV__BITBLAST__BITBLASTER_H +#define __CVC4__THEORY__BV__BITBLAST__BITBLASTER_H + +#include +#include +#include + +#include "expr/node.h" +#include "prop/sat_solver.h" +#include "theory/bv/bitblast/bitblast_strategies_template.h" +#include "theory/theory_registrar.h" +#include "theory/valuation.h" +#include "util/resource_manager.h" + +namespace CVC4 { +namespace theory { +namespace bv { + +typedef std::unordered_set NodeSet; +typedef std::unordered_set TNodeSet; + +/** + * The Bitblaster that manages the mapping between Nodes + * and their bitwise definition + * + */ + +template +class TBitblaster +{ + protected: + typedef std::vector Bits; + typedef std::unordered_map TermDefMap; + typedef std::unordered_set TNodeSet; + typedef std::unordered_map ModelCache; + + typedef void (*TermBBStrategy)(TNode, Bits&, TBitblaster*); + typedef T (*AtomBBStrategy)(TNode, TBitblaster*); + + // caches and mappings + TermDefMap d_termCache; + ModelCache d_modelCache; + + BitVectorProof* d_bvp; + + void initAtomBBStrategies(); + void initTermBBStrategies(); + + protected: + /// function tables for the various bitblasting strategies indexed by node + /// kind + TermBBStrategy d_termBBStrategies[kind::LAST_KIND]; + AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND]; + virtual Node getModelFromSatSolver(TNode node, bool fullModel) = 0; + + public: + TBitblaster(); + virtual ~TBitblaster() {} + virtual void bbAtom(TNode node) = 0; + virtual void bbTerm(TNode node, Bits& bits) = 0; + virtual void makeVariable(TNode node, Bits& bits) = 0; + virtual T getBBAtom(TNode atom) const = 0; + virtual bool hasBBAtom(TNode atom) const = 0; + virtual void storeBBAtom(TNode atom, T atom_bb) = 0; + + bool hasBBTerm(TNode node) const; + void getBBTerm(TNode node, Bits& bits) const; + virtual void storeBBTerm(TNode term, const Bits& bits); + /** + * Return a constant representing the value of a in the model. + * If fullModel is true set unconstrained bits to 0. If not return + * NullNode() for a fully or partially unconstrained. + * + */ + Node getTermModel(TNode node, bool fullModel); + void invalidateModelCache(); +}; + +class MinisatEmptyNotify : public prop::BVSatSolverInterface::Notify +{ + public: + MinisatEmptyNotify() {} + bool notify(prop::SatLiteral lit) override { return true; } + void notify(prop::SatClause& clause) override {} + void spendResource(unsigned amount) override + { + NodeManager::currentResourceManager()->spendResource(amount); + } + void safePoint(unsigned amount) override {} +}; + +// Bitblaster implementation + +template +void TBitblaster::initAtomBBStrategies() +{ + for (int i = 0; i < kind::LAST_KIND; ++i) + { + d_atomBBStrategies[i] = UndefinedAtomBBStrategy; + } + /// setting default bb strategies for atoms + d_atomBBStrategies[kind::EQUAL] = DefaultEqBB; + d_atomBBStrategies[kind::BITVECTOR_ULT] = DefaultUltBB; + d_atomBBStrategies[kind::BITVECTOR_ULE] = DefaultUleBB; + d_atomBBStrategies[kind::BITVECTOR_UGT] = DefaultUgtBB; + d_atomBBStrategies[kind::BITVECTOR_UGE] = DefaultUgeBB; + d_atomBBStrategies[kind::BITVECTOR_SLT] = DefaultSltBB; + d_atomBBStrategies[kind::BITVECTOR_SLE] = DefaultSleBB; + d_atomBBStrategies[kind::BITVECTOR_SGT] = DefaultSgtBB; + d_atomBBStrategies[kind::BITVECTOR_SGE] = DefaultSgeBB; +} + +template +void TBitblaster::initTermBBStrategies() +{ + for (int i = 0; i < kind::LAST_KIND; ++i) + { + d_termBBStrategies[i] = DefaultVarBB; + } + /// setting default bb strategies for terms: + d_termBBStrategies[kind::CONST_BITVECTOR] = DefaultConstBB; + d_termBBStrategies[kind::BITVECTOR_NOT] = DefaultNotBB; + d_termBBStrategies[kind::BITVECTOR_CONCAT] = DefaultConcatBB; + d_termBBStrategies[kind::BITVECTOR_AND] = DefaultAndBB; + d_termBBStrategies[kind::BITVECTOR_OR] = DefaultOrBB; + d_termBBStrategies[kind::BITVECTOR_XOR] = DefaultXorBB; + d_termBBStrategies[kind::BITVECTOR_XNOR] = DefaultXnorBB; + d_termBBStrategies[kind::BITVECTOR_NAND] = DefaultNandBB; + d_termBBStrategies[kind::BITVECTOR_NOR] = DefaultNorBB; + d_termBBStrategies[kind::BITVECTOR_COMP] = DefaultCompBB; + d_termBBStrategies[kind::BITVECTOR_MULT] = DefaultMultBB; + d_termBBStrategies[kind::BITVECTOR_PLUS] = DefaultPlusBB; + d_termBBStrategies[kind::BITVECTOR_SUB] = DefaultSubBB; + d_termBBStrategies[kind::BITVECTOR_NEG] = DefaultNegBB; + d_termBBStrategies[kind::BITVECTOR_UDIV] = UndefinedTermBBStrategy; + d_termBBStrategies[kind::BITVECTOR_UREM] = UndefinedTermBBStrategy; + d_termBBStrategies[kind::BITVECTOR_UDIV_TOTAL] = DefaultUdivBB; + d_termBBStrategies[kind::BITVECTOR_UREM_TOTAL] = DefaultUremBB; + d_termBBStrategies[kind::BITVECTOR_SDIV] = UndefinedTermBBStrategy; + d_termBBStrategies[kind::BITVECTOR_SREM] = UndefinedTermBBStrategy; + d_termBBStrategies[kind::BITVECTOR_SMOD] = UndefinedTermBBStrategy; + d_termBBStrategies[kind::BITVECTOR_SHL] = DefaultShlBB; + d_termBBStrategies[kind::BITVECTOR_LSHR] = DefaultLshrBB; + d_termBBStrategies[kind::BITVECTOR_ASHR] = DefaultAshrBB; + d_termBBStrategies[kind::BITVECTOR_ULTBV] = DefaultUltbvBB; + d_termBBStrategies[kind::BITVECTOR_SLTBV] = DefaultSltbvBB; + d_termBBStrategies[kind::BITVECTOR_ITE] = DefaultIteBB; + d_termBBStrategies[kind::BITVECTOR_EXTRACT] = DefaultExtractBB; + d_termBBStrategies[kind::BITVECTOR_REPEAT] = DefaultRepeatBB; + d_termBBStrategies[kind::BITVECTOR_ZERO_EXTEND] = DefaultZeroExtendBB; + d_termBBStrategies[kind::BITVECTOR_SIGN_EXTEND] = DefaultSignExtendBB; + d_termBBStrategies[kind::BITVECTOR_ROTATE_RIGHT] = DefaultRotateRightBB; + d_termBBStrategies[kind::BITVECTOR_ROTATE_LEFT] = DefaultRotateLeftBB; +} + +template +TBitblaster::TBitblaster() : d_termCache(), d_modelCache(), d_bvp(NULL) +{ + initAtomBBStrategies(); + initTermBBStrategies(); +} + +template +bool TBitblaster::hasBBTerm(TNode node) const +{ + return d_termCache.find(node) != d_termCache.end(); +} +template +void TBitblaster::getBBTerm(TNode node, Bits& bits) const +{ + Assert(hasBBTerm(node)); + bits = d_termCache.find(node)->second; +} + +template +void TBitblaster::storeBBTerm(TNode node, const Bits& bits) +{ + d_termCache.insert(std::make_pair(node, bits)); +} + +template +void TBitblaster::invalidateModelCache() +{ + d_modelCache.clear(); +} + +template +Node TBitblaster::getTermModel(TNode node, bool fullModel) +{ + if (d_modelCache.find(node) != d_modelCache.end()) return d_modelCache[node]; + + if (node.isConst()) return node; + + Node value = getModelFromSatSolver(node, false); + if (!value.isNull()) + { + Debug("bv-equality-status") + << "TLazyBitblaster::getTermModel from SatSolver" << node << " => " + << value << "\n"; + d_modelCache[node] = value; + Assert(value.isConst()); + return value; + } + + if (Theory::isLeafOf(node, theory::THEORY_BV)) + { + // if it is a leaf may ask for fullModel + value = getModelFromSatSolver(node, true); + Debug("bv-equality-status") << "TLazyBitblaster::getTermModel from VarValue" + << node << " => " << value << "\n"; + Assert((fullModel && !value.isNull() && value.isConst()) || !fullModel); + if (!value.isNull()) + { + d_modelCache[node] = value; + } + return value; + } + Assert(node.getType().isBitVector()); + + NodeBuilder<> nb(node.getKind()); + if (node.getMetaKind() == kind::metakind::PARAMETERIZED) + { + nb << node.getOperator(); + } + + for (unsigned i = 0; i < node.getNumChildren(); ++i) + { + nb << getTermModel(node[i], fullModel); + } + value = nb; + value = Rewriter::rewrite(value); + Assert(value.isConst()); + d_modelCache[node] = value; + Debug("bv-term-model") << "TLazyBitblaster::getTermModel Building Value" + << node << " => " << value << "\n"; + return value; +} + +} // namespace bv +} // namespace theory +} // namespace CVC4 + +#endif /* __CVC4__THEORY__BV__BITBLAST__BITBLASTER_H */ diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp similarity index 84% rename from src/theory/bv/eager_bitblaster.cpp rename to src/theory/bv/bitblast/eager_bitblaster.cpp index 25610af2b..d49c1f432 100644 --- a/src/theory/bv/eager_bitblaster.cpp +++ b/src/theory/bv/bitblast/eager_bitblaster.cpp @@ -16,12 +16,13 @@ #include "cvc4_private.h" +#include "theory/bv/bitblast/eager_bitblaster.h" + #include "options/bv_options.h" #include "proof/bitvector_proof.h" #include "prop/cnf_stream.h" #include "prop/sat_solver_factory.h" #include "smt/smt_statistics_registry.h" -#include "theory/bv/bitblaster_template.h" #include "theory/bv/theory_bv.h" #include "theory/theory_model.h" @@ -29,58 +30,50 @@ namespace CVC4 { namespace theory { namespace bv { -void BitblastingRegistrar::preRegister(Node n) { d_bitblaster->bbAtom(n); } - EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv) : TBitblaster(), - d_satSolver(NULL), - d_bitblastingRegistrar(NULL), - d_nullContext(NULL), - d_cnfStream(NULL), + d_satSolver(), + d_bitblastingRegistrar(new BitblastingRegistrar(this)), + d_nullContext(new context::Context()), + d_cnfStream(), d_bv(theory_bv), d_bbAtoms(), d_variables(), - d_notify(NULL) { - d_bitblastingRegistrar = new BitblastingRegistrar(this); - d_nullContext = new context::Context(); - + d_notify() +{ + prop::SatSolver *solver = nullptr; switch (options::bvSatSolver()) { case SAT_SOLVER_MINISAT: { prop::BVSatSolverInterface* minisat = prop::SatSolverFactory::createMinisat( - d_nullContext, smtStatisticsRegistry(), "EagerBitblaster"); - d_notify = new MinisatEmptyNotify(); - minisat->setNotify(d_notify); - d_satSolver = minisat; + d_nullContext.get(), smtStatisticsRegistry(), "EagerBitblaster"); + d_notify.reset(new MinisatEmptyNotify()); + minisat->setNotify(d_notify.get()); + solver = minisat; break; } case SAT_SOLVER_CADICAL: - d_satSolver = prop::SatSolverFactory::createCadical( - smtStatisticsRegistry(), "EagerBitblaster"); + solver = prop::SatSolverFactory::createCadical(smtStatisticsRegistry(), + "EagerBitblaster"); break; case SAT_SOLVER_CRYPTOMINISAT: - d_satSolver = prop::SatSolverFactory::createCryptoMinisat( + solver = prop::SatSolverFactory::createCryptoMinisat( smtStatisticsRegistry(), "EagerBitblaster"); break; default: Unreachable("Unknown SAT solver type"); } - - d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_bitblastingRegistrar, - d_nullContext, options::proof(), - "EagerBitblaster"); - - d_bvp = NULL; + d_satSolver.reset(solver); + d_cnfStream.reset( + new prop::TseitinCnfStream(d_satSolver.get(), + d_bitblastingRegistrar.get(), + d_nullContext.get(), + options::proof(), + "EagerBitblaster")); } -EagerBitblaster::~EagerBitblaster() { - delete d_cnfStream; - delete d_satSolver; - delete d_notify; - delete d_nullContext; - delete d_bitblastingRegistrar; -} +EagerBitblaster::~EagerBitblaster() {} void EagerBitblaster::bbFormula(TNode node) { d_cnfStream->convertAndAssert(node, false, false, RULE_INVALID, @@ -257,13 +250,14 @@ bool EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) void EagerBitblaster::setProofLog(BitVectorProof* bvp) { d_bvp = bvp; d_satSolver->setProofLog(bvp); - bvp->initCnfProof(d_cnfStream, d_nullContext); + bvp->initCnfProof(d_cnfStream.get(), d_nullContext.get()); } bool EagerBitblaster::isSharedTerm(TNode node) { return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end(); } -} /* namespace CVC4::theory::bv; */ -} /* namespace CVC4::theory; */ -} /* namespace CVC4; */ + +} // namespace bv +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/bv/bitblast/eager_bitblaster.h b/src/theory/bv/bitblast/eager_bitblaster.h new file mode 100644 index 000000000..8610d0181 --- /dev/null +++ b/src/theory/bv/bitblast/eager_bitblaster.h @@ -0,0 +1,89 @@ +/********************* */ +/*! \file eager_bitblaster.h + ** \verbatim + ** Top contributors (to current version): + ** Liana Hadarean, Tim King, Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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 Bitblaster for eager BV solver. + ** + ** Bitblaster for the eager BV solver. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H +#define __CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H + +#include + +#include "theory/bv/bitblast/bitblaster.h" + +#include "prop/cnf_stream.h" +#include "prop/sat_solver.h" + +namespace CVC4 { +namespace theory { +namespace bv { + +class BitblastingRegistrar; +class TheoryBV; + +class EagerBitblaster : public TBitblaster +{ + public: + EagerBitblaster(TheoryBV* theory_bv); + ~EagerBitblaster(); + + void addAtom(TNode atom); + void makeVariable(TNode node, Bits& bits) override; + void bbTerm(TNode node, Bits& bits) override; + void bbAtom(TNode node) override; + Node getBBAtom(TNode node) const override; + bool hasBBAtom(TNode atom) const override; + void bbFormula(TNode formula); + void storeBBAtom(TNode atom, Node atom_bb) override; + void storeBBTerm(TNode node, const Bits& bits) override; + + bool assertToSat(TNode node, bool propagate = true); + bool solve(); + bool collectModelInfo(TheoryModel* m, bool fullModel); + void setProofLog(BitVectorProof* bvp); + + private: + typedef std::unordered_set TNodeSet; + // sat solver used for bitblasting and associated CnfStream + std::unique_ptr d_satSolver; + std::unique_ptr d_bitblastingRegistrar; + std::unique_ptr d_nullContext; + std::unique_ptr d_cnfStream; + + TheoryBV* d_bv; + TNodeSet d_bbAtoms; + TNodeSet d_variables; + + // This is either an MinisatEmptyNotify or NULL. + std::unique_ptr d_notify; + + Node getModelFromSatSolver(TNode a, bool fullModel) override; + bool isSharedTerm(TNode node); +}; + +class BitblastingRegistrar : public prop::Registrar +{ + public: + BitblastingRegistrar(EagerBitblaster* bb) : d_bitblaster(bb) {} + void preRegister(Node n) override { d_bitblaster->bbAtom(n); } + + private: + EagerBitblaster* d_bitblaster; +}; + +} // namespace bv +} // namespace theory +} // namespace CVC4 +#endif // __CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp similarity index 88% rename from src/theory/bv/lazy_bitblaster.cpp rename to src/theory/bv/bitblast/lazy_bitblaster.cpp index 189898c0c..539d40384 100644 --- a/src/theory/bv/lazy_bitblaster.cpp +++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp @@ -14,8 +14,10 @@ ** Bitblaster for the lazy bv solver. **/ -#include "bitblaster_template.h" #include "cvc4_private.h" + +#include "theory/bv/bitblast/lazy_bitblaster.h" + #include "options/bv_options.h" #include "prop/cnf_stream.h" #include "prop/sat_solver.h" @@ -57,38 +59,42 @@ uint64_t numNodes(TNode node, utils::NodeSet& seen) } } +TLazyBitblaster::TLazyBitblaster(context::Context* c, + bv::TheoryBV* bv, + const std::string name, + bool emptyNotify) + : TBitblaster(), + d_bv(bv), + d_ctx(c), + d_nullRegistrar(new prop::NullRegistrar()), + d_nullContext(new context::Context()), + d_assertedAtoms(new (true) context::CDList(c)), + d_explanations(new (true) ExplanationMap(c)), + d_variables(), + d_bbAtoms(), + d_abstraction(NULL), + d_emptyNotify(emptyNotify), + d_fullModelAssertionLevel(c, 0), + d_name(name), + d_statistics(name) +{ + d_satSolver.reset( + prop::SatSolverFactory::createMinisat(c, smtStatisticsRegistry(), name)); -TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, - const std::string name, bool emptyNotify) - : TBitblaster() - , d_bv(bv) - , d_ctx(c) - , d_assertedAtoms(new(true) context::CDList(c)) - , d_explanations(new(true) ExplanationMap(c)) - , d_variables() - , d_bbAtoms() - , d_abstraction(NULL) - , d_emptyNotify(emptyNotify) - , d_fullModelAssertionLevel(c, 0) - , d_name(name) - , d_statistics(name) { - - d_satSolver = prop::SatSolverFactory::createMinisat( - c, smtStatisticsRegistry(), name); - d_nullRegistrar = new prop::NullRegistrar(); - d_nullContext = new context::Context(); - d_cnfStream = new prop::TseitinCnfStream(d_satSolver, - d_nullRegistrar, - d_nullContext, - options::proof(), - "LazyBitblaster"); + d_cnfStream.reset( + new prop::TseitinCnfStream(d_satSolver.get(), + d_nullRegistrar.get(), + d_nullContext.get(), + options::proof(), + "LazyBitblaster")); - d_satSolverNotify = d_emptyNotify ? - (prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() : - (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, bv, - this); + d_satSolverNotify.reset( + d_emptyNotify + ? (prop::BVSatSolverInterface::Notify*)new MinisatEmptyNotify() + : (prop::BVSatSolverInterface::Notify*)new MinisatNotify( + d_cnfStream.get(), bv, this)); - d_satSolver->setNotify(d_satSolverNotify); + d_satSolver->setNotify(d_satSolverNotify.get()); } void TLazyBitblaster::setAbstraction(AbstractionModule* abs) { @@ -97,11 +103,6 @@ void TLazyBitblaster::setAbstraction(AbstractionModule* abs) { TLazyBitblaster::~TLazyBitblaster() { - delete d_cnfStream; - delete d_nullRegistrar; - delete d_nullContext; - delete d_satSolver; - delete d_satSolverNotify; d_assertedAtoms->deleteSelf(); d_explanations->deleteSelf(); } @@ -568,14 +569,11 @@ bool TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) void TLazyBitblaster::setProofLog( BitVectorProof * bvp ){ d_bvp = bvp; d_satSolver->setProofLog( bvp ); - bvp->initCnfProof(d_cnfStream, d_nullContext); + bvp->initCnfProof(d_cnfStream.get(), d_nullContext.get()); } void TLazyBitblaster::clearSolver() { Assert (d_ctx->getLevel() == 0); - delete d_satSolver; - delete d_satSolverNotify; - delete d_cnfStream; d_assertedAtoms->deleteSelf(); d_assertedAtoms = new(true) context::CDList(d_ctx); d_explanations->deleteSelf(); @@ -586,18 +584,18 @@ void TLazyBitblaster::clearSolver() { invalidateModelCache(); // recreate sat solver - d_satSolver = prop::SatSolverFactory::createMinisat( - d_ctx, smtStatisticsRegistry()); - d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_nullRegistrar, - d_nullContext); - - d_satSolverNotify = d_emptyNotify ? - (prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() : - (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, d_bv, - this); - d_satSolver->setNotify(d_satSolverNotify); -} - -} /* namespace CVC4::theory::bv */ -} /* namespace CVC4::theory */ -} /* namespace CVC4 */ + d_satSolver.reset( + prop::SatSolverFactory::createMinisat(d_ctx, smtStatisticsRegistry())); + d_cnfStream.reset(new prop::TseitinCnfStream( + d_satSolver.get(), d_nullRegistrar.get(), d_nullContext.get())); + d_satSolverNotify.reset( + d_emptyNotify + ? (prop::BVSatSolverInterface::Notify*)new MinisatEmptyNotify() + : (prop::BVSatSolverInterface::Notify*)new MinisatNotify( + d_cnfStream.get(), d_bv, this)); + d_satSolver->setNotify(d_satSolverNotify.get()); +} + +} // namespace bv +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/bv/bitblast/lazy_bitblaster.h b/src/theory/bv/bitblast/lazy_bitblaster.h new file mode 100644 index 000000000..97fef1e50 --- /dev/null +++ b/src/theory/bv/bitblast/lazy_bitblaster.h @@ -0,0 +1,181 @@ +/********************* */ +/*! \file lazy_bitblaster.h + ** \verbatim + ** Top contributors (to current version): + ** Liana Hadarean, Tim King, Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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 Bitblaster for the lazy bv solver. + ** + ** Bitblaster for the lazy bv solver. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H +#define __CVC4__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H + +#include "theory/bv/bitblast/bitblaster.h" + +#include "context/cdhashmap.h" +#include "context/cdlist.h" +#include "prop/cnf_stream.h" +#include "prop/registrar.h" +#include "prop/sat_solver.h" +#include "theory/bv/abstraction.h" + +namespace CVC4 { +namespace theory { +namespace bv { + +class TheoryBV; + +class TLazyBitblaster : public TBitblaster +{ + public: + void bbTerm(TNode node, Bits& bits) override; + void bbAtom(TNode node) override; + Node getBBAtom(TNode atom) const override; + void storeBBAtom(TNode atom, Node atom_bb) override; + void storeBBTerm(TNode node, const Bits& bits) override; + bool hasBBAtom(TNode atom) const override; + + TLazyBitblaster(context::Context* c, + TheoryBV* bv, + const std::string name = "", + bool emptyNotify = false); + ~TLazyBitblaster(); + /** + * Pushes the assumption literal associated with node to the SAT + * solver assumption queue. + * + * @param node assumption + * @param propagate run bcp or not + * + * @return false if a conflict detected + */ + bool assertToSat(TNode node, bool propagate = true); + bool propagate(); + bool solve(); + prop::SatValue solveWithBudget(unsigned long conflict_budget); + void getConflict(std::vector& conflict); + void explain(TNode atom, std::vector& explanation); + void setAbstraction(AbstractionModule* abs); + + theory::EqualityStatus getEqualityStatus(TNode a, TNode b); + + /** + * Adds a constant value for each bit-blasted variable in the model. + * + * @param m the model + * @param fullModel whether to create a "full model," i.e., add + * constants to equivalence classes that don't already have them + */ + bool collectModelInfo(TheoryModel* m, bool fullModel); + void setProofLog(BitVectorProof* bvp); + + typedef TNodeSet::const_iterator vars_iterator; + vars_iterator beginVars() { return d_variables.begin(); } + vars_iterator endVars() { return d_variables.end(); } + + /** + * Creates the bits corresponding to the variable (or non-bv term). + * + * @param var + */ + void makeVariable(TNode var, Bits& bits) override; + + bool isSharedTerm(TNode node); + uint64_t computeAtomWeight(TNode node, NodeSet& seen); + /** + * Deletes SatSolver and CnfCache, but maintains bit-blasting + * terms cache. + * + */ + void clearSolver(); + + private: + typedef std::vector Bits; + typedef context::CDList AssertionList; + typedef context::CDHashMap, + prop::SatLiteralHashFunction> + ExplanationMap; + /** This class gets callbacks from minisat on propagations */ + class MinisatNotify : public prop::BVSatSolverInterface::Notify + { + prop::CnfStream* d_cnf; + TheoryBV* d_bv; + TLazyBitblaster* d_lazyBB; + + public: + MinisatNotify(prop::CnfStream* cnf, TheoryBV* bv, TLazyBitblaster* lbv) + : d_cnf(cnf), d_bv(bv), d_lazyBB(lbv) + { + } + + bool notify(prop::SatLiteral lit) override; + void notify(prop::SatClause& clause) override; + void spendResource(unsigned amount) override; + void safePoint(unsigned amount) override; + }; + + TheoryBV* d_bv; + context::Context* d_ctx; + + std::unique_ptr d_nullRegistrar; + std::unique_ptr d_nullContext; + // sat solver used for bitblasting and associated CnfStream + std::unique_ptr d_satSolver; + std::unique_ptr d_satSolverNotify; + std::unique_ptr d_cnfStream; + + AssertionList* + d_assertedAtoms; /**< context dependent list storing the atoms + currently asserted by the DPLL SAT solver. */ + ExplanationMap* d_explanations; /**< context dependent list of explanations + for the propagated literals. Only used when + bvEagerPropagate option enabled. */ + TNodeSet d_variables; + TNodeSet d_bbAtoms; + AbstractionModule* d_abstraction; + bool d_emptyNotify; + + // The size of the fact queue when we most recently called solve() in the + // bit-vector SAT solver. This is the level at which we should have + // a full model in the bv SAT solver. + context::CDO d_fullModelAssertionLevel; + + void addAtom(TNode atom); + bool hasValue(TNode a); + Node getModelFromSatSolver(TNode a, bool fullModel) override; + + class Statistics + { + public: + IntStat d_numTermClauses, d_numAtomClauses; + IntStat d_numTerms, d_numAtoms; + IntStat d_numExplainedPropagations; + IntStat d_numBitblastingPropagations; + TimerStat d_bitblastTimer; + Statistics(const std::string& name); + ~Statistics(); + }; + std::string d_name; + + // NOTE: d_statistics is public since d_bitblastTimer needs to be initalized + // prior to calling bbAtom. As it is now, the timer can't be initialized + // in bbAtom since the method is called recursively and the timer would + // be initialized multiple times, which is not allowed. + public: + Statistics d_statistics; +}; + +} // namespace bv +} // namespace theory +} // namespace CVC4 +#endif // __CVC4__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h deleted file mode 100644 index 3bb701fdf..000000000 --- a/src/theory/bv/bitblaster_template.h +++ /dev/null @@ -1,508 +0,0 @@ -/********************* */ -/*! \file bitblaster_template.h - ** \verbatim - ** Top contributors (to current version): - ** Liana Hadarean, Tim King, Clark Barrett - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 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 Wrapper around the SAT solver used for bitblasting - ** - ** Wrapper around the SAT solver used for bitblasting. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__BITBLASTER_TEMPLATE_H -#define __CVC4__BITBLASTER_TEMPLATE_H - -#include -#include -#include - -#include "bitblast_strategies_template.h" -#include "context/cdhashmap.h" -#include "expr/node.h" -#include "prop/sat_solver.h" -#include "theory/theory_registrar.h" -#include "theory/valuation.h" -#include "util/resource_manager.h" - -class Abc_Obj_t_; -typedef Abc_Obj_t_ Abc_Obj_t; - -class Abc_Ntk_t_; -typedef Abc_Ntk_t_ Abc_Ntk_t; - -class Abc_Aig_t_; -typedef Abc_Aig_t_ Abc_Aig_t; - -class Cnf_Dat_t_; -typedef Cnf_Dat_t_ Cnf_Dat_t; - - -namespace CVC4 { -namespace prop { -class CnfStream; -class BVSatSolverInterface; -class NullRegistrar; -} - -namespace theory { -class OutputChannel; -class TheoryModel; - -namespace bv { - -class BitblastingRegistrar; - -typedef std::unordered_set NodeSet; -typedef std::unordered_set TNodeSet; - -class AbstractionModule; - -/** - * The Bitblaster that manages the mapping between Nodes - * and their bitwise definition - * - */ - -template -class TBitblaster { -protected: - typedef std::vector Bits; - typedef std::unordered_map TermDefMap; - typedef std::unordered_set TNodeSet; - typedef std::unordered_map ModelCache; - - typedef void (*TermBBStrategy) (TNode, Bits&, TBitblaster*); - typedef T (*AtomBBStrategy) (TNode, TBitblaster*); - - // caches and mappings - TermDefMap d_termCache; - ModelCache d_modelCache; - - BitVectorProof * d_bvp; - - void initAtomBBStrategies(); - void initTermBBStrategies(); -protected: - /// function tables for the various bitblasting strategies indexed by node kind - TermBBStrategy d_termBBStrategies[kind::LAST_KIND]; - AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND]; - virtual Node getModelFromSatSolver(TNode node, bool fullModel) = 0; -public: - TBitblaster(); - virtual ~TBitblaster() {} - virtual void bbAtom(TNode node) = 0; - virtual void bbTerm(TNode node, Bits& bits) = 0; - virtual void makeVariable(TNode node, Bits& bits) = 0; - virtual T getBBAtom(TNode atom) const = 0; - virtual bool hasBBAtom(TNode atom) const = 0; - virtual void storeBBAtom(TNode atom, T atom_bb) = 0; - - - bool hasBBTerm(TNode node) const; - void getBBTerm(TNode node, Bits& bits) const; - virtual void storeBBTerm(TNode term, const Bits& bits); - /** - * Return a constant representing the value of a in the model. - * If fullModel is true set unconstrained bits to 0. If not return - * NullNode() for a fully or partially unconstrained. - * - */ - Node getTermModel(TNode node, bool fullModel); - void invalidateModelCache(); -}; - - -class TheoryBV; - -class TLazyBitblaster : public TBitblaster { - typedef std::vector Bits; - typedef context::CDList AssertionList; - typedef context::CDHashMap , prop::SatLiteralHashFunction> ExplanationMap; - /** This class gets callbacks from minisat on propagations */ - class MinisatNotify : public prop::BVSatSolverInterface::Notify { - prop::CnfStream* d_cnf; - TheoryBV *d_bv; - TLazyBitblaster* d_lazyBB; - public: - MinisatNotify(prop::CnfStream* cnf, TheoryBV *bv, TLazyBitblaster* lbv) - : d_cnf(cnf) - , d_bv(bv) - , d_lazyBB(lbv) - {} - - bool notify(prop::SatLiteral lit) override; - void notify(prop::SatClause& clause) override; - void spendResource(unsigned amount) override; - void safePoint(unsigned amount) override; - }; - - TheoryBV *d_bv; - context::Context* d_ctx; - - prop::NullRegistrar* d_nullRegistrar; - context::Context* d_nullContext; - // sat solver used for bitblasting and associated CnfStream - prop::BVSatSolverInterface* d_satSolver; - prop::BVSatSolverInterface::Notify* d_satSolverNotify; - prop::CnfStream* d_cnfStream; - - AssertionList* d_assertedAtoms; /**< context dependent list storing the atoms - currently asserted by the DPLL SAT solver. */ - ExplanationMap* d_explanations; /**< context dependent list of explanations for the propagated literals. - Only used when bvEagerPropagate option enabled. */ - TNodeSet d_variables; - TNodeSet d_bbAtoms; - AbstractionModule* d_abstraction; - bool d_emptyNotify; - - // The size of the fact queue when we most recently called solve() in the - // bit-vector SAT solver. This is the level at which we should have - // a full model in the bv SAT solver. - context::CDO d_fullModelAssertionLevel; - - void addAtom(TNode atom); - bool hasValue(TNode a); - Node getModelFromSatSolver(TNode a, bool fullModel) override; - - public: - void bbTerm(TNode node, Bits& bits) override; - void bbAtom(TNode node) override; - Node getBBAtom(TNode atom) const override; - void storeBBAtom(TNode atom, Node atom_bb) override; - void storeBBTerm(TNode node, const Bits& bits) override; - bool hasBBAtom(TNode atom) const override; - - TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const std::string name="", bool emptyNotify = false); - ~TLazyBitblaster(); - /** - * Pushes the assumption literal associated with node to the SAT - * solver assumption queue. - * - * @param node assumption - * @param propagate run bcp or not - * - * @return false if a conflict detected - */ - bool assertToSat(TNode node, bool propagate = true); - bool propagate(); - bool solve(); - prop::SatValue solveWithBudget(unsigned long conflict_budget); - void getConflict(std::vector& conflict); - void explain(TNode atom, std::vector& explanation); - void setAbstraction(AbstractionModule* abs); - - theory::EqualityStatus getEqualityStatus(TNode a, TNode b); - - /** - * Adds a constant value for each bit-blasted variable in the model. - * - * @param m the model - * @param fullModel whether to create a "full model," i.e., add - * constants to equivalence classes that don't already have them - */ - bool collectModelInfo(TheoryModel* m, bool fullModel); - void setProofLog( BitVectorProof * bvp ); - - typedef TNodeSet::const_iterator vars_iterator; - vars_iterator beginVars() { return d_variables.begin(); } - vars_iterator endVars() { return d_variables.end(); } - - /** - * Creates the bits corresponding to the variable (or non-bv term). - * - * @param var - */ - void makeVariable(TNode var, Bits& bits) override; - - bool isSharedTerm(TNode node); - uint64_t computeAtomWeight(TNode node, NodeSet& seen); - /** - * Deletes SatSolver and CnfCache, but maintains bit-blasting - * terms cache. - * - */ - void clearSolver(); -private: - - class Statistics { - public: - IntStat d_numTermClauses, d_numAtomClauses; - IntStat d_numTerms, d_numAtoms; - IntStat d_numExplainedPropagations; - IntStat d_numBitblastingPropagations; - TimerStat d_bitblastTimer; - Statistics(const std::string& name); - ~Statistics(); - }; - std::string d_name; -public: - Statistics d_statistics; -}; - -class MinisatEmptyNotify : public prop::BVSatSolverInterface::Notify { -public: - MinisatEmptyNotify() {} - bool notify(prop::SatLiteral lit) override { return true; } - void notify(prop::SatClause& clause) override {} - void spendResource(unsigned amount) override - { - NodeManager::currentResourceManager()->spendResource(amount); - } - void safePoint(unsigned amount) override {} -}; - - -class EagerBitblaster : public TBitblaster { - typedef std::unordered_set TNodeSet; - // sat solver used for bitblasting and associated CnfStream - prop::SatSolver* d_satSolver; - BitblastingRegistrar* d_bitblastingRegistrar; - context::Context* d_nullContext; - prop::CnfStream* d_cnfStream; - - theory::bv::TheoryBV* d_bv; - TNodeSet d_bbAtoms; - TNodeSet d_variables; - - // This is either an MinisatEmptyNotify or NULL. - MinisatEmptyNotify* d_notify; - - Node getModelFromSatSolver(TNode a, bool fullModel) override; - bool isSharedTerm(TNode node); - -public: - EagerBitblaster(theory::bv::TheoryBV* theory_bv); - ~EagerBitblaster(); - - void addAtom(TNode atom); - void makeVariable(TNode node, Bits& bits) override; - void bbTerm(TNode node, Bits& bits) override; - void bbAtom(TNode node) override; - Node getBBAtom(TNode node) const override; - bool hasBBAtom(TNode atom) const override; - void bbFormula(TNode formula); - void storeBBAtom(TNode atom, Node atom_bb) override; - void storeBBTerm(TNode node, const Bits& bits) override; - - bool assertToSat(TNode node, bool propagate = true); - bool solve(); - bool collectModelInfo(TheoryModel* m, bool fullModel); - void setProofLog( BitVectorProof * bvp ); -}; - -class BitblastingRegistrar: public prop::Registrar { - EagerBitblaster* d_bitblaster; -public: - BitblastingRegistrar(EagerBitblaster* bb) - : d_bitblaster(bb) - {} - void preRegister(Node n) override; -}; /* class Registrar */ - -class AigBitblaster : public TBitblaster { - typedef std::unordered_map TNodeAigMap; - typedef std::unordered_map NodeAigMap; - - static Abc_Ntk_t* abcAigNetwork; - context::Context* d_nullContext; - prop::SatSolver* d_satSolver; - TNodeAigMap d_aigCache; - NodeAigMap d_bbAtoms; - - NodeAigMap d_nodeToAigInput; - // the thing we are checking for sat - Abc_Obj_t* d_aigOutputNode; - - void addAtom(TNode atom); - void simplifyAig(); - void storeBBAtom(TNode atom, Abc_Obj_t* atom_bb) override; - Abc_Obj_t* getBBAtom(TNode atom) const override; - bool hasBBAtom(TNode atom) const override; - void cacheAig(TNode node, Abc_Obj_t* aig); - bool hasAig(TNode node); - Abc_Obj_t* getAig(TNode node); - Abc_Obj_t* mkInput(TNode input); - bool hasInput(TNode input); - void convertToCnfAndAssert(); - void assertToSatSolver(Cnf_Dat_t* pCnf); - Node getModelFromSatSolver(TNode a, bool fullModel) override - { - Unreachable(); - } - - public: - AigBitblaster(); - ~AigBitblaster(); - - void makeVariable(TNode node, Bits& bits) override; - void bbTerm(TNode node, Bits& bits) override; - void bbAtom(TNode node) override; - Abc_Obj_t* bbFormula(TNode formula); - bool solve(TNode query); - static Abc_Aig_t* currentAigM(); - static Abc_Ntk_t* currentAigNtk(); - -private: - class Statistics { - public: - IntStat d_numClauses; - IntStat d_numVariables; - TimerStat d_simplificationTime; - TimerStat d_cnfConversionTime; - TimerStat d_solveTime; - Statistics(); - ~Statistics(); - }; - - Statistics d_statistics; - -}; - - -// Bitblaster implementation - -template void TBitblaster::initAtomBBStrategies() { - for (int i = 0 ; i < kind::LAST_KIND; ++i ) { - d_atomBBStrategies[i] = UndefinedAtomBBStrategy; - } - /// setting default bb strategies for atoms - d_atomBBStrategies [ kind::EQUAL ] = DefaultEqBB; - d_atomBBStrategies [ kind::BITVECTOR_ULT ] = DefaultUltBB; - d_atomBBStrategies [ kind::BITVECTOR_ULE ] = DefaultUleBB; - d_atomBBStrategies [ kind::BITVECTOR_UGT ] = DefaultUgtBB; - d_atomBBStrategies [ kind::BITVECTOR_UGE ] = DefaultUgeBB; - d_atomBBStrategies [ kind::BITVECTOR_SLT ] = DefaultSltBB; - d_atomBBStrategies [ kind::BITVECTOR_SLE ] = DefaultSleBB; - d_atomBBStrategies [ kind::BITVECTOR_SGT ] = DefaultSgtBB; - d_atomBBStrategies [ kind::BITVECTOR_SGE ] = DefaultSgeBB; -} - -template void TBitblaster::initTermBBStrategies() { - for (int i = 0 ; i < kind::LAST_KIND; ++i ) { - d_termBBStrategies[i] = DefaultVarBB; - } - /// setting default bb strategies for terms: - d_termBBStrategies [ kind::CONST_BITVECTOR ] = DefaultConstBB; - d_termBBStrategies [ kind::BITVECTOR_NOT ] = DefaultNotBB; - d_termBBStrategies [ kind::BITVECTOR_CONCAT ] = DefaultConcatBB; - d_termBBStrategies [ kind::BITVECTOR_AND ] = DefaultAndBB; - d_termBBStrategies [ kind::BITVECTOR_OR ] = DefaultOrBB; - d_termBBStrategies [ kind::BITVECTOR_XOR ] = DefaultXorBB; - d_termBBStrategies [ kind::BITVECTOR_XNOR ] = DefaultXnorBB; - d_termBBStrategies [ kind::BITVECTOR_NAND ] = DefaultNandBB; - d_termBBStrategies [ kind::BITVECTOR_NOR ] = DefaultNorBB; - d_termBBStrategies [ kind::BITVECTOR_COMP ] = DefaultCompBB; - d_termBBStrategies [ kind::BITVECTOR_MULT ] = DefaultMultBB; - d_termBBStrategies [ kind::BITVECTOR_PLUS ] = DefaultPlusBB; - d_termBBStrategies [ kind::BITVECTOR_SUB ] = DefaultSubBB; - d_termBBStrategies [ kind::BITVECTOR_NEG ] = DefaultNegBB; - d_termBBStrategies [ kind::BITVECTOR_UDIV ] = UndefinedTermBBStrategy; - d_termBBStrategies [ kind::BITVECTOR_UREM ] = UndefinedTermBBStrategy; - d_termBBStrategies [ kind::BITVECTOR_UDIV_TOTAL ] = DefaultUdivBB; - d_termBBStrategies [ kind::BITVECTOR_UREM_TOTAL ] = DefaultUremBB; - d_termBBStrategies [ kind::BITVECTOR_SDIV ] = UndefinedTermBBStrategy; - d_termBBStrategies [ kind::BITVECTOR_SREM ] = UndefinedTermBBStrategy; - d_termBBStrategies [ kind::BITVECTOR_SMOD ] = UndefinedTermBBStrategy; - d_termBBStrategies [ kind::BITVECTOR_SHL ] = DefaultShlBB; - d_termBBStrategies [ kind::BITVECTOR_LSHR ] = DefaultLshrBB; - d_termBBStrategies [ kind::BITVECTOR_ASHR ] = DefaultAshrBB; - d_termBBStrategies [ kind::BITVECTOR_ULTBV ] = DefaultUltbvBB; - d_termBBStrategies [ kind::BITVECTOR_SLTBV ] = DefaultSltbvBB; - d_termBBStrategies [ kind::BITVECTOR_ITE ] = DefaultIteBB; - d_termBBStrategies [ kind::BITVECTOR_EXTRACT ] = DefaultExtractBB; - d_termBBStrategies [ kind::BITVECTOR_REPEAT ] = DefaultRepeatBB; - d_termBBStrategies [ kind::BITVECTOR_ZERO_EXTEND ] = DefaultZeroExtendBB; - d_termBBStrategies [ kind::BITVECTOR_SIGN_EXTEND ] = DefaultSignExtendBB; - d_termBBStrategies [ kind::BITVECTOR_ROTATE_RIGHT ] = DefaultRotateRightBB; - d_termBBStrategies [ kind::BITVECTOR_ROTATE_LEFT ] = DefaultRotateLeftBB; -} - -template -TBitblaster::TBitblaster() - : d_termCache() - , d_modelCache() - , d_bvp( NULL ) -{ - initAtomBBStrategies(); - initTermBBStrategies(); -} - -template -bool TBitblaster::hasBBTerm(TNode node) const { - return d_termCache.find(node) != d_termCache.end(); -} -template -void TBitblaster::getBBTerm(TNode node, Bits& bits) const { - Assert (hasBBTerm(node)); - bits = d_termCache.find(node)->second; -} - -template -void TBitblaster::storeBBTerm(TNode node, const Bits& bits) { - d_termCache.insert(std::make_pair(node, bits)); -} - -template -void TBitblaster::invalidateModelCache() { - d_modelCache.clear(); -} - -template -Node TBitblaster::getTermModel(TNode node, bool fullModel) { - if (d_modelCache.find(node) != d_modelCache.end()) - return d_modelCache[node]; - - if (node.isConst()) - return node; - - Node value = getModelFromSatSolver(node, false); - if (!value.isNull()) { - Debug("bv-equality-status")<< "TLazyBitblaster::getTermModel from SatSolver" << node <<" => " << value <<"\n"; - d_modelCache[node] = value; - Assert (value.isConst()); - return value; - } - - if (Theory::isLeafOf(node, theory::THEORY_BV)) { - // if it is a leaf may ask for fullModel - value = getModelFromSatSolver(node, true); - Debug("bv-equality-status")<< "TLazyBitblaster::getTermModel from VarValue" << node <<" => " << value <<"\n"; - Assert ((fullModel && !value.isNull() && value.isConst()) || !fullModel); - if (!value.isNull()) { - d_modelCache[node] = value; - } - return value; - } - Assert (node.getType().isBitVector()); - - NodeBuilder<> nb(node.getKind()); - if (node.getMetaKind() == kind::metakind::PARAMETERIZED) { - nb << node.getOperator(); - } - - for (unsigned i = 0; i < node.getNumChildren(); ++i) { - nb << getTermModel(node[i], fullModel); - } - value = nb; - value = Rewriter::rewrite(value); - Assert (value.isConst()); - d_modelCache[node] = value; - Debug("bv-term-model")<< "TLazyBitblaster::getTermModel Building Value" << node <<" => " << value <<"\n"; - return value; -} - - -} /* bv namespace */ - -} /* theory namespace */ - -} /* CVC4 namespace */ - -#endif /* __CVC4__BITBLASTER_H */ diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp index 01282880c..f1af28d04 100644 --- a/src/theory/bv/bv_eager_solver.cpp +++ b/src/theory/bv/bv_eager_solver.cpp @@ -15,9 +15,11 @@ **/ #include "theory/bv/bv_eager_solver.h" + #include "options/bv_options.h" #include "proof/bitvector_proof.h" -#include "theory/bv/bitblaster_template.h" +#include "theory/bv/bitblast/aig_bitblaster.h" +#include "theory/bv/bitblast/eager_bitblaster.h" using namespace std; diff --git a/src/theory/bv/bv_quick_check.cpp b/src/theory/bv/bv_quick_check.cpp index 101b64173..44e87e368 100644 --- a/src/theory/bv/bv_quick_check.cpp +++ b/src/theory/bv/bv_quick_check.cpp @@ -17,7 +17,7 @@ #include "theory/bv/bv_quick_check.h" #include "smt/smt_statistics_registry.h" -#include "theory/bv/bitblaster_template.h" +#include "theory/bv/bitblast/lazy_bitblaster.h" #include "theory/bv/theory_bv_utils.h" using namespace CVC4::prop; diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index 902a4dbe0..cdbf2f955 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -14,18 +14,18 @@ ** Algebraic solver. **/ +#include "theory/bv/bv_subtheory_bitblast.h" #include "decision/decision_attributes.h" -#include "options/decision_options.h" #include "options/bv_options.h" +#include "options/decision_options.h" +#include "proof/bitvector_proof.h" +#include "proof/proof_manager.h" #include "smt/smt_statistics_registry.h" #include "theory/bv/abstraction.h" -#include "theory/bv/bitblaster_template.h" +#include "theory/bv/bitblast/lazy_bitblaster.h" #include "theory/bv/bv_quick_check.h" -#include "theory/bv/bv_subtheory_bitblast.h" #include "theory/bv/theory_bv.h" #include "theory/bv/theory_bv_utils.h" -#include "proof/proof_manager.h" -#include "proof/bitvector_proof.h" using namespace std; using namespace CVC4::context; diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h index 509e59b19..ca9f472c2 100644 --- a/src/theory/bv/bv_subtheory_bitblast.h +++ b/src/theory/bv/bv_subtheory_bitblast.h @@ -20,14 +20,13 @@ #include -#include "theory/bv/bitblaster_template.h" #include "theory/bv/bv_subtheory.h" namespace CVC4 { namespace theory { namespace bv { -class LazyBitblaster; +class TLazyBitblaster; class AbstractionModule; class BVQuickCheck; class QuickXPlain; diff --git a/test/unit/theory/theory_bv_white.h b/test/unit/theory/theory_bv_white.h index 5721957ec..a8ce0290b 100644 --- a/test/unit/theory/theory_bv_white.h +++ b/test/unit/theory/theory_bv_white.h @@ -22,7 +22,7 @@ #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "theory/bv/theory_bv.h" -#include "theory/bv/bitblaster_template.h" +#include "theory/bv/bitblast/eager_bitblaster.h" #include "expr/node.h" #include "expr/node_manager.h" #include "context/context.h" -- 2.30.2