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.

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

Expose MILP timeout and Marabou preprocess to python interface. #438

Merged
merged 37 commits into from
Mar 1, 2021

Conversation

alexopenu
Copy link
Collaborator

I have been using these options for some time; apparently there is more demand for them.

alexopenu and others added 30 commits August 9, 2019 09:25
merging from guykatzz/master
I was getting the following error on build:

/Marabou/src/engine/ReluConstraint.cpp:913:14: error: call to 'abs' is ambiguous
    _score = std::abs( computePolarity() );
             ^~~~~~~~
Generally this probably happens because computePolarity() returns double, and abs accepts int or long int.

In cmath there is abs that accepts double, hence this fixed the issue.
@alexopenu alexopenu requested a review from wu-haoze March 1, 2021 19:07
Copy link
Collaborator

@wu-haoze wu-haoze left a comment

Choose a reason for hiding this comment

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

LGTM, except for the minor comments.

@@ -196,6 +196,7 @@ struct MarabouOptions {
, _sncSplittingStrategyString( Options::get()->getString( Options::SNC_SPLITTING_STRATEGY ).ascii() )
, _tighteningStrategyString( Options::get()->getString( Options::SYMBOLIC_BOUND_TIGHTENING_TYPE ).ascii() )
, _milpTighteningString( Options::get()->getString( Options::MILP_SOLVER_BOUND_TIGHTENING_TYPE ).ascii() )
, _milpSolverTimeout( Options::get()->getFloat( Options::MILP_SOLVER_TIMEOUT ) )
Copy link
Collaborator

Choose a reason for hiding this comment

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

Order the options such that all floatOptions are grouped together?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Good idea.

@@ -432,7 +475,8 @@ PYBIND11_MODULE(MarabouCore, m) {
.def_readwrite("_splittingStrategy", &MarabouOptions::_splittingStrategyString)
.def_readwrite("_sncSplittingStrategy", &MarabouOptions::_sncSplittingStrategyString)
.def_readwrite("_tighteningStrategy", &MarabouOptions::_tighteningStrategyString)
.def_readwrite("_milpTightening", &MarabouOptions::_milpTighteningString);
.def_readwrite("_milpTightening", &MarabouOptions::_milpTighteningString)
.def_readwrite("_milpSolverTimeout", &MarabouOptions::_milpSolverTimeout);
Copy link
Collaborator

Choose a reason for hiding this comment

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

Same here.

@alexopenu alexopenu merged commit a771a89 into NeuralNetworkVerification:master Mar 1, 2021
matanost pushed a commit that referenced this pull request Nov 2, 2021
* Fix a compilation issue on Mac.

I was getting the following error on build:

/Marabou/src/engine/ReluConstraint.cpp:913:14: error: call to 'abs' is ambiguous
    _score = std::abs( computePolarity() );
             ^~~~~~~~
Generally this probably happens because computePolarity() returns double, and abs accepts int or long int.

In cmath there is abs that accepts double, hence this fixed the issue.

* Remove extra newline

* Expose MILP timeout and Marabou preprocessor to python interface.

* Minor.

Co-authored-by: Guy Katz <guyk@cs.stanford.edu>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants