randriu / synthesis

GNU General Public License v3.0
22 stars 19 forks source link

C++17 Compatibility Issue with ranges in Storm during python3 setup.py develop #47

Open IOExceptionOI opened 2 weeks ago

IOExceptionOI commented 2 weeks ago

Hello PAYNT team,

I'm encountering a compatibility issue when building PAYNT. The problem arises during the step:

cd payntbind
python3 setup.py develop

I receive compilation errors due to the use of ranges,

Error Messages:

/usr/local/include/storm/storm/storage/BitVector.h:782:20: error: no member named 'ranges' in namespace 'std'
static_assert(std::ranges::forward_range<BitVector>);

which is not supported in C++17. But PAYNT is based on C++17, However, this step works correctly in my Docker container, where the setup does not seem to conflict with the C++ standard.

questions

Is there a recommended approach to integrate Storm, which requires C++20, into a project that is primarily using C++17? Or is there sth. wrong I have done?

Thank you for your assistance!

lukovdm commented 2 weeks ago

I came across the same problem. I fixed it for myself by just increasing the C++ version to C++20 in the payntbind/CMakeList.txt file. Furthermore, I also had to upgrade my Boost version to above 1.74, since there was some bug with C++20 and boost 1.74.

IOExceptionOI commented 2 weeks ago

@lukovdm Thanks for your help! But I have tried increasing the C++ version to C++20 in the payntbind/CMakeList.txt file but there still occurs the Error which maybe relevant to the new feature introduced in C++ 20:

error: use of overloaded operator '<' is ambiguous (with operand types 'z3::expr' and 'uint64_t' (aka 'unsigned long long'))
    solver.add(0 <= harmonizing_variable and harmonizing_variable < family.numHoles(), "harmonizing_domain");

and I also upgrade my Boost version to 1.76, but it seems not working. Do you have any advice for me?

lukovdm commented 2 weeks ago

That is weird, I don't have the same issue. I am using Boost 1.81, but that is the only difference I can see.

TheGreatfpmK commented 1 week ago

Hi! Sorry for late response but you can update the line 517 in payntbind/src/synthesis/quotient/ColoringSmt.cpp to:

solver.add(0 <= harmonizing_variable and harmonizing_variable < (int)family.numHoles(), "harmonizing_domain");

This should hopefully be enough to compile it, we will introduce a fix in master later.

randriu commented 6 days ago

We pushed the fix to master. @IOExceptionOI if the fix still does not work for you, try updating Boost to at least version 1.83.