1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Liana Hadarean, Mathias Preiner, Tim King |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
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. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Algebraic solver. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "cvc5_private.h" |
17 |
|
|
18 |
|
#ifndef CVC5__THEORY__BV__BV_INEQUALITY__GRAPH_H |
19 |
|
#define CVC5__THEORY__BV__BV_INEQUALITY__GRAPH_H |
20 |
|
|
21 |
|
#include <queue> |
22 |
|
#include <unordered_map> |
23 |
|
#include <unordered_set> |
24 |
|
|
25 |
|
#include "context/cdhashmap.h" |
26 |
|
#include "context/cdhashset.h" |
27 |
|
#include "context/cdo.h" |
28 |
|
#include "context/cdqueue.h" |
29 |
|
#include "context/context.h" |
30 |
|
#include "util/bitvector.h" |
31 |
|
|
32 |
|
namespace cvc5 { |
33 |
|
namespace theory { |
34 |
|
namespace bv { |
35 |
|
|
36 |
|
typedef unsigned TermId; |
37 |
|
typedef unsigned ReasonId; |
38 |
|
extern const TermId UndefinedTermId; |
39 |
|
extern const ReasonId UndefinedReasonId; |
40 |
|
extern const ReasonId AxiomReasonId; |
41 |
|
|
42 |
|
class InequalityGraph : public context::ContextNotifyObj{ |
43 |
|
|
44 |
|
struct InequalityEdge { |
45 |
|
TermId next; |
46 |
|
ReasonId reason; |
47 |
|
bool strict; |
48 |
|
InequalityEdge(TermId n, bool s, ReasonId r) |
49 |
|
: next(n), |
50 |
|
reason(r), |
51 |
|
strict(s) |
52 |
|
{} |
53 |
|
bool operator==(const InequalityEdge& other) const { |
54 |
|
return next == other.next && reason == other.reason && strict == other.strict; |
55 |
|
} |
56 |
|
}; |
57 |
|
|
58 |
|
class InequalityNode { |
59 |
|
TermId d_id; |
60 |
|
unsigned d_bitwidth; |
61 |
|
bool d_isConstant; |
62 |
|
public: |
63 |
|
InequalityNode(TermId id, unsigned bitwidth, bool isConst) |
64 |
|
: d_id(id), |
65 |
|
d_bitwidth(bitwidth), |
66 |
|
d_isConstant(isConst) |
67 |
|
{} |
68 |
|
TermId getId() const { return d_id; } |
69 |
|
unsigned getBitwidth() const { return d_bitwidth; } |
70 |
|
bool isConstant() const { return d_isConstant; } |
71 |
|
}; |
72 |
|
|
73 |
|
struct ModelValue { |
74 |
|
TermId parent; |
75 |
|
ReasonId reason; |
76 |
|
BitVector value; |
77 |
|
ModelValue() |
78 |
|
: parent(UndefinedTermId), |
79 |
|
reason(UndefinedReasonId), |
80 |
|
value(0, 0u) |
81 |
|
{} |
82 |
|
|
83 |
|
ModelValue(const BitVector& val, TermId p, ReasonId r) |
84 |
|
: parent(p), |
85 |
|
reason(r), |
86 |
|
value(val) |
87 |
|
{} |
88 |
|
}; |
89 |
|
|
90 |
|
typedef context::CDHashMap<TermId, ModelValue> ModelValues; |
91 |
|
|
92 |
|
struct QueueComparator { |
93 |
|
const ModelValues* d_model; |
94 |
|
QueueComparator(const ModelValues* model) |
95 |
|
: d_model(model) |
96 |
|
{} |
97 |
|
bool operator() (TermId left, TermId right) const { |
98 |
|
Assert(d_model->find(left) != d_model->end() |
99 |
|
&& d_model->find(right) != d_model->end()); |
100 |
|
|
101 |
|
return (*(d_model->find(left))).second.value < (*(d_model->find(right))).second.value; |
102 |
|
} |
103 |
|
}; |
104 |
|
|
105 |
|
typedef std::unordered_map<TNode, ReasonId> ReasonToIdMap; |
106 |
|
typedef std::unordered_map<TNode, TermId> TermNodeToIdMap; |
107 |
|
|
108 |
|
typedef std::vector<InequalityEdge> Edges; |
109 |
|
typedef std::unordered_set<TermId> TermIdSet; |
110 |
|
|
111 |
|
typedef std::priority_queue<TermId, std::vector<TermId>, QueueComparator> |
112 |
|
BFSQueue; |
113 |
|
typedef std::unordered_set<TNode> TNodeSet; |
114 |
|
typedef std::unordered_set<Node> NodeSet; |
115 |
|
|
116 |
|
std::vector<InequalityNode> d_ineqNodes; |
117 |
|
std::vector< Edges > d_ineqEdges; |
118 |
|
|
119 |
|
// to keep the explanation nodes alive |
120 |
|
NodeSet d_reasonSet; |
121 |
|
std::vector<TNode> d_reasonNodes; |
122 |
|
ReasonToIdMap d_reasonToIdMap; |
123 |
|
|
124 |
|
std::vector<Node> d_termNodes; |
125 |
|
TermNodeToIdMap d_termNodeToIdMap; |
126 |
|
|
127 |
|
context::CDO<bool> d_inConflict; |
128 |
|
std::vector<TNode> d_conflict; |
129 |
|
|
130 |
|
ModelValues d_modelValues; |
131 |
|
void initializeModelValue(TNode node); |
132 |
|
void setModelValue(TermId term, const ModelValue& mv); |
133 |
|
ModelValue getModelValue(TermId term) const; |
134 |
|
bool hasModelValue(TermId id) const; |
135 |
|
bool hasReason(TermId id) const; |
136 |
|
|
137 |
|
/** |
138 |
|
* Registers the term by creating its corresponding InequalityNode |
139 |
|
* and adding the min <= term <= max default edges. |
140 |
|
* |
141 |
|
* @param term |
142 |
|
* |
143 |
|
* @return |
144 |
|
*/ |
145 |
|
TermId registerTerm(TNode term); |
146 |
|
TNode getTermNode(TermId id) const; |
147 |
|
TermId getTermId(TNode node) const; |
148 |
|
bool isRegistered(TNode term) const; |
149 |
|
|
150 |
|
ReasonId registerReason(TNode reason); |
151 |
|
TNode getReasonNode(ReasonId id) const; |
152 |
|
|
153 |
|
Edges& getEdges(TermId id) |
154 |
|
{ |
155 |
|
Assert(id < d_ineqEdges.size()); |
156 |
|
return d_ineqEdges[id]; |
157 |
|
} |
158 |
|
InequalityNode& getInequalityNode(TermId id) |
159 |
|
{ |
160 |
|
Assert(id < d_ineqNodes.size()); |
161 |
|
return d_ineqNodes[id]; |
162 |
|
} |
163 |
|
const InequalityNode& getInequalityNode(TermId id) const |
164 |
|
{ |
165 |
|
Assert(id < d_ineqNodes.size()); |
166 |
|
return d_ineqNodes[id]; |
167 |
|
} |
168 |
|
unsigned getBitwidth(TermId id) const { return getInequalityNode(id).getBitwidth(); } |
169 |
|
bool isConst(TermId id) const { return getInequalityNode(id).isConstant(); } |
170 |
|
|
171 |
|
BitVector getValue(TermId id) const; |
172 |
|
|
173 |
|
void addEdge(TermId a, TermId b, bool strict, TermId reason); |
174 |
|
|
175 |
|
void setConflict(const std::vector<ReasonId>& conflict); |
176 |
|
/** |
177 |
|
* If necessary update the value in the model of the current queue element. |
178 |
|
* |
179 |
|
* @param id current queue element we are updating |
180 |
|
* @param start node we started with, to detect cycles |
181 |
|
* |
182 |
|
* @return |
183 |
|
*/ |
184 |
|
bool updateValue(TermId id, ModelValue new_mv, TermId start, bool& changed); |
185 |
|
/** |
186 |
|
* Update the current model starting with the start term. |
187 |
|
* |
188 |
|
* @param queue |
189 |
|
* @param start |
190 |
|
* |
191 |
|
* @return |
192 |
|
*/ |
193 |
|
bool processQueue(BFSQueue& queue, TermId start); |
194 |
|
/** |
195 |
|
* Return the reasons why from <= to. If from is undefined we just |
196 |
|
* explain the current value of to. |
197 |
|
* |
198 |
|
* @param from |
199 |
|
* @param to |
200 |
|
* @param explanation |
201 |
|
*/ |
202 |
|
void computeExplanation(TermId from, TermId to, std::vector<ReasonId>& explanation); |
203 |
|
// void splitDisequality(TNode diseq); |
204 |
|
|
205 |
|
/** |
206 |
|
Disequality reasoning |
207 |
|
*/ |
208 |
|
|
209 |
|
/*** The currently asserted disequalities */ |
210 |
|
context::CDQueue<TNode> d_disequalities; |
211 |
|
typedef context::CDHashSet<Node> CDNodeSet; |
212 |
|
CDNodeSet d_disequalitiesAlreadySplit; |
213 |
|
Node makeDiseqSplitLemma(TNode diseq); |
214 |
|
/** Backtracking mechanisms **/ |
215 |
|
std::vector<std::pair<TermId, InequalityEdge> > d_undoStack; |
216 |
|
context::CDO<unsigned> d_undoStackIndex; |
217 |
|
|
218 |
|
void contextNotifyPop() override { backtrack(); } |
219 |
|
|
220 |
|
void backtrack(); |
221 |
|
|
222 |
|
public: |
223 |
|
|
224 |
|
InequalityGraph(context::Context* c, context::Context* u, bool s = false) |
225 |
|
: ContextNotifyObj(c), |
226 |
|
d_ineqNodes(), |
227 |
|
d_ineqEdges(), |
228 |
|
d_inConflict(c, false), |
229 |
|
d_conflict(), |
230 |
|
d_modelValues(c), |
231 |
|
d_disequalities(c), |
232 |
|
d_disequalitiesAlreadySplit(u), |
233 |
|
d_undoStack(), |
234 |
|
d_undoStackIndex(c) |
235 |
|
{} |
236 |
|
/** |
237 |
|
* Add a new inequality to the graph |
238 |
|
* |
239 |
|
* @param a |
240 |
|
* @param b |
241 |
|
* @param strict |
242 |
|
* @param reason |
243 |
|
* |
244 |
|
* @return |
245 |
|
*/ |
246 |
|
bool addInequality(TNode a, TNode b, bool strict, TNode reason); |
247 |
|
/** |
248 |
|
* Add a new disequality to the graph. This may lead in a lemma. |
249 |
|
* |
250 |
|
* @param a |
251 |
|
* @param b |
252 |
|
* @param reason |
253 |
|
* |
254 |
|
* @return |
255 |
|
*/ |
256 |
|
bool addDisequality(TNode a, TNode b, TNode reason); |
257 |
|
void getConflict(std::vector<TNode>& conflict); |
258 |
|
virtual ~InequalityGraph() {} |
259 |
|
/** |
260 |
|
* Check that the currently asserted disequalities that have not been split on |
261 |
|
* are still true in the current model. |
262 |
|
*/ |
263 |
|
void checkDisequalities(std::vector<Node>& lemmas); |
264 |
|
/** |
265 |
|
* Return true if a < b is entailed by the current set of assertions. |
266 |
|
* |
267 |
|
* @param a |
268 |
|
* @param b |
269 |
|
* |
270 |
|
* @return |
271 |
|
*/ |
272 |
|
bool isLessThan(TNode a, TNode b); |
273 |
|
/** |
274 |
|
* Returns true if the term has a value in the model (i.e. if we have seen it) |
275 |
|
* |
276 |
|
* @param a |
277 |
|
* |
278 |
|
* @return |
279 |
|
*/ |
280 |
|
bool hasValueInModel(TNode a) const; |
281 |
|
/** |
282 |
|
* Return the value of a in the current model. |
283 |
|
* |
284 |
|
* @param a |
285 |
|
* |
286 |
|
* @return |
287 |
|
*/ |
288 |
|
BitVector getValueInModel(TNode a) const; |
289 |
|
|
290 |
|
void getAllValuesInModel(std::vector<Node>& assignments); |
291 |
|
}; |
292 |
|
|
293 |
|
} |
294 |
|
} |
295 |
|
} // namespace cvc5 |
296 |
|
|
297 |
|
#endif /* CVC5__THEORY__BV__BV_INEQUALITY__GRAPH_H */ |