（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）声明函数

回答

相关问题