PiecewiseLinearConstraint.h

 
#pragma once
 
#include <istream>
#include <optional>
 
#include "dlinear/libs/libgmp.h"
#include "dlinear/solver/BoundPreprocessor.h"
#include "dlinear/solver/PiecewiseConstraintState.h"
#include "dlinear/symbolic/literal.h"
#include "dlinear/symbolic/symbolic.h"
 
namespace dlinear {
 
class PiecewiseLinearConstraint {
 public:
  static const Expression zero_soi;  
 
  explicit PiecewiseLinearConstraint(const mpq_class* lb = nullptr, const mpq_class* ub = nullptr,
                                     Variable active_var = {}, Variable inactive_var = {}, Variable theory_var = {},
                                     Expression active_soi = {0}, Expression inactive_soi = {0},
                                     PiecewiseConstraintState state = PiecewiseConstraintState::NOT_FIXED);
  virtual ~PiecewiseLinearConstraint() = default;
 
  virtual std::set<LiteralSet> TightenBounds(BoundPreprocessor& preprocessor) = 0;
 
  virtual std::ostream& Print(std::ostream& os) const = 0;
 
  [[nodiscard]] virtual LiteralSet Assumptions() const = 0;
  [[nodiscard]] virtual LiteralSet LearnedClauses() const = 0;
 
  void UpdateBounds(const mpq_class& lb, const mpq_class& ub);
  void UpdateBounds(const mpq_class* lb, const mpq_class* ub);
  virtual void UpdateLowerBound(const mpq_class* lb);
  virtual void UpdateUpperBound(const mpq_class* ub);
 
  [[nodiscard]] mpq_class Cost(const Environment& env) const;
  [[nodiscard]] mpq_class Cost(const Environment& env, bool active) const;
 
  [[nodiscard]] bool has_lower_bound() const { return lower_bound_ != nullptr; }
  [[nodiscard]] bool has_upper_bound() const { return upper_bound_ != nullptr; }
  [[nodiscard]] bool fixed() const {
    return state_ == PiecewiseConstraintState::ACTIVE || state_ == PiecewiseConstraintState::INACTIVE;
  }
  [[nodiscard]] const mpq_class& lower_bound() const;
  [[nodiscard]] const mpq_class& upper_bound() const;
  [[nodiscard]] const Variable& active_var() const { return active_var_; }
  [[nodiscard]] const Variable& inactive_var() const { return inactive_var_; }
  [[nodiscard]] const Variable& theory_var() const { return theory_var_; }
  [[nodiscard]] const Expression& active_soi() const { return active_soi_; }
  [[nodiscard]] const Expression& inactive_soi() const { return inactive_soi_; }
  [[nodiscard]] const Expression& soi() const;
  [[nodiscard]] PiecewiseConstraintState state() const { return state_; }
 
 protected:
  const mpq_class* lower_bound_;  
  const mpq_class* upper_bound_;  
 
  const Variable active_var_;  
  const Variable
      inactive_var_;           
  const Variable theory_var_;  
 
  const Expression active_soi_;    
  const Expression inactive_soi_;  
 
  PiecewiseConstraintState state_;  
};
 
std::ostream& operator<<(std::ostream& os, const PiecewiseLinearConstraint& gc);
 
}  // namespace dlinear
 
#ifdef DLINEAR_INCLUDE_FMT
 
#include "dlinear/util/logging.h"
 
OSTREAM_FORMATTER(dlinear::PiecewiseLinearConstraint)
 
#endif