sambayless / monosat

MonoSAT - An SMT solver for Monotonic Theories
MIT License
106 stars 29 forks source link

Can't build on OSX #7

Closed seanmcl closed 6 years ago

seanmcl commented 6 years ago

I'm having trouble building on OSX. I've brew installed gmp and cmake. It makes it all the way to the linking step, but then can't find my gmp (I think)

[ 47%] Linking CXX executable monosat
/usr/local/Cellar/cmake/3.11.0/bin/cmake -E cmake_link_script CMakeFiles/monosat_static.dir/link.txt --verbose=1
/usr/local/bin/g++-7  -fopenmp  -DNO_GMP -std=c++11 -Wno-unused-variable -Wno-unused-but-set-variable   -Wno-sign-compare  -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -O3 -DNDEBUG -DNDEBUG -O3 -Wl,-search_paths_first -Wl,-headerpad_max_install_names  CMakeFiles/monosat_static.dir/src/monosat/Main.cc.o  -o monosat libmonosat.a -lz -lm -lgmpxx -lgmp
Undefined symbols for architecture x86_64:
  "operator<<(std::basic_ostream<char, std::char_traits<char> >&, __mpq_struct const*)", referenced from:
      dgl::DynamicGraph<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> >::setEdgeWeight(int, __gmp_expr<__mpq_struct [1], __mpq_struct [1]> const&) in Main.cc.o
      dgl::DynamicGraph<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> >::addEdge(int, int, int, __gmp_expr<__mpq_struct [1], __mpq_struct [1]>) in Main.cc.o
      std::basic_ostream<char, std::char_traits<char> >& operator<< <2u, __gmp_expr<__mpq_struct [1], __mpq_struct [1]> >(std::basic_ostream<char, std::char_traits<char> >&, ConvexPolygon<2u, __gmp_expr<__mpq_struct [1], __mpq_struct [1]> >&) in Main.cc.o
      std::basic_ostream<char, std::char_traits<char> >& operator<< <2u, __gmp_expr<__mpq_struct [1], __mpq_struct [1]> >(std::basic_ostream<char, std::char_traits<char> >&, Point<2u, __gmp_expr<__mpq_struct [1], __mpq_struct [1]> > const&) in Main.cc.o
      Monosat::BVTheorySolver<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> >::newComparison(Monosat::Comparison, int, __gmp_expr<__mpq_struct [1], __mpq_struct [1]> const&, int, bool) in Main.cc.o
      ConvexHullDetector<2u, __gmp_expr<__mpq_struct [1], __mpq_struct [1]> >::checkSatisfied() in Main.cc.o
      Monosat::BVTheorySolver<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> >::writeBounds(int) in Main.cc.o
      ...
  "operator>>(std::basic_istream<char, std::char_traits<char> >&, __mpq_struct*)", referenced from:
      Monosat::GeometryParser<char*, Monosat::SimpSolver, __gmp_expr<__mpq_struct [1], __mpq_struct [1]> >::readConvexHullArea(char*&, Monosat::SimpSolver&) in Main.cc.o
ld: symbol(s) not found for architecture x86_64
collect2: error: ld returned 1 exit status
make[2]: *** [monosat] Error 1
make[1]: *** [CMakeFiles/monosat_static.dir/all] Error 2
make: *** [all] Error 2

I know next to nothing about CMAKE. I tried

$ DYLD_LIBRARY_PATH=$DYLD_LIBRARY_PATH:/opt/local/lib make
$ LD_LIBRARY_PATH=$LD_LIBRARY_PATH:/opt/local/lib make 

Both failed. Any advice?

Thanks!

sambayless commented 6 years ago

I don't think you are doing anything wrong with CMake. There are two likely sources for this error message, both involving GMP.

Monosat uses the C++ bindings for GMP, which are not always installed by default. If you were building GMP from source you would need to use the --enable-cxx build option, but I would expect brew to install with that enabled by default. Monosat also needs a fairly recent version of GMP (version 5 may work, version 6 should definitely work).

In this case, it looks like the error may be arising during static linking. Monosat compiles the shared library (libmonosat) with dynamic linking, but compiles the monosat binary with static linkage (by default). In this case, the error is occurring during the static linking step, which means that either brew's gmp did not include the static GMP library (eg, libgmp.a, libgmpxx.a), or did include it but it is not on the build path.

On Linux at least, the static (not shared) library path is held in the LIBRARY_PATH environment variable, rather than the LD_LIBRARY_PATH environment variable. If brew installs static library archives to /opt/local/lib, then try setting LIBRARY_PATH=$LIBRARY_PATH:/opt/local/lib make

You may also need to specify the above before calling cmake, eg LIBRARY_PATH=$LIBRARY_PATH:/opt/local/lib cmake .

Another option is to compile the monosat binary with dynamic rather than static linkage. You should be able to build just the shared library or just the shared binary with:

cmake --target libmonosat . or cmake --target monosat .

If the source of the problem is that brew installed only the dynamic libraries and not the static libraries, then this is an easy work around. If the problem is that brew didn't install the c++ bindings at all, then you will need to manually compile gmp yourself.

sambayless commented 6 years ago

To follow up on this, it does seem that brew installs both the dynamic and static libraries, including C++ bindings. So the problem is likely that either cmake or make cannot find those libraries.

You can check where brew installed gmp (and hence what path to add to the various X_LIBRARY_PATH variables) using $brew --prefix gmp

On my machine at least, the libraries libgmp.a, libgmpxx.a, libgmp.dylib, libgmpxx.dylib were installed to /usr/local/opt/gmp/lib rather than /opt/local/lib

seanmcl commented 6 years ago

LIBRARY_PATH=$LIBRARY_PATH:/opt/local/lib make worked for me. Thanks!