src/theory/bv/bv_solver_bitblast_internal.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Mathias Preiner, Haniel Barbosa, Andrew Reynolds
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 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.
  11  * ****************************************************************************
  12  *
  13  * Bit-blast solver that sends bit-blast lemmas directly to the internal
  14  * MiniSat.
  15  */
  16
  17 #include "cvc5_private.h"
  18
  19 #ifndef CVC5__THEORY__BV__BV_SOLVER_BITBLAST_INTERNAL_H
  20 #define CVC5__THEORY__BV__BV_SOLVER_BITBLAST_INTERNAL_H
  21
  22 #include "smt/env_obj.h"
  23 #include "theory/bv/bitblast/proof_bitblaster.h"
  24 #include "theory/bv/bv_solver.h"
  25 #include "theory/bv/proof_checker.h"
  26
  27 namespace cvc5 {
  28 namespace theory {
  29 namespace bv {
  30
  31 /**
  32  * Bit-blasting solver that sends bit-blasting lemmas directly to the
  33  * internal MiniSat. It is also ablo to handle atoms of kind
  34  * BITVECTOR_EAGER_ATOM.
  35  *
  36  * Sends lemmas atom <=> bb(atom) to MiniSat on preNotifyFact().
  37  */
  38 class BVSolverBitblastInternal : public BVSolver
  39 {
  40  public:
  41   BVSolverBitblastInternal(Env& env,
  42                            TheoryState* state,
  43                            TheoryInferenceManager& inferMgr,
  44                            ProofNodeManager* pnm);
  45   ~BVSolverBitblastInternal() = default;
  46
  47   bool needsEqualityEngine(EeSetupInfo& esi) override { return true; }
  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   TrustNode explain(TNode n) override;
  58
  59   std::string identify() const override { return "BVSolverBitblastInternal"; };
  60
  61   bool collectModelValues(TheoryModel* m,
  62                           const std::set<Node>& termSet) override;
  63
  64   Node getValue(TNode node, bool initialize) override;
  65
  66   /** get the proof checker of this theory */
  67   BVProofRuleChecker* getProofChecker();
  68
  69  private:
  70   /**
  71    * Sends a bit-blasting lemma fact <=> d_bitblaster.bbAtom(fact) to the
  72    * inference manager.
  73    */
  74   void addBBLemma(TNode fact);
  75
  76   /** Proof node manager. */
  77   ProofNodeManager* d_pnm;
  78   /** Bit-blaster used to bit-blast atoms/terms. */
  79   std::unique_ptr<BBProof> d_bitblaster;
  80   /** Proof rule checker */
  81   BVProofRuleChecker d_checker;
  82 };
  83
  84 }  // namespace bv
  85 }  // namespace theory
  86 }  // namespace cvc5
  87
  88 #endif