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没有为 all定义函数。这只是说给定的值是。Z3 支持通用量词。但是，它们非常昂贵，并且当一组约束包含通用量词时，Z3 是不完整的，因为问题变得不可判定。也就是说，Z3可能会因为这种问题而回归。fxf xx*t + cunknown

请注意，这f本质上是脚本中的“宏”。我们可以创建一个 Python 函数来解决这个问题，而不是使用 Z3 函数来编码这个“宏”。也就是说，一个 Python 函数，给定一个 Z3 表达式，返回一个新的 Z3 表达式。这是一个新脚本。该脚本也可在线获取：http ://rise4fun.com/Z3Py/Yoi 这是该脚本的另一个版本，其中cand tareReal代替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 回答