macOSX 10.15.2 Minisat Error

[Kevin Silken]

Hi,

I downloaded minisat-2.2.0.tar.gz, extracted it and started following the directions. My command lines are:

export MROOT=minisat

cd core

make rs

Makefile:4: minisat/mtl/template.mk: No such file or directory

make: *** No rule to make target `minisat/mtl/template.mk'.  Stop.

Any suggestions?

[keith....@bt.com]

Was MROOT an absolute path?

Another thing which needs fixing in the source is lots of warning like this:

minisat/utils/Options.h:293:25: warning: invalid suffix on literal; C++11 requires a space between literal and string macro [-Wliteral-suffix]
         fprintf(stderr, "] (default: %"PRIi64")\n", value);

Keith

---

From: min...@googlegroups.com <min...@googlegroups.com> on behalf of Kevin Silken <kasi...@gmail.com>
Sent: 04 February 2020 21:01
To: MiniSat
Subject: macOSX 10.15.2 Minisat Error

 

--

---
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.
To view this discussion on the web visit https://groups.google.com/d/msgid/minisat/e6f59ef9-0316-4e7c-8092-01adadae5c0f%40googlegroups.com.

[Kevin Silken]

I don't know. What should I do to check?

On Wednesday, February 5, 2020 at 6:19:48 AM UTC-8, kbriggs wrote:

Was MROOT an absolute path?

Another thing which needs fixing in the source is lots of warning like this:

minisat/utils/Options.h:293:25: warning: invalid suffix on literal; C++11 requires a space between literal and string macro [-Wliteral-suffix]
         fprintf(stderr, "] (default: %"PRIi64")\n", value);

Keith

---

From: min...@googlegroups.com <min...@googlegroups.com> on behalf of Kevin Silken <kasi...@gmail.com>
Sent: 04 February 2020 21:01
To: MiniSat
Subject: macOSX 10.15.2 Minisat Error

 

Hi,

I downloaded minisat-2.2.0.tar.gz, extracted it and started following the directions. My command lines are:

export MROOT=minisat

cd core

make rs

Makefile:4: minisat/mtl/template.mk: No such file or directory

make: *** No rule to make target `minisat/mtl/template.mk'.  Stop.

Any suggestions?

--

---
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 min...@googlegroups.com.

[Allen Van Gelder]

It appears from the snippet that the answer is: MROOT is NOT an absolute path.

Here is a note to myself in the README file from way back, which suggests
MROOT must be the appropriate absolute path.

==================================================================
export MROOT=<minisat-dir> (or setenv in cshell)
By AVG: in csh in the same dir as this README do
setenv MROOT `pwd`
THEN continue as below.
==================================================================

I do not know how to say `pwd` in bash.

--Allen

>
> On Wednesday, February 5, 2020 at 6:19:48 AM UTC-8, kbriggs wrote:
>>
>> Was MROOT an absolute path?
>>

. . .

>> Keith
>>
>> ________________________________
>> From: min...@googlegroups.com <min...@googlegroups.com> on behalf of Kevin Silken <kasi...@gmail.com>

. . .

[Kevin Silken]

My Makefile error seems to have been sorted by using the following command line, but I've run into more errors:

export MROOT=$PWD

cd core

make r

Linking: minisat_release ( core/Main.or core/Solver.or utils/Options.or utils/System.or )

ld: warning: ignoring file /usr/local/lib/libz.dylib, building for macOS-x86_64 but attempting to link with file built for unknown-i386

Undefined symbols for architecture x86_64:

  "_gzclose", referenced from:

      _main in Main.or

  "_gzdopen", referenced from:

      _main in Main.or

  "_gzopen", referenced from:

      _main in Main.or

  "_gzread", referenced from:

      _main in Main.or

      int Minisat::parseInt<Minisat::StreamBuffer>(Minisat::StreamBuffer&) in Main.or

ld: symbol(s) not found for architecture x86_64

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

make: *** [minisat_release] Error 1

Someone suggested in another thread to link with libz so I downloaded libzdb from homebrew.

Then I tried the following, but I don't know if I'm doing this correctly:

make -lz

--Kevin

[Obilade Titilayo]

make r for mac. besides, try to update your software

To unsubscribe from this group and stop receiving emails from it, send an email to minisat+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/minisat/4ad1d410-cd69-436e-b941-a389854430e4%40googlegroups.com.

[Kevin Silken]

I've been using make r. Can you elaborate more on updating my software?

--Kevin

To view this discussion on the web visit https://groups.google.com/d/msgid/minisat/4ad1d410-cd69-436e-b941-a389854430e4%40googlegroups.com.

[Obilade Titilayo]

As in your pc software to the latest version

To unsubscribe from this group and stop receiving emails from it, send an email to minisat+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/minisat/3321c9a9-d7cf-446b-b7ae-974c95826beb%40googlegroups.com.

[Kevin Silken]

I was able to resolve my errors and run minisat. In order to run it on macOS Catalina Version 10.15.3, I needed to modify SolverTypes.h and System.cc to correct the friend declaration errors (modifications can be found by using your favorite search engine) and uninstall/reinstall libz to correct the 'lib is installed as i386, needs to be built for x86-64' error.

The procedure for libz was to download zlib from its webpage and extract it, then navigate in terminal to its extract location and enter:

sudo rm/opt/local/lib/libz*

./configure

make

sudo make install

Now we can continue with the typical directions. Navigating to the extracted minisat folder:

export MROOT=$PWD

cd core

make r

This creates a unix executable in core. To test a simple case, double click the executable, type 0, press enter, press ctrl d, and it exits with unsat.

To specify and test a cnf file, in the terminal enter:

./minisat_release input_file output_file

where the input file is your cnf and the output file you can name whatever you want. If the input is satisfiable, the output gives a case.

--Kevin

To view this discussion on the web visit https://groups.google.com/d/msgid/minisat/3321c9a9-d7cf-446b-b7ae-974c95826beb%40googlegroups.com.

[Allen Van Gelder]

One thing to think about is choosing rs instead of r.
As I recall rs makes a "static" that can run in environments
that do not have the matching dynamic libraries , which
the "r" version needs to find at run time.

I have only linux experience with minisat. Maybe someone
with mac experience can comment on mac issues with "static"
in gcc etc.

--Allen

> To unsubscribe from this group and stop receiving emails from it, send an email to minisat+u...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/minisat/9c05b923-56cf-40cb-b95e-25acbef60891%40googlegroups.com.