(Z3Py) 声明函数 [英] (Z3Py) declaring function

问题描述

对于某些给定的结果/x 对，我想在简单的result=x*t+c"公式中找到 c 和 t 系数:

I would like to find c and t coefficients in simple "result=x*t+c" formula for some given result/x pairs:

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

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

... but the result is obviously wrong. I probably need to find out how to map function arguments.

我应该如何正确定义函数?

How should I define function correctly?

推荐答案

断言f(x) == x*t + c 不是定义函数f 用于所有 x.这只是说给定 x 的f 的值是x*t + c.Z3 支持全称量词.然而，它们非常昂贵，并且当一组约束包含全称量词时 Z3 是不完整的，因为问题变得不可判定.也就是说，对于这种问题，Z3 可能会返回unknown.

The assertion f(x) == x*t + c is not defining the function f for all x. It is just saying that the value of f for the given x is x*t + c. Z3 supports universal quantifiers. However, they are very expensive, and Z3 is not complete when a set of constraints contains universal quantifiers since the problem becomes undecidable. That is, Z3 may return unknown for this kind of problem.

请注意，f 在您的脚本中本质上是一个宏".我们可以创建一个 Python 函数，而不是使用 Z3 函数来编码这个宏".也就是说，一个 Python 函数，给定一个 Z3 表达式，返回一个新的 Z3 表达式.这是一个新脚本.该脚本也可在线获取:http://rise4fun.com/Z3Py/Yoi这是脚本的另一个版本，其中 c 和 t 是 Real 而不是 Int:http://rise4fun.com/Z3Py/uZl

Note that f is essentially a "macro" in your script. Instead of using a Z3 function for encoding this "macro", we can create a Python function that does the trick. That is, a Python function that, given a Z3 expression, returns a new Z3 expression. Here is a new script. The script is also available online at: http://rise4fun.com/Z3Py/Yoi Here is another version of the script where c and t are Real instead of 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 定义宏.

Remark: In the SMT 2.0 front-end, macros can be defined using the command define-fun.

这篇关于(Z3Py) 声明函数的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！