Box.h

 
#pragma once
 
#include <iosfwd>
#include <memory>
#include <string>
#include <unordered_map>
#include <utility>
#include <vector>
 
#include "dlinear/libs/libgmp.h"
#include "dlinear/symbolic/literal.h"
#include "dlinear/symbolic/symbolic.h"  // IWYU pragma: keep for hash_value
#include "dlinear/util/Config.h"
#include "dlinear/util/Interval.h"
 
namespace dlinear {
 
class Box {
 public:
  explicit Box(Config::LPSolver lp_solver);
 
  explicit Box(const std::vector<Variable> &variables, Config::LPSolver lp_solver);
 
  void Add(const Variable &v);
 
  void Add(const Variable &v, const mpq_class &lb, const mpq_class &ub);
 
  [[nodiscard]] bool empty() const;
 
  void set_empty();
 
  [[nodiscard]] int size() const;
 
  Interval &operator[](int i);
 
  Interval &operator[](const Variable &var);
 
  const Interval &operator[](int i) const;
 
  const Interval &operator[](const Variable &var) const;
 
  [[nodiscard]] Config::LPSolver lp_solver() const { return lp_solver_; }
  [[nodiscard]] const std::vector<Variable> &variables() const;
 
  [[nodiscard]] const Variable &variable(int i) const;
 
  [[nodiscard]] bool has_variable(const Variable &var) const;
 
  [[nodiscard]] const std::vector<Interval> &interval_vector() const;
 
  std::vector<Interval> &m_interval_vector();
 
  [[nodiscard]] int index(const Variable &var) const;
 
  [[nodiscard]] std::pair<mpq_class, int> MaxDiam() const;
 
  [[nodiscard]] std::pair<Box, Box> Bisect(int i) const;
 
  [[nodiscard]] std::pair<Box, Box> Bisect(const Variable &var) const;
 
 private:
  [[nodiscard]] std::pair<Box, Box> BisectInt(int i) const;
 
  [[nodiscard]] std::pair<Box, Box> BisectContinuous(int i) const;
 
  Config::LPSolver lp_solver_;                                     
  std::vector<Interval> values_;                                   
  std::shared_ptr<std::vector<Variable>> variables_;               
  std::shared_ptr<std::unordered_map<Variable, int>> var_to_idx_;  
  std::shared_ptr<std::unordered_map<int, Variable>> idx_to_var_;  
 
  friend std::ostream &operator<<(std::ostream &os, const Box &box);
};
 
std::ostream &operator<<(std::ostream &os, const Box &box);
 
bool operator==(const Box &b1, const Box &b2);
 
bool operator!=(const Box &b1, const Box &b2);
 
std::ostream &DisplayDiff(std::ostream &os, const std::vector<Variable> &variables, const std::vector<Interval> &old_iv,
                          const std::vector<Interval> &new_iv);
 
}  // namespace dlinear
 
#ifdef DLINEAR_INCLUDE_FMT
 
#include "dlinear/util/logging.h"
 
OSTREAM_FORMATTER(dlinear::Box)
 
#endif