Fix for compilation under OSX

[xoolive]

Please find enclosed a fix for compilation under OSX (clang compiler) The current version still compiles ok under Ubuntu.

About the corrections:

• makefiles (seems generated, you might want to fix something uphill...):
  • -L../lib: the directory does not exist, clang fails
  • -lrt does not seem necessary under Ubuntu; besides, the library is not implemented in OSX.
• in the source files:
  • sighandler_t does not exist in OSX, but the proposed fix works fine
  • int64_t is not equivalent to long under OSX (or Windows), see this gist
  • similar issues with time.h, fixed by falling back to the Windows switch
  • missing include of <string> caused compilation to fail with clang
• in the Python API:
  • some signatures were missing causing the bitvalue theory to segfault (except with operator <). All tests pass ok now.
  • I do not have permission to write in my /usr/local/lib (and use virtualenv for packages): I added some lines in setup.py and in the loading of the libmonosat.so in order to ship the DLL with the package. (which is somehow cleaner if you want to keep several versions, like stable, dev, etc.)

Now it works :smile:

[xoolive]

By the way, I didn't try your cross-compilation for Windows, but I doubt the DLL would be usable by Python 64 bits. The process for compiling with Python 64 bits is somewhat painful and I never managed it without the Microsoft SDK compiler something...

(Well, I see there are things to be tried here I may try that when I am old and bored :stuck_out_tongue_winking_eye: )

[sambayless]

Hey, thanks a ton! I will look through this and merge it in shortly.

Yes, Windows support has been problematic.

[sambayless]

Thank you, this clearly took a bit of time on your part, and is much appreciated! Merged into master.

One clarification: librt is needed, on Linux, for clock_gettime (in utils/System.h). clock_gettime is not available on OSX, so a less precise clock is being used on OSX/Windows (not used for anything except collecting performance stats for the solver, so this isn't a problem for end users).

So until I find a more elegant solution, I'm keeping the -lrt dependency for Linux, and adding some OSX specific builds that won't link to -lrt: OSX_ClangRelease and OSX_SharedLibrary. I believe I've made the necessary changes to your patch to setup.py/monosat_c.py to support these changes, though if you have an opportunity to test this on an actual mac, I'd certainly appreciate it.

[xoolive]

Sure, once you merge and add your corrections, I will definitely try on my Mac. About -lrt, it compiled fine without it on my Ubuntu, but you must be right, that may not be some fact to be relied on for any compiler!

[sambayless]

Thanks, merged!

[xoolive]

Works fine on my Mac, I just commented in the commits for one major mistake and some suggestions in the setup.py

[sambayless]

Great, thanks again!