QEPCADは量化子除去(QE, Quantifier Elimination)のためのアカデミックツールで、作者のサイト
QEPCAD - Quantifier Elimination by Cylindrical Algebraic Decomposition
で公開されています。インストールのために自前ビルドが必要な上に、サイトの案内
Downloading and Installing QEPCADにそのまま従ってもいまのUbuntuだとインストールに失敗するので覚書をしておきます。
# インストール
1. 必要なライブラリsaclibとQEPCAD本体を(適当なディレクトリで)ダウンロードする
$ wget https://www.usna.edu/CS/qepcadweb/INSTALL/qepcad-B.1.69.tar.gz
$ wget https://www.usna.edu/CS/qepcadweb/INSTALL/saclib2.2.6.tar.gz
2. saclibのビルドに必要になるので先にcshを入れておく
$ sudo apt install csh
3. 普通はccはCコンパイラを指している気がするが、一応ccと叩いて確認しておく。もしも指していないならgccを指すようにしておく。
4. saclibを展開して中に入る。
$ tar xf saclib2.2.6.tar.gz
$ cd saclib2.2.6
5. 変数saclibがそのディレクトリを指すようにする。makeが使うのでexportしておく必要がある。いまはsaclibディレクトリのなかにいるのでpwdでやってしまう。
export saclib=`pwd`
6. 以下を順次叩いてビルドする。何かhoge.hが足りないと言われたら適当にぐぐってそれを含むubuntuパッケージを見つけ(普通はhoge-devみたいな名前になっている)、aptでインストールする。
$ cd $saclib/bin
$ ./sconf
$ ./mkproto
$ ./mkmake
$ ./mklib all
7. エラーが出なければsaclibのインストールはおわり。
8. qepcadのビルドに使うので先にlibreadline-devを入れておく
$ sudo apt install libreadline-dev
9. qepcadを展開し、中に入る。ディレクトリはqesourceという名前になっている。
$ tar xf qepcad-B.1.69.tar.gz
$ cd qesource
10. 変数qeを設定する。これもmakeが使うのでexportしておく必要がある。いまはqesourceのなかにいるのでpwdでやってしまう。
$ export qe=`pwd`
11. サイトだとgmakeを叩くとなっているが普通にmakeを叩く。
$ make
11. 結構時間がかかる。何もエラーがでなければおわり。
こんな感じのエラーが出たら、やっぱり足りないものが入っているパッケージをGoogle探してaptで入れる。
12. plot2dをビルドする。先にfreeglutを入れておく。
$ sudo apt install freeglut3-dev
13. makeする
$ cd $qe/plot2d
$ make
14. これでqesource/binにqepcadがビルドされているはず。必要に応じてパスを通す。
# 使い方
例と注意点だけ示す。今回は
の量化子を消してみる。
1. 起動する。ここでびっくりしたのだが、先の変数qeと変数saclibが有効になっていないとセグフォで落ちるので頻繁に使うのならちゃんと起動時に変数が設定されるようにしておく。
2. このプログラムは対話で進んでいく。まずタイトルを要求されるので、ブラケットで囲んで指定しEnter。今回はhogeにする。
Enter an informal description between '[' and ']':
[hoge]
3. 式に出てくる変数を、拘束される変数も自由変数もまとめて丸括弧囲み、カンマ区切りで書く。このとき、自由変数を先に、束縛変数(量化子のなかの変数)を後に書かなければならない。今回消したいのはxなので、xをあとに書く。また、拘束される変数は、式を冠頭標準形にしたときの順番で書かなければならない(今回は1個なので関係ないが)。
Enter a variable list:
(b,c,x)
4. 自由変数の個数を指定する。いまはbとcが自由なので2にする。
Enter the number of free variables:
2
5. 式を入力する。まず量化子と拘束する文字の組を並べて丸括弧で囲んで並べる。今回は存在量化子なので「(Ex)」となる。全称量化子のときは「(Ax)]とする。また、今回は量化子が1つだが、複数のときには3で入れた順番で量化子があらわれなければならない。例えば、「(a,b,x,y)」と変数を指定していて、自由変数の個数を2と指定しながら「(Ay)(Ex)」というのは駄目。次にブラケット(丸括弧でない)で囲んで式を書く。かけ算は空白を入れればよい。アンドは「/\」で、オアは「\/」で書く。その辺の記号は公式ページ
https://www.usna.edu/CS/qepcadweb/B/user/EnterForm.htmlにも書いてある。最後にピリオドを打ってEnter。打たないといつまで立っても始まらない(計算が重いんだなと勘違いしがち)。
(Ex)[x^2+b x+c=0 /\ x>=0].
6. よくわかんないけどずっとgoって答えると答えが出る。
=======================================================
Before Normalization >
go
Before Projection (x) >
go
Before Choice >
go
Before Solution >
go
An equivalent quantifier-free formula:
4 c - b^2 <= 0 /\ [ b < 0 \/ c <= 0 ]
===================== The End =======================
7. もしもtrueとかしか出なくて不満足なら、ここ
QEPCAD - Entering Formulas
を見ながらBefore solutionでsolution-extension Tなどを試すとよい。
(イ)
(ロ)
(ハ)
(ニ)
(イの両辺にロの行列をかける)
(ロを「代入」)
