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
|
/******************************************************************************
* Top contributors (to current version):
* Mathias Preiner, Andrew Reynolds, Andres Noetzli
*
* 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.
* ****************************************************************************
*
* Bit-vector solver interface.
*
* Describes the interface for the internal bit-vector solver of TheoryBV.
*/
#include "cvc5_private.h"
#ifndef CVC5__THEORY__BV__BV_SOLVER_H
#define CVC5__THEORY__BV__BV_SOLVER_H
#include "smt/env.h"
#include "smt/env_obj.h"
#include "theory/theory.h"
namespace cvc5 {
namespace theory {
namespace bv {
class BVSolver : protected EnvObj
{
public:
BVSolver(Env& env, TheoryState& state, TheoryInferenceManager& inferMgr)
: EnvObj(env), d_state(state), d_im(inferMgr){};
virtual ~BVSolver() {}
/**
* 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.
*/
virtual bool needsEqualityEngine(EeSetupInfo& esi) { return false; }
virtual void finishInit(){};
virtual void preRegisterTerm(TNode n) = 0;
/**
* Forwarded from TheoryBV::preCheck().
*/
virtual bool preCheck(Theory::Effort level = Theory::Effort::EFFORT_FULL)
{
return false;
}
/**
* Forwarded from TheoryBV::postCheck().
*/
virtual void postCheck(Theory::Effort level = Theory::Effort::EFFORT_FULL){};
/**
* Forwarded from TheoryBV:preNotifyFact().
*/
virtual bool preNotifyFact(
TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
{
return false;
}
/**
* Forwarded from TheoryBV::notifyFact().
*/
virtual void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) {}
virtual bool needsCheckLastEffort() { return false; }
virtual void propagate(Theory::Effort e) {}
virtual TrustNode explain(TNode n)
{
Unimplemented() << "BVSolver propagated a node but doesn't implement the "
"BVSolver::explain() interface!";
return TrustNode::null();
}
/** Additionally collect terms relevant for collecting model values. */
virtual void computeRelevantTerms(std::set<Node>& termSet) {}
/** Collect model values in m based on the relevant terms given by termSet */
virtual bool collectModelValues(TheoryModel* m,
const std::set<Node>& termSet) = 0;
virtual std::string identify() const = 0;
virtual TrustNode ppRewrite(TNode t) { return TrustNode::null(); }
virtual void ppStaticLearn(TNode in, NodeBuilder& learned) {}
virtual void presolve() {}
virtual void notifySharedTerm(TNode t) {}
virtual EqualityStatus getEqualityStatus(TNode a, TNode b)
{
return EqualityStatus::EQUALITY_UNKNOWN;
}
/**
* Get the current value of `node`.
*
* The `initialize` flag indicates whether bits should be zero-initialized
* if they don't have a value yet.
*/
virtual Node getValue(TNode node, bool initialize) { return Node::null(); }
/** Called by abstraction preprocessing pass. */
virtual bool applyAbstraction(const std::vector<Node>& assertions,
std::vector<Node>& new_assertions)
{
new_assertions.insert(
new_assertions.end(), assertions.begin(), assertions.end());
return false;
};
protected:
TheoryState& d_state;
TheoryInferenceManager& d_im;
};
} // namespace bv
} // namespace theory
} // namespace cvc5
#endif /* CVC5__THEORY__BV__BV_SOLVER_H */
|
