Reorganize bitblaster code. (#1695)

This splits bitblaster_template.h into the separate header files {aig,eager,lazy}_bitblaster.h and
bitblaster.h (the template class TBitblaster). All the bitblaster related code is moved into the
sub-directory bitblast/.

1 files changed, 494 insertions, 0 deletions

diff --git a/src/theory/bv/bitblast/aig_bitblaster.cpp b/src/theory/bv/bitblast/aig_bitblaster.cpp
new file mode 100644
index 000000000..7e666bcbf
--- /dev/null
+++ b/src/theory/bv/bitblast/aig_bitblaster.cpp
@@ -0,0 +1,494 @@
+/*********************                                                        */
+/*! \file aig_bitblaster.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Liana Hadarean, Andrew Reynolds, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief AIG bitblaster.
+ **
+ ** AIG bitblaster.
+ **/
+
+#include "cvc4_private.h"
+
+#include "theory/bv/bitblast/aig_bitblaster.h"
+
+#include "base/cvc4_check.h"
+#include "options/bv_options.h"
+#include "prop/sat_solver_factory.h"
+#include "smt/smt_statistics_registry.h"
+
+#ifdef CVC4_USE_ABC
+
+extern "C" {
+#include "base/abc/abc.h"
+#include "base/main/main.h"
+#include "sat/cnf/cnf.h"
+
+extern Aig_Man_t* Abc_NtkToDar(Abc_Ntk_t* pNtk, int fExors, int fRegisters);
+}
+
+// Function is defined as static in ABC. Not sure how else to do this.
+static inline int Cnf_Lit2Var(int Lit)
+{
+  return (Lit & 1) ? -(Lit >> 1) - 1 : (Lit >> 1) + 1;
+}
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+template <> inline
+std::string toString<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_THREAD_LOCAL Abc_Ntk_t* AigBitblaster::s_abcAigNetwork = nullptr;
+
+Abc_Ntk_t* AigBitblaster::currentAigNtk() {
+  if (!AigBitblaster::s_abcAigNetwork) {
+    Abc_Start();
+    s_abcAigNetwork = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1);
+    char pName[] = "CVC4::theory::bv::AigNetwork";
+    s_abcAigNetwork->pName = Extra_UtilStrsav(pName);
+  }
+  
+  return s_abcAigNetwork;
+}
+
+
+Abc_Aig_t* AigBitblaster::currentAigM() {
+  return (Abc_Aig_t*)(currentAigNtk()->pManFunc);
+}
+
+AigBitblaster::AigBitblaster()
+    : TBitblaster<Abc_Obj_t*>(),
+      d_nullContext(new context::Context()),
+      d_aigCache(),
+      d_bbAtoms(),
+      d_aigOutputNode(NULL)
+{
+  prop::SatSolver* solver = nullptr;
+  switch (options::bvSatSolver())
+  {
+    case SAT_SOLVER_MINISAT:
+    {
+      prop::BVSatSolverInterface* minisat =
+          prop::SatSolverFactory::createMinisat(
+              d_nullContext.get(), smtStatisticsRegistry(), "AigBitblaster");
+      MinisatEmptyNotify notify;
+      minisat->setNotify(&notify);
+      solver = minisat;
+      break;
+    }
+    case SAT_SOLVER_CADICAL:
+      solver = prop::SatSolverFactory::createCadical(smtStatisticsRegistry(),
+                                                     "AigBitblaster");
+      break;
+    case SAT_SOLVER_CRYPTOMINISAT:
+      solver = prop::SatSolverFactory::createCryptoMinisat(
+          smtStatisticsRegistry(), "AigBitblaster");
+      break;
+    default: CVC4_FATAL() << "Unknown SAT solver type";
+  }
+  d_satSolver.reset(solver);
+}
+
+AigBitblaster::~AigBitblaster() {}
+
+Abc_Obj_t* AigBitblaster::bbFormula(TNode node) {
+  Assert (node.getType().isBoolean());
+  Debug("bitvector-bitblast") << "AigBitblaster::bbFormula "<< node << "\n"; 
+  
+  if (hasAig(node))
+    return getAig(node);
+  
+  Abc_Obj_t* result = NULL;
+  
+  Debug("bitvector-aig") << "AigBitblaster::convertToAig " << node <<"\n"; 
+  switch (node.getKind()) {
+  case kind::AND:
+    {
+      result = bbFormula(node[0]);
+      for (unsigned i = 1; i < node.getNumChildren(); ++i) {
+        Abc_Obj_t* child = bbFormula(node[i]);
+        result = mkAnd(result, child);
+      }
+      break;
+    }
+  case kind::OR:
+    {
+      result = bbFormula(node[0]);
+      for (unsigned i = 1; i < node.getNumChildren(); ++i) {
+        Abc_Obj_t* child = bbFormula(node[i]);
+        result = mkOr(result, child);
+      }
+      break;
+    }
+  case kind::XOR:
+    {
+      result = bbFormula(node[0]);
+      for (unsigned i = 1; i < node.getNumChildren(); ++i) {
+        Abc_Obj_t* child = bbFormula(node[i]);
+        result = mkXor(result, child);
+      }
+      break;
+    }
+  case kind::IMPLIES:
+    {
+      Assert (node.getNumChildren() == 2); 
+      Abc_Obj_t* child1 = bbFormula(node[0]);
+      Abc_Obj_t* child2 = bbFormula(node[1]);
+
+      result = mkOr(mkNot(child1), child2);
+      break;
+    }
+  case kind::ITE:
+    {
+      Assert (node.getNumChildren() == 3); 
+      Abc_Obj_t* a = bbFormula(node[0]);
+      Abc_Obj_t* b = bbFormula(node[1]);
+      Abc_Obj_t* c = bbFormula(node[2]);
+      result = mkIte(a, b, c); 
+      break;
+    }
+  case kind::NOT:
+    {
+      Abc_Obj_t* child1 = bbFormula(node[0]);
+      result = mkNot(child1);
+      break;
+    }
+  case kind::CONST_BOOLEAN:
+    {
+      result = node.getConst<bool>() ? mkTrue<Abc_Obj_t*>() : mkFalse<Abc_Obj_t*>(); 
+      break;
+    }
+  case kind::EQUAL:
+    {
+      if( node[0].getType().isBoolean() ){
+        Assert (node.getNumChildren() == 2); 
+        Abc_Obj_t* child1 = bbFormula(node[0]);
+        Abc_Obj_t* child2 = bbFormula(node[1]);
+  
+        result = mkIff(child1, child2); 
+        break;
+      }
+      //else, continue...
+    }
+  default:
+    if( node.isVar() ){
+      result = mkInput(node);
+    }else{
+      bbAtom(node);
+      result = getBBAtom(node);
+    }
+  }
+
+  cacheAig(node, result);
+  Debug("bitvector-aig") << "AigBitblaster::bbFormula done " << node << " => " << result <<"\n"; 
+  return result; 
+}
+
+void AigBitblaster::bbAtom(TNode node) {
+  if (hasBBAtom(node)) {
+    return;
+  }
+
+  Debug("bitvector-bitblast") << "Bitblasting atom " << node <<"\n";
+
+  // the bitblasted definition of the atom
+  Node normalized = Rewriter::rewrite(node);
+  Abc_Obj_t* atom_bb = (d_atomBBStrategies[normalized.getKind()])(normalized, this);
+  storeBBAtom(node, atom_bb);
+  Debug("bitvector-bitblast") << "Done bitblasting atom " << node <<"\n";
+}
+
+void AigBitblaster::bbTerm(TNode node, Bits& bits) {
+  if (hasBBTerm(node)) {
+    getBBTerm(node, bits);
+    return;
+  }
+  Assert( node.getType().isBitVector() );
+
+  Debug("bitvector-bitblast") << "Bitblasting term " << node <<"\n";
+  d_termBBStrategies[node.getKind()] (node, bits, this);
+
+  Assert (bits.size() == utils::getSize(node));
+  storeBBTerm(node, bits);
+}
+
+
+void AigBitblaster::cacheAig(TNode node, Abc_Obj_t* aig) {
+  Assert (!hasAig(node));
+  d_aigCache.insert(std::make_pair(node, aig));
+}
+bool AigBitblaster::hasAig(TNode node) {
+  return d_aigCache.find(node) != d_aigCache.end(); 
+}
+Abc_Obj_t* AigBitblaster::getAig(TNode node) {
+  Assert(hasAig(node));
+  Debug("bitvector-aig") << "AigSimplifer::getAig " << node << " => " << d_aigCache.find(node)->second <<"\n"; 
+  return d_aigCache.find(node)->second; 
+}
+
+void AigBitblaster::makeVariable(TNode node, Bits& bits) {
+  
+  for (unsigned i = 0; i < utils::getSize(node); ++i) {
+    Node bit = utils::mkBitOf(node, i);
+    Abc_Obj_t* input = mkInput(bit);
+    cacheAig(bit, input); 
+    bits.push_back(input); 
+  }
+}
+
+Abc_Obj_t* AigBitblaster::mkInput(TNode input) {
+  Assert (!hasInput(input));
+  Assert(input.getKind() == kind::BITVECTOR_BITOF ||
+         (input.getType().isBoolean() && input.isVar()));
+  Abc_Obj_t* aig_input = Abc_NtkCreatePi(currentAigNtk());
+  // d_aigCache.insert(std::make_pair(input, aig_input));
+  d_nodeToAigInput.insert(std::make_pair(input, aig_input));
+  Debug("bitvector-aig") << "AigSimplifer::mkInput " << input << " " << aig_input <<"\n"; 
+  return aig_input; 
+}
+
+bool AigBitblaster::hasInput(TNode input) {
+  return d_nodeToAigInput.find(input) != d_nodeToAigInput.end(); 
+}
+
+bool AigBitblaster::solve(TNode node) {
+  // setting output of network to be the query
+  Assert (d_aigOutputNode == NULL);
+  Abc_Obj_t* query = bbFormula(node);
+  d_aigOutputNode = Abc_NtkCreatePo(currentAigNtk());
+  Abc_ObjAddFanin(d_aigOutputNode, query); 
+
+  simplifyAig();
+  convertToCnfAndAssert();
+  // no need to use abc anymore
+  
+  TimerStat::CodeTimer solveTimer(d_statistics.d_solveTime);
+  prop::SatValue result = d_satSolver->solve();
+
+  Assert (result != prop::SAT_VALUE_UNKNOWN); 
+  return result == prop::SAT_VALUE_TRUE; 
+}
+
+
+void addAliases(Abc_Frame_t* pAbc);
+
+void AigBitblaster::simplifyAig() {
+  TimerStat::CodeTimer simpTimer(d_statistics.d_simplificationTime);
+
+  Abc_AigCleanup(currentAigM());
+  Assert (Abc_NtkCheck(currentAigNtk()));
+
+  const char* command = options::bitvectorAigSimplifications().c_str(); 
+  Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
+  Abc_FrameSetCurrentNetwork(pAbc, currentAigNtk());
+
+  addAliases(pAbc); 
+  if ( Cmd_CommandExecute( pAbc, command ) ) {
+    fprintf( stdout, "Cannot execute command \"%s\".\n", command );
+    exit(-1); 
+  }
+  s_abcAigNetwork = Abc_FrameReadNtk(pAbc);
+}
+
+
+void AigBitblaster::convertToCnfAndAssert() {
+  TimerStat::CodeTimer cnfConversionTimer(d_statistics.d_cnfConversionTime);
+  
+  Aig_Man_t * pMan = NULL;
+  Cnf_Dat_t * pCnf = NULL;
+  Assert( Abc_NtkIsStrash(currentAigNtk()) );
+  
+  // convert to the AIG manager
+  pMan = Abc_NtkToDar(currentAigNtk(), 0, 0 );
+  Abc_Stop(); 
+
+  // // free old network
+  // Abc_NtkDelete(currentAigNtk());
+  // s_abcAigNetwork = NULL;
+  
+  Assert (pMan != NULL);
+  Assert (Aig_ManCheck(pMan));
+  pCnf = Cnf_DeriveFast( pMan, 0 );
+
+  assertToSatSolver(pCnf); 
+    
+  Cnf_DataFree( pCnf );
+  Cnf_ManFree();
+  Aig_ManStop(pMan);
+}
+
+void AigBitblaster::assertToSatSolver(Cnf_Dat_t* pCnf) {
+  unsigned numVariables = pCnf->nVars;
+  unsigned numClauses = pCnf->nClauses;
+  
+  d_statistics.d_numVariables += numVariables; 
+  d_statistics.d_numClauses += numClauses; 
+
+  // create variables in the sat solver
+  std::vector<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")
+{
+  smtStatisticsRegistry()->registerStat(&d_numClauses); 
+  smtStatisticsRegistry()->registerStat(&d_numVariables);
+  smtStatisticsRegistry()->registerStat(&d_simplificationTime); 
+  smtStatisticsRegistry()->registerStat(&d_cnfConversionTime);
+  smtStatisticsRegistry()->registerStat(&d_solveTime); 
+}
+
+AigBitblaster::Statistics::~Statistics() {
+  smtStatisticsRegistry()->unregisterStat(&d_numClauses); 
+  smtStatisticsRegistry()->unregisterStat(&d_numVariables);
+  smtStatisticsRegistry()->unregisterStat(&d_simplificationTime); 
+  smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime);
+  smtStatisticsRegistry()->unregisterStat(&d_solveTime); 
+}
+
+}  // namespace bv
+}  // namespace theory
+}  // namespace CVC4
+#endif // CVC4_USE_ABC