GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bv/bv_inequality_graph.h Lines: 41 41 100.0 %
Date: 2021-03-22 Branches: 23 82 28.0 %

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