src/theory/bv/bitblast/aig_bitblaster.cpp

   1 /*********************                                                        */
   2 /*! \file aig_bitblaster.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Liana Hadarean, Mathias Preiner, Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief AIG bitblaster.
  13  **
  14  ** AIG bitblaster.
  15  **/
  16
  17 #include "theory/bv/bitblast/aig_bitblaster.h"
  18
  19 #include "base/check.h"
  20 #include "cvc4_private.h"
  21 #include "options/bv_options.h"
  22 #include "prop/cnf_stream.h"
  23 #include "prop/sat_solver.h"
  24 #include "prop/sat_solver_factory.h"
  25 #include "smt/smt_statistics_registry.h"
  26
  27 #ifdef CVC4_USE_ABC
  28
  29 extern "C" {
  30 #include "base/abc/abc.h"
  31 #include "base/main/main.h"
  32 #include "sat/cnf/cnf.h"
  33
  34 extern Aig_Man_t* Abc_NtkToDar(Abc_Ntk_t* pNtk, int fExors, int fRegisters);
  35 }
  36
  37 // Function is defined as static in ABC. Not sure how else to do this.
  38 static inline int Cnf_Lit2Var(int Lit)
  39 {
  40   return (Lit & 1) ? -(Lit >> 1) - 1 : (Lit >> 1) + 1;
  41 }
  42
  43 namespace CVC5 {
  44 namespace theory {
  45 namespace bv {
  46
  47 template <> inline
  48 std::string toString<Abc_Obj_t*> (const std::vector<Abc_Obj_t*>& bits) {
  49   Unreachable() << "Don't know how to print AIG";
  50 }
  51
  52
  53 template <> inline
  54 Abc_Obj_t* mkTrue<Abc_Obj_t*>() {
  55   return Abc_AigConst1(AigBitblaster::currentAigNtk());
  56 }
  57
  58 template <> inline
  59 Abc_Obj_t* mkFalse<Abc_Obj_t*>() {
  60   return Abc_ObjNot(mkTrue<Abc_Obj_t*>());
  61 }
  62
  63 template <> inline
  64 Abc_Obj_t* mkNot<Abc_Obj_t*>(Abc_Obj_t* a) {
  65   return Abc_ObjNot(a);
  66 }
  67
  68 template <> inline
  69 Abc_Obj_t* mkOr<Abc_Obj_t*>(Abc_Obj_t* a, Abc_Obj_t* b) {
  70   return Abc_AigOr(AigBitblaster::currentAigM(), a, b);
  71 }
  72
  73 template <> inline
  74 Abc_Obj_t* mkOr<Abc_Obj_t*>(const std::vector<Abc_Obj_t*>& children) {
  75   Assert(children.size());
  76   if (children.size() == 1)
  77     return children[0];
  78
  79   Abc_Obj_t* result = children[0];
  80   for (unsigned i = 1; i < children.size(); ++i) {
  81     result = Abc_AigOr(AigBitblaster::currentAigM(), result, children[i]);
  82   }
  83   return result;
  84 }
  85
  86
  87 template <> inline
  88 Abc_Obj_t* mkAnd<Abc_Obj_t*>(Abc_Obj_t* a, Abc_Obj_t* b) {
  89   return Abc_AigAnd(AigBitblaster::currentAigM(), a, b);
  90 }
  91
  92 template <> inline
  93 Abc_Obj_t* mkAnd<Abc_Obj_t*>(const std::vector<Abc_Obj_t*>& children) {
  94   Assert(children.size());
  95   if (children.size() == 1)
  96     return children[0];
  97
  98   Abc_Obj_t* result = children[0];
  99   for (unsigned i = 1; i < children.size(); ++i) {
 100     result = Abc_AigAnd(AigBitblaster::currentAigM(), result, children[i]);
 101   }
 102   return result;
 103 }
 104
 105 template <> inline
 106 Abc_Obj_t* mkXor<Abc_Obj_t*>(Abc_Obj_t* a, Abc_Obj_t* b) {
 107   return Abc_AigXor(AigBitblaster::currentAigM(), a, b);
 108 }
 109
 110 template <> inline
 111 Abc_Obj_t* mkIff<Abc_Obj_t*>(Abc_Obj_t* a, Abc_Obj_t* b) {
 112   return mkNot(mkXor(a, b));
 113 }
 114
 115 template <> inline
 116 Abc_Obj_t* mkIte<Abc_Obj_t*>(Abc_Obj_t* cond, Abc_Obj_t* a, Abc_Obj_t* b) {
 117   return Abc_AigMux(AigBitblaster::currentAigM(), cond, a, b);
 118 }
 119
 120 thread_local Abc_Ntk_t* AigBitblaster::s_abcAigNetwork = nullptr;
 121
 122 Abc_Ntk_t* AigBitblaster::currentAigNtk() {
 123   if (!AigBitblaster::s_abcAigNetwork) {
 124     Abc_Start();
 125     s_abcAigNetwork = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1);
 126     char pName[] = "CVC5::theory::bv::AigNetwork";
 127     s_abcAigNetwork->pName = Extra_UtilStrsav(pName);
 128   }
 129
 130   return s_abcAigNetwork;
 131 }
 132
 133
 134 Abc_Aig_t* AigBitblaster::currentAigM() {
 135   return (Abc_Aig_t*)(currentAigNtk()->pManFunc);
 136 }
 137
 138 AigBitblaster::AigBitblaster()
 139     : TBitblaster<Abc_Obj_t*>(),
 140       d_nullContext(new context::Context()),
 141       d_aigCache(),
 142       d_bbAtoms(),
 143       d_aigOutputNode(NULL),
 144       d_notify()
 145 {
 146   prop::SatSolver* solver = nullptr;
 147   switch (options::bvSatSolver())
 148   {
 149     case options::SatSolverMode::MINISAT:
 150     {
 151       prop::BVSatSolverInterface* minisat =
 152           prop::SatSolverFactory::createMinisat(
 153               d_nullContext.get(), smtStatisticsRegistry(), "AigBitblaster");
 154       d_notify.reset(new MinisatEmptyNotify());
 155       minisat->setNotify(d_notify.get());
 156       solver = minisat;
 157       break;
 158     }
 159     case options::SatSolverMode::CADICAL:
 160       solver = prop::SatSolverFactory::createCadical(smtStatisticsRegistry(),
 161                                                      "AigBitblaster");
 162       break;
 163     case options::SatSolverMode::CRYPTOMINISAT:
 164       solver = prop::SatSolverFactory::createCryptoMinisat(
 165           smtStatisticsRegistry(), "AigBitblaster");
 166       break;
 167     case options::SatSolverMode::KISSAT:
 168       solver = prop::SatSolverFactory::createKissat(smtStatisticsRegistry(),
 169                                                     "AigBitblaster");
 170       break;
 171     default: CVC4_FATAL() << "Unknown SAT solver type";
 172   }
 173   d_satSolver.reset(solver);
 174 }
 175
 176 AigBitblaster::~AigBitblaster() {}
 177
 178 Abc_Obj_t* AigBitblaster::bbFormula(TNode node) {
 179   Assert(node.getType().isBoolean());
 180   Debug("bitvector-bitblast") << "AigBitblaster::bbFormula "<< node << "\n";
 181
 182   if (hasAig(node))
 183     return getAig(node);
 184
 185   Abc_Obj_t* result = NULL;
 186
 187   Debug("bitvector-aig") << "AigBitblaster::convertToAig " << node <<"\n";
 188   switch (node.getKind()) {
 189   case kind::AND:
 190     {
 191       result = bbFormula(node[0]);
 192       for (unsigned i = 1; i < node.getNumChildren(); ++i) {
 193         Abc_Obj_t* child = bbFormula(node[i]);
 194         result = mkAnd(result, child);
 195       }
 196       break;
 197     }
 198   case kind::OR:
 199     {
 200       result = bbFormula(node[0]);
 201       for (unsigned i = 1; i < node.getNumChildren(); ++i) {
 202         Abc_Obj_t* child = bbFormula(node[i]);
 203         result = mkOr(result, child);
 204       }
 205       break;
 206     }
 207   case kind::XOR:
 208     {
 209       result = bbFormula(node[0]);
 210       for (unsigned i = 1; i < node.getNumChildren(); ++i) {
 211         Abc_Obj_t* child = bbFormula(node[i]);
 212         result = mkXor(result, child);
 213       }
 214       break;
 215     }
 216   case kind::IMPLIES:
 217     {
 218       Assert(node.getNumChildren() == 2);
 219       Abc_Obj_t* child1 = bbFormula(node[0]);
 220       Abc_Obj_t* child2 = bbFormula(node[1]);
 221
 222       result = mkOr(mkNot(child1), child2);
 223       break;
 224     }
 225   case kind::ITE:
 226     {
 227       Assert(node.getNumChildren() == 3);
 228       Abc_Obj_t* a = bbFormula(node[0]);
 229       Abc_Obj_t* b = bbFormula(node[1]);
 230       Abc_Obj_t* c = bbFormula(node[2]);
 231       result = mkIte(a, b, c);
 232       break;
 233     }
 234   case kind::NOT:
 235     {
 236       Abc_Obj_t* child1 = bbFormula(node[0]);
 237       result = mkNot(child1);
 238       break;
 239     }
 240   case kind::CONST_BOOLEAN:
 241     {
 242       result = node.getConst<bool>() ? mkTrue<Abc_Obj_t*>() : mkFalse<Abc_Obj_t*>();
 243       break;
 244     }
 245   case kind::EQUAL:
 246     {
 247       if( node[0].getType().isBoolean() ){
 248         Assert(node.getNumChildren() == 2);
 249         Abc_Obj_t* child1 = bbFormula(node[0]);
 250         Abc_Obj_t* child2 = bbFormula(node[1]);
 251
 252         result = mkIff(child1, child2);
 253         break;
 254       }
 255       //else, continue...
 256     }
 257   default:
 258     if( node.isVar() ){
 259       result = mkInput(node);
 260     }else{
 261       bbAtom(node);
 262       result = getBBAtom(node);
 263     }
 264   }
 265
 266   cacheAig(node, result);
 267   Debug("bitvector-aig") << "AigBitblaster::bbFormula done " << node << " => " << result <<"\n";
 268   return result;
 269 }
 270
 271 void AigBitblaster::bbAtom(TNode node) {
 272   if (hasBBAtom(node)) {
 273     return;
 274   }
 275
 276   Debug("bitvector-bitblast") << "Bitblasting atom " << node <<"\n";
 277
 278   // the bitblasted definition of the atom
 279   Node normalized = Rewriter::rewrite(node);
 280   Abc_Obj_t* atom_bb = (d_atomBBStrategies[normalized.getKind()])(normalized, this);
 281   storeBBAtom(node, atom_bb);
 282   Debug("bitvector-bitblast") << "Done bitblasting atom " << node <<"\n";
 283 }
 284
 285 void AigBitblaster::bbTerm(TNode node, Bits& bits) {
 286   if (hasBBTerm(node)) {
 287     getBBTerm(node, bits);
 288     return;
 289   }
 290   Assert(node.getType().isBitVector());
 291
 292   Debug("bitvector-bitblast") << "Bitblasting term " << node <<"\n";
 293   d_termBBStrategies[node.getKind()] (node, bits, this);
 294
 295   Assert(bits.size() == utils::getSize(node));
 296   storeBBTerm(node, bits);
 297 }
 298
 299
 300 void AigBitblaster::cacheAig(TNode node, Abc_Obj_t* aig) {
 301   Assert(!hasAig(node));
 302   d_aigCache.insert(std::make_pair(node, aig));
 303 }
 304 bool AigBitblaster::hasAig(TNode node) {
 305   return d_aigCache.find(node) != d_aigCache.end();
 306 }
 307 Abc_Obj_t* AigBitblaster::getAig(TNode node) {
 308   Assert(hasAig(node));
 309   Debug("bitvector-aig") << "AigSimplifer::getAig " << node << " => " << d_aigCache.find(node)->second <<"\n";
 310   return d_aigCache.find(node)->second;
 311 }
 312
 313 void AigBitblaster::makeVariable(TNode node, Bits& bits) {
 314
 315   for (unsigned i = 0; i < utils::getSize(node); ++i) {
 316     Node bit = utils::mkBitOf(node, i);
 317     Abc_Obj_t* input = mkInput(bit);
 318     cacheAig(bit, input);
 319     bits.push_back(input);
 320   }
 321 }
 322
 323 Abc_Obj_t* AigBitblaster::mkInput(TNode input) {
 324   Assert(!hasInput(input));
 325   Assert(input.getKind() == kind::BITVECTOR_BITOF
 326          || (input.getType().isBoolean() && input.isVar()));
 327   Abc_Obj_t* aig_input = Abc_NtkCreatePi(currentAigNtk());
 328   // d_aigCache.insert(std::make_pair(input, aig_input));
 329   d_nodeToAigInput.insert(std::make_pair(input, aig_input));
 330   Debug("bitvector-aig") << "AigSimplifer::mkInput " << input << " " << aig_input <<"\n";
 331   return aig_input;
 332 }
 333
 334 bool AigBitblaster::hasInput(TNode input) {
 335   return d_nodeToAigInput.find(input) != d_nodeToAigInput.end();
 336 }
 337
 338 bool AigBitblaster::solve(TNode node) {
 339   // setting output of network to be the query
 340   Assert(d_aigOutputNode == NULL);
 341   Abc_Obj_t* query = bbFormula(node);
 342   d_aigOutputNode = Abc_NtkCreatePo(currentAigNtk());
 343   Abc_ObjAddFanin(d_aigOutputNode, query);
 344
 345   simplifyAig();
 346   convertToCnfAndAssert();
 347   // no need to use abc anymore
 348
 349   TimerStat::CodeTimer solveTimer(d_statistics.d_solveTime);
 350   prop::SatValue result = d_satSolver->solve();
 351
 352   Assert(result != prop::SAT_VALUE_UNKNOWN);
 353   return result == prop::SAT_VALUE_TRUE;
 354 }
 355
 356
 357 void addAliases(Abc_Frame_t* pAbc);
 358
 359 void AigBitblaster::simplifyAig() {
 360   TimerStat::CodeTimer simpTimer(d_statistics.d_simplificationTime);
 361
 362   Abc_AigCleanup(currentAigM());
 363   Assert(Abc_NtkCheck(currentAigNtk()));
 364
 365   const char* command = options::bitvectorAigSimplifications().c_str();
 366   Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
 367   Abc_FrameSetCurrentNetwork(pAbc, currentAigNtk());
 368
 369   addAliases(pAbc);
 370   if ( Cmd_CommandExecute( pAbc, command ) ) {
 371     fprintf( stdout, "Cannot execute command \"%s\".\n", command );
 372     exit(-1);
 373   }
 374   s_abcAigNetwork = Abc_FrameReadNtk(pAbc);
 375 }
 376
 377
 378 void AigBitblaster::convertToCnfAndAssert() {
 379   TimerStat::CodeTimer cnfConversionTimer(d_statistics.d_cnfConversionTime);
 380
 381   Aig_Man_t * pMan = NULL;
 382   Cnf_Dat_t * pCnf = NULL;
 383   Assert(Abc_NtkIsStrash(currentAigNtk()));
 384
 385   // convert to the AIG manager
 386   pMan = Abc_NtkToDar(currentAigNtk(), 0, 0 );
 387   Abc_Stop();
 388
 389   // // free old network
 390   // Abc_NtkDelete(currentAigNtk());
 391   // s_abcAigNetwork = NULL;
 392
 393   Assert(pMan != NULL);
 394   Assert(Aig_ManCheck(pMan));
 395   pCnf = Cnf_DeriveFast( pMan, 0 );
 396
 397   assertToSatSolver(pCnf);
 398
 399   Cnf_DataFree( pCnf );
 400   Cnf_ManFree();
 401   Aig_ManStop(pMan);
 402 }
 403
 404 void AigBitblaster::assertToSatSolver(Cnf_Dat_t* pCnf) {
 405   unsigned numVariables = pCnf->nVars;
 406   unsigned numClauses = pCnf->nClauses;
 407
 408   d_statistics.d_numVariables += numVariables;
 409   d_statistics.d_numClauses += numClauses;
 410
 411   // create variables in the sat solver
 412   std::vector<prop::SatVariable> sat_variables;
 413   for (unsigned i = 0; i < numVariables; ++i) {
 414     sat_variables.push_back(d_satSolver->newVar(false, false, false));
 415   }
 416
 417   // construct clauses and add to sat solver
 418   int * pLit, * pStop;
 419   for (unsigned i = 0; i < numClauses; i++ ) {
 420     prop::SatClause clause;
 421     for (pLit = pCnf->pClauses[i], pStop = pCnf->pClauses[i+1]; pLit < pStop; pLit++ ) {
 422       int int_lit = Cnf_Lit2Var(*pLit);
 423       Assert(int_lit != 0);
 424       unsigned index = int_lit < 0? -int_lit : int_lit;
 425       Assert(index - 1 < sat_variables.size());
 426       prop::SatLiteral lit(sat_variables[index-1], int_lit < 0);
 427       clause.push_back(lit);
 428     }
 429     d_satSolver->addClause(clause, false);
 430   }
 431 }
 432
 433 void addAliases(Abc_Frame_t* pAbc) {
 434   std::vector<std::string> aliases;
 435   aliases.push_back("alias b balance");
 436   aliases.push_back("alias rw rewrite");
 437   aliases.push_back("alias rwz rewrite -z");
 438   aliases.push_back("alias rf refactor");
 439   aliases.push_back("alias rfz refactor -z");
 440   aliases.push_back("alias re restructure");
 441   aliases.push_back("alias rez restructure -z");
 442   aliases.push_back("alias rs resub");
 443   aliases.push_back("alias rsz resub -z");
 444   aliases.push_back("alias rsk6 rs -K 6");
 445   aliases.push_back("alias rszk5 rsz -K 5");
 446   aliases.push_back("alias bl b -l");
 447   aliases.push_back("alias rwl rw -l");
 448   aliases.push_back("alias rwzl rwz -l");
 449   aliases.push_back("alias rwzl rwz -l");
 450   aliases.push_back("alias rfl rf -l");
 451   aliases.push_back("alias rfzl rfz -l");
 452   aliases.push_back("alias brw \"b; rw\"");
 453
 454   for (unsigned i = 0; i < aliases.size(); ++i) {
 455     if ( Cmd_CommandExecute( pAbc, aliases[i].c_str() ) ) {
 456       fprintf( stdout, "Cannot execute command \"%s\".\n", aliases[i].c_str() );
 457       exit(-1);
 458     }
 459   }
 460 }
 461
 462 bool AigBitblaster::hasBBAtom(TNode atom) const {
 463   return d_bbAtoms.find(atom) != d_bbAtoms.end();
 464 }
 465
 466 void AigBitblaster::storeBBAtom(TNode atom, Abc_Obj_t* atom_bb) {
 467   d_bbAtoms.insert(std::make_pair(atom, atom_bb));
 468 }
 469
 470 Abc_Obj_t* AigBitblaster::getBBAtom(TNode atom) const {
 471   Assert(hasBBAtom(atom));
 472   return d_bbAtoms.find(atom)->second;
 473 }
 474
 475 AigBitblaster::Statistics::Statistics()
 476   : d_numClauses("theory::bv::AigBitblaster::numClauses", 0)
 477   , d_numVariables("theory::bv::AigBitblaster::numVariables", 0)
 478   , d_simplificationTime("theory::bv::AigBitblaster::simplificationTime")
 479   , d_cnfConversionTime("theory::bv::AigBitblaster::cnfConversionTime")
 480   , d_solveTime("theory::bv::AigBitblaster::solveTime")
 481 {
 482   smtStatisticsRegistry()->registerStat(&d_numClauses);
 483   smtStatisticsRegistry()->registerStat(&d_numVariables);
 484   smtStatisticsRegistry()->registerStat(&d_simplificationTime);
 485   smtStatisticsRegistry()->registerStat(&d_cnfConversionTime);
 486   smtStatisticsRegistry()->registerStat(&d_solveTime);
 487 }
 488
 489 AigBitblaster::Statistics::~Statistics() {
 490   smtStatisticsRegistry()->unregisterStat(&d_numClauses);
 491   smtStatisticsRegistry()->unregisterStat(&d_numVariables);
 492   smtStatisticsRegistry()->unregisterStat(&d_simplificationTime);
 493   smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime);
 494   smtStatisticsRegistry()->unregisterStat(&d_solveTime);
 495 }
 496
 497 }  // namespace bv
 498 }  // namespace theory
 499 }  // namespace CVC5
 500 #endif // CVC4_USE_ABC