src/theory/bv/theory_bv.h

   1 /*********************                                                        */
   2 /*! \file theory_bv.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Mathias Preiner, Tim King
   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 Bitvector theory.
  13  **
  14  ** Bitvector theory.
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef CVC4__THEORY__BV__THEORY_BV_H
  20 #define CVC4__THEORY__BV__THEORY_BV_H
  21
  22 #include <unordered_map>
  23
  24 #include "theory/bv/theory_bv_rewriter.h"
  25 #include "theory/theory.h"
  26
  27 namespace CVC4 {
  28 namespace theory {
  29 namespace bv {
  30
  31 class BVSolver;
  32
  33 class TheoryBV : public Theory
  34 {
  35   /* BVSolverLazy accesses methods from theory in a way that is deprecated and
  36    * will be removed in the future. For now we allow direct access. */
  37   friend class BVSolverLazy;
  38
  39  public:
  40   TheoryBV(context::Context* c,
  41            context::UserContext* u,
  42            OutputChannel& out,
  43            Valuation valuation,
  44            const LogicInfo& logicInfo,
  45            ProofNodeManager* pnm = nullptr,
  46            std::string name = "");
  47
  48   ~TheoryBV();
  49
  50   /** get the official theory rewriter of this theory */
  51   TheoryRewriter* getTheoryRewriter() override;
  52
  53   /**
  54    * Returns true if we need an equality engine. If so, we initialize the
  55    * information regarding how it should be setup. For details, see the
  56    * documentation in Theory::needsEqualityEngine.
  57    */
  58   bool needsEqualityEngine(EeSetupInfo& esi) override;
  59
  60   void finishInit() override;
  61
  62   TrustNode expandDefinition(Node node) override;
  63
  64   void preRegisterTerm(TNode n) override;
  65
  66   bool preCheck(Effort e) override;
  67
  68   void postCheck(Effort e) override;
  69
  70   bool preNotifyFact(TNode atom,
  71                      bool pol,
  72                      TNode fact,
  73                      bool isPrereg,
  74                      bool isInternal) override;
  75
  76   void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) override;
  77
  78   bool needsCheckLastEffort() override;
  79
  80   void propagate(Effort e) override;
  81
  82   TrustNode explain(TNode n) override;
  83
  84   /** Collect model values in m based on the relevant terms given by termSet */
  85   bool collectModelValues(TheoryModel* m,
  86                           const std::set<Node>& termSet) override;
  87
  88   std::string identify() const override { return std::string("TheoryBV"); }
  89
  90   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
  91
  92   TrustNode ppRewrite(TNode t) override;
  93
  94   void ppStaticLearn(TNode in, NodeBuilder<>& learned) override;
  95
  96   void presolve() override;
  97
  98   /** Called by abstraction preprocessing pass. */
  99   bool applyAbstraction(const std::vector<Node>& assertions,
 100                         std::vector<Node>& new_assertions);
 101
 102  private:
 103   void notifySharedTerm(TNode t) override;
 104
 105   /**
 106    * Return the UF symbol corresponding to division-by-zero for this particular
 107    * bit-width.
 108    * @param k should be UREM or UDIV
 109    * @param width bit-width
 110    */
 111   Node getUFDivByZero(Kind k, unsigned width);
 112
 113   /** Internal BV solver. */
 114   std::unique_ptr<BVSolver> d_internal;
 115
 116   /**
 117    * Maps from bit-vector width to division-by-zero uninterpreted
 118    * function symbols.
 119    */
 120   std::unordered_map<unsigned, Node> d_ufDivByZero;
 121   std::unordered_map<unsigned, Node> d_ufRemByZero;
 122
 123   /** The theory rewriter for this theory. */
 124   TheoryBVRewriter d_rewriter;
 125
 126   /** A (default) theory state object */
 127   TheoryState d_state;
 128
 129   /** A (default) theory inference manager. */
 130   TheoryInferenceManager d_inferMgr;
 131
 132 }; /* class TheoryBV */
 133
 134 }  // namespace bv
 135 }  // namespace theory
 136 }  // namespace CVC4
 137
 138 #endif /* CVC4__THEORY__BV__THEORY_BV_H */