src/theory/bv/theory_bv.h

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