From a917cc2ab4956b542b1f565abf0e62b197692f8d Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Mon, 2 Apr 2018 12:48:44 -0700 Subject: 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/theory/bv/aig_bitblaster.cpp | 488 ----------- src/theory/bv/bitblast/aig_bitblaster.cpp | 494 +++++++++++ src/theory/bv/bitblast/aig_bitblaster.h | 105 +++ .../bv/bitblast/bitblast_strategies_template.h | 911 +++++++++++++++++++++ src/theory/bv/bitblast/bitblast_utils.h | 272 ++++++ src/theory/bv/bitblast/bitblaster.h | 261 ++++++ src/theory/bv/bitblast/eager_bitblaster.cpp | 263 ++++++ src/theory/bv/bitblast/eager_bitblaster.h | 89 ++ src/theory/bv/bitblast/lazy_bitblaster.cpp | 601 ++++++++++++++ src/theory/bv/bitblast/lazy_bitblaster.h | 181 ++++ src/theory/bv/bitblast_strategies_template.h | 910 -------------------- src/theory/bv/bitblast_utils.h | 283 ------- 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 +- src/theory/bv/eager_bitblaster.cpp | 269 ------ src/theory/bv/lazy_bitblaster.cpp | 603 -------------- 19 files changed, 3187 insertions(+), 3070 deletions(-) delete mode 100644 src/theory/bv/aig_bitblaster.cpp create mode 100644 src/theory/bv/bitblast/aig_bitblaster.cpp create mode 100644 src/theory/bv/bitblast/aig_bitblaster.h create mode 100644 src/theory/bv/bitblast/bitblast_strategies_template.h create mode 100644 src/theory/bv/bitblast/bitblast_utils.h create mode 100644 src/theory/bv/bitblast/bitblaster.h create mode 100644 src/theory/bv/bitblast/eager_bitblaster.cpp create mode 100644 src/theory/bv/bitblast/eager_bitblaster.h create mode 100644 src/theory/bv/bitblast/lazy_bitblaster.cpp create mode 100644 src/theory/bv/bitblast/lazy_bitblaster.h delete mode 100644 src/theory/bv/bitblast_strategies_template.h delete mode 100644 src/theory/bv/bitblast_utils.h delete mode 100644 src/theory/bv/bitblaster_template.h delete mode 100644 src/theory/bv/eager_bitblaster.cpp delete mode 100644 src/theory/bv/lazy_bitblaster.cpp (limited to 'src/theory/bv') diff --git a/src/theory/bv/aig_bitblaster.cpp b/src/theory/bv/aig_bitblaster.cpp deleted file mode 100644 index 010eaf4e5..000000000 --- a/src/theory/bv/aig_bitblaster.cpp +++ /dev/null @@ -1,488 +0,0 @@ -/********************* */ -/*! \file aig_bitblaster.cpp - ** \verbatim - ** Top contributors (to current version): - ** Liana Hadarean, Andrew Reynolds, Tim King - ** 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 - ** - ** Bitblaster for the lazy bv solver. - **/ - -#include "bitblaster_template.h" - -#include "cvc4_private.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 ); -} - - -namespace CVC4 { -namespace theory { -namespace bv { - -template <> inline -std::string toString (const std::vector& bits) { - Unreachable("Don't know how to print AIG"); -} - - -template <> inline -Abc_Obj_t* mkTrue() { - return Abc_AigConst1(AigBitblaster::currentAigNtk()); -} - -template <> inline -Abc_Obj_t* mkFalse() { - return Abc_ObjNot(mkTrue()); -} - -template <> inline -Abc_Obj_t* mkNot(Abc_Obj_t* a) { - return Abc_ObjNot(a); -} - -template <> inline -Abc_Obj_t* mkOr(Abc_Obj_t* a, Abc_Obj_t* b) { - return Abc_AigOr(AigBitblaster::currentAigM(), a, b); -} - -template <> inline -Abc_Obj_t* mkOr(const std::vector& children) { - Assert (children.size()); - if (children.size() == 1) - return children[0]; - - Abc_Obj_t* result = children[0]; - for (unsigned i = 1; i < children.size(); ++i) { - result = Abc_AigOr(AigBitblaster::currentAigM(), result, children[i]); - } - return result; -} - - -template <> inline -Abc_Obj_t* mkAnd(Abc_Obj_t* a, Abc_Obj_t* b) { - return Abc_AigAnd(AigBitblaster::currentAigM(), a, b); -} - -template <> inline -Abc_Obj_t* mkAnd(const std::vector& children) { - Assert (children.size()); - if (children.size() == 1) - return children[0]; - - Abc_Obj_t* result = children[0]; - for (unsigned i = 1; i < children.size(); ++i) { - result = Abc_AigAnd(AigBitblaster::currentAigM(), result, children[i]); - } - return result; -} - -template <> inline -Abc_Obj_t* mkXor(Abc_Obj_t* a, Abc_Obj_t* b) { - return Abc_AigXor(AigBitblaster::currentAigM(), a, b); -} - -template <> inline -Abc_Obj_t* mkIff(Abc_Obj_t* a, Abc_Obj_t* b) { - return mkNot(mkXor(a, b)); -} - -template <> inline -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; - -Abc_Ntk_t* AigBitblaster::currentAigNtk() { - if (!AigBitblaster::abcAigNetwork) { - Abc_Start(); - abcAigNetwork = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1); - char pName[] = "CVC4::theory::bv::AigNetwork"; - abcAigNetwork->pName = Extra_UtilStrsav(pName); - } - - return abcAigNetwork; -} - - -Abc_Aig_t* AigBitblaster::currentAigM() { - return (Abc_Aig_t*)(currentAigNtk()->pManFunc); -} - -AigBitblaster::AigBitblaster() - : TBitblaster() - , 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"; - } -} - -AigBitblaster::~AigBitblaster() { - Assert (abcAigNetwork == NULL); - delete d_nullContext; -} - -Abc_Obj_t* AigBitblaster::bbFormula(TNode node) { - Assert (node.getType().isBoolean()); - Debug("bitvector-bitblast") << "AigBitblaster::bbFormula "<< node << "\n"; - - if (hasAig(node)) - return getAig(node); - - Abc_Obj_t* result = NULL; - - Debug("bitvector-aig") << "AigBitblaster::convertToAig " << node <<"\n"; - switch (node.getKind()) { - case kind::AND: - { - result = bbFormula(node[0]); - for (unsigned i = 1; i < node.getNumChildren(); ++i) { - Abc_Obj_t* child = bbFormula(node[i]); - result = mkAnd(result, child); - } - break; - } - case kind::OR: - { - result = bbFormula(node[0]); - for (unsigned i = 1; i < node.getNumChildren(); ++i) { - Abc_Obj_t* child = bbFormula(node[i]); - result = mkOr(result, child); - } - break; - } - case kind::XOR: - { - result = bbFormula(node[0]); - for (unsigned i = 1; i < node.getNumChildren(); ++i) { - Abc_Obj_t* child = bbFormula(node[i]); - result = mkXor(result, child); - } - break; - } - case kind::IMPLIES: - { - Assert (node.getNumChildren() == 2); - Abc_Obj_t* child1 = bbFormula(node[0]); - Abc_Obj_t* child2 = bbFormula(node[1]); - - result = mkOr(mkNot(child1), child2); - break; - } - case kind::ITE: - { - Assert (node.getNumChildren() == 3); - Abc_Obj_t* a = bbFormula(node[0]); - Abc_Obj_t* b = bbFormula(node[1]); - Abc_Obj_t* c = bbFormula(node[2]); - result = mkIte(a, b, c); - break; - } - case kind::NOT: - { - Abc_Obj_t* child1 = bbFormula(node[0]); - result = mkNot(child1); - break; - } - case kind::CONST_BOOLEAN: - { - result = node.getConst() ? mkTrue() : mkFalse(); - break; - } - case kind::EQUAL: - { - if( node[0].getType().isBoolean() ){ - Assert (node.getNumChildren() == 2); - Abc_Obj_t* child1 = bbFormula(node[0]); - Abc_Obj_t* child2 = bbFormula(node[1]); - - result = mkIff(child1, child2); - break; - } - //else, continue... - } - default: - if( node.isVar() ){ - result = mkInput(node); - }else{ - bbAtom(node); - result = getBBAtom(node); - } - } - - cacheAig(node, result); - Debug("bitvector-aig") << "AigBitblaster::bbFormula done " << node << " => " << result <<"\n"; - return result; -} - -void AigBitblaster::bbAtom(TNode node) { - if (hasBBAtom(node)) { - return; - } - - Debug("bitvector-bitblast") << "Bitblasting atom " << node <<"\n"; - - // the bitblasted definition of the atom - Node normalized = Rewriter::rewrite(node); - Abc_Obj_t* atom_bb = (d_atomBBStrategies[normalized.getKind()])(normalized, this); - storeBBAtom(node, atom_bb); - Debug("bitvector-bitblast") << "Done bitblasting atom " << node <<"\n"; -} - -void AigBitblaster::bbTerm(TNode node, Bits& bits) { - if (hasBBTerm(node)) { - getBBTerm(node, bits); - return; - } - Assert( node.getType().isBitVector() ); - - Debug("bitvector-bitblast") << "Bitblasting term " << node <<"\n"; - d_termBBStrategies[node.getKind()] (node, bits, this); - - Assert (bits.size() == utils::getSize(node)); - storeBBTerm(node, bits); -} - - -void AigBitblaster::cacheAig(TNode node, Abc_Obj_t* aig) { - Assert (!hasAig(node)); - d_aigCache.insert(std::make_pair(node, aig)); -} -bool AigBitblaster::hasAig(TNode node) { - return d_aigCache.find(node) != d_aigCache.end(); -} -Abc_Obj_t* AigBitblaster::getAig(TNode node) { - Assert(hasAig(node)); - Debug("bitvector-aig") << "AigSimplifer::getAig " << node << " => " << d_aigCache.find(node)->second <<"\n"; - return d_aigCache.find(node)->second; -} - -void AigBitblaster::makeVariable(TNode node, Bits& bits) { - - for (unsigned i = 0; i < utils::getSize(node); ++i) { - Node bit = utils::mkBitOf(node, i); - Abc_Obj_t* input = mkInput(bit); - cacheAig(bit, input); - bits.push_back(input); - } -} - -Abc_Obj_t* AigBitblaster::mkInput(TNode input) { - Assert (!hasInput(input)); - Assert(input.getKind() == kind::BITVECTOR_BITOF || - (input.getType().isBoolean() && input.isVar())); - Abc_Obj_t* aig_input = Abc_NtkCreatePi(currentAigNtk()); - // d_aigCache.insert(std::make_pair(input, aig_input)); - d_nodeToAigInput.insert(std::make_pair(input, aig_input)); - Debug("bitvector-aig") << "AigSimplifer::mkInput " << input << " " << aig_input <<"\n"; - return aig_input; -} - -bool AigBitblaster::hasInput(TNode input) { - return d_nodeToAigInput.find(input) != d_nodeToAigInput.end(); -} - -bool AigBitblaster::solve(TNode node) { - // setting output of network to be the query - Assert (d_aigOutputNode == NULL); - Abc_Obj_t* query = bbFormula(node); - d_aigOutputNode = Abc_NtkCreatePo(currentAigNtk()); - Abc_ObjAddFanin(d_aigOutputNode, query); - - simplifyAig(); - convertToCnfAndAssert(); - // no need to use abc anymore - - TimerStat::CodeTimer solveTimer(d_statistics.d_solveTime); - prop::SatValue result = d_satSolver->solve(); - - Assert (result != prop::SAT_VALUE_UNKNOWN); - return result == prop::SAT_VALUE_TRUE; -} - - -void addAliases(Abc_Frame_t* pAbc); - -void AigBitblaster::simplifyAig() { - TimerStat::CodeTimer simpTimer(d_statistics.d_simplificationTime); - - Abc_AigCleanup(currentAigM()); - Assert (Abc_NtkCheck(currentAigNtk())); - - const char* command = options::bitvectorAigSimplifications().c_str(); - Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame(); - Abc_FrameSetCurrentNetwork(pAbc, currentAigNtk()); - - addAliases(pAbc); - if ( Cmd_CommandExecute( pAbc, command ) ) { - fprintf( stdout, "Cannot execute command \"%s\".\n", command ); - exit(-1); - } - abcAigNetwork = Abc_FrameReadNtk(pAbc); -} - - -void AigBitblaster::convertToCnfAndAssert() { - TimerStat::CodeTimer cnfConversionTimer(d_statistics.d_cnfConversionTime); - - Aig_Man_t * pMan = NULL; - Cnf_Dat_t * pCnf = NULL; - Assert( Abc_NtkIsStrash(currentAigNtk()) ); - - // convert to the AIG manager - pMan = Abc_NtkToDar(currentAigNtk(), 0, 0 ); - Abc_Stop(); - - // // free old network - // Abc_NtkDelete(currentAigNtk()); - // abcAigNetwork = NULL; - - Assert (pMan != NULL); - Assert (Aig_ManCheck(pMan)); - pCnf = Cnf_DeriveFast( pMan, 0 ); - - assertToSatSolver(pCnf); - - Cnf_DataFree( pCnf ); - Cnf_ManFree(); - Aig_ManStop(pMan); -} - -void AigBitblaster::assertToSatSolver(Cnf_Dat_t* pCnf) { - unsigned numVariables = pCnf->nVars; - unsigned numClauses = pCnf->nClauses; - - d_statistics.d_numVariables += numVariables; - d_statistics.d_numClauses += numClauses; - - // create variables in the sat solver - std::vector sat_variables; - for (unsigned i = 0; i < numVariables; ++i) { - sat_variables.push_back(d_satSolver->newVar(false, false, false)); - } - - // construct clauses and add to sat solver - int * pLit, * pStop; - for (unsigned i = 0; i < numClauses; i++ ) { - prop::SatClause clause; - for (pLit = pCnf->pClauses[i], pStop = pCnf->pClauses[i+1]; pLit < pStop; pLit++ ) { - int int_lit = Cnf_Lit2Var(*pLit); - Assert (int_lit != 0); - unsigned index = int_lit < 0? -int_lit : int_lit; - Assert (index - 1 < sat_variables.size()); - prop::SatLiteral lit(sat_variables[index-1], int_lit < 0); - clause.push_back(lit); - } - d_satSolver->addClause(clause, false); - } -} - -void addAliases(Abc_Frame_t* pAbc) { - std::vector aliases; - aliases.push_back("alias b balance"); - aliases.push_back("alias rw rewrite"); - aliases.push_back("alias rwz rewrite -z"); - aliases.push_back("alias rf refactor"); - aliases.push_back("alias rfz refactor -z"); - aliases.push_back("alias re restructure"); - aliases.push_back("alias rez restructure -z"); - aliases.push_back("alias rs resub"); - aliases.push_back("alias rsz resub -z"); - aliases.push_back("alias rsk6 rs -K 6"); - aliases.push_back("alias rszk5 rsz -K 5"); - aliases.push_back("alias bl b -l"); - aliases.push_back("alias rwl rw -l"); - aliases.push_back("alias rwzl rwz -l"); - aliases.push_back("alias rwzl rwz -l"); - aliases.push_back("alias rfl rf -l"); - aliases.push_back("alias rfzl rfz -l"); - aliases.push_back("alias brw \"b; rw\""); - - for (unsigned i = 0; i < aliases.size(); ++i) { - if ( Cmd_CommandExecute( pAbc, aliases[i].c_str() ) ) { - fprintf( stdout, "Cannot execute command \"%s\".\n", aliases[i].c_str() ); - exit(-1); - } - } -} - -bool AigBitblaster::hasBBAtom(TNode atom) const { - return d_bbAtoms.find(atom) != d_bbAtoms.end(); -} - -void AigBitblaster::storeBBAtom(TNode atom, Abc_Obj_t* atom_bb) { - d_bbAtoms.insert(std::make_pair(atom, atom_bb)); -} - -Abc_Obj_t* AigBitblaster::getBBAtom(TNode atom) const { - Assert (hasBBAtom(atom)); - return d_bbAtoms.find(atom)->second; -} - -AigBitblaster::Statistics::Statistics() - : d_numClauses("theory::bv::AigBitblaster::numClauses", 0) - , d_numVariables("theory::bv::AigBitblaster::numVariables", 0) - , d_simplificationTime("theory::bv::AigBitblaster::simplificationTime") - , d_cnfConversionTime("theory::bv::AigBitblaster::cnfConversionTime") - , d_solveTime("theory::bv::AigBitblaster::solveTime") -{ - smtStatisticsRegistry()->registerStat(&d_numClauses); - smtStatisticsRegistry()->registerStat(&d_numVariables); - smtStatisticsRegistry()->registerStat(&d_simplificationTime); - smtStatisticsRegistry()->registerStat(&d_cnfConversionTime); - smtStatisticsRegistry()->registerStat(&d_solveTime); -} - -AigBitblaster::Statistics::~Statistics() { - smtStatisticsRegistry()->unregisterStat(&d_numClauses); - smtStatisticsRegistry()->unregisterStat(&d_numVariables); - smtStatisticsRegistry()->unregisterStat(&d_simplificationTime); - smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime); - smtStatisticsRegistry()->unregisterStat(&d_solveTime); -} -#endif // CVC4_USE_ABC diff --git a/src/theory/bv/bitblast/aig_bitblaster.cpp b/src/theory/bv/bitblast/aig_bitblaster.cpp new file mode 100644 index 000000000..7e666bcbf --- /dev/null +++ b/src/theory/bv/bitblast/aig_bitblaster.cpp @@ -0,0 +1,494 @@ +/********************* */ +/*! \file aig_bitblaster.cpp + ** \verbatim + ** Top contributors (to current version): + ** Liana Hadarean, Andrew Reynolds, Tim King + ** 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 AIG bitblaster. + ** + ** AIG bitblaster. + **/ + +#include "cvc4_private.h" + +#include "theory/bv/bitblast/aig_bitblaster.h" + +#include "base/cvc4_check.h" +#include "options/bv_options.h" +#include "prop/sat_solver_factory.h" +#include "smt/smt_statistics_registry.h" + +#ifdef CVC4_USE_ABC + +extern "C" { +#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 { +namespace bv { + +template <> inline +std::string toString (const std::vector& bits) { + Unreachable("Don't know how to print AIG"); +} + + +template <> inline +Abc_Obj_t* mkTrue() { + return Abc_AigConst1(AigBitblaster::currentAigNtk()); +} + +template <> inline +Abc_Obj_t* mkFalse() { + return Abc_ObjNot(mkTrue()); +} + +template <> inline +Abc_Obj_t* mkNot(Abc_Obj_t* a) { + return Abc_ObjNot(a); +} + +template <> inline +Abc_Obj_t* mkOr(Abc_Obj_t* a, Abc_Obj_t* b) { + return Abc_AigOr(AigBitblaster::currentAigM(), a, b); +} + +template <> inline +Abc_Obj_t* mkOr(const std::vector& children) { + Assert (children.size()); + if (children.size() == 1) + return children[0]; + + Abc_Obj_t* result = children[0]; + for (unsigned i = 1; i < children.size(); ++i) { + result = Abc_AigOr(AigBitblaster::currentAigM(), result, children[i]); + } + return result; +} + + +template <> inline +Abc_Obj_t* mkAnd(Abc_Obj_t* a, Abc_Obj_t* b) { + return Abc_AigAnd(AigBitblaster::currentAigM(), a, b); +} + +template <> inline +Abc_Obj_t* mkAnd(const std::vector& children) { + Assert (children.size()); + if (children.size() == 1) + return children[0]; + + Abc_Obj_t* result = children[0]; + for (unsigned i = 1; i < children.size(); ++i) { + result = Abc_AigAnd(AigBitblaster::currentAigM(), result, children[i]); + } + return result; +} + +template <> inline +Abc_Obj_t* mkXor(Abc_Obj_t* a, Abc_Obj_t* b) { + return Abc_AigXor(AigBitblaster::currentAigM(), a, b); +} + +template <> inline +Abc_Obj_t* mkIff(Abc_Obj_t* a, Abc_Obj_t* b) { + return mkNot(mkXor(a, b)); +} + +template <> inline +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_THREAD_LOCAL Abc_Ntk_t* AigBitblaster::s_abcAigNetwork = nullptr; + +Abc_Ntk_t* AigBitblaster::currentAigNtk() { + if (!AigBitblaster::s_abcAigNetwork) { + Abc_Start(); + s_abcAigNetwork = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1); + char pName[] = "CVC4::theory::bv::AigNetwork"; + s_abcAigNetwork->pName = Extra_UtilStrsav(pName); + } + + return s_abcAigNetwork; +} + + +Abc_Aig_t* AigBitblaster::currentAigM() { + return (Abc_Aig_t*)(currentAigNtk()->pManFunc); +} + +AigBitblaster::AigBitblaster() + : TBitblaster(), + d_nullContext(new context::Context()), + d_aigCache(), + d_bbAtoms(), + d_aigOutputNode(NULL) +{ + 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() {} + +Abc_Obj_t* AigBitblaster::bbFormula(TNode node) { + Assert (node.getType().isBoolean()); + Debug("bitvector-bitblast") << "AigBitblaster::bbFormula "<< node << "\n"; + + if (hasAig(node)) + return getAig(node); + + Abc_Obj_t* result = NULL; + + Debug("bitvector-aig") << "AigBitblaster::convertToAig " << node <<"\n"; + switch (node.getKind()) { + case kind::AND: + { + result = bbFormula(node[0]); + for (unsigned i = 1; i < node.getNumChildren(); ++i) { + Abc_Obj_t* child = bbFormula(node[i]); + result = mkAnd(result, child); + } + break; + } + case kind::OR: + { + result = bbFormula(node[0]); + for (unsigned i = 1; i < node.getNumChildren(); ++i) { + Abc_Obj_t* child = bbFormula(node[i]); + result = mkOr(result, child); + } + break; + } + case kind::XOR: + { + result = bbFormula(node[0]); + for (unsigned i = 1; i < node.getNumChildren(); ++i) { + Abc_Obj_t* child = bbFormula(node[i]); + result = mkXor(result, child); + } + break; + } + case kind::IMPLIES: + { + Assert (node.getNumChildren() == 2); + Abc_Obj_t* child1 = bbFormula(node[0]); + Abc_Obj_t* child2 = bbFormula(node[1]); + + result = mkOr(mkNot(child1), child2); + break; + } + case kind::ITE: + { + Assert (node.getNumChildren() == 3); + Abc_Obj_t* a = bbFormula(node[0]); + Abc_Obj_t* b = bbFormula(node[1]); + Abc_Obj_t* c = bbFormula(node[2]); + result = mkIte(a, b, c); + break; + } + case kind::NOT: + { + Abc_Obj_t* child1 = bbFormula(node[0]); + result = mkNot(child1); + break; + } + case kind::CONST_BOOLEAN: + { + result = node.getConst() ? mkTrue() : mkFalse(); + break; + } + case kind::EQUAL: + { + if( node[0].getType().isBoolean() ){ + Assert (node.getNumChildren() == 2); + Abc_Obj_t* child1 = bbFormula(node[0]); + Abc_Obj_t* child2 = bbFormula(node[1]); + + result = mkIff(child1, child2); + break; + } + //else, continue... + } + default: + if( node.isVar() ){ + result = mkInput(node); + }else{ + bbAtom(node); + result = getBBAtom(node); + } + } + + cacheAig(node, result); + Debug("bitvector-aig") << "AigBitblaster::bbFormula done " << node << " => " << result <<"\n"; + return result; +} + +void AigBitblaster::bbAtom(TNode node) { + if (hasBBAtom(node)) { + return; + } + + Debug("bitvector-bitblast") << "Bitblasting atom " << node <<"\n"; + + // the bitblasted definition of the atom + Node normalized = Rewriter::rewrite(node); + Abc_Obj_t* atom_bb = (d_atomBBStrategies[normalized.getKind()])(normalized, this); + storeBBAtom(node, atom_bb); + Debug("bitvector-bitblast") << "Done bitblasting atom " << node <<"\n"; +} + +void AigBitblaster::bbTerm(TNode node, Bits& bits) { + if (hasBBTerm(node)) { + getBBTerm(node, bits); + return; + } + Assert( node.getType().isBitVector() ); + + Debug("bitvector-bitblast") << "Bitblasting term " << node <<"\n"; + d_termBBStrategies[node.getKind()] (node, bits, this); + + Assert (bits.size() == utils::getSize(node)); + storeBBTerm(node, bits); +} + + +void AigBitblaster::cacheAig(TNode node, Abc_Obj_t* aig) { + Assert (!hasAig(node)); + d_aigCache.insert(std::make_pair(node, aig)); +} +bool AigBitblaster::hasAig(TNode node) { + return d_aigCache.find(node) != d_aigCache.end(); +} +Abc_Obj_t* AigBitblaster::getAig(TNode node) { + Assert(hasAig(node)); + Debug("bitvector-aig") << "AigSimplifer::getAig " << node << " => " << d_aigCache.find(node)->second <<"\n"; + return d_aigCache.find(node)->second; +} + +void AigBitblaster::makeVariable(TNode node, Bits& bits) { + + for (unsigned i = 0; i < utils::getSize(node); ++i) { + Node bit = utils::mkBitOf(node, i); + Abc_Obj_t* input = mkInput(bit); + cacheAig(bit, input); + bits.push_back(input); + } +} + +Abc_Obj_t* AigBitblaster::mkInput(TNode input) { + Assert (!hasInput(input)); + Assert(input.getKind() == kind::BITVECTOR_BITOF || + (input.getType().isBoolean() && input.isVar())); + Abc_Obj_t* aig_input = Abc_NtkCreatePi(currentAigNtk()); + // d_aigCache.insert(std::make_pair(input, aig_input)); + d_nodeToAigInput.insert(std::make_pair(input, aig_input)); + Debug("bitvector-aig") << "AigSimplifer::mkInput " << input << " " << aig_input <<"\n"; + return aig_input; +} + +bool AigBitblaster::hasInput(TNode input) { + return d_nodeToAigInput.find(input) != d_nodeToAigInput.end(); +} + +bool AigBitblaster::solve(TNode node) { + // setting output of network to be the query + Assert (d_aigOutputNode == NULL); + Abc_Obj_t* query = bbFormula(node); + d_aigOutputNode = Abc_NtkCreatePo(currentAigNtk()); + Abc_ObjAddFanin(d_aigOutputNode, query); + + simplifyAig(); + convertToCnfAndAssert(); + // no need to use abc anymore + + TimerStat::CodeTimer solveTimer(d_statistics.d_solveTime); + prop::SatValue result = d_satSolver->solve(); + + Assert (result != prop::SAT_VALUE_UNKNOWN); + return result == prop::SAT_VALUE_TRUE; +} + + +void addAliases(Abc_Frame_t* pAbc); + +void AigBitblaster::simplifyAig() { + TimerStat::CodeTimer simpTimer(d_statistics.d_simplificationTime); + + Abc_AigCleanup(currentAigM()); + Assert (Abc_NtkCheck(currentAigNtk())); + + const char* command = options::bitvectorAigSimplifications().c_str(); + Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame(); + Abc_FrameSetCurrentNetwork(pAbc, currentAigNtk()); + + addAliases(pAbc); + if ( Cmd_CommandExecute( pAbc, command ) ) { + fprintf( stdout, "Cannot execute command \"%s\".\n", command ); + exit(-1); + } + s_abcAigNetwork = Abc_FrameReadNtk(pAbc); +} + + +void AigBitblaster::convertToCnfAndAssert() { + TimerStat::CodeTimer cnfConversionTimer(d_statistics.d_cnfConversionTime); + + Aig_Man_t * pMan = NULL; + Cnf_Dat_t * pCnf = NULL; + Assert( Abc_NtkIsStrash(currentAigNtk()) ); + + // convert to the AIG manager + pMan = Abc_NtkToDar(currentAigNtk(), 0, 0 ); + Abc_Stop(); + + // // free old network + // Abc_NtkDelete(currentAigNtk()); + // s_abcAigNetwork = NULL; + + Assert (pMan != NULL); + Assert (Aig_ManCheck(pMan)); + pCnf = Cnf_DeriveFast( pMan, 0 ); + + assertToSatSolver(pCnf); + + Cnf_DataFree( pCnf ); + Cnf_ManFree(); + Aig_ManStop(pMan); +} + +void AigBitblaster::assertToSatSolver(Cnf_Dat_t* pCnf) { + unsigned numVariables = pCnf->nVars; + unsigned numClauses = pCnf->nClauses; + + d_statistics.d_numVariables += numVariables; + d_statistics.d_numClauses += numClauses; + + // create variables in the sat solver + std::vector sat_variables; + for (unsigned i = 0; i < numVariables; ++i) { + sat_variables.push_back(d_satSolver->newVar(false, false, false)); + } + + // construct clauses and add to sat solver + int * pLit, * pStop; + for (unsigned i = 0; i < numClauses; i++ ) { + prop::SatClause clause; + for (pLit = pCnf->pClauses[i], pStop = pCnf->pClauses[i+1]; pLit < pStop; pLit++ ) { + int int_lit = Cnf_Lit2Var(*pLit); + Assert (int_lit != 0); + unsigned index = int_lit < 0? -int_lit : int_lit; + Assert (index - 1 < sat_variables.size()); + prop::SatLiteral lit(sat_variables[index-1], int_lit < 0); + clause.push_back(lit); + } + d_satSolver->addClause(clause, false); + } +} + +void addAliases(Abc_Frame_t* pAbc) { + std::vector aliases; + aliases.push_back("alias b balance"); + aliases.push_back("alias rw rewrite"); + aliases.push_back("alias rwz rewrite -z"); + aliases.push_back("alias rf refactor"); + aliases.push_back("alias rfz refactor -z"); + aliases.push_back("alias re restructure"); + aliases.push_back("alias rez restructure -z"); + aliases.push_back("alias rs resub"); + aliases.push_back("alias rsz resub -z"); + aliases.push_back("alias rsk6 rs -K 6"); + aliases.push_back("alias rszk5 rsz -K 5"); + aliases.push_back("alias bl b -l"); + aliases.push_back("alias rwl rw -l"); + aliases.push_back("alias rwzl rwz -l"); + aliases.push_back("alias rwzl rwz -l"); + aliases.push_back("alias rfl rf -l"); + aliases.push_back("alias rfzl rfz -l"); + aliases.push_back("alias brw \"b; rw\""); + + for (unsigned i = 0; i < aliases.size(); ++i) { + if ( Cmd_CommandExecute( pAbc, aliases[i].c_str() ) ) { + fprintf( stdout, "Cannot execute command \"%s\".\n", aliases[i].c_str() ); + exit(-1); + } + } +} + +bool AigBitblaster::hasBBAtom(TNode atom) const { + return d_bbAtoms.find(atom) != d_bbAtoms.end(); +} + +void AigBitblaster::storeBBAtom(TNode atom, Abc_Obj_t* atom_bb) { + d_bbAtoms.insert(std::make_pair(atom, atom_bb)); +} + +Abc_Obj_t* AigBitblaster::getBBAtom(TNode atom) const { + Assert (hasBBAtom(atom)); + return d_bbAtoms.find(atom)->second; +} + +AigBitblaster::Statistics::Statistics() + : d_numClauses("theory::bv::AigBitblaster::numClauses", 0) + , d_numVariables("theory::bv::AigBitblaster::numVariables", 0) + , d_simplificationTime("theory::bv::AigBitblaster::simplificationTime") + , d_cnfConversionTime("theory::bv::AigBitblaster::cnfConversionTime") + , d_solveTime("theory::bv::AigBitblaster::solveTime") +{ + smtStatisticsRegistry()->registerStat(&d_numClauses); + smtStatisticsRegistry()->registerStat(&d_numVariables); + smtStatisticsRegistry()->registerStat(&d_simplificationTime); + smtStatisticsRegistry()->registerStat(&d_cnfConversionTime); + smtStatisticsRegistry()->registerStat(&d_solveTime); +} + +AigBitblaster::Statistics::~Statistics() { + smtStatisticsRegistry()->unregisterStat(&d_numClauses); + smtStatisticsRegistry()->unregisterStat(&d_numVariables); + smtStatisticsRegistry()->unregisterStat(&d_simplificationTime); + 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/bitblast_strategies_template.h b/src/theory/bv/bitblast/bitblast_strategies_template.h new file mode 100644 index 000000000..3c8b7bddc --- /dev/null +++ b/src/theory/bv/bitblast/bitblast_strategies_template.h @@ -0,0 +1,911 @@ +/********************* */ +/*! \file bitblast_strategies_template.h + ** \verbatim + ** Top contributors (to current version): + ** Liana Hadarean, Aina Niemetz, Clark Barrett + ** 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 Implementation of bitblasting functions for various operators. + ** + ** Implementation of bitblasting functions for various operators. + **/ + +#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 "expr/node.h" +#include "theory/bv/bitblast/bitblast_utils.h" +#include "theory/bv/theory_bv_utils.h" +#include "theory/rewriter.h" + +namespace CVC4 { + +namespace theory { +namespace bv { + +/** + * Default Atom Bitblasting strategies: + * + * @param node the atom to be bitblasted + * @param bb the bitblaster + */ + +template +T UndefinedAtomBBStrategy(TNode node, TBitblaster* bb) { + Debug("bitvector") << "TheoryBV::Bitblaster Undefined bitblasting strategy for kind: " + << node.getKind() << "\n"; + Unreachable(); +} + + +template +T DefaultEqBB(TNode node, TBitblaster* bb) { + Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; + + Assert(node.getKind() == kind::EQUAL); + std::vector lhs, rhs; + bb->bbTerm(node[0], lhs); + bb->bbTerm(node[1], rhs); + + Assert(lhs.size() == rhs.size()); + + std::vector bits_eq; + for (unsigned i = 0; i < lhs.size(); i++) { + T bit_eq = mkIff(lhs[i], rhs[i]); + bits_eq.push_back(bit_eq); + } + T bv_eq = mkAnd(bits_eq); + return bv_eq; +} + +template +T AdderUltBB(TNode node, TBitblaster* bb) { + Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; + Assert(node.getKind() == kind::BITVECTOR_ULT); + std::vector a, b; + bb->bbTerm(node[0], a); + bb->bbTerm(node[1], b); + Assert(a.size() == b.size()); + + // a < b <=> ~ (add(a, ~b, 1).carry_out) + std::vector not_b; + negateBits(b, not_b); + T carry = mkTrue(); + + for (unsigned i = 0 ; i < a.size(); ++i) { + carry = mkOr( mkAnd(a[i], not_b[i]), + mkAnd( mkXor(a[i], not_b[i]), + carry)); + } + return mkNot(carry); +} + + +template +T DefaultUltBB(TNode node, TBitblaster* bb) { + Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; + Assert(node.getKind() == kind::BITVECTOR_ULT); + std::vector a, b; + bb->bbTerm(node[0], a); + bb->bbTerm(node[1], b); + Assert(a.size() == b.size()); + + // construct bitwise comparison + T res = uLessThanBB(a, b, false); + return res; +} + +template +T DefaultUleBB(TNode node, TBitblaster* bb){ + Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; + Assert(node.getKind() == kind::BITVECTOR_ULE); + std::vector a, b; + + bb->bbTerm(node[0], a); + bb->bbTerm(node[1], b); + Assert(a.size() == b.size()); + // construct bitwise comparison + T res = uLessThanBB(a, b, true); + return res; +} + +template +T DefaultUgtBB(TNode node, TBitblaster* bb){ + Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; + // should be rewritten + Unimplemented(); +} +template +T DefaultUgeBB(TNode node, TBitblaster* bb){ + Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; + // should be rewritten + Unimplemented(); +} + +template +T DefaultSltBB(TNode node, TBitblaster* bb){ + Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; + + std::vector a, b; + bb->bbTerm(node[0], a); + bb->bbTerm(node[1], b); + Assert(a.size() == b.size()); + + T res = sLessThanBB(a, b, false); + return res; +} + +template +T DefaultSleBB(TNode node, TBitblaster* bb){ + Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; + + std::vector a, b; + bb->bbTerm(node[0], a); + bb->bbTerm(node[1], b); + Assert(a.size() == b.size()); + + T res = sLessThanBB(a, b, true); + return res; +} + +template +T DefaultSgtBB(TNode node, TBitblaster* bb){ + Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; + // should be rewritten + Unimplemented(); +} + +template +T DefaultSgeBB(TNode node, TBitblaster* bb){ + Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; + // should be rewritten + Unimplemented(); +} + + +/// Term bitblasting strategies + +/** + * Default Term Bitblasting strategies + * + * @param node the term to be bitblasted + * @param bits [output parameter] bits representing the new term + * @param bb the bitblaster in which the clauses are added + */ +template +void UndefinedTermBBStrategy(TNode node, std::vector& bits, TBitblaster* bb) { + Debug("bitvector") << "theory::bv:: Undefined bitblasting strategy for kind: " + << node.getKind() << "\n"; + Unreachable(); +} + +template +void DefaultVarBB (TNode node, std::vector& bits, TBitblaster* bb) { + Assert(bits.size() == 0); + bb->makeVariable(node, bits); + + if(Debug.isOn("bitvector-bb")) { + Debug("bitvector-bb") << "theory::bv::DefaultVarBB bitblasting " << node << "\n"; + Debug("bitvector-bb") << " with bits " << toString(bits); + } +} + +template +void DefaultConstBB (TNode node, std::vector& bits, TBitblaster* bb) { + Debug("bitvector-bb") << "theory::bv::DefaultConstBB bitblasting " << node << "\n"; + Assert(node.getKind() == kind::CONST_BITVECTOR); + Assert(bits.size() == 0); + + for (unsigned i = 0; i < utils::getSize(node); ++i) { + Integer bit = node.getConst().extract(i, i).getValue(); + if(bit == Integer(0)){ + bits.push_back(mkFalse()); + } else { + Assert (bit == Integer(1)); + bits.push_back(mkTrue()); + } + } + if(Debug.isOn("bitvector-bb")) { + Debug("bitvector-bb") << "with bits: " << toString(bits) << "\n"; + } +} + + +template +void DefaultNotBB (TNode node, std::vector& bits, TBitblaster* bb) { + Debug("bitvector-bb") << "theory::bv::DefaultNotBB bitblasting " << node << "\n"; + Assert(node.getKind() == kind::BITVECTOR_NOT); + Assert(bits.size() == 0); + std::vector bv; + bb->bbTerm(node[0], bv); + negateBits(bv, bits); +} + +template +void DefaultConcatBB (TNode node, std::vector& bits, TBitblaster* bb) { + Debug("bitvector-bb") << "theory::bv::DefaultConcatBB bitblasting " << node << "\n"; + Assert(bits.size() == 0); + + Assert (node.getKind() == kind::BITVECTOR_CONCAT); + for (int i = node.getNumChildren() -1 ; i >= 0; --i ) { + TNode current = node[i]; + std::vector current_bits; + bb->bbTerm(current, current_bits); + + for(unsigned j = 0; j < utils::getSize(current); ++j) { + bits.push_back(current_bits[j]); + } + } + Assert (bits.size() == utils::getSize(node)); + if(Debug.isOn("bitvector-bb")) { + Debug("bitvector-bb") << "with bits: " << toString(bits) << "\n"; + } +} + +template +void DefaultAndBB (TNode node, std::vector& bits, TBitblaster* bb) { + Debug("bitvector-bb") << "theory::bv::DefaultAndBB bitblasting " << node << "\n"; + + Assert(node.getKind() == kind::BITVECTOR_AND && + bits.size() == 0); + + bb->bbTerm(node[0], bits); + std::vector current; + for(unsigned j = 1; j < node.getNumChildren(); ++j) { + bb->bbTerm(node[j], current); + for (unsigned i = 0; i < utils::getSize(node); ++i) { + bits[i] = mkAnd(bits[i], current[i]); + } + current.clear(); + } + Assert (bits.size() == utils::getSize(node)); +} + +template +void DefaultOrBB (TNode node, std::vector& bits, TBitblaster* bb) { + Debug("bitvector-bb") << "theory::bv::DefaultOrBB bitblasting " << node << "\n"; + + Assert(node.getKind() == kind::BITVECTOR_OR && + bits.size() == 0); + + bb->bbTerm(node[0], bits); + std::vector current; + for(unsigned j = 1; j < node.getNumChildren(); ++j) { + bb->bbTerm(node[j], current); + for (unsigned i = 0; i < utils::getSize(node); ++i) { + bits[i] = mkOr(bits[i], current[i]); + } + current.clear(); + } + Assert (bits.size() == utils::getSize(node)); +} + +template +void DefaultXorBB (TNode node, std::vector& bits, TBitblaster* bb) { + Debug("bitvector-bb") << "theory::bv::DefaultXorBB bitblasting " << node << "\n"; + + Assert(node.getKind() == kind::BITVECTOR_XOR && + bits.size() == 0); + + bb->bbTerm(node[0], bits); + std::vector current; + for(unsigned j = 1; j < node.getNumChildren(); ++j) { + bb->bbTerm(node[j], current); + for (unsigned i = 0; i < utils::getSize(node); ++i) { + bits[i] = mkXor(bits[i], current[i]); + } + current.clear(); + } + Assert (bits.size() == utils::getSize(node)); +} + +template +void DefaultXnorBB (TNode node, std::vector& bits, TBitblaster* bb) { + Debug("bitvector-bb") << "theory::bv::DefaultXnorBB bitblasting " << node << "\n"; + + Assert(node.getNumChildren() == 2 && + node.getKind() == kind::BITVECTOR_XNOR && + bits.size() == 0); + std::vector lhs, rhs; + bb->bbTerm(node[0], lhs); + bb->bbTerm(node[1], rhs); + Assert(lhs.size() == rhs.size()); + + for (unsigned i = 0; i < lhs.size(); ++i) { + bits.push_back(mkIff(lhs[i], rhs[i])); + } +} + + +template +void DefaultNandBB (TNode node, std::vector& bits, TBitblaster* bb) { + Debug("bitvector") << "theory::bv:: Unimplemented kind " + << node.getKind() << "\n"; + Unimplemented(); +} +template +void DefaultNorBB (TNode node, std::vector& bits, TBitblaster* bb) { + Debug("bitvector") << "theory::bv:: Unimplemented kind " + << node.getKind() << "\n"; + Unimplemented(); +} +template +void DefaultCompBB (TNode node, std::vector& bits, TBitblaster* bb) { + Debug("bitvector") << "theory::bv:: DefaultCompBB bitblasting "<< node << "\n"; + + Assert(utils::getSize(node) == 1 && bits.size() == 0 && node.getKind() == kind::BITVECTOR_COMP); + std::vector a, b; + bb->bbTerm(node[0], a); + bb->bbTerm(node[1], b); + + std::vector bit_eqs; + for (unsigned i = 0; i < a.size(); ++i) { + T eq = mkIff(a[i], b[i]); + bit_eqs.push_back(eq); + } + T a_eq_b = mkAnd(bit_eqs); + bits.push_back(a_eq_b); +} + +template +void DefaultMultBB (TNode node, std::vector& res, TBitblaster* bb) { + Debug("bitvector") << "theory::bv:: DefaultMultBB bitblasting "<< node << "\n"; + Assert(res.size() == 0 && + node.getKind() == kind::BITVECTOR_MULT); + + // if (node.getNumChildren() == 2) { + // std::vector a; + // std::vector b; + // bb->bbTerm(node[0], a); + // bb->bbTerm(node[1], b); + // unsigned bw = utils::getSize(node); + // unsigned thresh = bw % 2 ? bw/2 : bw/2 - 1; + // bool no_overflow = true; + // for (unsigned i = thresh; i < bw; ++i) { + // if (a[i] != mkFalse || b[i] != mkFalse ) { + // no_overflow = false; + // } + // } + // if (no_overflow) { + // shiftAddMultiplier(); + // return; + // } + + // } + + std::vector newres; + bb->bbTerm(node[0], res); + for(unsigned i = 1; i < node.getNumChildren(); ++i) { + std::vector current; + bb->bbTerm(node[i], current); + newres.clear(); + // constructs a simple shift and add multiplier building the result + // in res + shiftAddMultiplier(res, current, newres); + res = newres; + } + if(Debug.isOn("bitvector-bb")) { + Debug("bitvector-bb") << "with bits: " << toString(res) << "\n"; + } +} + +template +void DefaultPlusBB (TNode node, std::vector& res, TBitblaster* bb) { + Debug("bitvector-bb") << "theory::bv::DefaultPlusBB bitblasting " << node << "\n"; + Assert(node.getKind() == kind::BITVECTOR_PLUS && + res.size() == 0); + + bb->bbTerm(node[0], res); + + std::vector newres; + + for(unsigned i = 1; i < node.getNumChildren(); ++i) { + std::vector current; + bb->bbTerm(node[i], current); + newres.clear(); + rippleCarryAdder(res, current, newres, mkFalse()); + res = newres; + } + + Assert(res.size() == utils::getSize(node)); +} + + +template +void DefaultSubBB (TNode node, std::vector& bits, TBitblaster* bb) { + Debug("bitvector-bb") << "theory::bv::DefaultSubBB bitblasting " << node << "\n"; + Assert(node.getKind() == kind::BITVECTOR_SUB && + node.getNumChildren() == 2 && + bits.size() == 0); + + std::vector a, b; + bb->bbTerm(node[0], a); + bb->bbTerm(node[1], b); + Assert(a.size() == b.size() && utils::getSize(node) == a.size()); + + // bvsub a b = adder(a, ~b, 1) + std::vector not_b; + negateBits(b, not_b); + rippleCarryAdder(a, not_b, bits, mkTrue()); +} + +template +void DefaultNegBB (TNode node, std::vector& bits, TBitblaster* bb) { + Debug("bitvector-bb") << "theory::bv::DefaultNegBB bitblasting " << node << "\n"; + Assert(node.getKind() == kind::BITVECTOR_NEG); + + std::vector a; + bb->bbTerm(node[0], a); + Assert(utils::getSize(node) == a.size()); + + // -a = add(~a, 0, 1). + std::vector not_a; + negateBits(a, not_a); + std::vector zero; + makeZero(zero, utils::getSize(node)); + + rippleCarryAdder(not_a, zero, bits, mkTrue()); +} + +template +void uDivModRec(const std::vector& a, const std::vector& b, std::vector& q, std::vector& r, unsigned rec_width) { + Assert( q.size() == 0 && r.size() == 0); + + if(rec_width == 0 || isZero(a)) { + makeZero(q, a.size()); + makeZero(r, a.size()); + return; + } + + std::vector q1, r1; + std::vector a1 = a; + rshift(a1, 1); + + uDivModRec(a1, b, q1, r1, rec_width - 1); + // shift the quotient and remainder (i.e. multiply by two) and add 1 to remainder if a is odd + lshift(q1, 1); + lshift(r1, 1); + + + T is_odd = mkIff(a[0], mkTrue()); + T one_if_odd = mkIte(is_odd, mkTrue(), mkFalse()); + + std::vector zero; + makeZero(zero, b.size()); + + std::vector r1_shift_add; + // account for a being odd + rippleCarryAdder(r1, zero, r1_shift_add, one_if_odd); + // now check if the remainder is greater than b + std::vector not_b; + negateBits(b, not_b); + std::vector r_minus_b; + T co1; + // use adder because we need r_minus_b anyway + co1 = rippleCarryAdder(r1_shift_add, not_b, r_minus_b, mkTrue()); + // sign is true if r1 < b + T sign = mkNot(co1); + + q1[0] = mkIte(sign, q1[0], mkTrue()); + + // would be nice to have a high level ITE instead of bitwise + for(unsigned i = 0; i < a.size(); ++i) { + r1_shift_add[i] = mkIte(sign, r1_shift_add[i], r_minus_b[i]); + } + + // check if a < b + + std::vector a_minus_b; + T co2 = rippleCarryAdder(a, not_b, a_minus_b, mkTrue()); + // Node a_lt_b = a_minus_b.back(); + T a_lt_b = mkNot(co2); + + for(unsigned i = 0; i < a.size(); ++i) { + T qval = mkIte(a_lt_b, mkFalse(), q1[i]); + T rval = mkIte(a_lt_b, a[i], r1_shift_add[i]); + q.push_back(qval); + r.push_back(rval); + } + +} + +template +void DefaultUdivBB(TNode node, std::vector& q, TBitblaster* bb) +{ + Debug("bitvector-bb") << "theory::bv::DefaultUdivBB bitblasting " << node + << "\n"; + Assert(node.getKind() == kind::BITVECTOR_UDIV_TOTAL && q.size() == 0); + + std::vector a, b; + bb->bbTerm(node[0], a); + bb->bbTerm(node[1], b); + + std::vector r; + uDivModRec(a, b, q, r, utils::getSize(node)); + // adding a special case for division by 0 + std::vector iszero; + for (unsigned i = 0; i < b.size(); ++i) + { + iszero.push_back(mkIff(b[i], mkFalse())); + } + T b_is_0 = mkAnd(iszero); + + for (unsigned i = 0; i < q.size(); ++i) + { + q[i] = mkIte(b_is_0, mkTrue(), q[i]); // a udiv 0 is 11..11 + r[i] = mkIte(b_is_0, a[i], r[i]); // a urem 0 is a + } + + // cache the remainder in case we need it later + Node remainder = Rewriter::rewrite(NodeManager::currentNM()->mkNode( + kind::BITVECTOR_UREM_TOTAL, node[0], node[1])); + bb->storeBBTerm(remainder, r); +} + +template +void DefaultUremBB(TNode node, std::vector& rem, TBitblaster* bb) +{ + Debug("bitvector-bb") << "theory::bv::DefaultUremBB bitblasting " << node + << "\n"; + Assert(node.getKind() == kind::BITVECTOR_UREM_TOTAL && rem.size() == 0); + + std::vector a, b; + bb->bbTerm(node[0], a); + bb->bbTerm(node[1], b); + + std::vector q; + uDivModRec(a, b, q, rem, utils::getSize(node)); + // adding a special case for division by 0 + std::vector iszero; + for (unsigned i = 0; i < b.size(); ++i) + { + iszero.push_back(mkIff(b[i], mkFalse())); + } + T b_is_0 = mkAnd(iszero); + + for (unsigned i = 0; i < q.size(); ++i) + { + q[i] = mkIte(b_is_0, mkTrue(), q[i]); // a udiv 0 is 11..11 + rem[i] = mkIte(b_is_0, a[i], rem[i]); // a urem 0 is a + } + + // cache the quotient in case we need it later + Node quotient = Rewriter::rewrite(NodeManager::currentNM()->mkNode( + kind::BITVECTOR_UDIV_TOTAL, node[0], node[1])); + bb->storeBBTerm(quotient, q); +} + +template +void DefaultSdivBB (TNode node, std::vector& bits, TBitblaster* bb) { + Debug("bitvector") << "theory::bv:: Unimplemented kind " + << node.getKind() << "\n"; + Unimplemented(); +} +template +void DefaultSremBB (TNode node, std::vector& bits, TBitblaster* bb) { + Debug("bitvector") << "theory::bv:: Unimplemented kind " + << node.getKind() << "\n"; + Unimplemented(); +} +template +void DefaultSmodBB (TNode node, std::vector& bits, TBitblaster* bb) { + Debug("bitvector") << "theory::bv:: Unimplemented kind " + << node.getKind() << "\n"; + Unimplemented(); +} + +template +void DefaultShlBB(TNode node, std::vector& res, TBitblaster* bb) +{ + Debug("bitvector-bb") << "theory::bv::DefaultShlBB bitblasting " << node + << "\n"; + Assert(node.getKind() == kind::BITVECTOR_SHL && res.size() == 0); + std::vector a, b; + bb->bbTerm(node[0], a); + bb->bbTerm(node[1], b); + + // check for b < log2(n) + unsigned size = utils::getSize(node); + unsigned log2_size = std::ceil(log2((double)size)); + Node a_size = utils::mkConst(size, size); + Node b_ult_a_size_node = Rewriter::rewrite( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULT, node[1], a_size)); + // ensure that the inequality is bit-blasted + bb->bbAtom(b_ult_a_size_node); + T b_ult_a_size = bb->getBBAtom(b_ult_a_size_node); + std::vector prev_res; + res = a; + // we only need to look at the bits bellow log2_a_size + for (unsigned s = 0; s < log2_size; ++s) + { + // barrel shift stage: at each stage you can either shift by 2^s bits + // or leave the previous stage untouched + prev_res = res; + unsigned threshold = pow(2, s); + for (unsigned i = 0; i < a.size(); ++i) + { + if (i < threshold) + { + // if b[s] is true then we must have shifted by at least 2^b bits so + // all bits bellow 2^s will be 0, otherwise just use previous shift + // value + res[i] = mkIte(b[s], mkFalse(), prev_res[i]); + } + else + { + // if b[s]= 0, use previous value, otherwise shift by threshold bits + Assert(i >= threshold); + res[i] = mkIte(b[s], prev_res[i - threshold], prev_res[i]); + } + } + } + prev_res = res; + for (unsigned i = 0; i < b.size(); ++i) + { + // this is fine because b_ult_a_size has been bit-blasted + res[i] = mkIte(b_ult_a_size, prev_res[i], mkFalse()); + } + + if (Debug.isOn("bitvector-bb")) + { + Debug("bitvector-bb") << "with bits: " << toString(res) << "\n"; + } +} + +template +void DefaultLshrBB(TNode node, std::vector& res, TBitblaster* bb) +{ + Debug("bitvector-bb") << "theory::bv::DefaultLshrBB bitblasting " << node + << "\n"; + Assert(node.getKind() == kind::BITVECTOR_LSHR && res.size() == 0); + std::vector a, b; + bb->bbTerm(node[0], a); + bb->bbTerm(node[1], b); + + // check for b < log2(n) + unsigned size = utils::getSize(node); + unsigned log2_size = std::ceil(log2((double)size)); + Node a_size = utils::mkConst(size, size); + Node b_ult_a_size_node = Rewriter::rewrite( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULT, node[1], a_size)); + // ensure that the inequality is bit-blasted + bb->bbAtom(b_ult_a_size_node); + T b_ult_a_size = bb->getBBAtom(b_ult_a_size_node); + res = a; + std::vector prev_res; + + for (unsigned s = 0; s < log2_size; ++s) + { + // barrel shift stage: at each stage you can either shift by 2^s bits + // or leave the previous stage untouched + prev_res = res; + int threshold = pow(2, s); + for (unsigned i = 0; i < a.size(); ++i) + { + if (i + threshold >= a.size()) + { + // if b[s] is true then we must have shifted by at least 2^b bits so + // all bits above 2^s will be 0, otherwise just use previous shift value + res[i] = mkIte(b[s], mkFalse(), prev_res[i]); + } + else + { + // if b[s]= 0, use previous value, otherwise shift by threshold bits + Assert(i + threshold < a.size()); + res[i] = mkIte(mkNot(b[s]), prev_res[i], prev_res[i + threshold]); + } + } + } + + prev_res = res; + for (unsigned i = 0; i < b.size(); ++i) + { + // this is fine because b_ult_a_size has been bit-blasted + res[i] = mkIte(b_ult_a_size, prev_res[i], mkFalse()); + } + + if (Debug.isOn("bitvector-bb")) + { + Debug("bitvector-bb") << "with bits: " << toString(res) << "\n"; + } +} + +template +void DefaultAshrBB(TNode node, std::vector& res, TBitblaster* bb) +{ + Debug("bitvector-bb") << "theory::bv::DefaultAshrBB bitblasting " << node + << "\n"; + Assert(node.getKind() == kind::BITVECTOR_ASHR && res.size() == 0); + std::vector a, b; + bb->bbTerm(node[0], a); + bb->bbTerm(node[1], b); + + // check for b < n + unsigned size = utils::getSize(node); + unsigned log2_size = std::ceil(log2((double)size)); + Node a_size = utils::mkConst(size, size); + Node b_ult_a_size_node = Rewriter::rewrite( + NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULT, node[1], a_size)); + // ensure that the inequality is bit-blasted + bb->bbAtom(b_ult_a_size_node); + T b_ult_a_size = bb->getBBAtom(b_ult_a_size_node); + + res = a; + T sign_bit = a.back(); + std::vector prev_res; + + for (unsigned s = 0; s < log2_size; ++s) + { + // barrel shift stage: at each stage you can either shift by 2^s bits + // or leave the previous stage untouched + prev_res = res; + int threshold = pow(2, s); + for (unsigned i = 0; i < a.size(); ++i) + { + if (i + threshold >= a.size()) + { + // if b[s] is true then we must have shifted by at least 2^b bits so + // all bits above 2^s will be the sign bit, otherwise just use previous + // shift value + res[i] = mkIte(b[s], sign_bit, prev_res[i]); + } + else + { + // if b[s]= 0, use previous value, otherwise shift by threshold bits + Assert(i + threshold < a.size()); + res[i] = mkIte(mkNot(b[s]), prev_res[i], prev_res[i + threshold]); + } + } + } + + prev_res = res; + for (unsigned i = 0; i < b.size(); ++i) + { + // this is fine because b_ult_a_size has been bit-blasted + res[i] = mkIte(b_ult_a_size, prev_res[i], sign_bit); + } + + if (Debug.isOn("bitvector-bb")) + { + Debug("bitvector-bb") << "with bits: " << toString(res) << "\n"; + } +} + +template +void DefaultUltbvBB (TNode node, std::vector& res, TBitblaster* bb) { + Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; + Assert(node.getKind() == kind::BITVECTOR_ULTBV); + std::vector a, b; + bb->bbTerm(node[0], a); + bb->bbTerm(node[1], b); + Assert(a.size() == b.size()); + + // construct bitwise comparison + res.push_back(uLessThanBB(a, b, false)); +} + +template +void DefaultSltbvBB (TNode node, std::vector& res, TBitblaster* bb) { + Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; + Assert(node.getKind() == kind::BITVECTOR_SLTBV); + std::vector a, b; + bb->bbTerm(node[0], a); + bb->bbTerm(node[1], b); + Assert(a.size() == b.size()); + + // construct bitwise comparison + res.push_back(sLessThanBB(a, b, false)); +} + +template +void DefaultIteBB (TNode node, std::vector& res, TBitblaster* bb) { + Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; + Assert(node.getKind() == kind::BITVECTOR_ITE); + std::vector cond, thenpart, elsepart; + bb->bbTerm(node[0], cond); + bb->bbTerm(node[1], thenpart); + bb->bbTerm(node[2], elsepart); + + Assert(cond.size() == 1); + Assert(thenpart.size() == elsepart.size()); + + for (unsigned i = 0; i < thenpart.size(); ++i) { + // (~cond OR thenpart) AND (cond OR elsepart) + res.push_back(mkAnd(mkOr(mkNot(cond[0]),thenpart[i]),mkOr(cond[0],elsepart[i]))); + } +} + +template +void DefaultExtractBB (TNode node, std::vector& bits, TBitblaster* bb) { + Assert (node.getKind() == kind::BITVECTOR_EXTRACT); + Assert(bits.size() == 0); + + std::vector base_bits; + bb->bbTerm(node[0], base_bits); + unsigned high = utils::getExtractHigh(node); + unsigned low = utils::getExtractLow(node); + + for (unsigned i = low; i <= high; ++i) { + bits.push_back(base_bits[i]); + } + Assert (bits.size() == high - low + 1); + + if(Debug.isOn("bitvector-bb")) { + Debug("bitvector-bb") << "theory::bv::DefaultExtractBB bitblasting " << node << "\n"; + Debug("bitvector-bb") << " with bits " << toString(bits); + } +} + + +template +void DefaultRepeatBB (TNode node, std::vector& bits, TBitblaster* bb) { + Debug("bitvector") << "theory::bv:: Unimplemented kind " + << node.getKind() << "\n"; + // this should be rewritten + Unimplemented(); +} + +template +void DefaultZeroExtendBB (TNode node, std::vector& res_bits, TBitblaster* bb) { + + Debug("bitvector-bb") << "theory::bv::DefaultZeroExtendBB bitblasting " << node << "\n"; + + // this should be rewritten + Unimplemented(); + +} + +template +void DefaultSignExtendBB (TNode node, std::vector& res_bits, TBitblaster* bb) { + Debug("bitvector-bb") << "theory::bv::DefaultSignExtendBB bitblasting " << node << "\n"; + + Assert (node.getKind() == kind::BITVECTOR_SIGN_EXTEND && + res_bits.size() == 0); + + std::vector bits; + bb->bbTerm(node[0], bits); + + T sign_bit = bits.back(); + unsigned amount = node.getOperator().getConst().signExtendAmount; + + for (unsigned i = 0; i < bits.size(); ++i ) { + res_bits.push_back(bits[i]); + } + + for (unsigned i = 0 ; i < amount ; ++i ) { + res_bits.push_back(sign_bit); + } + + Assert (res_bits.size() == amount + bits.size()); +} + +template +void DefaultRotateRightBB (TNode node, std::vector& res, TBitblaster* bb) { + Debug("bitvector") << "theory::bv:: Unimplemented kind " + << node.getKind() << "\n"; + + Unimplemented(); +} + +template +void DefaultRotateLeftBB (TNode node, std::vector& bits, TBitblaster* bb) { + Debug("bitvector") << "theory::bv:: Unimplemented kind " + << node.getKind() << "\n"; + Unimplemented(); +} + + +} +} +} + +#endif diff --git a/src/theory/bv/bitblast/bitblast_utils.h b/src/theory/bv/bitblast/bitblast_utils.h new file mode 100644 index 000000000..a2991c529 --- /dev/null +++ b/src/theory/bv/bitblast/bitblast_utils.h @@ -0,0 +1,272 @@ +/********************* */ +/*! \file bitblast_utils.h + ** \verbatim + ** Top contributors (to current version): + ** Liana Hadarean, Paul Meng, Andrew Reynolds + ** 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 Various utility functions for bit-blasting. + ** + ** Various utility functions for bit-blasting. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__BV__BITBLAST__BITBLAST_UTILS_H +#define __CVC4__THEORY__BV__BITBLAST__BITBLAST_UTILS_H + + +#include +#include "expr/node.h" + +namespace CVC4 { +namespace theory { +namespace bv { + +template class TBitblaster; + +template +std::string toString (const std::vector& bits); + +template <> inline +std::string toString (const std::vector& bits) { + std::ostringstream os; + for (int i = bits.size() - 1; i >= 0; --i) { + TNode bit = bits[i]; + if (bit.getKind() == kind::CONST_BOOLEAN) { + os << (bit.getConst() ? "1" : "0"); + } else { + os << bit<< " "; + } + } + os <<"\n"; + return os.str(); +} + +template T mkTrue(); +template T mkFalse(); +template T mkNot(T a); +template T mkOr(T a, T b); +template T mkOr(const std::vector& a); +template T mkAnd(T a, T b); +template T mkAnd(const std::vector& a); +template T mkXor(T a, T b); +template T mkIff(T a, T b); +template T mkIte(T cond, T a, T b); + + +template <> inline +Node mkTrue() { + return NodeManager::currentNM()->mkConst(true); +} + +template <> inline +Node mkFalse() { + return NodeManager::currentNM()->mkConst(false); +} + +template <> inline +Node mkNot(Node a) { + return NodeManager::currentNM()->mkNode(kind::NOT, a); +} + +template <> inline +Node mkOr(Node a, Node b) { + return NodeManager::currentNM()->mkNode(kind::OR, a, b); +} + +template <> inline +Node mkOr(const std::vector& children) { + Assert (children.size()); + if (children.size() == 1) + return children[0]; + return NodeManager::currentNM()->mkNode(kind::OR, children); +} + + +template <> inline +Node mkAnd(Node a, Node b) { + return NodeManager::currentNM()->mkNode(kind::AND, a, b); +} + +template <> inline +Node mkAnd(const std::vector& children) { + Assert (children.size()); + if (children.size() == 1) + return children[0]; + return NodeManager::currentNM()->mkNode(kind::AND, children); +} + + +template <> inline +Node mkXor(Node a, Node b) { + return NodeManager::currentNM()->mkNode(kind::XOR, a, b); +} + +template <> inline +Node mkIff(Node a, Node b) { + return NodeManager::currentNM()->mkNode(kind::EQUAL, a, b); +} + +template <> inline +Node mkIte(Node cond, Node a, Node b) { + return NodeManager::currentNM()->mkNode(kind::ITE, cond, a, b); +} + +/* + Various helper functions that get called by the bitblasting procedures + */ + +template +void inline extractBits(const std::vector& b, std::vector& dest, unsigned lo, unsigned hi) { + Assert ( lo < b.size() && hi < b.size() && lo <= hi); + for (unsigned i = lo; i <= hi; ++i) { + dest.push_back(b[i]); + } +} + +template +void inline negateBits(const std::vector& bits, std::vector& negated_bits) { + for(unsigned i = 0; i < bits.size(); ++i) { + negated_bits.push_back(mkNot(bits[i])); + } +} + +template +bool inline isZero(const std::vector& bits) { + for(unsigned i = 0; i < bits.size(); ++i) { + if(bits[i] != mkFalse()) { + return false; + } + } + return true; +} + +template +void inline rshift(std::vector& bits, unsigned amount) { + for (unsigned i = 0; i < bits.size() - amount; ++i) { + bits[i] = bits[i+amount]; + } + for(unsigned i = bits.size() - amount; i < bits.size(); ++i) { + bits[i] = mkFalse(); + } +} + +template +void inline lshift(std::vector& bits, unsigned amount) { + for (int i = (int)bits.size() - 1; i >= (int)amount ; --i) { + bits[i] = bits[i-amount]; + } + for(unsigned i = 0; i < amount; ++i) { + bits[i] = mkFalse(); + } +} + +template +void inline makeZero(std::vector& bits, unsigned width) { + Assert(bits.size() == 0); + for(unsigned i = 0; i < width; ++i) { + bits.push_back(mkFalse()); + } +} + + +/** + * Constructs a simple ripple carry adder + * + * @param a first term to be added + * @param b second term to be added + * @param res the result + * @param carry the carry-in bit + * + * @return the carry-out + */ +template +T inline rippleCarryAdder(const std::vector&a, const std::vector& b, std::vector& res, T carry) { + Assert(a.size() == b.size() && res.size() == 0); + + for (unsigned i = 0 ; i < a.size(); ++i) { + T sum = mkXor(mkXor(a[i], b[i]), carry); + carry = mkOr( mkAnd(a[i], b[i]), + mkAnd( mkXor(a[i], b[i]), + carry)); + res.push_back(sum); + } + + return carry; +} + +template +inline void shiftAddMultiplier(const std::vector&a, const std::vector&b, std::vector& res) { + + for (unsigned i = 0; i < a.size(); ++i) { + res.push_back(mkAnd(b[0], a[i])); + } + + for(unsigned k = 1; k < res.size(); ++k) { + T carry_in = mkFalse(); + T carry_out; + for(unsigned j = 0; j < res.size() -k; ++j) { + T aj = mkAnd(b[k], a[j]); + carry_out = mkOr(mkAnd(res[j+k], aj), + mkAnd( mkXor(res[j+k], aj), carry_in)); + res[j+k] = mkXor(mkXor(res[j+k], aj), carry_in); + carry_in = carry_out; + } + } +} + +template +T inline uLessThanBB(const std::vector&a, const std::vector& b, bool orEqual) { + Assert (a.size() && b.size()); + + T res = mkAnd(mkNot(a[0]), b[0]); + + if(orEqual) { + res = mkOr(res, mkIff(a[0], b[0])); + } + + for (unsigned i = 1; i < a.size(); ++i) { + // a < b iff ( a[i] <-> b[i] AND a[i-1:0] < b[i-1:0]) OR (~a[i] AND b[i]) + res = mkOr(mkAnd(mkIff(a[i], b[i]), res), + mkAnd(mkNot(a[i]), b[i])); + } + return res; +} + +template +T inline sLessThanBB(const std::vector&a, const std::vector& b, bool orEqual) { + Assert (a.size() && b.size()); + if (a.size() == 1) { + if(orEqual) { + return mkOr(mkIff(a[0], b[0]), + mkAnd(a[0], mkNot(b[0]))); + } + + return mkAnd(a[0], mkNot(b[0])); + } + unsigned n = a.size() - 1; + std::vector a1, b1; + extractBits(a, a1, 0, n-1); + extractBits(b, b1, 0, n-1); + + // unsigned comparison of the first n-1 bits + T ures = uLessThanBB(a1, b1, orEqual); + T res = mkOr(// a b have the same sign + mkAnd(mkIff(a[n], b[n]), + ures), + // a is negative and b positive + mkAnd(a[n], + mkNot(b[n]))); + return res; +} + +} // namespace bv +} // namespace theory +} // namespace CVC4 + +#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/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp new file mode 100644 index 000000000..d49c1f432 --- /dev/null +++ b/src/theory/bv/bitblast/eager_bitblaster.cpp @@ -0,0 +1,263 @@ +/********************* */ +/*! \file eager_bitblaster.cpp + ** \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 eager bv solver. + **/ + +#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/theory_bv.h" +#include "theory/theory_model.h" + +namespace CVC4 { +namespace theory { +namespace bv { + +EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv) + : TBitblaster(), + d_satSolver(), + d_bitblastingRegistrar(new BitblastingRegistrar(this)), + d_nullContext(new context::Context()), + d_cnfStream(), + d_bv(theory_bv), + d_bbAtoms(), + d_variables(), + d_notify() +{ + prop::SatSolver *solver = nullptr; + switch (options::bvSatSolver()) + { + case SAT_SOLVER_MINISAT: + { + prop::BVSatSolverInterface* minisat = + prop::SatSolverFactory::createMinisat( + d_nullContext.get(), smtStatisticsRegistry(), "EagerBitblaster"); + d_notify.reset(new MinisatEmptyNotify()); + minisat->setNotify(d_notify.get()); + solver = minisat; + break; + } + case SAT_SOLVER_CADICAL: + solver = prop::SatSolverFactory::createCadical(smtStatisticsRegistry(), + "EagerBitblaster"); + break; + case SAT_SOLVER_CRYPTOMINISAT: + solver = prop::SatSolverFactory::createCryptoMinisat( + smtStatisticsRegistry(), "EagerBitblaster"); + break; + default: Unreachable("Unknown SAT solver type"); + } + d_satSolver.reset(solver); + d_cnfStream.reset( + new prop::TseitinCnfStream(d_satSolver.get(), + d_bitblastingRegistrar.get(), + d_nullContext.get(), + options::proof(), + "EagerBitblaster")); +} + +EagerBitblaster::~EagerBitblaster() {} + +void EagerBitblaster::bbFormula(TNode node) { + d_cnfStream->convertAndAssert(node, false, false, RULE_INVALID, + TNode::null()); +} + +/** + * Bitblasts the atom, assigns it a marker literal, adding it to the SAT solver + * NOTE: duplicate clauses are not detected because of marker literal + * @param node the atom to be bitblasted + * + */ +void EagerBitblaster::bbAtom(TNode node) +{ + node = node.getKind() == kind::NOT ? node[0] : node; + if (node.getKind() == kind::BITVECTOR_BITOF) return; + if (hasBBAtom(node)) + { + return; + } + + Debug("bitvector-bitblast") << "Bitblasting node " << node << "\n"; + + // the bitblasted definition of the atom + Node normalized = Rewriter::rewrite(node); + Node atom_bb = + normalized.getKind() != kind::CONST_BOOLEAN + ? d_atomBBStrategies[normalized.getKind()](normalized, this) + : normalized; + + if (!options::proof()) + { + atom_bb = Rewriter::rewrite(atom_bb); + } + + // asserting that the atom is true iff the definition holds + Node atom_definition = + NodeManager::currentNM()->mkNode(kind::EQUAL, node, atom_bb); + + AlwaysAssert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER); + storeBBAtom(node, atom_bb); + d_cnfStream->convertAndAssert( + atom_definition, false, false, RULE_INVALID, TNode::null()); +} + +void EagerBitblaster::storeBBAtom(TNode atom, Node atom_bb) { + if (d_bvp) { + d_bvp->registerAtomBB(atom.toExpr(), atom_bb.toExpr()); + } + d_bbAtoms.insert(atom); +} + +void EagerBitblaster::storeBBTerm(TNode node, const Bits& bits) { + if (d_bvp) { + d_bvp->registerTermBB(node.toExpr()); + } + d_termCache.insert(std::make_pair(node, bits)); +} + +bool EagerBitblaster::hasBBAtom(TNode atom) const { + return d_bbAtoms.find(atom) != d_bbAtoms.end(); +} + +void EagerBitblaster::bbTerm(TNode node, Bits& bits) { + Assert(node.getType().isBitVector()); + + if (hasBBTerm(node)) { + getBBTerm(node, bits); + return; + } + + d_bv->spendResource(options::bitblastStep()); + Debug("bitvector-bitblast") << "Bitblasting node " << node << "\n"; + + d_termBBStrategies[node.getKind()](node, bits, this); + + Assert(bits.size() == utils::getSize(node)); + + storeBBTerm(node, bits); +} + +void EagerBitblaster::makeVariable(TNode var, Bits& bits) { + Assert(bits.size() == 0); + for (unsigned i = 0; i < utils::getSize(var); ++i) { + bits.push_back(utils::mkBitOf(var, i)); + } + d_variables.insert(var); +} + +Node EagerBitblaster::getBBAtom(TNode node) const { return node; } + +/** + * Calls the solve method for the Sat Solver. + * + * @return true for sat, and false for unsat + */ + +bool EagerBitblaster::solve() { + if (Trace.isOn("bitvector")) { + Trace("bitvector") << "EagerBitblaster::solve(). \n"; + } + Debug("bitvector") << "EagerBitblaster::solve(). \n"; + // TODO: clear some memory + // if (something) { + // NodeManager* nm= NodeManager::currentNM(); + // Rewriter::garbageCollect(); + // nm->reclaimZombiesUntil(options::zombieHuntThreshold()); + // } + return prop::SAT_VALUE_TRUE == d_satSolver->solve(); +} + +/** + * Returns the value a is currently assigned to in the SAT solver + * or null if the value is completely unassigned. + * + * @param a + * @param fullModel whether to create a "full model," i.e., add + * constants to equivalence classes that don't already have them + * + * @return + */ +Node EagerBitblaster::getModelFromSatSolver(TNode a, bool fullModel) { + if (!hasBBTerm(a)) { + return fullModel ? utils::mkConst(utils::getSize(a), 0u) : Node(); + } + + Bits bits; + getBBTerm(a, bits); + Integer value(0); + for (int i = bits.size() - 1; i >= 0; --i) { + prop::SatValue bit_value; + if (d_cnfStream->hasLiteral(bits[i])) { + prop::SatLiteral bit = d_cnfStream->getLiteral(bits[i]); + bit_value = d_satSolver->value(bit); + Assert(bit_value != prop::SAT_VALUE_UNKNOWN); + } else { + if (!fullModel) return Node(); + // unconstrained bits default to false + bit_value = prop::SAT_VALUE_FALSE; + } + Integer bit_int = + bit_value == prop::SAT_VALUE_TRUE ? Integer(1) : Integer(0); + value = value * 2 + bit_int; + } + return utils::mkConst(bits.size(), value); +} + +bool EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) +{ + TNodeSet::iterator it = d_variables.begin(); + for (; it != d_variables.end(); ++it) { + TNode var = *it; + if (d_bv->isLeaf(var) || isSharedTerm(var) || + (var.isVar() && var.getType().isBoolean())) { + // only shared terms could not have been bit-blasted + Assert(hasBBTerm(var) || isSharedTerm(var)); + + Node const_value = getModelFromSatSolver(var, true); + + if (const_value != Node()) { + Debug("bitvector-model") + << "EagerBitblaster::collectModelInfo (assert (= " << var << " " + << const_value << "))\n"; + if (!m->assertEquality(var, const_value, true)) + { + return false; + } + } + } + } + return true; +} + +void EagerBitblaster::setProofLog(BitVectorProof* bvp) { + d_bvp = bvp; + d_satSolver->setProofLog(bvp); + 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 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/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp new file mode 100644 index 000000000..539d40384 --- /dev/null +++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp @@ -0,0 +1,601 @@ +/********************* */ +/*! \file lazy_bitblaster.cpp + ** \verbatim + ** Top contributors (to current version): + ** Liana Hadarean, Aina Niemetz, Tim King + ** 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" + +#include "theory/bv/bitblast/lazy_bitblaster.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/theory_bv.h" +#include "theory/rewriter.h" +#include "theory/theory_model.h" +#include "proof/bitvector_proof.h" +#include "proof/proof_manager.h" +#include "theory/bv/theory_bv_utils.h" + +namespace CVC4 { +namespace theory { +namespace bv { + +namespace { + +/* Determine the number of uncached nodes that a given node consists of. */ +uint64_t numNodes(TNode node, utils::NodeSet& seen) +{ + std::vector stack; + uint64_t res = 0; + + stack.push_back(node); + while (!stack.empty()) + { + Node n = stack.back(); + stack.pop_back(); + + if (seen.find(n) != seen.end()) continue; + + res += 1; + seen.insert(n); + stack.insert(stack.end(), n.begin(), n.end()); + } + return res; +} +} + +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)); + + d_cnfStream.reset( + new prop::TseitinCnfStream(d_satSolver.get(), + d_nullRegistrar.get(), + d_nullContext.get(), + options::proof(), + "LazyBitblaster")); + + 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.get()); +} + +void TLazyBitblaster::setAbstraction(AbstractionModule* abs) { + d_abstraction = abs; +} + +TLazyBitblaster::~TLazyBitblaster() +{ + d_assertedAtoms->deleteSelf(); + d_explanations->deleteSelf(); +} + + +/** + * Bitblasts the atom, assigns it a marker literal, adding it to the SAT solver + * NOTE: duplicate clauses are not detected because of marker literal + * @param node the atom to be bitblasted + * + */ +void TLazyBitblaster::bbAtom(TNode node) +{ + NodeManager* nm = NodeManager::currentNM(); + node = node.getKind() == kind::NOT ? node[0] : node; + + if (hasBBAtom(node)) + { + return; + } + + // make sure it is marked as an atom + addAtom(node); + + Debug("bitvector-bitblast") << "Bitblasting node " << node << "\n"; + ++d_statistics.d_numAtoms; + + /// if we are using bit-vector abstraction bit-blast the original + /// interpretation + if (options::bvAbstraction() && d_abstraction != NULL + && d_abstraction->isAbstraction(node)) + { + // node must be of the form P(args) = bv1 + Node expansion = Rewriter::rewrite(d_abstraction->getInterpretation(node)); + + Node atom_bb; + if (expansion.getKind() == kind::CONST_BOOLEAN) + { + atom_bb = expansion; + } + else + { + Assert(expansion.getKind() == kind::AND); + std::vector atoms; + for (unsigned i = 0; i < expansion.getNumChildren(); ++i) + { + Node normalized_i = Rewriter::rewrite(expansion[i]); + Node atom_i = + normalized_i.getKind() != kind::CONST_BOOLEAN + ? Rewriter::rewrite(d_atomBBStrategies[normalized_i.getKind()]( + normalized_i, this)) + : normalized_i; + atoms.push_back(atom_i); + } + atom_bb = utils::mkAnd(atoms); + } + Assert(!atom_bb.isNull()); + Node atom_definition = nm->mkNode(kind::EQUAL, node, atom_bb); + storeBBAtom(node, atom_bb); + d_cnfStream->convertAndAssert( + atom_definition, false, false, RULE_INVALID, TNode::null()); + return; + } + + // the bitblasted definition of the atom + Node normalized = Rewriter::rewrite(node); + Node atom_bb = + normalized.getKind() != kind::CONST_BOOLEAN + ? d_atomBBStrategies[normalized.getKind()](normalized, this) + : normalized; + + if (!options::proof()) + { + atom_bb = Rewriter::rewrite(atom_bb); + } + + // asserting that the atom is true iff the definition holds + Node atom_definition = nm->mkNode(kind::EQUAL, node, atom_bb); + storeBBAtom(node, atom_bb); + d_cnfStream->convertAndAssert( + atom_definition, false, false, RULE_INVALID, TNode::null()); +} + +void TLazyBitblaster::storeBBAtom(TNode atom, Node atom_bb) { + // No need to store the definition for the lazy bit-blaster (unless proofs are enabled). + if( d_bvp != NULL ){ + d_bvp->registerAtomBB(atom.toExpr(), atom_bb.toExpr()); + } + d_bbAtoms.insert(atom); +} + +void TLazyBitblaster::storeBBTerm(TNode node, const Bits& bits) { + if( d_bvp ){ d_bvp->registerTermBB(node.toExpr()); } + d_termCache.insert(std::make_pair(node, bits)); +} + + +bool TLazyBitblaster::hasBBAtom(TNode atom) const { + return d_bbAtoms.find(atom) != d_bbAtoms.end(); +} + + +void TLazyBitblaster::makeVariable(TNode var, Bits& bits) { + Assert(bits.size() == 0); + for (unsigned i = 0; i < utils::getSize(var); ++i) { + bits.push_back(utils::mkBitOf(var, i)); + } + d_variables.insert(var); +} + +uint64_t TLazyBitblaster::computeAtomWeight(TNode node, NodeSet& seen) +{ + node = node.getKind() == kind::NOT ? node[0] : node; + if (!utils::isBitblastAtom(node)) { return 0; } + Node atom_bb = + Rewriter::rewrite(d_atomBBStrategies[node.getKind()](node, this)); + uint64_t size = numNodes(atom_bb, seen); + return size; +} + +// cnf conversion ensures the atom represents itself +Node TLazyBitblaster::getBBAtom(TNode node) const { + return node; +} + +void TLazyBitblaster::bbTerm(TNode node, Bits& bits) { + + if (hasBBTerm(node)) { + getBBTerm(node, bits); + return; + } + Assert( node.getType().isBitVector() ); + + d_bv->spendResource(options::bitblastStep()); + Debug("bitvector-bitblast") << "Bitblasting term " << node <<"\n"; + ++d_statistics.d_numTerms; + + d_termBBStrategies[node.getKind()] (node, bits,this); + + Assert (bits.size() == utils::getSize(node)); + + storeBBTerm(node, bits); +} +/// Public methods + +void TLazyBitblaster::addAtom(TNode atom) { + d_cnfStream->ensureLiteral(atom); + prop::SatLiteral lit = d_cnfStream->getLiteral(atom); + d_satSolver->addMarkerLiteral(lit); +} + +void TLazyBitblaster::explain(TNode atom, std::vector& explanation) { + prop::SatLiteral lit = d_cnfStream->getLiteral(atom); + + ++(d_statistics.d_numExplainedPropagations); + if (options::bvEagerExplanations()) { + Assert (d_explanations->find(lit) != d_explanations->end()); + const std::vector& literal_explanation = (*d_explanations)[lit].get(); + for (unsigned i = 0; i < literal_explanation.size(); ++i) { + explanation.push_back(d_cnfStream->getNode(literal_explanation[i])); + } + return; + } + + std::vector literal_explanation; + d_satSolver->explain(lit, literal_explanation); + for (unsigned i = 0; i < literal_explanation.size(); ++i) { + explanation.push_back(d_cnfStream->getNode(literal_explanation[i])); + } +} + + +/* + * Asserts the clauses corresponding to the atom to the Sat Solver + * by turning on the marker literal (i.e. setting it to false) + * @param node the atom to be asserted + * + */ + +bool TLazyBitblaster::propagate() { + return d_satSolver->propagate() == prop::SAT_VALUE_TRUE; +} + +bool TLazyBitblaster::assertToSat(TNode lit, bool propagate) { + // strip the not + TNode atom; + if (lit.getKind() == kind::NOT) { + atom = lit[0]; + } else { + atom = lit; + } + Assert( utils::isBitblastAtom( atom ) ); + + Assert (hasBBAtom(atom)); + + prop::SatLiteral markerLit = d_cnfStream->getLiteral(atom); + + if(lit.getKind() == kind::NOT) { + markerLit = ~markerLit; + } + + Debug("bitvector-bb") << "TheoryBV::TLazyBitblaster::assertToSat asserting node: " << atom <<"\n"; + Debug("bitvector-bb") << "TheoryBV::TLazyBitblaster::assertToSat with literal: " << markerLit << "\n"; + + prop::SatValue ret = d_satSolver->assertAssumption(markerLit, propagate); + + d_assertedAtoms->push_back(markerLit); + + return ret == prop::SAT_VALUE_TRUE || ret == prop::SAT_VALUE_UNKNOWN; +} + +/** + * Calls the solve method for the Sat Solver. + * passing it the marker literals to be asserted + * + * @return true for sat, and false for unsat + */ + +bool TLazyBitblaster::solve() { + if (Trace.isOn("bitvector")) { + Trace("bitvector") << "TLazyBitblaster::solve() asserted atoms "; + context::CDList::const_iterator it = d_assertedAtoms->begin(); + for (; it != d_assertedAtoms->end(); ++it) { + Trace("bitvector") << " " << d_cnfStream->getNode(*it) << "\n"; + } + } + Debug("bitvector") << "TLazyBitblaster::solve() asserted atoms " << d_assertedAtoms->size() <<"\n"; + d_fullModelAssertionLevel.set(d_bv->numAssertions()); + return prop::SAT_VALUE_TRUE == d_satSolver->solve(); +} + +prop::SatValue TLazyBitblaster::solveWithBudget(unsigned long budget) { + if (Trace.isOn("bitvector")) { + Trace("bitvector") << "TLazyBitblaster::solveWithBudget() asserted atoms "; + context::CDList::const_iterator it = d_assertedAtoms->begin(); + for (; it != d_assertedAtoms->end(); ++it) { + Trace("bitvector") << " " << d_cnfStream->getNode(*it) << "\n"; + } + } + Debug("bitvector") << "TLazyBitblaster::solveWithBudget() asserted atoms " << d_assertedAtoms->size() <<"\n"; + return d_satSolver->solve(budget); +} + +void TLazyBitblaster::getConflict(std::vector& conflict) +{ + NodeManager* nm = NodeManager::currentNM(); + prop::SatClause conflictClause; + d_satSolver->getUnsatCore(conflictClause); + + for (unsigned i = 0; i < conflictClause.size(); i++) + { + prop::SatLiteral lit = conflictClause[i]; + TNode atom = d_cnfStream->getNode(lit); + Node not_atom; + if (atom.getKind() == kind::NOT) + { + not_atom = atom[0]; + } + else + { + not_atom = nm->mkNode(kind::NOT, atom); + } + conflict.push_back(not_atom); + } +} + +TLazyBitblaster::Statistics::Statistics(const std::string& prefix) : + d_numTermClauses(prefix + "::NumTermSatClauses", 0), + d_numAtomClauses(prefix + "::NumAtomSatClauses", 0), + d_numTerms(prefix + "::NumBitblastedTerms", 0), + d_numAtoms(prefix + "::NumBitblastedAtoms", 0), + d_numExplainedPropagations(prefix + "::NumExplainedPropagations", 0), + d_numBitblastingPropagations(prefix + "::NumBitblastingPropagations", 0), + d_bitblastTimer(prefix + "::BitblastTimer") +{ + smtStatisticsRegistry()->registerStat(&d_numTermClauses); + smtStatisticsRegistry()->registerStat(&d_numAtomClauses); + smtStatisticsRegistry()->registerStat(&d_numTerms); + smtStatisticsRegistry()->registerStat(&d_numAtoms); + smtStatisticsRegistry()->registerStat(&d_numExplainedPropagations); + smtStatisticsRegistry()->registerStat(&d_numBitblastingPropagations); + smtStatisticsRegistry()->registerStat(&d_bitblastTimer); +} + + +TLazyBitblaster::Statistics::~Statistics() { + smtStatisticsRegistry()->unregisterStat(&d_numTermClauses); + smtStatisticsRegistry()->unregisterStat(&d_numAtomClauses); + smtStatisticsRegistry()->unregisterStat(&d_numTerms); + smtStatisticsRegistry()->unregisterStat(&d_numAtoms); + smtStatisticsRegistry()->unregisterStat(&d_numExplainedPropagations); + smtStatisticsRegistry()->unregisterStat(&d_numBitblastingPropagations); + smtStatisticsRegistry()->unregisterStat(&d_bitblastTimer); +} + +bool TLazyBitblaster::MinisatNotify::notify(prop::SatLiteral lit) { + if(options::bvEagerExplanations()) { + // compute explanation + if (d_lazyBB->d_explanations->find(lit) == d_lazyBB->d_explanations->end()) { + std::vector literal_explanation; + d_lazyBB->d_satSolver->explain(lit, literal_explanation); + d_lazyBB->d_explanations->insert(lit, literal_explanation); + } else { + // we propagated it at a lower level + return true; + } + } + ++(d_lazyBB->d_statistics.d_numBitblastingPropagations); + TNode atom = d_cnf->getNode(lit); + return d_bv->storePropagation(atom, SUB_BITBLAST); +} + +void TLazyBitblaster::MinisatNotify::notify(prop::SatClause& clause) { + if (clause.size() > 1) { + NodeBuilder<> lemmab(kind::OR); + for (unsigned i = 0; i < clause.size(); ++ i) { + lemmab << d_cnf->getNode(clause[i]); + } + Node lemma = lemmab; + d_bv->d_out->lemma(lemma); + } else { + d_bv->d_out->lemma(d_cnf->getNode(clause[0])); + } +} + +void TLazyBitblaster::MinisatNotify::spendResource(unsigned amount) +{ + d_bv->spendResource(amount); +} + +void TLazyBitblaster::MinisatNotify::safePoint(unsigned amount) +{ + d_bv->d_out->safePoint(amount); +} + +EqualityStatus TLazyBitblaster::getEqualityStatus(TNode a, TNode b) +{ + int numAssertions = d_bv->numAssertions(); + Debug("bv-equality-status") + << "TLazyBitblaster::getEqualityStatus " << a << " = " << b << "\n"; + Debug("bv-equality-status") + << "BVSatSolver has full model? " + << (d_fullModelAssertionLevel.get() == numAssertions) << "\n"; + + // First check if it trivially rewrites to false/true + Node a_eq_b = + Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL, a, b)); + + if (a_eq_b == utils::mkFalse()) return theory::EQUALITY_FALSE; + if (a_eq_b == utils::mkTrue()) return theory::EQUALITY_TRUE; + + if (d_fullModelAssertionLevel.get() != numAssertions) + { + return theory::EQUALITY_UNKNOWN; + } + + // Check if cache is valid (invalidated in check and pops) + if (d_bv->d_invalidateModelCache.get()) + { + invalidateModelCache(); + } + d_bv->d_invalidateModelCache.set(false); + + Node a_value = getTermModel(a, true); + Node b_value = getTermModel(b, true); + + Assert(a_value.isConst() && b_value.isConst()); + + if (a_value == b_value) + { + Debug("bv-equality-status") << "theory::EQUALITY_TRUE_IN_MODEL\n"; + return theory::EQUALITY_TRUE_IN_MODEL; + } + Debug("bv-equality-status") << "theory::EQUALITY_FALSE_IN_MODEL\n"; + return theory::EQUALITY_FALSE_IN_MODEL; +} + +bool TLazyBitblaster::isSharedTerm(TNode node) { + return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end(); +} + +bool TLazyBitblaster::hasValue(TNode a) { + Assert (hasBBTerm(a)); + Bits bits; + getBBTerm(a, bits); + for (int i = bits.size() -1; i >= 0; --i) { + prop::SatValue bit_value; + if (d_cnfStream->hasLiteral(bits[i])) { + prop::SatLiteral bit = d_cnfStream->getLiteral(bits[i]); + bit_value = d_satSolver->value(bit); + if (bit_value == prop::SAT_VALUE_UNKNOWN) + return false; + } else { + return false; + } + } + return true; +} +/** + * Returns the value a is currently assigned to in the SAT solver + * or null if the value is completely unassigned. + * + * @param a + * @param fullModel whether to create a "full model," i.e., add + * constants to equivalence classes that don't already have them + * + * @return + */ +Node TLazyBitblaster::getModelFromSatSolver(TNode a, bool fullModel) { + if (!hasBBTerm(a)) { + return fullModel? utils::mkConst(utils::getSize(a), 0u) : Node(); + } + + Bits bits; + getBBTerm(a, bits); + Integer value(0); + for (int i = bits.size() -1; i >= 0; --i) { + prop::SatValue bit_value; + if (d_cnfStream->hasLiteral(bits[i])) { + prop::SatLiteral bit = d_cnfStream->getLiteral(bits[i]); + bit_value = d_satSolver->value(bit); + Assert (bit_value != prop::SAT_VALUE_UNKNOWN); + } else { + if (!fullModel) return Node(); + // unconstrained bits default to false + bit_value = prop::SAT_VALUE_FALSE; + } + Integer bit_int = bit_value == prop::SAT_VALUE_TRUE ? Integer(1) : Integer(0); + value = value * 2 + bit_int; + } + return utils::mkConst(bits.size(), value); +} + +bool TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) +{ + std::set termSet; + d_bv->computeRelevantTerms(termSet); + + for (std::set::const_iterator it = termSet.begin(); it != termSet.end(); ++it) { + TNode var = *it; + // not actually a leaf of the bit-vector theory + if (d_variables.find(var) == d_variables.end()) + continue; + + Assert (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)); + // only shared terms could not have been bit-blasted + Assert (hasBBTerm(var) || isSharedTerm(var)); + + Node const_value = getModelFromSatSolver(var, true); + Assert (const_value.isNull() || const_value.isConst()); + if(const_value != Node()) { + Debug("bitvector-model") << "TLazyBitblaster::collectModelInfo (assert (= " + << var << " " + << const_value << "))\n"; + if (!m->assertEquality(var, const_value, true)) + { + return false; + } + } + } + return true; +} + +void TLazyBitblaster::setProofLog( BitVectorProof * bvp ){ + d_bvp = bvp; + d_satSolver->setProofLog( bvp ); + bvp->initCnfProof(d_cnfStream.get(), d_nullContext.get()); +} + +void TLazyBitblaster::clearSolver() { + Assert (d_ctx->getLevel() == 0); + d_assertedAtoms->deleteSelf(); + d_assertedAtoms = new(true) context::CDList(d_ctx); + d_explanations->deleteSelf(); + d_explanations = new(true) ExplanationMap(d_ctx); + d_bbAtoms.clear(); + d_variables.clear(); + d_termCache.clear(); + + invalidateModelCache(); + // recreate sat solver + 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/bitblast_strategies_template.h b/src/theory/bv/bitblast_strategies_template.h deleted file mode 100644 index 60e7fc051..000000000 --- a/src/theory/bv/bitblast_strategies_template.h +++ /dev/null @@ -1,910 +0,0 @@ -/********************* */ -/*! \file bitblast_strategies_template.h - ** \verbatim - ** Top contributors (to current version): - ** Liana Hadarean, Aina Niemetz, Clark Barrett - ** 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 Implementation of bitblasting functions for various operators. - ** - ** Implementation of bitblasting functions for various operators. - **/ - -#ifndef __CVC4__BITBLAST__STRATEGIES_TEMPLATE_H -#define __CVC4__BITBLAST__STRATEGIES_TEMPLATE_H - -#include -#include - -#include "cvc4_private.h" -#include "expr/node.h" -#include "theory/bv/bitblast_utils.h" -#include "theory/bv/theory_bv_utils.h" -#include "theory/rewriter.h" - -namespace CVC4 { - -namespace theory { -namespace bv { - -/** - * Default Atom Bitblasting strategies: - * - * @param node the atom to be bitblasted - * @param bb the bitblaster - */ - -template -T UndefinedAtomBBStrategy(TNode node, TBitblaster* bb) { - Debug("bitvector") << "TheoryBV::Bitblaster Undefined bitblasting strategy for kind: " - << node.getKind() << "\n"; - Unreachable(); -} - - -template -T DefaultEqBB(TNode node, TBitblaster* bb) { - Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; - - Assert(node.getKind() == kind::EQUAL); - std::vector lhs, rhs; - bb->bbTerm(node[0], lhs); - bb->bbTerm(node[1], rhs); - - Assert(lhs.size() == rhs.size()); - - std::vector bits_eq; - for (unsigned i = 0; i < lhs.size(); i++) { - T bit_eq = mkIff(lhs[i], rhs[i]); - bits_eq.push_back(bit_eq); - } - T bv_eq = mkAnd(bits_eq); - return bv_eq; -} - -template -T AdderUltBB(TNode node, TBitblaster* bb) { - Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; - Assert(node.getKind() == kind::BITVECTOR_ULT); - std::vector a, b; - bb->bbTerm(node[0], a); - bb->bbTerm(node[1], b); - Assert(a.size() == b.size()); - - // a < b <=> ~ (add(a, ~b, 1).carry_out) - std::vector not_b; - negateBits(b, not_b); - T carry = mkTrue(); - - for (unsigned i = 0 ; i < a.size(); ++i) { - carry = mkOr( mkAnd(a[i], not_b[i]), - mkAnd( mkXor(a[i], not_b[i]), - carry)); - } - return mkNot(carry); -} - - -template -T DefaultUltBB(TNode node, TBitblaster* bb) { - Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; - Assert(node.getKind() == kind::BITVECTOR_ULT); - std::vector a, b; - bb->bbTerm(node[0], a); - bb->bbTerm(node[1], b); - Assert(a.size() == b.size()); - - // construct bitwise comparison - T res = uLessThanBB(a, b, false); - return res; -} - -template -T DefaultUleBB(TNode node, TBitblaster* bb){ - Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; - Assert(node.getKind() == kind::BITVECTOR_ULE); - std::vector a, b; - - bb->bbTerm(node[0], a); - bb->bbTerm(node[1], b); - Assert(a.size() == b.size()); - // construct bitwise comparison - T res = uLessThanBB(a, b, true); - return res; -} - -template -T DefaultUgtBB(TNode node, TBitblaster* bb){ - Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; - // should be rewritten - Unimplemented(); -} -template -T DefaultUgeBB(TNode node, TBitblaster* bb){ - Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; - // should be rewritten - Unimplemented(); -} - -template -T DefaultSltBB(TNode node, TBitblaster* bb){ - Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; - - std::vector a, b; - bb->bbTerm(node[0], a); - bb->bbTerm(node[1], b); - Assert(a.size() == b.size()); - - T res = sLessThanBB(a, b, false); - return res; -} - -template -T DefaultSleBB(TNode node, TBitblaster* bb){ - Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; - - std::vector a, b; - bb->bbTerm(node[0], a); - bb->bbTerm(node[1], b); - Assert(a.size() == b.size()); - - T res = sLessThanBB(a, b, true); - return res; -} - -template -T DefaultSgtBB(TNode node, TBitblaster* bb){ - Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; - // should be rewritten - Unimplemented(); -} - -template -T DefaultSgeBB(TNode node, TBitblaster* bb){ - Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; - // should be rewritten - Unimplemented(); -} - - -/// Term bitblasting strategies - -/** - * Default Term Bitblasting strategies - * - * @param node the term to be bitblasted - * @param bits [output parameter] bits representing the new term - * @param bb the bitblaster in which the clauses are added - */ -template -void UndefinedTermBBStrategy(TNode node, std::vector& bits, TBitblaster* bb) { - Debug("bitvector") << "theory::bv:: Undefined bitblasting strategy for kind: " - << node.getKind() << "\n"; - Unreachable(); -} - -template -void DefaultVarBB (TNode node, std::vector& bits, TBitblaster* bb) { - Assert(bits.size() == 0); - bb->makeVariable(node, bits); - - if(Debug.isOn("bitvector-bb")) { - Debug("bitvector-bb") << "theory::bv::DefaultVarBB bitblasting " << node << "\n"; - Debug("bitvector-bb") << " with bits " << toString(bits); - } -} - -template -void DefaultConstBB (TNode node, std::vector& bits, TBitblaster* bb) { - Debug("bitvector-bb") << "theory::bv::DefaultConstBB bitblasting " << node << "\n"; - Assert(node.getKind() == kind::CONST_BITVECTOR); - Assert(bits.size() == 0); - - for (unsigned i = 0; i < utils::getSize(node); ++i) { - Integer bit = node.getConst().extract(i, i).getValue(); - if(bit == Integer(0)){ - bits.push_back(mkFalse()); - } else { - Assert (bit == Integer(1)); - bits.push_back(mkTrue()); - } - } - if(Debug.isOn("bitvector-bb")) { - Debug("bitvector-bb") << "with bits: " << toString(bits) << "\n"; - } -} - - -template -void DefaultNotBB (TNode node, std::vector& bits, TBitblaster* bb) { - Debug("bitvector-bb") << "theory::bv::DefaultNotBB bitblasting " << node << "\n"; - Assert(node.getKind() == kind::BITVECTOR_NOT); - Assert(bits.size() == 0); - std::vector bv; - bb->bbTerm(node[0], bv); - negateBits(bv, bits); -} - -template -void DefaultConcatBB (TNode node, std::vector& bits, TBitblaster* bb) { - Debug("bitvector-bb") << "theory::bv::DefaultConcatBB bitblasting " << node << "\n"; - Assert(bits.size() == 0); - - Assert (node.getKind() == kind::BITVECTOR_CONCAT); - for (int i = node.getNumChildren() -1 ; i >= 0; --i ) { - TNode current = node[i]; - std::vector current_bits; - bb->bbTerm(current, current_bits); - - for(unsigned j = 0; j < utils::getSize(current); ++j) { - bits.push_back(current_bits[j]); - } - } - Assert (bits.size() == utils::getSize(node)); - if(Debug.isOn("bitvector-bb")) { - Debug("bitvector-bb") << "with bits: " << toString(bits) << "\n"; - } -} - -template -void DefaultAndBB (TNode node, std::vector& bits, TBitblaster* bb) { - Debug("bitvector-bb") << "theory::bv::DefaultAndBB bitblasting " << node << "\n"; - - Assert(node.getKind() == kind::BITVECTOR_AND && - bits.size() == 0); - - bb->bbTerm(node[0], bits); - std::vector current; - for(unsigned j = 1; j < node.getNumChildren(); ++j) { - bb->bbTerm(node[j], current); - for (unsigned i = 0; i < utils::getSize(node); ++i) { - bits[i] = mkAnd(bits[i], current[i]); - } - current.clear(); - } - Assert (bits.size() == utils::getSize(node)); -} - -template -void DefaultOrBB (TNode node, std::vector& bits, TBitblaster* bb) { - Debug("bitvector-bb") << "theory::bv::DefaultOrBB bitblasting " << node << "\n"; - - Assert(node.getKind() == kind::BITVECTOR_OR && - bits.size() == 0); - - bb->bbTerm(node[0], bits); - std::vector current; - for(unsigned j = 1; j < node.getNumChildren(); ++j) { - bb->bbTerm(node[j], current); - for (unsigned i = 0; i < utils::getSize(node); ++i) { - bits[i] = mkOr(bits[i], current[i]); - } - current.clear(); - } - Assert (bits.size() == utils::getSize(node)); -} - -template -void DefaultXorBB (TNode node, std::vector& bits, TBitblaster* bb) { - Debug("bitvector-bb") << "theory::bv::DefaultXorBB bitblasting " << node << "\n"; - - Assert(node.getKind() == kind::BITVECTOR_XOR && - bits.size() == 0); - - bb->bbTerm(node[0], bits); - std::vector current; - for(unsigned j = 1; j < node.getNumChildren(); ++j) { - bb->bbTerm(node[j], current); - for (unsigned i = 0; i < utils::getSize(node); ++i) { - bits[i] = mkXor(bits[i], current[i]); - } - current.clear(); - } - Assert (bits.size() == utils::getSize(node)); -} - -template -void DefaultXnorBB (TNode node, std::vector& bits, TBitblaster* bb) { - Debug("bitvector-bb") << "theory::bv::DefaultXnorBB bitblasting " << node << "\n"; - - Assert(node.getNumChildren() == 2 && - node.getKind() == kind::BITVECTOR_XNOR && - bits.size() == 0); - std::vector lhs, rhs; - bb->bbTerm(node[0], lhs); - bb->bbTerm(node[1], rhs); - Assert(lhs.size() == rhs.size()); - - for (unsigned i = 0; i < lhs.size(); ++i) { - bits.push_back(mkIff(lhs[i], rhs[i])); - } -} - - -template -void DefaultNandBB (TNode node, std::vector& bits, TBitblaster* bb) { - Debug("bitvector") << "theory::bv:: Unimplemented kind " - << node.getKind() << "\n"; - Unimplemented(); -} -template -void DefaultNorBB (TNode node, std::vector& bits, TBitblaster* bb) { - Debug("bitvector") << "theory::bv:: Unimplemented kind " - << node.getKind() << "\n"; - Unimplemented(); -} -template -void DefaultCompBB (TNode node, std::vector& bits, TBitblaster* bb) { - Debug("bitvector") << "theory::bv:: DefaultCompBB bitblasting "<< node << "\n"; - - Assert(utils::getSize(node) == 1 && bits.size() == 0 && node.getKind() == kind::BITVECTOR_COMP); - std::vector a, b; - bb->bbTerm(node[0], a); - bb->bbTerm(node[1], b); - - std::vector bit_eqs; - for (unsigned i = 0; i < a.size(); ++i) { - T eq = mkIff(a[i], b[i]); - bit_eqs.push_back(eq); - } - T a_eq_b = mkAnd(bit_eqs); - bits.push_back(a_eq_b); -} - -template -void DefaultMultBB (TNode node, std::vector& res, TBitblaster* bb) { - Debug("bitvector") << "theory::bv:: DefaultMultBB bitblasting "<< node << "\n"; - Assert(res.size() == 0 && - node.getKind() == kind::BITVECTOR_MULT); - - // if (node.getNumChildren() == 2) { - // std::vector a; - // std::vector b; - // bb->bbTerm(node[0], a); - // bb->bbTerm(node[1], b); - // unsigned bw = utils::getSize(node); - // unsigned thresh = bw % 2 ? bw/2 : bw/2 - 1; - // bool no_overflow = true; - // for (unsigned i = thresh; i < bw; ++i) { - // if (a[i] != mkFalse || b[i] != mkFalse ) { - // no_overflow = false; - // } - // } - // if (no_overflow) { - // shiftAddMultiplier(); - // return; - // } - - // } - - std::vector newres; - bb->bbTerm(node[0], res); - for(unsigned i = 1; i < node.getNumChildren(); ++i) { - std::vector current; - bb->bbTerm(node[i], current); - newres.clear(); - // constructs a simple shift and add multiplier building the result - // in res - shiftAddMultiplier(res, current, newres); - res = newres; - } - if(Debug.isOn("bitvector-bb")) { - Debug("bitvector-bb") << "with bits: " << toString(res) << "\n"; - } -} - -template -void DefaultPlusBB (TNode node, std::vector& res, TBitblaster* bb) { - Debug("bitvector-bb") << "theory::bv::DefaultPlusBB bitblasting " << node << "\n"; - Assert(node.getKind() == kind::BITVECTOR_PLUS && - res.size() == 0); - - bb->bbTerm(node[0], res); - - std::vector newres; - - for(unsigned i = 1; i < node.getNumChildren(); ++i) { - std::vector current; - bb->bbTerm(node[i], current); - newres.clear(); - rippleCarryAdder(res, current, newres, mkFalse()); - res = newres; - } - - Assert(res.size() == utils::getSize(node)); -} - - -template -void DefaultSubBB (TNode node, std::vector& bits, TBitblaster* bb) { - Debug("bitvector-bb") << "theory::bv::DefaultSubBB bitblasting " << node << "\n"; - Assert(node.getKind() == kind::BITVECTOR_SUB && - node.getNumChildren() == 2 && - bits.size() == 0); - - std::vector a, b; - bb->bbTerm(node[0], a); - bb->bbTerm(node[1], b); - Assert(a.size() == b.size() && utils::getSize(node) == a.size()); - - // bvsub a b = adder(a, ~b, 1) - std::vector not_b; - negateBits(b, not_b); - rippleCarryAdder(a, not_b, bits, mkTrue()); -} - -template -void DefaultNegBB (TNode node, std::vector& bits, TBitblaster* bb) { - Debug("bitvector-bb") << "theory::bv::DefaultNegBB bitblasting " << node << "\n"; - Assert(node.getKind() == kind::BITVECTOR_NEG); - - std::vector a; - bb->bbTerm(node[0], a); - Assert(utils::getSize(node) == a.size()); - - // -a = add(~a, 0, 1). - std::vector not_a; - negateBits(a, not_a); - std::vector zero; - makeZero(zero, utils::getSize(node)); - - rippleCarryAdder(not_a, zero, bits, mkTrue()); -} - -template -void uDivModRec(const std::vector& a, const std::vector& b, std::vector& q, std::vector& r, unsigned rec_width) { - Assert( q.size() == 0 && r.size() == 0); - - if(rec_width == 0 || isZero(a)) { - makeZero(q, a.size()); - makeZero(r, a.size()); - return; - } - - std::vector q1, r1; - std::vector a1 = a; - rshift(a1, 1); - - uDivModRec(a1, b, q1, r1, rec_width - 1); - // shift the quotient and remainder (i.e. multiply by two) and add 1 to remainder if a is odd - lshift(q1, 1); - lshift(r1, 1); - - - T is_odd = mkIff(a[0], mkTrue()); - T one_if_odd = mkIte(is_odd, mkTrue(), mkFalse()); - - std::vector zero; - makeZero(zero, b.size()); - - std::vector r1_shift_add; - // account for a being odd - rippleCarryAdder(r1, zero, r1_shift_add, one_if_odd); - // now check if the remainder is greater than b - std::vector not_b; - negateBits(b, not_b); - std::vector r_minus_b; - T co1; - // use adder because we need r_minus_b anyway - co1 = rippleCarryAdder(r1_shift_add, not_b, r_minus_b, mkTrue()); - // sign is true if r1 < b - T sign = mkNot(co1); - - q1[0] = mkIte(sign, q1[0], mkTrue()); - - // would be nice to have a high level ITE instead of bitwise - for(unsigned i = 0; i < a.size(); ++i) { - r1_shift_add[i] = mkIte(sign, r1_shift_add[i], r_minus_b[i]); - } - - // check if a < b - - std::vector a_minus_b; - T co2 = rippleCarryAdder(a, not_b, a_minus_b, mkTrue()); - // Node a_lt_b = a_minus_b.back(); - T a_lt_b = mkNot(co2); - - for(unsigned i = 0; i < a.size(); ++i) { - T qval = mkIte(a_lt_b, mkFalse(), q1[i]); - T rval = mkIte(a_lt_b, a[i], r1_shift_add[i]); - q.push_back(qval); - r.push_back(rval); - } - -} - -template -void DefaultUdivBB(TNode node, std::vector& q, TBitblaster* bb) -{ - Debug("bitvector-bb") << "theory::bv::DefaultUdivBB bitblasting " << node - << "\n"; - Assert(node.getKind() == kind::BITVECTOR_UDIV_TOTAL && q.size() == 0); - - std::vector a, b; - bb->bbTerm(node[0], a); - bb->bbTerm(node[1], b); - - std::vector r; - uDivModRec(a, b, q, r, utils::getSize(node)); - // adding a special case for division by 0 - std::vector iszero; - for (unsigned i = 0; i < b.size(); ++i) - { - iszero.push_back(mkIff(b[i], mkFalse())); - } - T b_is_0 = mkAnd(iszero); - - for (unsigned i = 0; i < q.size(); ++i) - { - q[i] = mkIte(b_is_0, mkTrue(), q[i]); // a udiv 0 is 11..11 - r[i] = mkIte(b_is_0, a[i], r[i]); // a urem 0 is a - } - - // cache the remainder in case we need it later - Node remainder = Rewriter::rewrite(NodeManager::currentNM()->mkNode( - kind::BITVECTOR_UREM_TOTAL, node[0], node[1])); - bb->storeBBTerm(remainder, r); -} - -template -void DefaultUremBB(TNode node, std::vector& rem, TBitblaster* bb) -{ - Debug("bitvector-bb") << "theory::bv::DefaultUremBB bitblasting " << node - << "\n"; - Assert(node.getKind() == kind::BITVECTOR_UREM_TOTAL && rem.size() == 0); - - std::vector a, b; - bb->bbTerm(node[0], a); - bb->bbTerm(node[1], b); - - std::vector q; - uDivModRec(a, b, q, rem, utils::getSize(node)); - // adding a special case for division by 0 - std::vector iszero; - for (unsigned i = 0; i < b.size(); ++i) - { - iszero.push_back(mkIff(b[i], mkFalse())); - } - T b_is_0 = mkAnd(iszero); - - for (unsigned i = 0; i < q.size(); ++i) - { - q[i] = mkIte(b_is_0, mkTrue(), q[i]); // a udiv 0 is 11..11 - rem[i] = mkIte(b_is_0, a[i], rem[i]); // a urem 0 is a - } - - // cache the quotient in case we need it later - Node quotient = Rewriter::rewrite(NodeManager::currentNM()->mkNode( - kind::BITVECTOR_UDIV_TOTAL, node[0], node[1])); - bb->storeBBTerm(quotient, q); -} - -template -void DefaultSdivBB (TNode node, std::vector& bits, TBitblaster* bb) { - Debug("bitvector") << "theory::bv:: Unimplemented kind " - << node.getKind() << "\n"; - Unimplemented(); -} -template -void DefaultSremBB (TNode node, std::vector& bits, TBitblaster* bb) { - Debug("bitvector") << "theory::bv:: Unimplemented kind " - << node.getKind() << "\n"; - Unimplemented(); -} -template -void DefaultSmodBB (TNode node, std::vector& bits, TBitblaster* bb) { - Debug("bitvector") << "theory::bv:: Unimplemented kind " - << node.getKind() << "\n"; - Unimplemented(); -} - -template -void DefaultShlBB(TNode node, std::vector& res, TBitblaster* bb) -{ - Debug("bitvector-bb") << "theory::bv::DefaultShlBB bitblasting " << node - << "\n"; - Assert(node.getKind() == kind::BITVECTOR_SHL && res.size() == 0); - std::vector a, b; - bb->bbTerm(node[0], a); - bb->bbTerm(node[1], b); - - // check for b < log2(n) - unsigned size = utils::getSize(node); - unsigned log2_size = std::ceil(log2((double)size)); - Node a_size = utils::mkConst(size, size); - Node b_ult_a_size_node = Rewriter::rewrite( - NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULT, node[1], a_size)); - // ensure that the inequality is bit-blasted - bb->bbAtom(b_ult_a_size_node); - T b_ult_a_size = bb->getBBAtom(b_ult_a_size_node); - std::vector prev_res; - res = a; - // we only need to look at the bits bellow log2_a_size - for (unsigned s = 0; s < log2_size; ++s) - { - // barrel shift stage: at each stage you can either shift by 2^s bits - // or leave the previous stage untouched - prev_res = res; - unsigned threshold = pow(2, s); - for (unsigned i = 0; i < a.size(); ++i) - { - if (i < threshold) - { - // if b[s] is true then we must have shifted by at least 2^b bits so - // all bits bellow 2^s will be 0, otherwise just use previous shift - // value - res[i] = mkIte(b[s], mkFalse(), prev_res[i]); - } - else - { - // if b[s]= 0, use previous value, otherwise shift by threshold bits - Assert(i >= threshold); - res[i] = mkIte(b[s], prev_res[i - threshold], prev_res[i]); - } - } - } - prev_res = res; - for (unsigned i = 0; i < b.size(); ++i) - { - // this is fine because b_ult_a_size has been bit-blasted - res[i] = mkIte(b_ult_a_size, prev_res[i], mkFalse()); - } - - if (Debug.isOn("bitvector-bb")) - { - Debug("bitvector-bb") << "with bits: " << toString(res) << "\n"; - } -} - -template -void DefaultLshrBB(TNode node, std::vector& res, TBitblaster* bb) -{ - Debug("bitvector-bb") << "theory::bv::DefaultLshrBB bitblasting " << node - << "\n"; - Assert(node.getKind() == kind::BITVECTOR_LSHR && res.size() == 0); - std::vector a, b; - bb->bbTerm(node[0], a); - bb->bbTerm(node[1], b); - - // check for b < log2(n) - unsigned size = utils::getSize(node); - unsigned log2_size = std::ceil(log2((double)size)); - Node a_size = utils::mkConst(size, size); - Node b_ult_a_size_node = Rewriter::rewrite( - NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULT, node[1], a_size)); - // ensure that the inequality is bit-blasted - bb->bbAtom(b_ult_a_size_node); - T b_ult_a_size = bb->getBBAtom(b_ult_a_size_node); - res = a; - std::vector prev_res; - - for (unsigned s = 0; s < log2_size; ++s) - { - // barrel shift stage: at each stage you can either shift by 2^s bits - // or leave the previous stage untouched - prev_res = res; - int threshold = pow(2, s); - for (unsigned i = 0; i < a.size(); ++i) - { - if (i + threshold >= a.size()) - { - // if b[s] is true then we must have shifted by at least 2^b bits so - // all bits above 2^s will be 0, otherwise just use previous shift value - res[i] = mkIte(b[s], mkFalse(), prev_res[i]); - } - else - { - // if b[s]= 0, use previous value, otherwise shift by threshold bits - Assert(i + threshold < a.size()); - res[i] = mkIte(mkNot(b[s]), prev_res[i], prev_res[i + threshold]); - } - } - } - - prev_res = res; - for (unsigned i = 0; i < b.size(); ++i) - { - // this is fine because b_ult_a_size has been bit-blasted - res[i] = mkIte(b_ult_a_size, prev_res[i], mkFalse()); - } - - if (Debug.isOn("bitvector-bb")) - { - Debug("bitvector-bb") << "with bits: " << toString(res) << "\n"; - } -} - -template -void DefaultAshrBB(TNode node, std::vector& res, TBitblaster* bb) -{ - Debug("bitvector-bb") << "theory::bv::DefaultAshrBB bitblasting " << node - << "\n"; - Assert(node.getKind() == kind::BITVECTOR_ASHR && res.size() == 0); - std::vector a, b; - bb->bbTerm(node[0], a); - bb->bbTerm(node[1], b); - - // check for b < n - unsigned size = utils::getSize(node); - unsigned log2_size = std::ceil(log2((double)size)); - Node a_size = utils::mkConst(size, size); - Node b_ult_a_size_node = Rewriter::rewrite( - NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULT, node[1], a_size)); - // ensure that the inequality is bit-blasted - bb->bbAtom(b_ult_a_size_node); - T b_ult_a_size = bb->getBBAtom(b_ult_a_size_node); - - res = a; - T sign_bit = a.back(); - std::vector prev_res; - - for (unsigned s = 0; s < log2_size; ++s) - { - // barrel shift stage: at each stage you can either shift by 2^s bits - // or leave the previous stage untouched - prev_res = res; - int threshold = pow(2, s); - for (unsigned i = 0; i < a.size(); ++i) - { - if (i + threshold >= a.size()) - { - // if b[s] is true then we must have shifted by at least 2^b bits so - // all bits above 2^s will be the sign bit, otherwise just use previous - // shift value - res[i] = mkIte(b[s], sign_bit, prev_res[i]); - } - else - { - // if b[s]= 0, use previous value, otherwise shift by threshold bits - Assert(i + threshold < a.size()); - res[i] = mkIte(mkNot(b[s]), prev_res[i], prev_res[i + threshold]); - } - } - } - - prev_res = res; - for (unsigned i = 0; i < b.size(); ++i) - { - // this is fine because b_ult_a_size has been bit-blasted - res[i] = mkIte(b_ult_a_size, prev_res[i], sign_bit); - } - - if (Debug.isOn("bitvector-bb")) - { - Debug("bitvector-bb") << "with bits: " << toString(res) << "\n"; - } -} - -template -void DefaultUltbvBB (TNode node, std::vector& res, TBitblaster* bb) { - Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; - Assert(node.getKind() == kind::BITVECTOR_ULTBV); - std::vector a, b; - bb->bbTerm(node[0], a); - bb->bbTerm(node[1], b); - Assert(a.size() == b.size()); - - // construct bitwise comparison - res.push_back(uLessThanBB(a, b, false)); -} - -template -void DefaultSltbvBB (TNode node, std::vector& res, TBitblaster* bb) { - Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; - Assert(node.getKind() == kind::BITVECTOR_SLTBV); - std::vector a, b; - bb->bbTerm(node[0], a); - bb->bbTerm(node[1], b); - Assert(a.size() == b.size()); - - // construct bitwise comparison - res.push_back(sLessThanBB(a, b, false)); -} - -template -void DefaultIteBB (TNode node, std::vector& res, TBitblaster* bb) { - Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; - Assert(node.getKind() == kind::BITVECTOR_ITE); - std::vector cond, thenpart, elsepart; - bb->bbTerm(node[0], cond); - bb->bbTerm(node[1], thenpart); - bb->bbTerm(node[2], elsepart); - - Assert(cond.size() == 1); - Assert(thenpart.size() == elsepart.size()); - - for (unsigned i = 0; i < thenpart.size(); ++i) { - // (~cond OR thenpart) AND (cond OR elsepart) - res.push_back(mkAnd(mkOr(mkNot(cond[0]),thenpart[i]),mkOr(cond[0],elsepart[i]))); - } -} - -template -void DefaultExtractBB (TNode node, std::vector& bits, TBitblaster* bb) { - Assert (node.getKind() == kind::BITVECTOR_EXTRACT); - Assert(bits.size() == 0); - - std::vector base_bits; - bb->bbTerm(node[0], base_bits); - unsigned high = utils::getExtractHigh(node); - unsigned low = utils::getExtractLow(node); - - for (unsigned i = low; i <= high; ++i) { - bits.push_back(base_bits[i]); - } - Assert (bits.size() == high - low + 1); - - if(Debug.isOn("bitvector-bb")) { - Debug("bitvector-bb") << "theory::bv::DefaultExtractBB bitblasting " << node << "\n"; - Debug("bitvector-bb") << " with bits " << toString(bits); - } -} - - -template -void DefaultRepeatBB (TNode node, std::vector& bits, TBitblaster* bb) { - Debug("bitvector") << "theory::bv:: Unimplemented kind " - << node.getKind() << "\n"; - // this should be rewritten - Unimplemented(); -} - -template -void DefaultZeroExtendBB (TNode node, std::vector& res_bits, TBitblaster* bb) { - - Debug("bitvector-bb") << "theory::bv::DefaultZeroExtendBB bitblasting " << node << "\n"; - - // this should be rewritten - Unimplemented(); - -} - -template -void DefaultSignExtendBB (TNode node, std::vector& res_bits, TBitblaster* bb) { - Debug("bitvector-bb") << "theory::bv::DefaultSignExtendBB bitblasting " << node << "\n"; - - Assert (node.getKind() == kind::BITVECTOR_SIGN_EXTEND && - res_bits.size() == 0); - - std::vector bits; - bb->bbTerm(node[0], bits); - - T sign_bit = bits.back(); - unsigned amount = node.getOperator().getConst().signExtendAmount; - - for (unsigned i = 0; i < bits.size(); ++i ) { - res_bits.push_back(bits[i]); - } - - for (unsigned i = 0 ; i < amount ; ++i ) { - res_bits.push_back(sign_bit); - } - - Assert (res_bits.size() == amount + bits.size()); -} - -template -void DefaultRotateRightBB (TNode node, std::vector& res, TBitblaster* bb) { - Debug("bitvector") << "theory::bv:: Unimplemented kind " - << node.getKind() << "\n"; - - Unimplemented(); -} - -template -void DefaultRotateLeftBB (TNode node, std::vector& bits, TBitblaster* bb) { - Debug("bitvector") << "theory::bv:: Unimplemented kind " - << node.getKind() << "\n"; - Unimplemented(); -} - - -} -} -} - -#endif diff --git a/src/theory/bv/bitblast_utils.h b/src/theory/bv/bitblast_utils.h deleted file mode 100644 index 1d6920007..000000000 --- a/src/theory/bv/bitblast_utils.h +++ /dev/null @@ -1,283 +0,0 @@ -/********************* */ -/*! \file bitblast_utils.h - ** \verbatim - ** Top contributors (to current version): - ** Liana Hadarean, Paul Meng, Andrew Reynolds - ** 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 Various utility functions for bit-blasting. - ** - ** Various utility functions for bit-blasting. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__BITBLAST__UTILS_H -#define __CVC4__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 { - -template class TBitblaster; - -template -std::string toString (const std::vector& bits); - -template <> inline -std::string toString (const std::vector& bits) { - std::ostringstream os; - for (int i = bits.size() - 1; i >= 0; --i) { - TNode bit = bits[i]; - if (bit.getKind() == kind::CONST_BOOLEAN) { - os << (bit.getConst() ? "1" : "0"); - } else { - os << bit<< " "; - } - } - os <<"\n"; - return os.str(); -} - -template T mkTrue(); -template T mkFalse(); -template T mkNot(T a); -template T mkOr(T a, T b); -template T mkOr(const std::vector& a); -template T mkAnd(T a, T b); -template T mkAnd(const std::vector& a); -template T mkXor(T a, T b); -template T mkIff(T a, T b); -template T mkIte(T cond, T a, T b); - - -template <> inline -Node mkTrue() { - return NodeManager::currentNM()->mkConst(true); -} - -template <> inline -Node mkFalse() { - return NodeManager::currentNM()->mkConst(false); -} - -template <> inline -Node mkNot(Node a) { - return NodeManager::currentNM()->mkNode(kind::NOT, a); -} - -template <> inline -Node mkOr(Node a, Node b) { - return NodeManager::currentNM()->mkNode(kind::OR, a, b); -} - -template <> inline -Node mkOr(const std::vector& children) { - Assert (children.size()); - if (children.size() == 1) - return children[0]; - return NodeManager::currentNM()->mkNode(kind::OR, children); -} - - -template <> inline -Node mkAnd(Node a, Node b) { - return NodeManager::currentNM()->mkNode(kind::AND, a, b); -} - -template <> inline -Node mkAnd(const std::vector& children) { - Assert (children.size()); - if (children.size() == 1) - return children[0]; - return NodeManager::currentNM()->mkNode(kind::AND, children); -} - - -template <> inline -Node mkXor(Node a, Node b) { - return NodeManager::currentNM()->mkNode(kind::XOR, a, b); -} - -template <> inline -Node mkIff(Node a, Node b) { - return NodeManager::currentNM()->mkNode(kind::EQUAL, a, b); -} - -template <> inline -Node mkIte(Node cond, Node a, Node b) { - return NodeManager::currentNM()->mkNode(kind::ITE, cond, a, b); -} - -/* - Various helper functions that get called by the bitblasting procedures - */ - -template -void inline extractBits(const std::vector& b, std::vector& dest, unsigned lo, unsigned hi) { - Assert ( lo < b.size() && hi < b.size() && lo <= hi); - for (unsigned i = lo; i <= hi; ++i) { - dest.push_back(b[i]); - } -} - -template -void inline negateBits(const std::vector& bits, std::vector& negated_bits) { - for(unsigned i = 0; i < bits.size(); ++i) { - negated_bits.push_back(mkNot(bits[i])); - } -} - -template -bool inline isZero(const std::vector& bits) { - for(unsigned i = 0; i < bits.size(); ++i) { - if(bits[i] != mkFalse()) { - return false; - } - } - return true; -} - -template -void inline rshift(std::vector& bits, unsigned amount) { - for (unsigned i = 0; i < bits.size() - amount; ++i) { - bits[i] = bits[i+amount]; - } - for(unsigned i = bits.size() - amount; i < bits.size(); ++i) { - bits[i] = mkFalse(); - } -} - -template -void inline lshift(std::vector& bits, unsigned amount) { - for (int i = (int)bits.size() - 1; i >= (int)amount ; --i) { - bits[i] = bits[i-amount]; - } - for(unsigned i = 0; i < amount; ++i) { - bits[i] = mkFalse(); - } -} - -template -void inline makeZero(std::vector& bits, unsigned width) { - Assert(bits.size() == 0); - for(unsigned i = 0; i < width; ++i) { - bits.push_back(mkFalse()); - } -} - - -/** - * Constructs a simple ripple carry adder - * - * @param a first term to be added - * @param b second term to be added - * @param res the result - * @param carry the carry-in bit - * - * @return the carry-out - */ -template -T inline rippleCarryAdder(const std::vector&a, const std::vector& b, std::vector& res, T carry) { - Assert(a.size() == b.size() && res.size() == 0); - - for (unsigned i = 0 ; i < a.size(); ++i) { - T sum = mkXor(mkXor(a[i], b[i]), carry); - carry = mkOr( mkAnd(a[i], b[i]), - mkAnd( mkXor(a[i], b[i]), - carry)); - res.push_back(sum); - } - - return carry; -} - -template -inline void shiftAddMultiplier(const std::vector&a, const std::vector&b, std::vector& res) { - - for (unsigned i = 0; i < a.size(); ++i) { - res.push_back(mkAnd(b[0], a[i])); - } - - for(unsigned k = 1; k < res.size(); ++k) { - T carry_in = mkFalse(); - T carry_out; - for(unsigned j = 0; j < res.size() -k; ++j) { - T aj = mkAnd(b[k], a[j]); - carry_out = mkOr(mkAnd(res[j+k], aj), - mkAnd( mkXor(res[j+k], aj), carry_in)); - res[j+k] = mkXor(mkXor(res[j+k], aj), carry_in); - carry_in = carry_out; - } - } -} - -template -T inline uLessThanBB(const std::vector&a, const std::vector& b, bool orEqual) { - Assert (a.size() && b.size()); - - T res = mkAnd(mkNot(a[0]), b[0]); - - if(orEqual) { - res = mkOr(res, mkIff(a[0], b[0])); - } - - for (unsigned i = 1; i < a.size(); ++i) { - // a < b iff ( a[i] <-> b[i] AND a[i-1:0] < b[i-1:0]) OR (~a[i] AND b[i]) - res = mkOr(mkAnd(mkIff(a[i], b[i]), res), - mkAnd(mkNot(a[i]), b[i])); - } - return res; -} - -template -T inline sLessThanBB(const std::vector&a, const std::vector& b, bool orEqual) { - Assert (a.size() && b.size()); - if (a.size() == 1) { - if(orEqual) { - return mkOr(mkIff(a[0], b[0]), - mkAnd(a[0], mkNot(b[0]))); - } - - return mkAnd(a[0], mkNot(b[0])); - } - unsigned n = a.size() - 1; - std::vector a1, b1; - extractBits(a, a1, 0, n-1); - extractBits(b, b1, 0, n-1); - - // unsigned comparison of the first n-1 bits - T ures = uLessThanBB(a1, b1, orEqual); - T res = mkOr(// a b have the same sign - mkAnd(mkIff(a[n], b[n]), - ures), - // a is negative and b positive - mkAnd(a[n], - mkNot(b[n]))); - return res; -} - - -} -} -} - -#endif 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/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp deleted file mode 100644 index 25610af2b..000000000 --- a/src/theory/bv/eager_bitblaster.cpp +++ /dev/null @@ -1,269 +0,0 @@ -/********************* */ -/*! \file eager_bitblaster.cpp - ** \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 eager bv solver. - **/ - -#include "cvc4_private.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" - -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_bv(theory_bv), - d_bbAtoms(), - d_variables(), - d_notify(NULL) { - d_bitblastingRegistrar = new BitblastingRegistrar(this); - d_nullContext = new context::Context(); - - 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; - break; - } - case SAT_SOLVER_CADICAL: - d_satSolver = prop::SatSolverFactory::createCadical( - smtStatisticsRegistry(), "EagerBitblaster"); - break; - case SAT_SOLVER_CRYPTOMINISAT: - d_satSolver = 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; -} - -EagerBitblaster::~EagerBitblaster() { - delete d_cnfStream; - delete d_satSolver; - delete d_notify; - delete d_nullContext; - delete d_bitblastingRegistrar; -} - -void EagerBitblaster::bbFormula(TNode node) { - d_cnfStream->convertAndAssert(node, false, false, RULE_INVALID, - TNode::null()); -} - -/** - * Bitblasts the atom, assigns it a marker literal, adding it to the SAT solver - * NOTE: duplicate clauses are not detected because of marker literal - * @param node the atom to be bitblasted - * - */ -void EagerBitblaster::bbAtom(TNode node) -{ - node = node.getKind() == kind::NOT ? node[0] : node; - if (node.getKind() == kind::BITVECTOR_BITOF) return; - if (hasBBAtom(node)) - { - return; - } - - Debug("bitvector-bitblast") << "Bitblasting node " << node << "\n"; - - // the bitblasted definition of the atom - Node normalized = Rewriter::rewrite(node); - Node atom_bb = - normalized.getKind() != kind::CONST_BOOLEAN - ? d_atomBBStrategies[normalized.getKind()](normalized, this) - : normalized; - - if (!options::proof()) - { - atom_bb = Rewriter::rewrite(atom_bb); - } - - // asserting that the atom is true iff the definition holds - Node atom_definition = - NodeManager::currentNM()->mkNode(kind::EQUAL, node, atom_bb); - - AlwaysAssert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER); - storeBBAtom(node, atom_bb); - d_cnfStream->convertAndAssert( - atom_definition, false, false, RULE_INVALID, TNode::null()); -} - -void EagerBitblaster::storeBBAtom(TNode atom, Node atom_bb) { - if (d_bvp) { - d_bvp->registerAtomBB(atom.toExpr(), atom_bb.toExpr()); - } - d_bbAtoms.insert(atom); -} - -void EagerBitblaster::storeBBTerm(TNode node, const Bits& bits) { - if (d_bvp) { - d_bvp->registerTermBB(node.toExpr()); - } - d_termCache.insert(std::make_pair(node, bits)); -} - -bool EagerBitblaster::hasBBAtom(TNode atom) const { - return d_bbAtoms.find(atom) != d_bbAtoms.end(); -} - -void EagerBitblaster::bbTerm(TNode node, Bits& bits) { - Assert(node.getType().isBitVector()); - - if (hasBBTerm(node)) { - getBBTerm(node, bits); - return; - } - - d_bv->spendResource(options::bitblastStep()); - Debug("bitvector-bitblast") << "Bitblasting node " << node << "\n"; - - d_termBBStrategies[node.getKind()](node, bits, this); - - Assert(bits.size() == utils::getSize(node)); - - storeBBTerm(node, bits); -} - -void EagerBitblaster::makeVariable(TNode var, Bits& bits) { - Assert(bits.size() == 0); - for (unsigned i = 0; i < utils::getSize(var); ++i) { - bits.push_back(utils::mkBitOf(var, i)); - } - d_variables.insert(var); -} - -Node EagerBitblaster::getBBAtom(TNode node) const { return node; } - -/** - * Calls the solve method for the Sat Solver. - * - * @return true for sat, and false for unsat - */ - -bool EagerBitblaster::solve() { - if (Trace.isOn("bitvector")) { - Trace("bitvector") << "EagerBitblaster::solve(). \n"; - } - Debug("bitvector") << "EagerBitblaster::solve(). \n"; - // TODO: clear some memory - // if (something) { - // NodeManager* nm= NodeManager::currentNM(); - // Rewriter::garbageCollect(); - // nm->reclaimZombiesUntil(options::zombieHuntThreshold()); - // } - return prop::SAT_VALUE_TRUE == d_satSolver->solve(); -} - -/** - * Returns the value a is currently assigned to in the SAT solver - * or null if the value is completely unassigned. - * - * @param a - * @param fullModel whether to create a "full model," i.e., add - * constants to equivalence classes that don't already have them - * - * @return - */ -Node EagerBitblaster::getModelFromSatSolver(TNode a, bool fullModel) { - if (!hasBBTerm(a)) { - return fullModel ? utils::mkConst(utils::getSize(a), 0u) : Node(); - } - - Bits bits; - getBBTerm(a, bits); - Integer value(0); - for (int i = bits.size() - 1; i >= 0; --i) { - prop::SatValue bit_value; - if (d_cnfStream->hasLiteral(bits[i])) { - prop::SatLiteral bit = d_cnfStream->getLiteral(bits[i]); - bit_value = d_satSolver->value(bit); - Assert(bit_value != prop::SAT_VALUE_UNKNOWN); - } else { - if (!fullModel) return Node(); - // unconstrained bits default to false - bit_value = prop::SAT_VALUE_FALSE; - } - Integer bit_int = - bit_value == prop::SAT_VALUE_TRUE ? Integer(1) : Integer(0); - value = value * 2 + bit_int; - } - return utils::mkConst(bits.size(), value); -} - -bool EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) -{ - TNodeSet::iterator it = d_variables.begin(); - for (; it != d_variables.end(); ++it) { - TNode var = *it; - if (d_bv->isLeaf(var) || isSharedTerm(var) || - (var.isVar() && var.getType().isBoolean())) { - // only shared terms could not have been bit-blasted - Assert(hasBBTerm(var) || isSharedTerm(var)); - - Node const_value = getModelFromSatSolver(var, true); - - if (const_value != Node()) { - Debug("bitvector-model") - << "EagerBitblaster::collectModelInfo (assert (= " << var << " " - << const_value << "))\n"; - if (!m->assertEquality(var, const_value, true)) - { - return false; - } - } - } - } - return true; -} - -void EagerBitblaster::setProofLog(BitVectorProof* bvp) { - d_bvp = bvp; - d_satSolver->setProofLog(bvp); - bvp->initCnfProof(d_cnfStream, d_nullContext); -} - -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; */ diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp deleted file mode 100644 index 189898c0c..000000000 --- a/src/theory/bv/lazy_bitblaster.cpp +++ /dev/null @@ -1,603 +0,0 @@ -/********************* */ -/*! \file lazy_bitblaster.cpp - ** \verbatim - ** Top contributors (to current version): - ** Liana Hadarean, Aina Niemetz, Tim King - ** 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 "bitblaster_template.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/theory_bv.h" -#include "theory/rewriter.h" -#include "theory/theory_model.h" -#include "proof/bitvector_proof.h" -#include "proof/proof_manager.h" -#include "theory/bv/theory_bv_utils.h" - -namespace CVC4 { -namespace theory { -namespace bv { - -namespace { - -/* Determine the number of uncached nodes that a given node consists of. */ -uint64_t numNodes(TNode node, utils::NodeSet& seen) -{ - std::vector stack; - uint64_t res = 0; - - stack.push_back(node); - while (!stack.empty()) - { - Node n = stack.back(); - stack.pop_back(); - - if (seen.find(n) != seen.end()) continue; - - res += 1; - seen.insert(n); - stack.insert(stack.end(), n.begin(), n.end()); - } - return res; -} -} - - -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_satSolverNotify = d_emptyNotify ? - (prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() : - (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, bv, - this); - - d_satSolver->setNotify(d_satSolverNotify); -} - -void TLazyBitblaster::setAbstraction(AbstractionModule* abs) { - d_abstraction = abs; -} - -TLazyBitblaster::~TLazyBitblaster() -{ - delete d_cnfStream; - delete d_nullRegistrar; - delete d_nullContext; - delete d_satSolver; - delete d_satSolverNotify; - d_assertedAtoms->deleteSelf(); - d_explanations->deleteSelf(); -} - - -/** - * Bitblasts the atom, assigns it a marker literal, adding it to the SAT solver - * NOTE: duplicate clauses are not detected because of marker literal - * @param node the atom to be bitblasted - * - */ -void TLazyBitblaster::bbAtom(TNode node) -{ - NodeManager* nm = NodeManager::currentNM(); - node = node.getKind() == kind::NOT ? node[0] : node; - - if (hasBBAtom(node)) - { - return; - } - - // make sure it is marked as an atom - addAtom(node); - - Debug("bitvector-bitblast") << "Bitblasting node " << node << "\n"; - ++d_statistics.d_numAtoms; - - /// if we are using bit-vector abstraction bit-blast the original - /// interpretation - if (options::bvAbstraction() && d_abstraction != NULL - && d_abstraction->isAbstraction(node)) - { - // node must be of the form P(args) = bv1 - Node expansion = Rewriter::rewrite(d_abstraction->getInterpretation(node)); - - Node atom_bb; - if (expansion.getKind() == kind::CONST_BOOLEAN) - { - atom_bb = expansion; - } - else - { - Assert(expansion.getKind() == kind::AND); - std::vector atoms; - for (unsigned i = 0; i < expansion.getNumChildren(); ++i) - { - Node normalized_i = Rewriter::rewrite(expansion[i]); - Node atom_i = - normalized_i.getKind() != kind::CONST_BOOLEAN - ? Rewriter::rewrite(d_atomBBStrategies[normalized_i.getKind()]( - normalized_i, this)) - : normalized_i; - atoms.push_back(atom_i); - } - atom_bb = utils::mkAnd(atoms); - } - Assert(!atom_bb.isNull()); - Node atom_definition = nm->mkNode(kind::EQUAL, node, atom_bb); - storeBBAtom(node, atom_bb); - d_cnfStream->convertAndAssert( - atom_definition, false, false, RULE_INVALID, TNode::null()); - return; - } - - // the bitblasted definition of the atom - Node normalized = Rewriter::rewrite(node); - Node atom_bb = - normalized.getKind() != kind::CONST_BOOLEAN - ? d_atomBBStrategies[normalized.getKind()](normalized, this) - : normalized; - - if (!options::proof()) - { - atom_bb = Rewriter::rewrite(atom_bb); - } - - // asserting that the atom is true iff the definition holds - Node atom_definition = nm->mkNode(kind::EQUAL, node, atom_bb); - storeBBAtom(node, atom_bb); - d_cnfStream->convertAndAssert( - atom_definition, false, false, RULE_INVALID, TNode::null()); -} - -void TLazyBitblaster::storeBBAtom(TNode atom, Node atom_bb) { - // No need to store the definition for the lazy bit-blaster (unless proofs are enabled). - if( d_bvp != NULL ){ - d_bvp->registerAtomBB(atom.toExpr(), atom_bb.toExpr()); - } - d_bbAtoms.insert(atom); -} - -void TLazyBitblaster::storeBBTerm(TNode node, const Bits& bits) { - if( d_bvp ){ d_bvp->registerTermBB(node.toExpr()); } - d_termCache.insert(std::make_pair(node, bits)); -} - - -bool TLazyBitblaster::hasBBAtom(TNode atom) const { - return d_bbAtoms.find(atom) != d_bbAtoms.end(); -} - - -void TLazyBitblaster::makeVariable(TNode var, Bits& bits) { - Assert(bits.size() == 0); - for (unsigned i = 0; i < utils::getSize(var); ++i) { - bits.push_back(utils::mkBitOf(var, i)); - } - d_variables.insert(var); -} - -uint64_t TLazyBitblaster::computeAtomWeight(TNode node, NodeSet& seen) -{ - node = node.getKind() == kind::NOT ? node[0] : node; - if (!utils::isBitblastAtom(node)) { return 0; } - Node atom_bb = - Rewriter::rewrite(d_atomBBStrategies[node.getKind()](node, this)); - uint64_t size = numNodes(atom_bb, seen); - return size; -} - -// cnf conversion ensures the atom represents itself -Node TLazyBitblaster::getBBAtom(TNode node) const { - return node; -} - -void TLazyBitblaster::bbTerm(TNode node, Bits& bits) { - - if (hasBBTerm(node)) { - getBBTerm(node, bits); - return; - } - Assert( node.getType().isBitVector() ); - - d_bv->spendResource(options::bitblastStep()); - Debug("bitvector-bitblast") << "Bitblasting term " << node <<"\n"; - ++d_statistics.d_numTerms; - - d_termBBStrategies[node.getKind()] (node, bits,this); - - Assert (bits.size() == utils::getSize(node)); - - storeBBTerm(node, bits); -} -/// Public methods - -void TLazyBitblaster::addAtom(TNode atom) { - d_cnfStream->ensureLiteral(atom); - prop::SatLiteral lit = d_cnfStream->getLiteral(atom); - d_satSolver->addMarkerLiteral(lit); -} - -void TLazyBitblaster::explain(TNode atom, std::vector& explanation) { - prop::SatLiteral lit = d_cnfStream->getLiteral(atom); - - ++(d_statistics.d_numExplainedPropagations); - if (options::bvEagerExplanations()) { - Assert (d_explanations->find(lit) != d_explanations->end()); - const std::vector& literal_explanation = (*d_explanations)[lit].get(); - for (unsigned i = 0; i < literal_explanation.size(); ++i) { - explanation.push_back(d_cnfStream->getNode(literal_explanation[i])); - } - return; - } - - std::vector literal_explanation; - d_satSolver->explain(lit, literal_explanation); - for (unsigned i = 0; i < literal_explanation.size(); ++i) { - explanation.push_back(d_cnfStream->getNode(literal_explanation[i])); - } -} - - -/* - * Asserts the clauses corresponding to the atom to the Sat Solver - * by turning on the marker literal (i.e. setting it to false) - * @param node the atom to be asserted - * - */ - -bool TLazyBitblaster::propagate() { - return d_satSolver->propagate() == prop::SAT_VALUE_TRUE; -} - -bool TLazyBitblaster::assertToSat(TNode lit, bool propagate) { - // strip the not - TNode atom; - if (lit.getKind() == kind::NOT) { - atom = lit[0]; - } else { - atom = lit; - } - Assert( utils::isBitblastAtom( atom ) ); - - Assert (hasBBAtom(atom)); - - prop::SatLiteral markerLit = d_cnfStream->getLiteral(atom); - - if(lit.getKind() == kind::NOT) { - markerLit = ~markerLit; - } - - Debug("bitvector-bb") << "TheoryBV::TLazyBitblaster::assertToSat asserting node: " << atom <<"\n"; - Debug("bitvector-bb") << "TheoryBV::TLazyBitblaster::assertToSat with literal: " << markerLit << "\n"; - - prop::SatValue ret = d_satSolver->assertAssumption(markerLit, propagate); - - d_assertedAtoms->push_back(markerLit); - - return ret == prop::SAT_VALUE_TRUE || ret == prop::SAT_VALUE_UNKNOWN; -} - -/** - * Calls the solve method for the Sat Solver. - * passing it the marker literals to be asserted - * - * @return true for sat, and false for unsat - */ - -bool TLazyBitblaster::solve() { - if (Trace.isOn("bitvector")) { - Trace("bitvector") << "TLazyBitblaster::solve() asserted atoms "; - context::CDList::const_iterator it = d_assertedAtoms->begin(); - for (; it != d_assertedAtoms->end(); ++it) { - Trace("bitvector") << " " << d_cnfStream->getNode(*it) << "\n"; - } - } - Debug("bitvector") << "TLazyBitblaster::solve() asserted atoms " << d_assertedAtoms->size() <<"\n"; - d_fullModelAssertionLevel.set(d_bv->numAssertions()); - return prop::SAT_VALUE_TRUE == d_satSolver->solve(); -} - -prop::SatValue TLazyBitblaster::solveWithBudget(unsigned long budget) { - if (Trace.isOn("bitvector")) { - Trace("bitvector") << "TLazyBitblaster::solveWithBudget() asserted atoms "; - context::CDList::const_iterator it = d_assertedAtoms->begin(); - for (; it != d_assertedAtoms->end(); ++it) { - Trace("bitvector") << " " << d_cnfStream->getNode(*it) << "\n"; - } - } - Debug("bitvector") << "TLazyBitblaster::solveWithBudget() asserted atoms " << d_assertedAtoms->size() <<"\n"; - return d_satSolver->solve(budget); -} - -void TLazyBitblaster::getConflict(std::vector& conflict) -{ - NodeManager* nm = NodeManager::currentNM(); - prop::SatClause conflictClause; - d_satSolver->getUnsatCore(conflictClause); - - for (unsigned i = 0; i < conflictClause.size(); i++) - { - prop::SatLiteral lit = conflictClause[i]; - TNode atom = d_cnfStream->getNode(lit); - Node not_atom; - if (atom.getKind() == kind::NOT) - { - not_atom = atom[0]; - } - else - { - not_atom = nm->mkNode(kind::NOT, atom); - } - conflict.push_back(not_atom); - } -} - -TLazyBitblaster::Statistics::Statistics(const std::string& prefix) : - d_numTermClauses(prefix + "::NumTermSatClauses", 0), - d_numAtomClauses(prefix + "::NumAtomSatClauses", 0), - d_numTerms(prefix + "::NumBitblastedTerms", 0), - d_numAtoms(prefix + "::NumBitblastedAtoms", 0), - d_numExplainedPropagations(prefix + "::NumExplainedPropagations", 0), - d_numBitblastingPropagations(prefix + "::NumBitblastingPropagations", 0), - d_bitblastTimer(prefix + "::BitblastTimer") -{ - smtStatisticsRegistry()->registerStat(&d_numTermClauses); - smtStatisticsRegistry()->registerStat(&d_numAtomClauses); - smtStatisticsRegistry()->registerStat(&d_numTerms); - smtStatisticsRegistry()->registerStat(&d_numAtoms); - smtStatisticsRegistry()->registerStat(&d_numExplainedPropagations); - smtStatisticsRegistry()->registerStat(&d_numBitblastingPropagations); - smtStatisticsRegistry()->registerStat(&d_bitblastTimer); -} - - -TLazyBitblaster::Statistics::~Statistics() { - smtStatisticsRegistry()->unregisterStat(&d_numTermClauses); - smtStatisticsRegistry()->unregisterStat(&d_numAtomClauses); - smtStatisticsRegistry()->unregisterStat(&d_numTerms); - smtStatisticsRegistry()->unregisterStat(&d_numAtoms); - smtStatisticsRegistry()->unregisterStat(&d_numExplainedPropagations); - smtStatisticsRegistry()->unregisterStat(&d_numBitblastingPropagations); - smtStatisticsRegistry()->unregisterStat(&d_bitblastTimer); -} - -bool TLazyBitblaster::MinisatNotify::notify(prop::SatLiteral lit) { - if(options::bvEagerExplanations()) { - // compute explanation - if (d_lazyBB->d_explanations->find(lit) == d_lazyBB->d_explanations->end()) { - std::vector literal_explanation; - d_lazyBB->d_satSolver->explain(lit, literal_explanation); - d_lazyBB->d_explanations->insert(lit, literal_explanation); - } else { - // we propagated it at a lower level - return true; - } - } - ++(d_lazyBB->d_statistics.d_numBitblastingPropagations); - TNode atom = d_cnf->getNode(lit); - return d_bv->storePropagation(atom, SUB_BITBLAST); -} - -void TLazyBitblaster::MinisatNotify::notify(prop::SatClause& clause) { - if (clause.size() > 1) { - NodeBuilder<> lemmab(kind::OR); - for (unsigned i = 0; i < clause.size(); ++ i) { - lemmab << d_cnf->getNode(clause[i]); - } - Node lemma = lemmab; - d_bv->d_out->lemma(lemma); - } else { - d_bv->d_out->lemma(d_cnf->getNode(clause[0])); - } -} - -void TLazyBitblaster::MinisatNotify::spendResource(unsigned amount) -{ - d_bv->spendResource(amount); -} - -void TLazyBitblaster::MinisatNotify::safePoint(unsigned amount) -{ - d_bv->d_out->safePoint(amount); -} - -EqualityStatus TLazyBitblaster::getEqualityStatus(TNode a, TNode b) -{ - int numAssertions = d_bv->numAssertions(); - Debug("bv-equality-status") - << "TLazyBitblaster::getEqualityStatus " << a << " = " << b << "\n"; - Debug("bv-equality-status") - << "BVSatSolver has full model? " - << (d_fullModelAssertionLevel.get() == numAssertions) << "\n"; - - // First check if it trivially rewrites to false/true - Node a_eq_b = - Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL, a, b)); - - if (a_eq_b == utils::mkFalse()) return theory::EQUALITY_FALSE; - if (a_eq_b == utils::mkTrue()) return theory::EQUALITY_TRUE; - - if (d_fullModelAssertionLevel.get() != numAssertions) - { - return theory::EQUALITY_UNKNOWN; - } - - // Check if cache is valid (invalidated in check and pops) - if (d_bv->d_invalidateModelCache.get()) - { - invalidateModelCache(); - } - d_bv->d_invalidateModelCache.set(false); - - Node a_value = getTermModel(a, true); - Node b_value = getTermModel(b, true); - - Assert(a_value.isConst() && b_value.isConst()); - - if (a_value == b_value) - { - Debug("bv-equality-status") << "theory::EQUALITY_TRUE_IN_MODEL\n"; - return theory::EQUALITY_TRUE_IN_MODEL; - } - Debug("bv-equality-status") << "theory::EQUALITY_FALSE_IN_MODEL\n"; - return theory::EQUALITY_FALSE_IN_MODEL; -} - -bool TLazyBitblaster::isSharedTerm(TNode node) { - return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end(); -} - -bool TLazyBitblaster::hasValue(TNode a) { - Assert (hasBBTerm(a)); - Bits bits; - getBBTerm(a, bits); - for (int i = bits.size() -1; i >= 0; --i) { - prop::SatValue bit_value; - if (d_cnfStream->hasLiteral(bits[i])) { - prop::SatLiteral bit = d_cnfStream->getLiteral(bits[i]); - bit_value = d_satSolver->value(bit); - if (bit_value == prop::SAT_VALUE_UNKNOWN) - return false; - } else { - return false; - } - } - return true; -} -/** - * Returns the value a is currently assigned to in the SAT solver - * or null if the value is completely unassigned. - * - * @param a - * @param fullModel whether to create a "full model," i.e., add - * constants to equivalence classes that don't already have them - * - * @return - */ -Node TLazyBitblaster::getModelFromSatSolver(TNode a, bool fullModel) { - if (!hasBBTerm(a)) { - return fullModel? utils::mkConst(utils::getSize(a), 0u) : Node(); - } - - Bits bits; - getBBTerm(a, bits); - Integer value(0); - for (int i = bits.size() -1; i >= 0; --i) { - prop::SatValue bit_value; - if (d_cnfStream->hasLiteral(bits[i])) { - prop::SatLiteral bit = d_cnfStream->getLiteral(bits[i]); - bit_value = d_satSolver->value(bit); - Assert (bit_value != prop::SAT_VALUE_UNKNOWN); - } else { - if (!fullModel) return Node(); - // unconstrained bits default to false - bit_value = prop::SAT_VALUE_FALSE; - } - Integer bit_int = bit_value == prop::SAT_VALUE_TRUE ? Integer(1) : Integer(0); - value = value * 2 + bit_int; - } - return utils::mkConst(bits.size(), value); -} - -bool TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) -{ - std::set termSet; - d_bv->computeRelevantTerms(termSet); - - for (std::set::const_iterator it = termSet.begin(); it != termSet.end(); ++it) { - TNode var = *it; - // not actually a leaf of the bit-vector theory - if (d_variables.find(var) == d_variables.end()) - continue; - - Assert (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)); - // only shared terms could not have been bit-blasted - Assert (hasBBTerm(var) || isSharedTerm(var)); - - Node const_value = getModelFromSatSolver(var, true); - Assert (const_value.isNull() || const_value.isConst()); - if(const_value != Node()) { - Debug("bitvector-model") << "TLazyBitblaster::collectModelInfo (assert (= " - << var << " " - << const_value << "))\n"; - if (!m->assertEquality(var, const_value, true)) - { - return false; - } - } - } - return true; -} - -void TLazyBitblaster::setProofLog( BitVectorProof * bvp ){ - d_bvp = bvp; - d_satSolver->setProofLog( bvp ); - bvp->initCnfProof(d_cnfStream, d_nullContext); -} - -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(); - d_explanations = new(true) ExplanationMap(d_ctx); - d_bbAtoms.clear(); - d_variables.clear(); - d_termCache.clear(); - - 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 */ -- cgit v1.2.3