BoundVector.h

 
#pragma once
 
#include <compare>
#include <cstddef>
#include <iosfwd>
#include <map>
#include <utility>
#include <vector>
 
#include "dlinear/libs/libgmp.h"
#include "dlinear/solver/BoundIterator.h"
#include "dlinear/solver/LpColBound.h"
#include "dlinear/symbolic/literal.h"
#include "dlinear/util/SortedVector.hpp"
 
namespace dlinear {
 
class BoundVector {
 public:
  using Bounds = SortedVector<Bound>;  
 
  BoundVector(const mpq_class& inf_l, const mpq_class& inf_u);
 
  BoundIterator AddBound(const Bound& bound);
  BoundIterator AddBound(const mpq_class& value, LpColBound lp_bound, const Literal& theory_lit,
                         const LiteralSet& explanation = {});
  bool RemoveBound(const Bound& bound);
  bool RemoveBound(const mpq_class& value, LpColBound lp_bound, const Literal& theory_lit,
                   const LiteralSet& explanation = {});
  void SetLowerBound(const mpq_class& value);
  void SetUpperBound(const mpq_class& value);
  void SetBounds(const mpq_class& lb, const mpq_class& ub);
 
  void Clear();
 
  [[nodiscard]] int n_lower_bounds() const { return n_lower_bounds_; }
  [[nodiscard]] int n_upper_bounds() const { return static_cast<int>(bounds_.size()) - n_lower_bounds_; }
  [[nodiscard]] BoundIterator GetActiveBound() const;
  [[nodiscard]] BoundIterator GetActiveBound(const mpq_class& value) const;
  [[nodiscard]] BoundIterator GetActiveBounds() const;
  [[nodiscard]] BoundIterator GetActiveBounds(const mpq_class& value) const;
  void GetActiveExplanation(LiteralSet& explanation) const;
  [[nodiscard]] LiteralSet GetActiveExplanation() const;
  void GetActiveEqExplanation(LiteralSet& explanation) const;
  [[nodiscard]] LiteralSet GetActiveEqExplanation() const;
  [[nodiscard]] std::pair<const mpq_class&, const mpq_class&> GetActiveBoundsValue() const;
  [[nodiscard]] const Bounds& bounds() const { return bounds_; }
  [[nodiscard]] const Bounds& nq_bounds() const { return nq_bounds_; }
  [[nodiscard]] const mpq_class& inf_l() const { return *inf_l_; }
  [[nodiscard]] const mpq_class& inf_u() const { return *inf_u_; }
  [[nodiscard]] const mpq_class& active_lower_bound() const { return *active_lower_bound_; }
  [[nodiscard]] const mpq_class& active_upper_bound() const { return *active_upper_bound_; }
 
  [[nodiscard]] const mpq_class* GetActiveEqualityBound() const {
    return IsActiveEquality(*active_lower_bound_) ? active_lower_bound_ : nullptr;
  }
 
  [[nodiscard]] const Bound& operator[](std::size_t idx) const { return bounds_[idx]; }
 
  [[nodiscard]] BoundIterator ViolatedBounds(const mpq_class& value, LpColBound lp_bound) const;
  [[nodiscard]] bool ViolatedNqBounds() const;
  [[nodiscard]] bool ViolatedNqBounds(const mpq_class& lb, const mpq_class& ub) const;
 
  [[nodiscard]] bool IsActiveEquality(const mpq_class& value) const;
  [[nodiscard]] bool IsLowerBound(const mpq_class& value) const;
 
  [[nodiscard]] bool IsUpperBound(const mpq_class& value) const;
  [[nodiscard]] bool IsLowerBounded() const;
  [[nodiscard]] bool IsUpperBounded() const;
  [[nodiscard]] bool IsBounded() const;
 
 private:
  [[nodiscard]] Bounds::const_iterator LowerBoundEnd() const;
  [[nodiscard]] BoundIterator GetActiveBound(const mpq_class& lb, const mpq_class& ub) const;
  [[nodiscard]] BoundIterator GetActiveBounds(const mpq_class& lb, const mpq_class& ub) const;
 
  std::size_t n_lower_bounds_;           
  Bounds bounds_;                        
  Bounds nq_bounds_;                     
  const mpq_class* inf_l_;               
  const mpq_class* inf_u_;               
  const mpq_class* active_lower_bound_;  
  const mpq_class* active_upper_bound_;  
};
 
using BoundVectorMap = std::map<Variable, BoundVector>;
using BoundVectorVector = std::vector<BoundVector>;
 
std::ostream& operator<<(std::ostream& os, const BoundVector& bounds_vector);
std::ostream& operator<<(std::ostream& os, const BoundVectorMap& bounds_vector_map);
std::ostream& operator<<(std::ostream& os, const BoundVectorVector& bounds_vector_vector);
 
}  // namespace dlinear
 
#ifdef DLINEAR_INCLUDE_FMT
 
#include "dlinear/util/logging.h"
 
OSTREAM_FORMATTER(dlinear::BoundIterator)
OSTREAM_FORMATTER(dlinear::BoundVector)
OSTREAM_FORMATTER(dlinear::BoundVectorMap)
OSTREAM_FORMATTER(dlinear::BoundVectorVector)
 
#endif