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

Calling _IntVarImpl makes model unsat #262

Open
Wout4 opened this issue Mar 27, 2023 · 4 comments · May be fixed by #402
Open

Calling _IntVarImpl makes model unsat #262

Wout4 opened this issue Mar 27, 2023 · 4 comments · May be fixed by #402

Comments

@Wout4
Copy link
Collaborator

Wout4 commented Mar 27, 2023

you need the model matrix_element_test16650504392567291.bt from cpmpy/bigtest to reproduce this bug

example below prints true, then false.
For z3 it prints twice true
for minizinc it prints twice false
for ortools + mininzinc it returns twice true
for minizinc + ortools it returns false, true
...

import brotli
import pickle
from cpmpy.expressions.variables import _IntVarImpl
f = 'models\matrix_element_test16650504392567291.bt'
with open(f, 'rb') as fpcl:
model = pickle.loads(brotli.decompress(fpcl.read()))
print(model.solve('ortools'))
_IntVarImpl(0, 1)
print(model.solve('ortools'))

@Wout4
Copy link
Collaborator Author

Wout4 commented Apr 17, 2023

minizinc no longer thinks this model is unsat, since bugfix #272

@Dimosts
Copy link
Collaborator

Dimosts commented Jun 12, 2023

so is this fixed? Or besides minizinc it still crashes?

One way to get over this (and also similar problems with using directly _BoolVarImpl) we could check the function calling the constructor of _IntVarImpl (and _BoolVarImpl) with inspect and return an exception if it is not the expected function(s). However this would require to include inspect in the requirements etc., which I am not sure we want ..

@Wout4
Copy link
Collaborator Author

Wout4 commented Jun 12, 2023

I think it still crashes, can verify later. The bug occurred without a user directly calling _intvarimpl, but because one of the transformations called it. I just tried to write a minimized bug report here ;)

@Wout4
Copy link
Collaborator Author

Wout4 commented Jul 3, 2023

can confirm this bug is still active

@Wout4 Wout4 linked a pull request Aug 21, 2023 that will close this issue
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants