（Z3Py）声明功能((Z3Py) declaring function)

我想找到在简单的“结果= X * T + C”配方C和T系数一些给定的结果/ X对：

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

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

我应该如何正确定义的功能？

断言f(x) == x*t + c 不限定函数f所有x 。它只是说，价值f对于给定的 x为x*t + c 。 Z3支持全称量词。然而，他们是非常昂贵的，当一组约束含有全称量词因为这个问题变得不可判定Z3是不完整的。也就是说，Z3可以返回unknown的这样那样的问题。

需要注意的是f基本上是在你的脚本中的“宏”。而是采用了Z3的功能编码这个“宏”，我们可以创建一个Python函数，它的伎俩。也就是说，给出一个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)])