src/theory/arith/soi_simplex.h

   1 /*********************                                                        */
   2 /*! \file soi_simplex.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Tim King, Morgan Deters
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2016 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 This is an implementation of the Simplex Module for the Simplex for DPLL(T)
  13  ** decision procedure.
  14  **
  15  ** This implements the Simplex module for the Simpelx for DPLL(T) decision procedure.
  16  ** See the Simplex for DPLL(T) technical report for more background.(citation?)
  17  ** This shares with the theory a Tableau, and a PartialModel that:
  18  **  - satisfies the equalities in the Tableau, and
  19  **  - the assignment for the non-basic variables satisfies their bounds.
  20  ** This is required to either produce a conflict or satisifying PartialModel.
  21  ** Further, we require being told when a basic variable updates its value.
  22  **
  23  ** During the Simplex search we maintain a queue of variables.
  24  ** The queue is required to contain all of the basic variables that voilate their bounds.
  25  ** As elimination from the queue is more efficient to be done lazily,
  26  ** we do not maintain that the queue of variables needs to be only basic variables or only
  27  ** variables that satisfy their bounds.
  28  **
  29  ** The simplex procedure roughly follows Alberto's thesis. (citation?)
  30  ** There is one round of selecting using a heuristic pivoting rule. (See PreferenceFunction
  31  ** Documentation for the available options.)
  32  ** The non-basic variable is the one that appears in the fewest pivots. (Bruno says that
  33  ** Leonardo invented this first.)
  34  ** After this, Bland's pivot rule is invoked.
  35  **
  36  ** During this proccess, we periodically inspect the queue of variables to
  37  ** 1) remove now extraneous extries,
  38  ** 2) detect conflicts that are "waiting" on the queue but may not be detected by the
  39  **  current queue heuristics, and
  40  ** 3) detect multiple conflicts.
  41  **
  42  ** Conflicts are greedily slackened to use the weakest bounds that still produce the
  43  ** conflict.
  44  **
  45  ** Extra things tracked atm: (Subject to change at Tim's whims)
  46  ** - A superset of all of the newly pivoted variables.
  47  ** - A queue of additional conflicts that were discovered by Simplex.
  48  **   These are theory valid and are currently turned into lemmas
  49  **/
  50
  51 #include "cvc4_private.h"
  52
  53 #pragma once
  54
  55 #include <stdint.h>
  56
  57 #include "theory/arith/simplex.h"
  58 #include "util/dense_map.h"
  59 #include "util/statistics_registry.h"
  60
  61 namespace CVC4 {
  62 namespace theory {
  63 namespace arith {
  64
  65 class SumOfInfeasibilitiesSPD : public SimplexDecisionProcedure {
  66 public:
  67   SumOfInfeasibilitiesSPD(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc);
  68
  69   Result::Sat findModel(bool exactResult);
  70
  71   // other error variables are dropping
  72   WitnessImprovement dualLikeImproveError(ArithVar evar);
  73   WitnessImprovement primalImproveError(ArithVar evar);
  74
  75 private:
  76   /** The current sum of infeasibilities variable. */
  77   ArithVar d_soiVar;
  78
  79   // dual like
  80   // - found conflict
  81   // - satisfied error set
  82   Result::Sat sumOfInfeasibilities();
  83
  84   // static const uint32_t PENALTY = 4;
  85   // DenseMultiset d_scores;
  86   // void decreasePenalties(){ d_scores.removeOneOfEverything(); }
  87   // uint32_t penalty(ArithVar x) const { return d_scores.count(x); }
  88   // void setPenalty(ArithVar x, WitnessImprovement w){
  89   //   if(improvement(w)){
  90   //     if(d_scores.count(x) > 0){
  91   //       d_scores.removeAll(x);
  92   //     }
  93   //   }else{
  94   //     d_scores.setCount(x, PENALTY);
  95   //   }
  96   // }
  97
  98   int32_t d_pivotBudget;
  99   // enum PivotImprovement {
 100   //   ErrorDropped,
 101   //   NonDegenerate,
 102   //   HeuristicDegenerate,
 103   //   BlandsDegenerate
 104   // };
 105
 106   WitnessImprovement d_prevWitnessImprovement;
 107   uint32_t d_witnessImprovementInARow;
 108
 109   uint32_t degeneratePivotsInARow() const;
 110
 111   static const uint32_t s_focusThreshold = 6;
 112   static const uint32_t s_maxDegeneratePivotsBeforeBlandsOnLeaving = 100;
 113   static const uint32_t s_maxDegeneratePivotsBeforeBlandsOnEntering = 10;
 114
 115   DenseMap<uint32_t> d_leavingCountSinceImprovement;
 116   void increaseLeavingCount(ArithVar x){
 117     if(!d_leavingCountSinceImprovement.isKey(x)){
 118       d_leavingCountSinceImprovement.set(x,1);
 119     }else{
 120       (d_leavingCountSinceImprovement.get(x))++;
 121     }
 122   }
 123   LinearEqualityModule::UpdatePreferenceFunction selectLeavingFunction(ArithVar x){
 124     bool useBlands = d_leavingCountSinceImprovement.isKey(x) &&
 125       d_leavingCountSinceImprovement[x] >= s_maxDegeneratePivotsBeforeBlandsOnEntering;
 126     if(useBlands) {
 127       return &LinearEqualityModule::preferWitness<false>;
 128     } else {
 129       return &LinearEqualityModule::preferWitness<true>;
 130     }
 131   }
 132
 133   bool debugSOI(WitnessImprovement w, std::ostream& out, int instance) const;
 134
 135   void debugPrintSignal(ArithVar updated) const;
 136
 137   ArithVarVec d_sgnDisagreements;
 138
 139   void logPivot(WitnessImprovement w);
 140
 141   void updateAndSignal(const UpdateInfo& selected, WitnessImprovement w);
 142
 143   UpdateInfo selectUpdate(LinearEqualityModule::UpdatePreferenceFunction upf,
 144                           LinearEqualityModule::VarPreferenceFunction bpf);
 145
 146
 147   // UpdateInfo selectUpdateForDualLike(ArithVar basic){
 148   //   TimerStat::CodeTimer codeTimer(d_statistics.d_selectUpdateForDualLike);
 149
 150   //   LinearEqualityModule::UpdatePreferenceFunction upf =
 151   //     &LinearEqualityModule::preferWitness<true>;
 152   //   LinearEqualityModule::VarPreferenceFunction bpf =
 153   //     &LinearEqualityModule::minVarOrder;
 154   //   return selectPrimalUpdate(basic, upf, bpf);
 155   // }
 156
 157   // UpdateInfo selectUpdateForPrimal(ArithVar basic, bool useBlands){
 158   //   TimerStat::CodeTimer codeTimer(d_statistics.d_selectUpdateForPrimal);
 159
 160   //   LinearEqualityModule::UpdatePreferenceFunction upf = useBlands ?
 161   //     &LinearEqualityModule::preferWitness<false>:
 162   //     &LinearEqualityModule::preferWitness<true>;
 163
 164   //   LinearEqualityModule::VarPreferenceFunction bpf = useBlands ?
 165   //     &LinearEqualityModule::minVarOrder :
 166   //     &LinearEqualityModule::minRowLength;
 167   //   bpf = &LinearEqualityModule::minVarOrder;
 168
 169   //   return selectPrimalUpdate(basic, upf, bpf);
 170   // }
 171   // WitnessImprovement selectFocusImproving() ;
 172   WitnessImprovement soiRound();
 173   WitnessImprovement SOIConflict();
 174   std::vector< ArithVarVec > greedyConflictSubsets();
 175   bool generateSOIConflict(const ArithVarVec& subset);
 176
 177   // WitnessImprovement focusUsingSignDisagreements(ArithVar basic);
 178   // WitnessImprovement focusDownToLastHalf();
 179   // WitnessImprovement adjustFocusShrank(const ArithVarVec& drop);
 180   // WitnessImprovement focusDownToJust(ArithVar v);
 181
 182
 183   void adjustFocusAndError(const UpdateInfo& up, const AVIntPairVec& focusChanges);
 184
 185   /**
 186    * This is the main simplex for DPLL(T) loop.
 187    * It runs for at most maxIterations.
 188    *
 189    * Returns true iff it has found a conflict.
 190    * d_conflictVariable will be set and the conflict for this row is reported.
 191    */
 192   bool searchForFeasibleSolution(uint32_t maxIterations);
 193
 194   bool initialProcessSignals(){
 195     TimerStat &timer = d_statistics.d_initialSignalsTime;
 196     IntStat& conflictStat  = d_statistics.d_initialConflicts;
 197     return standardProcessSignals(timer, conflictStat);
 198   }
 199
 200   void quickExplain();
 201   DenseSet d_qeInSoi;
 202   DenseSet d_qeInUAndNotInSoi;
 203   ArithVarVec d_qeConflict;
 204   ArithVarVec d_qeGreedyOrder;
 205   sgn_table d_qeSgns;
 206
 207   uint32_t quickExplainRec(uint32_t cEnd, uint32_t uEnd);
 208   void qeAddRange(uint32_t begin, uint32_t end);
 209   void qeRemoveRange(uint32_t begin, uint32_t end);
 210   void qeSwapRange(uint32_t N, uint32_t r, uint32_t s);
 211
 212   unsigned trySet(const ArithVarVec& set);
 213   unsigned tryAllSubsets(const ArithVarVec& set, unsigned depth, ArithVarVec& tmp);
 214
 215   /** These fields are designed to be accessible to TheoryArith methods. */
 216   class Statistics {
 217   public:
 218     TimerStat d_initialSignalsTime;
 219     IntStat d_initialConflicts;
 220
 221     IntStat d_soiFoundUnsat;
 222     IntStat d_soiFoundSat;
 223     IntStat d_soiMissed;
 224
 225     IntStat d_soiConflicts;
 226     IntStat d_hasToBeMinimal;
 227     IntStat d_maybeNotMinimal;
 228
 229     TimerStat d_soiTimer;
 230     TimerStat d_soiFocusConstructionTimer;
 231     TimerStat d_soiConflictMinimization;
 232     TimerStat d_selectUpdateForSOI;
 233
 234     ReferenceStat<uint32_t> d_finalCheckPivotCounter;
 235
 236     Statistics(uint32_t& pivots);
 237     ~Statistics();
 238   } d_statistics;
 239 };/* class FCSimplexDecisionProcedure */
 240
 241 }/* CVC4::theory::arith namespace */
 242 }/* CVC4::theory namespace */
 243 }/* CVC4 namespace */