1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Liana Hadarean, Aina Niemetz, Mathias Preiner |
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 |
|
* A graph representation of the currently asserted bv inequalities. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/bv/bv_inequality_graph.h" |
17 |
|
#include "theory/bv/theory_bv_utils.h" |
18 |
|
|
19 |
|
using namespace std; |
20 |
|
using namespace cvc5; |
21 |
|
using namespace cvc5::context; |
22 |
|
using namespace cvc5::theory; |
23 |
|
using namespace cvc5::theory::bv; |
24 |
|
using namespace cvc5::theory::bv::utils; |
25 |
|
|
26 |
|
const TermId cvc5::theory::bv::UndefinedTermId = -1; |
27 |
|
const ReasonId cvc5::theory::bv::UndefinedReasonId = -1; |
28 |
|
const ReasonId cvc5::theory::bv::AxiomReasonId = -2; |
29 |
|
|
30 |
|
bool InequalityGraph::addInequality(TNode a, TNode b, bool strict, TNode reason) { |
31 |
|
Debug("bv-inequality") << "InequalityGraph::addInequality " << a << " " << b << " strict: " << strict << "\n"; |
32 |
|
|
33 |
|
TermId id_a = registerTerm(a); |
34 |
|
TermId id_b = registerTerm(b); |
35 |
|
ReasonId id_reason = registerReason(reason); |
36 |
|
|
37 |
|
Assert(!(isConst(id_a) && isConst(id_b))); |
38 |
|
BitVector a_val = getValue(id_a); |
39 |
|
BitVector b_val = getValue(id_b); |
40 |
|
|
41 |
|
unsigned bitwidth = utils::getSize(a); |
42 |
|
BitVector diff = strict ? BitVector(bitwidth, 1u) : BitVector(bitwidth, 0u); |
43 |
|
|
44 |
|
if (a_val + diff < a_val) { |
45 |
|
// we have an overflow |
46 |
|
std::vector<ReasonId> conflict; |
47 |
|
conflict.push_back(id_reason); |
48 |
|
computeExplanation(UndefinedTermId, id_a, conflict); |
49 |
|
setConflict(conflict); |
50 |
|
return false; |
51 |
|
} |
52 |
|
|
53 |
|
if (a_val + diff <= b_val) { |
54 |
|
// the inequality is true in the current partial model |
55 |
|
// we still add the edge because it may not be true later (cardinality) |
56 |
|
addEdge(id_a, id_b, strict, id_reason); |
57 |
|
return true; |
58 |
|
} |
59 |
|
|
60 |
|
if (isConst(id_b) && a_val + diff > b_val) { |
61 |
|
// we must be in a conflict since a has the minimum value that |
62 |
|
// satisifes the constraints |
63 |
|
std::vector<ReasonId> conflict; |
64 |
|
conflict.push_back(id_reason); |
65 |
|
computeExplanation(UndefinedTermId, id_a, conflict); |
66 |
|
Debug("bv-inequality") << "InequalityGraph::addInequality conflict: constant UB \n"; |
67 |
|
setConflict(conflict); |
68 |
|
return false; |
69 |
|
} |
70 |
|
|
71 |
|
// add the inequality edge |
72 |
|
addEdge(id_a, id_b, strict, id_reason); |
73 |
|
BFSQueue queue(&d_modelValues); |
74 |
|
Assert(hasModelValue(id_a)); |
75 |
|
queue.push(id_a); |
76 |
|
return processQueue(queue, id_a); |
77 |
|
} |
78 |
|
|
79 |
|
bool InequalityGraph::updateValue(TermId id, ModelValue new_mv, TermId start, bool& changed) { |
80 |
|
BitVector lower_bound = new_mv.value; |
81 |
|
|
82 |
|
if (isConst(id)) { |
83 |
|
if (getValue(id) < lower_bound) { |
84 |
|
Debug("bv-inequality") << "Conflict: constant " << getValue(id) << "\n"; |
85 |
|
std::vector<ReasonId> conflict; |
86 |
|
TermId parent = new_mv.parent; |
87 |
|
ReasonId reason = new_mv.reason; |
88 |
|
conflict.push_back(reason); |
89 |
|
computeExplanation(UndefinedTermId, parent, conflict); |
90 |
|
Debug("bv-inequality") << "InequalityGraph::addInequality conflict: constant\n"; |
91 |
|
setConflict(conflict); |
92 |
|
return false; |
93 |
|
} |
94 |
|
} else { |
95 |
|
// if not constant we can try to update the value |
96 |
|
if (getValue(id) < lower_bound) { |
97 |
|
// if we are updating the term we started with we must be in a cycle |
98 |
|
if (id == start) { |
99 |
|
TermId parent = new_mv.parent; |
100 |
|
ReasonId reason = new_mv.reason; |
101 |
|
std::vector<TermId> conflict; |
102 |
|
conflict.push_back(reason); |
103 |
|
computeExplanation(id, parent, conflict); |
104 |
|
Debug("bv-inequality") << "InequalityGraph::addInequality conflict: cycle \n"; |
105 |
|
setConflict(conflict); |
106 |
|
return false; |
107 |
|
} |
108 |
|
Debug("bv-inequality-internal") << "Updating " << getTermNode(id) |
109 |
|
<< " from " << getValue(id) << "\n" |
110 |
|
<< " to " << lower_bound << "\n"; |
111 |
|
changed = true; |
112 |
|
setModelValue(id, new_mv); |
113 |
|
} |
114 |
|
} |
115 |
|
return true; |
116 |
|
} |
117 |
|
|
118 |
|
bool InequalityGraph::processQueue(BFSQueue& queue, TermId start) { |
119 |
|
while (!queue.empty()) { |
120 |
|
TermId current = queue.top(); |
121 |
|
queue.pop(); |
122 |
|
Debug("bv-inequality-internal") << "InequalityGraph::processQueue processing " << getTermNode(current) << "\n"; |
123 |
|
|
124 |
|
BitVector current_value = getValue(current); |
125 |
|
|
126 |
|
unsigned size = getBitwidth(current); |
127 |
|
const BitVector zero(size, 0u); |
128 |
|
const BitVector one(size, 1u); |
129 |
|
|
130 |
|
const Edges& edges = getEdges(current); |
131 |
|
for (Edges::const_iterator it = edges.begin(); it!= edges.end(); ++it) { |
132 |
|
TermId next = it->next; |
133 |
|
ReasonId reason = it->reason; |
134 |
|
|
135 |
|
const BitVector increment = it->strict ? one : zero; |
136 |
|
const BitVector next_lower_bound = current_value + increment; |
137 |
|
|
138 |
|
if (next_lower_bound < current_value) { |
139 |
|
// it means we have an overflow and hence a conflict |
140 |
|
std::vector<TermId> conflict; |
141 |
|
conflict.push_back(it->reason); |
142 |
|
Assert(hasModelValue(start)); |
143 |
|
ReasonId start_reason = getModelValue(start).reason; |
144 |
|
if (start_reason != UndefinedReasonId) { |
145 |
|
conflict.push_back(start_reason); |
146 |
|
} |
147 |
|
computeExplanation(UndefinedTermId, current, conflict); |
148 |
|
Debug("bv-inequality") << "InequalityGraph::addInequality conflict: cycle \n"; |
149 |
|
setConflict(conflict); |
150 |
|
return false; |
151 |
|
} |
152 |
|
|
153 |
|
ModelValue new_mv(next_lower_bound, current, reason); |
154 |
|
bool updated = false; |
155 |
|
if (!updateValue(next, new_mv, start, updated)) { |
156 |
|
return false; |
157 |
|
} |
158 |
|
|
159 |
|
if (next == start) { |
160 |
|
// we know what we didn't update start or we would have had a conflict |
161 |
|
// this means we are in a cycle where all the values are forced to be equal |
162 |
|
Debug("bv-inequality-internal") << "InequalityGraph::processQueue equal cycle."; |
163 |
|
continue; |
164 |
|
} |
165 |
|
|
166 |
|
if (!updated) { |
167 |
|
// if we didn't update current we don't need to add to the queue it's children |
168 |
|
Debug("bv-inequality-internal") << " unchanged " << getTermNode(next) << "\n"; |
169 |
|
continue; |
170 |
|
} |
171 |
|
|
172 |
|
queue.push(next); |
173 |
|
Debug("bv-inequality-internal") << " enqueue " << getTermNode(next) << "\n"; |
174 |
|
} |
175 |
|
} |
176 |
|
return true; |
177 |
|
} |
178 |
|
|
179 |
|
void InequalityGraph::computeExplanation(TermId from, TermId to, std::vector<ReasonId>& explanation) { |
180 |
|
if(Debug.isOn("bv-inequality")) { |
181 |
|
if (from == UndefinedTermId) { |
182 |
|
Debug("bv-inequality") << "InequalityGraph::computeExplanation " << getTermNode(to) << "\n"; |
183 |
|
} else { |
184 |
|
Debug("bv-inequality") << "InequalityGraph::computeExplanation " << getTermNode(from) <<" => " |
185 |
|
<< getTermNode(to) << "\n"; |
186 |
|
} |
187 |
|
} |
188 |
|
|
189 |
|
TermIdSet seen; |
190 |
|
|
191 |
|
while(hasReason(to) && from != to && !seen.count(to)) { |
192 |
|
seen.insert(to); |
193 |
|
const ModelValue& exp = getModelValue(to); |
194 |
|
Assert(exp.reason != UndefinedReasonId); |
195 |
|
explanation.push_back(exp.reason); |
196 |
|
Assert(exp.parent != UndefinedTermId); |
197 |
|
to = exp.parent; |
198 |
|
Debug("bv-inequality-internal") << " parent: " << getTermNode(to) << "\n" |
199 |
|
<< " reason: " << getReasonNode(exp.reason) << "\n"; |
200 |
|
} |
201 |
|
} |
202 |
|
|
203 |
|
void InequalityGraph::addEdge(TermId a, TermId b, bool strict, TermId reason) { |
204 |
|
Debug("bv-inequality-internal") << "InequalityGraph::addEdge " << getTermNode(a) << " => " << getTermNode(b) << "\n" |
205 |
|
<< " strict ? " << strict << "\n"; |
206 |
|
Edges& edges = getEdges(a); |
207 |
|
InequalityEdge new_edge(b, strict, reason); |
208 |
|
edges.push_back(new_edge); |
209 |
|
d_undoStack.push_back(std::make_pair(a, new_edge)); |
210 |
|
d_undoStackIndex = d_undoStackIndex + 1; |
211 |
|
} |
212 |
|
|
213 |
|
void InequalityGraph::initializeModelValue(TNode node) { |
214 |
|
TermId id = getTermId(node); |
215 |
|
Assert(!hasModelValue(id)); |
216 |
|
bool isConst = node.getKind() == kind::CONST_BITVECTOR; |
217 |
|
unsigned size = utils::getSize(node); |
218 |
|
BitVector value = isConst? node.getConst<BitVector>() : BitVector(size, 0u); |
219 |
|
setModelValue(id, ModelValue(value, UndefinedTermId, UndefinedReasonId)); |
220 |
|
} |
221 |
|
|
222 |
|
bool InequalityGraph::isRegistered(TNode term) const { |
223 |
|
return d_termNodeToIdMap.find(term) != d_termNodeToIdMap.end(); |
224 |
|
} |
225 |
|
|
226 |
|
TermId InequalityGraph::registerTerm(TNode term) { |
227 |
|
if (d_termNodeToIdMap.find(term) != d_termNodeToIdMap.end()) { |
228 |
|
TermId id = d_termNodeToIdMap[term]; |
229 |
|
if (!hasModelValue(id)) { |
230 |
|
// we could have backtracked and |
231 |
|
initializeModelValue(term); |
232 |
|
} |
233 |
|
return id; |
234 |
|
} |
235 |
|
|
236 |
|
// store in node mapping |
237 |
|
TermId id = d_termNodes.size(); |
238 |
|
Debug("bv-inequality-internal") << "InequalityGraph::registerTerm " << term << " => id"<< id << "\n"; |
239 |
|
|
240 |
|
d_termNodes.push_back(term); |
241 |
|
d_termNodeToIdMap[term] = id; |
242 |
|
|
243 |
|
// create InequalityNode |
244 |
|
unsigned size = utils::getSize(term); |
245 |
|
|
246 |
|
bool isConst = term.getKind() == kind::CONST_BITVECTOR; |
247 |
|
InequalityNode ineq = InequalityNode(id, size, isConst); |
248 |
|
|
249 |
|
Assert(d_ineqNodes.size() == id); |
250 |
|
d_ineqNodes.push_back(ineq); |
251 |
|
|
252 |
|
Assert(d_ineqEdges.size() == id); |
253 |
|
d_ineqEdges.push_back(Edges()); |
254 |
|
|
255 |
|
initializeModelValue(term); |
256 |
|
|
257 |
|
return id; |
258 |
|
} |
259 |
|
|
260 |
|
ReasonId InequalityGraph::registerReason(TNode reason) { |
261 |
|
if (d_reasonToIdMap.find(reason) != d_reasonToIdMap.end()) { |
262 |
|
return d_reasonToIdMap[reason]; |
263 |
|
} |
264 |
|
d_reasonSet.insert(reason); |
265 |
|
ReasonId id = d_reasonNodes.size(); |
266 |
|
d_reasonNodes.push_back(reason); |
267 |
|
d_reasonToIdMap[reason] = id; |
268 |
|
Debug("bv-inequality-internal") << "InequalityGraph::registerReason " << reason << " => id"<< id << "\n"; |
269 |
|
return id; |
270 |
|
} |
271 |
|
|
272 |
|
TNode InequalityGraph::getReasonNode(ReasonId id) const { |
273 |
|
Assert(d_reasonNodes.size() > id); |
274 |
|
return d_reasonNodes[id]; |
275 |
|
} |
276 |
|
|
277 |
|
TNode InequalityGraph::getTermNode(TermId id) const { |
278 |
|
Assert(d_termNodes.size() > id); |
279 |
|
return d_termNodes[id]; |
280 |
|
} |
281 |
|
|
282 |
|
TermId InequalityGraph::getTermId(TNode node) const { |
283 |
|
Assert(d_termNodeToIdMap.find(node) != d_termNodeToIdMap.end()); |
284 |
|
return d_termNodeToIdMap.find(node)->second; |
285 |
|
} |
286 |
|
|
287 |
|
void InequalityGraph::setConflict(const std::vector<ReasonId>& conflict) { |
288 |
|
Assert(!d_inConflict); |
289 |
|
d_inConflict = true; |
290 |
|
d_conflict.clear(); |
291 |
|
for (unsigned i = 0; i < conflict.size(); ++i) { |
292 |
|
if (conflict[i] != AxiomReasonId) { |
293 |
|
d_conflict.push_back(getReasonNode(conflict[i])); |
294 |
|
} |
295 |
|
} |
296 |
|
if (Debug.isOn("bv-inequality")) { |
297 |
|
Debug("bv-inequality") << "InequalityGraph::setConflict \n"; |
298 |
|
for (unsigned i = 0; i < d_conflict.size(); ++i) { |
299 |
|
Debug("bv-inequality") << " " << d_conflict[i] <<"\n"; |
300 |
|
} |
301 |
|
} |
302 |
|
} |
303 |
|
|
304 |
|
void InequalityGraph::getConflict(std::vector<TNode>& conflict) { |
305 |
|
for (unsigned i = 0; i < d_conflict.size(); ++i) { |
306 |
|
conflict.push_back(d_conflict[i]); |
307 |
|
} |
308 |
|
} |
309 |
|
|
310 |
|
void InequalityGraph::setModelValue(TermId term, const ModelValue& mv) { |
311 |
|
d_modelValues[term] = mv; |
312 |
|
} |
313 |
|
|
314 |
|
InequalityGraph::ModelValue InequalityGraph::getModelValue(TermId term) const { |
315 |
|
Assert(d_modelValues.find(term) != d_modelValues.end()); |
316 |
|
return (*(d_modelValues.find(term))).second; |
317 |
|
} |
318 |
|
|
319 |
|
bool InequalityGraph::hasModelValue(TermId id) const { |
320 |
|
return d_modelValues.find(id) != d_modelValues.end(); |
321 |
|
} |
322 |
|
|
323 |
|
BitVector InequalityGraph::getValue(TermId id) const { |
324 |
|
Assert(hasModelValue(id)); |
325 |
|
return (*(d_modelValues.find(id))).second.value; |
326 |
|
} |
327 |
|
|
328 |
|
bool InequalityGraph::hasReason(TermId id) const { |
329 |
|
const ModelValue& mv = getModelValue(id); |
330 |
|
return mv.reason != UndefinedReasonId; |
331 |
|
} |
332 |
|
|
333 |
|
bool InequalityGraph::addDisequality(TNode a, TNode b, TNode reason) { |
334 |
|
Debug("bv-inequality") << "InequalityGraph::addDisequality " << reason << "\n"; |
335 |
|
d_disequalities.push_back(reason); |
336 |
|
|
337 |
|
if (!isRegistered(a) || !isRegistered(b)) { |
338 |
|
//splitDisequality(reason); |
339 |
|
return true; |
340 |
|
} |
341 |
|
TermId id_a = getTermId(a); |
342 |
|
TermId id_b = getTermId(b); |
343 |
|
if (!hasModelValue(id_a)) { |
344 |
|
initializeModelValue(a); |
345 |
|
} |
346 |
|
if (!hasModelValue(id_b)) { |
347 |
|
initializeModelValue(b); |
348 |
|
} |
349 |
|
const BitVector val_a = getValue(id_a); |
350 |
|
const BitVector val_b = getValue(id_b); |
351 |
|
if (val_a == val_b) { |
352 |
|
if (a.getKind() == kind::CONST_BITVECTOR) { |
353 |
|
// then we know b cannot be smaller than the assigned value so we try to make it larger |
354 |
|
std::vector<ReasonId> explanation_ids; |
355 |
|
computeExplanation(UndefinedTermId, id_b, explanation_ids); |
356 |
|
std::vector<TNode> explanation_nodes; |
357 |
|
explanation_nodes.push_back(reason); |
358 |
|
for (unsigned i = 0; i < explanation_ids.size(); ++i) { |
359 |
|
explanation_nodes.push_back(getReasonNode(explanation_ids[i])); |
360 |
|
} |
361 |
|
Node explanation = utils::mkAnd(explanation_nodes); |
362 |
|
d_reasonSet.insert(explanation); |
363 |
|
return addInequality(a, b, true, explanation); |
364 |
|
} |
365 |
|
if (b.getKind() == kind::CONST_BITVECTOR) { |
366 |
|
// then we know b cannot be smaller than the assigned value so we try to make it larger |
367 |
|
std::vector<ReasonId> explanation_ids; |
368 |
|
computeExplanation(UndefinedTermId, id_a, explanation_ids); |
369 |
|
std::vector<TNode> explanation_nodes; |
370 |
|
explanation_nodes.push_back(reason); |
371 |
|
for (unsigned i = 0; i < explanation_ids.size(); ++i) { |
372 |
|
explanation_nodes.push_back(getReasonNode(explanation_ids[i])); |
373 |
|
} |
374 |
|
Node explanation = utils::mkAnd(explanation_nodes); |
375 |
|
d_reasonSet.insert(explanation); |
376 |
|
return addInequality(b, a, true, explanation); |
377 |
|
} |
378 |
|
// if none of the terms are constants just add the lemma |
379 |
|
//splitDisequality(reason); |
380 |
|
} else { |
381 |
|
Debug("bv-inequality-internal") << "Disequal: " << a << " => " << val_a.toString(10) << "\n" |
382 |
|
<< " " << b << " => " << val_b.toString(10) << "\n"; |
383 |
|
} |
384 |
|
return true; |
385 |
|
} |
386 |
|
|
387 |
|
// void InequalityGraph::splitDisequality(TNode diseq) { |
388 |
|
// Debug("bv-inequality-internal")<<"InequalityGraph::splitDisequality " << |
389 |
|
// diseq <<"\n"; Assert (diseq.getKind() == kind::NOT && |
390 |
|
// diseq[0].getKind() == kind::EQUAL); if |
391 |
|
// (d_disequalitiesAlreadySplit.find(diseq) == |
392 |
|
// d_disequalitiesAlreadySplit.end()) { |
393 |
|
// d_disequalitiesToSplit.push_back(diseq); |
394 |
|
// } |
395 |
|
// } |
396 |
|
|
397 |
|
void InequalityGraph::backtrack() { |
398 |
|
Debug("bv-inequality-internal") << "InequalityGraph::backtrack()\n"; |
399 |
|
int size = d_undoStack.size(); |
400 |
|
for (int i = size - 1; i >= (int)d_undoStackIndex.get(); --i) { |
401 |
|
Assert(!d_undoStack.empty()); |
402 |
|
TermId id = d_undoStack.back().first; |
403 |
|
InequalityEdge edge = d_undoStack.back().second; |
404 |
|
d_undoStack.pop_back(); |
405 |
|
|
406 |
|
Debug("bv-inequality-internal") << " remove edge " << getTermNode(id) << " => " |
407 |
|
<< getTermNode(edge.next) <<"\n"; |
408 |
|
Edges& edges = getEdges(id); |
409 |
|
for (Edges::const_iterator it = edges.begin(); it!= edges.end(); ++it) { |
410 |
|
Debug("bv-inequality-internal") << getTermNode(it->next) <<" " << it->strict << "\n"; |
411 |
|
} |
412 |
|
Assert(!edges.empty()); |
413 |
|
Assert(edges.back() == edge); |
414 |
|
edges.pop_back(); |
415 |
|
} |
416 |
|
} |
417 |
|
|
418 |
|
Node InequalityGraph::makeDiseqSplitLemma(TNode diseq) |
419 |
|
{ |
420 |
|
Assert(diseq.getKind() == kind::NOT && diseq[0].getKind() == kind::EQUAL); |
421 |
|
NodeManager* nm = NodeManager::currentNM(); |
422 |
|
TNode a = diseq[0][0]; |
423 |
|
TNode b = diseq[0][1]; |
424 |
|
Node a_lt_b = nm->mkNode(kind::BITVECTOR_ULT, a, b); |
425 |
|
Node b_lt_a = nm->mkNode(kind::BITVECTOR_ULT, b, a); |
426 |
|
Node eq = diseq[0]; |
427 |
|
Node lemma = nm->mkNode(kind::OR, a_lt_b, b_lt_a, eq); |
428 |
|
return lemma; |
429 |
|
} |
430 |
|
|
431 |
|
void InequalityGraph::checkDisequalities(std::vector<Node>& lemmas) { |
432 |
|
for (CDQueue<TNode>::const_iterator it = d_disequalities.begin(); it != d_disequalities.end(); ++it) { |
433 |
|
if (d_disequalitiesAlreadySplit.find(*it) == d_disequalitiesAlreadySplit.end()) { |
434 |
|
// if we haven't already split on this disequality |
435 |
|
TNode diseq = *it; |
436 |
|
TermId a_id = registerTerm(diseq[0][0]); |
437 |
|
TermId b_id = registerTerm(diseq[0][1]); |
438 |
|
if (getValue(a_id) == getValue(b_id)) { |
439 |
|
lemmas.push_back(makeDiseqSplitLemma(diseq)); |
440 |
|
d_disequalitiesAlreadySplit.insert(diseq); |
441 |
|
} |
442 |
|
} |
443 |
|
} |
444 |
|
} |
445 |
|
|
446 |
|
bool InequalityGraph::isLessThan(TNode a, TNode b) { |
447 |
|
Assert(isRegistered(a) && isRegistered(b)); |
448 |
|
Unimplemented(); |
449 |
|
} |
450 |
|
|
451 |
|
bool InequalityGraph::hasValueInModel(TNode node) const { |
452 |
|
if (isRegistered(node)) { |
453 |
|
TermId id = getTermId(node); |
454 |
|
return hasModelValue(id); |
455 |
|
} |
456 |
|
return false; |
457 |
|
} |
458 |
|
|
459 |
|
BitVector InequalityGraph::getValueInModel(TNode node) const { |
460 |
|
TermId id = getTermId(node); |
461 |
|
Assert(hasModelValue(id)); |
462 |
|
return getValue(id); |
463 |
|
} |
464 |
|
|
465 |
|
void InequalityGraph::getAllValuesInModel(std::vector<Node>& assignments) |
466 |
|
{ |
467 |
|
NodeManager* nm = NodeManager::currentNM(); |
468 |
|
for (ModelValues::const_iterator it = d_modelValues.begin(); |
469 |
|
it != d_modelValues.end(); |
470 |
|
++it) |
471 |
|
{ |
472 |
|
TermId id = (*it).first; |
473 |
|
BitVector value = (*it).second.value; |
474 |
|
TNode var = getTermNode(id); |
475 |
|
Node constant = utils::mkConst(value); |
476 |
|
Node assignment = nm->mkNode(kind::EQUAL, var, constant); |
477 |
|
assignments.push_back(assignment); |
478 |
|
Debug("bitvector-model") << " " << var << " => " << constant << "\n"; |
479 |
|
} |
480 |
29280 |
} |