-
Notifications
You must be signed in to change notification settings - Fork 93
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
add script to run canonical benchmarks #431
add script to run canonical benchmarks #431
Conversation
Looks like this PR subsumes your other PR #436 |
maraboupy/MarabouCore.cpp
Outdated
@@ -317,6 +341,7 @@ InputQuery loadQuery(std::string filename){ | |||
// Describes which classes and functions are exposed to API | |||
PYBIND11_MODULE(MarabouCore, m) { | |||
m.doc() = "Maraboupy bindings to the C++ Marabou via pybind11"; | |||
m.def("loadProperty", &loadProperty, "Create input query from property file"); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It's not really creating an IPQ, right? Just adding the property on top of an existing IPQ?
maraboupy/runMarabou.py
Outdated
print("The network must be in .pb, .nnet, or .onnx format!") | ||
return None, None | ||
|
||
if args.prop != None: |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
double space after if
maraboupy/runMarabou.py
Outdated
encode_cifar10_linf(network, args.index, args.epsilon, args.target_label) | ||
return network.getMarabouQuery(), network | ||
else: | ||
print("No property encoded! The dataset must be taxi or mnist or cifar10.") |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I didnt understand the comment. Can you have both a dataset and a property? I guess not
* add new file * clean up run file * move to resource * minor
Add a python script to run canonical benchmarks.
It's intended to behave the same as the Marabou executable, but in addition supports
e.g.,
./maraboupy/runMarabou.py resources/nnet/acasxu/ACASXU_experimental_v2a_2_9.nnet resources/properties/acas_property_2.txt --snc --verbosity=0
./maraboupy/runMarabou.py resources/nnet/mnist/mnist10x10.nnet --index 2 --target-label 8 --epsilon 0.005 --dataset=mnist