CPMpy / cpmpy

Constraint Programming and Modeling library in Python, based on numpy, with direct solver access.
Apache License 2.0
206 stars 19 forks source link

Calling _IntVarImpl makes model unsat #262

Open Wout4 opened 1 year ago

Wout4 commented 1 year ago

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 commented 1 year ago

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

Dimosts commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

can confirm this bug is still active