src/theory/arith/error_set.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Tim King, Mathias Preiner, Morgan Deters
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   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.
  11  * ****************************************************************************
  12  *
  13  * [[ Add one-line brief description here ]]
  14  *
  15  * [[ Add lengthier description here ]]
  16  * \todo document this file
  17  */
  18
  19 #include "cvc5_private.h"
  20
  21 #pragma once
  22
  23 #include <memory>
  24 #include <vector>
  25
  26 #include "options/arith_options.h"
  27 #include "theory/arith/arithvar.h"
  28 #include "theory/arith/bound_counts.h"
  29 #include "theory/arith/callbacks.h"
  30 #include "theory/arith/delta_rational.h"
  31 #include "theory/arith/partial_model.h"
  32 #include "theory/arith/tableau_sizes.h"
  33 #include "util/bin_heap.h"
  34 #include "util/statistics_stats.h"
  35
  36 namespace cvc5 {
  37 namespace theory {
  38 namespace arith {
  39
  40
  41 /**
  42  * The priority queue has 3 different modes of operation:
  43  * - Collection
  44  *   This passively collects arithmetic variables that may be inconsistent.
  45  *   This does not maintain any heap structure.
  46  *   dequeueInconsistentBasicVariable() does not work in this mode!
  47  *   Entering this mode requires the queue to be empty.
  48  *
  49  * - Difference Queue
  50  *   This mode uses the difference between a variables and its bound
  51  *   to determine which to dequeue first.
  52  *
  53  * - Variable Order Queue
  54  *   This mode uses the variable order to determine which ArithVar is dequeued first.
  55  *
  56  * The transitions between the modes of operation are:
  57  *  Collection => Difference Queue
  58  *  Difference Queue => Variable Order Queue
  59  *  Difference Queue => Collection (queue must be empty!)
  60  *  Variable Order Queue => Collection (queue must be empty!)
  61  *
  62  * The queue begins in Collection mode.
  63  */
  64
  65
  66 class ErrorSet;
  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 CVC5_PB_DS_NAMESPACE::priority_queue<
  91 //   ArithVar,
  92 //   ComparatorPivotRule,
  93 //   CVC5_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   std::unique_ptr<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 != nullptr);
 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 == nullptr)
 206     {
 207       os << "nullptr";
 208     }
 209     else
 210     {
 211       os << (*d_amount);
 212     }
 213     os << "}";
 214   }
 215 };
 216
 217 class ErrorInfoMap : public DenseMap<ErrorInformation> {};
 218
 219 class ErrorSet {
 220 private:
 221   /**
 222    * Reference to the arithmetic partial model for checking if a variable
 223    * is consistent with its upper and lower bounds.
 224    */
 225   ArithVariables& d_variables;
 226
 227   /**
 228    * The set of all variables that violate exactly one of their bounds.
 229    */
 230   ErrorInfoMap d_errInfo;
 231
 232   options::ErrorSelectionRule d_selectionRule;
 233   /**
 234    * The ordered heap for the variables that are in ErrorSet.
 235    */
 236   FocusSet d_focus;
 237
 238
 239   /**
 240    * A strict subset of the error set.
 241    *   d_outOfFocus \neq d_errInfo.
 242    *
 243    * Its symbolic complement is Focus.
 244    *   d_outOfFocus \intersect Focus == \emptyset
 245    *   d_outOfFocus \union Focus == d_errInfo
 246    */
 247   ArithVarVec d_outOfFocus;
 248
 249   /**
 250    * Before a variable is added to the error set, it is added to the signals list.
 251    * A variable may appear on the list multiple times.
 252    * This introduces a delay.
 253    */
 254   ArithVarVec d_signals;
 255
 256   TableauSizes d_tableauSizes;
 257
 258   BoundCountingLookup d_boundLookup;
 259
 260   /**
 261    * Computes the difference between the assignment and its bound for x.
 262    */
 263 public:
 264   DeltaRational computeDiff(ArithVar x) const;
 265 private:
 266  void recomputeAmount(ErrorInformation& ei, options::ErrorSelectionRule r);
 267
 268  void update(ErrorInformation& ei);
 269  void transitionVariableOutOfError(ArithVar v);
 270  void transitionVariableIntoError(ArithVar v);
 271  void addBackIntoFocus(ArithVar v);
 272
 273 public:
 274
 275   /** The new focus set is the entire error set. */
 276   void blur();
 277   void dropFromFocus(ArithVar v);
 278
 279   void dropFromFocusAll(const ArithVarVec& vec) {
 280     for(ArithVarVec::const_iterator i = vec.begin(), i_end = vec.end(); i != i_end; ++i){
 281       ArithVar v = *i;
 282       dropFromFocus(v);
 283     }
 284   }
 285
 286   ErrorSet(ArithVariables& var, TableauSizes tabSizes, BoundCountingLookup boundLookup);
 287
 288   typedef ErrorInfoMap::const_iterator error_iterator;
 289   error_iterator errorBegin() const { return d_errInfo.begin(); }
 290   error_iterator errorEnd() const { return d_errInfo.end(); }
 291
 292   bool inError(ArithVar v) const { return d_errInfo.isKey(v); }
 293   bool inFocus(ArithVar v) const { return d_errInfo[v].inFocus(); }
 294
 295   void pushErrorInto(ArithVarVec& vec) const;
 296   void pushFocusInto(ArithVarVec& vec) const;
 297
 298   options::ErrorSelectionRule getSelectionRule() const;
 299   void setSelectionRule(options::ErrorSelectionRule rule);
 300
 301   inline ArithVar topFocusVariable() const{
 302     Assert(!focusEmpty());
 303     return d_focus.top();
 304   }
 305
 306   inline void signalVariable(ArithVar var){
 307     d_signals.push_back(var);
 308   }
 309
 310   inline void signalUnderCnd(ArithVar var, bool b){
 311     if(b){ signalVariable(var); }
 312   }
 313
 314   inline bool inconsistent(ArithVar var) const{
 315     return !d_variables.assignmentIsConsistent(var) ;
 316   }
 317   inline void signalIfInconsistent(ArithVar var){
 318     signalUnderCnd(var, inconsistent(var));
 319   }
 320
 321   inline bool errorEmpty() const{
 322     return d_errInfo.empty();
 323   }
 324   inline uint32_t errorSize() const{
 325     return d_errInfo.size();
 326   }
 327
 328   inline bool focusEmpty() const {
 329     return d_focus.empty();
 330   }
 331   inline uint32_t focusSize() const{
 332     return d_focus.size();
 333   }
 334
 335   inline int getSgn(ArithVar x) const {
 336     Assert(inError(x));
 337     return d_errInfo[x].sgn();
 338   }
 339   inline int focusSgn(ArithVar v) const {
 340     if(inError(v)){
 341       return d_errInfo[v].focusSgn();
 342     }else{
 343       return 0;
 344     }
 345   }
 346
 347   void focusDownToJust(ArithVar v);
 348
 349   void clearFocus();
 350
 351   /** Clears the set. */
 352   void clear();
 353   void reduceToSignals();
 354
 355   bool noSignals() const {
 356     return d_signals.empty();
 357   }
 358   bool moreSignals() const {
 359     return !noSignals();
 360   }
 361   ArithVar topSignal() const {
 362     Assert(moreSignals());
 363     return d_signals.back();
 364   }
 365
 366   /**
 367    * Moves a variable out of the signals.
 368    * This moves it into the error set.
 369    * Return the previous focus sign.
 370    */
 371   int popSignal();
 372
 373   const DeltaRational& getAmount(ArithVar v) const {
 374     return d_errInfo[v].getAmount();
 375   }
 376
 377   uint32_t sumMetric(ArithVar a) const{
 378     Assert(inError(a));
 379     BoundCounts bcs = d_boundLookup.atBounds(a);
 380     uint32_t count = getSgn(a) > 0 ? bcs.upperBoundCount() : bcs.lowerBoundCount();
 381
 382     uint32_t length = d_tableauSizes.getRowLength(a);
 383
 384     return (length - count);
 385   }
 386
 387   uint32_t getMetric(ArithVar a) const {
 388     return d_errInfo[a].getMetric();
 389   }
 390
 391   ConstraintP getViolated(ArithVar a) const {
 392     return d_errInfo[a].getViolated();
 393   }
 394
 395
 396   typedef FocusSet::const_iterator focus_iterator;
 397   focus_iterator focusBegin() const { return d_focus.begin(); }
 398   focus_iterator focusEnd() const { return d_focus.end(); }
 399
 400   void debugPrint(std::ostream& out) const;
 401
 402 private:
 403   class Statistics {
 404   public:
 405     IntStat d_enqueues;
 406     IntStat d_enqueuesCollection;
 407     IntStat d_enqueuesDiffMode;
 408     IntStat d_enqueuesVarOrderMode;
 409
 410     IntStat d_enqueuesCollectionDuplicates;
 411     IntStat d_enqueuesVarOrderModeDuplicates;
 412
 413     Statistics();
 414   };
 415
 416   Statistics d_statistics;
 417 };
 418
 419 }  // namespace arith
 420 }  // namespace theory
 421 }  // namespace cvc5