src/theory/arith/fc_simplex.h

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