search

sambayless / monosat

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

#dynamic library builds on OSX Yosemite with clang #1

Closed lamestllama closed 9 years ago

lamestllama commented 9 years ago

Hi

I built this on OSX Yosemite with clang and got lots of warnings and a couple of small errors.

The warnings where pretty much all printf format errors using %d instead of %ld where a long was used.

The errors where a missing header file and a couple of conditional compilations around memUsedPeak() which doesnt exist on osx so the print stats methods in the solver will print 0 on OSX but work as before elsewhere.

There are now still 7 warnings but I have not yet decided the best way to solve them. They are hidden virtual function warnings.

Regards

Eric

lamestllama commented 9 years ago

I found out the problem with memUsedPeak() was that somebody had forgotten to implement one small part in system.cc for osx so I have included that now.

sambayless commented 9 years ago

Hey! Thanks a ton! Yes, the printf issues I knew about; but I've never tried building on Mac, so I am impressed you got it to work at all.

Did you use the clang makefiles (not mentioned in the readme), or did you modify the GCC ones? On Jul 30, 2015 9:18 PM, "Eric Parsonage" notifications@github.com wrote:

Hi

I built this on OSX Yosemite with clang and got lots of warnings and a couple of small errors.

The warnings where pretty much all printf format errors using %d instead of %ld where a long was used.

The errors where a missing header file and a couple of conditional compilations around memUsedPeak() which doesnt exist on osx so the print stats methods in the solver will print 0 on OSX but work as before elsewhere.

There are now still 7 warnings but I have not yet decided the best way to solve them. They are hidden virtual function warnings.

Regards

Eric

You can view, comment on, or merge this pull request online at:

https://github.com/sambayless/monosat/pull/1 Commit Summary

  • dynamic library builds on OSX with clang included included

    in one file and fixed many warning for incorrect printf formats also put a guard around memUsed function in the solvers print stats method because apple doesnt make such a function available

File Changes

Patch Links:

— Reply to this email directly or view it on GitHub https://github.com/sambayless/monosat/pull/1.

lamestllama commented 9 years ago

I used both:

The only warnings that the Clang makefiles produce are about a bunch of hidden overloaded virtual functions like 'Monosat::Solver::solve' which are declared with a different number of parameters.

I did not modify the GCC ones but they still build but for every file I get the same three warnings:

clang: warning: argument unused during compilation: '-static-libgcc' clang: warning: argument unused during compilation: '-static-libstdc++' warning: unknown warning option '-Wno-unused-but-set-variable'

and then the same warnings as the Clang files give.

I will probably work out how to fix the code to get rid of the warnings about overloaded hidden functions next.