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

remove assumption that merged and fixed variables are disjoint #178

Conversation

yuvaljacoby
Copy link
Collaborator

It's a minor change.
In Preprocessor.cpp we assume that fixedVariables and mergedVariables are disjoint (preprocess function).

I tried an example that it wasn't the case and then number of variables overflowed and the query got stuck.
Not the most elegant solution but fixed my problem...

@guykatzz
Copy link
Collaborator

I don't really understand this fix. You're suggesting that the "variableCount" can be negative, and that it should be set to 0 instead? We should add a more general fix, as it seems this phenomenon can happen also when variableCount is positive.

@yuvaljacoby yuvaljacoby changed the title merged and fixed variables are disjoint assumption [WIP] merged and fixed variables are disjoint assumption Sep 23, 2019
@yuvaljacoby
Copy link
Collaborator Author

You are probably right.
This fix is a patch and not what we actually need to do.
I pushed code that reproduce the problem, I prefer not to fix it right now (after finishing CMake I can do it). In the mean time should I also open an issue?

src/engine/Makefile Outdated Show resolved Hide resolved
@guykatzz
Copy link
Collaborator

For the failing example, did you run in DEBUG mode? Did the assertion at the end of Preprocessor::preprocess go off?

@yuvaljacoby
Copy link
Collaborator Author

Didn't run in debug mode, didn't know about the DEBUG_ON flag.
After adding it the assert raises exception.

@guykatzz
Copy link
Collaborator

Please try now

@yuvaljacoby yuvaljacoby changed the title [WIP] merged and fixed variables are disjoint assumption remove assumption that merged and fixed variables are disjoint Sep 23, 2019
@yuvaljacoby
Copy link
Collaborator Author

Works, Thanks.
Cleaned the pull request, I think we can squash and merge.

@guykatzz
Copy link
Collaborator

guykatzz commented Sep 23, 2019 via email

@yuvaljacoby
Copy link
Collaborator Author

done
did also a small fix in sec/common/debug , we need the three dots there in order to use variables.

The default compilation of the tests does not have the DEBUG_ON flag, should we change it?

@guykatzz
Copy link
Collaborator

Yes, lets have DBEUG_ON for the tests.

@guykatzz guykatzz merged commit b516c6e into NeuralNetworkVerification:master Sep 24, 2019
yuvaljacoby added a commit to yuvaljacoby/Marabou-1 that referenced this pull request Oct 7, 2019
…lNetworkVerification#178)

* we assume the merged and fixed variables are disjoint, but if it's not the case they might overflow, fix that

* reproduce problem

* add the main test file

* an attempted fix

* clean

* more clean

* add test to verify merged and fix variables are disjoint

* cosmetics
matanost pushed a commit that referenced this pull request Nov 2, 2021
* we assume the merged and fixed variables are disjoint, but if it's not the case they might overflow, fix that

* reproduce problem

* add the main test file

* an attempted fix

* clean

* more clean

* add test to verify merged and fix variables are disjoint

* cosmetics
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