src/theory/arith/simplex_update.h

   1 /*********************                                                        */
   2 /*! \file simplex_update.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-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.\endverbatim
  11  **
  12  ** \brief This provides a class for summarizing pivot proposals.
  13  **
  14  ** This shares with the theory a Tableau, and a PartialModel that:
  15  **  - satisfies the equalities in the Tableau, and
  16  **  - the assignment for the non-basic variables satisfies their bounds.
  17  ** This maintains the relationship needed by the SimplexDecisionProcedure.
  18  **
  19  ** In the language of Simplex for DPLL(T), this provides:
  20  ** - update()
  21  ** - pivotAndUpdate()
  22  **
  23  ** This class also provides utility functions that require
  24  ** using both the Tableau and PartialModel.
  25  **/
  26
  27 #include "cvc4_private.h"
  28
  29 #pragma once
  30
  31 #include "theory/arith/delta_rational.h"
  32 #include "theory/arith/arithvar.h"
  33 #include "theory/arith/constraint_forward.h"
  34 #include "util/maybe.h"
  35
  36 namespace cvc5 {
  37 namespace theory {
  38 namespace arith {
  39
  40 enum WitnessImprovement {
  41   ConflictFound = 0,
  42   ErrorDropped = 1,
  43   FocusImproved = 2,
  44   FocusShrank = 3,
  45   Degenerate = 4,
  46   BlandsDegenerate = 5,
  47   HeuristicDegenerate = 6,
  48   AntiProductive = 7
  49 };
  50
  51 inline bool strongImprovement(WitnessImprovement w){
  52   return w <= FocusImproved;
  53 }
  54
  55 inline bool improvement(WitnessImprovement w){
  56   return w <= FocusShrank;
  57 }
  58
  59 inline bool degenerate(WitnessImprovement w){
  60   switch(w){
  61   case Degenerate:
  62   case BlandsDegenerate:
  63   case HeuristicDegenerate:
  64     return true;
  65   default:
  66     return false;
  67   }
  68 }
  69
  70 std::ostream& operator<<(std::ostream& out,  WitnessImprovement w);
  71
  72 /**
  73  * This class summarizes both potential:
  74  * - pivot-and-update operations or
  75  * - a pure update operation.
  76  * This stores enough information for the various algorithms  hat consider these operations.
  77  * These require slightly different pieces of information at different points
  78  * so they are a bit verbose and paranoid.
  79  */
  80 class UpdateInfo {
  81 private:
  82
  83   /**
  84    * The nonbasic variables under consideration.
  85    * This is either the entering variable on a pivot and update
  86    * or the variable being updated.
  87    * This can only be set in the constructor or assignment.
  88    *
  89    * If this uninitialized, then this is ARITHVAR_SENTINEL.
  90    */
  91   ArithVar d_nonbasic;
  92
  93   /**
  94    * The sgn of the "intended" derivative (delta) of the update to d_nonbasic.
  95    * This is either 1, -1, or 0.
  96    * It is "intended" as the delta is always allowed to be 0.
  97    * (See debugSgnAgreement().)
  98    *
  99    * If this uninitialized, then this is 0.
 100    * If this is initialized, then it is -1 or 1.
 101    *
 102    * This can only be set in the constructor or assignment.
 103    */
 104   int d_nonbasicDirection;
 105
 106   /**
 107    * The change in the assignment of d_nonbasic.
 108    * This is changed via the updateProposal(...) methods.
 109    * The value needs to satisfy debugSgnAgreement() or it is in conflict.
 110    */
 111   Maybe<DeltaRational> d_nonbasicDelta;
 112
 113   /**
 114    * This is true if the pivot-and-update is *known* to cause a conflict.
 115    * This can only be true if it was constructed through the static conflict(...) method.
 116    */
 117   bool d_foundConflict;
 118
 119   /** This is the change in the size of the error set. */
 120   Maybe<int> d_errorsChange;
 121
 122   /** This is the sgn of the change in the value of the focus set.*/
 123   Maybe<int> d_focusDirection;
 124
 125   /** This is the sgn of the change in the value of the focus set.*/
 126   Maybe<DeltaRational> d_focusChange;
 127
 128   /** This is the coefficient in the tableau for the entry.*/
 129   Maybe<const Rational*> d_tableauCoefficient;
 130
 131   /**
 132    * This is the constraint that nonbasic is basic is updating s.t. its variable is against it.
 133    * This has 3 different possibilities:
 134    * - Unbounded : then this is NullConstraint and unbounded() is true.
 135    * - Pivot-And-Update: then this is not NullConstraint and the variable is not d_nonbasic.
 136    * - Update: then this is not NullConstraint and the variable is d_nonbasic.
 137    */
 138   ConstraintP d_limiting;
 139
 140   WitnessImprovement d_witness;
 141
 142   /**
 143    * This returns true if
 144    * d_nonbasicDelta is zero() or its sgn() must agree with d_nonbasicDirection.
 145    */
 146   bool debugSgnAgreement() const {
 147     int deltaSgn = d_nonbasicDelta.value().sgn();
 148     return deltaSgn == 0 || deltaSgn == d_nonbasicDirection;
 149   }
 150
 151   /** This private constructor allows for setting conflict to true. */
 152   UpdateInfo(bool conflict, ArithVar nb, const DeltaRational& delta, const Rational& r, ConstraintP lim);
 153
 154 public:
 155
 156   /** This constructs an uninitialized UpdateInfo. */
 157   UpdateInfo();
 158
 159   /**
 160    * This constructs an initialized UpdateInfo.
 161    * dir must be 1 or -1.
 162    */
 163   UpdateInfo(ArithVar nb, int dir);
 164
 165   /**
 166    * This updates the nonBasicDelta to d and limiting to NullConstraint.
 167    * This describes an unbounded() update.
 168    */
 169   void updateUnbounded(const DeltaRational& d, int ec, int f);
 170
 171
 172   void updatePureFocus(const DeltaRational& d, ConstraintP c);
 173   //void updatePureError(const DeltaRational& d, Constraint c, int e);
 174   //void updatePure(const DeltaRational& d, Constraint c, int e, int f);
 175
 176   /**
 177    * This updates the nonBasicDelta to d and limiting to c.
 178    * This clears errorChange() and focusDir().
 179    */
 180   void updatePivot(const DeltaRational& d, const Rational& r,  ConstraintP c);
 181
 182   /**
 183    * This updates the nonBasicDelta to d, limiting to c, and errorChange to e.
 184    * This clears focusDir().
 185    */
 186   void updatePivot(const DeltaRational& d, const Rational& r, ConstraintP c, int e);
 187
 188   /**
 189    * This updates the nonBasicDelta to d, limiting to c, errorChange to e and
 190    * focusDir to f.
 191    */
 192   void witnessedUpdate(const DeltaRational& d, ConstraintP c, int e, int f);
 193   void update(const DeltaRational& d, const Rational& r, ConstraintP c, int e, int f);
 194
 195
 196   static UpdateInfo conflict(ArithVar nb, const DeltaRational& delta, const Rational& r, ConstraintP lim);
 197
 198   inline ArithVar nonbasic() const { return d_nonbasic; }
 199   inline bool uninitialized() const {
 200     return d_nonbasic == ARITHVAR_SENTINEL;
 201   }
 202
 203   /**
 204    * There is no limiting value to the improvement of the focus.
 205    * If this is true, this never describes an update.
 206    */
 207   inline bool unbounded() const {
 208     return d_limiting == NullConstraint;
 209   }
 210
 211   /**
 212    * The update either describes a pivotAndUpdate operation
 213    * or it describes just an update.
 214    */
 215   bool describesPivot() const;
 216
 217   /** Returns the . describesPivot() must be true. */
 218   ArithVar leaving() const;
 219
 220   /**
 221    * Returns true if this is *known* to find a conflict.
 222    * If true, this must have been made through the static conflict(...) function.
 223    */
 224   bool foundConflict() const { return d_foundConflict; }
 225
 226   /** Returns the direction nonbasic is supposed to move. */
 227   inline int nonbasicDirection() const{  return d_nonbasicDirection; }
 228
 229   /** Requires errorsChange to be set through setErrorsChange or updateProposal. */
 230   inline int errorsChange() const { return d_errorsChange.value(); }
 231
 232   /**
 233    * If errorsChange has been set, return errorsChange().
 234    * Otherwise, return def.
 235    */
 236   inline int errorsChangeSafe(int def) const {
 237     if (d_errorsChange)
 238     {
 239       return d_errorsChange.value();
 240     }
 241     else
 242     {
 243       return def;
 244     }
 245   }
 246
 247   /** Sets the errorChange. */
 248   void setErrorsChange(int ec){
 249     d_errorsChange = ec;
 250     updateWitness();
 251   }
 252
 253
 254   /** Requires errorsChange to be set through setErrorsChange or updateProposal. */
 255   inline int focusDirection() const { return d_focusDirection.value(); }
 256
 257   /** Sets the focusDirection. */
 258   void setFocusDirection(int fd){
 259     Assert(-1 <= fd && fd <= 1);
 260     d_focusDirection = fd;
 261     updateWitness();
 262   }
 263
 264   /**
 265    * nonbasicDirection must be the same as the sign for the focus function's
 266    * coefficient for this to be safe.
 267    * The burden for this being safe is on the user!
 268    */
 269   void determineFocusDirection(){
 270     const int deltaSgn = d_nonbasicDelta.value().sgn();
 271     setFocusDirection(deltaSgn * d_nonbasicDirection);
 272   }
 273
 274   /** Requires nonbasicDelta to be set through updateProposal(...). */
 275   const DeltaRational& nonbasicDelta() const { return d_nonbasicDelta.value(); }
 276   const Rational& getCoefficient() const {
 277     Assert(describesPivot());
 278     Assert(d_tableauCoefficient.value() != NULL);
 279     return *(d_tableauCoefficient.value());
 280   }
 281   int basicDirection() const {
 282     return nonbasicDirection() * (getCoefficient().sgn());
 283   }
 284
 285   /** Returns the limiting constraint. */
 286   inline ConstraintP limiting() const {
 287     return d_limiting;
 288   }
 289
 290   WitnessImprovement getWitness(bool useBlands = false) const{
 291     Assert(d_witness == computeWitness());
 292
 293     if(d_witness == Degenerate){
 294       if(useBlands){
 295         return BlandsDegenerate;
 296       }else{
 297         return HeuristicDegenerate;
 298       }
 299     }else{
 300       return d_witness;
 301     }
 302   }
 303
 304   const DeltaRational& focusChange() const { return d_focusChange.value(); }
 305   void setFocusChange(const DeltaRational& fc) {
 306     d_focusChange = fc;
 307   }
 308
 309   /** Outputs the UpdateInfo into out. */
 310   void output(std::ostream& out) const;
 311
 312 private:
 313   void updateWitness() {
 314     d_witness = computeWitness();
 315     Assert(describesPivot() || improvement(d_witness));
 316   }
 317
 318   /**
 319    * Determines the appropriate WitnessImprovement for the update.
 320    * useBlands breaks ties for degenerate pivots.
 321    *
 322    * This is safe if:
 323    * - d_foundConflict is true, or
 324    * - d_foundConflict is false and d_errorsChange has been set and d_errorsChange < 0, or
 325    * - d_foundConflict is false and d_errorsChange has been set and d_errorsChange >= 0 and d_focusDirection has been set.
 326    */
 327   WitnessImprovement computeWitness() const {
 328     if(d_foundConflict){
 329       return ConflictFound;
 330     }
 331     else if (d_errorsChange.just() && d_errorsChange.value() < 0)
 332     {
 333       return ErrorDropped;
 334     }
 335     else if (d_errorsChange.nothing() || d_errorsChange.value() == 0)
 336     {
 337       if(d_focusDirection.just()){
 338         if (d_focusDirection.value() > 0)
 339         {
 340           return FocusImproved;
 341         }
 342         else if (d_focusDirection.value() == 0)
 343         {
 344           return Degenerate;
 345         }
 346       }
 347     }
 348     return AntiProductive;
 349   }
 350
 351 };
 352
 353 std::ostream& operator<<(std::ostream& out, const UpdateInfo& up);
 354
 355 }  // namespace arith
 356 }  // namespace theory
 357 }  // namespace cvc5