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

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