function - z3py:如何在推断函数时对 "else"值进行约束

Question

我正在使用 z3py 推断一个函数，如下所示

f = Function('f',IntSort(),IntSort(),IntSort())

在断言一组约束之后:

s.add(f(a1,b1)==c1)
s.add(f(a2,b2)==c2)
s.add(f(a3,b3)==c3)...

函数推断为

[(a1,b1) -> c1,
(a2,b2) -> c2,
(a3,b3) -> c3,
...,
else -> 2]

如何将“else”值限制为固定数字？这样推断的 f 的输出将是

[(a1,b1) -> c1,
(a2,b2) -> c2,
(a3,b3) -> c3,
...,
else -> some number that I assert]

编辑:

from z3 import *

s = Solver()
k = Int('k')
f = Function('f',IntSort(),IntSort())

s.add(And(f(1)==1,f(2)==2))

list1 = []
list1.append(k!=1)
list1.append(k!=2)
s.add(ForAll(k,Implies(And(list1),f(k)==5)))

print s.check()
print s.model()

输出是

sat
[f = [1 -> 1, 2 -> 2, else -> 5]]

这对于这个简单的案例来说似乎工作得很好。

但是，当约束中函数“f”的输入未定时。输出可能很奇怪。例如

from z3 import *

s = Solver()

f = Function('f',IntSort(),IntSort(),IntSort())

i = Int('i')
j = Int('j')
k = Int('k')
l = Int('l')


s.add(i>=0,i<5)
s.add(j>=0,j<5)

s.add(And(f(j,1)==i,f(i,2)==j))

list1 = []
list1.append(And(k==1,l==j))
list1.append(And(k==2,l==i))
s.add(ForAll([k,l],Implies(Not(Or(list1)),f(l,k)==5)))

print s.check()
print s.model()

输出是

[i = 0,
 k!6 = 0,
 j = 3,
 k!12 = 6,
 f = [else -> f!15(k!13(Var(0)), k!14(Var(1)))],
 f!15 = [(3, 1) -> 0, (0, 2) -> 3, else -> 5],
 k!13 = [0 -> 0, 3 -> 3, else -> 6],
 k!14 = [2 -> 2, 1 -> 1, else -> 0]]

然后很难解释推断的 f。

Answer 1

这是一个很好的问题和非常有根据的分析。是的，您可以使用量词控制默认值。 Z3别无选择，只能同意。然而，模型的编码是基于量词实例化引擎的方式(参见 Yeting Ge 和 Leonardo de Moura 的完整量词实例化)。Z3 不会对模型中的表达式进行 beta 归约，如果需要，它会留给应用程序来执行 beta 归约。您可以让 Z3 beta 减少其他分支，方法是将您的参数插入函数的参数(使用 API 公开的替换例程)，然后调用模型评估器来减少关于模型的结果表达式。