text: /*********************                                                        */
  /*! \file error_set.h
   ** \verbatim
   ** Original author: Tim King
   ** Major contributors: none
   ** Minor contributors (to current version): Morgan Deters
   ** This file is part of the CVC4 project.
   ** Copyright (c) 2009-2013  New York University and The University of Iowa
   ** See the file COPYING in the top-level source directory for licensing
   ** information.\endverbatim
   **
   ** \brief [[ Add one-line brief description here ]]
   **
   ** [[ Add lengthier description here ]]
   ** \todo document this file
   **/
  
  
  #include "cvc4_private.h"
  
  #pragma once
  
  #include "theory/arith/arithvar.h"
  #include "theory/arith/bound_counts.h"
  #include "theory/arith/delta_rational.h"
  #include "theory/arith/partial_model.h"
  #include "theory/arith/arith_heuristic_pivot_rule.h"
  #include "theory/arith/tableau_sizes.h"
  #include "theory/arith/callbacks.h"
  
  #include "util/statistics_registry.h"
  
  #if CVC4_GCC_HAS_PB_DS_BUG
     // Unfortunate bug in some older GCCs (e.g., v4.2):
     //   http://gcc.gnu.org/bugzilla/show_bug.cgi?id=36612
     // Requires some header-hacking to work around
  #  define __throw_container_error inline __throw_container_error
  #  define __throw_insert_error inline __throw_insert_error
  #  define __throw_join_error inline __throw_join_error
  #  define __throw_resize_error inline __throw_resize_error
  #  include <ext/pb_ds/exception.hpp>
  #  undef __throw_container_error
  #  undef __throw_insert_error
  #  undef __throw_join_error
  #  undef __throw_resize_error
  #endif /* CVC4_GCC_HAS_PB_DS_BUG */
  
  #include <ext/pb_ds/priority_queue.hpp>
  
  #include <vector>
  
  namespace CVC4 {
  namespace theory {
  namespace arith {
  
  
  /**
   * The priority queue has 3 different modes of operation:
   * - Collection
   *   This passively collects arithmetic variables that may be inconsistent.
   *   This does not maintain any heap structure.
   *   dequeueInconsistentBasicVariable() does not work in this mode!
   *   Entering this mode requires the queue to be empty.
   *
   * - Difference Queue
   *   This mode uses the difference between a variables and its bound
   *   to determine which to dequeue first.
   *
   * - Variable Order Queue
   *   This mode uses the variable order to determine which ArithVar is dequeued first.
   *
   * The transitions between the modes of operation are:
   *  Collection => Difference Queue
   *  Difference Queue => Variable Order Queue
   *  Difference Queue => Collection (queue must be empty!)
   *  Variable Order Queue => Collection (queue must be empty!)
   *
   * The queue begins in Collection mode.
   */
  
  
  class ErrorSet;
  class ErrorInfoMap;
  
  class ComparatorPivotRule {
  private:
    const ErrorSet* d_errorSet;
  
    ErrorSelectionRule d_rule;
  public:
    ComparatorPivotRule();
    ComparatorPivotRule(const ErrorSet* es, ErrorSelectionRule r);
  
    bool operator()(ArithVar v, ArithVar u) const;
    ErrorSelectionRule getRule() const { return d_rule; }
  };
  
  // typedef boost::heap::d_ary_heap<
  //   ArithVar,
  //   boost::heap::arity<2>,
  //   boost::heap::compare<ComparatorPivotRule>,
  //   boost::heap::mutable_<true> > FocusSet;
  //
  // typedef FocusSet::handle_type FocusSetHandle;
  
  typedef CVC4_PB_DS_NAMESPACE::priority_queue<
    ArithVar,
    ComparatorPivotRule,
    CVC4_PB_DS_NAMESPACE::pairing_heap_tag> FocusSet;
  
  typedef FocusSet::point_iterator FocusSetHandle;
  
  class ErrorInformation {
  private:
    /** The variable that is in error. */
    ArithVar d_variable;
  
    /**
     * The constraint that was violated.
     * This needs to be saved in case that the
     * violated constraint
     */
    Constraint d_violated;
  
    /**
     * This is the sgn of the first derivate the variable must move to satisfy
     * the bound violated.
     * If d_sgn > 0, then d_violated was a lowerbound.
     * If d_sgn < 0, then d_violated was an upperbound.
     */
    int d_sgn;
  
    /**
     * If this is true, then the bound is no longer set on d_variables.
     * This MUST be undone before this is deleted.
     */
    bool d_relaxed;
  
    /**
     * If this is true, then the variable is in the focus set and the focus heap.
     * d_handle is then a reasonable thing to interpret.
     * If this is false, the variable is somewhere in
     */
    bool d_inFocus;
    FocusSetHandle d_handle;
  
    /**
     * Auxillary information for storing the difference between a variable and its bound.
     * Only set on signals.
     */
    DeltaRational* d_amount;
  
    /** */
    uint32_t d_metric;
  
  public:
    ErrorInformation();
    ErrorInformation(ArithVar var, Constraint vio, int sgn);
    ~ErrorInformation();
    ErrorInformation(const ErrorInformation& ei);
    ErrorInformation& operator=(const ErrorInformation& ei);
  
    void reset(Constraint c, int sgn);
  
    inline ArithVar getVariable() const { return d_variable; }
  
    bool isRelaxed() const { return d_relaxed; }
    void setRelaxed(){ Assert(!d_relaxed); d_relaxed = true; }
    void setUnrelaxed(){ Assert(d_relaxed); d_relaxed = false; }
  
    inline int sgn() const { return d_sgn; }
  
    inline bool inFocus() const { return d_inFocus; }
    inline int focusSgn() const {
      return (d_inFocus) ? sgn() : 0;
    }
  
    inline void setInFocus(bool inFocus) { d_inFocus = inFocus; }
  
    const DeltaRational& getAmount() const {
      Assert(d_amount != NULL);
      return *d_amount;
    }
  
    void setAmount(const DeltaRational& am);
    void setMetric(uint32_t m) { d_metric = m; }
    uint32_t getMetric() const { return d_metric; }
  
    inline void setHandle(FocusSetHandle h) {
      Assert(d_inFocus);
      d_handle = h;
    }
    inline const FocusSetHandle& getHandle() const{ return d_handle; }
  
    inline Constraint getViolated() const { return d_violated; }
  
    bool debugInitialized() const {
      return
        d_variable != ARITHVAR_SENTINEL &&
        d_violated != NullConstraint &&
        d_sgn != 0;
    }
    void print(std::ostream& os) const {
      os << "{ErrorInfo: " << d_variable
         << ", " << d_violated
         << ", " << d_sgn
         << ", " << d_relaxed
         << ", " << d_inFocus;
      if(d_amount == NULL){
        os << "NULL";
      }else{
        os << (*d_amount);
      }
      os << "}";
    }
  };
  
  class ErrorInfoMap : public DenseMap<ErrorInformation> {};
  
  class ErrorSet {
  private:
    /**
     * Reference to the arithmetic partial model for checking if a variable
     * is consistent with its upper and lower bounds.
     */
    ArithVariables& d_variables;
  
    /**
     * The set of all variables that violate exactly one of their bounds.
     */
    ErrorInfoMap d_errInfo;
  
    ErrorSelectionRule d_selectionRule;
    /**
     * The ordered heap for the variables that are in ErrorSet.
     */
    FocusSet d_focus;
  
  
    /**
     * A strict subset of the error set.
     *   d_outOfFocus \neq d_errInfo.
     *
     * Its symbolic complement is Focus.
     *   d_outOfFocus \intersect Focus == \emptyset
     *   d_outOfFocus \union Focus == d_errInfo
     */
    ArithVarVec d_outOfFocus;
  
    /**
     * Before a variable is added to the error set, it is added to the signals list.
     * A variable may appear on the list multiple times.
     * This introduces a delay.
     */
    ArithVarVec d_signals;
  
    TableauSizes d_tableauSizes;
  
    BoundCountingLookup d_boundLookup;
  
    /**
     * Computes the difference between the assignment and its bound for x.
     */
  public:
    DeltaRational computeDiff(ArithVar x) const;
  private:
    void recomputeAmount(ErrorInformation& ei, ErrorSelectionRule r);
  
    void update(ErrorInformation& ei);
    void transitionVariableOutOfError(ArithVar v);
    void transitionVariableIntoError(ArithVar v);
    void addBackIntoFocus(ArithVar v);
  
  public:
  
    /** The new focus set is the entire error set. */
    void blur();
    void dropFromFocus(ArithVar v);
  
    void dropFromFocusAll(const ArithVarVec& vec) {
      for(ArithVarVec::const_iterator i = vec.begin(), i_end = vec.end(); i != i_end; ++i){
        ArithVar v = *i;
        dropFromFocus(v);
      }
    }
  
    ErrorSet(ArithVariables& var, TableauSizes tabSizes, BoundCountingLookup boundLookup);
  
    typedef ErrorInfoMap::const_iterator error_iterator;
    error_iterator errorBegin() const { return d_errInfo.begin(); }
    error_iterator errorEnd() const { return d_errInfo.end(); }
  
    bool inError(ArithVar v) const { return d_errInfo.isKey(v); }
    bool inFocus(ArithVar v) const { return d_errInfo[v].inFocus(); }
  
    void pushErrorInto(ArithVarVec& vec) const;
    void pushFocusInto(ArithVarVec& vec) const;
  
    ErrorSelectionRule getSelectionRule() const;
    void setSelectionRule(ErrorSelectionRule rule);
  
    inline ArithVar topFocusVariable() const{
      Assert(!focusEmpty());
      return d_focus.top();
    }
  
    inline void signalVariable(ArithVar var){
      d_signals.push_back(var);
    }
  
    inline void signalUnderCnd(ArithVar var, bool b){
      if(b){ signalVariable(var); }
    }
  
    inline bool inconsistent(ArithVar var) const{
      return !d_variables.assignmentIsConsistent(var) ;
    }
    inline void signalIfInconsistent(ArithVar var){
      signalUnderCnd(var, inconsistent(var));
    }
  
    inline bool errorEmpty() const{
      return d_errInfo.empty();
    }
    inline uint32_t errorSize() const{
      return d_errInfo.size();
    }
  
    inline bool focusEmpty() const {
      return d_focus.empty();
    }
    inline uint32_t focusSize() const{
      return d_focus.size();
    }
  
    inline int getSgn(ArithVar x) const {
      Assert(inError(x));
      return d_errInfo[x].sgn();
    }
    inline int focusSgn(ArithVar v) const {
      if(inError(v)){
        return d_errInfo[v].focusSgn();
      }else{
        return 0;
      }
    }
  
    void focusDownToJust(ArithVar v);
  
    void clearFocus();
  
    /** Clears the set. */
    void clear();
    void reduceToSignals();
  
    bool noSignals() const {
      return d_signals.empty();
    }
    bool moreSignals() const {
      return !noSignals();
    }
    ArithVar topSignal() const {
      Assert(moreSignals());
      return d_signals.back();
    }
  
    /**
     * Moves a variable out of the signals.
     * This moves it into the error set.
     * Return the previous focus sign.
     */
    int popSignal();
  
    const DeltaRational& getAmount(ArithVar v) const {
      return d_errInfo[v].getAmount();
    }
  
    uint32_t sumMetric(ArithVar a) const{
      Assert(inError(a));
      BoundCounts bcs = d_boundLookup.atBounds(a);
      uint32_t count = getSgn(a) > 0 ? bcs.upperBoundCount() : bcs.lowerBoundCount();
  
      uint32_t length = d_tableauSizes.getRowLength(a);
  
      return (length - count);
    }
  
    uint32_t getMetric(ArithVar a) const {
      return d_errInfo[a].getMetric();
    }
  
    Constraint getViolated(ArithVar a) const {
      return d_errInfo[a].getViolated();
    }
  
  
    typedef FocusSet::const_iterator focus_iterator;
    focus_iterator focusBegin() const { return d_focus.begin(); }
    focus_iterator focusEnd() const { return d_focus.end(); }
  
    void debugPrint(std::ostream& out) const;
  
  private:
    class Statistics {
    public:
      IntStat d_enqueues;
      IntStat d_enqueuesCollection;
      IntStat d_enqueuesDiffMode;
      IntStat d_enqueuesVarOrderMode;
  
      IntStat d_enqueuesCollectionDuplicates;
      IntStat d_enqueuesVarOrderModeDuplicates;
  
      Statistics();
      ~Statistics();
    };
  
    Statistics d_statistics;
  };
  
  }/* CVC4::theory::arith namespace */
  }/* CVC4::theory namespace */
  }/* CVC4 namespace */
  