Mingw64にYices2をインストールする

Yices2は昔からあるSMTソルバーです．
現在ではSMTソルバーと言えばCVC4やZ3がメジャーですが，それらが登場する以前はこのYicesが一世を風靡していたらしい？
gprefとGMPに依存しています．途中，Mingwでは解決できないシンボルがソースコード中に登場するためそれを修正する必要があります．

gprefのインストール

Terminal.sh

$ cd gperf-3.0.4
$ ./configure
$ make
$ make install

GMPのインストール

Terminal.sh

$ cd gmp-6.1.1
$ ./configure

summary-of-build-options.sh

configure: summary of build options:

  Version:           GNU MP 6.1.1
  Host type:         ivybridge-pc-mingw64
  ABI:               64
  Install prefix:    /usr/local
  Compiler:          gcc
  Static libraries:  yes
  Shared libraries:  no

Terminal.sh

$ make -j 4
$ make install

make checkをしていないのでCAUTIONは出るが無視する．

CAUTION.sh

+-------------------------------------------------------------+
| CAUTION:                                                    |
|                                                             |
| If you have not already run "make check", then we strongly  |
| recommend you do so.                                        |
|                                                             |
| GMP has been carefully tested by its authors, but compilers |
| are all too often released with serious bugs.  GMP tends to |
| explore interesting corners in compilers and has hit bugs   |
| on quite a few occasions.                                   |
|                                                             |
+-------------------------------------------------------------+

Yices-2.5.1のインストール

Terminal.sh

$ cd yices-2.5.1

/src/frontend/yices/yices_reval.cの44行目を編集する．

yices_reval.c

- #define STDIN_FILENO (_fileno(stdin))
+ #define STDIN_FILENO (fileno(stdin))

46行目も編集する．

yices_reval.c

- #define isatty _isatty
+ #define isatty isatty

./configureのオプションは以下．

• LDGLAGSに-L/usr/local/lib
• --with-static-gmpに/usr/local/lib/libgmp.a
• --with-static-gmp-include-dirに/usr/local/include

Terminal.sh

$ ./configure LDFLAGS=-L/usr/local/lib --with-static-gmp=/usr/local/lib/libgmp.a --with-static-gmp-include-dir=/usr/local/include
$ make
$ make install