Declaration of mkLit breaks compilation on OS X (with clang-503.0.40)

[fniksic]

When building minisat on OS X, with clang-503.0.40, the compilation breaks with the following error:

Compiling: build/release/minisat/simp/Main.o
In file included from minisat/simp/Main.cc:27:
In file included from ./minisat/core/Dimacs.h:27:
./minisat/core/SolverTypes.h:55:16: error: friend declaration specifying a default argument must be a definition
    friend Lit mkLit(Var var, bool sign = false);
               ^
./minisat/core/SolverTypes.h:63:14: error: friend declaration specifying a default argument must be the only declaration
inline  Lit  mkLit     (Var var, bool sign) { Lit p; p.x = var + var + (int)sign; return p; }
             ^
./minisat/core/SolverTypes.h:55:16: note: previous declaration is here
    friend Lit mkLit(Var var, bool sign = false);
               ^
In file included from minisat/simp/Main.cc:27:
./minisat/core/Dimacs.h:43:39: error: use of undeclared identifier 'mkLit'
        lits.push( (parsed_lit > 0) ? mkLit(var) : ~mkLit(var) );
                                      ^
./minisat/core/Dimacs.h:43:53: error: use of undeclared identifier 'mkLit'
        lits.push( (parsed_lit > 0) ? mkLit(var) : ~mkLit(var) );
                                                    ^
In file included from minisat/simp/Main.cc:28:
./minisat/simp/SimpSolver.h:117:70: error: use of undeclared identifier 'mkLit'
        uint64_t cost  (Var x)        const { return (uint64_t)n_occ[mkLit(x)] * (uint64_t)n_occ[~mkLit(x)]; }
                                                                     ^
./minisat/simp/SimpSolver.h:117:99: error: use of undeclared identifier 'mkLit'
        uint64_t cost  (Var x)        const { return (uint64_t)n_occ[mkLit(x)] * (uint64_t)n_occ[~mkLit(x)]; }
                                                                                                  ^
6 errors generated.
make: *** [build/release/minisat/simp/Main.o] Error 1

The issue seems to be with the friend declaration of mkLit within the structure Lit, which specifies a default value. According to ISO C++11 standard, such a declaration is illegal:

"If a friend declaration specifies a default argument expression, that declaration shall be a definition and shall be the only declaration of the function or function template in the translation unit.”

An obvious fix is to remove the declaration, as there is no real reason for mkLit to be declared as friend. The default value should instead be specified in the definition of mkLit.

[zhzdeng]

1. syntax error

bash$ diff SolverTypes.h
~/Downloads/glucose-3.0/core/SolverTypes.h
58c58
<     // friend Lit mkLit(Var var, bool sign = false);
---
>     friend Lit mkLit(Var var, bool sign = false);
66c66
< inline  Lit  mkLit     (Var var, bool sign = false) { Lit p; p.x =
var + var + (int)sign; return p; }
---
> inline  Lit  mkLit     (Var var, bool sign) { Lit p; p.x = var + var + (int)sign; return p; }

2. link error
   Edit the file utils/System.cc to include the stub for memUsedPeak, patched code will look like this:

#elif defined(__APPLE__)
#include 

double Minisat::memUsed(void) {
   malloc_statistics_t t;
   malloc_zone_statistics(NULL, &t);
   return (double)t.max_size_in_use / (1024*1024); }
double Minisat::memUsedPeak(void) {return memUsed(); }
#else

[richardmzhang]

I just ran into this same issue. Is there any update on what I should do (just apply zhzdeng's patch?)

[liffiton]

The fastest solution is probably to clone one of the forks in which this issue (and a few others) has been fixed. agurfinkel/minisat should work, for example.

[MontyThibault]

This commit off of agurfinkel/minisat resolves OSX linking issues I faced.

MontyThibault/minisat@7184c66

[jannichorst]

The fastest solution is probably to clone one of the forks in which this issue (and a few others) has been fixed. agurfinkel/minisat should work, for example.

Think that worked for me too. Thanks!