（Z3Py）聲明函數

我想找到在簡單的「結果= X * T + C」配方C和T係數一些給定的結果/ X對：（Z3Py）聲明函數

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

...但結果顯然是錯誤的。我可能需要找出如何映射函數參數。

如何正確定義功能？

來源

2012-08-09 Dennis Yurichev

[Z3 API中define-fun的等價物]的可能重複（http://stackoverflow.com/questions/7740556/equivalent-of-define-fun-in-z3-api） – usr 2014-05-07 10:14:36

斷言f(x) == x*t + c是不定義函數f所有x。這只是說，f對於給定的x的值是x*t + c。 Z3支持通用量詞。然而，它們非常昂貴，而且當一組約束包含通用量詞時Z3並不完整，因爲問題變得不可判定。也就是說，Z3可能會爲此類問題返回unknown。

請注意，f本質上是您的腳本中的「宏」。我們可以創建一個可以實現這個技巧的Python函數，而不是使用Z3函數來編碼這個「宏」。也就是說，給定Z3表達式的Python函數返回一個新的Z3表達式。這是一個新的腳本。該腳本也可在網上：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-09 14:26:57

（Z3Py）聲明函數

回答

相關問題