LeakyReluConstraint.h

 
#pragma once
 
#include "dlinear/solver/PiecewiseLinearConstraint.h"
#include "dlinear/symbolic/PredicateAbstractor.h"
#include "dlinear/symbolic/literal.h"
 
namespace dlinear {
 
class LeakyReluConstraint : public PiecewiseLinearConstraint {
 public:
  static const mpq_class zero;  
  LeakyReluConstraint(const Variable& relu_var, const Expression& e, float alpha, const PredicateAbstractor& pa);
  LeakyReluConstraint(const Formula& active_formula, const Formula& inactive_formula, Variable relu_var,
                      Expression active_soi, Expression inactive_soi, const PredicateAbstractor& pa);
  LeakyReluConstraint(Variable active_var, Variable inactive_var, Variable relu_var, Expression active_soi,
                      Expression inactive_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