CODEWITHSUNDEEP
prologartificial-intelligenceswi-prologsatsat-solvers
wizzardm
wizzardm

Reputation: 29

BumbleBEE SAT-solver compilation

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.

Upvotes: 1

Views: 399

Answers (1)

Guy Coder
Guy Coder

Reputation: 24976

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

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

  2. Install SWI-Prolog - used PPA

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

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

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

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

  7. Change to the source code directory
    cd satsolver_src

  8. Read README.txt

  9. 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$
  1. 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$
  1. 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.

Upvotes: 3

Related Questions