Minisat-p_v1.14 installation on Mac

[Mahum Naseer]

Hi,

I am trying to install Minisat version 1.14 on macOS Mojave (version 10.14.6), but I get lots of compilation errors:

Macbook:MiniSat-p_v1.14 mahum$ make
Building minisat (standard)
Compiling: File.C
clang: warning: optimization flag '-ffloat-store' is not supported [-Wignored-optimization-argument]
In file included from File.C:1:
In file included from ./File.h:5:
./Global.h:195:43: error: implicit instantiation of undefined template
      'STATIC_ASSERTION_FAILURE<false>'
    vec<T>&  operator = (vec<T>& other) { TEMPLATE_FAIL; }
                                          ^
./Global.h:58:23: note: expanded from macro 'TEMPLATE_FAIL'
#define TEMPLATE_FAIL STATIC_ASSERTION_FAILURE<false>()
                      ^
./Global.h:56:24: note: template is declared here
template <bool> struct STATIC_ASSERTION_FAILURE;
                       ^
./Global.h:196:43: error: implicit instantiation of undefined template
      'STATIC_ASSERTION_FAILURE<false>'
             vec        (vec<T>& other) { TEMPLATE_FAIL; }
                                          ^
./Global.h:58:23: note: expanded from macro 'TEMPLATE_FAIL'
#define TEMPLATE_FAIL STATIC_ASSERTION_FAILURE<false>()
                      ^
./Global.h:56:24: note: template is declared here
template <bool> struct STATIC_ASSERTION_FAILURE;
                       ^
File.C:91:9: error: unknown type name 'uint'
        uint    v = (uint)val;
        ^
File.C:91:22: error: use of undeclared identifier 'uint'
        uint    v = (uint)val;
                     ^
File.C:91:27: error: expected ';' at end of declaration
        uint    v = (uint)val;
                          ^
                          ;
File.C:124:5: error: unknown type name 'uint'
    uint byte0, byte1, byte2, byte3, byte4, byte5, byte6, byte7;
    ^
File.C:126:19: error: use of undeclared identifier 'uint'
    if (byte0 == (uint)EOF)
                  ^
File.C:133:13: error: use of undeclared identifier 'byte1'; did you mean
      'byte0'?
            byte1 = in.getChar();
            ^~~~~
            byte0
File.C:124:10: note: 'byte0' declared here
    uint byte0, byte1, byte2, byte3, byte4, byte5, byte6, byte7;
         ^
File.C:134:44: error: use of undeclared identifier 'byte1'
            return ((byte0 & 0x1F) << 8) | byte1;
                                           ^
File.C:136:13: error: use of undeclared identifier 'byte1'; did you mean
      'byte0'?
            byte1 = in.getChar();
            ^~~~~
            byte0
File.C:124:10: note: 'byte0' declared here
    uint byte0, byte1, byte2, byte3, byte4, byte5, byte6, byte7;
         ^
File.C:137:13: error: use of undeclared identifier 'byte2'; did you mean
      'byte0'?
            byte2 = in.getChar();
            ^~~~~
            byte0
File.C:124:10: note: 'byte0' declared here
    uint byte0, byte1, byte2, byte3, byte4, byte5, byte6, byte7;
         ^
File.C:138:46: error: use of undeclared identifier 'byte1'; did you mean
      'byte0'?
            return ((byte0 & 0x1F) << 16) | (byte1 << 8) | byte2;
                                             ^~~~~
                                             byte0
File.C:124:10: note: 'byte0' declared here
    uint byte0, byte1, byte2, byte3, byte4, byte5, byte6, byte7;
         ^
File.C:138:60: error: use of undeclared identifier 'byte2'
            return ((byte0 & 0x1F) << 16) | (byte1 << 8) | byte2;
                                                           ^
File.C:140:13: error: use of undeclared identifier 'byte1'; did you mean
      'byte0'?
            byte1 = in.getChar();
            ^~~~~
            byte0
File.C:124:10: note: 'byte0' declared here
    uint byte0, byte1, byte2, byte3, byte4, byte5, byte6, byte7;
         ^
File.C:141:13: error: use of undeclared identifier 'byte2'; did you mean
      'byte0'?
            byte2 = in.getChar();
            ^~~~~
            byte0
File.C:124:10: note: 'byte0' declared here
    uint byte0, byte1, byte2, byte3, byte4, byte5, byte6, byte7;
         ^
File.C:142:13: error: use of undeclared identifier 'byte3'; did you mean
      'byte0'?
            byte3 = in.getChar();
            ^~~~~
            byte0
File.C:124:10: note: 'byte0' declared here
    uint byte0, byte1, byte2, byte3, byte4, byte5, byte6, byte7;
         ^
File.C:143:46: error: use of undeclared identifier 'byte1'; did you mean
      'byte0'?
            return ((byte0 & 0x1F) << 24) | (byte1 << 16) | (byte2 << 8...
                                             ^~~~~
                                             byte0
File.C:124:10: note: 'byte0' declared here
    uint byte0, byte1, byte2, byte3, byte4, byte5, byte6, byte7;
         ^
File.C:143:62: error: use of undeclared identifier 'byte2'; did you mean
      'byte0'?
  ...return ((byte0 & 0x1F) << 24) | (byte1 << 16) | (byte2 << 8) | byte3;
                                                      ^~~~~
                                                      byte0
File.C:124:10: note: 'byte0' declared here
    uint byte0, byte1, byte2, byte3, byte4, byte5, byte6, byte7;
         ^
File.C:143:76: error: use of undeclared identifier 'byte3'
  ...return ((byte0 & 0x1F) << 24) | (byte1 << 16) | (byte2 << 8) | byte3;
                                                                    ^
fatal error: too many errors emitted, stopping now [-ferror-limit=]
20 errors generated.
make: *** [File.o] Error 1

My gcc version is 4.2.1:

Macbook:MiniSat-p_v1.14 mahum$ gcc --version
Configured with: --prefix=/Library/Developer/CommandLineTools/usr --with-gxx-include-dir=/Library/Developer/CommandLineTools/SDKs/MacOSX10.14.sdk/usr/include/c++/4.2.1
Apple LLVM version 10.0.1 (clang-1001.0.46.4)
Target: x86_64-apple-darwin18.7.0
Thread model: posix
InstalledDir: /Library/Developer/CommandLineTools/usr/bin

It would be great if someone could help me with the following:

1. Is there a problem with the compatibility of my GCC version with Minisat v1.14?
2. The README with the p_v1.14 wasn’t very elaborate. Is there a prerequisite for installation that I could have missed? 
3. I want to use the proof-logging feature of Minisat. The Minisat available with home-brew is version 2.2.0, and from I understand from Minisat homepage, this one doesn’t have proof-logging. Is there another Minisat version with proof-logging that I could try installing instead?

Looking forward to any suggestions regarding installation.

Regards,

Mahum