Merging CAV14 paper bit-vector work.

1 files changed, 658 insertions, 0 deletions

diff --git a/src/theory/bv/aig_bitblaster.h b/src/theory/bv/aig_bitblaster.h
new file mode 100644
index 000000000..d1635f950
--- /dev/null
+++ b/src/theory/bv/aig_bitblaster.h
@@ -0,0 +1,658 @@
+/*********************                                                        */
+/*! \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<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); 
+}
+
+
+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); 
+}
+
+
+
+} /*bv namespace */
+} /* theory namespace */
+} /* CVC4 namespace*/
+
+
+#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;
+}
+
+
+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