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

Extended testsuite uncovers flatten problems #217

Closed
IgnaceBleukx opened this issue Jan 25, 2023 · 2 comments
Closed

Extended testsuite uncovers flatten problems #217

IgnaceBleukx opened this issue Jan 25, 2023 · 2 comments

Comments

@IgnaceBleukx
Copy link
Collaborator

IgnaceBleukx commented Jan 25, 2023

I extended the test_constraints.py testsuite (in branch "extended_testsuite") this uncovers a range of errors related to boolean vs integer comparisons.
Bugs pop up in all solvers using the flatten transformation, so very likely this should be catched there.

As discusses offline, fixing this might have the need to introduce the unary "Not" operator to wrap around expressions instead of using == 0 to negate boolean expressions in general.

@IgnaceBleukx IgnaceBleukx changed the title Boolean expression comparing with integer Extended testsuite uncovers flatten problems Jan 26, 2023
@tias
Copy link
Collaborator

tias commented Feb 7, 2023

Yes to introducing 'Not' operator after all. And then we should take negate_normal out of flatten.py and make it a separate transformation 'negation' that pushes the negations down... will enable a few more optimisations in flatten, and eliminate the current ==0 !=1 weird checks too.

@Wout4
Copy link
Collaborator

Wout4 commented Jun 30, 2023

we now have push_down_negation and the not-operator

@Wout4 Wout4 closed this as completed Jun 30, 2023
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

3 participants