src/theory/arith/error_set.h

   1 /*********************                                                        */
   2 /*! \file error_set.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Tim King, Mathias Preiner, Morgan Deters
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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 [[ Add one-line brief description here ]]
  13  **
  14  ** [[ Add lengthier description here ]]
  15  ** \todo document this file
  16  **/
  17
  18
  19 #include "cvc4_private.h"
  20
  21 #pragma once
  22
  23 #include <vector>
  24
  25 #include "options/arith_options.h"
  26 #include "theory/arith/arithvar.h"
  27 #include "theory/arith/bound_counts.h"
  28 #include "theory/arith/callbacks.h"
  29 #include "theory/arith/delta_rational.h"
  30 #include "theory/arith/partial_model.h"
  31 #include "theory/arith/tableau_sizes.h"
  32 #include "util/bin_heap.h"
  33 #include "util/statistics_registry.h"
  34
  35 namespace CVC4 {
  36 namespace theory {
  37 namespace arith {
  38
  39
  40 /**
  41  * The priority queue has 3 different modes of operation:
  42  * - Collection
  43  *   This passively collects arithmetic variables that may be inconsistent.
  44  *   This does not maintain any heap structure.
  45  *   dequeueInconsistentBasicVariable() does not work in this mode!
  46  *   Entering this mode requires the queue to be empty.
  47  *
  48  * - Difference Queue
  49  *   This mode uses the difference between a variables and its bound
  50  *   to determine which to dequeue first.
  51  *
  52  * - Variable Order Queue
  53  *   This mode uses the variable order to determine which ArithVar is dequeued first.
  54  *
  55  * The transitions between the modes of operation are:
  56  *  Collection => Difference Queue
  57  *  Difference Queue => Variable Order Queue
  58  *  Difference Queue => Collection (queue must be empty!)
  59  *  Variable Order Queue => Collection (queue must be empty!)
  60  *
  61  * The queue begins in Collection mode.
  62  */
  63
  64
  65 class ErrorSet;
  66 class ErrorInfoMap;
  67
  68 class ComparatorPivotRule {
  69 private:
  70   const ErrorSet* d_errorSet;
  71
  72   options::ErrorSelectionRule d_rule;
  73
  74  public:
  75   ComparatorPivotRule();
  76   ComparatorPivotRule(const ErrorSet* es, options::ErrorSelectionRule r);
  77
  78   bool operator()(ArithVar v, ArithVar u) const;
  79   options::ErrorSelectionRule getRule() const { return d_rule; }
  80 };
  81
  82 // typedef boost::heap::d_ary_heap<
  83 //   ArithVar,
  84 //   boost::heap::arity<2>,
  85 //   boost::heap::compare<ComparatorPivotRule>,
  86 //   boost::heap::mutable_<true> > FocusSet;
  87 //
  88 // typedef FocusSet::handle_type FocusSetHandle;
  89
  90 // typedef CVC4_PB_DS_NAMESPACE::priority_queue<
  91 //   ArithVar,
  92 //   ComparatorPivotRule,
  93 //   CVC4_PB_DS_NAMESPACE::pairing_heap_tag> FocusSet;
  94
  95 // typedef FocusSet::point_iterator FocusSetHandle;
  96
  97 typedef BinaryHeap<ArithVar, ComparatorPivotRule> FocusSet;
  98 typedef FocusSet::handle FocusSetHandle;
  99
 100
 101 class ErrorInformation {
 102 private:
 103   /** The variable that is in error. */
 104   ArithVar d_variable;
 105
 106   /**
 107    * The constraint that was violated.
 108    * This needs to be saved in case that the
 109    * violated constraint
 110    */
 111   ConstraintP d_violated;
 112
 113   /**
 114    * This is the sgn of the first derivate the variable must move to satisfy
 115    * the bound violated.
 116    * If d_sgn > 0, then d_violated was a lowerbound.
 117    * If d_sgn < 0, then d_violated was an upperbound.
 118    */
 119   int d_sgn;
 120
 121   /**
 122    * If this is true, then the bound is no longer set on d_variables.
 123    * This MUST be undone before this is deleted.
 124    */
 125   bool d_relaxed;
 126
 127   /**
 128    * If this is true, then the variable is in the focus set and the focus heap.
 129    * d_handle is then a reasonable thing to interpret.
 130    * If this is false, the variable is somewhere in
 131    */
 132   bool d_inFocus;
 133   FocusSetHandle d_handle;
 134
 135   /**
 136    * Auxillary information for storing the difference between a variable and its bound.
 137    * Only set on signals.
 138    */
 139   DeltaRational* d_amount;
 140
 141   /** */
 142   uint32_t d_metric;
 143
 144 public:
 145   ErrorInformation();
 146   ErrorInformation(ArithVar var, ConstraintP vio, int sgn);
 147   ~ErrorInformation();
 148   ErrorInformation(const ErrorInformation& ei);
 149   ErrorInformation& operator=(const ErrorInformation& ei);
 150
 151   void reset(ConstraintP c, int sgn);
 152
 153   inline ArithVar getVariable() const { return d_variable; }
 154
 155   bool isRelaxed() const { return d_relaxed; }
 156   void setRelaxed()
 157   {
 158     Assert(!d_relaxed);
 159     d_relaxed = true;
 160   }
 161   void setUnrelaxed()
 162   {
 163     Assert(d_relaxed);
 164     d_relaxed = false;
 165   }
 166
 167   inline int sgn() const { return d_sgn; }
 168
 169   inline bool inFocus() const { return d_inFocus; }
 170   inline int focusSgn() const {
 171     return (d_inFocus) ? sgn() : 0;
 172   }
 173
 174   inline void setInFocus(bool inFocus) { d_inFocus = inFocus; }
 175
 176   const DeltaRational& getAmount() const {
 177     Assert(d_amount != NULL);
 178     return *d_amount;
 179   }
 180
 181   void setAmount(const DeltaRational& am);
 182   void setMetric(uint32_t m) { d_metric = m; }
 183   uint32_t getMetric() const { return d_metric; }
 184
 185   inline void setHandle(FocusSetHandle h) {
 186     Assert(d_inFocus);
 187     d_handle = h;
 188   }
 189   inline const FocusSetHandle& getHandle() const{ return d_handle; }
 190
 191   inline ConstraintP getViolated() const { return d_violated; }
 192
 193   bool debugInitialized() const {
 194     return
 195       d_variable != ARITHVAR_SENTINEL &&
 196       d_violated != NullConstraint &&
 197       d_sgn != 0;
 198   }
 199   void print(std::ostream& os) const {
 200     os << "{ErrorInfo: " << d_variable
 201        << ", " << d_violated
 202        << ", " << d_sgn
 203        << ", " << d_relaxed
 204        << ", " << d_inFocus;
 205     if(d_amount == NULL){
 206       os << "NULL";
 207     }else{
 208       os << (*d_amount);
 209     }
 210     os << "}";
 211   }
 212 };
 213
 214 class ErrorInfoMap : public DenseMap<ErrorInformation> {};
 215
 216 class ErrorSet {
 217 private:
 218   /**
 219    * Reference to the arithmetic partial model for checking if a variable
 220    * is consistent with its upper and lower bounds.
 221    */
 222   ArithVariables& d_variables;
 223
 224   /**
 225    * The set of all variables that violate exactly one of their bounds.
 226    */
 227   ErrorInfoMap d_errInfo;
 228
 229   options::ErrorSelectionRule d_selectionRule;
 230   /**
 231    * The ordered heap for the variables that are in ErrorSet.
 232    */
 233   FocusSet d_focus;
 234
 235
 236   /**
 237    * A strict subset of the error set.
 238    *   d_outOfFocus \neq d_errInfo.
 239    *
 240    * Its symbolic complement is Focus.
 241    *   d_outOfFocus \intersect Focus == \emptyset
 242    *   d_outOfFocus \union Focus == d_errInfo
 243    */
 244   ArithVarVec d_outOfFocus;
 245
 246   /**
 247    * Before a variable is added to the error set, it is added to the signals list.
 248    * A variable may appear on the list multiple times.
 249    * This introduces a delay.
 250    */
 251   ArithVarVec d_signals;
 252
 253   TableauSizes d_tableauSizes;
 254
 255   BoundCountingLookup d_boundLookup;
 256
 257   /**
 258    * Computes the difference between the assignment and its bound for x.
 259    */
 260 public:
 261   DeltaRational computeDiff(ArithVar x) const;
 262 private:
 263  void recomputeAmount(ErrorInformation& ei, options::ErrorSelectionRule r);
 264
 265  void update(ErrorInformation& ei);
 266  void transitionVariableOutOfError(ArithVar v);
 267  void transitionVariableIntoError(ArithVar v);
 268  void addBackIntoFocus(ArithVar v);
 269
 270 public:
 271
 272   /** The new focus set is the entire error set. */
 273   void blur();
 274   void dropFromFocus(ArithVar v);
 275
 276   void dropFromFocusAll(const ArithVarVec& vec) {
 277     for(ArithVarVec::const_iterator i = vec.begin(), i_end = vec.end(); i != i_end; ++i){
 278       ArithVar v = *i;
 279       dropFromFocus(v);
 280     }
 281   }
 282
 283   ErrorSet(ArithVariables& var, TableauSizes tabSizes, BoundCountingLookup boundLookup);
 284
 285   typedef ErrorInfoMap::const_iterator error_iterator;
 286   error_iterator errorBegin() const { return d_errInfo.begin(); }
 287   error_iterator errorEnd() const { return d_errInfo.end(); }
 288
 289   bool inError(ArithVar v) const { return d_errInfo.isKey(v); }
 290   bool inFocus(ArithVar v) const { return d_errInfo[v].inFocus(); }
 291
 292   void pushErrorInto(ArithVarVec& vec) const;
 293   void pushFocusInto(ArithVarVec& vec) const;
 294
 295   options::ErrorSelectionRule getSelectionRule() const;
 296   void setSelectionRule(options::ErrorSelectionRule rule);
 297
 298   inline ArithVar topFocusVariable() const{
 299     Assert(!focusEmpty());
 300     return d_focus.top();
 301   }
 302
 303   inline void signalVariable(ArithVar var){
 304     d_signals.push_back(var);
 305   }
 306
 307   inline void signalUnderCnd(ArithVar var, bool b){
 308     if(b){ signalVariable(var); }
 309   }
 310
 311   inline bool inconsistent(ArithVar var) const{
 312     return !d_variables.assignmentIsConsistent(var) ;
 313   }
 314   inline void signalIfInconsistent(ArithVar var){
 315     signalUnderCnd(var, inconsistent(var));
 316   }
 317
 318   inline bool errorEmpty() const{
 319     return d_errInfo.empty();
 320   }
 321   inline uint32_t errorSize() const{
 322     return d_errInfo.size();
 323   }
 324
 325   inline bool focusEmpty() const {
 326     return d_focus.empty();
 327   }
 328   inline uint32_t focusSize() const{
 329     return d_focus.size();
 330   }
 331
 332   inline int getSgn(ArithVar x) const {
 333     Assert(inError(x));
 334     return d_errInfo[x].sgn();
 335   }
 336   inline int focusSgn(ArithVar v) const {
 337     if(inError(v)){
 338       return d_errInfo[v].focusSgn();
 339     }else{
 340       return 0;
 341     }
 342   }
 343
 344   void focusDownToJust(ArithVar v);
 345
 346   void clearFocus();
 347
 348   /** Clears the set. */
 349   void clear();
 350   void reduceToSignals();
 351
 352   bool noSignals() const {
 353     return d_signals.empty();
 354   }
 355   bool moreSignals() const {
 356     return !noSignals();
 357   }
 358   ArithVar topSignal() const {
 359     Assert(moreSignals());
 360     return d_signals.back();
 361   }
 362
 363   /**
 364    * Moves a variable out of the signals.
 365    * This moves it into the error set.
 366    * Return the previous focus sign.
 367    */
 368   int popSignal();
 369
 370   const DeltaRational& getAmount(ArithVar v) const {
 371     return d_errInfo[v].getAmount();
 372   }
 373
 374   uint32_t sumMetric(ArithVar a) const{
 375     Assert(inError(a));
 376     BoundCounts bcs = d_boundLookup.atBounds(a);
 377     uint32_t count = getSgn(a) > 0 ? bcs.upperBoundCount() : bcs.lowerBoundCount();
 378
 379     uint32_t length = d_tableauSizes.getRowLength(a);
 380
 381     return (length - count);
 382   }
 383
 384   uint32_t getMetric(ArithVar a) const {
 385     return d_errInfo[a].getMetric();
 386   }
 387
 388   ConstraintP getViolated(ArithVar a) const {
 389     return d_errInfo[a].getViolated();
 390   }
 391
 392
 393   typedef FocusSet::const_iterator focus_iterator;
 394   focus_iterator focusBegin() const { return d_focus.begin(); }
 395   focus_iterator focusEnd() const { return d_focus.end(); }
 396
 397   void debugPrint(std::ostream& out) const;
 398
 399 private:
 400   class Statistics {
 401   public:
 402     IntStat d_enqueues;
 403     IntStat d_enqueuesCollection;
 404     IntStat d_enqueuesDiffMode;
 405     IntStat d_enqueuesVarOrderMode;
 406
 407     IntStat d_enqueuesCollectionDuplicates;
 408     IntStat d_enqueuesVarOrderModeDuplicates;
 409
 410     Statistics();
 411     ~Statistics();
 412   };
 413
 414   Statistics d_statistics;
 415 };
 416
 417 }/* CVC4::theory::arith namespace */
 418 }/* CVC4::theory namespace */
 419 }/* CVC4 namespace */