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, 181 insertions, 0 deletions

diff --git a/src/theory/bv/bitblast/lazy_bitblaster.h b/src/theory/bv/bitblast/lazy_bitblaster.h
new file mode 100644
index 000000000..97fef1e50
--- /dev/null
+++ b/src/theory/bv/bitblast/lazy_bitblaster.h
@@ -0,0 +1,181 @@
+/*********************                                                        */
+/*! \file lazy_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 the lazy bv solver.
+ **
+ ** Bitblaster for the lazy bv solver.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H
+#define __CVC4__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H
+
+#include "theory/bv/bitblast/bitblaster.h"
+
+#include "context/cdhashmap.h"
+#include "context/cdlist.h"
+#include "prop/cnf_stream.h"
+#include "prop/registrar.h"
+#include "prop/sat_solver.h"
+#include "theory/bv/abstraction.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+class TheoryBV;
+
+class TLazyBitblaster : public TBitblaster<Node>
+{
+ public:
+  void bbTerm(TNode node, Bits& bits) override;
+  void bbAtom(TNode node) override;
+  Node getBBAtom(TNode atom) const override;
+  void storeBBAtom(TNode atom, Node atom_bb) override;
+  void storeBBTerm(TNode node, const Bits& bits) override;
+  bool hasBBAtom(TNode atom) const override;
+
+  TLazyBitblaster(context::Context* c,
+                  TheoryBV* bv,
+                  const std::string name = "",
+                  bool emptyNotify = false);
+  ~TLazyBitblaster();
+  /**
+   * Pushes the assumption literal associated with node to the SAT
+   * solver assumption queue.
+   *
+   * @param node assumption
+   * @param propagate run bcp or not
+   *
+   * @return false if a conflict detected
+   */
+  bool assertToSat(TNode node, bool propagate = true);
+  bool propagate();
+  bool solve();
+  prop::SatValue solveWithBudget(unsigned long conflict_budget);
+  void getConflict(std::vector<TNode>& conflict);
+  void explain(TNode atom, std::vector<TNode>& explanation);
+  void setAbstraction(AbstractionModule* abs);
+
+  theory::EqualityStatus getEqualityStatus(TNode a, TNode b);
+
+  /**
+   * Adds a constant value for each bit-blasted variable in the model.
+   *
+   * @param m the model
+   * @param fullModel whether to create a "full model," i.e., add
+   * constants to equivalence classes that don't already have them
+   */
+  bool collectModelInfo(TheoryModel* m, bool fullModel);
+  void setProofLog(BitVectorProof* bvp);
+
+  typedef TNodeSet::const_iterator vars_iterator;
+  vars_iterator beginVars() { return d_variables.begin(); }
+  vars_iterator endVars() { return d_variables.end(); }
+
+  /**
+   * Creates the bits corresponding to the variable (or non-bv term).
+   *
+   * @param var
+   */
+  void makeVariable(TNode var, Bits& bits) override;
+
+  bool isSharedTerm(TNode node);
+  uint64_t computeAtomWeight(TNode node, NodeSet& seen);
+  /**
+   * Deletes SatSolver and CnfCache, but maintains bit-blasting
+   * terms cache.
+   *
+   */
+  void clearSolver();
+
+ private:
+  typedef std::vector<Node> Bits;
+  typedef context::CDList<prop::SatLiteral> AssertionList;
+  typedef context::CDHashMap<prop::SatLiteral,
+                             std::vector<prop::SatLiteral>,
+                             prop::SatLiteralHashFunction>
+      ExplanationMap;
+  /** This class gets callbacks from minisat on propagations */
+  class MinisatNotify : public prop::BVSatSolverInterface::Notify
+  {
+    prop::CnfStream* d_cnf;
+    TheoryBV* d_bv;
+    TLazyBitblaster* d_lazyBB;
+
+   public:
+    MinisatNotify(prop::CnfStream* cnf, TheoryBV* bv, TLazyBitblaster* lbv)
+        : d_cnf(cnf), d_bv(bv), d_lazyBB(lbv)
+    {
+    }
+
+    bool notify(prop::SatLiteral lit) override;
+    void notify(prop::SatClause& clause) override;
+    void spendResource(unsigned amount) override;
+    void safePoint(unsigned amount) override;
+  };
+
+  TheoryBV* d_bv;
+  context::Context* d_ctx;
+
+  std::unique_ptr<prop::NullRegistrar> d_nullRegistrar;
+  std::unique_ptr<context::Context> d_nullContext;
+  // sat solver used for bitblasting and associated CnfStream
+  std::unique_ptr<prop::BVSatSolverInterface> d_satSolver;
+  std::unique_ptr<prop::BVSatSolverInterface::Notify> d_satSolverNotify;
+  std::unique_ptr<prop::CnfStream> d_cnfStream;
+
+  AssertionList*
+      d_assertedAtoms;            /**< context dependent list storing the atoms
+                                     currently asserted by the DPLL SAT solver. */
+  ExplanationMap* d_explanations; /**< context dependent list of explanations
+                                    for the propagated literals. Only used when
+                                    bvEagerPropagate option enabled. */
+  TNodeSet d_variables;
+  TNodeSet d_bbAtoms;
+  AbstractionModule* d_abstraction;
+  bool d_emptyNotify;
+
+  // The size of the fact queue when we most recently called solve() in the
+  // bit-vector SAT solver. This is the level at which we should have
+  // a full model in the bv SAT solver.
+  context::CDO<int> d_fullModelAssertionLevel;
+
+  void addAtom(TNode atom);
+  bool hasValue(TNode a);
+  Node getModelFromSatSolver(TNode a, bool fullModel) override;
+
+  class Statistics
+  {
+   public:
+    IntStat d_numTermClauses, d_numAtomClauses;
+    IntStat d_numTerms, d_numAtoms;
+    IntStat d_numExplainedPropagations;
+    IntStat d_numBitblastingPropagations;
+    TimerStat d_bitblastTimer;
+    Statistics(const std::string& name);
+    ~Statistics();
+  };
+  std::string d_name;
+
+ // NOTE: d_statistics is public since d_bitblastTimer needs to be initalized
+ //       prior to calling bbAtom. As it is now, the timer can't be initialized
+ //       in bbAtom since the method is called recursively and the timer would
+ //       be initialized multiple times, which is not allowed.
+ public:
+  Statistics d_statistics;
+};
+
+}  // namespace bv
+}  // namespace theory
+}  // namespace CVC4
+#endif  //  __CVC4__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H