(Z3Py)声明功能

Question

对于某些给定的结果/ 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

......但结果显然是错误的.我可能需要找出如何映射函数参数.

我该如何正确定义功能？

Answer 1

断言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.