GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/error_set.h Lines: 47 92 51.1 %
Date: 2021-03-22 Branches: 12 138 8.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file error_set.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Tim King, Mathias Preiner, Morgan Deters
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 [[ Add one-line brief description here ]]
13
 **
14
 ** [[ Add lengthier description here ]]
15
 ** \todo document this file
16
 **/
17
18
#include "cvc4_private.h"
19
20
#pragma once
21
22
#include <vector>
23
24
#include "options/arith_options.h"
25
#include "theory/arith/arithvar.h"
26
#include "theory/arith/bound_counts.h"
27
#include "theory/arith/callbacks.h"
28
#include "theory/arith/delta_rational.h"
29
#include "theory/arith/partial_model.h"
30
#include "theory/arith/tableau_sizes.h"
31
#include "util/bin_heap.h"
32
#include "util/statistics_registry.h"
33
34
namespace CVC4 {
35
namespace theory {
36
namespace arith {
37
38
39
/**
40
 * The priority queue has 3 different modes of operation:
41
 * - Collection
42
 *   This passively collects arithmetic variables that may be inconsistent.
43
 *   This does not maintain any heap structure.
44
 *   dequeueInconsistentBasicVariable() does not work in this mode!
45
 *   Entering this mode requires the queue to be empty.
46
 *
47
 * - Difference Queue
48
 *   This mode uses the difference between a variables and its bound
49
 *   to determine which to dequeue first.
50
 *
51
 * - Variable Order Queue
52
 *   This mode uses the variable order to determine which ArithVar is dequeued first.
53
 *
54
 * The transitions between the modes of operation are:
55
 *  Collection => Difference Queue
56
 *  Difference Queue => Variable Order Queue
57
 *  Difference Queue => Collection (queue must be empty!)
58
 *  Variable Order Queue => Collection (queue must be empty!)
59
 *
60
 * The queue begins in Collection mode.
61
 */
62
63
64
class ErrorSet;
65
66
class ComparatorPivotRule {
67
private:
68
  const ErrorSet* d_errorSet;
69
70
  options::ErrorSelectionRule d_rule;
71
72
 public:
73
  ComparatorPivotRule();
74
  ComparatorPivotRule(const ErrorSet* es, options::ErrorSelectionRule r);
75
76
  bool operator()(ArithVar v, ArithVar u) const;
77
  options::ErrorSelectionRule getRule() const { return d_rule; }
78
};
79
80
// typedef boost::heap::d_ary_heap<
81
//   ArithVar,
82
//   boost::heap::arity<2>,
83
//   boost::heap::compare<ComparatorPivotRule>,
84
//   boost::heap::mutable_<true> > FocusSet;
85
//
86
// typedef FocusSet::handle_type FocusSetHandle;
87
88
// typedef CVC4_PB_DS_NAMESPACE::priority_queue<
89
//   ArithVar,
90
//   ComparatorPivotRule,
91
//   CVC4_PB_DS_NAMESPACE::pairing_heap_tag> FocusSet;
92
93
// typedef FocusSet::point_iterator FocusSetHandle;
94
95
typedef BinaryHeap<ArithVar, ComparatorPivotRule> FocusSet;
96
typedef FocusSet::handle FocusSetHandle;
97
98
99
class ErrorInformation {
100
private:
101
  /** The variable that is in error. */
102
  ArithVar d_variable;
103
104
  /**
105
   * The constraint that was violated.
106
   * This needs to be saved in case that the
107
   * violated constraint
108
   */
109
  ConstraintP d_violated;
110
111
  /**
112
   * This is the sgn of the first derivate the variable must move to satisfy
113
   * the bound violated.
114
   * If d_sgn > 0, then d_violated was a lowerbound.
115
   * If d_sgn < 0, then d_violated was an upperbound.
116
   */
117
  int d_sgn;
118
119
  /**
120
   * If this is true, then the bound is no longer set on d_variables.
121
   * This MUST be undone before this is deleted.
122
   */
123
  bool d_relaxed;
124
125
  /**
126
   * If this is true, then the variable is in the focus set and the focus heap.
127
   * d_handle is then a reasonable thing to interpret.
128
   * If this is false, the variable is somewhere in
129
   */
130
  bool d_inFocus;
131
  FocusSetHandle d_handle;
132
133
  /**
134
   * Auxillary information for storing the difference between a variable and its bound.
135
   * Only set on signals.
136
   */
137
  DeltaRational* d_amount;
138
139
  /** */
140
  uint32_t d_metric;
141
142
public:
143
  ErrorInformation();
144
  ErrorInformation(ArithVar var, ConstraintP vio, int sgn);
145
  ~ErrorInformation();
146
  ErrorInformation(const ErrorInformation& ei);
147
  ErrorInformation& operator=(const ErrorInformation& ei);
148
149
  void reset(ConstraintP c, int sgn);
150
151
281844
  inline ArithVar getVariable() const { return d_variable; }
152
153
300314
  bool isRelaxed() const { return d_relaxed; }
154
  void setRelaxed()
155
  {
156
    Assert(!d_relaxed);
157
    d_relaxed = true;
158
  }
159
  void setUnrelaxed()
160
  {
161
    Assert(d_relaxed);
162
    d_relaxed = false;
163
  }
164
165
1072920
  inline int sgn() const { return d_sgn; }
166
167
704065
  inline bool inFocus() const { return d_inFocus; }
168
536460
  inline int focusSgn() const {
169
536460
    return (d_inFocus) ? sgn() : 0;
170
  }
171
172
700931
  inline void setInFocus(bool inFocus) { d_inFocus = inFocus; }
173
174
1005130
  const DeltaRational& getAmount() const {
175
1005130
    Assert(d_amount != NULL);
176
1005130
    return *d_amount;
177
  }
178
179
  void setAmount(const DeltaRational& am);
180
  void setMetric(uint32_t m) { d_metric = m; }
181
  uint32_t getMetric() const { return d_metric; }
182
183
569395
  inline void setHandle(FocusSetHandle h) {
184
569395
    Assert(d_inFocus);
185
569395
    d_handle = h;
186
569395
  }
187
362477
  inline const FocusSetHandle& getHandle() const{ return d_handle; }
188
189
  inline ConstraintP getViolated() const { return d_violated; }
190
191
700931
  bool debugInitialized() const {
192
    return
193
1401862
      d_variable != ARITHVAR_SENTINEL &&
194
1401862
      d_violated != NullConstraint &&
195
1401862
      d_sgn != 0;
196
  }
197
  void print(std::ostream& os) const {
198
    os << "{ErrorInfo: " << d_variable
199
       << ", " << d_violated
200
       << ", " << d_sgn
201
       << ", " << d_relaxed
202
       << ", " << d_inFocus;
203
    if(d_amount == NULL){
204
      os << "NULL";
205
    }else{
206
      os << (*d_amount);
207
    }
208
    os << "}";
209
  }
210
};
211
212
17987
class ErrorInfoMap : public DenseMap<ErrorInformation> {};
213
214
8992
class ErrorSet {
215
private:
216
  /**
217
   * Reference to the arithmetic partial model for checking if a variable
218
   * is consistent with its upper and lower bounds.
219
   */
220
  ArithVariables& d_variables;
221
222
  /**
223
   * The set of all variables that violate exactly one of their bounds.
224
   */
225
  ErrorInfoMap d_errInfo;
226
227
  options::ErrorSelectionRule d_selectionRule;
228
  /**
229
   * The ordered heap for the variables that are in ErrorSet.
230
   */
231
  FocusSet d_focus;
232
233
234
  /**
235
   * A strict subset of the error set.
236
   *   d_outOfFocus \neq d_errInfo.
237
   *
238
   * Its symbolic complement is Focus.
239
   *   d_outOfFocus \intersect Focus == \emptyset
240
   *   d_outOfFocus \union Focus == d_errInfo
241
   */
242
  ArithVarVec d_outOfFocus;
243
244
  /**
245
   * Before a variable is added to the error set, it is added to the signals list.
246
   * A variable may appear on the list multiple times.
247
   * This introduces a delay.
248
   */
249
  ArithVarVec d_signals;
250
251
  TableauSizes d_tableauSizes;
252
253
  BoundCountingLookup d_boundLookup;
254
255
  /**
256
   * Computes the difference between the assignment and its bound for x.
257
   */
258
public:
259
  DeltaRational computeDiff(ArithVar x) const;
260
private:
261
 void recomputeAmount(ErrorInformation& ei, options::ErrorSelectionRule r);
262
263
 void update(ErrorInformation& ei);
264
 void transitionVariableOutOfError(ArithVar v);
265
 void transitionVariableIntoError(ArithVar v);
266
 void addBackIntoFocus(ArithVar v);
267
268
public:
269
270
  /** The new focus set is the entire error set. */
271
  void blur();
272
  void dropFromFocus(ArithVar v);
273
274
  void dropFromFocusAll(const ArithVarVec& vec) {
275
    for(ArithVarVec::const_iterator i = vec.begin(), i_end = vec.end(); i != i_end; ++i){
276
      ArithVar v = *i;
277
      dropFromFocus(v);
278
    }
279
  }
280
281
  ErrorSet(ArithVariables& var, TableauSizes tabSizes, BoundCountingLookup boundLookup);
282
283
  typedef ErrorInfoMap::const_iterator error_iterator;
284
794577
  error_iterator errorBegin() const { return d_errInfo.begin(); }
285
794577
  error_iterator errorEnd() const { return d_errInfo.end(); }
286
287
7482538
  bool inError(ArithVar v) const { return d_errInfo.isKey(v); }
288
  bool inFocus(ArithVar v) const { return d_errInfo[v].inFocus(); }
289
290
  void pushErrorInto(ArithVarVec& vec) const;
291
  void pushFocusInto(ArithVarVec& vec) const;
292
293
  options::ErrorSelectionRule getSelectionRule() const;
294
  void setSelectionRule(options::ErrorSelectionRule rule);
295
296
194887
  inline ArithVar topFocusVariable() const{
297
194887
    Assert(!focusEmpty());
298
194887
    return d_focus.top();
299
  }
300
301
7482926
  inline void signalVariable(ArithVar var){
302
7482926
    d_signals.push_back(var);
303
7482926
  }
304
305
  inline void signalUnderCnd(ArithVar var, bool b){
306
    if(b){ signalVariable(var); }
307
  }
308
309
7942730
  inline bool inconsistent(ArithVar var) const{
310
7942730
    return !d_variables.assignmentIsConsistent(var) ;
311
  }
312
  inline void signalIfInconsistent(ArithVar var){
313
    signalUnderCnd(var, inconsistent(var));
314
  }
315
316
2768682
  inline bool errorEmpty() const{
317
2768682
    return d_errInfo.empty();
318
  }
319
1379238
  inline uint32_t errorSize() const{
320
1379238
    return d_errInfo.size();
321
  }
322
323
609833
  inline bool focusEmpty() const {
324
609833
    return d_focus.empty();
325
  }
326
  inline uint32_t focusSize() const{
327
    return d_focus.size();
328
  }
329
330
  inline int getSgn(ArithVar x) const {
331
    Assert(inError(x));
332
    return d_errInfo[x].sgn();
333
  }
334
  inline int focusSgn(ArithVar v) const {
335
    if(inError(v)){
336
      return d_errInfo[v].focusSgn();
337
    }else{
338
      return 0;
339
    }
340
  }
341
342
  void focusDownToJust(ArithVar v);
343
344
  void clearFocus();
345
346
  /** Clears the set. */
347
  void clear();
348
  void reduceToSignals();
349
350
19593737
  bool noSignals() const {
351
19593737
    return d_signals.empty();
352
  }
353
18529634
  bool moreSignals() const {
354
18529634
    return !noSignals();
355
  }
356
7482538
  ArithVar topSignal() const {
357
7482538
    Assert(moreSignals());
358
7482538
    return d_signals.back();
359
  }
360
361
  /**
362
   * Moves a variable out of the signals.
363
   * This moves it into the error set.
364
   * Return the previous focus sign.
365
   */
366
  int popSignal();
367
368
1005130
  const DeltaRational& getAmount(ArithVar v) const {
369
1005130
    return d_errInfo[v].getAmount();
370
  }
371
372
  uint32_t sumMetric(ArithVar a) const{
373
    Assert(inError(a));
374
    BoundCounts bcs = d_boundLookup.atBounds(a);
375
    uint32_t count = getSgn(a) > 0 ? bcs.upperBoundCount() : bcs.lowerBoundCount();
376
377
    uint32_t length = d_tableauSizes.getRowLength(a);
378
379
    return (length - count);
380
  }
381
382
  uint32_t getMetric(ArithVar a) const {
383
    return d_errInfo[a].getMetric();
384
  }
385
386
  ConstraintP getViolated(ArithVar a) const {
387
    return d_errInfo[a].getViolated();
388
  }
389
390
391
  typedef FocusSet::const_iterator focus_iterator;
392
  focus_iterator focusBegin() const { return d_focus.begin(); }
393
  focus_iterator focusEnd() const { return d_focus.end(); }
394
395
  void debugPrint(std::ostream& out) const;
396
397
private:
398
  class Statistics {
399
  public:
400
    IntStat d_enqueues;
401
    IntStat d_enqueuesCollection;
402
    IntStat d_enqueuesDiffMode;
403
    IntStat d_enqueuesVarOrderMode;
404
405
    IntStat d_enqueuesCollectionDuplicates;
406
    IntStat d_enqueuesVarOrderModeDuplicates;
407
408
    Statistics();
409
    ~Statistics();
410
  };
411
412
  Statistics d_statistics;
413
};
414
415
}/* CVC4::theory::arith namespace */
416
}/* CVC4::theory namespace */
417
}/* CVC4 namespace */