Reorganize bitblaster code. (#1695)

This splits bitblaster_template.h into the separate header files {aig,eager,lazy}_bitblaster.h and
bitblaster.h (the template class TBitblaster). All the bitblaster related code is moved into the
sub-directory bitblast/.

1 files changed, 89 insertions, 0 deletions

diff --git a/src/theory/bv/bitblast/eager_bitblaster.h b/src/theory/bv/bitblast/eager_bitblaster.h
new file mode 100644
index 000000000..8610d0181
--- /dev/null
+++ b/src/theory/bv/bitblast/eager_bitblaster.h
@@ -0,0 +1,89 @@
+/*********************                                                        */
+/*! \file eager_bitblaster.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Liana Hadarean, Tim King, Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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.\endverbatim
+ **
+ ** \brief Bitblaster for eager BV solver.
+ **
+ ** Bitblaster for the eager BV solver.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
+#define __CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
+
+#include <unordered_set>
+
+#include "theory/bv/bitblast/bitblaster.h"
+
+#include "prop/cnf_stream.h"
+#include "prop/sat_solver.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+class BitblastingRegistrar;
+class TheoryBV;
+
+class EagerBitblaster : public TBitblaster<Node>
+{
+ public:
+  EagerBitblaster(TheoryBV* theory_bv);
+  ~EagerBitblaster();
+
+  void addAtom(TNode atom);
+  void makeVariable(TNode node, Bits& bits) override;
+  void bbTerm(TNode node, Bits& bits) override;
+  void bbAtom(TNode node) override;
+  Node getBBAtom(TNode node) const override;
+  bool hasBBAtom(TNode atom) const override;
+  void bbFormula(TNode formula);
+  void storeBBAtom(TNode atom, Node atom_bb) override;
+  void storeBBTerm(TNode node, const Bits& bits) override;
+
+  bool assertToSat(TNode node, bool propagate = true);
+  bool solve();
+  bool collectModelInfo(TheoryModel* m, bool fullModel);
+  void setProofLog(BitVectorProof* bvp);
+
+ private:
+  typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
+  // sat solver used for bitblasting and associated CnfStream
+  std::unique_ptr<prop::SatSolver> d_satSolver;
+  std::unique_ptr<BitblastingRegistrar> d_bitblastingRegistrar;
+  std::unique_ptr<context::Context> d_nullContext;
+  std::unique_ptr<prop::CnfStream> d_cnfStream;
+
+  TheoryBV* d_bv;
+  TNodeSet d_bbAtoms;
+  TNodeSet d_variables;
+
+  // This is either an MinisatEmptyNotify or NULL.
+  std::unique_ptr<MinisatEmptyNotify> d_notify;
+
+  Node getModelFromSatSolver(TNode a, bool fullModel) override;
+  bool isSharedTerm(TNode node);
+};
+
+class BitblastingRegistrar : public prop::Registrar
+{
+ public:
+  BitblastingRegistrar(EagerBitblaster* bb) : d_bitblaster(bb) {}
+  void preRegister(Node n) override { d_bitblaster->bbAtom(n); }
+
+ private:
+  EagerBitblaster* d_bitblaster;
+};
+
+}  // namespace bv
+}  // namespace theory
+}  // namespace CVC4
+#endif  //  __CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H