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
|
/********************* */
/*! \file theory_bv.h
** \verbatim
** Top contributors (to current version):
** Mathias Preiner, Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 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.\endverbatim
**
** \brief Bitvector theory.
**
** Bitvector theory.
**/
#include "cvc4_private.h"
#ifndef CVC4__THEORY__BV__THEORY_BV_H
#define CVC4__THEORY__BV__THEORY_BV_H
#include <unordered_map>
#include "theory/bv/theory_bv_rewriter.h"
#include "theory/theory.h"
#include "theory/theory_eq_notify.h"
namespace CVC4 {
namespace theory {
namespace bv {
class BVSolver;
class TheoryBV : public Theory
{
/* BVSolverLazy 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 BVSolverLazy;
public:
TheoryBV(context::Context* c,
context::UserContext* u,
OutputChannel& out,
Valuation valuation,
const LogicInfo& logicInfo,
ProofNodeManager* pnm = nullptr,
std::string name = "");
~TheoryBV();
/** get the official theory rewriter of this theory */
TheoryRewriter* getTheoryRewriter() 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;
TrustNode expandDefinition(Node node) 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;
/** 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) 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;
/**
* Return the UF symbol corresponding to division-by-zero for this particular
* bit-width.
* @param k should be UREM or UDIV
* @param width bit-width
*/
Node getUFDivByZero(Kind k, unsigned width);
/** Internal BV solver. */
std::unique_ptr<BVSolver> d_internal;
/**
* Maps from bit-vector width to division-by-zero uninterpreted
* function symbols.
*/
std::unordered_map<unsigned, Node> d_ufDivByZero;
std::unordered_map<unsigned, Node> d_ufRemByZero;
/** 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;
}; /* class TheoryBV */
} // namespace bv
} // namespace theory
} // namespace CVC4
#endif /* CVC4__THEORY__BV__THEORY_BV_H */
|
