ReluConstraint.h

 
#pragma once
 
#include <optional>
 
#include "dlinear/solver/PiecewiseLinearConstraint.h"
#include "dlinear/symbolic/PredicateAbstractor.h"
#include "dlinear/symbolic/symbolic.h"
 
namespace dlinear {
 
class ReluConstraint : public PiecewiseLinearConstraint {
 public:
  static const mpq_class zero;  
 
  ReluConstraint(const Variable& relu_var, const Expression& e, const PredicateAbstractor& pa);
  ReluConstraint(Variable active_var, Variable inactive_var, Variable relu_var, Expression active_soi);
 
  void UpdateUpperBound(const mpq_class* upper_bound) override;
  void UpdateLowerBound(const mpq_class* lower_bound) override;
 
  void EnableLiteral(const Variable& var);
 
  std::set<LiteralSet> TightenBounds(BoundPreprocessor& preprocessor) override;
 
  [[nodiscard]] LiteralSet Assumptions() const override;
 
  [[nodiscard]] LiteralSet LearnedClauses() const override;
 
  std::ostream& Print(std::ostream& os) const override;
};
 
}  // namespace dlinear