Update CMakeLists.txt to compile with optimizations.

[PetterS]

minisat runs 10x faster on my system with this change.

[PetterS]

For this pull request, "my system" was Linux with gcc 4.4.

[PetterS]

Any thoughts?

[niklasso]

Hi Petter,

I have not had time to look at this unfortunately. A 10x difference is not
expected though for any differences in compile-parameters. Can you show
exactly which compile flags were used in the bad vs. good cases on your
machine?

I'm not going to merge architecture-specific compile flags I think, but if
there is something seriously wrong I'd like to fix that. Generally this
cmake-file is more intended to be included in other project make-files,
where more configuration options can be placed. See
https://github.com/niklasso/supermini for an example I used for my minisat
based software.

Thanks,
Niklas

On Tue, Jul 2, 2013 at 11:34 AM, Petter Strandmark <notifications@github.com

wrote:

Any thoughts?

—
Reply to this email directly or view it on GitHubhttps://github.com//pull/5#issuecomment-20335774
.

[PetterS]

I don't think a 10x difference is unreasonable. Without this change, no optimization at all is used. With this change, the speed of the binary compiled with CMake is the same or similar to the one with the Makefile (which uses -O3).

I just redid my benchmark:
With this change: 0.52592 s
Without this change: 4.83926 s

With g++ 4.7.2. cmake version 2.8.10

[niklasso]

I think you didn't configure with "Release" as the CMAKE_BUILD_TYPE. There
are a couple of default build types with reasonable flags (Debug, Release,
etc) that I assume user will either rely on, or if they include MiniSat it
in their own build-systems they can add more elaborate versions. Can you
try a release build and see if that works for you?

What is a worse problem though is the more recently introduced -D
MINISAT_CONSTANTS_AS_MACROS that produces worse code unless defined. I
guess is should preferably be a cmake configurable variable...

/Niklas

On Tue, Jul 2, 2013 at 5:26 PM, Petter Strandmark
notifications@github.comwrote:

I don't think a 10x difference is unreasonable. Without this change, no
optimization at all is used. With this change, the speed of the binary
compiled with CMake is the same or similar to the one with the Makefile
(which uses -O3).

I just redid my benchmark:
With this change: 0.52592 s
With this change: 4.83926 s

With g++ 4.7.2.

—
Reply to this email directly or view it on GitHubhttps://github.com//pull/5#issuecomment-20352975
.

[PetterS]

Yeah, the idea was to make "Release" the default build type if it was not specified.