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

exitCode "Not_DONE" #842

Open
YourSaDady opened this issue Oct 3, 2024 · 4 comments
Open

exitCode "Not_DONE" #842

YourSaDady opened this issue Oct 3, 2024 · 4 comments

Comments

@YourSaDady
Copy link

Hi developers!
I try to solve a query using the MarabouNetworkONNX, and the exitCode that the .solve() returns is NOT_DONE. What does this result means?

The Marabou I use is just cloned, so I think there shouldn't be any issue with the version.
The simple ONNX network looks like this:
decoder_softmax

@YourSaDady
Copy link
Author

Could the prolem be that the current Marabou doesn't support flexible input dimension while ONNX does?

@YourSaDady
Copy link
Author

My query-solving options is set to Marabou.createOptions(snc=True, verbosity=0, initialSplits=2, timeoutInSeconds=1800).

I searched keyword NOT_DONE in the repository, and it seems that it only appears in DnCManager class. However, I didn't use the DnC mode.

@YourSaDady
Copy link
Author

My query constraint and model constraint should be error-free:
For the model constraint, I used the ONNX model to do inference and the generated result was as expected.
For the query constraint, I tested a trivial case where the returned result should be SAT when the perturbation on the inputVars is small. However, as I increased the perturbation on the inputVars, the exitCode changes from SAT to UNSAT and then to NOT_DONE. I find it hard to explain this.

@YourSaDady
Copy link
Author

For my case, the time_stamp dimension in the input and output of the ONNX model are flexible (different among different sample cases). However, after read_onnx(), the corresponding dimension becomes 1 for inputVars and outputVars.

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

No branches or pull requests

1 participant