MiniSat on Mac OS X 10.10.2

[Leo John Thomas]

Hi,

While trying to install MiniSat on Mac, the following error is being thrown. I've installed Xcode mentioned in the forum before trying to compile MiniSat. Any pointers on what could've gone wrong?

Thanks,

Leo

MiniSat version  : 2.2.0

Mac OS X version : 10.10.2

gcc Version      : 4.2.1

Error Message:

./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

[Michael Tautschnig]

Hello Leo,

You may wish to apply the attached patch to resolve this problem.

Best,
Michael

On Wed, Feb 18, 2015 at 7:39:41 -0800, Leo John Thomas wrote:
> Hi,
> While trying to install MiniSat on Mac, the following error is being
> thrown. I've installed Xcode mentioned in the forum before trying to
> compile MiniSat. Any pointers on what could've gone wrong?
>
> Thanks,
> Leo
>
>
> MiniSat version : 2.2.0
> Mac OS X version : 10.10.2
> gcc Version : 4.2.1
>
> Error Message:
>

> *./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
>
>
>
>

> --
>
> ---
> You received this message because you are subscribed to the Google Groups "MiniSat" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to minisat+u...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[Leo]

Thank you so much Michael, that helped me to compile it successfully!.. :)

One last question; is it possible to build a static binary; I've read negative replies in forums, still just checking.

These are the steps I've followed for anybody who's trying to do it.

1. make config

2. Apply the above patch                                                                                   

3. make this edit in utils/System.h:

   namespace Minisat {                                                                                    

                                                                                                          

   static inline double cpuTime(void); // CPU-time in seconds.                                            

                                                                                                          

   extern double memUsed();            // Memory in mega bytes (returns 0 for unsupported architectures).

   - extern double memUsedPeak(bool strictlyPeak = false); // Peak-memory in mega bytes (returns 0 for unsupported architectures).

   + extern double memUsedPeak(); // Peak-memory in mega bytes (returns 0 for unsupported architectures).

4. make this edit in Makefile

   ## Shared Library rule                                                                                 

   $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB).$(SOMAJOR).$(SOMINOR)$(SORELEASE)\                            

    $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB).$(SOMAJOR)\                                                  

    $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB):                                                             

           $(ECHO) Linking Shared Library: $@                                                             

           $(VERB) mkdir -p $(dir $@)                                                                     

   -       $(VERB) $(CXX) $(MINISAT_LDFLAGS) $(LDFLAGS) -o $@ -shared -Wl,-soname,$(MINISAT_DLIB).$(SOMAJOR) $^

   +       $(VERB) $(CXX) $(MINISAT_LDFLAGS) $(LDFLAGS) -o $@ -shared -Wl,-install_name,$(MINISAT_DLIB).$(SOMAJOR) $^

5. update DYLD_LIBRARY_PATH to point to minisat_install/lib/

[Michael Tautschnig]

> Thank you so much Michael, that helped me to compile it successfully!.. :)
> One last question; is it possible to build a static binary; I've read
> negative replies in forums, still just checking.
>

[...] (making things compile)

Building statically-linked binaries is discouraged on OS X (and I'm not quite
sure why you'd want to do so anyway). See this information from Apple:

https://developer.apple.com/library/mac/qa/qa1118/_index.html

Best,
Michael

[Leo]

Building statically-linked binaries is discouraged on OS X (and I'm not quite
sure why you'd want to do so anyway). See this information from Apple:

https://developer.apple.com/library/mac/qa/qa1118/_index.html

The reason behind trying to do so was to avoid the need to update/recompile incase of changes in these linked libraries. Understood from the thread that there could be issues one level inside on the system call itself. 

Thank you Michael for clarifying,

Leo

[Obilade Titilayo]

Good afternoon,

Please, I got the below error while trying to install the minisat on my mac! Help me out.

clang-4.0: error: linker command failed with exit code 1(use -v to see invocation)