diff options
Diffstat (limited to 'src/theory/bv/aig_bitblaster.cpp')
-rw-r--r-- | src/theory/bv/aig_bitblaster.cpp | 653 |
1 files changed, 653 insertions, 0 deletions
diff --git a/src/theory/bv/aig_bitblaster.cpp b/src/theory/bv/aig_bitblaster.cpp new file mode 100644 index 000000000..ce775874f --- /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): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 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<Abc_Obj_t*> (const std::vector<Abc_Obj_t*>& bits) { + Unreachable("Don't know how to print AIG"); +} + + +template <> inline +Abc_Obj_t* mkTrue<Abc_Obj_t*>() { + return Abc_AigConst1(AigBitblaster::currentAigNtk()); +} + +template <> inline +Abc_Obj_t* mkFalse<Abc_Obj_t*>() { + return Abc_ObjNot(mkTrue<Abc_Obj_t*>()); +} + +template <> inline +Abc_Obj_t* mkNot<Abc_Obj_t*>(Abc_Obj_t* a) { + return Abc_ObjNot(a); +} + +template <> inline +Abc_Obj_t* mkOr<Abc_Obj_t*>(Abc_Obj_t* a, Abc_Obj_t* b) { + return Abc_AigOr(AigBitblaster::currentAigM(), a, b); +} + +template <> inline +Abc_Obj_t* mkOr<Abc_Obj_t*>(const std::vector<Abc_Obj_t*>& 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*>(Abc_Obj_t* a, Abc_Obj_t* b) { + return Abc_AigAnd(AigBitblaster::currentAigM(), a, b); +} + +template <> inline +Abc_Obj_t* mkAnd<Abc_Obj_t*>(const std::vector<Abc_Obj_t*>& 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*>(Abc_Obj_t* a, Abc_Obj_t* b) { + return Abc_AigXor(AigBitblaster::currentAigM(), a, b); +} + +template <> inline +Abc_Obj_t* mkIff<Abc_Obj_t*>(Abc_Obj_t* a, Abc_Obj_t* b) { + return mkNot(mkXor(a, b)); +} + +template <> inline +Abc_Obj_t* mkIte<Abc_Obj_t*>(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<Abc_Obj_t*>() + , 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<bool>() ? mkTrue<Abc_Obj_t*>() : mkFalse<Abc_Obj_t*>(); + 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<prop::SatVariable> 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<std::string> 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<Abc_Obj_t*> (const std::vector<Abc_Obj_t*>& bits) { + Unreachable("Don't know how to print AIG"); +} + + +template <> inline +Abc_Obj_t* mkTrue<Abc_Obj_t*>() { + Unreachable(); + return NULL; +} + +template <> inline +Abc_Obj_t* mkFalse<Abc_Obj_t*>() { + Unreachable(); + return NULL; +} + +template <> inline +Abc_Obj_t* mkNot<Abc_Obj_t*>(Abc_Obj_t* a) { + Unreachable(); + return NULL; +} + +template <> inline +Abc_Obj_t* mkOr<Abc_Obj_t*>(Abc_Obj_t* a, Abc_Obj_t* b) { + Unreachable(); + return NULL; +} + +template <> inline +Abc_Obj_t* mkOr<Abc_Obj_t*>(const std::vector<Abc_Obj_t*>& children) { + Unreachable(); + return NULL; +} + + +template <> inline +Abc_Obj_t* mkAnd<Abc_Obj_t*>(Abc_Obj_t* a, Abc_Obj_t* b) { + Unreachable(); + return NULL; +} + +template <> inline +Abc_Obj_t* mkAnd<Abc_Obj_t*>(const std::vector<Abc_Obj_t*>& children) { + Unreachable(); + return NULL; +} + +template <> inline +Abc_Obj_t* mkXor<Abc_Obj_t*>(Abc_Obj_t* a, Abc_Obj_t* b) { + Unreachable(); + return NULL; +} + +template <> inline +Abc_Obj_t* mkIff<Abc_Obj_t*>(Abc_Obj_t* a, Abc_Obj_t* b) { + Unreachable(); + return NULL; +} + +template <> inline +Abc_Obj_t* mkIte<Abc_Obj_t*>(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 |