1

Z3 の初心者として、定義済みの Python 関数で Z3Py を動作させる方法があるかどうか疑問に思っています。以下は、私の質問を説明する小さな例です。

from z3 import *

def f(x):
    if x > 0:
        print " > 0"
        return 1
    else:
        print " <= 0"
        return 0

a=Int('a')
s=Solver()
s.insert(f(a) == 0)

t = s.check()
print t
print a
m = s.model()
print m

f(x) は Python で定義されている関数です。x <= 0 の場合、f(x) は 0 を返します。制約を追加し、 s.insert(f(a) == 0)Z3 が変数 "a" の適切な値 (たとえば -3) を見つけられることを期待します。しかし、これらのコードは正しく機能していません。どのように変更すればよいですか？

(Z3 の外部で定義された f(x) が必要であり、Z3 によって呼び出されることに注意してください。)

私がやろうとしているのは、Z3 に変換せずに、グラフ ライブラリによって提供される事前定義された関数を呼び出すことです。私はNetworkXライブラリを使用しています.いくつかのコードは次のように与えられています:

import networkx as nx

G1=nx.Graph()
G1.add_edge(0,1)

G2=nx.Graph()
G2.add_edge(0,1)
G2.add_edge(1,2)

print(nx.is_isomorphic(G1, G2))
#False

この頂点を削除した後、G2 が G1 と同型になるように、G2 の頂点を見つけるのに Z3 が必要です。例えば

G2.remove_node(0)
print(nx.is_isomorphic(G1, G2))
#True
4

1 に答える 1

1

一般的な関数の場合 (たとえば、再帰関数の場合) は難しいと思いますがf、何らかの構造があると仮定すると (たとえば、if then else)、単純なトランスレータを作成できる可能性があります。問題は、Z3 の関数は本質的に数学的なものであり、Python 関数と直接同等ではないことです ( http://en.wikipedia.org/wiki/Uninterpreted_functionを参照)。あなたの目的のために可能であれば、私は反対の方向に進むことを提案しますf.Z3コンストラクトに関して関数を定義し、プログラム内で評価します(たとえば、この方法を使用: Z3/Python gets python values from model )。それがうまくいかない場合は、関数をどのように使用する必要があるかについての追加の詳細を含めてください。最小限の例を次に示します (rise4fun リンク:http://rise4fun.com/Z3Py/pslw ):

def f(x):
    return If(x > 0, 1, 0)

a=Int('a')
s=Solver()
P = (f(a) == 0)
s.add(P)

t = s.check()
print t
print a
m = s.model()
print m

res = simplify(f(m[a])) # evaluate f at the assignment to a found by Z3

print "is_int_value(res):", is_int_value(res)

print res.as_long() == 0 # Python 0

print f(1)
print simplify(f(1)) # Z3 value of 1, need to convert as above
于 2014-03-21T16:28:21.307 に答える