/******************************************************************************

 * Top contributors (to current version):

 *   Tim King, Mathias Preiner, Morgan Deters

 *

 * This file is part of the cvc5 project.

 *

 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS

 * in the top-level source directory and their institutional affiliations.

 * All rights reserved.  See the file COPYING in the top-level source

 * directory for licensing information.

 * ****************************************************************************

 *

 * [[ Add one-line brief description here ]]

 *

 * [[ Add lengthier description here ]]

 * \todo document this file

 */

#include "cvc5_private.h"

#pragma once

#include <vector>

#include "options/arith_options.h"

#include "theory/arith/arithvar.h"

#include "theory/arith/bound_counts.h"

#include "theory/arith/callbacks.h"

#include "theory/arith/delta_rational.h"

#include "theory/arith/partial_model.h"

#include "theory/arith/tableau_sizes.h"

#include "util/bin_heap.h"

#include "util/statistics_stats.h"

namespace cvc5 {

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 ComparatorPivotRule {

private:

  const ErrorSet* d_errorSet;

  options::ErrorSelectionRule d_rule;

 public:

  ComparatorPivotRule();

  ComparatorPivotRule(const ErrorSet* es, options::ErrorSelectionRule r);

  bool operator()(ArithVar v, ArithVar u) const;

  options::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 CVC5_PB_DS_NAMESPACE::priority_queue<

//   ArithVar,

//   ComparatorPivotRule,

//   CVC5_PB_DS_NAMESPACE::pairing_heap_tag> FocusSet;

// typedef FocusSet::point_iterator FocusSetHandle;

typedef BinaryHeap<ArithVar, ComparatorPivotRule> FocusSet;

typedef FocusSet::handle 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

   */

  ConstraintP 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, ConstraintP vio, int sgn);

  ~ErrorInformation();

  ErrorInformation(const ErrorInformation& ei);

  ErrorInformation& operator=(const ErrorInformation& ei);

  void reset(ConstraintP c, int sgn);

  void setRelaxed()

  {

    Assert(!d_relaxed);

    d_relaxed = true;

  }

  {

  }

  }

  void setAmount(const DeltaRational& am);

    return

  }

    }else{

    }

};

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;

  options::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, options::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);

    }

  ErrorSet(ArithVariables& var, TableauSizes tabSizes, BoundCountingLookup boundLookup);

  typedef ErrorInfoMap::const_iterator error_iterator;

  void pushErrorInto(ArithVarVec& vec) const;

  void pushFocusInto(ArithVarVec& vec) const;

  options::ErrorSelectionRule getSelectionRule() const;

  void setSelectionRule(options::ErrorSelectionRule rule);

  }

  inline void signalUnderCnd(ArithVar var, bool b){

    if(b){ signalVariable(var); }

  }

  }

  inline void signalIfInconsistent(ArithVar var){

    signalUnderCnd(var, inconsistent(var));

  }

  }

  }

  }

  }

  }

    }else{

    }

  }

  void focusDownToJust(ArithVar v);

  void clearFocus();

  /** Clears the set. */

  void clear();

  void reduceToSignals();

  }

  }

  }

  /**

   * Moves a variable out of the signals.

   * This moves it into the error set.

   * Return the previous focus sign.

   */

  int popSignal();

  }

  }

  }

  }

  typedef FocusSet::const_iterator focus_iterator;

  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 d_statistics;

};

}  // namespace arith

}  // namespace theory

}  // namespace cvc5