Hello SMT-Solver by z3

導入

z3とは、Microsoft Researchが開発を進めているSMTソルバです。
SMTソルバは、条件式(ex. if(a > 1 && b > 2) ) を受け取り、条件式がTRUEになる入力が存在するか否か、もし存在するならばその入力の一例(ex. a=2, b=3)を提示します。

z3はCUI, C, C++, Java, Ocaml, .NET, Pythonから呼び出して使用できます(z3自体はC++で記述されています)。

今回、macのIntelliJ IDEAにてJavaを用いてz3を使ってみたので、その際の流れを個人的なメモの意味も込めて書き残します。基本的には、READ.mdを参照して行いました。

環境

• macOS Sierra 10.12.6
• IntelliJ IDEA 2017.2

流れ

1. z3 をダウンロード。ダウンロードしたフォルダ中のbin中に入っている上記の3つを使用します。

2. IntelliJのライブラリにcom.microsoft.z3.jarファイルを登録する。右上のProject Structure->Librariesから登録できるかと思います。

3. libz3.dylibとlibz3java.dylibを/usr/local/libに配置します。ちなみに、私はここでつまづきました。Javaにライブラリが見つからないと怒られたので、調べながらRun->Edit configuresのVM Optionsに、

-Djava.library.path=libz3.dylibとlibz3java.dylibを置いたパス

の追加を行いましたがダメでした。結局、その他の*.dylibが入っていた上記のフォルダに二つを放り込んだところ動きました(何も起きないといいな…)。
4. 以下のコードを実行しました。参照

import com.microsoft.z3.*;

import java.util.HashMap;

public class HelloZ3 {
    public static void main(String[] args) {

        //application example of z3
        //reference https://qiita.com/quentin-maisonneuve/items/4f32cf52293dc44ffc3d

        Context context = new Context(new HashMap<>());
        BoolExpr a = context.mkBoolConst("a");
        BoolExpr b = context.mkBoolConst("b");
        BoolExpr c = context.mkBoolConst("c");

        BoolExpr formula = context.mkAnd(context.mkOr(a, b), c); // (a || b) && c


        Solver solver = context.mkSolver();
        solver.add(formula);

        if(solver.check() == Status.SATISFIABLE) {
            Model model = solver.getModel();
            Expr resultVa = model.eval(a, false);
            Expr resultVb = model.eval(b, false);
            Expr resultVc = model.eval(c, false);

            System.out.println(resultVa);   // Result is true
            System.out.println(resultVb);   // Result is false
            System.out.println(resultVc);   // Result is true

        }

    }

}

ソースからのビルド(ソース版をダウンロードすること)(うろ覚え)

1. ダウンロードしたフォルダのルート(configureファイルがある場所)で、

./configure

を実行。私はjavaから使用したかったので、--javaオプションをつけました。

./configure --java
2. buildディレクトリに移動、

make
と打ち込む。そこそこ待った後に、先ほど示した3つのファイルがビルドされます。

終わりに

私用で不等式などの条件式(ex. a > 4)を解く必要があるので、出来次第追記します。