z3py：推断函数时如何对“else”值进行约束答案

【问题标题】：z3py: how to make constraints for "else" value when inferring a functionz3py：推断函数时如何对“else”值进行约束
【发布时间】：2015-06-29 20:21:33
【问题描述】：

我正在使用 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 就很难解释了。

【问题讨论】：

标签： function z3 smt z3py inference

【解决方案1】：

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

【讨论】：