在Z3 python中修改變量

Question

我在寫一些模擬某種規則的應用程序。我發現Z3py的固定點是我的幫助。我的應用程序的輪廓可以是如下： （FP =定點（））

1. 聲明一些整數變量，例如：A，B，C =整數（ 'AB C'）和寄存器到定點 - FP（ a，b，c）

2. 按照某些變量的屬性（事實），增加或減少一些其他變量。例如： if（a> 0 and b> 0）then c = c + 1

3. 查詢目標變量是否滿足某些條件，例如：查詢（目標> 0）

我不知道如何使用規則來指定2.有人能告訴我，這是有可能做到這一點？

Answer 1

我把你介紹的例子，創建了一個例子：

• http://rise4fun.com/Z3Py/kD1P

我希望這有助於。

Z3打印UNSAT，因爲查詢不可訪問。 然後它顯示一個不變量，證明 查詢不可訪問。

更詳細

要使用三個參數聲明屬性做：

fp.register_relation(P) 

添加你心目中的規矩：

P = Function('P', IntSort(), IntSort(), IntSort(), BoolSort()) 

要爲定點引擎註冊吧：

fp.rule(P(-1,1,-10)) 
fp.rule(P(a,b,c+1), [a > 0, b > 0, P(a,b,c)]) 
fp.rule(P(a+1,b,c-1), [a <= 0, b < 0, P(a,b,c)]) 

第一條規則說明什麼屬性最初持有。 第二條規則說C能遞增如果a> 0，B> 0

最後問，如果某些屬性是可到達：

print fp.query(P(a,b,c),c > 0)