GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/fc_simplex.cpp Lines: 29 495 5.9 %
Date: 2021-03-22 Branches: 45 2208 2.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file fc_simplex.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Tim King, Aina Niemetz, 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
#include "theory/arith/fc_simplex.h"
18
19
#include "base/output.h"
20
#include "options/arith_options.h"
21
#include "smt/smt_statistics_registry.h"
22
#include "theory/arith/constraint.h"
23
#include "theory/arith/error_set.h"
24
#include "util/statistics_registry.h"
25
26
using namespace std;
27
28
namespace CVC4 {
29
namespace theory {
30
namespace arith {
31
32
33
8995
FCSimplexDecisionProcedure::FCSimplexDecisionProcedure(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc)
34
  : SimplexDecisionProcedure(linEq, errors, conflictChannel, tvmalloc)
35
  , d_focusSize(0)
36
  , d_focusErrorVar(ARITHVAR_SENTINEL)
37
  , d_focusCoefficients()
38
  , d_pivotBudget(0)
39
  , d_prevWitnessImprovement(AntiProductive)
40
  , d_witnessImprovementInARow(0)
41
  , d_sgnDisagreements()
42
8995
  , d_statistics(d_pivots)
43
8995
{ }
44
45
8995
FCSimplexDecisionProcedure::Statistics::Statistics(uint32_t& pivots):
46
  d_initialSignalsTime("theory::arith::FC::initialProcessTime"),
47
  d_initialConflicts("theory::arith::FC::UpdateConflicts", 0),
48
  d_fcFoundUnsat("theory::arith::FC::FoundUnsat", 0),
49
  d_fcFoundSat("theory::arith::FC::FoundSat", 0),
50
  d_fcMissed("theory::arith::FC::Missed", 0),
51
  d_fcTimer("theory::arith::FC::Timer"),
52
  d_fcFocusConstructionTimer("theory::arith::FC::Construction"),
53
  d_selectUpdateForDualLike("theory::arith::FC::selectUpdateForDualLike"),
54
  d_selectUpdateForPrimal("theory::arith::FC::selectUpdateForPrimal"),
55
8995
  d_finalCheckPivotCounter("theory::arith::FC::lastPivots", pivots)
56
{
57
8995
  smtStatisticsRegistry()->registerStat(&d_initialSignalsTime);
58
8995
  smtStatisticsRegistry()->registerStat(&d_initialConflicts);
59
60
8995
  smtStatisticsRegistry()->registerStat(&d_fcFoundUnsat);
61
8995
  smtStatisticsRegistry()->registerStat(&d_fcFoundSat);
62
8995
  smtStatisticsRegistry()->registerStat(&d_fcMissed);
63
64
8995
  smtStatisticsRegistry()->registerStat(&d_fcTimer);
65
8995
  smtStatisticsRegistry()->registerStat(&d_fcFocusConstructionTimer);
66
67
8995
  smtStatisticsRegistry()->registerStat(&d_selectUpdateForDualLike);
68
8995
  smtStatisticsRegistry()->registerStat(&d_selectUpdateForPrimal);
69
70
8995
  smtStatisticsRegistry()->registerStat(&d_finalCheckPivotCounter);
71
8995
}
72
73
17984
FCSimplexDecisionProcedure::Statistics::~Statistics(){
74
8992
  smtStatisticsRegistry()->unregisterStat(&d_initialSignalsTime);
75
8992
  smtStatisticsRegistry()->unregisterStat(&d_initialConflicts);
76
77
8992
  smtStatisticsRegistry()->unregisterStat(&d_fcFoundUnsat);
78
8992
  smtStatisticsRegistry()->unregisterStat(&d_fcFoundSat);
79
8992
  smtStatisticsRegistry()->unregisterStat(&d_fcMissed);
80
81
8992
  smtStatisticsRegistry()->unregisterStat(&d_fcTimer);
82
8992
  smtStatisticsRegistry()->unregisterStat(&d_fcFocusConstructionTimer);
83
84
8992
  smtStatisticsRegistry()->unregisterStat(&d_selectUpdateForDualLike);
85
8992
  smtStatisticsRegistry()->unregisterStat(&d_selectUpdateForPrimal);
86
87
8992
  smtStatisticsRegistry()->unregisterStat(&d_finalCheckPivotCounter);
88
8992
}
89
90
Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){
91
  Assert(d_conflictVariables.empty());
92
  Assert(d_sgnDisagreements.empty());
93
94
  d_pivots = 0;
95
  static thread_local unsigned int instance = 0;
96
  instance = instance + 1;
97
  static const bool verbose = false;
98
99
  if(d_errorSet.errorEmpty() && !d_errorSet.moreSignals()){
100
    Debug("arith::findModel") << "fcFindModel("<< instance <<") trivial" << endl;
101
    Assert(d_conflictVariables.empty());
102
    //if (verbose)
103
    //{
104
    //  CVC4Message() << "fcFindModel(" << instance << ") trivial" << endl;
105
    //}
106
    return Result::SAT;
107
  }
108
109
  // We need to reduce this because of
110
  d_errorSet.reduceToSignals();
111
112
  // We must start tracking NOW
113
  d_errorSet.setSelectionRule(options::ErrorSelectionRule::SUM_METRIC);
114
115
  if(initialProcessSignals()){
116
    d_conflictVariables.purge();
117
    if (verbose)
118
    {
119
      CVC4Message() << "fcFindModel(" << instance << ") early conflict" << endl;
120
    }
121
    Debug("arith::findModel") << "fcFindModel("<< instance <<") early conflict" << endl;
122
    Assert(d_conflictVariables.empty());
123
    return Result::UNSAT;
124
  }else if(d_errorSet.errorEmpty()){
125
    //if (verbose)
126
    //{
127
    //  CVC4Message() << "fcFindModel(" << instance << ") fixed itself" << endl;
128
    //}
129
    Debug("arith::findModel") << "fcFindModel("<< instance <<") fixed itself" << endl;
130
    if (verbose) Assert(!d_errorSet.moreSignals());
131
    Assert(d_conflictVariables.empty());
132
    return Result::SAT;
133
  }
134
135
  Debug("arith::findModel") << "fcFindModel(" << instance <<") start non-trivial" << endl;
136
137
  exactResult |= options::arithStandardCheckVarOrderPivots() < 0;
138
139
  d_prevWitnessImprovement = HeuristicDegenerate;
140
  d_witnessImprovementInARow = 0;
141
142
  Result::Sat result = Result::SAT_UNKNOWN;
143
144
  if(result == Result::SAT_UNKNOWN){
145
    if(exactResult){
146
      d_pivotBudget = -1;
147
    }else{
148
      d_pivotBudget = options::arithStandardCheckVarOrderPivots();
149
    }
150
151
    result = dualLike();
152
153
    if(result ==  Result::UNSAT){
154
      ++(d_statistics.d_fcFoundUnsat);
155
      if (verbose)
156
      {
157
        CVC4Message() << "fc found unsat";
158
      }
159
    }else if(d_errorSet.errorEmpty()){
160
      ++(d_statistics.d_fcFoundSat);
161
      if (verbose)
162
      {
163
        CVC4Message() << "fc found model";
164
      }
165
    }else{
166
      ++(d_statistics.d_fcMissed);
167
      if (verbose)
168
      {
169
        CVC4Message() << "fc missed";
170
      }
171
    }
172
  }
173
  if (verbose)
174
  {
175
    CVC4Message() << "(" << instance << ") pivots " << d_pivots << endl;
176
  }
177
178
  Assert(!d_errorSet.moreSignals());
179
  if(result == Result::SAT_UNKNOWN && d_errorSet.errorEmpty()){
180
    result = Result::SAT;
181
  }
182
183
  // ensure that the conflict variable is still in the queue.
184
  d_conflictVariables.purge();
185
186
  Debug("arith::findModel") << "end findModel() " << instance << " " << result <<  endl;
187
188
  Assert(d_conflictVariables.empty());
189
  return result;
190
}
191
192
193
void FCSimplexDecisionProcedure::logPivot(WitnessImprovement w){
194
  if(d_pivotBudget > 0) {
195
    --d_pivotBudget;
196
  }
197
  Assert(w != AntiProductive);
198
199
  if(w == d_prevWitnessImprovement){
200
    ++d_witnessImprovementInARow;
201
    // ignore overflow : probably never reached
202
    if(d_witnessImprovementInARow == 0){
203
      --d_witnessImprovementInARow;
204
    }
205
  }else{
206
    if(w != BlandsDegenerate){
207
      d_witnessImprovementInARow = 1;
208
    }
209
    // if w == BlandsDegenerate do not reset the counter
210
    d_prevWitnessImprovement = w;
211
  }
212
  if(strongImprovement(w)){
213
    d_leavingCountSinceImprovement.purge();
214
  }
215
216
  Debug("logPivot") << "logPivot " << d_prevWitnessImprovement << " "  << d_witnessImprovementInARow << endl;
217
218
}
219
220
uint32_t FCSimplexDecisionProcedure::degeneratePivotsInARow() const {
221
  switch(d_prevWitnessImprovement){
222
  case ConflictFound:
223
  case ErrorDropped:
224
  case FocusImproved:
225
    return 0;
226
  case HeuristicDegenerate:
227
  case BlandsDegenerate:
228
    return d_witnessImprovementInARow;
229
  // Degenerate is unreachable for its own reasons
230
  case Degenerate:
231
  case FocusShrank:
232
  case AntiProductive:
233
    Unreachable();
234
    return -1;
235
  }
236
  Unreachable();
237
}
238
239
void FCSimplexDecisionProcedure::adjustFocusAndError(const UpdateInfo& up, const AVIntPairVec& focusChanges){
240
  uint32_t newErrorSize = d_errorSet.errorSize();
241
  uint32_t newFocusSize = d_errorSet.focusSize();
242
243
  //Assert(!d_conflictVariables.empty() || newFocusSize <= d_focusSize);
244
  Assert(!d_conflictVariables.empty() || newErrorSize <= d_errorSize);
245
246
  if(newFocusSize == 0 || !d_conflictVariables.empty() ){
247
    tearDownInfeasiblityFunction(d_statistics.d_fcFocusConstructionTimer, d_focusErrorVar);
248
    d_focusErrorVar = ARITHVAR_SENTINEL;
249
  }else if(2*newFocusSize < d_focusSize ){
250
    tearDownInfeasiblityFunction(d_statistics.d_fcFocusConstructionTimer, d_focusErrorVar);
251
    d_focusErrorVar = constructInfeasiblityFunction(d_statistics.d_fcFocusConstructionTimer);
252
  }else{
253
    adjustInfeasFunc(d_statistics.d_fcFocusConstructionTimer, d_focusErrorVar, focusChanges);
254
  }
255
256
  d_errorSize = newErrorSize;
257
  d_focusSize = newFocusSize;
258
}
259
260
WitnessImprovement FCSimplexDecisionProcedure::adjustFocusShrank(const ArithVarVec& dropped){
261
  Assert(dropped.size() > 0);
262
  Assert(d_errorSet.focusSize() == d_focusSize);
263
  Assert(d_errorSet.focusSize() > dropped.size());
264
265
  uint32_t newFocusSize = d_focusSize - dropped.size();
266
  Assert(newFocusSize > 0);
267
268
  if(2 * newFocusSize <= d_focusSize){
269
    d_errorSet.dropFromFocusAll(dropped);
270
    tearDownInfeasiblityFunction(d_statistics.d_fcFocusConstructionTimer, d_focusErrorVar);
271
    d_focusErrorVar = constructInfeasiblityFunction(d_statistics.d_fcFocusConstructionTimer);
272
  }else{
273
    shrinkInfeasFunc(d_statistics.d_fcFocusConstructionTimer, d_focusErrorVar, dropped);
274
    d_errorSet.dropFromFocusAll(dropped);
275
  }
276
277
  d_focusSize = newFocusSize;
278
  Assert(d_errorSet.focusSize() == d_focusSize);
279
  return FocusShrank;
280
}
281
282
WitnessImprovement FCSimplexDecisionProcedure::focusDownToJust(ArithVar v){
283
  // uint32_t newErrorSize = d_errorSet.errorSize();
284
  // uint32_t newFocusSize = d_errorSet.focusSize();
285
  Assert(d_focusSize == d_errorSet.focusSize());
286
  Assert(d_focusSize > 1);
287
  Assert(d_errorSet.inFocus(v));
288
289
  d_errorSet.focusDownToJust(v);
290
  Assert(d_errorSet.focusSize() == 1);
291
  d_focusSize = 1;
292
293
  tearDownInfeasiblityFunction(d_statistics.d_fcFocusConstructionTimer, d_focusErrorVar);
294
  d_focusErrorVar = constructInfeasiblityFunction(d_statistics.d_fcFocusConstructionTimer);
295
296
  return FocusShrank;
297
}
298
299
300
301
UpdateInfo FCSimplexDecisionProcedure::selectPrimalUpdate(ArithVar basic, LinearEqualityModule::UpdatePreferenceFunction upf, LinearEqualityModule::VarPreferenceFunction bpf) {
302
  UpdateInfo selected;
303
304
  static int instance = 0 ;
305
  ++instance;
306
307
  Debug("arith::selectPrimalUpdate")
308
    << "selectPrimalUpdate " << instance << endl
309
    << basic << " " << d_tableau.basicRowLength(basic)
310
    << " " << d_linEq.debugBasicAtBoundCount(basic) << endl;
311
312
  static const int s_maxCandidatesAfterImprove = 3;
313
  bool isFocus = basic == d_focusErrorVar;
314
  Assert(isFocus || d_errorSet.inError(basic));
315
  int basicDir =  isFocus? 1 : d_errorSet.getSgn(basic);
316
  bool dualLike = !isFocus && d_focusSize > 1;
317
318
  if(!isFocus){
319
    loadFocusSigns();
320
  }
321
322
  decreasePenalties();
323
324
  typedef std::vector<Cand> CandVector;
325
  CandVector candidates;
326
327
  for(Tableau::RowIterator ri = d_tableau.basicRowIterator(basic); !ri.atEnd(); ++ri){
328
    const Tableau::Entry& e = *ri;
329
    ArithVar curr = e.getColVar();
330
    if(curr == basic){ continue; }
331
332
    int sgn = e.getCoefficient().sgn();
333
    int curr_movement = basicDir * sgn;
334
335
    bool candidate =
336
      (curr_movement > 0 && d_variables.cmpAssignmentUpperBound(curr) < 0) ||
337
      (curr_movement < 0 && d_variables.cmpAssignmentLowerBound(curr) > 0);
338
339
    Debug("arith::selectPrimalUpdate")
340
      << "storing " << basic
341
      << " " << curr
342
      << " " << candidate
343
      << " " << e.getCoefficient()
344
      << " " << curr_movement
345
      << " " << focusCoefficient(curr) << endl;
346
347
    if(!candidate) { continue; }
348
349
    if(!isFocus){
350
      const Rational& focusC = focusCoefficient(curr);
351
      Assert(dualLike || !focusC.isZero());
352
      if(dualLike && curr_movement != focusC.sgn()){
353
        Debug("arith::selectPrimalUpdate") << "sgn disagreement " << curr << endl;
354
        d_sgnDisagreements.push_back(curr);
355
        continue;
356
      }else{
357
        candidates.push_back(Cand(curr, penalty(curr), curr_movement, &focusC));
358
      }
359
    }else{
360
      candidates.push_back(Cand(curr, penalty(curr), curr_movement, &e.getCoefficient()));
361
    }
362
  }
363
364
  CompPenaltyColLength colCmp(&d_linEq);
365
  CandVector::iterator i = candidates.begin();
366
  CandVector::iterator end = candidates.end();
367
  std::make_heap(i, end, colCmp);
368
369
  bool checkEverything = d_pivots == 0;
370
371
  int candidatesAfterFocusImprove = 0;
372
  while(i != end && (checkEverything || candidatesAfterFocusImprove <= s_maxCandidatesAfterImprove)){
373
    std::pop_heap(i, end, colCmp);
374
    --end;
375
    Cand& cand = (*end);
376
    ArithVar curr = cand.d_nb;
377
    const Rational& coeff = *cand.d_coeff;
378
379
    LinearEqualityModule::UpdatePreferenceFunction leavingPrefFunc = selectLeavingFunction(curr);
380
    UpdateInfo currProposal = d_linEq.speculativeUpdate(curr, coeff, leavingPrefFunc);
381
382
    Debug("arith::selectPrimalUpdate")
383
      << "selected " << selected << endl
384
      << "currProp " << currProposal << endl
385
      << "coeff " << coeff << endl;
386
387
    Assert(!currProposal.uninitialized());
388
389
    if(candidatesAfterFocusImprove > 0){
390
      candidatesAfterFocusImprove++;
391
    }
392
393
    if(selected.uninitialized() || (d_linEq.*upf)(selected, currProposal)){
394
395
      selected = currProposal;
396
      WitnessImprovement w = selected.getWitness(false);
397
      Debug("arith::selectPrimalUpdate") << "selected " << w << endl;
398
      setPenalty(curr, w);
399
      if(improvement(w)){
400
        bool exitEarly;
401
        switch(w){
402
        case ConflictFound: exitEarly = true; break;
403
        case ErrorDropped:
404
          if(checkEverything){
405
            exitEarly = d_errorSize + selected.errorsChange() == 0;
406
            Debug("arith::selectPrimalUpdate")
407
              << "ee " << d_errorSize << " "
408
              << selected.errorsChange() << " "
409
              << d_errorSize + selected.errorsChange() << endl;
410
          }else{
411
            exitEarly = true;
412
          }
413
          break;
414
        case FocusImproved:
415
          candidatesAfterFocusImprove = 1;
416
          exitEarly = false;
417
          break;
418
        default:
419
          exitEarly = false; break;
420
        }
421
        if(exitEarly){ break; }
422
      }
423
    }else{
424
      Debug("arith::selectPrimalUpdate") << "dropped "<< endl;
425
    }
426
427
  }
428
429
  if(!isFocus){
430
    unloadFocusSigns();
431
  }
432
  return selected;
433
}
434
435
bool FCSimplexDecisionProcedure::debugCheckWitness(const UpdateInfo& inf, WitnessImprovement w, bool useBlands){
436
  if(inf.getWitness(useBlands) == w){
437
    switch(w){
438
    case ConflictFound: return inf.foundConflict();
439
    case ErrorDropped: return inf.errorsChange() < 0;
440
    case FocusImproved: return inf.focusDirection() > 0;
441
    case FocusShrank: return false; // This is not a valid output
442
    case Degenerate: return false; // This is not a valid output
443
    case BlandsDegenerate: return useBlands;
444
    case HeuristicDegenerate: return !useBlands;
445
    case AntiProductive: return false;
446
    }
447
  }
448
  return false;
449
}
450
451
WitnessImprovement FCSimplexDecisionProcedure::primalImproveError(ArithVar errorVar){
452
  bool useBlands = degeneratePivotsInARow() >= s_maxDegeneratePivotsBeforeBlandsOnLeaving;
453
  UpdateInfo selected = selectUpdateForPrimal (errorVar, useBlands);
454
  Assert(!selected.uninitialized());
455
  WitnessImprovement w = selected.getWitness(useBlands);
456
  Assert(debugCheckWitness(selected, w, useBlands));
457
458
  updateAndSignal(selected, w);
459
  logPivot(w);
460
  return w;
461
}
462
463
464
WitnessImprovement FCSimplexDecisionProcedure::focusUsingSignDisagreements(ArithVar basic){
465
  Assert(!d_sgnDisagreements.empty());
466
  Assert(d_errorSet.focusSize() >= 2);
467
468
  if(Debug.isOn("arith::focus")){
469
    d_errorSet.debugPrint(Debug("arith::focus"));
470
  }
471
472
  ArithVar nb = d_linEq.minBy(d_sgnDisagreements, &LinearEqualityModule::minColLength);
473
  const Tableau::Entry& e_evar_nb = d_tableau.basicFindEntry(basic, nb);
474
  int oppositeSgn = - (e_evar_nb.getCoefficient().sgn());
475
  Debug("arith::focus") << "focusUsingSignDisagreements " << basic << " " << oppositeSgn << endl;
476
477
  ArithVarVec dropped;
478
479
  Tableau::ColIterator colIter = d_tableau.colIterator(nb);
480
  for(; !colIter.atEnd(); ++colIter){
481
    const Tableau::Entry& entry = *colIter;
482
    Assert(entry.getColVar() == nb);
483
484
    int sgn = entry.getCoefficient().sgn();
485
    Debug("arith::focus")
486
      << "on row "
487
      << d_tableau.rowIndexToBasic(entry.getRowIndex())
488
      << " "
489
      << entry.getCoefficient() << endl;
490
    ArithVar currRow = d_tableau.rowIndexToBasic(entry.getRowIndex());
491
    if(d_errorSet.inError(currRow) && d_errorSet.inFocus(currRow)){
492
      int errSgn = d_errorSet.getSgn(currRow);
493
494
      if(errSgn * sgn == oppositeSgn){
495
        dropped.push_back(currRow);
496
        Debug("arith::focus") << "dropping from focus " << currRow << endl;
497
      }
498
    }
499
  }
500
501
  d_sgnDisagreements.clear();
502
  return adjustFocusShrank(dropped);
503
}
504
505
bool debugSelectedErrorDropped(const UpdateInfo& selected, int32_t prevErrorSize, int32_t currErrorSize){
506
  int diff = currErrorSize - prevErrorSize;
507
  return selected.foundConflict() || diff == selected.errorsChange();
508
}
509
510
void FCSimplexDecisionProcedure::debugPrintSignal(ArithVar updated) const{
511
  Debug("updateAndSignal") << "updated basic " << updated;
512
  Debug("updateAndSignal") << " length " << d_tableau.basicRowLength(updated);
513
  Debug("updateAndSignal") << " consistent " << d_variables.assignmentIsConsistent(updated);
514
  int dir = !d_variables.assignmentIsConsistent(updated) ?
515
    d_errorSet.getSgn(updated) : 0;
516
  Debug("updateAndSignal") << " dir " << dir;
517
  Debug("updateAndSignal") << " debugBasicAtBoundCount " << d_linEq.debugBasicAtBoundCount(updated) << endl;
518
}
519
520
bool debugUpdatedBasic(const UpdateInfo& selected, ArithVar updated){
521
  if(selected.describesPivot() &&  updated == selected.leaving()){
522
    return selected.foundConflict();
523
  }else{
524
    return true;
525
  }
526
}
527
528
void FCSimplexDecisionProcedure::updateAndSignal(const UpdateInfo& selected, WitnessImprovement w){
529
  ArithVar nonbasic = selected.nonbasic();
530
531
  static bool verbose = false;
532
533
  Debug("updateAndSignal") << "updateAndSignal " << selected << endl;
534
535
  stringstream ss;
536
  if(verbose){
537
    d_errorSet.debugPrint(ss);
538
    if(selected.describesPivot()){
539
      ArithVar leaving = selected.leaving();
540
      ss << "leaving " << leaving
541
         << " " << d_tableau.basicRowLength(leaving)
542
         << " " << d_linEq.debugBasicAtBoundCount(leaving)
543
         << endl;
544
    }
545
    if(degenerate(w) && selected.describesPivot()){
546
      ArithVar leaving = selected.leaving();
547
      CVC4Message() << "degenerate " << leaving << ", atBounds "
548
                    << d_linEq.basicsAtBounds(selected) << ", len "
549
                    << d_tableau.basicRowLength(leaving) << ", bc "
550
                    << d_linEq.debugBasicAtBoundCount(leaving) << endl;
551
    }
552
  }
553
554
  if(selected.describesPivot()){
555
    ConstraintP limiting = selected.limiting();
556
    ArithVar basic = limiting->getVariable();
557
    Assert(d_linEq.basicIsTracked(basic));
558
    d_linEq.pivotAndUpdate(basic, nonbasic, limiting->getValue());
559
  }else{
560
    Assert(!selected.unbounded() || selected.errorsChange() < 0);
561
562
    DeltaRational newAssignment =
563
      d_variables.getAssignment(nonbasic) + selected.nonbasicDelta();
564
565
    d_linEq.updateTracked(nonbasic, newAssignment);
566
  }
567
  d_pivots++;
568
569
  increaseLeavingCount(nonbasic);
570
571
  vector< pair<ArithVar, int> > focusChanges;
572
  while(d_errorSet.moreSignals()){
573
    ArithVar updated = d_errorSet.topSignal();
574
    int prevFocusSgn = d_errorSet.popSignal();
575
576
    if(d_tableau.isBasic(updated)){
577
      Assert(!d_variables.assignmentIsConsistent(updated)
578
             == d_errorSet.inError(updated));
579
      if(Debug.isOn("updateAndSignal")){debugPrintSignal(updated);}
580
      if(!d_variables.assignmentIsConsistent(updated)){
581
        if(checkBasicForConflict(updated)){
582
          reportConflict(updated);
583
          Assert(debugUpdatedBasic(selected, updated));
584
        }
585
      }
586
    }else{
587
      Debug("updateAndSignal") << "updated nonbasic " << updated << endl;
588
    }
589
    int currFocusSgn = d_errorSet.focusSgn(updated);
590
    if(currFocusSgn != prevFocusSgn){
591
      int change = currFocusSgn - prevFocusSgn;
592
      focusChanges.push_back(make_pair(updated, change));
593
    }
594
  }
595
596
  if (verbose)
597
  {
598
    CVC4Message() << "conflict variable " << selected << endl;
599
    CVC4Message() << ss.str();
600
  }
601
  if(Debug.isOn("error")){ d_errorSet.debugPrint(Debug("error")); }
602
603
  Assert(
604
      debugSelectedErrorDropped(selected, d_errorSize, d_errorSet.errorSize()));
605
606
  adjustFocusAndError(selected, focusChanges);
607
}
608
609
WitnessImprovement FCSimplexDecisionProcedure::dualLikeImproveError(ArithVar errorVar){
610
  Assert(d_sgnDisagreements.empty());
611
  Assert(d_focusSize > 1);
612
613
  UpdateInfo selected = selectUpdateForDualLike(errorVar);
614
615
  if(selected.uninitialized()){
616
    // we found no proposals
617
    // If this is empty, there must be an error on this variable!
618
    // this should not be possible. It Should have been caught as a signal earlier
619
    WitnessImprovement dropped = focusUsingSignDisagreements(errorVar);
620
    Assert(d_sgnDisagreements.empty());
621
622
    return dropped;
623
  }else{
624
    d_sgnDisagreements.clear();
625
  }
626
627
  Assert(d_sgnDisagreements.empty());
628
  Assert(!selected.uninitialized());
629
630
  if(selected.focusDirection() == 0 &&
631
     d_prevWitnessImprovement == HeuristicDegenerate &&
632
     d_witnessImprovementInARow >= s_focusThreshold){
633
634
    Debug("focusDownToJust") << "focusDownToJust " << errorVar << endl;
635
636
    return focusDownToJust(errorVar);
637
  }else{
638
    WitnessImprovement w = selected.getWitness(false);
639
    Assert(debugCheckWitness(selected, w, false));
640
    updateAndSignal(selected, w);
641
    logPivot(w);
642
    return w;
643
  }
644
}
645
646
WitnessImprovement FCSimplexDecisionProcedure::focusDownToLastHalf(){
647
  Assert(d_focusSize >= 2);
648
649
  Debug("focusDownToLastHalf") << "focusDownToLastHalf "
650
       << d_errorSet.errorSize()  << " "
651
       << d_errorSet.focusSize() << " ";
652
653
  uint32_t half = d_focusSize/2;
654
  ArithVarVec buf;
655
  for(ErrorSet::focus_iterator i = d_errorSet.focusBegin(),
656
        i_end = d_errorSet.focusEnd(); i != i_end; ++i){
657
    if(half > 0){
658
      --half;
659
    } else{
660
      buf.push_back(*i);
661
    }
662
  }
663
  WitnessImprovement w = adjustFocusShrank(buf);
664
  Debug("focusDownToLastHalf") << "-> " << d_errorSet.focusSize() << endl;
665
  return w;
666
}
667
668
WitnessImprovement FCSimplexDecisionProcedure::selectFocusImproving() {
669
  Assert(d_focusErrorVar != ARITHVAR_SENTINEL);
670
  Assert(d_focusSize >= 2);
671
672
  LinearEqualityModule::UpdatePreferenceFunction upf =
673
    &LinearEqualityModule::preferWitness<true>;
674
675
  LinearEqualityModule::VarPreferenceFunction bpf =
676
    &LinearEqualityModule::minRowLength;
677
678
  UpdateInfo selected = selectPrimalUpdate(d_focusErrorVar, upf, bpf);
679
680
  if(selected.uninitialized()){
681
    Debug("selectFocusImproving") << "focus is optimum, but we don't have sat/conflict yet" << endl;
682
683
    return focusDownToLastHalf();
684
  }
685
  Assert(!selected.uninitialized());
686
  WitnessImprovement w = selected.getWitness(false);
687
  Assert(debugCheckWitness(selected, w, false));
688
689
  if(degenerate(w)){
690
    Debug("selectFocusImproving") << "only degenerate" << endl;
691
    if(d_prevWitnessImprovement == HeuristicDegenerate &&
692
       d_witnessImprovementInARow >= s_focusThreshold){
693
      Debug("selectFocusImproving") << "focus down been degenerate too long" << endl;
694
      return focusDownToLastHalf();
695
    }else{
696
      Debug("selectFocusImproving") << "taking degenerate" << endl;
697
    }
698
  }
699
  Debug("selectFocusImproving") << "selectFocusImproving did this " << selected << endl;
700
701
  updateAndSignal(selected, w);
702
  logPivot(w);
703
  return w;
704
}
705
706
bool FCSimplexDecisionProcedure::debugDualLike(WitnessImprovement w, ostream& out, int instance, uint32_t prevFocusSize, uint32_t prevErrorSize ) const{
707
  out << "DLV("<<instance<<") ";
708
  switch(w){
709
  case ConflictFound:
710
    out << "found conflict" << endl;
711
    return !d_conflictVariables.empty();
712
  case ErrorDropped:
713
    out << "dropped " << prevErrorSize - d_errorSize << endl;
714
    return d_errorSize < prevErrorSize;
715
  case FocusImproved:
716
    out << "focus improved"<< endl;
717
    return d_errorSize == prevErrorSize;
718
  case FocusShrank:
719
    out << "focus shrank"<< endl;
720
    return d_errorSize == prevErrorSize && prevFocusSize > d_focusSize;
721
  case BlandsDegenerate:
722
    out << "bland degenerate"<< endl;
723
    return true;
724
  case HeuristicDegenerate:
725
    out << "heuristic degenerate"<< endl;
726
    return true;
727
  case AntiProductive:
728
    out << "focus blur" << endl;
729
    return prevFocusSize == 0;
730
  case Degenerate:
731
    return false;
732
  }
733
  return false;
734
}
735
736
Result::Sat FCSimplexDecisionProcedure::dualLike(){
737
  static int instance = 0;
738
  static bool verbose = false;
739
740
  TimerStat::CodeTimer codeTimer(d_statistics.d_fcTimer);
741
742
  Assert(d_sgnDisagreements.empty());
743
  Assert(d_pivotBudget != 0);
744
  Assert(d_errorSize == d_errorSet.errorSize());
745
  Assert(d_errorSize > 0);
746
  Assert(d_focusSize == d_errorSet.focusSize());
747
  Assert(d_focusSize > 0);
748
  Assert(d_conflictVariables.empty());
749
  Assert(d_focusErrorVar == ARITHVAR_SENTINEL);
750
751
  d_scores.purge();
752
  d_focusErrorVar = constructInfeasiblityFunction(d_statistics.d_fcFocusConstructionTimer);
753
754
755
  while(d_pivotBudget != 0  && d_errorSize > 0 && d_conflictVariables.empty()){
756
    ++instance;
757
    Debug("dualLike") << "dualLike " << instance << endl;
758
759
    Assert(d_errorSet.noSignals());
760
761
    WitnessImprovement w = AntiProductive;
762
    uint32_t prevFocusSize = d_focusSize;
763
    uint32_t prevErrorSize = d_errorSize;
764
765
    if(d_focusSize == 0){
766
      Assert(d_errorSize == d_errorSet.errorSize());
767
      Assert(d_focusErrorVar == ARITHVAR_SENTINEL);
768
769
      d_errorSet.blur();
770
771
      d_focusSize = d_errorSet.focusSize();
772
773
      Assert(d_errorSize == d_focusSize);
774
      Assert(d_errorSize >= 1);
775
776
      d_focusErrorVar = constructInfeasiblityFunction(d_statistics.d_fcFocusConstructionTimer);
777
778
      Debug("dualLike") << "blur " << d_focusSize << endl;
779
    }else if(d_focusSize == 1){
780
      // Possible outcomes:
781
      // - errorSet size shrunk
782
      // -- fixed v
783
      // -- fixed something other than v
784
      // - conflict
785
      // - budget was exhausted
786
787
      ArithVar e = d_errorSet.topFocusVariable();
788
      Debug("dualLike") << "primalImproveError " << e << endl;
789
      w = primalImproveError(e);
790
    }else{
791
792
      // Possible outcomes:
793
      // - errorSet size shrunk
794
      // -- fixed v
795
      // -- fixed something other than v
796
      // - conflict
797
      // - budget was exhausted
798
      // - focus went down
799
      Assert(d_focusSize > 1);
800
      ArithVar e = d_errorSet.topFocusVariable();
801
      static const unsigned s_sumMetricThreshold = 1;
802
      if(d_errorSet.sumMetric(e) <= s_sumMetricThreshold){
803
        Debug("dualLike") << "dualLikeImproveError " << e << endl;
804
        w = dualLikeImproveError(e);
805
      }else{
806
        Debug("dualLike") << "selectFocusImproving " << endl;
807
        w = selectFocusImproving();
808
      }
809
    }
810
    Assert(d_focusSize == d_errorSet.focusSize());
811
    Assert(d_errorSize == d_errorSet.errorSize());
812
813
    if (verbose)
814
    {
815
      debugDualLike(w, CVC4Message(), instance, prevFocusSize, prevErrorSize);
816
    }
817
    Assert(debugDualLike(
818
        w, Debug("dualLike"), instance, prevFocusSize, prevErrorSize));
819
  }
820
821
822
  if(d_focusErrorVar != ARITHVAR_SENTINEL){
823
    tearDownInfeasiblityFunction(d_statistics.d_fcFocusConstructionTimer, d_focusErrorVar);
824
    d_focusErrorVar = ARITHVAR_SENTINEL;
825
  }
826
827
  Assert(d_focusErrorVar == ARITHVAR_SENTINEL);
828
  if(!d_conflictVariables.empty()){
829
    return Result::UNSAT;
830
  }else if(d_errorSet.errorEmpty()){
831
    Assert(d_errorSet.noSignals());
832
    return Result::SAT;
833
  }else{
834
    Assert(d_pivotBudget == 0);
835
    return Result::SAT_UNKNOWN;
836
  }
837
}
838
839
840
void FCSimplexDecisionProcedure::loadFocusSigns(){
841
  Assert(d_focusCoefficients.empty());
842
  Assert(d_focusErrorVar != ARITHVAR_SENTINEL);
843
  for(Tableau::RowIterator ri = d_tableau.basicRowIterator(d_focusErrorVar); !ri.atEnd(); ++ri){
844
    const Tableau::Entry& e = *ri;
845
    ArithVar curr = e.getColVar();
846
    d_focusCoefficients.set(curr, &e.getCoefficient());
847
  }
848
}
849
850
void FCSimplexDecisionProcedure::unloadFocusSigns(){
851
  d_focusCoefficients.purge();
852
}
853
854
const Rational& FCSimplexDecisionProcedure::focusCoefficient(ArithVar nb) const {
855
  if(d_focusCoefficients.isKey(nb)){
856
    return *(d_focusCoefficients[nb]);
857
  }else{
858
    return d_zero;
859
  }
860
}
861
862
}/* CVC4::theory::arith namespace */
863
}/* CVC4::theory namespace */
864
26676
}/* CVC4 namespace */