2

Z3 を使用して、式が満足できるかどうかを判断しようとしています。コンテキストを定義してから int_const 変数と数式を定義することで、これを簡単に行うことができます。プログラムで式を評価するには、すべてをコードで記述する必要があります。論理式が文字列の形で与えられたとしましょう。例えば、

「x == y && !x == z」

C API では次のように表現されます。

context c;
expr x = c.int_const("x")
//Same for other variables
...
formula = (x == y) && (!x == z);
solver s(c);
s.add(formula);
//s.check() ...etc etc

さて、この特定の数式のコードを書くことはできますが、文字列を指定してプログラムでそれを行うにはどうすればよいでしょうか。私はあなたが考えることができるものなら何でも受け入れます。

ありがとうございました ：）

4

1 に答える 1

4

次のオプションが表示されます。

1) 独自のパーサーを実装し、Z3 API 関数を呼び出すことができます。長所: 「お気に入りの」言語を使用して式を記述できます。短所：「忙しい」仕事です。

2) API を使用できますZ3_parse_smtlib2_string。短所: 数式は SMT 2.0 形式でなければなりません。たとえば、(and (= x y) (not (= x y)))の代わりに書く必要があり(x == y) && !(x == z)ます。

3) Z3 Python API を使用し、evalPython の関数を使用して文字列を解析できます。次に例を示します。

from z3 import *
# Creating x, y 
x = Int('x')
y = Int('y')

# Creating the formula using Python
f = And(x == y, Not(x == y))
print f

# Using eval to parse the string.
s = "And(x == y, Not(x == y))"
f2 = eval(s)
print f2

ところで、このスクリプトは rise4fun http://rise4fun.com/z3pyでは機能しません。これは機能evalが許可されていないためですが、ローカルの Z3 インストールでは上記のスクリプトを使用できます。

于 2012-05-30T05:56:04.067 に答える