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