src/theory/arith/simplex.h

   1
   2 #include "cvc4_private.h"
   3
   4 #ifndef __CVC4__THEORY__ARITH__SIMPLEX_H
   5 #define __CVC4__THEORY__ARITH__SIMPLEX_H
   6
   7 #include "theory/arith/arith_utilities.h"
   8 #include "theory/arith/arith_priority_queue.h"
   9 #include "theory/arith/arithvar_set.h"
  10 #include "theory/arith/delta_rational.h"
  11 #include "theory/arith/tableau.h"
  12 #include "theory/arith/partial_model.h"
  13 #include "theory/arith/arith_prop_manager.h"
  14
  15 #include "util/options.h"
  16
  17 #include "util/stats.h"
  18
  19 #include <queue>
  20
  21 namespace CVC4 {
  22 namespace theory {
  23 namespace arith {
  24
  25 class SimplexDecisionProcedure {
  26 private:
  27
  28   /**
  29    * Manages information about the assignment and upper and lower bounds on
  30    * variables.
  31    */
  32   ArithPartialModel& d_partialModel;
  33
  34   Tableau& d_tableau;
  35   ArithPriorityQueue d_queue;
  36
  37   ArithPropManager& d_propManager;
  38
  39   ArithVar d_numVariables;
  40
  41   std::queue<Node> d_delayedLemmas;
  42
  43   PermissiveBackArithVarSet d_updatedBounds;
  44   PermissiveBackArithVarSet d_candidateBasics;
  45
  46   Rational d_ZERO;
  47   DeltaRational d_DELTA_ZERO;
  48
  49 public:
  50   SimplexDecisionProcedure(ArithPropManager& propManager,
  51                            ArithPartialModel& pm,
  52                            Tableau& tableau);
  53
  54
  55   /**
  56    * Assert*(n, orig) takes an bound n that is implied by orig.
  57    * and asserts that as a new bound if it is tighter than the current bound
  58    * and updates the value of a basic variable if needed.
  59    *
  60    * orig must be a literal in the SAT solver so that it can be used for
  61    * conflict analysis.
  62    *
  63    * x is the variable getting the new bound,
  64    * c is the value of the new bound.
  65    *
  66    * If this new bound is in conflict with the other bound,
  67    * a node describing this conflict is returned.
  68    * If this new bound is not in conflict, Node::null() is returned.
  69    */
  70   Node AssertLower(ArithVar x, const DeltaRational& c, TNode orig);
  71   Node AssertUpper(ArithVar x, const DeltaRational& c, TNode orig);
  72   Node AssertEquality(ArithVar x, const DeltaRational& c, TNode orig);
  73
  74 private:
  75   /**
  76    * Updates the assignment of a nonbasic variable x_i to v.
  77    * Also updates the assignment of basic variables accordingly.
  78    */
  79   void update(ArithVar x_i, const DeltaRational& v);
  80
  81   /**
  82    * Updates the value of a basic variable x_i to v,
  83    * and then pivots x_i with the nonbasic variable in its row x_j.
  84    * Updates the assignment of the other basic variables accordingly.
  85    */
  86   void pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRational& v);
  87
  88 private:
  89   /**
  90    * A PreferenceFunction takes a const ref to the SimplexDecisionProcedure,
  91    * and 2 ArithVar variables and returns one of the ArithVar variables potentially
  92    * using the internals of the SimplexDecisionProcedure.
  93    *
  94    * Both ArithVar must be non-basic in d_tableau.
  95    */
  96   typedef ArithVar (*PreferenceFunction)(const SimplexDecisionProcedure&, ArithVar, ArithVar);
  97
  98   /**
  99    * minVarOrder is a PreferenceFunction for selecting the smaller of the 2 ArithVars.
 100    * This PreferenceFunction is used during the VarOrder stage of
 101    * updateInconsistentVars.
 102    */
 103   static ArithVar minVarOrder(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y);
 104
 105   /**
 106    * minRowCount is a PreferenceFunction for selecting the variable with the smaller
 107    * row count in the tableau.
 108    *
 109    * This is a hueristic rule and should not be used
 110    * during the VarOrder stage of updateInconsistentVars.
 111    */
 112   static ArithVar minColLength(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y);
 113   /**
 114    * minBoundAndRowCount is a PreferenceFunction for preferring a variable
 115    * without an asserted bound over variables with an asserted bound.
 116    * If both have bounds or both do not have bounds,
 117    * the rule falls back to minRowCount(...).
 118    *
 119    * This is a hueristic rule and should not be used
 120    * during the VarOrder stage of updateInconsistentVars.
 121    */
 122   static ArithVar minBoundAndRowCount(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y);
 123
 124 public:
 125   /**
 126    * Tries to update the assignments of variables such that all of the
 127    * assignments are consistent with their bounds.
 128    *
 129    * This is done by searching through the tableau.
 130    * If all of the variables can be made consistent with their bounds
 131    * Node::null() is returned. Otherwise a minimized conflict is returned.
 132    *
 133    * If a conflict is found, changes to the assignments need to be reverted.
 134    *
 135    * Tableau pivoting is performed so variables may switch from being basic to
 136    * nonbasic and vice versa.
 137    *
 138    * Corresponds to the "check()" procedure in [Cav06].
 139    */
 140   Node updateInconsistentVars();
 141 private:
 142   template <PreferenceFunction> Node searchForFeasibleSolution(uint32_t maxIterations);
 143
 144   enum SearchPeriod {BeforeDiffSearch, DuringDiffSearch, AfterDiffSearch, DuringVarOrderSearch, AfterVarOrderSearch};
 145
 146   Node findConflictOnTheQueue(SearchPeriod period, bool returnFirst = true);
 147
 148
 149   /**
 150    * Given the basic variable x_i,
 151    * this function finds the smallest nonbasic variable x_j in the row of x_i
 152    * in the tableau that can "take up the slack" to let x_i satisfy its bounds.
 153    * This returns ARITHVAR_SENTINEL if none exists.
 154    *
 155    * More formally one of the following conditions must be satisfied:
 156    * -  lowerBound && a_ij < 0 && assignment(x_j) < upperbound(x_j)
 157    * -  lowerBound && a_ij > 0 && assignment(x_j) > lowerbound(x_j)
 158    * - !lowerBound && a_ij > 0 && assignment(x_j) < upperbound(x_j)
 159    * - !lowerBound && a_ij < 0 && assignment(x_j) > lowerbound(x_j)
 160    *
 161    */
 162   template <bool lowerBound, PreferenceFunction>  ArithVar selectSlack(ArithVar x_i);
 163   template <PreferenceFunction pf> ArithVar selectSlackLowerBound(ArithVar x_i) {
 164     return selectSlack<true, pf>(x_i);
 165   }
 166   template <PreferenceFunction pf> ArithVar selectSlackUpperBound(ArithVar x_i) {
 167     return selectSlack<false, pf>(x_i);
 168   }
 169   /**
 170    * Returns the smallest basic variable whose assignment is not consistent
 171    * with its upper and lower bounds.
 172    */
 173   ArithVar selectSmallestInconsistentVar();
 174
 175
 176   /**
 177    * Exports either the explanation of an upperbound or a lower bound
 178    * of the basic variable basic, using the non-basic variables in the row.
 179    */
 180   template <bool upperBound>
 181   void explainNonbasics(ArithVar basic, NodeBuilder<>& output);
 182   void explainNonbasicsLowerBound(ArithVar basic, NodeBuilder<>& output){
 183     explainNonbasics<false>(basic, output);
 184   }
 185   void explainNonbasicsUpperBound(ArithVar basic, NodeBuilder<>& output){
 186     explainNonbasics<true>(basic, output);
 187   }
 188
 189   Node deduceUpperBound(ArithVar basicVar);
 190   Node deduceLowerBound(ArithVar basicVar);
 191
 192   /**
 193    * Given a non-basic variable that is know to not be updatable
 194    * to a consistent value, construct and return a conflict.
 195    * Follows section 4.2 in the CAV06 paper.
 196    */
 197   Node generateConflictAboveUpperBound(ArithVar conflictVar);
 198   Node generateConflictBelowLowerBound(ArithVar conflictVar);
 199
 200 public:
 201   /**
 202    * Checks to make sure the assignment is consistent with the tableau.
 203    * This code is for debugging.
 204    */
 205   void debugCheckTableau();
 206   void debugPivotSimplex(ArithVar x_i, ArithVar x_j);
 207
 208
 209   /**
 210    * Computes the value of a basic variable using the assignments
 211    * of the values of the variables in the basic variable's row tableau.
 212    * This can compute the value using either:
 213    * - the the current assignment (useSafe=false) or
 214    * - the safe assignment (useSafe = true).
 215    */
 216   DeltaRational computeRowValue(ArithVar x, bool useSafe);
 217
 218   bool hasAnyUpdates() { return !d_updatedBounds.empty(); }
 219   void clearUpdates(){
 220     d_updatedBounds.purge();
 221   }
 222   void propagateCandidates();
 223
 224   void increaseMax() {d_numVariables++;}
 225
 226   /** Returns true if the simplex procedure has more delayed lemmas in its queue.*/
 227   bool hasMoreLemmas() const {
 228     return !d_delayedLemmas.empty();
 229   }
 230   /** Returns the next delayed lemmas on the queue.*/
 231   Node popLemma(){
 232     Assert(hasMoreLemmas());
 233     Node lemma = d_delayedLemmas.front();
 234     d_delayedLemmas.pop();
 235     return lemma;
 236   }
 237
 238 private:
 239   /** Adds a lemma to the queue. */
 240   void pushLemma(Node lemma){
 241     d_delayedLemmas.push(lemma);
 242     ++(d_statistics.d_delayedConflicts);
 243   }
 244
 245   /** Adds a conflict as a lemma to the queue. */
 246   void delayConflictAsLemma(Node conflict){
 247    Node negatedConflict = negateConjunctionAsClause(conflict);
 248     pushLemma(negatedConflict);
 249   }
 250
 251   template <bool above>
 252   inline bool isAcceptableSlack(int sgn, ArithVar nonbasic){
 253     return
 254       ( above && sgn < 0 && d_partialModel.strictlyBelowUpperBound(nonbasic)) ||
 255       ( above && sgn > 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)) ||
 256       (!above && sgn > 0 && d_partialModel.strictlyBelowUpperBound(nonbasic)) ||
 257       (!above && sgn < 0 && d_partialModel.strictlyAboveLowerBound(nonbasic));
 258   }
 259
 260   /**
 261    * Checks a basic variable, b, to see if it is in conflict.
 262    * If a conflict is discovered a node summarizing the conflict is returned.
 263    * Otherwise, Node::null() is returned.
 264    */
 265   Node checkBasicForConflict(ArithVar b);
 266
 267   Node weakenConflict(bool aboveUpper, ArithVar basicVar);
 268   TNode weakestExplanation(bool aboveUpper, DeltaRational& surplus, ArithVar v, const Rational& coeff, bool& anyWeakening, ArithVar basic);
 269
 270   void propagateCandidate(ArithVar basic);
 271   bool propagateCandidateBound(ArithVar basic, bool upperBound);
 272
 273   inline bool propagateCandidateLowerBound(ArithVar basic){
 274     return propagateCandidateBound(basic, false);
 275   }
 276   inline bool propagateCandidateUpperBound(ArithVar basic){
 277     return propagateCandidateBound(basic, true);
 278   }
 279
 280   bool hasBounds(ArithVar basic, bool upperBound);
 281   bool hasLowerBounds(ArithVar basic){
 282     return hasBounds(basic, false);
 283   }
 284   bool hasUpperBounds(ArithVar basic){
 285     return hasBounds(basic, true);
 286   }
 287   DeltaRational computeBound(ArithVar basic, bool upperBound);
 288
 289   inline DeltaRational computeLowerBound(ArithVar basic){
 290     return computeBound(basic, false);
 291   }
 292   inline DeltaRational computeUpperBound(ArithVar basic){
 293     return computeBound(basic, true);
 294   }
 295
 296
 297   /** These fields are designed to be accessable to TheoryArith methods. */
 298   class Statistics {
 299   public:
 300     IntStat d_statPivots, d_statUpdates;
 301
 302     IntStat d_statAssertUpperConflicts, d_statAssertLowerConflicts;
 303     IntStat d_statUpdateConflicts;
 304
 305     TimerStat d_findConflictOnTheQueueTime;
 306
 307     IntStat d_attemptBeforeDiffSearch, d_successBeforeDiffSearch;
 308     IntStat d_attemptAfterDiffSearch, d_successAfterDiffSearch;
 309     IntStat d_attemptDuringDiffSearch, d_successDuringDiffSearch;
 310     IntStat d_attemptDuringVarOrderSearch, d_successDuringVarOrderSearch;
 311     IntStat d_attemptAfterVarOrderSearch, d_successAfterVarOrderSearch;
 312
 313     IntStat d_weakeningAttempts, d_weakeningSuccesses, d_weakenings;
 314     TimerStat d_weakenTime;
 315
 316     TimerStat d_boundComputationTime;
 317     IntStat d_boundComputations, d_boundPropagations;
 318
 319     IntStat d_delayedConflicts;
 320
 321     TimerStat d_pivotTime;
 322
 323     AverageStat d_avgNumRowsNotContainingOnUpdate;
 324     AverageStat d_avgNumRowsNotContainingOnPivot;
 325
 326     Statistics();
 327     ~Statistics();
 328   };
 329
 330   Statistics d_statistics;
 331
 332 };/* class SimplexDecisionProcedure */
 333
 334 }/* CVC4::theory::arith namespace */
 335 }/* CVC4::theory namespace */
 336 }/* CVC4 namespace */
 337
 338 #endif /* __CVC4__THEORY__ARITH__SIMPLEX_H */
 339