GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/error_set.cpp Lines: 201 312 64.4 %
Date: 2021-03-23 Branches: 179 649 27.6 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file error_set.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Tim King, 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 [[ Add one-line brief description here ]]
13
 **
14
 ** [[ Add lengthier description here ]]
15
 ** \todo document this file
16
 **/
17
18
#include "theory/arith/error_set.h"
19
20
#include "smt/smt_statistics_registry.h"
21
#include "theory/arith/constraint.h"
22
23
using namespace std;
24
25
namespace CVC4 {
26
namespace theory {
27
namespace arith {
28
29
30
530785
ErrorInformation::ErrorInformation()
31
  : d_variable(ARITHVAR_SENTINEL)
32
  , d_violated(NullConstraint)
33
  , d_sgn(0)
34
  , d_relaxed(false)
35
  , d_inFocus(false)
36
  , d_handle()
37
  , d_amount(NULL)
38
530785
  , d_metric(0)
39
{
40
530785
  Debug("arith::error::mem") << "def constructor " << d_variable << " "  << d_amount << endl;
41
530785
}
42
43
401846
ErrorInformation::ErrorInformation(ArithVar var, ConstraintP vio, int sgn)
44
  : d_variable(var)
45
  , d_violated(vio)
46
  , d_sgn(sgn)
47
  , d_relaxed(false)
48
  , d_inFocus(false)
49
  , d_handle()
50
  , d_amount(NULL)
51
401846
  , d_metric(0)
52
{
53
401846
  Assert(debugInitialized());
54
401846
  Debug("arith::error::mem") << "constructor " << d_variable << " "  << d_amount << endl;
55
401846
}
56
57
58
2118270
ErrorInformation::~ErrorInformation() {
59
1059135
  Assert(d_relaxed != true);
60
1059135
  if(d_amount != NULL){
61
842
    Debug("arith::error::mem") << d_amount << endl;
62
842
    Debug("arith::error::mem") << "destroy " << d_variable << " "  << d_amount << endl;
63
842
    delete d_amount;
64
842
    d_amount = NULL;
65
  }
66
1059135
}
67
68
126504
ErrorInformation::ErrorInformation(const ErrorInformation& ei)
69
126504
  : d_variable(ei.d_variable)
70
126504
  , d_violated(ei.d_violated)
71
126504
  , d_sgn(ei.d_sgn)
72
126504
  , d_relaxed(ei.d_relaxed)
73
126504
  , d_inFocus(ei.d_inFocus)
74
  , d_handle(ei.d_handle)
75
632520
  , d_metric(0)
76
{
77
126504
  if(ei.d_amount == NULL){
78
126276
    d_amount = NULL;
79
  }else{
80
228
    d_amount = new DeltaRational(*ei.d_amount);
81
  }
82
126504
  Debug("arith::error::mem") << "copy const " << d_variable << " "  << d_amount << endl;
83
126504
}
84
85
802560
ErrorInformation& ErrorInformation::operator=(const ErrorInformation& ei){
86
802560
  d_variable = ei.d_variable;
87
802560
  d_violated = ei.d_violated;
88
802560
  d_sgn = ei.d_sgn;
89
802560
  d_relaxed = (ei.d_relaxed);
90
802560
  d_inFocus = (ei.d_inFocus);
91
802560
  d_handle = (ei.d_handle);
92
802560
  d_metric = ei.d_metric;
93
802560
  if(d_amount != NULL && ei.d_amount != NULL){
94
    Debug("arith::error::mem") << "assignment assign " << d_variable << " "  << d_amount << endl;
95
    *d_amount = *ei.d_amount;
96
802560
  }else if(ei.d_amount != NULL){
97
    d_amount = new DeltaRational(*ei.d_amount);
98
    Debug("arith::error::mem") << "assignment alloc " << d_variable << " "  << d_amount << endl;
99
802560
  }else if(d_amount != NULL){
100
231783
    Debug("arith::error::mem") << "assignment release " << d_variable << " "  << d_amount << endl;
101
231783
    delete d_amount;
102
231783
    d_amount = NULL;
103
  }else{
104
570777
    d_amount = NULL;
105
  }
106
802560
  return *this;
107
}
108
109
1173
void ErrorInformation::reset(ConstraintP c, int sgn){
110
1173
  Assert(!isRelaxed());
111
1173
  Assert(c != NullConstraint);
112
1173
  d_violated = c;
113
1173
  d_sgn = sgn;
114
115
1173
  if(d_amount != NULL){
116
230
    delete d_amount;
117
230
    Debug("arith::error::mem") << "reset " << d_variable << " "  << d_amount << endl;
118
230
    d_amount = NULL;
119
  }
120
1173
}
121
122
295773
void ErrorInformation::setAmount(const DeltaRational& am){
123
295773
  if(d_amount == NULL){
124
232627
    d_amount = new DeltaRational;
125
232627
    Debug("arith::error::mem") << "setAmount " << d_variable << " "  << d_amount << endl;
126
  }
127
295773
  (*d_amount) = am;
128
295773
}
129
130
8997
ErrorSet::Statistics::Statistics():
131
  d_enqueues("theory::arith::pqueue::enqueues", 0),
132
  d_enqueuesCollection("theory::arith::pqueue::enqueuesCollection", 0),
133
  d_enqueuesDiffMode("theory::arith::pqueue::enqueuesDiffMode", 0),
134
  d_enqueuesVarOrderMode("theory::arith::pqueue::enqueuesVarOrderMode", 0),
135
  d_enqueuesCollectionDuplicates("theory::arith::pqueue::enqueuesCollectionDuplicates", 0),
136
8997
  d_enqueuesVarOrderModeDuplicates("theory::arith::pqueue::enqueuesVarOrderModeDuplicates", 0)
137
{
138
8997
  smtStatisticsRegistry()->registerStat(&d_enqueues);
139
8997
  smtStatisticsRegistry()->registerStat(&d_enqueuesCollection);
140
8997
  smtStatisticsRegistry()->registerStat(&d_enqueuesDiffMode);
141
8997
  smtStatisticsRegistry()->registerStat(&d_enqueuesVarOrderMode);
142
8997
  smtStatisticsRegistry()->registerStat(&d_enqueuesCollectionDuplicates);
143
8997
  smtStatisticsRegistry()->registerStat(&d_enqueuesVarOrderModeDuplicates);
144
8997
}
145
146
17988
ErrorSet::Statistics::~Statistics(){
147
8994
  smtStatisticsRegistry()->unregisterStat(&d_enqueues);
148
8994
  smtStatisticsRegistry()->unregisterStat(&d_enqueuesCollection);
149
8994
  smtStatisticsRegistry()->unregisterStat(&d_enqueuesDiffMode);
150
8994
  smtStatisticsRegistry()->unregisterStat(&d_enqueuesVarOrderMode);
151
8994
  smtStatisticsRegistry()->unregisterStat(&d_enqueuesCollectionDuplicates);
152
8994
  smtStatisticsRegistry()->unregisterStat(&d_enqueuesVarOrderModeDuplicates);
153
8994
}
154
155
8997
ErrorSet::ErrorSet(ArithVariables& vars,
156
                   TableauSizes tabSizes,
157
8997
                   BoundCountingLookup lookups)
158
    : d_variables(vars),
159
      d_errInfo(),
160
      d_selectionRule(options::ErrorSelectionRule::VAR_ORDER),
161
17994
      d_focus(ComparatorPivotRule(this, d_selectionRule)),
162
      d_outOfFocus(),
163
      d_signals(),
164
      d_tableauSizes(tabSizes),
165
26991
      d_boundLookup(lookups)
166
8997
{}
167
168
2477983
options::ErrorSelectionRule ErrorSet::getSelectionRule() const
169
{
170
2477983
  return d_selectionRule;
171
}
172
173
167641
void ErrorSet::recomputeAmount(ErrorInformation& ei,
174
                               options::ErrorSelectionRule rule)
175
{
176
167641
  switch(rule){
177
155208
    case options::ErrorSelectionRule::MINIMUM_AMOUNT:
178
    case options::ErrorSelectionRule::MAXIMUM_AMOUNT:
179
155208
      ei.setAmount(computeDiff(ei.getVariable()));
180
155208
      break;
181
    case options::ErrorSelectionRule::SUM_METRIC:
182
      ei.setMetric(sumMetric(ei.getVariable()));
183
      break;
184
12433
    case options::ErrorSelectionRule::VAR_ORDER:
185
      // do nothing
186
12433
      break;
187
  }
188
167641
}
189
190
919401
void ErrorSet::setSelectionRule(options::ErrorSelectionRule rule)
191
{
192
919401
  if(rule != getSelectionRule()){
193
324682
    FocusSet into(ComparatorPivotRule(this, rule));
194
162341
    FocusSet::const_iterator iter = d_focus.begin();
195
162341
    FocusSet::const_iterator i_end = d_focus.end();
196
497623
    for(; iter != i_end; ++iter){
197
167641
      ArithVar v = *iter;
198
167641
      ErrorInformation& ei = d_errInfo.get(v);
199
167641
      if(ei.inFocus()){
200
167641
        recomputeAmount(ei, rule);
201
167641
        FocusSetHandle handle = into.push(v);
202
167641
        ei.setHandle(handle);
203
      }
204
    }
205
162341
    d_focus.swap(into);
206
162341
    d_selectionRule = rule;
207
  }
208
919401
  Assert(getSelectionRule() == rule);
209
919401
}
210
211
171338
ComparatorPivotRule::ComparatorPivotRule(const ErrorSet* es,
212
171338
                                         options::ErrorSelectionRule r)
213
171338
    : d_errorSet(es), d_rule(r)
214
171338
{}
215
216
1062198
bool ComparatorPivotRule::operator()(ArithVar v, ArithVar u) const {
217
1062198
  switch(d_rule){
218
559625
    case options::ErrorSelectionRule::VAR_ORDER:
219
      // This needs to be the reverse of the minVariableOrder
220
559625
      return v > u;
221
    case options::ErrorSelectionRule::SUM_METRIC:
222
    {
223
      uint32_t v_metric = d_errorSet->getMetric(v);
224
      uint32_t u_metric = d_errorSet->getMetric(u);
225
      if(v_metric == u_metric){
226
        return v > u;
227
      }else{
228
        return v_metric > u_metric;
229
      }
230
    }
231
502573
    case options::ErrorSelectionRule::MINIMUM_AMOUNT:
232
    {
233
502573
      const DeltaRational& vamt = d_errorSet->getAmount(v);
234
502573
      const DeltaRational& uamt = d_errorSet->getAmount(u);
235
502573
      int cmp = vamt.cmp(uamt);
236
502573
      if(cmp == 0){
237
197887
        return v > u;
238
      }else{
239
304686
        return cmp > 0;
240
      }
241
    }
242
    case options::ErrorSelectionRule::MAXIMUM_AMOUNT:
243
    {
244
      const DeltaRational& vamt = d_errorSet->getAmount(v);
245
      const DeltaRational& uamt = d_errorSet->getAmount(u);
246
      int cmp = vamt.cmp(uamt);
247
      if(cmp == 0){
248
        return v > u;
249
      }else{
250
        return cmp < 0;
251
      }
252
    }
253
  }
254
  Unreachable();
255
}
256
257
237335
void ErrorSet::update(ErrorInformation& ei){
258
237335
  if(ei.inFocus()){
259
260
237335
    switch(getSelectionRule()){
261
63336
      case options::ErrorSelectionRule::MINIMUM_AMOUNT:
262
      case options::ErrorSelectionRule::MAXIMUM_AMOUNT:
263
63336
        ei.setAmount(computeDiff(ei.getVariable()));
264
63336
        d_focus.update(ei.getHandle(), ei.getVariable());
265
63336
        break;
266
      case options::ErrorSelectionRule::SUM_METRIC:
267
        ei.setMetric(sumMetric(ei.getVariable()));
268
        d_focus.update(ei.getHandle(), ei.getVariable());
269
        break;
270
173999
      case options::ErrorSelectionRule::VAR_ORDER:
271
        // do nothing
272
173999
        break;
273
    }
274
  }
275
237335
}
276
277
/** A variable becomes satisfied. */
278
299181
void ErrorSet::transitionVariableOutOfError(ArithVar v) {
279
299181
  Assert(!inconsistent(v));
280
299181
  ErrorInformation& ei = d_errInfo.get(v);
281
299181
  Assert(ei.debugInitialized());
282
299181
  if(ei.isRelaxed()){
283
    ConstraintP viol = ei.getViolated();
284
    if(ei.sgn() > 0){
285
      d_variables.setLowerBoundConstraint(viol);
286
    }else{
287
      d_variables.setUpperBoundConstraint(viol);
288
    }
289
    Assert(!inconsistent(v));
290
    ei.setUnrelaxed();
291
  }
292
299181
  if(ei.inFocus()){
293
299181
    d_focus.erase(ei.getHandle());
294
299181
    ei.setInFocus(false);
295
  }
296
299181
  d_errInfo.remove(v);
297
299181
}
298
299
300
401846
void ErrorSet::transitionVariableIntoError(ArithVar v) {
301
401846
  Assert(inconsistent(v));
302
401846
  bool vilb = d_variables.cmpAssignmentLowerBound(v) < 0;
303
401846
  int sgn = vilb ? 1 : -1;
304
803692
  ConstraintP c = vilb ?
305
803692
    d_variables.getLowerBoundConstraint(v) : d_variables.getUpperBoundConstraint(v);
306
401846
  d_errInfo.set(v, ErrorInformation(v, c, sgn));
307
401846
  ErrorInformation& ei = d_errInfo.get(v);
308
309
401846
  switch(getSelectionRule()){
310
77229
    case options::ErrorSelectionRule::MINIMUM_AMOUNT:
311
    case options::ErrorSelectionRule::MAXIMUM_AMOUNT:
312
77229
      ei.setAmount(computeDiff(v));
313
77229
      break;
314
    case options::ErrorSelectionRule::SUM_METRIC:
315
      ei.setMetric(sumMetric(ei.getVariable()));
316
      break;
317
324617
    case options::ErrorSelectionRule::VAR_ORDER:
318
      // do nothing
319
324617
      break;
320
  }
321
401846
  ei.setInFocus(true);
322
401846
  FocusSetHandle handle = d_focus.push(v);
323
401846
  ei.setHandle(handle);
324
401846
}
325
326
void ErrorSet::dropFromFocus(ArithVar v) {
327
  Assert(inError(v));
328
  ErrorInformation& ei = d_errInfo.get(v);
329
  Assert(ei.inFocus());
330
  d_focus.erase(ei.getHandle());
331
  ei.setInFocus(false);
332
  d_outOfFocus.push_back(v);
333
}
334
335
void ErrorSet::addBackIntoFocus(ArithVar v) {
336
  Assert(inError(v));
337
  ErrorInformation& ei = d_errInfo.get(v);
338
  Assert(!ei.inFocus());
339
  switch(getSelectionRule()){
340
    case options::ErrorSelectionRule::MINIMUM_AMOUNT:
341
    case options::ErrorSelectionRule::MAXIMUM_AMOUNT:
342
      ei.setAmount(computeDiff(v));
343
      break;
344
    case options::ErrorSelectionRule::SUM_METRIC:
345
      ei.setMetric(sumMetric(v));
346
      break;
347
    case options::ErrorSelectionRule::VAR_ORDER:
348
      // do nothing
349
      break;
350
  }
351
352
  ei.setInFocus(true);
353
  FocusSetHandle handle = d_focus.push(v);
354
  ei.setHandle(handle);
355
}
356
357
void ErrorSet::blur(){
358
  while(!d_outOfFocus.empty()){
359
    ArithVar v = d_outOfFocus.back();
360
    d_outOfFocus.pop_back();
361
362
    if(inError(v) && !inFocus(v)){
363
      addBackIntoFocus(v);
364
    }
365
  }
366
}
367
368
369
370
7482793
int ErrorSet::popSignal() {
371
7482793
  ArithVar back = d_signals.back();
372
7482793
  d_signals.pop_back();
373
374
7482793
  if(inError(back)){
375
536516
    ErrorInformation& ei = d_errInfo.get(back);
376
536516
    int prevSgn = ei.sgn();
377
536516
    int focusSgn = ei.focusSgn();
378
536516
    bool vilb = d_variables.cmpAssignmentLowerBound(back) < 0;
379
536516
    bool viub = d_variables.cmpAssignmentUpperBound(back) > 0;
380
536516
    if(vilb || viub){
381
237335
      Assert(!vilb || !viub);
382
237335
      int currSgn = vilb ? 1 : -1;
383
237335
      if(currSgn != prevSgn){
384
1793
        ConstraintP curr = vilb ?  d_variables.getLowerBoundConstraint(back)
385
1793
          : d_variables.getUpperBoundConstraint(back);
386
1173
        ei.reset(curr, currSgn);
387
      }
388
237335
      update(ei);
389
    }else{
390
299181
      transitionVariableOutOfError(back);
391
    }
392
536516
    return focusSgn;
393
6946277
  }else if(inconsistent(back)){
394
401846
    transitionVariableIntoError(back);
395
  }
396
6946277
  return 0;
397
}
398
399
void ErrorSet::clear(){
400
  // Nothing should be relaxed!
401
  d_signals.clear();
402
  d_errInfo.purge();
403
  d_focus.clear();
404
}
405
406
void ErrorSet::clearFocus(){
407
  for(ErrorSet::focus_iterator i =focusBegin(), i_end = focusEnd(); i != i_end; ++i){
408
    ArithVar f = *i;
409
    ErrorInformation& fei = d_errInfo.get(f);
410
    fei.setInFocus(false);
411
    d_outOfFocus.push_back(f);
412
  }
413
  d_focus.clear();
414
}
415
416
794648
void ErrorSet::reduceToSignals(){
417
896181
  for(error_iterator ei=errorBegin(), ei_end=errorEnd(); ei != ei_end; ++ei){
418
101533
    ArithVar curr = *ei;
419
101533
    signalVariable(curr);
420
  }
421
422
794648
  d_errInfo.purge();
423
794648
  d_focus.clear();
424
794648
  d_outOfFocus.clear();
425
794648
}
426
427
295773
DeltaRational ErrorSet::computeDiff(ArithVar v) const{
428
295773
  Assert(inconsistent(v));
429
295773
  const DeltaRational& beta = d_variables.getAssignment(v);
430
295773
  DeltaRational diff = d_variables.cmpAssignmentLowerBound(v) < 0 ?
431
151641
    d_variables.getLowerBound(v) - beta:
432
447414
    beta - d_variables.getUpperBound(v);
433
434
295773
  Assert(diff.sgn() > 0);
435
295773
  return diff;
436
}
437
438
void ErrorSet::debugPrint(std::ostream& out) const {
439
  static int instance = 0;
440
  ++instance;
441
  out << "error set debugprint " << instance << endl;
442
  for(error_iterator i = errorBegin(), i_end = errorEnd();
443
      i != i_end; ++i){
444
    ArithVar e = *i;
445
    const ErrorInformation& ei = d_errInfo[e];
446
    ei.print(out);
447
    out << "  ";
448
    d_variables.printModel(e, out);
449
    out << endl;
450
  }
451
  out << "focus ";
452
  for(focus_iterator i = focusBegin(), i_end = focusEnd();
453
      i != i_end; ++i){
454
    out << *i << " ";
455
  }
456
  out << ";" << endl;
457
}
458
459
void ErrorSet::focusDownToJust(ArithVar v) {
460
  clearFocus();
461
462
  ErrorInformation& vei = d_errInfo.get(v);
463
  vei.setInFocus(true);
464
  FocusSetHandle handle = d_focus.push(v);
465
  vei.setHandle(handle);
466
}
467
468
void ErrorSet::pushErrorInto(ArithVarVec& vec) const{
469
  for(error_iterator i = errorBegin(), e = errorEnd(); i != e; ++i ){
470
    vec.push_back(*i);
471
  }
472
}
473
474
void ErrorSet::pushFocusInto(ArithVarVec& vec) const{
475
  for(focus_iterator i = focusBegin(), e = focusEnd(); i != e; ++i ){
476
    vec.push_back(*i);
477
  }
478
}
479
480
}/* CVC4::theory::arith namespace */
481
}/* CVC4::theory namespace */
482
26685
}/* CVC4 namespace */