Bug 1707353

Created attachment 1565098 [details]
Fix for swig 4.0.0

Thank you for the patches, Jitka.  I have been working on an update to cvc4 1.7.  It uses cmake instead of autotools; the first patch does not seem to be needed.  I applied the second patch, which does indeed fix the build of the Java interface.  However, the python 3 interface still fails to build.  The error (shown below) says that there is no 0-argument Datatype constructor, which is what the code the second patch touches is supposed to avoid.  I get the same error with and without that second patch, which suggests that python 3 needs a slightly different approach.  I am not conversant with swig, however, and would appreciate a hint from anyone who is.

This is the error:
In file included from /usr/include/c++/9/bits/stl_tempbuf.h:60,
                 from /usr/include/c++/9/bits/stl_algo.h:62,
                 from /usr/include/c++/9/algorithm:62,
                 from /builddir/build/BUILD/CVC4-1.7/src/bindings/python/CMakeFiles/_CVC4.dir/cvc4PYTHON_wrap.cxx:3525:
/usr/include/c++/9/bits/stl_construct.h: In instantiation of 'void std::_Construct(_T1*, _Args&& ...) [with _T1 = CVC4::Datatype; _Args = {}]':
/usr/include/c++/9/bits/stl_uninitialized.h:527:18:   required from 'static _ForwardIterator std::__uninitialized_default_n_1<_TrivialValueType>::__uninit_default_n(_ForwardIterator, _Size) [with _ForwardIterator = CVC4::Datatype*; _Size = long unsigned int; bool _TrivialValueType = false]'
/usr/include/c++/9/bits/stl_uninitialized.h:583:20:   required from '_ForwardIterator std::__uninitialized_default_n(_ForwardIterator, _Size) [with _ForwardIterator = CVC4::Datatype*; _Size = long unsigned int]'
/usr/include/c++/9/bits/stl_uninitialized.h:645:44:   required from '_ForwardIterator std::__uninitialized_default_n_a(_ForwardIterator, _Size, std::allocator<_Tp>&) [with _ForwardIterator = CVC4::Datatype*; _Size = long unsigned int; _Tp = CVC4::Datatype]'
/usr/include/c++/9/bits/stl_vector.h:1603:36:   required from 'void std::vector<_Tp, _Alloc>::_M_default_initialize(std::vector<_Tp, _Alloc>::size_type) [with _Tp = CVC4::Datatype; _Alloc = std::allocator<CVC4::Datatype>; std::vector<_Tp, _Alloc>::size_type = long unsigned int]'
/usr/include/c++/9/bits/stl_vector.h:509:9:   required from 'std::vector<_Tp, _Alloc>::vector(std::vector<_Tp, _Alloc>::size_type, const allocator_type&) [with _Tp = CVC4::Datatype; _Alloc = std::allocator<CVC4::Datatype>; std::vector<_Tp, _Alloc>::size_type = long unsigned int; std::vector<_Tp, _Alloc>::allocator_type = std::allocator<CVC4::Datatype>]'
/builddir/build/BUILD/CVC4-1.7/src/bindings/python/CMakeFiles/_CVC4.dir/cvc4PYTHON_wrap.cxx:46498:83:   required from here
/usr/include/c++/9/bits/stl_construct.h:75:7: error: no matching function for call to 'CVC4::Datatype::Datatype()'
   75 |     { ::new(static_cast<void*>(__p)) _T1(std::forward<_Args>(__args)...); }
      |       ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In file included from /builddir/build/BUILD/CVC4-1.7/src/bindings/python/CMakeFiles/_CVC4.dir/cvc4PYTHON_wrap.cxx:3575:
/builddir/build/BUILD/CVC4-1.7/src/expr/datatype.h:1160:8: note: candidate: 'CVC4::Datatype::Datatype(std::string, const std::vector<CVC4::Type>&, bool)'
 1160 | inline Datatype::Datatype(std::string name, const std::vector<Type>& params,
      |        ^~~~~~~~
/builddir/build/BUILD/CVC4-1.7/src/expr/datatype.h:1160:8: note:   candidate expects 3 arguments, 0 provided
/builddir/build/BUILD/CVC4-1.7/src/expr/datatype.h:1143:8: note: candidate: 'CVC4::Datatype::Datatype(std::string, bool)'
 1143 | inline Datatype::Datatype(std::string name, bool isCo)
      |        ^~~~~~~~
/builddir/build/BUILD/CVC4-1.7/src/expr/datatype.h:1143:8: note:   candidate expects 2 arguments, 0 provided
/builddir/build/BUILD/CVC4-1.7/src/expr/datatype.h:600:19: note: candidate: 'CVC4::Datatype::Datatype(const CVC4::Datatype&)'
  600 | class CVC4_PUBLIC Datatype {
      |                   ^~~~~~~~
/builddir/build/BUILD/CVC4-1.7/src/expr/datatype.h:600:19: note:   candidate expects 1 argument, 0 provided
make[2]: *** [src/bindings/python/CMakeFiles/_CVC4.dir/build.make:66: src/bindings/python/CMakeFiles/_CVC4.dir/CMakeFiles/_CVC4.dir/cvc4PYTHON_wrap.cxx.o] Error 1
make[2]: Leaving directory '/builddir/build/BUILD/CVC4-1.7'
make[1]: *** [CMakeFiles/Makefile2:3056: src/bindings/python/CMakeFiles/_CVC4.dir/all] Error 2


These are the only swig warnings related to datatype.h:
/builddir/build/BUILD/CVC4-1.7/src/expr/datatype.h:62: Warning 383: operator++ ignored
/builddir/build/BUILD/CVC4-1.7/src/expr/datatype.h:63: Warning 383: operator++ ignored
/builddir/build/BUILD/CVC4-1.7/src/expr/datatype.h:81: Warning 383: operator++ ignored
/builddir/build/BUILD/CVC4-1.7/src/expr/datatype.h:82: Warning 383: operator++ ignored

Could you please provide me a source rpm? I'll try to look on it.

You can also send the report to swig-user.net

I am currently in a place where outbound SSL connections cannot be made, and the src.rpm is rather large, so I will attach the spec file and the current set of patches to this bug.  Thank you for any help you can provide.

Created attachment 1566189 [details]
cvc4 spec file

Created attachment 1566190 [details]
First patch for cvc4

Created attachment 1566197 [details]
Second patch for cvc4

Created attachment 1566200 [details]
Third patch for cvc4

Of course, you already attached the final patch for cvc4, the one named "Fix for swig 4.0.0".  I just named it cvc4-swig4.patch.

I tried to rebuild the CVC4 version 1.7 with your changes and it failed with different error:

BUILDSTDERR: /builddir/build/BUILD/CVC4-1.7/src/smt/smt_engine.cpp: In member function 'void CVC4::SmtEngine::checkProof()':
BUILDSTDERR: /builddir/build/BUILD/CVC4-1.7/src/smt/smt_engine.cpp:4457:22: error: cannot convert 'std::stringstream' {aka 'std::__cxx11::basic_stringstream<char>'} to 'const char*'
BUILDSTDERR:  4457 |     lfscc_check_file(pfStream, false, false, false, false, false, false, false);
BUILDSTDERR:       |                      ^~~~~~~~
BUILDSTDERR:       |                      |
BUILDSTDERR:       |                      std::stringstream {aka std::__cxx11::basic_stringstream<char>}


However, it seem the error is not related to swig 4.0.0. I ran rebuild of the cvc4-1.7 on Fedora 30 with swig 3.0.12 and it failed with the same error.

Created attachment 1570248 [details]
Updated lfsc

You need an updated version of lfsc, too.  Sorry, I didn't realize that was required.  A source RPM is attached.

FEDORA-2019-80a9b551fc has been submitted as an update to Fedora 30. https://bodhi.fedoraproject.org/updates/FEDORA-2019-80a9b551fc

abc-1.01-22.git20190608.fc30, cadical-0-1.sr19.fc30, cvc4-1.7-1.fc30, lfsc-0.20190226-1.fc30, symfpu-0-0.4.20190517gitc3acaf6.fc30 has been pushed to the Fedora 30 testing repository. If problems still persist, please make note of it in this bug report.
See https://fedoraproject.org/wiki/QA:Updates_Testing for
instructions on how to install test updates.
You can provide feedback for this update here: https://bodhi.fedoraproject.org/updates/FEDORA-2019-80a9b551fc

abc-1.01-22.git20190608.fc30, cadical-0-1.sr19.fc30, cvc4-1.7-1.fc30, lfsc-0.20190226-1.fc30, symfpu-0-0.4.20190517gitc3acaf6.fc30 has been pushed to the Fedora 30 stable repository. If problems still persist, please make note of it in this bug report.