GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/soi_simplex.cpp Lines: 35 555 6.3 %
Date: 2021-03-22 Branches: 58 2476 2.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file soi_simplex.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Tim King, Aina Niemetz, 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
#include "theory/arith/soi_simplex.h"
18
19
#include <algorithm>
20
21
#include "base/output.h"
22
#include "options/arith_options.h"
23
#include "smt/smt_statistics_registry.h"
24
#include "theory/arith/constraint.h"
25
#include "theory/arith/error_set.h"
26
#include "theory/arith/tableau.h"
27
#include "util/statistics_registry.h"
28
29
using namespace std;
30
31
namespace CVC4 {
32
namespace theory {
33
namespace arith {
34
35
36
8995
SumOfInfeasibilitiesSPD::SumOfInfeasibilitiesSPD(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc)
37
  : SimplexDecisionProcedure(linEq, errors, conflictChannel, tvmalloc)
38
  , d_soiVar(ARITHVAR_SENTINEL)
39
  , d_pivotBudget(0)
40
  , d_prevWitnessImprovement(AntiProductive)
41
  , d_witnessImprovementInARow(0)
42
  , d_sgnDisagreements()
43
8995
  , d_statistics(d_pivots)
44
8995
{ }
45
46
8995
SumOfInfeasibilitiesSPD::Statistics::Statistics(uint32_t& pivots):
47
  d_initialSignalsTime("theory::arith::SOI::initialProcessTime"),
48
  d_initialConflicts("theory::arith::SOI::UpdateConflicts", 0),
49
  d_soiFoundUnsat("theory::arith::SOI::FoundUnsat", 0),
50
  d_soiFoundSat("theory::arith::SOI::FoundSat", 0),
51
  d_soiMissed("theory::arith::SOI::Missed", 0),
52
  d_soiConflicts("theory::arith::SOI::ConfMin::num", 0),
53
  d_hasToBeMinimal("theory::arith::SOI::HasToBeMin", 0),
54
  d_maybeNotMinimal("theory::arith::SOI::MaybeNotMin", 0),
55
  d_soiTimer("theory::arith::SOI::Time"),
56
  d_soiFocusConstructionTimer("theory::arith::SOI::Construction"),
57
  d_soiConflictMinimization("theory::arith::SOI::Conflict::Minimization"),
58
  d_selectUpdateForSOI("theory::arith::SOI::selectSOI"),
59
8995
  d_finalCheckPivotCounter("theory::arith::SOI::lastPivots", pivots)
60
{
61
8995
  smtStatisticsRegistry()->registerStat(&d_initialSignalsTime);
62
8995
  smtStatisticsRegistry()->registerStat(&d_initialConflicts);
63
64
8995
  smtStatisticsRegistry()->registerStat(&d_soiFoundUnsat);
65
8995
  smtStatisticsRegistry()->registerStat(&d_soiFoundSat);
66
8995
  smtStatisticsRegistry()->registerStat(&d_soiMissed);
67
68
8995
  smtStatisticsRegistry()->registerStat(&d_soiConflicts);
69
8995
  smtStatisticsRegistry()->registerStat(&d_hasToBeMinimal);
70
8995
  smtStatisticsRegistry()->registerStat(&d_maybeNotMinimal);
71
72
8995
  smtStatisticsRegistry()->registerStat(&d_soiTimer);
73
8995
  smtStatisticsRegistry()->registerStat(&d_soiFocusConstructionTimer);
74
75
8995
  smtStatisticsRegistry()->registerStat(&d_soiConflictMinimization);
76
77
8995
  smtStatisticsRegistry()->registerStat(&d_selectUpdateForSOI);
78
79
8995
  smtStatisticsRegistry()->registerStat(&d_finalCheckPivotCounter);
80
8995
}
81
82
17984
SumOfInfeasibilitiesSPD::Statistics::~Statistics(){
83
8992
  smtStatisticsRegistry()->unregisterStat(&d_initialSignalsTime);
84
8992
  smtStatisticsRegistry()->unregisterStat(&d_initialConflicts);
85
86
8992
  smtStatisticsRegistry()->unregisterStat(&d_soiFoundUnsat);
87
8992
  smtStatisticsRegistry()->unregisterStat(&d_soiFoundSat);
88
8992
  smtStatisticsRegistry()->unregisterStat(&d_soiMissed);
89
90
8992
  smtStatisticsRegistry()->unregisterStat(&d_soiConflicts);
91
8992
  smtStatisticsRegistry()->unregisterStat(&d_hasToBeMinimal);
92
8992
  smtStatisticsRegistry()->unregisterStat(&d_maybeNotMinimal);
93
94
8992
  smtStatisticsRegistry()->unregisterStat(&d_soiTimer);
95
8992
  smtStatisticsRegistry()->unregisterStat(&d_soiFocusConstructionTimer);
96
97
8992
  smtStatisticsRegistry()->unregisterStat(&d_soiConflictMinimization);
98
99
8992
  smtStatisticsRegistry()->unregisterStat(&d_selectUpdateForSOI);
100
8992
  smtStatisticsRegistry()->unregisterStat(&d_finalCheckPivotCounter);
101
8992
}
102
103
Result::Sat SumOfInfeasibilitiesSPD::findModel(bool exactResult){
104
  Assert(d_conflictVariables.empty());
105
  Assert(d_sgnDisagreements.empty());
106
107
  d_pivots = 0;
108
  static thread_local unsigned int instance = 0;
109
  instance = instance + 1;
110
  static const bool verbose = false;
111
112
  if(d_errorSet.errorEmpty() && !d_errorSet.moreSignals()){
113
    Debug("soi::findModel") << "soiFindModel("<< instance <<") trivial" << endl;
114
    Assert(d_conflictVariables.empty());
115
    return Result::SAT;
116
  }
117
118
  // We need to reduce this because of
119
  d_errorSet.reduceToSignals();
120
121
  // We must start tracking NOW
122
  d_errorSet.setSelectionRule(options::ErrorSelectionRule::SUM_METRIC);
123
124
  if(initialProcessSignals()){
125
    d_conflictVariables.purge();
126
    if (verbose)
127
    {
128
      CVC4Message() << "fcFindModel(" << instance << ") early conflict" << endl;
129
    }
130
    Debug("soi::findModel") << "fcFindModel("<< instance <<") early conflict" << endl;
131
    Assert(d_conflictVariables.empty());
132
    return Result::UNSAT;
133
  }else if(d_errorSet.errorEmpty()){
134
    Debug("soi::findModel") << "fcFindModel("<< instance <<") fixed itself" << endl;
135
    Assert(!d_errorSet.moreSignals());
136
    Assert(d_conflictVariables.empty());
137
    return Result::SAT;
138
  }
139
140
  Debug("soi::findModel") << "fcFindModel(" << instance <<") start non-trivial" << endl;
141
142
  exactResult |= options::arithStandardCheckVarOrderPivots() < 0;
143
144
  d_prevWitnessImprovement = HeuristicDegenerate;
145
  d_witnessImprovementInARow = 0;
146
147
  Result::Sat result = Result::SAT_UNKNOWN;
148
149
  if(result == Result::SAT_UNKNOWN){
150
    if(exactResult){
151
      d_pivotBudget = -1;
152
    }else{
153
      d_pivotBudget = options::arithStandardCheckVarOrderPivots();
154
    }
155
156
    result = sumOfInfeasibilities();
157
158
    if(result ==  Result::UNSAT){
159
      ++(d_statistics.d_soiFoundUnsat);
160
      if (verbose)
161
      {
162
        CVC4Message() << "fc found unsat";
163
      }
164
    }else if(d_errorSet.errorEmpty()){
165
      ++(d_statistics.d_soiFoundSat);
166
      if (verbose)
167
      {
168
        CVC4Message() << "fc found model";
169
      }
170
    }else{
171
      ++(d_statistics.d_soiMissed);
172
      if (verbose)
173
      {
174
        CVC4Message() << "fc missed";
175
      }
176
    }
177
  }
178
  if (verbose)
179
  {
180
    CVC4Message() << "(" << instance << ") pivots " << d_pivots << endl;
181
  }
182
183
  Assert(!d_errorSet.moreSignals());
184
  if(result == Result::SAT_UNKNOWN && d_errorSet.errorEmpty()){
185
    result = Result::SAT;
186
  }
187
188
  // ensure that the conflict variable is still in the queue.
189
  d_conflictVariables.purge();
190
191
  Debug("soi::findModel") << "end findModel() " << instance << " " << result <<  endl;
192
193
  Assert(d_conflictVariables.empty());
194
  return result;
195
}
196
197
198
void SumOfInfeasibilitiesSPD::logPivot(WitnessImprovement w){
199
  if(d_pivotBudget > 0) {
200
    --d_pivotBudget;
201
  }
202
  Assert(w != AntiProductive);
203
204
  if(w == d_prevWitnessImprovement){
205
    ++d_witnessImprovementInARow;
206
    if(d_witnessImprovementInARow == 0){
207
      --d_witnessImprovementInARow;
208
    }
209
  }else{
210
    if(w != BlandsDegenerate){
211
      d_witnessImprovementInARow = 1;
212
    }
213
    d_prevWitnessImprovement = w;
214
  }
215
  if(strongImprovement(w)){
216
    d_leavingCountSinceImprovement.purge();
217
  }
218
219
  Debug("logPivot") << "logPivot " << d_prevWitnessImprovement << " "  << d_witnessImprovementInARow << endl;
220
}
221
222
uint32_t SumOfInfeasibilitiesSPD::degeneratePivotsInARow() const {
223
  switch(d_prevWitnessImprovement){
224
  case ConflictFound:
225
  case ErrorDropped:
226
  case FocusImproved:
227
    return 0;
228
  case HeuristicDegenerate:
229
  case BlandsDegenerate:
230
    return d_witnessImprovementInARow;
231
  // Degenerate is unreachable for its own reasons
232
  case Degenerate:
233
  case FocusShrank:
234
  case AntiProductive:
235
    Unreachable();
236
    return -1;
237
  }
238
  Unreachable();
239
}
240
241
void SumOfInfeasibilitiesSPD::adjustFocusAndError(const UpdateInfo& up, const AVIntPairVec& focusChanges){
242
  uint32_t newErrorSize = d_errorSet.errorSize();
243
  adjustInfeasFunc(d_statistics.d_soiFocusConstructionTimer, d_soiVar, focusChanges);
244
  d_errorSize = newErrorSize;
245
}
246
247
248
UpdateInfo SumOfInfeasibilitiesSPD::selectUpdate(LinearEqualityModule::UpdatePreferenceFunction upf, LinearEqualityModule::VarPreferenceFunction bpf) {
249
  UpdateInfo selected;
250
251
  static int instance = 0 ;
252
  ++instance;
253
254
  Debug("soi::selectPrimalUpdate")
255
    << "selectPrimalUpdate " << instance << endl
256
    << d_soiVar << " " << d_tableau.basicRowLength(d_soiVar)
257
    << " " << d_linEq.debugBasicAtBoundCount(d_soiVar) << endl;
258
259
  typedef std::vector<Cand> CandVector;
260
  CandVector candidates;
261
262
  for(Tableau::RowIterator ri = d_tableau.basicRowIterator(d_soiVar); !ri.atEnd(); ++ri){
263
    const Tableau::Entry& e = *ri;
264
    ArithVar curr = e.getColVar();
265
    if(curr == d_soiVar){ continue; }
266
267
    int sgn = e.getCoefficient().sgn();
268
    bool candidate =
269
      (sgn > 0 && d_variables.cmpAssignmentUpperBound(curr) < 0) ||
270
      (sgn < 0 && d_variables.cmpAssignmentLowerBound(curr) > 0);
271
272
    Debug("soi::selectPrimalUpdate")
273
      << "storing " << d_soiVar
274
      << " " << curr
275
      << " " << candidate
276
      << " " << e.getCoefficient()
277
      << " " << sgn << endl;
278
279
    if(candidate) {
280
      candidates.push_back(Cand(curr, 0, sgn, &e.getCoefficient()));
281
    }
282
  }
283
284
  CompPenaltyColLength colCmp(&d_linEq);
285
  CandVector::iterator i = candidates.begin();
286
  CandVector::iterator end = candidates.end();
287
  std::make_heap(i, end, colCmp);
288
289
  // For the first 3 pivots take the best
290
  // After that, once an improvement is found on look at a
291
  // small number of pivots after finding an improvement
292
  // the longer the search to more willing we are to look at more candidates
293
  int maxCandidatesAfterImprove =
294
    (d_pivots <= 2) ?  std::numeric_limits<int>::max() : d_pivots/5;
295
296
  int candidatesAfterFocusImprove = 0;
297
  while(i != end && candidatesAfterFocusImprove <= maxCandidatesAfterImprove){
298
    std::pop_heap(i, end, colCmp);
299
    --end;
300
    Cand& cand = (*end);
301
    ArithVar curr = cand.d_nb;
302
    const Rational& coeff = *cand.d_coeff;
303
304
    LinearEqualityModule::UpdatePreferenceFunction leavingPrefFunc = selectLeavingFunction(curr);
305
    UpdateInfo currProposal = d_linEq.speculativeUpdate(curr, coeff, leavingPrefFunc);
306
307
    Debug("soi::selectPrimalUpdate")
308
      << "selected " << selected << endl
309
      << "currProp " << currProposal << endl
310
      << "coeff " << coeff << endl;
311
312
    Assert(!currProposal.uninitialized());
313
314
    if(candidatesAfterFocusImprove > 0){
315
      candidatesAfterFocusImprove++;
316
    }
317
318
    if(selected.uninitialized() || (d_linEq.*upf)(selected, currProposal)){
319
      selected = currProposal;
320
      WitnessImprovement w = selected.getWitness(false);
321
      Debug("soi::selectPrimalUpdate") << "selected " << w << endl;
322
      //setPenalty(curr, w);
323
      if(improvement(w)){
324
        bool exitEarly;
325
        switch(w){
326
        case ConflictFound: exitEarly = true; break;
327
        case FocusImproved:
328
          candidatesAfterFocusImprove = 1;
329
          exitEarly = false;
330
          break;
331
        default:
332
          exitEarly = false; break;
333
        }
334
        if(exitEarly){ break; }
335
      }
336
    }else{
337
      Debug("soi::selectPrimalUpdate") << "dropped "<< endl;
338
    }
339
340
  }
341
  return selected;
342
}
343
344
bool debugCheckWitness(const UpdateInfo& inf, WitnessImprovement w, bool useBlands){
345
  if(inf.getWitness(useBlands) == w){
346
    switch(w){
347
    case ConflictFound: return inf.foundConflict();
348
    case ErrorDropped: return inf.errorsChange() < 0;
349
    case FocusImproved: return inf.focusDirection() > 0;
350
    case FocusShrank: return false; // This is not a valid output
351
    case Degenerate: return false; // This is not a valid output
352
    case BlandsDegenerate: return useBlands;
353
    case HeuristicDegenerate: return !useBlands;
354
    case AntiProductive: return false;
355
    }
356
  }
357
  return false;
358
}
359
360
361
void SumOfInfeasibilitiesSPD::debugPrintSignal(ArithVar updated) const{
362
  Debug("updateAndSignal") << "updated basic " << updated;
363
  Debug("updateAndSignal") << " length " << d_tableau.basicRowLength(updated);
364
  Debug("updateAndSignal") << " consistent " << d_variables.assignmentIsConsistent(updated);
365
  int dir = !d_variables.assignmentIsConsistent(updated) ?
366
    d_errorSet.getSgn(updated) : 0;
367
  Debug("updateAndSignal") << " dir " << dir;
368
  Debug("updateAndSignal") << " debugBasicAtBoundCount " << d_linEq.debugBasicAtBoundCount(updated) << endl;
369
}
370
371
372
void SumOfInfeasibilitiesSPD::updateAndSignal(const UpdateInfo& selected, WitnessImprovement w){
373
  ArithVar nonbasic = selected.nonbasic();
374
375
  static bool verbose = false;
376
377
  Debug("updateAndSignal") << "updateAndSignal " << selected << endl;
378
379
  stringstream ss;
380
  if(verbose){
381
    d_errorSet.debugPrint(ss);
382
    if(selected.describesPivot()){
383
      ArithVar leaving = selected.leaving();
384
      ss << "leaving " << leaving
385
         << " " << d_tableau.basicRowLength(leaving)
386
         << " " << d_linEq.debugBasicAtBoundCount(leaving)
387
         << endl;
388
    }
389
    if(degenerate(w) && selected.describesPivot()){
390
      ArithVar leaving = selected.leaving();
391
      CVC4Message() << "degenerate " << leaving << ", atBounds "
392
                    << d_linEq.basicsAtBounds(selected) << ", len "
393
                    << d_tableau.basicRowLength(leaving) << ", bc "
394
                    << d_linEq.debugBasicAtBoundCount(leaving) << endl;
395
    }
396
  }
397
398
  if(selected.describesPivot()){
399
    ConstraintP limiting = selected.limiting();
400
    ArithVar basic = limiting->getVariable();
401
    Assert(d_linEq.basicIsTracked(basic));
402
    d_linEq.pivotAndUpdate(basic, nonbasic, limiting->getValue());
403
  }else{
404
    Assert(!selected.unbounded() || selected.errorsChange() < 0);
405
406
    DeltaRational newAssignment =
407
      d_variables.getAssignment(nonbasic) + selected.nonbasicDelta();
408
409
    d_linEq.updateTracked(nonbasic, newAssignment);
410
  }
411
  d_pivots++;
412
413
  increaseLeavingCount(nonbasic);
414
415
  vector< pair<ArithVar, int> > focusChanges;
416
  while(d_errorSet.moreSignals()){
417
    ArithVar updated = d_errorSet.topSignal();
418
    int prevFocusSgn = d_errorSet.popSignal();
419
420
    if(d_tableau.isBasic(updated)){
421
      Assert(!d_variables.assignmentIsConsistent(updated)
422
             == d_errorSet.inError(updated));
423
      if(Debug.isOn("updateAndSignal")){debugPrintSignal(updated);}
424
      if(!d_variables.assignmentIsConsistent(updated)){
425
        if(checkBasicForConflict(updated)){
426
          reportConflict(updated);
427
          //Assert(debugUpdatedBasic(selected, updated));
428
        }
429
      }
430
    }else{
431
      Debug("updateAndSignal") << "updated nonbasic " << updated << endl;
432
    }
433
    int currFocusSgn = d_errorSet.focusSgn(updated);
434
    if(currFocusSgn != prevFocusSgn){
435
      int change = currFocusSgn - prevFocusSgn;
436
      focusChanges.push_back(make_pair(updated, change));
437
    }
438
  }
439
440
  if (verbose)
441
  {
442
    CVC4Message() << "conflict variable " << selected << endl;
443
    CVC4Message() << ss.str();
444
  }
445
  if(Debug.isOn("error")){ d_errorSet.debugPrint(Debug("error")); }
446
447
  //Assert(debugSelectedErrorDropped(selected, d_errorSize, d_errorSet.errorSize()));
448
449
  adjustFocusAndError(selected, focusChanges);
450
}
451
452
void SumOfInfeasibilitiesSPD::qeAddRange(uint32_t begin, uint32_t end){
453
  Assert(!d_qeInSoi.empty());
454
  for(uint32_t i = begin; i != end; ++i){
455
    ArithVar v = d_qeConflict[i];
456
    addToInfeasFunc(d_statistics.d_soiConflictMinimization, d_soiVar, v);
457
    d_qeInSoi.add(v);
458
  }
459
}
460
461
void SumOfInfeasibilitiesSPD::qeRemoveRange(uint32_t begin, uint32_t end){
462
  for(uint32_t i = begin; i != end; ++i){
463
    ArithVar v = d_qeConflict[i];
464
    removeFromInfeasFunc(d_statistics.d_soiConflictMinimization, d_soiVar, v);
465
    d_qeInSoi.remove(v);
466
  }
467
  Assert(!d_qeInSoi.empty());
468
}
469
470
void SumOfInfeasibilitiesSPD::qeSwapRange(uint32_t N, uint32_t r, uint32_t s){
471
  for(uint32_t i = 0; i < N; ++i){
472
    std::swap(d_qeConflict[r+i], d_qeConflict[s+i]);
473
  }
474
}
475
476
/**
477
 * Region notation:
478
 * A region is either
479
 *  - A single element X@i with the name X at the position i
480
 *  - A sequence of indices X@[i,j) with the name X and the elements between i [inclusive] and j exclusive
481
 *  - A concatenation of regions R1 and R2, R1;R2
482
 *
483
 * Given the fixed assumptions C @ [0,cEnd) and a set of candidate minimizations U@[cEnd, uEnd)
484
 * s.t. C \cup U is known to be in conflict ([0,uEnd) has a conflict), find a minimal
485
 * subset of U, Delta, s.t. C \cup Delta is in conflict.
486
 *
487
 * Pre:
488
 *  [0, uEnd) is a set and is in conflict.
489
 *    uEnd <= assumptions.size()
490
 *  [0, cEnd) is in d_inSoi.
491
 *
492
 * Invariants: [0,cEnd) is never modified
493
 *
494
 * Post:
495
 *  [0, cEnd); [cEnd, deltaEnd) is in conflict
496
 *  [0, deltaEnd) is a set
497
 *  [0, deltaEnd) is in d_inSoi
498
 */
499
uint32_t SumOfInfeasibilitiesSPD::quickExplainRec(uint32_t cEnd, uint32_t uEnd){
500
  Assert(cEnd <= uEnd);
501
  Assert(d_qeInUAndNotInSoi.empty());
502
  Assert(d_qeGreedyOrder.empty());
503
504
  const Tableau::Entry* spoiler = NULL;
505
506
  if(d_soiVar != ARITHVAR_SENTINEL && d_linEq.selectSlackEntry(d_soiVar, false) == NULL){
507
    // already in conflict
508
    return cEnd;
509
  }
510
511
  Assert(cEnd < uEnd);
512
513
  // Phase 1 : Construct the conflict greedily
514
515
  for(uint32_t i = cEnd; i < uEnd; ++i){
516
    d_qeInUAndNotInSoi.add(d_qeConflict[i]);
517
  }
518
  if(d_soiVar == ARITHVAR_SENTINEL){ // special case for d_soiVar being empty
519
    ArithVar first = d_qeConflict[cEnd];
520
    d_soiVar = constructInfeasiblityFunction(d_statistics.d_soiConflictMinimization, first);
521
    d_qeInSoi.add(first);
522
    d_qeInUAndNotInSoi.remove(first);
523
    d_qeGreedyOrder.push_back(first);
524
  }
525
  while((spoiler = d_linEq.selectSlackEntry(d_soiVar, false)) != NULL){
526
    Assert(!d_qeInUAndNotInSoi.empty());
527
528
    ArithVar nb = spoiler->getColVar();
529
    int oppositeSgn = -(spoiler->getCoefficient().sgn());
530
    Assert(oppositeSgn != 0);
531
532
    ArithVar basicWithOp = find_basic_in_sgns(d_qeSgns, nb, oppositeSgn, d_qeInUAndNotInSoi, true);
533
    Assert(basicWithOp != ARITHVAR_SENTINEL);
534
535
    addToInfeasFunc(d_statistics.d_soiConflictMinimization, d_soiVar, basicWithOp);
536
    d_qeInSoi.add(basicWithOp);
537
    d_qeInUAndNotInSoi.remove(basicWithOp);
538
    d_qeGreedyOrder.push_back(basicWithOp);
539
  }
540
  Assert(spoiler == NULL);
541
542
  // Compact the set u
543
  uint32_t newEnd = cEnd + d_qeGreedyOrder.size();
544
  std::copy(d_qeGreedyOrder.begin(), d_qeGreedyOrder.end(), d_qeConflict.begin()+cEnd);
545
546
  d_qeInUAndNotInSoi.purge();
547
  d_qeGreedyOrder.clear();
548
549
   // Phase 2 : Recursively determine the minimal set of rows
550
551
  uint32_t xPos = cEnd;
552
  std::swap(d_qeGreedyOrder[xPos], d_qeGreedyOrder[newEnd - 1]);
553
  uint32_t uBegin = xPos + 1;
554
  uint32_t split = (newEnd - uBegin)/2 + uBegin;
555
556
  //assumptions : C @ [0, cEnd); X @ xPos; U1 @ [u1Begin, split); U2 @ [split, newEnd)
557
  // [0, newEnd) == d_inSoi
558
559
  uint32_t compactU2;
560
  if(split == newEnd){ // U2 is empty
561
    compactU2 = newEnd;
562
  }else{
563
    // Remove U2 from Soi
564
    qeRemoveRange(split, newEnd);
565
    // [0, split) == d_inSoi
566
567
    // pre assumptions: C + X + U1 @ [0,split); U2 [split, newEnd)
568
    compactU2 = quickExplainRec(split, newEnd);
569
    // post:
570
    //  assumptions: C + X + U1 @ [0, split); delta2 @ [split - compactU2)
571
    //  d_inSoi = [0, compactU2)
572
  }
573
  uint32_t deltaSize = compactU2 - split;
574
  qeSwapRange(deltaSize, uBegin, split);
575
  uint32_t d2End = uBegin+deltaSize;
576
  // assumptions : C @ [0, cEnd); X @ xPos; delta2 @ [uBegin, d2End); U1 @ [d2End, compactU2)
577
  //  d_inSoi == [0, compactU2)
578
579
  uint32_t d1End;
580
  if(d2End == compactU2){ // U1 is empty
581
    d1End = d2End;
582
  }else{
583
    qeRemoveRange(d2End, compactU2);
584
585
    //pre assumptions : C + X + delta2 @ [0, d2End); U1 @ [d2End, compactU2);
586
    d1End = quickExplainRec(d2End, compactU2);
587
    //post:
588
    // assumptions : C + X + delta2 @ [0, d2End); delta1 @ [d2End, d1End);
589
    // d_inSoi = [0, d1End)
590
  }
591
  //After both:
592
  // d_inSoi == [0, d1End), C @ [0, cEnd); X + delta2 + delta 1 @ [xPos, d1End);
593
594
  Assert(d_qeInUAndNotInSoi.empty());
595
  Assert(d_qeGreedyOrder.empty());
596
  return d1End;
597
}
598
599
void SumOfInfeasibilitiesSPD::quickExplain(){
600
  Assert(d_qeInSoi.empty());
601
  Assert(d_qeInUAndNotInSoi.empty());
602
  Assert(d_qeGreedyOrder.empty());
603
  Assert(d_soiVar == ARITHVAR_SENTINEL);
604
  Assert(d_qeSgns.empty());
605
606
  d_qeConflict.clear();
607
  d_errorSet.pushFocusInto(d_qeConflict);
608
609
  //cout <<  d_qeConflict.size() << " ";
610
  uint32_t size = d_qeConflict.size();
611
612
  if(size > 2){
613
    for(ErrorSet::focus_iterator iter = d_errorSet.focusBegin(), end = d_errorSet.focusEnd(); iter != end; ++iter){
614
      ArithVar e = *iter;
615
      addRowSgns(d_qeSgns, e, d_errorSet.getSgn(e));
616
    }
617
    uint32_t end = quickExplainRec(0u, size);
618
    Assert(end <= d_qeConflict.size());
619
    Assert(d_soiVar != ARITHVAR_SENTINEL);
620
    Assert(!d_qeInSoi.empty());
621
622
    d_qeConflict.resize(end);
623
    tearDownInfeasiblityFunction(d_statistics.d_soiConflictMinimization, d_soiVar);
624
    d_soiVar = ARITHVAR_SENTINEL;
625
    d_qeInSoi.purge();
626
    d_qeSgns.clear();
627
  }
628
629
  //cout << d_qeConflict.size() << endl;
630
631
  Assert(d_qeInSoi.empty());
632
  Assert(d_qeInUAndNotInSoi.empty());
633
  Assert(d_qeGreedyOrder.empty());
634
  Assert(d_soiVar == ARITHVAR_SENTINEL);
635
  Assert(d_qeSgns.empty());
636
}
637
638
unsigned SumOfInfeasibilitiesSPD::trySet(const ArithVarVec& set){
639
  Assert(d_soiVar == ARITHVAR_SENTINEL);
640
  bool success = false;
641
  if(set.size() >= 2){
642
    d_soiVar = constructInfeasiblityFunction(d_statistics.d_soiConflictMinimization, set);
643
    success = d_linEq.selectSlackEntry(d_soiVar, false) == NULL;
644
645
    tearDownInfeasiblityFunction(d_statistics.d_soiConflictMinimization, d_soiVar);
646
    d_soiVar = ARITHVAR_SENTINEL;
647
  }
648
  return success ? set.size() : std::numeric_limits<int>::max();
649
}
650
651
std::vector< ArithVarVec > SumOfInfeasibilitiesSPD::greedyConflictSubsets(){
652
  Debug("arith::greedyConflictSubsets") << "greedyConflictSubsets start" << endl;
653
654
  std::vector< ArithVarVec > subsets;
655
  Assert(d_soiVar == ARITHVAR_SENTINEL);
656
657
  if(d_errorSize <= 2){
658
    ArithVarVec inError;
659
    d_errorSet.pushFocusInto(inError);
660
661
    Assert(debugIsASet(inError));
662
    subsets.push_back(inError);
663
    return subsets;
664
  }
665
  Assert(d_errorSize > 2);
666
667
  //sgns_table< <nonbasic,sgn>, [basics] >;
668
  // Phase 0: Construct the sgns table
669
  sgn_table sgns;
670
  DenseSet hasParticipated; //Has participated in a conflict
671
  for(ErrorSet::focus_iterator iter = d_errorSet.focusBegin(), end = d_errorSet.focusEnd(); iter != end; ++iter){
672
    ArithVar e = *iter;
673
    addRowSgns(sgns, e, d_errorSet.getSgn(e));
674
675
    Debug("arith::greedyConflictSubsets") << "basic error var: " << e << endl;
676
    if(Debug.isOn("arith::greedyConflictSubsets")){
677
      d_tableau.debugPrintIsBasic(e);
678
      d_tableau.printBasicRow(e, Debug("arith::greedyConflictSubsets"));
679
    }
680
  }
681
682
  // Phase 1: Try to find at least 1 pair for every element
683
  ArithVarVec tmp;
684
  tmp.push_back(0);
685
  tmp.push_back(0);
686
  for(ErrorSet::focus_iterator iter = d_errorSet.focusBegin(), end = d_errorSet.focusEnd(); iter != end; ++iter){
687
    ArithVar e = *iter;
688
    tmp[0] = e;
689
690
    int errSgn = d_errorSet.getSgn(e);
691
    bool decreasing = errSgn < 0;
692
    const Tableau::Entry* spoiler = d_linEq.selectSlackEntry(e, decreasing);
693
    Assert(spoiler != NULL);
694
    ArithVar nb = spoiler->getColVar();
695
    int oppositeSgn = -(errSgn * (spoiler->getCoefficient().sgn()));
696
697
    sgn_table::const_iterator opposites = find_sgns(sgns, nb, oppositeSgn);
698
    Assert(opposites != sgns.end());
699
700
    const ArithVarVec& choices = (*opposites).second;
701
    for(ArithVarVec::const_iterator j = choices.begin(), jend = choices.end(); j != jend; ++j){
702
      ArithVar b = *j;
703
      if(b < e){ continue; }
704
      tmp[0] = e;
705
      tmp[1] = b;
706
      if(trySet(tmp) == 2){
707
        Debug("arith::greedyConflictSubsets")  << "found a pair " << b << " " << e << endl;
708
        hasParticipated.softAdd(b);
709
        hasParticipated.softAdd(e);
710
        Assert(debugIsASet(tmp));
711
        subsets.push_back(tmp);
712
        ++(d_statistics.d_soiConflicts);
713
        ++(d_statistics.d_hasToBeMinimal);
714
      }
715
    }
716
  }
717
718
719
  // Phase 2: If there is a variable that has not participated attempt to start a conflict
720
  ArithVarVec possibleStarts; //List of elements that can be tried for starts.
721
  d_errorSet.pushFocusInto(possibleStarts);
722
  while(!possibleStarts.empty()){
723
    Assert(d_soiVar == ARITHVAR_SENTINEL);
724
725
    ArithVar v = possibleStarts.back();
726
    possibleStarts.pop_back();
727
    if(hasParticipated.isMember(v)){ continue; }
728
729
    hasParticipated.add(v);
730
731
    Assert(d_soiVar == ARITHVAR_SENTINEL);
732
    //d_soiVar's row =  \sumofinfeasibilites underConstruction
733
    ArithVarVec underConstruction;
734
    underConstruction.push_back(v);
735
    d_soiVar = constructInfeasiblityFunction(d_statistics.d_soiConflictMinimization, v);
736
737
    Debug("arith::greedyConflictSubsets") << "trying " << v << endl;
738
739
    const Tableau::Entry* spoiler = NULL;
740
    while( (spoiler = d_linEq.selectSlackEntry(d_soiVar, false)) != NULL){
741
      ArithVar nb = spoiler->getColVar();
742
      int oppositeSgn = -(spoiler->getCoefficient().sgn());
743
      Assert(oppositeSgn != 0);
744
745
      Debug("arith::greedyConflictSubsets") << "looking for " << nb << " " << oppositeSgn << endl;
746
747
      ArithVar basicWithOp = find_basic_in_sgns(sgns, nb, oppositeSgn, hasParticipated, false);
748
749
      if(basicWithOp == ARITHVAR_SENTINEL){
750
        Debug("arith::greedyConflictSubsets") << "search did not work  for " << nb << endl;
751
        // greedy construction has failed
752
        break;
753
      }else{
754
        Debug("arith::greedyConflictSubsets") << "found  " << basicWithOp << endl;
755
756
        addToInfeasFunc(d_statistics.d_soiConflictMinimization, d_soiVar, basicWithOp);
757
        hasParticipated.softAdd(basicWithOp);
758
        underConstruction.push_back(basicWithOp);
759
      }
760
    }
761
    if(spoiler == NULL){
762
      Debug("arith::greedyConflictSubsets") << "success" << endl;
763
      //then underConstruction contains a conflicting subset
764
      Assert(debugIsASet(underConstruction));
765
      subsets.push_back(underConstruction);
766
      ++d_statistics.d_soiConflicts;
767
      if(underConstruction.size() == 3){
768
        ++d_statistics.d_hasToBeMinimal;
769
      }else{
770
        ++d_statistics.d_maybeNotMinimal;
771
      }
772
    }else{
773
      Debug("arith::greedyConflictSubsets") << "failure" << endl;
774
    }
775
    tearDownInfeasiblityFunction(d_statistics.d_soiConflictMinimization, d_soiVar);
776
    d_soiVar = ARITHVAR_SENTINEL;
777
    // if(false && spoiler == NULL){
778
    //   ArithVarVec tmp;
779
    //   int smallest = tryAllSubsets(underConstruction, 0, tmp);
780
    //   cout << underConstruction.size() << " " << smallest << endl;
781
    //   Assert(smallest >= underConstruction.size());
782
    //   if(smallest < underConstruction.size()){
783
    //     exit(-1);
784
    //   }
785
    // }
786
  }
787
788
  Assert(d_soiVar == ARITHVAR_SENTINEL);
789
  Debug("arith::greedyConflictSubsets") << "greedyConflictSubsets done" << endl;
790
  return subsets;
791
}
792
793
bool SumOfInfeasibilitiesSPD::generateSOIConflict(const ArithVarVec& subset){
794
  Assert(d_soiVar == ARITHVAR_SENTINEL);
795
  d_soiVar = constructInfeasiblityFunction(d_statistics.d_soiConflictMinimization, subset);
796
  Assert(!subset.empty());
797
  Assert(!d_conflictBuilder->underConstruction());
798
799
  Debug("arith::generateSOIConflict") << "SumOfInfeasibilitiesSPD::generateSOIConflict(...) start" << endl;
800
801
  bool success = false;
802
803
  for(ArithVarVec::const_iterator iter = subset.begin(), end = subset.end(); iter != end; ++iter){
804
    ArithVar e = *iter;
805
    ConstraintP violated = d_errorSet.getViolated(e);
806
    Assert(violated != NullConstraint);
807
808
    int sgn = d_errorSet.getSgn(e);
809
    const Rational& violatedCoeff = sgn > 0 ? d_negOne : d_posOne;
810
    Debug("arith::generateSOIConflict") << "basic error var: "
811
                                        << "(" <<  violatedCoeff << ")"
812
                                        << " " << violated
813
                                        << endl;
814
815
816
    d_conflictBuilder->addConstraint(violated, violatedCoeff);
817
    Assert(violated->hasProof());
818
    if(!success && !violated->negationHasProof()){
819
      success = true;
820
      d_conflictBuilder->makeLastConsequent();
821
    }
822
  }
823
824
  if(!success){
825
    // failure
826
    d_conflictBuilder->reset();
827
  } else {
828
    // pick a violated constraint arbitrarily. any of them may be selected for the conflict
829
    Assert(d_conflictBuilder->underConstruction());
830
    Assert(d_conflictBuilder->consequentIsSet());
831
832
    for(Tableau::RowIterator i = d_tableau.basicRowIterator(d_soiVar); !i.atEnd(); ++i){
833
      const Tableau::Entry& entry = *i;
834
      ArithVar v = entry.getColVar();
835
      if(v == d_soiVar){ continue; }
836
      const Rational& coeff = entry.getCoefficient();
837
838
      ConstraintP c = (coeff.sgn() > 0) ?
839
        d_variables.getUpperBoundConstraint(v) :
840
        d_variables.getLowerBoundConstraint(v);
841
842
      Debug("arith::generateSOIConflict") << "non-basic var: "
843
                                          << "(" <<  coeff << ")"
844
                                          << " " << c
845
                                          << endl;
846
      d_conflictBuilder->addConstraint(c, coeff);
847
    }
848
    ConstraintCP conflicted = d_conflictBuilder->commitConflict();
849
    d_conflictChannel.raiseConflict(conflicted, InferenceId::UNKNOWN);
850
  }
851
852
  tearDownInfeasiblityFunction(d_statistics.d_soiConflictMinimization, d_soiVar);
853
  d_soiVar = ARITHVAR_SENTINEL;
854
  Debug("arith::generateSOIConflict") << "SumOfInfeasibilitiesSPD::generateSOIConflict(...) done" << endl;
855
  Assert(d_soiVar == ARITHVAR_SENTINEL);
856
  Assert(!d_conflictBuilder->underConstruction());
857
  return success;
858
}
859
860
861
WitnessImprovement SumOfInfeasibilitiesSPD::SOIConflict(){
862
  static int instance = 0;
863
  instance++;
864
865
  Debug("arith::SOIConflict") << "SumOfInfeasibilitiesSPD::SOIConflict() start "
866
                              << instance << ": |E| = " << d_errorSize << endl;
867
  if(Debug.isOn("arith::SOIConflict")){
868
    d_errorSet.debugPrint(cout);
869
  }
870
  Debug("arith::SOIConflict") << endl;
871
872
  tearDownInfeasiblityFunction(d_statistics.d_soiConflictMinimization, d_soiVar);
873
  d_soiVar = ARITHVAR_SENTINEL;
874
875
  if(options::soiQuickExplain()){
876
    quickExplain();
877
    generateSOIConflict(d_qeConflict);
878
  }else{
879
    vector<ArithVarVec> subsets = greedyConflictSubsets();
880
    Assert(d_soiVar == ARITHVAR_SENTINEL);
881
    bool anySuccess = false;
882
    Assert(!subsets.empty());
883
    for(vector<ArithVarVec>::const_iterator i = subsets.begin(), end = subsets.end(); i != end; ++i){
884
      const ArithVarVec& subset = *i;
885
      Assert(debugIsASet(subset));
886
      anySuccess = generateSOIConflict(subset) || anySuccess;
887
      //Node conflict = generateSOIConflict(subset);
888
      //cout << conflict << endl;
889
890
      //reportConflict(conf); do not do this. We need a custom explanations!
891
      //d_conflictChannel(conflict);
892
    }
893
    Assert(anySuccess);
894
  }
895
  Assert(d_soiVar == ARITHVAR_SENTINEL);
896
  d_soiVar = constructInfeasiblityFunction(d_statistics.d_soiConflictMinimization);
897
898
  //reportConflict(conf); do not do this. We need a custom explanations!
899
  d_conflictVariables.add(d_soiVar);
900
901
  Debug("arith::SOIConflict") << "SumOfInfeasibilitiesSPD::SOIConflict() done "
902
                              << instance << "end" << endl;
903
  return ConflictFound;
904
}
905
906
WitnessImprovement SumOfInfeasibilitiesSPD::soiRound() {
907
  Assert(d_soiVar != ARITHVAR_SENTINEL);
908
909
  bool useBlands = degeneratePivotsInARow() >= s_maxDegeneratePivotsBeforeBlandsOnLeaving;
910
  LinearEqualityModule::UpdatePreferenceFunction upf;
911
  if(useBlands) {
912
    upf = &LinearEqualityModule::preferWitness<false>;
913
  } else {
914
    upf = &LinearEqualityModule::preferWitness<true>;
915
  }
916
917
  LinearEqualityModule::VarPreferenceFunction bpf = useBlands ?
918
    &LinearEqualityModule::minVarOrder :
919
    &LinearEqualityModule::minRowLength;
920
  bpf = &LinearEqualityModule::minVarOrder;
921
922
  UpdateInfo selected = selectUpdate(upf, bpf);
923
924
  if(selected.uninitialized()){
925
    Debug("selectFocusImproving") << "SOI is optimum, but we don't have sat/conflict yet" << endl;
926
    return SOIConflict();
927
  }else{
928
    Assert(!selected.uninitialized());
929
    WitnessImprovement w = selected.getWitness(false);
930
    Assert(debugCheckWitness(selected, w, false));
931
932
    updateAndSignal(selected, w);
933
    logPivot(w);
934
    return w;
935
  }
936
}
937
938
bool SumOfInfeasibilitiesSPD::debugSOI(WitnessImprovement w, ostream& out, int instance) const{
939
  return true;
940
  // out << "DLV("<<instance<<") ";
941
  // switch(w){
942
  // case ConflictFound:
943
  //   out << "found conflict" << endl;
944
  //   return !d_conflictVariables.empty();
945
  // case ErrorDropped:
946
  //   return false;
947
  //   // out << "dropped " << prevErrorSize - d_errorSize << endl;
948
  //   // return d_errorSize < prevErrorSize;
949
  // case FocusImproved:
950
  //   out << "focus improved"<< endl;
951
  //   return d_errorSize == prevErrorSize;
952
  // case FocusShrank:
953
  //   Unreachable();
954
  //   return false;
955
  // case BlandsDegenerate:
956
  //   out << "bland degenerate"<< endl;
957
  //   return true;
958
  // case HeuristicDegenerate:
959
  //   out << "heuristic degenerate"<< endl;
960
  //   return true;
961
  // case AntiProductive:
962
  // case Degenerate:
963
  //   return false;
964
  // }
965
  // return false;
966
}
967
968
Result::Sat SumOfInfeasibilitiesSPD::sumOfInfeasibilities(){
969
  static int instance = 0;
970
  static bool verbose = false;
971
972
  TimerStat::CodeTimer codeTimer(d_statistics.d_soiTimer);
973
974
  Assert(d_sgnDisagreements.empty());
975
  Assert(d_pivotBudget != 0);
976
  Assert(d_errorSize == d_errorSet.errorSize());
977
  Assert(d_errorSize > 0);
978
  Assert(d_conflictVariables.empty());
979
  Assert(d_soiVar == ARITHVAR_SENTINEL);
980
981
  //d_scores.purge();
982
  d_soiVar = constructInfeasiblityFunction(d_statistics.d_soiFocusConstructionTimer);
983
984
985
  while(d_pivotBudget != 0  && d_errorSize > 0 && d_conflictVariables.empty()){
986
    ++instance;
987
    Debug("dualLike") << "dualLike " << instance << endl;
988
989
    Assert(d_errorSet.noSignals());
990
    // Possible outcomes:
991
    // - conflict
992
    // - budget was exhausted
993
    // - focus went down
994
    Debug("dualLike") << "selectFocusImproving " << endl;
995
    WitnessImprovement w = soiRound();
996
997
    Assert(d_errorSize == d_errorSet.errorSize());
998
999
    if (verbose)
1000
    {
1001
      debugSOI(w, CVC4Message(), instance);
1002
    }
1003
    Assert(debugSOI(w, Debug("dualLike"), instance));
1004
  }
1005
1006
1007
  if(d_soiVar != ARITHVAR_SENTINEL){
1008
    tearDownInfeasiblityFunction(d_statistics.d_soiFocusConstructionTimer, d_soiVar);
1009
    d_soiVar = ARITHVAR_SENTINEL;
1010
  }
1011
1012
  Assert(d_soiVar == ARITHVAR_SENTINEL);
1013
  if(!d_conflictVariables.empty()){
1014
    return Result::UNSAT;
1015
  }else if(d_errorSet.errorEmpty()){
1016
    Assert(d_errorSet.noSignals());
1017
    return Result::SAT;
1018
  }else{
1019
    Assert(d_pivotBudget == 0);
1020
    return Result::SAT_UNKNOWN;
1021
  }
1022
}
1023
1024
}/* CVC4::theory::arith namespace */
1025
}/* CVC4::theory namespace */
1026
26676
}/* CVC4 namespace */