6

与えられたいくつかの結果/ xペアに対して、単純な「result = x * t + c」式でcおよびt係数を見つけたいと思います。

from z3 import *

x=Int('x')
c=Int('c')
t=Int('t')

s=Solver()

f = Function('f', IntSort(), IntSort())

# x*t+c = result
# x, result = [(1,55), (12,34), (13,300)]

s.add (f(x)==(x*t+c))
s.add (f(1)==55, f(12)==34, f(13)==300)

t=s.check()
if t==sat:
    print s.model()
else:
   print t

...しかし、結果は明らかに間違っています。おそらく、関数の引数をマップする方法を見つける必要があります。

関数を正しく定義するにはどうすればよいですか?

4

1 に答える 1

5

アサーションf(x) == x*t + cは、すべての関数を定義していません。与えられた の値がであると言っているだけです。Z3 は全称量指定子をサポートしています。ただし、それらは非常に高価であり、一連の制約に全称量指定子が含まれている場合、問題が決定不能になるため、Z3 は完全ではありません。つまり、Z3 はこのような問題で戻ってくる可能性があります。fxf xx*t + cunknown

これfは基本的にスクリプトの「マクロ」であることに注意してください。この「マクロ」をエンコードするために Z3 関数を使用する代わりに、このトリックを実行する Python 関数を作成できます。つまり、Z3 式を指定すると、新しい Z3 式を返す Python 関数です。これが新しいスクリプトです。このスクリプトはオンラインでも入手できます: http://rise4fun.com/Z3Py/Yoi 別のバージョンのスクリプトでは、cとtがRealの代わりになっていIntます: http://rise4fun.com/Z3Py/uZl

from z3 import *

c=Int('c')
t=Int('t')

def f(x):
    return x*t + c

# data is a list of pairs (x, r)
def find(data):
    s=Solver()
    s.add([ f(x) == r for (x, r) in data ])
    t = s.check()
    if s.check() == sat:
        print s.model()
    else:
        print t

find([(1, 55)])
find([(1, 55), (12, 34)])
find([(1, 55), (12, 34), (13, 300)])

注意: SMT 2.0 フロントエンドでは、コマンドを使用してマクロを定義できますdefine-fun。

于 2012-08-09T14:26:57.783 に答える