src/theory/bv/bitblast/eager_bitblaster.h

   1 /*********************                                                        */
   2 /*! \file eager_bitblaster.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Mathias Preiner, Andres Noetzli
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Bitblaster for eager BV solver.
  13  **
  14  ** Bitblaster for the eager BV solver.
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef __CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
  20 #define __CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
  21
  22 #include <unordered_set>
  23
  24 #include "theory/bv/bitblast/bitblaster.h"
  25
  26 #include "prop/cnf_stream.h"
  27 #include "prop/sat_solver.h"
  28
  29 namespace CVC4 {
  30 namespace theory {
  31 namespace bv {
  32
  33 class BitblastingRegistrar;
  34 class TheoryBV;
  35
  36 class EagerBitblaster : public TBitblaster<Node>
  37 {
  38  public:
  39   EagerBitblaster(TheoryBV* theory_bv, context::Context* context);
  40   ~EagerBitblaster();
  41
  42   void addAtom(TNode atom);
  43   void makeVariable(TNode node, Bits& bits) override;
  44   void bbTerm(TNode node, Bits& bits) override;
  45   void bbAtom(TNode node) override;
  46   Node getBBAtom(TNode node) const override;
  47   bool hasBBAtom(TNode atom) const override;
  48   void bbFormula(TNode formula);
  49   void storeBBAtom(TNode atom, Node atom_bb) override;
  50   void storeBBTerm(TNode node, const Bits& bits) override;
  51
  52   bool assertToSat(TNode node, bool propagate = true);
  53   bool solve();
  54   bool solve(const std::vector<Node>& assumptions);
  55   bool collectModelInfo(TheoryModel* m, bool fullModel);
  56   void setProofLog(BitVectorProof* bvp);
  57
  58  private:
  59   context::Context* d_context;
  60   std::unique_ptr<context::Context> d_nullContext;
  61
  62   typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
  63   // sat solver used for bitblasting and associated CnfStream
  64   std::unique_ptr<prop::SatSolver> d_satSolver;
  65   std::unique_ptr<BitblastingRegistrar> d_bitblastingRegistrar;
  66   std::unique_ptr<prop::CnfStream> d_cnfStream;
  67
  68   TheoryBV* d_bv;
  69   TNodeSet d_bbAtoms;
  70   TNodeSet d_variables;
  71
  72   // This is either an MinisatEmptyNotify or NULL.
  73   std::unique_ptr<MinisatEmptyNotify> d_notify;
  74
  75   Node getModelFromSatSolver(TNode a, bool fullModel) override;
  76   bool isSharedTerm(TNode node);
  77 };
  78
  79 class BitblastingRegistrar : public prop::Registrar
  80 {
  81  public:
  82   BitblastingRegistrar(EagerBitblaster* bb) : d_bitblaster(bb) {}
  83   void preRegister(Node n) override { d_bitblaster->bbAtom(n); }
  84
  85  private:
  86   EagerBitblaster* d_bitblaster;
  87 };
  88
  89 }  // namespace bv
  90 }  // namespace theory
  91 }  // namespace CVC4
  92 #endif  //  __CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H