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
|
/********************* */
/*! \file bv_solver.h
** \verbatim
** Top contributors (to current version):
** Mathias Preiner, Andrew Reynolds
** This file is part of the CVC4 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.\endverbatim
**
** \brief Bit-vector solver interface.
**
** Describes the interface for the internal bit-vector solver of TheoryBV.
**/
#include "cvc4_private.h"
#ifndef CVC5__THEORY__BV__BV_SOLVER_H
#define CVC5__THEORY__BV__BV_SOLVER_H
#include "theory/theory.h"
namespace cvc5 {
namespace theory {
namespace bv {
class BVSolver
{
public:
BVSolver(TheoryState& state, TheoryInferenceManager& inferMgr)
: 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();
}
/** 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 Theory::PPAssertStatus ppAssert(
TrustNode in, TrustSubstitutionMap& outSubstitutions) = 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;
}
/** 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 */
|
