src/theory/arith/fc_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/error_set.h"
  59 #include "theory/arith/linear_equality.h"
  60 #include "theory/arith/simplex.h"
  61 #include "theory/arith/simplex_update.h"
  62 #include "util/dense_map.h"
  63 #include "util/statistics_stats.h"
  64
  65 namespace cvc5 {
  66 namespace theory {
  67 namespace arith {
  68
  69 class FCSimplexDecisionProcedure : public SimplexDecisionProcedure{
  70 public:
  71  FCSimplexDecisionProcedure(Env& env,
  72                             LinearEqualityModule& linEq,
  73                             ErrorSet& errors,
  74                             RaiseConflict conflictChannel,
  75                             TempVarMalloc tvmalloc);
  76
  77  Result::Sat findModel(bool exactResult) override;
  78
  79  // other error variables are dropping
  80  WitnessImprovement dualLikeImproveError(ArithVar evar);
  81  WitnessImprovement primalImproveError(ArithVar evar);
  82
  83  // dual like
  84  // - found conflict
  85  // - satisfied error set
  86  Result::Sat dualLike();
  87
  88 private:
  89   static const uint32_t PENALTY = 4;
  90   DenseMultiset d_scores;
  91   void decreasePenalties(){ d_scores.removeOneOfEverything(); }
  92   uint32_t penalty(ArithVar x) const { return d_scores.count(x); }
  93   void setPenalty(ArithVar x, WitnessImprovement w){
  94     if(improvement(w)){
  95       if(d_scores.count(x) > 0){
  96         d_scores.removeAll(x);
  97       }
  98     }else{
  99       d_scores.setCount(x, PENALTY);
 100     }
 101   }
 102
 103   /** The size of the focus set. */
 104   uint32_t d_focusSize;
 105
 106   /** The current error focus variable. */
 107   ArithVar d_focusErrorVar;
 108
 109   /**
 110    * The signs of the coefficients in the focus set.
 111    * This is empty until this has been loaded.
 112    */
 113   DenseMap<const Rational*> d_focusCoefficients;
 114
 115   /**
 116    * Loads the signs of the coefficients of the variables on the row d_focusErrorVar
 117    * into d_focusSgns.
 118    */
 119   void loadFocusSigns();
 120
 121   /** Unloads the information from d_focusSgns. */
 122   void unloadFocusSigns();
 123
 124   /**
 125    * The signs of a variable in the row of d_focusErrorVar.
 126    * d_focusSgns must be loaded.
 127    */
 128   const Rational& focusCoefficient(ArithVar nb) const;
 129
 130   int32_t d_pivotBudget;
 131   // enum PivotImprovement {
 132   //   ErrorDropped,
 133   //   NonDegenerate,
 134   //   HeuristicDegenerate,
 135   //   BlandsDegenerate
 136   // };
 137
 138   WitnessImprovement d_prevWitnessImprovement;
 139   uint32_t d_witnessImprovementInARow;
 140
 141   uint32_t degeneratePivotsInARow() const;
 142
 143   static const uint32_t s_focusThreshold = 6;
 144   static const uint32_t s_maxDegeneratePivotsBeforeBlandsOnLeaving = 100;
 145   static const uint32_t s_maxDegeneratePivotsBeforeBlandsOnEntering = 10;
 146
 147   DenseMap<uint32_t> d_leavingCountSinceImprovement;
 148   void increaseLeavingCount(ArithVar x){
 149     if(!d_leavingCountSinceImprovement.isKey(x)){
 150       d_leavingCountSinceImprovement.set(x,1);
 151     }else{
 152       (d_leavingCountSinceImprovement.get(x))++;
 153     }
 154   }
 155   LinearEqualityModule::UpdatePreferenceFunction selectLeavingFunction(ArithVar x){
 156     bool useBlands = d_leavingCountSinceImprovement.isKey(x) &&
 157       d_leavingCountSinceImprovement[x] >= s_maxDegeneratePivotsBeforeBlandsOnEntering;
 158     if(useBlands) {
 159       return &LinearEqualityModule::preferWitness<false>;
 160     } else {
 161       return &LinearEqualityModule::preferWitness<true>;
 162     }
 163   }
 164
 165   bool debugDualLike(WitnessImprovement w, std::ostream& out,
 166                      int instance,
 167                      uint32_t prevFocusSize, uint32_t prevErrorSize) const;
 168
 169   void debugPrintSignal(ArithVar updated) const;
 170
 171   ArithVarVec d_sgnDisagreements;
 172
 173   //static PivotImprovement pivotImprovement(const UpdateInfo& selected, bool useBlands = false);
 174
 175   void logPivot(WitnessImprovement w);
 176
 177   void updateAndSignal(const UpdateInfo& selected, WitnessImprovement w);
 178
 179   UpdateInfo selectPrimalUpdate(ArithVar error,
 180                                 LinearEqualityModule::UpdatePreferenceFunction upf,
 181                                 LinearEqualityModule::VarPreferenceFunction bpf);
 182
 183
 184   UpdateInfo selectUpdateForDualLike(ArithVar basic){
 185     TimerStat::CodeTimer codeTimer(d_statistics.d_selectUpdateForDualLike);
 186
 187     LinearEqualityModule::UpdatePreferenceFunction upf =
 188       &LinearEqualityModule::preferWitness<true>;
 189     LinearEqualityModule::VarPreferenceFunction bpf =
 190       &LinearEqualityModule::minVarOrder;
 191     return selectPrimalUpdate(basic, upf, bpf);
 192   }
 193
 194   UpdateInfo selectUpdateForPrimal(ArithVar basic, bool useBlands){
 195     TimerStat::CodeTimer codeTimer(d_statistics.d_selectUpdateForPrimal);
 196
 197     LinearEqualityModule::UpdatePreferenceFunction upf;
 198     if(useBlands) {
 199       upf = &LinearEqualityModule::preferWitness<false>;
 200     } else {
 201       upf = &LinearEqualityModule::preferWitness<true>;
 202     }
 203
 204     LinearEqualityModule::VarPreferenceFunction bpf = useBlands ?
 205       &LinearEqualityModule::minVarOrder :
 206       &LinearEqualityModule::minRowLength;
 207
 208     return selectPrimalUpdate(basic, upf, bpf);
 209   }
 210   WitnessImprovement selectFocusImproving() ;
 211
 212   WitnessImprovement focusUsingSignDisagreements(ArithVar basic);
 213   WitnessImprovement focusDownToLastHalf();
 214   WitnessImprovement adjustFocusShrank(const ArithVarVec& drop);
 215   WitnessImprovement focusDownToJust(ArithVar v);
 216
 217
 218   void adjustFocusAndError(const UpdateInfo& up, const AVIntPairVec& focusChanges);
 219
 220   /**
 221    * This is the main simplex for DPLL(T) loop.
 222    * It runs for at most maxIterations.
 223    *
 224    * Returns true iff it has found a conflict.
 225    * d_conflictVariable will be set and the conflict for this row is reported.
 226    */
 227   bool searchForFeasibleSolution(uint32_t maxIterations);
 228
 229   bool initialProcessSignals(){
 230     TimerStat &timer = d_statistics.d_initialSignalsTime;
 231     IntStat& conflictStat  = d_statistics.d_initialConflicts;
 232     bool res = standardProcessSignals(timer, conflictStat);
 233     d_focusSize = d_errorSet.focusSize();
 234     return res;
 235   }
 236
 237   static bool debugCheckWitness(const UpdateInfo& inf, WitnessImprovement w, bool useBlands);
 238
 239   /** These fields are designed to be accessible to TheoryArith methods. */
 240   class Statistics {
 241   public:
 242     TimerStat d_initialSignalsTime;
 243     IntStat d_initialConflicts;
 244
 245     IntStat d_fcFoundUnsat;
 246     IntStat d_fcFoundSat;
 247     IntStat d_fcMissed;
 248
 249     TimerStat d_fcTimer;
 250     TimerStat d_fcFocusConstructionTimer;
 251
 252     TimerStat d_selectUpdateForDualLike;
 253     TimerStat d_selectUpdateForPrimal;
 254
 255     ReferenceStat<uint32_t> d_finalCheckPivotCounter;
 256
 257     Statistics(const std::string& name, uint32_t& pivots);
 258   } d_statistics;
 259 };/* class FCSimplexDecisionProcedure */
 260
 261 }  // namespace arith
 262 }  // namespace theory
 263 }  // namespace cvc5