1 files changed, 82 insertions, 0 deletions
diff --git a/src/theory/bv/bitblast/node_bitblaster.h b/src/theory/bv/bitblast/node_bitblaster.h
new file mode 100644
index 000000000..9b3bdda07
--- /dev/null
+++ b/src/theory/bv/bitblast/node_bitblaster.h
@@ -0,0 +1,82 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Mathias Preiner
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Bitblaster used to bitblast to Boolean Nodes.
+ */
+#include "cvc5_private.h"
+
+#ifndef CVC5__THEORY__BV__BITBLAST_NODE_BITBLASTER_H
+#define CVC5__THEORY__BV__BITBLAST_NODE_BITBLASTER_H
+
+#include "theory/bv/bitblast/bitblaster.h"
+
+namespace cvc5 {
+namespace theory {
+namespace bv {
+
+/**
+ * Implementation of a simple Node-based bit-blaster.
+ *
+ * Implements the bare minimum to bit-blast bit-vector atoms/terms.
+ */
+class NodeBitblaster : public TBitblaster<Node>
+{
+  using Bits = std::vector<Node>;
+
+ public:
+  NodeBitblaster(TheoryState* state);
+  ~NodeBitblaster() = default;
+
+  /** Bit-blast term 'node' and return bit-blasted 'bits'. */
+  void bbTerm(TNode node, Bits& bits) override;
+  /** Bit-blast atom 'node'. */
+  void bbAtom(TNode node) override;
+  /** Get bit-blasted atom, returns 'atom' itself since it's Boolean. */
+  Node getBBAtom(TNode atom) const override;
+  /** Store Boolean node representing the bit-blasted atom. */
+  void storeBBAtom(TNode atom, Node atom_bb) override;
+  /** Store bits of bit-blasted term. */
+  void storeBBTerm(TNode node, const Bits& bits) override;
+  /** Check if atom was already bit-blasted. */
+  bool hasBBAtom(TNode atom) const override;
+  /** Get bit-blasted node stored for atom. */
+  Node getStoredBBAtom(TNode node);
+  /** Create 'bits' for variable 'var'. */
+  void makeVariable(TNode var, Bits& bits) override;
+
+  /** Add d_variables to termSet. */
+  void computeRelevantTerms(std::set<Node>& termSet);
+  /** Collect model values for all relevant terms given in 'relevantTerms'. */
+  bool collectModelValues(TheoryModel* m, const std::set<Node>& relevantTerms);
+
+  prop::SatSolver* getSatSolver() override { Unreachable(); }
+
+  /** Checks whether node is a variable introduced via `makeVariable`.*/
+  bool isVariable(TNode node);
+
+ private:
+  /** Query SAT solver for assignment of node 'a'. */
+  Node getModelFromSatSolver(TNode a, bool fullModel) override;
+
+  /** Caches variables for which we already created bits. */
+  TNodeSet d_variables;
+  /** Stores bit-blasted atoms. */
+  std::unordered_map<Node, Node> d_bbAtoms;
+  /** Theory state. */
+  TheoryState* d_state;
+};
+
+}  // namespace bv
+}  // namespace theory
+}  // namespace cvc5
+
+#endif