大黄蜂 SAT 求解器编译

我试图从 http://amit.metodi.me/research/bee/编译大黄蜂卫星求解器。我已经安装了SWI-Prolog和MinGW，但是在cmd中键入"make-minisat"后，我得到：

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++ 无法访问 prolog 头文件。有什么想法吗？我致力于 win 10、64 位。

Windows10有一个测试版功能，称为WSL(Linux的Windows子系统(，或Windows上的Bash，或Windows上的Ubuntu上的Bash。

Bash on Windows 为开发人员提供了一个熟悉的 Bash shell和可以在其中运行大多数 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，或使用SuperUser标签windows-subsystem-linux。

我最初用它来解决这个问题。

您需要阅读主页左侧注明的所有页面。

面包屑

根据安装指南
使用 Windows 10 安装 WSL 使用正确的指令集：
For Anniversary Update and Creators Update: Install using lxrun

注意：其余说明在 WSL 或从 WSL 运行的应用中完成

安装 gcc
sudo apt-get -y install build-essential
安装 SWI-Prolog - 二手 PPA
在我的系统上为 Bee
mkdir Bee
创建目录是 eric@WINDOWS：~/projects/Bee$
更改为蜜蜂目录
cd ~/projects/Bee
下载蜜蜂
wget http://amit.metodi.me/research/bee/bee20170615.zip
解压缩压缩 zip
我安装并使用了 7-Zip
sudo apt-get install p7zip-full
7z x bee20170615.zip
更改为源代码目录
cd satsolver_src
阅读自述文件
.txt
使用 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$

验证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$

运行自述文件中
的第一个示例.txtswipl
[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.

面包屑

相关内容

最新更新

热门标签：