diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2017-08-09 15:47:27 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-08-09 15:47:27 -0700 |
commit | 9ca56527c709d151a35d506a34d62c03e44764fd (patch) | |
tree | d357f8147a1ee14d30dc6a6e033312f162e09867 /src | |
parent | b725191b5edc9d2fcdabab0abb42f60cb124e59b (diff) |
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.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/bv/aig_bitblaster.cpp | 181 | ||||
-rw-r--r-- | src/theory/bv/bv_eager_solver.cpp | 16 |
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(); |