Remove AigBitblaster implementation if ABC is not compiled (#212)

* Guard use of AigBitblaster with CVC4_USE_ABC.

This removes the Unreachable() implementation of AigBitblaster in case CVC4 is
not compiled with ABC support.

2 files changed, 15 insertions, 182 deletions

diff --git a/src/theory/bv/aig_bitblaster.cpp b/src/theory/bv/aig_bitblaster.cpp
index fad1ea89b..aa67069f5 100644
--- a/src/theory/bv/aig_bitblaster.cpp
+++ b/src/theory/bv/aig_bitblaster.cpp
@@ -483,185 +483,4 @@ AigBitblaster::Statistics::~Statistics() {
   smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime);
   smtStatisticsRegistry()->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
diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp
index 05b314fad..845b90931 100644
--- a/src/theory/bv/bv_eager_solver.cpp
+++ b/src/theory/bv/bv_eager_solver.cpp
@@ -52,7 +52,11 @@ void EagerBitblastSolver::turnOffAig() {
 void EagerBitblastSolver::initialize() {
   Assert(!isInitialized());
   if (d_useAig) {
+#ifdef CVC4_USE_ABC
     d_aigBitblaster = new AigBitblaster();
+#else
+    Unreachable();
+#endif
   } else {
     d_bitblaster = new EagerBitblaster(d_bv);
     THEORY_PROOF(
@@ -79,8 +83,14 @@ void EagerBitblastSolver::assertFormula(TNode formula) {
   Debug("bitvector-eager") << "EagerBitblastSolver::assertFormula "<< formula <<"\n"; 
   d_assertionSet.insert(formula);
   //ensures all atoms are bit-blasted and converted to AIG
-  if (d_useAig) 
+  if (d_useAig)
+  {
+#ifdef CVC4_USE_ABC
     d_aigBitblaster->bbFormula(formula);
+#else
+    Unreachable();
+#endif
+  }
   else
     d_bitblaster->bbFormula(formula);
 }
@@ -95,8 +105,12 @@ bool EagerBitblastSolver::checkSat() {
     return true;
   
   if (d_useAig) {
+#ifdef CVC4_USE_ABC
     Node query = utils::mkAnd(assertions); 
     return d_aigBitblaster->solve(query);
+#else
+    Unreachable();
+#endif
   }
   
   return d_bitblaster->solve();