src/theory/arith/error_set.h

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