【问题标题】:BumbleBEE SAT-solver compilationBumbleBEE SAT-solver 编译
【发布时间】:2017-07-30 21:19:32
【问题描述】:

我正在尝试从 http://amit.metodi.me/research/bee/ 编译 bumblebee sat-solver。我已经安装了 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 位上工作。

【问题讨论】:

  • 这是known issue 中的minisat。作为解决方法,您可以用空格将宏 PRi64 括起来。它在包含文件inttypes.h 中定义。如果没有,请自行定义。要修复undefined reference 错误,您必须告诉链接器它应该添加哪些库。

标签: prolog artificial-intelligence swi-prolog sat sat-solvers


【解决方案1】:

Windows 10 有一个测试版功能,称为 WSL(适用于 Linux 的 Windows 子系统),或 Windows 上的 Bash,或 Windows 上的 Ubuntu 上的 Bash。

Windows 上的 Bash 为开发人员提供了熟悉的 Bash shell 和 可以运行大多数 Linux 命令行工具的 Linux 环境, 直接在 Windows 上,未修改,不需要整个 Linux 虚拟机!

我已经用它来installSWI-Prolog 并运行我自己的一些 Prolog 程序。 AFAIK 我可能是这个星球上唯一这样做的人。

我已经使用
PPA
安装了它 或
sudo apt-get install swi-prolog-nox -y.
PPA 安装更新的版本。

计划从开始到安装和更新所有内容大约花费一个小时,因为您实际上是从头开始下载和安装 Ubuntu 和所有应用程序。

WSL 安装指南是here

您可能不在 Windows Insider 计划中,因此请不要关注For Windows Insiders: Install Linux distribution of choice,而是关注For Anniversary Update and Creators Update: Install using lxrun

如果你遇到问题我可以帮助你,或者你可以在 GitHub 上发布问题issues page,或者使用 SO 标签wsl,或者使用 Ask Ubuntu 标签wsl,或者使用 SuperUser 标签@ 987654328@.

我最初将它用于这个problem

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

面包屑

  1. 根据installation guide使用 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.

【讨论】:

    猜你喜欢
    • 1970-01-01
    • 1970-01-01
    • 2013-02-28
    • 1970-01-01
    • 1970-01-01
    • 2013-06-11
    • 2018-05-02
    • 1970-01-01
    • 1970-01-01
    相关资源
    最近更新 更多