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
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(
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);
}
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();