Carl version mismatch? SMT-RAT build fails on Linux
rpgoldman opened this issue · 8 comments
I just pulled the latest SMTRAT and tried to build it on Linux, but got a failure that looks like a version mismatch with Carl. Specifically, SMTRAT wants a template type RealAlgebraicNumber from carl, but either it is not there, or it's not a template.
In file included from /home/rpg/src/smtrat/src/smtrat-analyzer/analyzers/cad_projections.cpp:5:0:
/home/rpg/src/smtrat/src/smtrat-cad/common.h:14:20: error: ‘RealAlgebraicNumber’ in namespace ‘carl’ does not name a template type
using RAN = carl::RealAlgebraicNumber<Rational>;
^~~~~~~~~~~~~~~~~~~
/home/rpg/src/smtrat/src/smtrat-cad/common.h:15:46: error: ‘RAN’ was not declared in this scope
using Assignment = std::map<carl::Variable, RAN>;
^~~
/home/rpg/src/smtrat/src/smtrat-cad/common.h:15:46: note: suggested alternative: ‘NAN’
using Assignment = std::map<carl::Variable, RAN>;
^~~
NAN
/home/rpg/src/smtrat/src/smtrat-cad/common.h:15:49: error: template argument 2 is invalid
using Assignment = std::map<carl::Variable, RAN>;
^
/home/rpg/src/smtrat/src/smtrat-cad/common.h:15:49: error: template argument 4 is invalid
In file included from /home/rpg/src/smtrat/src/smtrat-cad/projection/Projection.h:29:0,
from /home/rpg/src/smtrat/src/smtrat-analyzer/analyzers/cad_projections.cpp:7:
/home/rpg/src/smtrat/src/smtrat-cad/projection/Projection_Model.h: In member function ‘void smtrat::cad::ModelBasedProjection<(smtrat::cad::Incrementality)0, (smtrat::cad::Backtracking)0, Settings>::findPIDsForProjection(carl::Variable, std::size_t, const Model&, std::pair<long unsigned int, long unsigned int>&)’:
/home/rpg/src/smtrat/src/smtrat-cad/projection/Projection_Model.h:91:25: error: ‘RAN’ was not declared in this scope
RAN value = val.isRational() ? RAN(val.asRational()) : val.asRAN();
^~~
/home/rpg/src/smtrat/src/smtrat-cad/projection/Projection_Model.h:91:25: note: suggested alternative: ‘NAN’
RAN value = val.isRational() ? RAN(val.asRational()) : val.asRAN();
^~~
NAN
compilation terminated due to -fmax-errors=5.
src/smtrat-analyzer/CMakeFiles/smtrat-analyzer-objects.dir/build.make:62: recipe for target 'src/smtrat-analyzer/CMakeFiles/smtrat-analyzer-objects.dir/analyzers/cad_projections.cpp.o' failed
make[2]: *** [src/smtrat-analyzer/CMakeFiles/smtrat-analyzer-objects.dir/analyzers/cad_projections.cpp.o] Error 1
CMakeFiles/Makefile2:659: recipe for target 'src/smtrat-analyzer/CMakeFiles/smtrat-analyzer-objects.dir/all' failed
make[1]: *** [src/smtrat-analyzer/CMakeFiles/smtrat-analyzer-objects.dir/all] Error 2
Makefile:162: recipe for target 'all' failed
make: *** [all] Error 2
Looking in the Carl download in smtrat/build I see definitions for IntRepRealAlgebraicNumber and LPRealAlgebraicNumber but no RealAlgebraicNumber. Does this indicate a version mismatch?
I don't know how cmake works, but is there some way to record a version requirement in the cmake files so that it will emit an understandable error message when the version of Carl doesn't match the desired version?
Finally, is there a work-around? Is there some way to separately download the correct version of Carl, and build it before trying to build SMT-RAT.
I don't mean to seem disagreeable, but SMT-RAT's dependency tail is so big, and so brittle, that it would really be very helpful if we could get a Docker image instead of trying to build it ourselves.
Thank you for any advice
When I look at Carl, I see a definition of RealAlgebraicNumber as a template in src/carl-arith/ran/thom/ThomRootFinder.h
There is also a reference to RealAlgebraicNumber in src/carl-arith/ran/thom/ThomEvaluation.h
(edited this because the two files were swapped in the original)
I have tracked this down to some extent:
The file smtrat/src/smtrat-analyzer/analyzers/cad_projections.cpp references RealAlgebraicNumber but does not include the definition of this template class. The reference appears in src/smtrat/src/smtrat-cad/common.h
I think perhaps that file needs #include <carl-arith/ran/thom/ThomRootFinder.h> to get the definition it needs of RealAlgebraicNumber .
Unfortunately, adding that include directive, while it does fix the above problem, introduces 2 new errors:
/home/rpg/src/smtrat/src/smtrat-cad/projection/Projection_Model.h:91:54: error: operands to ?: have different types ‘smtrat::cad::RAN {aka carl::RealAlgebraicNumber<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> >}’ and ‘const RootType {aka const carl::IntRepRealAlgebraicNumber<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> >}’
RAN value = val.isRational() ? RAN(val.asRational()) : val.asRAN();
~~~~~~~~~~~~~~~~~^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
I don't know for sure, but it seems like there might be a relationship between the types carl::RealAlgebraicNumber and carl::IntRepRealAlgebraicNumber that the compiler does not know about (just judging from the names).
/home/rpg/src/smtrat/src/smtrat-cad/projection/Projection_Model.h:107:54: required from here
/usr/include/c++/7/bits/stl_pair.h:214:11: error: ‘std::pair<_T1, _T2>::first’ has incomplete type
_T1 first; /// @c first is a copy of the first object
^~~~~
In file included from /home/rpg/src/smtrat/src/smtrat-cad/common.h:3:0,
from /home/rpg/src/smtrat/src/smtrat-analyzer/analyzers/cad_projections.cpp:5:
/home/rpg/src/smtrat/build/resources/src/CArL-EP/src/carl-arith/ran/thom/ThomRootFinder.h:21:7: note: declaration of ‘class carl::RealAlgebraicNumber<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> >’
class RealAlgebraicNumber;
^~~~~~~~~~~~~~~~~~~
I don't understand this error message, either, but could it be because Projection_Model.h needs to include the headers from GMP and MPQ?
Clang gives slightly different messages and finds three errors instead of two:
In file included from /home/rpg/src/smtrat/src/smtrat-analyzer/analyzers/cad_projections.cpp:7:
In file included from /home/rpg/src/smtrat/src/smtrat-cad/projection/Projection.h:29:
/home/rpg/src/smtrat/src/smtrat-cad/projection/Projection_Model.h:91:29: error:
implicit instantiation of undefined template
'carl::RealAlgebraicNumber<__gmp_expr<mpq_t, mpq_t> >'
RAN value = val.isRational() ? RAN(val.asRational()) : v...
^
/home/rpg/src/smtrat/build/resources/src/CArL-EP/src/carl-arith/ran/thom/ThomRootFinder.h:21:7: note:
template is declared here
class RealAlgebraicNumber;
^
In file included from /home/rpg/src/smtrat/src/smtrat-analyzer/analyzers/cad_projections.cpp:1:
In file included from /home/rpg/src/smtrat/src/smtrat-analyzer/analyzers/variables.h:3:
In file included from /home/rpg/src/smtrat/src/smtrat-analyzer/analyzers/../statistics.h:3:
In file included from /home/rpg/src/smtrat/src/smtrat-common/statistics/Statistics.h:4:
In file included from /home/rpg/src/smtrat/build/resources/src/CArL-EP/src/carl-statistics/Statistics.h:3:
In file included from /home/rpg/src/smtrat/build/resources/src/CArL-EP/src/carl-statistics/StatisticsCollector.h:5:
In file included from /usr/bin/../lib/gcc/x86_64-linux-gnu/7.5.0/../../../../include/c++/7.5.0/memory:62:
In file included from /usr/bin/../lib/gcc/x86_64-linux-gnu/7.5.0/../../../../include/c++/7.5.0/bits/stl_algobase.h:64:
/usr/bin/../lib/gcc/x86_64-linux-gnu/7.5.0/../../../../include/c++/7.5.0/bits/stl_pair.h:214:11: error:
implicit instantiation of undefined template
'carl::RealAlgebraicNumber<__gmp_expr<mpq_t, mpq_t> >'
_T1 first; /// @c first is a copy of the first object
^
/usr/bin/../lib/gcc/x86_64-linux-gnu/7.5.0/../../../../include/c++/7.5.0/type_traits:1409:4: note:
in instantiation of template class
'std::pair<carl::RealAlgebraicNumber<__gmp_expr<mpq_t, mpq_t> >, bool>' requested
here
__is_trivially_constructible(_Tp, const _Tp&)>>
^
/usr/bin/../lib/gcc/x86_64-linux-gnu/7.5.0/../../../../include/c++/7.5.0/optional:104:8: note:
in instantiation of template class
'std::is_trivially_copy_constructible<std::pair<carl::RealAlgebraicNumber<__gmp_expr<mpq_t,
mpq_t> >, bool> >' requested here
is_trivially_copy_constructible<_Tp>::value
^
/usr/bin/../lib/gcc/x86_64-linux-gnu/7.5.0/../../../../include/c++/7.5.0/optional:425:7: note:
in instantiation of default argument for
'_Optional_payload<std::pair<carl::RealAlgebraicNumber<__gmp_expr<mpq_t, mpq_t> >,
bool> >' required here
_Optional_payload<_Tp> _M_payload;
^~~~~~~~~~~~~~~~~~~~~~
/usr/bin/../lib/gcc/x86_64-linux-gnu/7.5.0/../../../../include/c++/7.5.0/optional:454:15: note:
in instantiation of template class
'std::_Optional_base<std::pair<carl::RealAlgebraicNumber<__gmp_expr<mpq_t, mpq_t>
>, bool> >' requested here
: private _Optional_base<_Tp>,
^
/home/rpg/src/smtrat/src/smtrat-cad/projection/Projection_Model.h:103:68: note: in
instantiation of template class
'std::optional<std::pair<carl::RealAlgebraicNumber<__gmp_expr<mpq_t, mpq_t> >,
bool> >' requested here
std::optional<std::pair<RAN,bool>> lower;
^
/home/rpg/src/smtrat/build/resources/src/CArL-EP/src/carl-arith/ran/thom/ThomRootFinder.h:21:7: note:
template is declared here
class RealAlgebraicNumber;
^
In file included from /home/rpg/src/smtrat/src/smtrat-analyzer/analyzers/cad_projections.cpp:1:
In file included from /home/rpg/src/smtrat/src/smtrat-analyzer/analyzers/variables.h:3:
In file included from /home/rpg/src/smtrat/src/smtrat-analyzer/analyzers/../statistics.h:3:
In file included from /home/rpg/src/smtrat/src/smtrat-common/statistics/Statistics.h:4:
In file included from /home/rpg/src/smtrat/build/resources/src/CArL-EP/src/carl-statistics/Statistics.h:6:
In file included from /usr/bin/../lib/gcc/x86_64-linux-gnu/7.5.0/../../../../include/c++/7.5.0/map:60:
In file included from /usr/bin/../lib/gcc/x86_64-linux-gnu/7.5.0/../../../../include/c++/7.5.0/bits/stl_tree.h:72:
In file included from /usr/bin/../lib/gcc/x86_64-linux-gnu/7.5.0/../../../../include/c++/7.5.0/bits/node_handle.h:39:
/usr/bin/../lib/gcc/x86_64-linux-gnu/7.5.0/../../../../include/c++/7.5.0/optional:716:22: error:
no member named '_M_is_engaged' in
'std::optional<std::pair<carl::RealAlgebraicNumber<__gmp_expr<mpq_t, mpq_t> >,
bool> >'
{ return this->_M_is_engaged(); }
~~~~ ^
/home/rpg/src/smtrat/src/smtrat-cad/projection/Projection_Model.h:117:54: note: in
instantiation of member function
'std::optional<std::pair<carl::RealAlgebraicNumber<__gmp_expr<mpq_t, mpq_t> >,
bool> >::operator bool' requested here
if (!upper || root < upper->first) {
^
3 errors generated.
I checked out release 22.06 instead of master, but I found the same error: src/smtrat-cad/common.h references carl::RealAlgebraicNumber but it is not defined. As before, when I modify this header file to include the Carl header defining RealAlgebraicNumber, I get new errors (the same as described above).
I have had a colleague who is more adept at C++ than I am have a look at this, too, and he wasn't able to get any further. It really seems that somehow the code in the GitHub repositories is defective. Is there any chance that there is a substantial difference in your internal development environment, or that there is some defect in the process of exporting from your internal repository to GitHub?
SMT-RAT is pulling the wrong CArL version. We will release a new version of SMT-RAT soon, such that this problem does not occur anymore.
Meanwhile, you could first download an older version of CArL (matching the version number of SMT-RAT), build it locally and then build SMT-RAT (the carl_DIR parameter needs to be set accordingly).
@derjasper -- what is the right syntax for setting the carl_DIR parameter and to what should it be set? Should it be set to the carl git working directory, or to the build/ directory inside the git working directory?
I think what my experience clearly shows is the need for a GitHub action like the one I have added to my fork. Such an action will show whether or not a release on GitHub can be built successfully. My experience demonstrates that builds can be successful at Aachen even when the GitHub release cannot be built successfully.