CTF/Toolkit/z3py - 電気通信大学MMA

インストール Z3のGithubページからgit cloneしてビルド・インストールする． z3pyは /usr/lib/python2.7/dist-packages 以下に同時にインストールされる． 基本的な流れ 1 # モジュールをimport 2 from z3 import * 3 4 # 変数を作成．引数は人間が見てわかりやすい変数名． 5 p, q = Bools(["p", "q"]) 6 x = Int("x") 7 8 # ソルバのインスタンスを生成して 9 s = Solver() 10 11 # 制約を追加 12 s.add(q == True, p != q) 13 s.add(x * x - x == 2) 14 15 # 解を探索，モデルを取得 16 r = s.check() 17 if r == sat: 18 m = s.model() 19 else:

[zyxwv]

z3 の基本的な使い方

[yag_ays]

“Z3はMicrosoft Researchが開発したSAT・SMTソルバである． ブール代数の充足問題に限らず，整数や実数上の不等式を含む充足問題にも適用できる．”