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 "proof/bitvector_proof.h"
  27 #include "proof/resolution_bitvector_proof.h"
  28 #include "prop/cnf_stream.h"
  29 #include "prop/sat_solver.h"
  30
  31 namespace CVC4 {
  32 namespace theory {
  33 namespace bv {
  34
  35 class BitblastingRegistrar;
  36 class TheoryBV;
  37
  38 class EagerBitblaster : public TBitblaster<Node>
  39 {
  40  public:
  41   EagerBitblaster(TheoryBV* theory_bv, context::Context* context);
  42   ~EagerBitblaster();
  43
  44   void addAtom(TNode atom);
  45   void makeVariable(TNode node, Bits& bits) override;
  46   void bbTerm(TNode node, Bits& bits) override;
  47   void bbAtom(TNode node) override;
  48   Node getBBAtom(TNode node) const override;
  49   bool hasBBAtom(TNode atom) const override;
  50   void bbFormula(TNode formula);
  51   void storeBBAtom(TNode atom, Node atom_bb) override;
  52   void storeBBTerm(TNode node, const Bits& bits) override;
  53
  54   bool assertToSat(TNode node, bool propagate = true);
  55   bool solve();
  56   bool solve(const std::vector<Node>& assumptions);
  57   bool collectModelInfo(TheoryModel* m, bool fullModel);
  58
  59  private:
  60   context::Context* d_context;
  61
  62   typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
  63   std::unique_ptr<prop::SatSolver> d_satSolver;
  64   std::unique_ptr<BitblastingRegistrar> d_bitblastingRegistrar;
  65
  66   TheoryBV* d_bv;
  67   TNodeSet d_bbAtoms;
  68   TNodeSet d_variables;
  69
  70   // This is either an MinisatEmptyNotify or NULL.
  71   std::unique_ptr<MinisatEmptyNotify> d_notify;
  72
  73   Node getModelFromSatSolver(TNode a, bool fullModel) override;
  74   prop::SatSolver* getSatSolver() override { return d_satSolver.get(); }
  75   bool isSharedTerm(TNode node);
  76 };
  77
  78 class BitblastingRegistrar : public prop::Registrar
  79 {
  80  public:
  81   BitblastingRegistrar(EagerBitblaster* bb) : d_bitblaster(bb) {}
  82   void preRegister(Node n) override { d_bitblaster->bbAtom(n); }
  83
  84  private:
  85   EagerBitblaster* d_bitblaster;
  86 };
  87
  88 }  // namespace bv
  89 }  // namespace theory
  90 }  // namespace CVC4
  91 #endif  //  __CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H