Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

implementing addReluConstraint() #8

Closed
wants to merge 1 commit into from
Closed

implementing addReluConstraint() #8

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 7 additions & 0 deletions src/engine/InputQuery.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@
#include "MStringf.h"
#include "ReluplexError.h"
#include "FloatUtils.h"
#include "ReluConstraint.h"
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This violates our current encapsulation: input query doesn't know about particular piecewise linear constraints. It only supports the more general "addPiecewiseLinearConstraint" method. I suggest to remove this new code, and simply have the caller instantiate a ReluConstraint and pass it through the existing interface.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We were trying to avoid exposing the PiecewiseLinearConstraint class to the API, so we wrote this helper function for convenience.
Instead, we could have a function in the MarabouCore.cpp file
void addReluConstraint(InputQuery& ipq, unsigned x1, unsigned x2)
which would add the corresponding Relu constraint to the InputQuery. In this way, the encapsulation would be maintained, and the Python side does not need to know about the general LinearPiecewiseConstraint objects.

Would this be better?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The ReluConstraint class is a child class of PiecewiseLinearConstraint, so by exposing ReluConstraint I think we are actually exposing more, not less. The idea is that the entire Marabou core only knows about the more general PiecewiseLinearConstraint class, so that we don't have to make any changes when we add, e.g., max constraints. Currently only the code that populates the input queries knows about the actual sub-classes of PiecewiseLinearConstraint.

I would recommend having a similar abstraction in the python code for easier maintenance and extension, but I won't insist on this :)

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sorry, maybe I was unclear. I did not mean exposing the ReluConstraint class to the API. I meant exposing a function which, given an InputQuery and a pair of variables, adds the corresponding Relu constraint to the InputQuery. Thus, we do not expose the constraint classes themselves to the API, only this function which acts as an interface to add new constraints.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sure, if you want to have such a function in MarabouCore, that's fine.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In that case, we will close this PR and add this functionality to MarabouCore.cpp, which is in a different PR.


InputQuery::InputQuery()
{
Expand Down Expand Up @@ -117,6 +118,12 @@ double InputQuery::getSolutionValue( unsigned variable ) const
return _solution.get( variable );
}

void InputQuery::addReluConstraint(unsigned var1, unsigned var2)
{
PiecewiseLinearConstraint* r = new ReluConstraint(var1, var2);
addPiecewiseLinearConstraint(r);
}

void InputQuery::addPiecewiseLinearConstraint( PiecewiseLinearConstraint *constraint )
{
_plConstraints.append( constraint );
Expand Down
1 change: 1 addition & 0 deletions src/engine/InputQuery.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,7 @@ class InputQuery
const List<Equation> &getEquations() const;
List<Equation> &getEquations();

void addReluConstraint(unsigned var1, unsigned var2);
void addPiecewiseLinearConstraint( PiecewiseLinearConstraint *constraint );
const List<PiecewiseLinearConstraint *> &getPiecewiseLinearConstraints() const;
List<PiecewiseLinearConstraint *> &getPiecewiseLinearConstraints();
Expand Down