GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bv/theory_bv.h Lines: 0 1 0.0 %
Date: 2021-03-23 Branches: 0 2 0.0 %

Line Exec Source
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-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.\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 "theory/bv/theory_bv_rewriter.h"
23
#include "theory/theory.h"
24
#include "theory/theory_eq_notify.h"
25
#include "theory/theory_state.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(TrustNode in,
91
                          TrustSubstitutionMap& outSubstitutions) override;
92
93
  TrustNode ppRewrite(TNode t, std::vector<SkolemLemma>& lems) override;
94
95
  void ppStaticLearn(TNode in, NodeBuilder<>& learned) override;
96
97
  void presolve() override;
98
99
  EqualityStatus getEqualityStatus(TNode a, TNode b) override;
100
101
  /** Called by abstraction preprocessing pass. */
102
  bool applyAbstraction(const std::vector<Node>& assertions,
103
                        std::vector<Node>& new_assertions);
104
105
 private:
106
  void notifySharedTerm(TNode t) override;
107
108
  /** Internal BV solver. */
109
  std::unique_ptr<BVSolver> d_internal;
110
111
  /** The theory rewriter for this theory. */
112
  TheoryBVRewriter d_rewriter;
113
114
  /** A (default) theory state object */
115
  TheoryState d_state;
116
117
  /** A (default) theory inference manager. */
118
  TheoryInferenceManager d_im;
119
120
  /** The notify class for equality engine. */
121
  TheoryEqNotifyClass d_notify;
122
123
}; /* class TheoryBV */
124
125
}  // namespace bv
126
}  // namespace theory
127
}  // namespace CVC4
128
129
#endif /* CVC4__THEORY__BV__THEORY_BV_H */