sat - 如何在 Mac 上编译葡萄糖 SAT 求解器？

Question

当我在 Mac 上编译葡萄糖 SAT 求解器时，在编译葡萄糖 3.0 时出现以下编译时错误。如何避免这些错误？

~/acl2/glucose-3.0/simp$ make
Making dependencies
Compiling: /Users/me/acl2/glucose-3.0/simp/Main.o
In file included from /Users/me/acl2/glucose-3.0/simp/Main.cc:39:
In file included from /Users/me/acl2/glucose-3.0/simp/../core/Dimacs.h:27:
/Users/me/acl2/glucose-3.0/simp/../core/SolverTypes.h:58:16: error:
      friend declaration specifying a default argument must be a definition
    friend Lit mkLit(Var var, bool sign = false);
               ^
<snip>                                                                       
6 errors generated.
make: *** [/Users/me/acl2/glucose-3.0/simp/Main.o] Error 1
~/acl2/glucose-3.0/simp$

Answer 1

此解决方案归功于 Marijn Heule：

修改您的葡萄糖源代码以适应以下更改：

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; }

顶部 (<) 是 Mac 版本，底部 (>) 是默认源。