src/theory/arith/soi_simplex.cpp

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