Bound.h

 
#pragma once
 
#include <utility>
 
#include "dlinear/libs/libgmp.h"
#include "dlinear/solver/LpColBound.h"
#include "dlinear/symbolic/literal.h"
 
namespace dlinear {
 
struct Bound {
  Bound() = default;
  Bound(const mpq_class* value_, LpColBound lp_bound_, Literal theory_literal_, LiteralSet explanation_)
      : value{value_},
        lp_bound{lp_bound_},
        theory_literal{std::move(theory_literal_)},
        explanation{std::move(explanation_)} {}
  Bound(const mpq_class* value_, LpColBound lp_bound_, Literal theory_literal_)
      : value{value_}, lp_bound{lp_bound_}, theory_literal{std::move(theory_literal_)}, explanation{} {}
 
  const mpq_class* value;  
  LpColBound lp_bound;     
  Literal theory_literal;  
  LiteralSet explanation;  
 
  std::strong_ordering operator<=>(const Bound& other) const;
  bool operator==(const Bound& other) const;
};
 
std::ostream& operator<<(std::ostream& os, const Bound& bound);
 
}  // namespace dlinear
 
#ifdef DLINEAR_INCLUDE_FMT
 
#include "dlinear/util/logging.h"
 
OSTREAM_FORMATTER(dlinear::Bound)
 
#endif