dlinear::LeakyReluConstraint Class Reference

Inheritance diagram for dlinear::LeakyReluConstraint:

Public Member Functions
	LeakyReluConstraint (const Variable &relu_var, const Expression &e, float alpha, const PredicateAbstractor &pa)
	Construct a new LeakyReluConstraint object.
	LeakyReluConstraint (const Formula &active_formula, const Formula &inactive_formula, Variable relu_var, Expression active_soi, Expression inactive_soi, const PredicateAbstractor &pa)
	Construct a new Relu Constraint object.
	LeakyReluConstraint (Variable active_var, Variable inactive_var, Variable relu_var, Expression active_soi, Expression inactive_soi)
	Construct a new Relu Constraint object.
void	UpdateUpperBound (const mpq_class *upper_bound) override
	Update the upper bounds of the constraint.
void	UpdateLowerBound (const mpq_class *lower_bound) override
	Update the lower bounds of the constraint.
std::set< LiteralSet >	TightenBounds (BoundPreprocessor &preprocessor) override
	Use the preprocessor to tighten the bounds of the constraint and hopefully fix its state to either active or inactive.
LiteralSet	Assumptions () const override
	The assumptions used to guide the SAT solver towards the most promising sub-problems.
LiteralSet	LearnedClauses () const override
	Produce some learned clauses the SAT solver will use to prune the sub-problems this piecewise constraint will not be satisfied in.
std::ostream &	Print (std::ostream &os) const override
	Print the constraint on the standard output.
Public Member Functions inherited from dlinear::PiecewiseLinearConstraint
	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)
	Construct a new Piecewise Linear Constraint object.
void	UpdateBounds (const mpq_class &lb, const mpq_class &ub)
	Update the bounds of the constraint.
void	UpdateBounds (const mpq_class *lb, const mpq_class *ub)
	Update the bounds of the constraint.
mpq_class	Cost (const Environment &env) const
	Calculate the cost of the violation of the constraint.
mpq_class	Cost (const Environment &env, bool active) const
	Calculate the cost of the violation of the constraint forcing a specific state.
bool	has_lower_bound () const
	Check whether the constraint is lower bounded.
bool	has_upper_bound () const
	Check whether the constraint is upper bounded.
bool	fixed () const
	Check whether the constraint is fixed.
const mpq_class &	lower_bound () const
	Get read-only access to the lower bound of the constraint.
const mpq_class &	upper_bound () const
	Get read-only access to the upper bound of the constraint.
const Variable &	active_var () const
	Get read-only access to the boolean variable associated with the $y = f_\text{active}(x)$ theory literal of the constraint.
const Variable &	inactive_var () const
	Get read-only access to the boolean variable associated with the $y = f_\text{inactive}(x)$ theory literal of the constraint.
const Variable &	theory_var () const
	Get read-only access to the theory variable $y$ of the constraint.
const Expression &	active_soi () const
	Get read-only access to the expression $y - f_\text{active}(x)$ of the constraint.
const Expression &	inactive_soi () const
	Get read-only access to the expression $y - f_\text{inactive}(x)$ of the constraint.
const Expression &	soi () const
PiecewiseConstraintState	state () const
	Get read-only access to the state of the constraint.

Static Public Attributes
static const mpq_class	zero {0}
	Zero constant all the pointers to the default lower bound will point to.
Static Public Attributes inherited from dlinear::PiecewiseLinearConstraint
static const Expression	zero_soi {0}
	Expression $0$ used as a soi if the constraint is not fixed yet.

Additional Inherited Members
Protected Attributes inherited from dlinear::PiecewiseLinearConstraint
const mpq_class *	lower_bound_
	Lower bound of the constraint.
const mpq_class *	upper_bound_
	Upper bound of the constraint.
const Variable	active_var_
	Boolean variable associated with the $y = f_\text{active}(x)$ theory literal.
const Variable	inactive_var_
	Boolean variable associated with the $y = f_\text{inactive}(x)$ theory literal.
const Variable	theory_var_
	Theory variable $y$.
const Expression	active_soi_
	Expression $y - f_\text{active}(x)$.
const Expression	inactive_soi_
	Expression $y - f_\text{inactive}(x)$.
PiecewiseConstraintState	state_
	State of the constraint.

Detailed Description

Definition at line 15 of file LeakyReluConstraint.h.

Constructor & Destructor Documentation

LeakyReluConstraint() [1/3]

dlinear::LeakyReluConstraint::LeakyReluConstraint	(	const Variable &	relu_var,
		const Expression &	e,
		float	alpha,
		const PredicateAbstractor &	pa )

Construct a new LeakyReluConstraint object.

Given the standard ReLU definition, where relu_var is $y$ and e is $x$, we store the following:

• inactive_formula is the formula $y = alpha * x$
• active_formula is the formula $y = x$
• active_soi is the sum of infeasibility $y - x$ used if the constraint is active.
• inactive_soi is the sum of infeasibility $y - alpha * x$ used if the constraint is inactive.

  Parameters

  relu_var	theory variable $y$
  e	expression $x$
  alpha	leaky factor
  pa	predicate abstractor used to convert the formula to a boolean variable

Definition at line 18 of file LeakyReluConstraint.cpp.

LeakyReluConstraint() [2/3]

dlinear::LeakyReluConstraint::LeakyReluConstraint	(	const Formula &	active_formula,
		const Formula &	inactive_formula,
		Variable	relu_var,
		Expression	active_soi,
		Expression	inactive_soi,
		const PredicateAbstractor &	pa )

Construct a new Relu Constraint object.

Given the standard ReLU definition, the three theory variables are:

• inactive_formula is the formula $y = 0$
• active_formula is the formula $y = x$
• relu_var is the theory variable $y$

  Parameters

  active_formula	formula $y = x$
  inactive_formula	formula $y = 0$
  relu_var	theory variable $y$
  active_soi	sum of infeasibility $y - x$ used if the constraint is active. It must be $0$ for the constraint to be satisfied
  pa	predicate abstractor used to convert the formula to a boolean variable

LeakyReluConstraint() [3/3]

dlinear::LeakyReluConstraint::LeakyReluConstraint	(	Variable	active_var,
		Variable	inactive_var,
		Variable	relu_var,
		Expression	active_soi,
		Expression	inactive_soi )

Construct a new Relu Constraint object.

Given the standard ReLU definition, the three theory variables are:

• inactive_var is the boolean variable associated with the formula $y = 0$
• active_var is the boolean variable associated with the formula $y = x$
• relu_var is the theory variable $y$

  Parameters

  active_var	boolean variable associated with the formula $y = x$
  inactive_var	boolean variable associated with the formula $y = 0$
  relu_var	theory variable $y$
  active_soi	sum of infeasibility $y - x$ used if the constraint is active. It must be $0$ for the constraint to be satisfied

Definition at line 23 of file LeakyReluConstraint.cpp.

Member Function Documentation

Assumptions()

LiteralSet dlinear::LeakyReluConstraint::Assumptions ( ) const

nodiscardoverridevirtual

The assumptions used to guide the SAT solver towards the most promising sub-problems.

Returns

set of literals

Implements dlinear::PiecewiseLinearConstraint.

Definition at line 72 of file LeakyReluConstraint.cpp.

LearnedClauses()

LiteralSet dlinear::LeakyReluConstraint::LearnedClauses ( ) const

nodiscardoverridevirtual

Produce some learned clauses the SAT solver will use to prune the sub-problems this piecewise constraint will not be satisfied in.

Returns

set of literals

Implements dlinear::PiecewiseLinearConstraint.

Definition at line 78 of file LeakyReluConstraint.cpp.

Print()

std::ostream & dlinear::LeakyReluConstraint::Print ( std::ostream & os ) const

overridevirtual

Print the constraint on the standard output.

Parameters

os	standard output

Returns

updated standard output

Implements dlinear::PiecewiseLinearConstraint.

Definition at line 86 of file LeakyReluConstraint.cpp.

TightenBounds()

std::set< LiteralSet > dlinear::LeakyReluConstraint::TightenBounds ( BoundPreprocessor & preprocessor )

overridevirtual

Use the preprocessor to tighten the bounds of the constraint and hopefully fix its state to either active or inactive.

Parameters

preprocessor

preprocessor to use to tighten the bounds

Returns

explanation of why the inactive state of this constraint is unsat

Implements dlinear::PiecewiseLinearConstraint.

Definition at line 52 of file LeakyReluConstraint.cpp.

UpdateLowerBound()

void dlinear::LeakyReluConstraint::UpdateLowerBound ( const mpq_class * lb )

overridevirtual

Update the lower bounds of the constraint.

Precondition

the new lower bound must be greater than or equal to the current lower bound

Parameters

lb	lower bound of the constraint

Reimplemented from dlinear::PiecewiseLinearConstraint.

Definition at line 33 of file LeakyReluConstraint.cpp.

UpdateUpperBound()

void dlinear::LeakyReluConstraint::UpdateUpperBound ( const mpq_class * ub )

overridevirtual

Update the upper bounds of the constraint.

Precondition

the new upper bound must be less than or equal to the current upper bound

Parameters

ub	upper bound of the constraint

Reimplemented from dlinear::PiecewiseLinearConstraint.

Definition at line 40 of file LeakyReluConstraint.cpp.

---

The documentation for this class was generated from the following files:

• dlinear/solver/LeakyReluConstraint.h
• dlinear/solver/LeakyReluConstraint.cpp