1 files changed, 0 insertions, 124 deletions
diff --git a/src/theory/bv/bitblast/aig_bitblaster.h b/src/theory/bv/bitblast/aig_bitblaster.h
deleted file mode 100644
index bf184585f..000000000
--- a/src/theory/bv/bitblast/aig_bitblaster.h
+++ /dev/null
@@ -1,124 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Liana Hadarean, Mathias Preiner, Andres Noetzli
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * AIG Bitblaster based on ABC.
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
-#define CVC5__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
-
-#include "theory/bv/bitblast/bitblaster.h"
-
-class Abc_Obj_t_;
-typedef Abc_Obj_t_ Abc_Obj_t;
-
-class Abc_Ntk_t_;
-typedef Abc_Ntk_t_ Abc_Ntk_t;
-
-class Abc_Aig_t_;
-typedef Abc_Aig_t_ Abc_Aig_t;
-
-class Cnf_Dat_t_;
-typedef Cnf_Dat_t_ Cnf_Dat_t;
-
-namespace cvc5 {
-namespace prop {
-class SatSolver;
-}
-namespace theory {
-namespace bv {
-
-#ifdef CVC5_USE_ABC
-
-class AigBitblaster : public TBitblaster<Abc_Obj_t*>
-{
- public:
-  AigBitblaster();
-  ~AigBitblaster();
-
-  void makeVariable(TNode node, Bits& bits) override;
-  void bbTerm(TNode node, Bits& bits) override;
-  void bbAtom(TNode node) override;
-  Abc_Obj_t* bbFormula(TNode formula);
-  bool solve(TNode query);
-  static Abc_Aig_t* currentAigM();
-  static Abc_Ntk_t* currentAigNtk();
-
- private:
-  typedef std::unordered_map<TNode, Abc_Obj_t*> TNodeAigMap;
-  typedef std::unordered_map<Node, Abc_Obj_t*> NodeAigMap;
-
-  static thread_local Abc_Ntk_t* s_abcAigNetwork;
-  std::unique_ptr<context::Context> d_nullContext;
-  std::unique_ptr<prop::SatSolver> d_satSolver;
-  TNodeAigMap d_aigCache;
-  NodeAigMap d_bbAtoms;
-
-  NodeAigMap d_nodeToAigInput;
-  // the thing we are checking for sat
-  Abc_Obj_t* d_aigOutputNode;
-
-  std::unique_ptr<MinisatEmptyNotify> d_notify;
-
-  void addAtom(TNode atom);
-  void simplifyAig();
-  void storeBBAtom(TNode atom, Abc_Obj_t* atom_bb) override;
-  Abc_Obj_t* getBBAtom(TNode atom) const override;
-  bool hasBBAtom(TNode atom) const override;
-  void cacheAig(TNode node, Abc_Obj_t* aig);
-  bool hasAig(TNode node);
-  Abc_Obj_t* getAig(TNode node);
-  Abc_Obj_t* mkInput(TNode input);
-  bool hasInput(TNode input);
-  void convertToCnfAndAssert();
-  void assertToSatSolver(Cnf_Dat_t* pCnf);
-  Node getModelFromSatSolver(TNode a, bool fullModel) override
-  {
-    Unreachable();
-  }
-
-  prop::SatSolver* getSatSolver() override { return d_satSolver.get(); }
-
-  class Statistics
-  {
-   public:
-    IntStat d_numClauses;
-    IntStat d_numVariables;
-    TimerStat d_simplificationTime;
-    TimerStat d_cnfConversionTime;
-    TimerStat d_solveTime;
-    Statistics();
-  };
-
-  Statistics d_statistics;
-};
-
-#else /* CVC5_USE_ABC */
-
-/**
- * Dummy version of the AigBitblaster class that cannot be instantiated s.t. we
- * can declare `std::unique_ptr<AigBitblaster>` without ABC.
- */
-class AigBitblaster : public TBitblaster<Abc_Obj_t*>
-{
-  AigBitblaster() = delete;
-};
-
-#endif /* CVC5_USE_ABC */
-
-}  // namespace bv
-}  // namespace theory
-}  // namespace cvc5
-
-#endif  //  CVC5__THEORY__BV__BITBLAST__AIG_BITBLASTER_H