From: lianah Date: Sat, 21 Jun 2014 21:45:31 +0000 (-0400) Subject: fixed build failure X-Git-Tag: cvc5-1.0.0~6756 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7b8c765e84987ae90226f9f7244492318fa85817;p=cvc5.git fixed build failure --- diff --git a/src/Makefile.am b/src/Makefile.am index fb7994699..805ed6cb7 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -188,9 +188,9 @@ libcvc4_la_SOURCES = \ theory/bv/bv_inequality_graph.cpp \ theory/bv/bitblast_strategies_template.h \ theory/bv/bitblaster_template.h \ - theory/bv/lazy_bitblaster.h \ - theory/bv/eager_bitblaster.h \ - theory/bv/aig_bitblaster.h \ + theory/bv/lazy_bitblaster.cpp \ + theory/bv/eager_bitblaster.cpp \ + theory/bv/aig_bitblaster.cpp \ theory/bv/bv_eager_solver.h \ theory/bv/bv_eager_solver.cpp \ theory/bv/slicer.h \ diff --git a/src/theory/bv/aig_bitblaster.cpp b/src/theory/bv/aig_bitblaster.cpp new file mode 100644 index 000000000..70d69a138 --- /dev/null +++ b/src/theory/bv/aig_bitblaster.cpp @@ -0,0 +1,653 @@ +/********************* */ +/*! \file aig_bitblaster.cpp + ** \verbatim + ** Original author: Liana Hadarean + ** Major contributors: none + ** Minor contributors (to current version): lianah + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief + ** + ** Bitblaster for the lazy bv solver. + **/ + +#include "cvc4_private.h" +#include "bitblaster_template.h" +#include "prop/cnf_stream.h" +#include "prop/sat_solver_factory.h" +#include "theory/bv/options.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(); + d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext, "AigBitblaster"); + MinisatEmptyNotify* notify = new MinisatEmptyNotify(); + d_satSolver->setNotify(notify); +} + +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::IFF: + { + Assert (node.getNumChildren() == 2); + Abc_Obj_t* child1 = bbFormula(node[0]); + Abc_Obj_t* child2 = bbFormula(node[1]); + + result = mkIff(child1, child2); + 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::VARIABLE: + case kind::SKOLEM: + { + result = mkInput(node); + break; + } + default: + 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; + } + + 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.getKind() == kind::VARIABLE || + input.getKind() == kind::SKOLEM))); + 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") +{ + StatisticsRegistry::registerStat(&d_numClauses); + StatisticsRegistry::registerStat(&d_numVariables); + StatisticsRegistry::registerStat(&d_simplificationTime); + StatisticsRegistry::registerStat(&d_cnfConversionTime); + StatisticsRegistry::registerStat(&d_solveTime); +} + +AigBitblaster::Statistics::~Statistics() { + StatisticsRegistry::unregisterStat(&d_numClauses); + StatisticsRegistry::unregisterStat(&d_numVariables); + StatisticsRegistry::unregisterStat(&d_simplificationTime); + StatisticsRegistry::unregisterStat(&d_cnfConversionTime); + StatisticsRegistry::unregisterStat(&d_solveTime); +} + +#else // CVC4_USE_ABC + +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() { + Unreachable(); + return NULL; +} + +template <> inline +Abc_Obj_t* mkFalse() { + Unreachable(); + return NULL; +} + +template <> inline +Abc_Obj_t* mkNot(Abc_Obj_t* a) { + Unreachable(); + return NULL; +} + +template <> inline +Abc_Obj_t* mkOr(Abc_Obj_t* a, Abc_Obj_t* b) { + Unreachable(); + return NULL; +} + +template <> inline +Abc_Obj_t* mkOr(const std::vector& children) { + Unreachable(); + return NULL; +} + + +template <> inline +Abc_Obj_t* mkAnd(Abc_Obj_t* a, Abc_Obj_t* b) { + Unreachable(); + return NULL; +} + +template <> inline +Abc_Obj_t* mkAnd(const std::vector& children) { + Unreachable(); + return NULL; +} + +template <> inline +Abc_Obj_t* mkXor(Abc_Obj_t* a, Abc_Obj_t* b) { + Unreachable(); + return NULL; +} + +template <> inline +Abc_Obj_t* mkIff(Abc_Obj_t* a, Abc_Obj_t* b) { + Unreachable(); + return NULL; +} + +template <> inline +Abc_Obj_t* mkIte(Abc_Obj_t* cond, Abc_Obj_t* a, Abc_Obj_t* b) { + Unreachable(); + return NULL; +} + +} /* 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() { + Unreachable(); + return NULL; +} + + +Abc_Aig_t* AigBitblaster::currentAigM() { + Unreachable(); + return NULL; +} + +AigBitblaster::~AigBitblaster() { + Unreachable(); +} + +Abc_Obj_t* AigBitblaster::bbFormula(TNode node) { + Unreachable(); + return NULL; +} + +void AigBitblaster::bbAtom(TNode node) { + Unreachable(); +} + +void AigBitblaster::bbTerm(TNode node, Bits& bits) { + Unreachable(); +} + + +void AigBitblaster::cacheAig(TNode node, Abc_Obj_t* aig) { + Unreachable(); +} +bool AigBitblaster::hasAig(TNode node) { + Unreachable(); + return false; +} +Abc_Obj_t* AigBitblaster::getAig(TNode node) { + Unreachable(); + return NULL; +} + +void AigBitblaster::makeVariable(TNode node, Bits& bits) { + Unreachable(); +} + +Abc_Obj_t* AigBitblaster::mkInput(TNode input) { + Unreachable(); + return NULL; +} + +bool AigBitblaster::hasInput(TNode input) { + Unreachable(); + return false; +} + +bool AigBitblaster::solve(TNode node) { + Unreachable(); + return false; +} +void AigBitblaster::simplifyAig() { + Unreachable(); +} + +void AigBitblaster::convertToCnfAndAssert() { + Unreachable(); +} + +void AigBitblaster::assertToSatSolver(Cnf_Dat_t* pCnf) { + Unreachable(); +} +bool AigBitblaster::hasBBAtom(TNode atom) const { + Unreachable(); + return false; +} + +void AigBitblaster::storeBBAtom(TNode atom, Abc_Obj_t* atom_bb) { + Unreachable(); +} + +Abc_Obj_t* AigBitblaster::getBBAtom(TNode atom) const { + Unreachable(); + return NULL; +} + +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") +{} + +AigBitblaster::Statistics::~Statistics() {} + +AigBitblaster::AigBitblaster() { + Unreachable(); +} +#endif // CVC4_USE_ABC diff --git a/src/theory/bv/aig_bitblaster.h b/src/theory/bv/aig_bitblaster.h deleted file mode 100644 index d1635f950..000000000 --- a/src/theory/bv/aig_bitblaster.h +++ /dev/null @@ -1,658 +0,0 @@ -/********************* */ -/*! \file aig_bitblaster.h - ** \verbatim - ** Original author: Liana Hadarean - ** Major contributors: none - ** Minor contributors (to current version): lianah - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief - ** - ** Bitblaster for the lazy bv solver. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__AIG__BITBLASTER_H -#define __CVC4__AIG__BITBLASTER_H - - -#include "bitblaster_template.h" -#include "prop/cnf_stream.h" -#include "prop/sat_solver_factory.h" -#include "theory/bv/options.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); -} - - -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(); - d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext, "AigBitblaster"); - MinisatEmptyNotify* notify = new MinisatEmptyNotify(); - d_satSolver->setNotify(notify); -} - -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::IFF: - { - Assert (node.getNumChildren() == 2); - Abc_Obj_t* child1 = bbFormula(node[0]); - Abc_Obj_t* child2 = bbFormula(node[1]); - - result = mkIff(child1, child2); - 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::VARIABLE: - case kind::SKOLEM: - { - result = mkInput(node); - break; - } - default: - 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; - } - - 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.getKind() == kind::VARIABLE || - input.getKind() == kind::SKOLEM))); - 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") -{ - StatisticsRegistry::registerStat(&d_numClauses); - StatisticsRegistry::registerStat(&d_numVariables); - StatisticsRegistry::registerStat(&d_simplificationTime); - StatisticsRegistry::registerStat(&d_cnfConversionTime); - StatisticsRegistry::registerStat(&d_solveTime); -} - -AigBitblaster::Statistics::~Statistics() { - StatisticsRegistry::unregisterStat(&d_numClauses); - StatisticsRegistry::unregisterStat(&d_numVariables); - StatisticsRegistry::unregisterStat(&d_simplificationTime); - StatisticsRegistry::unregisterStat(&d_cnfConversionTime); - StatisticsRegistry::unregisterStat(&d_solveTime); -} - - - -} /*bv namespace */ -} /* theory namespace */ -} /* CVC4 namespace*/ - - -#else // CVC4_USE_ABC - -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() { - Unreachable(); - return NULL; -} - -template <> inline -Abc_Obj_t* mkFalse() { - Unreachable(); - return NULL; -} - -template <> inline -Abc_Obj_t* mkNot(Abc_Obj_t* a) { - Unreachable(); - return NULL; -} - -template <> inline -Abc_Obj_t* mkOr(Abc_Obj_t* a, Abc_Obj_t* b) { - Unreachable(); - return NULL; -} - -template <> inline -Abc_Obj_t* mkOr(const std::vector& children) { - Unreachable(); - return NULL; -} - - -template <> inline -Abc_Obj_t* mkAnd(Abc_Obj_t* a, Abc_Obj_t* b) { - Unreachable(); - return NULL; -} - -template <> inline -Abc_Obj_t* mkAnd(const std::vector& children) { - Unreachable(); - return NULL; -} - -template <> inline -Abc_Obj_t* mkXor(Abc_Obj_t* a, Abc_Obj_t* b) { - Unreachable(); - return NULL; -} - -template <> inline -Abc_Obj_t* mkIff(Abc_Obj_t* a, Abc_Obj_t* b) { - Unreachable(); - return NULL; -} - -template <> inline -Abc_Obj_t* mkIte(Abc_Obj_t* cond, Abc_Obj_t* a, Abc_Obj_t* b) { - Unreachable(); - return NULL; -} - - -Abc_Ntk_t* AigBitblaster::abcAigNetwork = NULL; - -Abc_Ntk_t* AigBitblaster::currentAigNtk() { - Unreachable(); - return NULL; -} - - -Abc_Aig_t* AigBitblaster::currentAigM() { - Unreachable(); - return NULL; -} - -AigBitblaster::~AigBitblaster() { - Unreachable(); -} - -Abc_Obj_t* AigBitblaster::bbFormula(TNode node) { - Unreachable(); - return NULL; -} - -void AigBitblaster::bbAtom(TNode node) { - Unreachable(); -} - -void AigBitblaster::bbTerm(TNode node, Bits& bits) { - Unreachable(); -} - - -void AigBitblaster::cacheAig(TNode node, Abc_Obj_t* aig) { - Unreachable(); -} -bool AigBitblaster::hasAig(TNode node) { - Unreachable(); - return false; -} -Abc_Obj_t* AigBitblaster::getAig(TNode node) { - Unreachable(); - return NULL; -} - -void AigBitblaster::makeVariable(TNode node, Bits& bits) { - Unreachable(); -} - -Abc_Obj_t* AigBitblaster::mkInput(TNode input) { - Unreachable(); - return NULL; -} - -bool AigBitblaster::hasInput(TNode input) { - Unreachable(); - return false; -} - -bool AigBitblaster::solve(TNode node) { - Unreachable(); - return false; -} -void AigBitblaster::simplifyAig() { - Unreachable(); -} - -void AigBitblaster::convertToCnfAndAssert() { - Unreachable(); -} - -void AigBitblaster::assertToSatSolver(Cnf_Dat_t* pCnf) { - Unreachable(); -} -bool AigBitblaster::hasBBAtom(TNode atom) const { - Unreachable(); - return false; -} - -void AigBitblaster::storeBBAtom(TNode atom, Abc_Obj_t* atom_bb) { - Unreachable(); -} - -Abc_Obj_t* AigBitblaster::getBBAtom(TNode atom) const { - Unreachable(); - return NULL; -} - -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") -{} - -AigBitblaster::Statistics::~Statistics() {} - -AigBitblaster::AigBitblaster() { - Unreachable(); -} - -} // namespace bv -} // namespace theory -} // namespace CVC4 - - -#endif // CVC4_USE_ABC - -#endif // __CVC4__AIG__BITBLASTER_H diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h index 4b0465498..2b6037a12 100644 --- a/src/theory/bv/bitblaster_template.h +++ b/src/theory/bv/bitblaster_template.h @@ -27,6 +27,7 @@ #include "bitblast_strategies_template.h" #include "prop/sat_solver.h" #include "theory/valuation.h" +#include "theory/theory_registrar.h" class Abc_Obj_t_; typedef Abc_Obj_t_ Abc_Obj_t; @@ -263,6 +264,15 @@ public: void collectModelInfo(TheoryModel* m, bool fullModel); }; +class BitblastingRegistrar: public prop::Registrar { + EagerBitblaster* d_bitblaster; +public: + BitblastingRegistrar(EagerBitblaster* bb) + : d_bitblaster(bb) + {} + void preRegister(Node n); +}; /* class Registrar */ + class AigBitblaster : public TBitblaster { typedef std::hash_map TNodeAigMap; typedef std::hash_map NodeAigMap; diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp index 166d43e35..4e822d3c0 100644 --- a/src/theory/bv/bv_eager_solver.cpp +++ b/src/theory/bv/bv_eager_solver.cpp @@ -16,8 +16,7 @@ #include "theory/bv/bv_eager_solver.h" #include "theory/bv/bitblaster_template.h" -#include "theory/bv/eager_bitblaster.h" -#include "theory/bv/aig_bitblaster.h" +#include "theory/bv/options.h" using namespace std; using namespace CVC4; diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index ebe017ee1..ad5ff15b6 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -17,9 +17,10 @@ #include "theory/bv/bv_subtheory_bitblast.h" #include "theory/bv/theory_bv.h" #include "theory/bv/theory_bv_utils.h" -#include "theory/bv/lazy_bitblaster.h" +#include "theory/bv/bitblaster_template.h" #include "theory/bv/bv_quick_check.h" #include "theory/bv/options.h" +#include "theory/bv/abstraction.h" #include "theory/decision_attributes.h" #include "decision/options.h" diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp new file mode 100644 index 000000000..5b52fc241 --- /dev/null +++ b/src/theory/bv/eager_bitblaster.cpp @@ -0,0 +1,208 @@ +/********************* */ +/*! \file eager_bitblaster.cpp + ** \verbatim + ** Original author: Liana Hadarean + ** Major contributors: none + ** Minor contributors (to current version): lianah + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** 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/bitblaster_template.h" +#include "theory/bv/options.h" +#include "theory/theory_model.h" +#include "theory/bv/theory_bv.h" +#include "prop/cnf_stream.h" +#include "prop/sat_solver_factory.h" + + +using namespace CVC4; +using namespace CVC4::theory; +using namespace CVC4::theory::bv; + +void BitblastingRegistrar::preRegister(Node n) { + d_bitblaster->bbAtom(n); +}; + +EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv) + : TBitblaster() + , d_bv(theory_bv) + , d_bbAtoms() + , d_variables() +{ + d_bitblastingRegistrar = new BitblastingRegistrar(this); + d_nullContext = new context::Context(); + + d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext, "EagerBitblaster"); + d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_bitblastingRegistrar, d_nullContext); + + MinisatEmptyNotify* notify = new MinisatEmptyNotify(); + d_satSolver->setNotify(notify); +} + +EagerBitblaster::~EagerBitblaster() { + delete d_cnfStream; + delete d_satSolver; + delete d_nullContext; + delete d_bitblastingRegistrar; +} + +void EagerBitblaster::bbFormula(TNode node) { + d_cnfStream->convertAndAssert(node, false, false); +} + +/** + * 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 ? + Rewriter::rewrite(d_atomBBStrategies[normalized.getKind()](normalized, this)) : + normalized; + // asserting that the atom is true iff the definition holds + Node atom_definition = utils::mkNode(kind::IFF, node, atom_bb); + + AlwaysAssert (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER); + storeBBAtom(node, atom_definition); + d_cnfStream->convertAndAssert(atom_definition, false, false); +} + +void EagerBitblaster::storeBBAtom(TNode atom, Node atom_bb) { + // no need to store the definition for the lazy bit-blaster + d_bbAtoms.insert(atom); +} + +bool EagerBitblaster::hasBBAtom(TNode atom) const { + return d_bbAtoms.find(atom) != d_bbAtoms.end(); +} + +void EagerBitblaster::bbTerm(TNode node, Bits& bits) { + if (hasBBTerm(node)) { + getBBTerm(node, bits); + return; + } + + 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::getVarValue(TNode a, bool fullModel) { + if (!hasBBTerm(a)) { + Assert(isSharedTerm(a)); + return 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 { + // the bit is unconstrainted so we can give it an arbitrary value + 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(BitVector(bits.size(), value)); +} + + +void EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) { + TNodeSet::const_iterator it = d_variables.begin(); + for (; it!= d_variables.end(); ++it) { + TNode var = *it; + if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)) { + Node const_value = getVarValue(var, fullModel); + if(const_value == Node()) { + if( fullModel ){ + // if the value is unassigned just set it to zero + const_value = utils::mkConst(BitVector(utils::getSize(var), 0u)); + } + } + if(const_value != Node()) { + Debug("bitvector-model") << "TLazyBitblaster::collectModelInfo (assert (= " + << var << " " + << const_value << "))\n"; + m->assertEquality(var, const_value, true); + } + } + } +} + +bool EagerBitblaster::isSharedTerm(TNode node) { + return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end(); +} diff --git a/src/theory/bv/eager_bitblaster.h b/src/theory/bv/eager_bitblaster.h deleted file mode 100644 index 91ef866bd..000000000 --- a/src/theory/bv/eager_bitblaster.h +++ /dev/null @@ -1,230 +0,0 @@ -/********************* */ -/*! \file eager_bitblaster.h - ** \verbatim - ** Original author: Liana Hadarean - ** Major contributors: none - ** Minor contributors (to current version): lianah - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief - ** - ** Bitblaster for the lazy bv solver. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__EAGER__BITBLASTER_H -#define __CVC4__EAGER__BITBLASTER_H - - -#include "theory/theory_registrar.h" -#include "theory/bv/bitblaster_template.h" -#include "theory/bv/options.h" -#include "theory/theory_model.h" -#include "prop/cnf_stream.h" -#include "prop/sat_solver_factory.h" - - -namespace CVC4 { -namespace theory { -namespace bv { - - -class BitblastingRegistrar: public prop::Registrar { - EagerBitblaster* d_bitblaster; -public: - BitblastingRegistrar(EagerBitblaster* bb) - : d_bitblaster(bb) - {} - void preRegister(Node n) { - d_bitblaster->bbAtom(n); - }; - -};/* class Registrar */ - -EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv) - : TBitblaster() - , d_bv(theory_bv) - , d_bbAtoms() - , d_variables() -{ - d_bitblastingRegistrar = new BitblastingRegistrar(this); - d_nullContext = new context::Context(); - - d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext, "EagerBitblaster"); - d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_bitblastingRegistrar, d_nullContext); - - MinisatEmptyNotify* notify = new MinisatEmptyNotify(); - d_satSolver->setNotify(notify); -} - -EagerBitblaster::~EagerBitblaster() { - delete d_cnfStream; - delete d_satSolver; - delete d_nullContext; - delete d_bitblastingRegistrar; -} - -void EagerBitblaster::bbFormula(TNode node) { - d_cnfStream->convertAndAssert(node, false, false); -} - -/** - * 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 ? - Rewriter::rewrite(d_atomBBStrategies[normalized.getKind()](normalized, this)) : - normalized; - // asserting that the atom is true iff the definition holds - Node atom_definition = utils::mkNode(kind::IFF, node, atom_bb); - - AlwaysAssert (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER); - storeBBAtom(node, atom_definition); - d_cnfStream->convertAndAssert(atom_definition, false, false); -} - -void EagerBitblaster::storeBBAtom(TNode atom, Node atom_bb) { - // no need to store the definition for the lazy bit-blaster - d_bbAtoms.insert(atom); -} - -bool EagerBitblaster::hasBBAtom(TNode atom) const { - return d_bbAtoms.find(atom) != d_bbAtoms.end(); -} - -void EagerBitblaster::bbTerm(TNode node, Bits& bits) { - if (hasBBTerm(node)) { - getBBTerm(node, bits); - return; - } - - 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::getVarValue(TNode a, bool fullModel) { - if (!hasBBTerm(a)) { - Assert(isSharedTerm(a)); - return 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 { - // the bit is unconstrainted so we can give it an arbitrary value - 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(BitVector(bits.size(), value)); -} - - -void EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) { - TNodeSet::const_iterator it = d_variables.begin(); - for (; it!= d_variables.end(); ++it) { - TNode var = *it; - if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)) { - Node const_value = getVarValue(var, fullModel); - if(const_value == Node()) { - if( fullModel ){ - // if the value is unassigned just set it to zero - const_value = utils::mkConst(BitVector(utils::getSize(var), 0u)); - } - } - if(const_value != Node()) { - Debug("bitvector-model") << "TLazyBitblaster::collectModelInfo (assert (= " - << var << " " - << const_value << "))\n"; - m->assertEquality(var, const_value, true); - } - } - } -} - -bool EagerBitblaster::isSharedTerm(TNode node) { - return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end(); -} - - -} /*bv namespace */ -} /* theory namespace */ -} /* CVC4 namespace*/ - - - -#endif diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp new file mode 100644 index 000000000..d3ab68a5a --- /dev/null +++ b/src/theory/bv/lazy_bitblaster.cpp @@ -0,0 +1,495 @@ +/********************* */ +/*! \file lazy_bitblaster.cpp +** \verbatim +** Original author: Liana Hadarean +** Major contributors: none +** Minor contributors (to current version): lianah +** This file is part of the CVC4 project. +** Copyright (c) 2009-2013 New York University and The University of Iowa +** See the file COPYING in the top-level source directory for licensing +** information.\endverbatim +** +** \brief +** +** Bitblaster for the lazy bv solver. +**/ + +#include "cvc4_private.h" +#include "bitblaster_template.h" +#include "theory_bv_utils.h" +#include "theory/rewriter.h" +#include "prop/cnf_stream.h" +#include "prop/sat_solver.h" +#include "prop/sat_solver_factory.h" +#include "theory/bv/theory_bv.h" +#include "theory/bv/options.h" +#include "theory/theory_model.h" +#include "theory/bv/abstraction.h" + +using namespace CVC4; +using namespace CVC4::theory; +using namespace CVC4::theory::bv; + + +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_name(name) + , d_statistics(name) { + d_satSolver = prop::SatSolverFactory::createMinisat(c, name); + d_nullRegistrar = new prop::NullRegistrar(); + d_nullContext = new context::Context(); + d_cnfStream = new prop::TseitinCnfStream(d_satSolver, + d_nullRegistrar, + d_nullContext); + + prop::BVSatSolverInterface::Notify* notify = d_emptyNotify ? + (prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() : + (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, bv, this); + + d_satSolver->setNotify(notify); +} + +void TLazyBitblaster::setAbstraction(AbstractionModule* abs) { + d_abstraction = abs; +} + +TLazyBitblaster::~TLazyBitblaster() { + delete d_cnfStream; + delete d_nullRegistrar; + delete d_nullContext; + delete d_satSolver; +} + + +/** + * 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) { + 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 = utils::mkNode(kind::IFF, node, atom_bb); + storeBBAtom(node, atom_bb); + d_cnfStream->convertAndAssert(atom_definition, false, false); + return; + } + + // the bitblasted definition of the atom + Node normalized = Rewriter::rewrite(node); + Node atom_bb = normalized.getKind() != kind::CONST_BOOLEAN ? + Rewriter::rewrite(d_atomBBStrategies[normalized.getKind()](normalized, this)) : + normalized; + // asserting that the atom is true iff the definition holds + Node atom_definition = utils::mkNode(kind::IFF, node, atom_bb); + storeBBAtom(node, atom_bb); + d_cnfStream->convertAndAssert(atom_definition, false, false); +} + +void TLazyBitblaster::storeBBAtom(TNode atom, Node atom_bb) { + // no need to store the definition for the lazy bit-blaster + d_bbAtoms.insert(atom); +} + +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; + + Node atom_bb = Rewriter::rewrite(d_atomBBStrategies[node.getKind()](node, this)); + uint64_t size = utils::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; + } + + Debug("bitvector-bitblast") << "Bitblasting node " << 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 (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"; + 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) { + 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 = NodeManager::currentNM()->mkNode(kind::NOT, atom); + } + conflict.push_back(not_atom); + } +} + +TLazyBitblaster::Statistics::Statistics(const std::string& prefix) : + d_numTermClauses("theory::bv::"+prefix+"::NumberOfTermSatClauses", 0), + d_numAtomClauses("theory::bv::"+prefix+"::NumberOfAtomSatClauses", 0), + d_numTerms("theory::bv::"+prefix+"::NumberOfBitblastedTerms", 0), + d_numAtoms("theory::bv::"+prefix+"::NumberOfBitblastedAtoms", 0), + d_numExplainedPropagations("theory::bv::"+prefix+"::NumberOfExplainedPropagations", 0), + d_numBitblastingPropagations("theory::bv::"+prefix+"::NumberOfBitblastingPropagations", 0), + d_bitblastTimer("theory::bv::"+prefix+"::BitblastTimer") +{ + StatisticsRegistry::registerStat(&d_numTermClauses); + StatisticsRegistry::registerStat(&d_numAtomClauses); + StatisticsRegistry::registerStat(&d_numTerms); + StatisticsRegistry::registerStat(&d_numAtoms); + StatisticsRegistry::registerStat(&d_numExplainedPropagations); + StatisticsRegistry::registerStat(&d_numBitblastingPropagations); + StatisticsRegistry::registerStat(&d_bitblastTimer); +} + + +TLazyBitblaster::Statistics::~Statistics() { + StatisticsRegistry::unregisterStat(&d_numTermClauses); + StatisticsRegistry::unregisterStat(&d_numAtomClauses); + StatisticsRegistry::unregisterStat(&d_numTerms); + StatisticsRegistry::unregisterStat(&d_numAtoms); + StatisticsRegistry::unregisterStat(&d_numExplainedPropagations); + StatisticsRegistry::unregisterStat(&d_numBitblastingPropagations); + StatisticsRegistry::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::safePoint() { + d_bv->d_out->safePoint(); +} + +EqualityStatus TLazyBitblaster::getEqualityStatus(TNode a, TNode b) { + + // We don't want to bit-blast every possibly expensive term for the sake of equality checking + if (hasBBTerm(a) && hasBBTerm(b)) { + + Bits a_bits, b_bits; + getBBTerm(a, a_bits); + getBBTerm(b, b_bits); + theory::EqualityStatus status = theory::EQUALITY_TRUE_IN_MODEL; + for (unsigned i = 0; i < a_bits.size(); ++ i) { + if (d_cnfStream->hasLiteral(a_bits[i]) && d_cnfStream->hasLiteral(b_bits[i])) { + prop::SatLiteral a_lit = d_cnfStream->getLiteral(a_bits[i]); + prop::SatValue a_lit_value = d_satSolver->value(a_lit); + if (a_lit_value != prop::SAT_VALUE_UNKNOWN) { + prop::SatLiteral b_lit = d_cnfStream->getLiteral(b_bits[i]); + prop::SatValue b_lit_value = d_satSolver->value(b_lit); + if (b_lit_value != prop::SAT_VALUE_UNKNOWN) { + if (a_lit_value != b_lit_value) { + return theory::EQUALITY_FALSE_IN_MODEL; + } + } else { + status = theory::EQUALITY_UNKNOWN; + } + } { + status = theory::EQUALITY_UNKNOWN; + } + } else { + status = theory::EQUALITY_UNKNOWN; + } + } + + return status; + + } else { + return theory::EQUALITY_UNKNOWN; + } +} + + +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::getVarValue(TNode a, bool fullModel) { + if (!hasBBTerm(a)) { + Assert(isSharedTerm(a)); + return 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 { + // the bit is unconstrainted so we can give it an arbitrary value + 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(BitVector(bits.size(), value)); +} + +void TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) { + TNodeSet::iterator it = d_variables.begin(); + for (; it!= d_variables.end(); ++it) { + TNode var = *it; + if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)) { + Node const_value = getVarValue(var, fullModel); + if(const_value == Node()) { + if( fullModel ){ + // if the value is unassigned just set it to zero + const_value = utils::mkConst(BitVector(utils::getSize(var), 0u)); + } + } + if(const_value != Node()) { + Debug("bitvector-model") << "TLazyBitblaster::collectModelInfo (assert (= " + << var << " " + << const_value << "))\n"; + m->assertEquality(var, const_value, true); + } + } + } +} + +void TLazyBitblaster::clearSolver() { + Assert (d_ctx->getLevel() == 0); + delete d_satSolver; + 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(); + + // recreate sat solver + d_satSolver = prop::SatSolverFactory::createMinisat(d_ctx); + d_cnfStream = new prop::TseitinCnfStream(d_satSolver, + new prop::NullRegistrar(), + new context::Context()); + + prop::BVSatSolverInterface::Notify* notify = d_emptyNotify ? + (prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() : + (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, d_bv, this); + d_satSolver->setNotify(notify); +} diff --git a/src/theory/bv/lazy_bitblaster.h b/src/theory/bv/lazy_bitblaster.h deleted file mode 100644 index e11254dbb..000000000 --- a/src/theory/bv/lazy_bitblaster.h +++ /dev/null @@ -1,505 +0,0 @@ -/********************* */ -/*! \file lazy_bitblaster.h -** \verbatim -** Original author: Liana Hadarean -** Major contributors: none -** Minor contributors (to current version): lianah -** This file is part of the CVC4 project. -** Copyright (c) 2009-2013 New York University and The University of Iowa -** See the file COPYING in the top-level source directory for licensing -** information.\endverbatim -** -** \brief -** -** Bitblaster for the lazy bv solver. -**/ - -#include "cvc4_private.h" - -#ifndef __CVC4__LAZY__BITBLASTER_H -#define __CVC4__LAZY__BITBLASTER_H - - -#include "bitblaster_template.h" -#include "theory_bv_utils.h" -#include "theory/rewriter.h" -#include "prop/cnf_stream.h" -#include "prop/sat_solver.h" -#include "prop/sat_solver_factory.h" -#include "theory/bv/theory_bv.h" -#include "theory/bv/options.h" -#include "theory/theory_model.h" -#include "theory/bv/abstraction.h" - -namespace CVC4 { -namespace theory { -namespace bv { - -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_name(name) - , d_statistics(name) { - d_satSolver = prop::SatSolverFactory::createMinisat(c, name); - d_nullRegistrar = new prop::NullRegistrar(); - d_nullContext = new context::Context(); - d_cnfStream = new prop::TseitinCnfStream(d_satSolver, - d_nullRegistrar, - d_nullContext); - - prop::BVSatSolverInterface::Notify* notify = d_emptyNotify ? - (prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() : - (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, bv, this); - - d_satSolver->setNotify(notify); -} - -void TLazyBitblaster::setAbstraction(AbstractionModule* abs) { - d_abstraction = abs; -} - -TLazyBitblaster::~TLazyBitblaster() { - delete d_cnfStream; - delete d_nullRegistrar; - delete d_nullContext; - delete d_satSolver; -} - - -/** - * 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) { - 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 = utils::mkNode(kind::IFF, node, atom_bb); - storeBBAtom(node, atom_bb); - d_cnfStream->convertAndAssert(atom_definition, false, false); - return; - } - - // the bitblasted definition of the atom - Node normalized = Rewriter::rewrite(node); - Node atom_bb = normalized.getKind() != kind::CONST_BOOLEAN ? - Rewriter::rewrite(d_atomBBStrategies[normalized.getKind()](normalized, this)) : - normalized; - // asserting that the atom is true iff the definition holds - Node atom_definition = utils::mkNode(kind::IFF, node, atom_bb); - storeBBAtom(node, atom_bb); - d_cnfStream->convertAndAssert(atom_definition, false, false); -} - -void TLazyBitblaster::storeBBAtom(TNode atom, Node atom_bb) { - // no need to store the definition for the lazy bit-blaster - d_bbAtoms.insert(atom); -} - -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; - - Node atom_bb = Rewriter::rewrite(d_atomBBStrategies[node.getKind()](node, this)); - uint64_t size = utils::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; - } - - Debug("bitvector-bitblast") << "Bitblasting node " << 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 (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"; - 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) { - 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 = NodeManager::currentNM()->mkNode(kind::NOT, atom); - } - conflict.push_back(not_atom); - } -} - -TLazyBitblaster::Statistics::Statistics(const std::string& prefix) : - d_numTermClauses("theory::bv::"+prefix+"::NumberOfTermSatClauses", 0), - d_numAtomClauses("theory::bv::"+prefix+"::NumberOfAtomSatClauses", 0), - d_numTerms("theory::bv::"+prefix+"::NumberOfBitblastedTerms", 0), - d_numAtoms("theory::bv::"+prefix+"::NumberOfBitblastedAtoms", 0), - d_numExplainedPropagations("theory::bv::"+prefix+"::NumberOfExplainedPropagations", 0), - d_numBitblastingPropagations("theory::bv::"+prefix+"::NumberOfBitblastingPropagations", 0), - d_bitblastTimer("theory::bv::"+prefix+"::BitblastTimer") -{ - StatisticsRegistry::registerStat(&d_numTermClauses); - StatisticsRegistry::registerStat(&d_numAtomClauses); - StatisticsRegistry::registerStat(&d_numTerms); - StatisticsRegistry::registerStat(&d_numAtoms); - StatisticsRegistry::registerStat(&d_numExplainedPropagations); - StatisticsRegistry::registerStat(&d_numBitblastingPropagations); - StatisticsRegistry::registerStat(&d_bitblastTimer); -} - - -TLazyBitblaster::Statistics::~Statistics() { - StatisticsRegistry::unregisterStat(&d_numTermClauses); - StatisticsRegistry::unregisterStat(&d_numAtomClauses); - StatisticsRegistry::unregisterStat(&d_numTerms); - StatisticsRegistry::unregisterStat(&d_numAtoms); - StatisticsRegistry::unregisterStat(&d_numExplainedPropagations); - StatisticsRegistry::unregisterStat(&d_numBitblastingPropagations); - StatisticsRegistry::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::safePoint() { - d_bv->d_out->safePoint(); -} - -EqualityStatus TLazyBitblaster::getEqualityStatus(TNode a, TNode b) { - - // We don't want to bit-blast every possibly expensive term for the sake of equality checking - if (hasBBTerm(a) && hasBBTerm(b)) { - - Bits a_bits, b_bits; - getBBTerm(a, a_bits); - getBBTerm(b, b_bits); - theory::EqualityStatus status = theory::EQUALITY_TRUE_IN_MODEL; - for (unsigned i = 0; i < a_bits.size(); ++ i) { - if (d_cnfStream->hasLiteral(a_bits[i]) && d_cnfStream->hasLiteral(b_bits[i])) { - prop::SatLiteral a_lit = d_cnfStream->getLiteral(a_bits[i]); - prop::SatValue a_lit_value = d_satSolver->value(a_lit); - if (a_lit_value != prop::SAT_VALUE_UNKNOWN) { - prop::SatLiteral b_lit = d_cnfStream->getLiteral(b_bits[i]); - prop::SatValue b_lit_value = d_satSolver->value(b_lit); - if (b_lit_value != prop::SAT_VALUE_UNKNOWN) { - if (a_lit_value != b_lit_value) { - return theory::EQUALITY_FALSE_IN_MODEL; - } - } else { - status = theory::EQUALITY_UNKNOWN; - } - } { - status = theory::EQUALITY_UNKNOWN; - } - } else { - status = theory::EQUALITY_UNKNOWN; - } - } - - return status; - - } else { - return theory::EQUALITY_UNKNOWN; - } -} - - -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::getVarValue(TNode a, bool fullModel) { - if (!hasBBTerm(a)) { - Assert(isSharedTerm(a)); - return 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 { - // the bit is unconstrainted so we can give it an arbitrary value - 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(BitVector(bits.size(), value)); -} - -void TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) { - TNodeSet::iterator it = d_variables.begin(); - for (; it!= d_variables.end(); ++it) { - TNode var = *it; - if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)) { - Node const_value = getVarValue(var, fullModel); - if(const_value == Node()) { - if( fullModel ){ - // if the value is unassigned just set it to zero - const_value = utils::mkConst(BitVector(utils::getSize(var), 0u)); - } - } - if(const_value != Node()) { - Debug("bitvector-model") << "TLazyBitblaster::collectModelInfo (assert (= " - << var << " " - << const_value << "))\n"; - m->assertEquality(var, const_value, true); - } - } - } -} - -void TLazyBitblaster::clearSolver() { - Assert (d_ctx->getLevel() == 0); - delete d_satSolver; - 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(); - - // recreate sat solver - d_satSolver = prop::SatSolverFactory::createMinisat(d_ctx); - d_cnfStream = new prop::TseitinCnfStream(d_satSolver, - new prop::NullRegistrar(), - new context::Context()); - - prop::BVSatSolverInterface::Notify* notify = d_emptyNotify ? - (prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() : - (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, d_bv, this); - d_satSolver->setNotify(notify); -} - -} /*bv namespace */ -} /* theory namespace */ -} /* CVC4 namespace*/ - -#endif diff --git a/test/unit/theory/theory_bv_white.h b/test/unit/theory/theory_bv_white.h index dd65fc8e4..64dd680ae 100644 --- a/test/unit/theory/theory_bv_white.h +++ b/test/unit/theory/theory_bv_white.h @@ -22,7 +22,7 @@ #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "theory/bv/theory_bv.h" -#include "theory/bv/eager_bitblaster.h" +#include "theory/bv/bitblaster_template.h" #include "expr/node.h" #include "expr/node_manager.h" #include "context/context.h"