Компиляция SAT-решателя BumbleBEE

Я пытаюсь скомпилировать спутниковый решатель шмеля из http://amit.metodi.me/research/bee/ . Я уже установил SWI-Prolog и MinGW, но после ввода «make-minisat» в cmd я получаю:

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

Похоже, что g++ не может получить доступ к файлам заголовков пролога. Любые идеи? Работаю на вин 10, 64 бита.


person wizzardm    schedule 30.07.2017    source источник
comment
Это известная проблема в minisat. В качестве обходного пути вы можете окружить макрос PRi64 пробелами. Он определен во включаемом файле inttypes.h. Если нет, определите сами. Чтобы исправить ошибку undefined reference, вы должны сообщить компоновщику, какие библиотеки он должен добавить.   -  person Axel Kemper    schedule 01.08.2017


Ответы (1)


В Windows 10 есть бета-функция, известная как WSL (подсистема Windows для Linux), или Bash для Windows, или Bash для Ubuntu в Windows.

Bash для Windows предоставляет разработчикам знакомую оболочку Bash и среду Linux, в которой вы можете запускать большинство инструментов командной строки Linux, непосредственно в Windows, БЕЗ ИЗМЕНЕНИЙ, без необходимости использования всей виртуальной машины Linux!

Я использовал его для установки SWI-Prolog и запуска некоторых моих собственных программ Prolog. AFAIK Я мог бы быть единственным на планете, кто сделал это.

Я установил его с помощью
PPA
или
sudo apt-get install swi-prolog-nox -y.
PPA устанавливает более новую версию.

Планируйте потратить около часа с момента начала до момента, когда все будет установлено и обновлено, поскольку вы буквально загружаете и устанавливаете Ubuntu и все приложения с нуля.

Руководство по установке WSL находится здесь.

Вероятно, вы не участвуете в программе предварительной оценки Windows, поэтому НЕ следуйте For Windows Insiders: Install Linux distribution of choice, а вместо этого следуйте For Anniversary Update and Creators Update: Install using lxrun.

Если у вас возникнут проблемы, я могу вам помочь, или вы можете опубликовать вопросы на странице вопросов GitHub или использовать тег SO wsl или используйте тег Ask Ubuntu wsl или используйте тег суперпользователя windows-subsystem-linux.

Сначала я использовал его для этой проблемы.

Вам необходимо прочитать все страницы, указанные слева от домашней страницы.

Панировочные сухари

  1. Используя Windows 10, установите WSL в соответствии с руководством по установке
    . набор инструкций:
    For Anniversary Update and Creators Update: Install using lxrun

Примечание. Остальные инструкции выполняются в WSL или в приложении, запускаемом из WSL.

  1. Установить gcc
    sudo apt-get -y install build-essential

  2. Установите SWI-Prolog — используется PPA

  3. Создайте каталог для Bee
    mkdir Bee
    В моей системе это eric@WINDOWS:~/projects/Bee$

  4. Перейдите в каталог Bee
    cd ~/projects/Bee

  5. Скачать Би
    wget http://amit.metodi.me/research/bee/bee20170615.zip

  6. Распаковать zip
    Я установил и использовал 7-Zip
    sudo apt-get install p7zip-full
    7z x bee20170615.zip

  7. Перейдите в каталог исходного кода
    cd satsolver_src

  8. Читать README.txt

  9. Создание решателей с помощью 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. Проверка созданных исполняемых файлов
    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. Запустите первый пример из 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.

person Guy Coder    schedule 30.07.2017