GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bv/bv_inequality_graph.cpp Lines: 284 300 94.7 %
Date: 2021-05-21 Branches: 510 1247 40.9 %

Line Exec Source
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
1148473
bool InequalityGraph::addInequality(TNode a, TNode b, bool strict, TNode reason) {
31
1148473
  Debug("bv-inequality") << "InequalityGraph::addInequality " << a << " " << b << " strict: " << strict << "\n";
32
33
1148473
  TermId id_a = registerTerm(a);
34
1148473
  TermId id_b = registerTerm(b);
35
1148473
  ReasonId id_reason = registerReason(reason);
36
37
1148473
  Assert(!(isConst(id_a) && isConst(id_b)));
38
2296946
  BitVector a_val = getValue(id_a);
39
2296946
  BitVector b_val = getValue(id_b);
40
41
1148473
  unsigned bitwidth = utils::getSize(a);
42
2296946
  BitVector diff = strict ? BitVector(bitwidth, 1u) : BitVector(bitwidth, 0u);
43
44
1148473
  if (a_val + diff < a_val) {
45
    // we have an overflow
46
86
    std::vector<ReasonId> conflict;
47
43
    conflict.push_back(id_reason);
48
43
    computeExplanation(UndefinedTermId, id_a, conflict);
49
43
    setConflict(conflict);
50
43
    return false;
51
  }
52
53
1148430
  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
936332
    addEdge(id_a, id_b, strict, id_reason);
57
936332
    return true;
58
  }
59
60
212098
  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
366
    std::vector<ReasonId> conflict;
64
183
    conflict.push_back(id_reason);
65
183
    computeExplanation(UndefinedTermId, id_a, conflict);
66
183
    Debug("bv-inequality") << "InequalityGraph::addInequality conflict: constant UB \n";
67
183
    setConflict(conflict);
68
183
    return false;
69
  }
70
71
  // add the inequality edge
72
211915
  addEdge(id_a, id_b, strict, id_reason);
73
423830
  BFSQueue queue(&d_modelValues);
74
211915
  Assert(hasModelValue(id_a));
75
211915
  queue.push(id_a);
76
211915
  return processQueue(queue, id_a);
77
}
78
79
4283927
bool InequalityGraph::updateValue(TermId id, ModelValue new_mv, TermId start, bool& changed) {
80
8567854
  BitVector lower_bound = new_mv.value;
81
82
4283927
  if (isConst(id)) {
83
109437
    if (getValue(id) < lower_bound) {
84
209
      Debug("bv-inequality") << "Conflict: constant " << getValue(id) << "\n";
85
418
      std::vector<ReasonId> conflict;
86
209
      TermId parent = new_mv.parent;
87
209
      ReasonId reason = new_mv.reason;
88
209
      conflict.push_back(reason);
89
209
      computeExplanation(UndefinedTermId, parent, conflict);
90
209
      Debug("bv-inequality") << "InequalityGraph::addInequality conflict: constant\n";
91
209
      setConflict(conflict);
92
209
      return false;
93
    }
94
  } else {
95
    // if not constant we can try to update the value
96
4174490
    if (getValue(id) < lower_bound) {
97
      // if we are updating the term we started with we must be in a cycle
98
226421
      if (id == start) {
99
153
        TermId parent = new_mv.parent;
100
153
        ReasonId reason = new_mv.reason;
101
306
        std::vector<TermId> conflict;
102
153
        conflict.push_back(reason);
103
153
        computeExplanation(id, parent, conflict);
104
153
        Debug("bv-inequality") << "InequalityGraph::addInequality conflict: cycle \n";
105
153
        setConflict(conflict);
106
153
        return false;
107
      }
108
452536
      Debug("bv-inequality-internal") << "Updating " << getTermNode(id)
109
452536
                                      << "  from " << getValue(id) << "\n"
110
226268
                                      << "  to " << lower_bound << "\n";
111
226268
      changed = true;
112
226268
      setModelValue(id, new_mv);
113
    }
114
  }
115
4283565
  return true;
116
}
117
118
649610
bool InequalityGraph::processQueue(BFSQueue& queue, TermId start) {
119
1087305
  while (!queue.empty()) {
120
438087
    TermId current = queue.top();
121
438087
    queue.pop();
122
438087
    Debug("bv-inequality-internal") << "InequalityGraph::processQueue processing " << getTermNode(current) << "\n";
123
124
875782
    BitVector current_value = getValue(current);
125
126
438087
    unsigned size = getBitwidth(current);
127
875782
    const BitVector zero(size, 0u);
128
875782
    const BitVector one(size, 1u);
129
130
438087
    const Edges& edges = getEdges(current);
131
4721652
    for (Edges::const_iterator it = edges.begin(); it!= edges.end(); ++it) {
132
4283957
      TermId next = it->next;
133
4283957
      ReasonId reason = it->reason;
134
135
4510225
      const BitVector increment = it->strict ? one : zero;
136
4510225
      const BitVector next_lower_bound = current_value + increment;
137
138
4283957
      if (next_lower_bound < current_value) {
139
        // it means we have an overflow and hence a conflict
140
60
        std::vector<TermId> conflict;
141
30
        conflict.push_back(it->reason);
142
30
        Assert(hasModelValue(start));
143
30
        ReasonId start_reason = getModelValue(start).reason;
144
30
        if (start_reason != UndefinedReasonId) {
145
4
          conflict.push_back(start_reason);
146
        }
147
30
        computeExplanation(UndefinedTermId, current, conflict);
148
30
        Debug("bv-inequality") << "InequalityGraph::addInequality conflict: cycle \n";
149
30
        setConflict(conflict);
150
30
        return false;
151
      }
152
153
4510195
      ModelValue new_mv(next_lower_bound, current, reason);
154
4283927
      bool updated = false;
155
4283927
      if (!updateValue(next, new_mv, start, updated)) {
156
362
        return false;
157
      }
158
159
4391112
      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
107547
        Debug("bv-inequality-internal") << "InequalityGraph::processQueue equal cycle.";
163
107547
        continue;
164
      }
165
166
8125768
      if (!updated) {
167
        // if we didn't update current we don't need to add to the queue it's children
168
3949750
        Debug("bv-inequality-internal") << "  unchanged " << getTermNode(next) << "\n";
169
3949750
        continue;
170
      }
171
172
226268
      queue.push(next);
173
226268
      Debug("bv-inequality-internal") << "   enqueue " << getTermNode(next) << "\n";
174
    }
175
  }
176
211523
  return true;
177
}
178
179
15571
void InequalityGraph::computeExplanation(TermId from, TermId to, std::vector<ReasonId>& explanation) {
180
15571
  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
31142
  TermIdSet seen;
190
191
17209
  while(hasReason(to) && from != to && !seen.count(to)) {
192
819
    seen.insert(to);
193
1638
    const ModelValue& exp = getModelValue(to);
194
819
    Assert(exp.reason != UndefinedReasonId);
195
819
    explanation.push_back(exp.reason);
196
819
    Assert(exp.parent != UndefinedTermId);
197
819
    to = exp.parent;
198
1638
    Debug("bv-inequality-internal") << "  parent: " << getTermNode(to) << "\n"
199
819
                                    << "  reason: " << getReasonNode(exp.reason) << "\n";
200
  }
201
15571
}
202
203
1148247
void InequalityGraph::addEdge(TermId a, TermId b, bool strict, TermId reason) {
204
2296494
  Debug("bv-inequality-internal") << "InequalityGraph::addEdge " << getTermNode(a) << " => " << getTermNode(b) << "\n"
205
1148247
                                  << " strict ? " << strict << "\n";
206
1148247
  Edges& edges = getEdges(a);
207
1148247
  InequalityEdge new_edge(b, strict, reason);
208
1148247
  edges.push_back(new_edge);
209
1148247
  d_undoStack.push_back(std::make_pair(a, new_edge));
210
1148247
  d_undoStackIndex = d_undoStackIndex + 1;
211
1148247
}
212
213
921334
void InequalityGraph::initializeModelValue(TNode node) {
214
921334
  TermId id = getTermId(node);
215
921334
  Assert(!hasModelValue(id));
216
921334
  bool isConst = node.getKind() == kind::CONST_BITVECTOR;
217
921334
  unsigned size = utils::getSize(node);
218
1842668
  BitVector value = isConst? node.getConst<BitVector>() : BitVector(size, 0u);
219
921334
  setModelValue(id, ModelValue(value, UndefinedTermId, UndefinedReasonId));
220
921334
}
221
222
671736
bool InequalityGraph::isRegistered(TNode term) const {
223
671736
  return d_termNodeToIdMap.find(term) != d_termNodeToIdMap.end();
224
}
225
226
2296980
TermId InequalityGraph::registerTerm(TNode term) {
227
2296980
  if (d_termNodeToIdMap.find(term) != d_termNodeToIdMap.end()) {
228
2267780
    TermId id = d_termNodeToIdMap[term];
229
2267780
    if (!hasModelValue(id)) {
230
      // we could have backtracked and
231
728241
      initializeModelValue(term);
232
    }
233
2267780
    return id;
234
  }
235
236
  // store in node mapping
237
29200
  TermId id = d_termNodes.size();
238
29200
  Debug("bv-inequality-internal") << "InequalityGraph::registerTerm " << term << " => id"<< id << "\n";
239
240
29200
  d_termNodes.push_back(term);
241
29200
  d_termNodeToIdMap[term] = id;
242
243
  // create InequalityNode
244
29200
  unsigned size = utils::getSize(term);
245
246
29200
  bool isConst = term.getKind() == kind::CONST_BITVECTOR;
247
29200
  InequalityNode ineq = InequalityNode(id, size, isConst);
248
249
29200
  Assert(d_ineqNodes.size() == id);
250
29200
  d_ineqNodes.push_back(ineq);
251
252
29200
  Assert(d_ineqEdges.size() == id);
253
29200
  d_ineqEdges.push_back(Edges());
254
255
29200
  initializeModelValue(term);
256
257
29200
  return id;
258
}
259
260
1148473
ReasonId InequalityGraph::registerReason(TNode reason) {
261
1148473
  if (d_reasonToIdMap.find(reason) != d_reasonToIdMap.end()) {
262
1105363
    return d_reasonToIdMap[reason];
263
  }
264
43110
  d_reasonSet.insert(reason);
265
43110
  ReasonId id = d_reasonNodes.size();
266
43110
  d_reasonNodes.push_back(reason);
267
43110
  d_reasonToIdMap[reason] = id;
268
43110
  Debug("bv-inequality-internal") << "InequalityGraph::registerReason " << reason << " => id"<< id << "\n";
269
43110
  return id;
270
}
271
272
2260
TNode InequalityGraph::getReasonNode(ReasonId id) const {
273
2260
  Assert(d_reasonNodes.size() > id);
274
2260
  return d_reasonNodes[id];
275
}
276
277
19489958
TNode InequalityGraph::getTermNode(TermId id) const {
278
19489958
  Assert(d_termNodes.size() > id);
279
19489958
  return d_termNodes[id];
280
}
281
282
1532942
TermId InequalityGraph::getTermId(TNode node) const {
283
1532942
  Assert(d_termNodeToIdMap.find(node) != d_termNodeToIdMap.end());
284
1532942
  return d_termNodeToIdMap.find(node)->second;
285
}
286
287
618
void InequalityGraph::setConflict(const std::vector<ReasonId>& conflict) {
288
618
  Assert(!d_inConflict);
289
618
  d_inConflict = true;
290
618
  d_conflict.clear();
291
1862
  for (unsigned i = 0; i < conflict.size(); ++i) {
292
1244
    if (conflict[i] != AxiomReasonId) {
293
1244
      d_conflict.push_back(getReasonNode(conflict[i]));
294
    }
295
  }
296
618
  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
618
}
303
304
618
void InequalityGraph::getConflict(std::vector<TNode>& conflict) {
305
1862
  for (unsigned i = 0; i < d_conflict.size(); ++i) {
306
1244
    conflict.push_back(d_conflict[i]);
307
  }
308
618
}
309
310
1147602
void InequalityGraph::setModelValue(TermId term, const ModelValue& mv) {
311
1147602
  d_modelValues[term] = mv;
312
1147602
}
313
314
17239
InequalityGraph::ModelValue InequalityGraph::getModelValue(TermId term) const {
315
17239
  Assert(d_modelValues.find(term) != d_modelValues.end());
316
17239
  return (*(d_modelValues.find(term))).second;
317
}
318
319
11869746
bool InequalityGraph::hasModelValue(TermId id) const {
320
11869746
  return d_modelValues.find(id) != d_modelValues.end();
321
}
322
323
7857079
BitVector InequalityGraph::getValue(TermId id) const {
324
7857079
  Assert(hasModelValue(id));
325
7857079
  return (*(d_modelValues.find(id))).second.value;
326
}
327
328
16390
bool InequalityGraph::hasReason(TermId id) const {
329
32780
  const ModelValue& mv = getModelValue(id);
330
32780
  return mv.reason != UndefinedReasonId;
331
}
332
333
358202
bool InequalityGraph::addDisequality(TNode a, TNode b, TNode reason) {
334
358202
  Debug("bv-inequality") << "InequalityGraph::addDisequality " << reason << "\n";
335
358202
  d_disequalities.push_back(reason);
336
337
358202
  if (!isRegistered(a) || !isRegistered(b)) {
338
    //splitDisequality(reason);
339
52398
    return true;
340
  }
341
305804
  TermId id_a = getTermId(a);
342
305804
  TermId id_b = getTermId(b);
343
305804
  if (!hasModelValue(id_a)) {
344
93593
    initializeModelValue(a);
345
  }
346
305804
  if (!hasModelValue(id_b)) {
347
70300
    initializeModelValue(b);
348
  }
349
611608
  const BitVector val_a = getValue(id_a);
350
611608
  const BitVector val_b = getValue(id_b);
351
305804
  if (val_a == val_b) {
352
105928
    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
1042
      std::vector<ReasonId> explanation_ids;
355
521
      computeExplanation(UndefinedTermId, id_b, explanation_ids);
356
1042
      std::vector<TNode> explanation_nodes;
357
521
      explanation_nodes.push_back(reason);
358
575
      for (unsigned i = 0; i < explanation_ids.size(); ++i) {
359
54
        explanation_nodes.push_back(getReasonNode(explanation_ids[i]));
360
      }
361
1042
      Node explanation = utils::mkAnd(explanation_nodes);
362
521
      d_reasonSet.insert(explanation);
363
521
      return addInequality(a, b, true, explanation);
364
    }
365
105407
    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
28864
      std::vector<ReasonId> explanation_ids;
368
14432
      computeExplanation(UndefinedTermId, id_a, explanation_ids);
369
28864
      std::vector<TNode> explanation_nodes;
370
14432
      explanation_nodes.push_back(reason);
371
14575
      for (unsigned i = 0; i < explanation_ids.size(); ++i) {
372
143
        explanation_nodes.push_back(getReasonNode(explanation_ids[i]));
373
      }
374
28864
      Node explanation = utils::mkAnd(explanation_nodes);
375
14432
      d_reasonSet.insert(explanation);
376
14432
      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
399752
    Debug("bv-inequality-internal") << "Disequal: " << a << " => " << val_a.toString(10) << "\n"
382
199876
                                    << "          " << b << " => " << val_b.toString(10) << "\n";
383
  }
384
290851
  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
2201294
void InequalityGraph::backtrack() {
398
2201294
  Debug("bv-inequality-internal") << "InequalityGraph::backtrack()\n";
399
2201294
  int size = d_undoStack.size();
400
3349541
  for (int i = size - 1; i >= (int)d_undoStackIndex.get(); --i) {
401
1148247
    Assert(!d_undoStack.empty());
402
1148247
    TermId id = d_undoStack.back().first;
403
1148247
    InequalityEdge edge = d_undoStack.back().second;
404
1148247
    d_undoStack.pop_back();
405
406
2296494
    Debug("bv-inequality-internal") << " remove edge " << getTermNode(id) << " => "
407
1148247
                                                       << getTermNode(edge.next) <<"\n";
408
1148247
    Edges& edges = getEdges(id);
409
11203870
    for (Edges::const_iterator it = edges.begin(); it!= edges.end(); ++it) {
410
10055623
      Debug("bv-inequality-internal") << getTermNode(it->next) <<" " << it->strict << "\n";
411
    }
412
1148247
    Assert(!edges.empty());
413
1148247
    Assert(edges.back() == edge);
414
1148247
    edges.pop_back();
415
  }
416
2201294
}
417
418
7
Node InequalityGraph::makeDiseqSplitLemma(TNode diseq)
419
{
420
7
  Assert(diseq.getKind() == kind::NOT && diseq[0].getKind() == kind::EQUAL);
421
7
  NodeManager* nm = NodeManager::currentNM();
422
14
  TNode a = diseq[0][0];
423
14
  TNode b = diseq[0][1];
424
14
  Node a_lt_b = nm->mkNode(kind::BITVECTOR_ULT, a, b);
425
14
  Node b_lt_a = nm->mkNode(kind::BITVECTOR_ULT, b, a);
426
14
  Node eq = diseq[0];
427
7
  Node lemma = nm->mkNode(kind::OR, a_lt_b, b_lt_a, eq);
428
14
  return lemma;
429
}
430
431
44
void InequalityGraph::checkDisequalities(std::vector<Node>& lemmas) {
432
66
  for (CDQueue<TNode>::const_iterator it = d_disequalities.begin(); it != d_disequalities.end(); ++it) {
433
22
    if (d_disequalitiesAlreadySplit.find(*it) == d_disequalitiesAlreadySplit.end()) {
434
      // if we haven't already split on this disequality
435
34
      TNode diseq = *it;
436
17
      TermId a_id = registerTerm(diseq[0][0]);
437
17
      TermId b_id = registerTerm(diseq[0][1]);
438
17
      if (getValue(a_id) == getValue(b_id)) {
439
7
        lemmas.push_back(makeDiseqSplitLemma(diseq));
440
7
        d_disequalitiesAlreadySplit.insert(diseq);
441
      }
442
    }
443
  }
444
44
}
445
446
bool InequalityGraph::isLessThan(TNode a, TNode b) {
447
  Assert(isRegistered(a) && isRegistered(b));
448
  Unimplemented();
449
}
450
451
74
bool InequalityGraph::hasValueInModel(TNode node) const {
452
74
  if (isRegistered(node)) {
453
    TermId id = getTermId(node);
454
    return hasModelValue(id);
455
  }
456
74
  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
31
void InequalityGraph::getAllValuesInModel(std::vector<Node>& assignments)
466
{
467
31
  NodeManager* nm = NodeManager::currentNM();
468
186
  for (ModelValues::const_iterator it = d_modelValues.begin();
469
186
       it != d_modelValues.end();
470
       ++it)
471
  {
472
155
    TermId id = (*it).first;
473
310
    BitVector value = (*it).second.value;
474
310
    TNode var = getTermNode(id);
475
310
    Node constant = utils::mkConst(value);
476
310
    Node assignment = nm->mkNode(kind::EQUAL, var, constant);
477
155
    assignments.push_back(assignment);
478
155
    Debug("bitvector-model") << "   " << var << " => " << constant << "\n";
479
  }
480
27766
}