src/theory/arith/simplex_update.h

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