GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/error_set.cpp Lines: 201 312 64.4 %
Date: 2021-03-22 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
530661
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
530661
  , d_metric(0)
39
{
40
530661
  Debug("arith::error::mem") << "def constructor " << d_variable << " "  << d_amount << endl;
41
530661
}
42
43
401790
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
401790
  , d_metric(0)
52
{
53
401790
  Assert(debugInitialized());
54
401790
  Debug("arith::error::mem") << "constructor " << d_variable << " "  << d_amount << endl;
55
401790
}
56
57
58
2117830
ErrorInformation::~ErrorInformation() {
59
1058915
  Assert(d_relaxed != true);
60
1058915
  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
1058915
}
67
68
126464
ErrorInformation::ErrorInformation(const ErrorInformation& ei)
69
126464
  : d_variable(ei.d_variable)
70
126464
  , d_violated(ei.d_violated)
71
126464
  , d_sgn(ei.d_sgn)
72
126464
  , d_relaxed(ei.d_relaxed)
73
126464
  , d_inFocus(ei.d_inFocus)
74
  , d_handle(ei.d_handle)
75
632320
  , d_metric(0)
76
{
77
126464
  if(ei.d_amount == NULL){
78
126236
    d_amount = NULL;
79
  }else{
80
228
    d_amount = new DeltaRational(*ei.d_amount);
81
  }
82
126464
  Debug("arith::error::mem") << "copy const " << d_variable << " "  << d_amount << endl;
83
126464
}
84
85
802448
ErrorInformation& ErrorInformation::operator=(const ErrorInformation& ei){
86
802448
  d_variable = ei.d_variable;
87
802448
  d_violated = ei.d_violated;
88
802448
  d_sgn = ei.d_sgn;
89
802448
  d_relaxed = (ei.d_relaxed);
90
802448
  d_inFocus = (ei.d_inFocus);
91
802448
  d_handle = (ei.d_handle);
92
802448
  d_metric = ei.d_metric;
93
802448
  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
802448
  }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
802448
  }else if(d_amount != NULL){
100
231731
    Debug("arith::error::mem") << "assignment release " << d_variable << " "  << d_amount << endl;
101
231731
    delete d_amount;
102
231731
    d_amount = NULL;
103
  }else{
104
570717
    d_amount = NULL;
105
  }
106
802448
  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
295721
void ErrorInformation::setAmount(const DeltaRational& am){
123
295721
  if(d_amount == NULL){
124
232575
    d_amount = new DeltaRational;
125
232575
    Debug("arith::error::mem") << "setAmount " << d_variable << " "  << d_amount << endl;
126
  }
127
295721
  (*d_amount) = am;
128
295721
}
129
130
8995
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
8995
  d_enqueuesVarOrderModeDuplicates("theory::arith::pqueue::enqueuesVarOrderModeDuplicates", 0)
137
{
138
8995
  smtStatisticsRegistry()->registerStat(&d_enqueues);
139
8995
  smtStatisticsRegistry()->registerStat(&d_enqueuesCollection);
140
8995
  smtStatisticsRegistry()->registerStat(&d_enqueuesDiffMode);
141
8995
  smtStatisticsRegistry()->registerStat(&d_enqueuesVarOrderMode);
142
8995
  smtStatisticsRegistry()->registerStat(&d_enqueuesCollectionDuplicates);
143
8995
  smtStatisticsRegistry()->registerStat(&d_enqueuesVarOrderModeDuplicates);
144
8995
}
145
146
17984
ErrorSet::Statistics::~Statistics(){
147
8992
  smtStatisticsRegistry()->unregisterStat(&d_enqueues);
148
8992
  smtStatisticsRegistry()->unregisterStat(&d_enqueuesCollection);
149
8992
  smtStatisticsRegistry()->unregisterStat(&d_enqueuesDiffMode);
150
8992
  smtStatisticsRegistry()->unregisterStat(&d_enqueuesVarOrderMode);
151
8992
  smtStatisticsRegistry()->unregisterStat(&d_enqueuesCollectionDuplicates);
152
8992
  smtStatisticsRegistry()->unregisterStat(&d_enqueuesVarOrderModeDuplicates);
153
8992
}
154
155
8995
ErrorSet::ErrorSet(ArithVariables& vars,
156
                   TableauSizes tabSizes,
157
8995
                   BoundCountingLookup lookups)
158
    : d_variables(vars),
159
      d_errInfo(),
160
      d_selectionRule(options::ErrorSelectionRule::VAR_ORDER),
161
17990
      d_focus(ComparatorPivotRule(this, d_selectionRule)),
162
      d_outOfFocus(),
163
      d_signals(),
164
      d_tableauSizes(tabSizes),
165
26985
      d_boundLookup(lookups)
166
8995
{}
167
168
2477681
options::ErrorSelectionRule ErrorSet::getSelectionRule() const
169
{
170
2477681
  return d_selectionRule;
171
}
172
173
167605
void ErrorSet::recomputeAmount(ErrorInformation& ei,
174
                               options::ErrorSelectionRule rule)
175
{
176
167605
  switch(rule){
177
155172
    case options::ErrorSelectionRule::MINIMUM_AMOUNT:
178
    case options::ErrorSelectionRule::MAXIMUM_AMOUNT:
179
155172
      ei.setAmount(computeDiff(ei.getVariable()));
180
155172
      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
167605
}
189
190
919286
void ErrorSet::setSelectionRule(options::ErrorSelectionRule rule)
191
{
192
919286
  if(rule != getSelectionRule()){
193
324522
    FocusSet into(ComparatorPivotRule(this, rule));
194
162261
    FocusSet::const_iterator iter = d_focus.begin();
195
162261
    FocusSet::const_iterator i_end = d_focus.end();
196
497471
    for(; iter != i_end; ++iter){
197
167605
      ArithVar v = *iter;
198
167605
      ErrorInformation& ei = d_errInfo.get(v);
199
167605
      if(ei.inFocus()){
200
167605
        recomputeAmount(ei, rule);
201
167605
        FocusSetHandle handle = into.push(v);
202
167605
        ei.setHandle(handle);
203
      }
204
    }
205
162261
    d_focus.swap(into);
206
162261
    d_selectionRule = rule;
207
  }
208
919286
  Assert(getSelectionRule() == rule);
209
919286
}
210
211
171256
ComparatorPivotRule::ComparatorPivotRule(const ErrorSet* es,
212
171256
                                         options::ErrorSelectionRule r)
213
171256
    : d_errorSet(es), d_rule(r)
214
171256
{}
215
216
1062190
bool ComparatorPivotRule::operator()(ArithVar v, ArithVar u) const {
217
1062190
  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
502565
    case options::ErrorSelectionRule::MINIMUM_AMOUNT:
232
    {
233
502565
      const DeltaRational& vamt = d_errorSet->getAmount(v);
234
502565
      const DeltaRational& uamt = d_errorSet->getAmount(u);
235
502565
      int cmp = vamt.cmp(uamt);
236
502565
      if(cmp == 0){
237
197907
        return v > u;
238
      }else{
239
304658
        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
237319
void ErrorSet::update(ErrorInformation& ei){
258
237319
  if(ei.inFocus()){
259
260
237319
    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
173983
      case options::ErrorSelectionRule::VAR_ORDER:
271
        // do nothing
272
173983
        break;
273
    }
274
  }
275
237319
}
276
277
/** A variable becomes satisfied. */
278
299141
void ErrorSet::transitionVariableOutOfError(ArithVar v) {
279
299141
  Assert(!inconsistent(v));
280
299141
  ErrorInformation& ei = d_errInfo.get(v);
281
299141
  Assert(ei.debugInitialized());
282
299141
  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
299141
  if(ei.inFocus()){
293
299141
    d_focus.erase(ei.getHandle());
294
299141
    ei.setInFocus(false);
295
  }
296
299141
  d_errInfo.remove(v);
297
299141
}
298
299
300
401790
void ErrorSet::transitionVariableIntoError(ArithVar v) {
301
401790
  Assert(inconsistent(v));
302
401790
  bool vilb = d_variables.cmpAssignmentLowerBound(v) < 0;
303
401790
  int sgn = vilb ? 1 : -1;
304
803580
  ConstraintP c = vilb ?
305
803580
    d_variables.getLowerBoundConstraint(v) : d_variables.getUpperBoundConstraint(v);
306
401790
  d_errInfo.set(v, ErrorInformation(v, c, sgn));
307
401790
  ErrorInformation& ei = d_errInfo.get(v);
308
309
401790
  switch(getSelectionRule()){
310
77213
    case options::ErrorSelectionRule::MINIMUM_AMOUNT:
311
    case options::ErrorSelectionRule::MAXIMUM_AMOUNT:
312
77213
      ei.setAmount(computeDiff(v));
313
77213
      break;
314
    case options::ErrorSelectionRule::SUM_METRIC:
315
      ei.setMetric(sumMetric(ei.getVariable()));
316
      break;
317
324577
    case options::ErrorSelectionRule::VAR_ORDER:
318
      // do nothing
319
324577
      break;
320
  }
321
401790
  ei.setInFocus(true);
322
401790
  FocusSetHandle handle = d_focus.push(v);
323
401790
  ei.setHandle(handle);
324
401790
}
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
7482538
int ErrorSet::popSignal() {
371
7482538
  ArithVar back = d_signals.back();
372
7482538
  d_signals.pop_back();
373
374
7482538
  if(inError(back)){
375
536460
    ErrorInformation& ei = d_errInfo.get(back);
376
536460
    int prevSgn = ei.sgn();
377
536460
    int focusSgn = ei.focusSgn();
378
536460
    bool vilb = d_variables.cmpAssignmentLowerBound(back) < 0;
379
536460
    bool viub = d_variables.cmpAssignmentUpperBound(back) > 0;
380
536460
    if(vilb || viub){
381
237319
      Assert(!vilb || !viub);
382
237319
      int currSgn = vilb ? 1 : -1;
383
237319
      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
237319
      update(ei);
389
    }else{
390
299141
      transitionVariableOutOfError(back);
391
    }
392
536460
    return focusSgn;
393
6946078
  }else if(inconsistent(back)){
394
401790
    transitionVariableIntoError(back);
395
  }
396
6946078
  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
794577
void ErrorSet::reduceToSignals(){
417
896094
  for(error_iterator ei=errorBegin(), ei_end=errorEnd(); ei != ei_end; ++ei){
418
101517
    ArithVar curr = *ei;
419
101517
    signalVariable(curr);
420
  }
421
422
794577
  d_errInfo.purge();
423
794577
  d_focus.clear();
424
794577
  d_outOfFocus.clear();
425
794577
}
426
427
295721
DeltaRational ErrorSet::computeDiff(ArithVar v) const{
428
295721
  Assert(inconsistent(v));
429
295721
  const DeltaRational& beta = d_variables.getAssignment(v);
430
295721
  DeltaRational diff = d_variables.cmpAssignmentLowerBound(v) < 0 ?
431
151619
    d_variables.getLowerBound(v) - beta:
432
447340
    beta - d_variables.getUpperBound(v);
433
434
295721
  Assert(diff.sgn() > 0);
435
295721
  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
26676
}/* CVC4 namespace */