src/theory/arith/soi_simplex.h

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