BumbleBEE SAT-solver compilation

Question

Im trying to compile bumblebee sat-solver from http://amit.metodi.me/research/bee/. I have installed SWI-Prolog and MinGW already but after i type "make-minisat" in cmd i get:

A subdirectory or file ..\satsolver already exists.
In file included from Solver.h:27:0,
                 from pl-minisat.cpp:6:
../utils/Options.h:285:29: warning: invalid suffix on literal; C++11 requires a space between literal and string macro [-Wliteral-suffix]
             fprintf(stderr, "%4"PRIi64, range.begin);
                             ^
../utils/Options.h:291:29: warning: invalid suffix on literal; C++11 requires a space between literal and string macro [-Wliteral-suffix]
             fprintf(stderr, "%4"PRIi64, range.end);
                             ^
../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);
                         ^
In file included from ../core/Solver.h:27:0,
                 from Solver.cc:24:
../utils/Options.h:285:29: warning: invalid suffix on literal; C++11 requires a space between literal and string macro [-Wliteral-suffix]
             fprintf(stderr, "%4"PRIi64, range.begin);
                             ^
../utils/Options.h:291:29: warning: invalid suffix on literal; C++11 requires a space between literal and string macro [-Wliteral-suffix]
             fprintf(stderr, "%4"PRIi64, range.end);
                             ^
../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);
                         ^
pl-minisat.obj:pl-minisat.cpp:(.text+0x13): undefined reference to `PL_get_integer'
pl-minisat.obj:pl-minisat.cpp:(.text+0x4d): undefined reference to `Sdprintf'
pl-minisat.obj:pl-minisat.cpp:(.text+0x76): undefined reference to `Sdprintf'
pl-minisat.obj:pl-minisat.cpp:(.text+0x18a): undefined reference to `PL_unify_integer'
pl-minisat.obj:pl-minisat.cpp:(.text+0x1b4): undefined reference to `PL_get_integer'
pl-minisat.obj:pl-minisat.cpp:(.text+0x1ed): undefined reference to `PL_unify_integer'
pl-minisat.obj:pl-minisat.cpp:(.text+0x220): undefined reference to `PL_copy_term_ref'
pl-minisat.obj:pl-minisat.cpp:(.text+0x227): undefined reference to `PL_new_term_ref'
pl-minisat.obj:pl-minisat.cpp:(.text+0x23c): undefined reference to `PL_unify_integer'
pl-minisat.obj:pl-minisat.cpp:(.text+0x24f): undefined reference to `PL_get_list'
pl-minisat.obj:pl-minisat.cpp:(.text+0x271): undefined reference to `PL_unify_integer'
pl-minisat.obj:pl-minisat.cpp:(.text+0x298): undefined reference to `PL_new_term_ref'
pl-minisat.obj:pl-minisat.cpp:(.text+0x29f): undefined reference to `PL_new_term_ref'
pl-minisat.obj:pl-minisat.cpp:(.text+0x2a9): undefined reference to `PL_put_nil'
pl-minisat.obj:pl-minisat.cpp:(.text+0x2ec): undefined reference to `PL_put_integer'
pl-minisat.obj:pl-minisat.cpp:(.text+0x2ff): undefined reference to `PL_cons_list'
pl-minisat.obj:pl-minisat.cpp:(.text+0x314): undefined reference to `PL_unify'
pl-minisat.obj:pl-minisat.cpp:(.text+0x33e): undefined reference to `Sdprintf'
pl-minisat.obj:pl-minisat.cpp:(.text+0x38d): undefined reference to `Sdprintf'
pl-minisat.obj:pl-minisat.cpp:(.text+0x3cb): undefined reference to `Sdprintf'
pl-minisat.obj:pl-minisat.cpp:(.text+0x3d7): undefined reference to `PL_register_extensions'
pl-minisat.obj:pl-minisat.cpp:(.text+0x3e3): undefined reference to `Sdprintf'
pl-minisat.obj:pl-minisat.cpp:(.text+0x44a): undefined reference to `PL_new_term_ref'
pl-minisat.obj:pl-minisat.cpp:(.text+0x457): undefined reference to `PL_copy_term_ref'
pl-minisat.obj:pl-minisat.cpp:(.text+0x47e): undefined reference to `PL_get_list'
pl-minisat.obj:pl-minisat.cpp:(.text+0x497): undefined reference to `PL_get_integer'
pl-minisat.obj:pl-minisat.cpp:(.text+0x51a): undefined reference to `PL_get_nil'
pl-minisat.obj:pl-minisat.cpp:(.text+0x5fa): undefined reference to `PL_new_term_ref'
pl-minisat.obj:pl-minisat.cpp:(.text+0x607): undefined reference to `PL_copy_term_ref'
pl-minisat.obj:pl-minisat.cpp:(.text+0x62e): undefined reference to `PL_get_list'
pl-minisat.obj:pl-minisat.cpp:(.text+0x647): undefined reference to `PL_get_integer'
pl-minisat.obj:pl-minisat.cpp:(.text+0x6ca): undefined reference to `PL_get_nil'
pl-minisat.obj:pl-minisat.cpp:(.text+0x808): undefined reference to `Sdprintf'
pl-minisat.obj:pl-minisat.cpp:(.text.startup+0x21): undefined reference to `PL_initialise'
pl-minisat.obj:pl-minisat.cpp:(.text.startup+0x31): undefined reference to `PL_halt'
pl-minisat.obj:pl-minisat.cpp:(.text.startup+0x36): undefined reference to `PL_toplevel'
pl-minisat.obj:pl-minisat.cpp:(.text.startup+0x46): undefined reference to `PL_halt'
collect2.exe: error: ld returned 1 exit status
g++ returned code 1
*** swipl-ld exit status 1

It looks like g++ can't reach prolog header files. Any ideas? I work on win 10, 64 bits.

Answer 1

There is a beta feature of Windows 10 know as WSL (Windows Subsystem for Linux), or Bash on Windows, or Bash on Ubuntu on Windows.

Bash on Windows provides developers with a familiar Bash shell and Linux environment in which you can run most Linux command-line tools, directly on Windows, UNMODIFIED, without needing an entire Linux virtual machine!

I have used it to install SWI-Prolog and run some of my own Prolog programs. AFAIK I might be the only one on the planet to have done this.

I have installed it using the
PPA
or
sudo apt-get install swi-prolog-nox -y.
The PPA installs a newer version.

Plan on spending about an hour from the time you start to the time you get everything installed and updated as you are literally downloading and installing Ubuntu and all the apps from the ground up.

The WSL installation guide is here.

You are probably not on the Windows insider program, so DO NOT follow For Windows Insiders: Install Linux distribution of choice but instead follow For Anniversary Update and Creators Update: Install using lxrun.

If you run into problems I can help you, or you can post issues on the GitHub issues page, or use the SO tag wsl, or use the Ask Ubuntu tag wsl, or use the SuperUser tag windows-subsystem-linux.

I initially used it for this problem.

You need to read all of the pages noted on the left of the home page.

Breadcrumbs

1. Using Windows 10 install WSL per installation guide
   Use the right instruction set:
   For Anniversary Update and Creators Update: Install using lxrun

Note: The rest of the instructions are done within WSL or an app run from WSL

2. Install gcc
   sudo apt-get -y install build-essential

3. Install SWI-Prolog - used PPA

4. Create directory for Bee
   mkdir Bee
   On my system it is eric@WINDOWS:~/projects/Bee$

5. Change to the Bee directory
   cd ~/projects/Bee

6. Download Bee
   wget http://amit.metodi.me/research/bee/bee20170615.zip

7. Uncompress zip
   I installed and used 7-Zip
   sudo apt-get install p7zip-full
7z x bee20170615.zip

8. Change to the source code directory
   cd satsolver_src

9. Read README.txt

10. Build solvers using make
    make satSolvers

eric@WINDOWS:~/projects/Bee/satsolver_src$ make satSolvers
rm -r -f ../satsolver
mkdir -p ../satsolver
tar xf ../satsolver_src/plSATsolver.tar.gz -C ../satsolver
tar -xf plMiniSAT_src.tar.gz -C ../satsolver
(cd ../satsolver/prologinterface && ./configure && make)
make[1]: Entering directory '/home/eric/projects/Bee/satsolver/prologinterface'
rm -f *.so
g++ -Wno-unused-result -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS -O3 -fomit-frame-pointer -s -shared -fpic -o pl-minisat.so pl-minisat.cpp \
../minisat-2.0.2/core/Solver.cc \
-L/usr/lib/swi-prolog/lib/amd64 \
-I /usr/lib/swi-prolog/include \
-I ../minisat-2.0.2/ \
-I ../minisat-2.0.2/core
make[1]: Leaving directory '/home/eric/projects/Bee/satsolver/prologinterface'
mv ../satsolver/prologinterface/pl-minisat.so ../satsolver/pl-minisat.so
rm -r -f ../satsolver/minisat-2.0.2
rm -r -f ../satsolver/prologinterface
tar xf ../satsolver_src/plGlucose_src.tar.gz -C ../satsolver
(cd ../satsolver/prologinterface && ./configure && make)
make[1]: Entering directory '/home/eric/projects/Bee/satsolver/prologinterface'
rm -f *.so
g++ -Wno-unused-result -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS -O3 -fomit-frame-pointer -s -shared -fpic -o pl-glucose.so pl-glucose.cpp \
../glucose-2.2/core/Solver.cc \
-L/usr/lib/swi-prolog/lib/amd64 \
-I /usr/lib/swi-prolog/include \
-I ../glucose-2.2/ \
-I ../glucose-2.2/core
make[1]: Leaving directory '/home/eric/projects/Bee/satsolver/prologinterface'
mv ../satsolver/prologinterface/pl-glucose.so ../satsolver/pl-glucose.so
rm -r -f ../satsolver/glucose-2.2
rm -r -f ../satsolver/prologinterface
tar xf ../satsolver_src/plGlucose4_src.tar.gz -C ../satsolver
(cd ../satsolver/prologinterface && ./configure && make)
make[1]: Entering directory '/home/eric/projects/Bee/satsolver/prologinterface'
rm -f *.so
g++ -Wno-unused-result -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS -O3 -fomit-frame-pointer -s -shared -fpic -o pl-glucose4.so pl-glucose4.cpp \
../glucose-4/core/Solver.cc \
-L/usr/lib/swi-prolog/lib/amd64 \
-I /usr/lib/swi-prolog/include \
-I ../glucose-4/ \
-I ../glucose-4/core
make[1]: Leaving directory '/home/eric/projects/Bee/satsolver/prologinterface'
mv ../satsolver/prologinterface/pl-glucose4.so ../satsolver/pl-glucose4.so
rm -r -f ../satsolver/glucose-4
rm -r -f ../satsolver/prologinterface
eric@WINDOWS:~/projects/Bee/satsolver_src$

11. Verify executables created
    cd ..
cd satsolver
ll

eric@WINDOWS:~/projects/Bee/satsolver$ ll
total 372
drwxrwxrwx 0 eric eric   4096 Jul 31 07:12 ./
drwxrwxrwx 0 eric eric   4096 Jul 31 07:11 ../
-rwxrwxrwx 1 eric eric 101200 Jul 31 07:12 pl-glucose4.so*
-rwxrwxrwx 1 eric eric  80656 Jul 31 07:12 pl-glucose.so*
-rwxrwxrwx 1 eric eric  68360 Jul 31 07:12 pl-minisat.so*
-rw-r--r-- 1 eric eric  10268 Apr  1  2016 satsolver.pl
eric@WINDOWS:~/projects/Bee/satsolver$

12. Run first example from README.txt
    swipl
[satsolver].
sat([[A,-B],[-A,B]]).

eric@WINDOWS:~/projects/Bee/satsolver$ swipl
Welcome to SWI-Prolog (threaded, 64 bits, version 7.4.2)
SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software.
Please run ?- license. for legal details.

For online help and background, visit http://www.swi-prolog.org
For built-in help, use ?- help(Topic). or ?- apropos(Word).

?- [satsolver].
% SWI-Prolog interface to Glucose v2.2 ... OK
true.

?- sat([[A,-B],[-A,B]]).
A = B, B = -1.