src/theory/bv/bv_solver_simple.h

   1 /*********************                                                        */
   2 /*! \file bv_solver_simple.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Mathias Preiner, Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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 Simple bit-blast solver
  13  **
  14  ** Simple bit-blast solver that sends bit-blast lemmas directly to MiniSat.
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef CVC4__THEORY__BV__BV_SOLVER_SIMPLE_H
  20 #define CVC4__THEORY__BV__BV_SOLVER_SIMPLE_H
  21
  22 #include <unordered_map>
  23
  24 #include "theory/bv/bitblast/simple_bitblaster.h"
  25 #include "theory/bv/bv_solver.h"
  26 #include "theory/bv/proof_checker.h"
  27 #include "theory/eager_proof_generator.h"
  28
  29 namespace CVC4 {
  30
  31 namespace theory {
  32 namespace bv {
  33
  34 /**
  35  * Simple bit-blasting solver that sends bit-blasting lemmas directly to the
  36  * internal MiniSat. It is also ablo to handle atoms of kind
  37  * BITVECTOR_EAGER_ATOM.
  38  *
  39  * Sends lemmas atom <=> bb(atom) to MiniSat on preNotifyFact().
  40  */
  41 class BVSolverSimple : public BVSolver
  42 {
  43  public:
  44   BVSolverSimple(TheoryState* state,
  45                  TheoryInferenceManager& inferMgr,
  46                  ProofNodeManager* pnm);
  47   ~BVSolverSimple() = default;
  48
  49   void preRegisterTerm(TNode n) override {}
  50
  51   bool preNotifyFact(TNode atom,
  52                      bool pol,
  53                      TNode fact,
  54                      bool isPrereg,
  55                      bool isInternal) override;
  56
  57   std::string identify() const override { return "BVSolverSimple"; };
  58
  59   Theory::PPAssertStatus ppAssert(
  60       TrustNode in, TrustSubstitutionMap& outSubstitutions) override
  61   {
  62     return Theory::PPAssertStatus::PP_ASSERT_STATUS_UNSOLVED;
  63   }
  64
  65   bool collectModelValues(TheoryModel* m,
  66                           const std::set<Node>& termSet) override;
  67
  68  private:
  69   /**
  70    * Sends a bit-blasting lemma fact <=> d_bitblaster.bbAtom(fact) to the
  71    * inference manager.
  72    */
  73   void addBBLemma(TNode fact);
  74
  75   /** Bit-blaster used to bit-blast atoms/terms. */
  76   std::unique_ptr<BBSimple> d_bitblaster;
  77
  78   /** Proof generator that manages proofs for lemmas generated by this class. */
  79   std::unique_ptr<EagerProofGenerator> d_epg;
  80
  81   BVProofRuleChecker d_bvProofChecker;
  82 };
  83
  84 }  // namespace bv
  85 }  // namespace theory
  86 }  // namespace CVC4
  87
  88 #endif