src/theory/bv/theory_bv.h

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