z3py:如何在推断函数时对 "else" 值进行约束
z3py: how to make constraints for "else" value when inferring a function
我正在使用 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。
这是一个很好的问题和非常有见地的分析。是的,您可以使用量词控制默认值。 Z3别无选择,只能同意。
然而,模型的编码是基于量词实例化引擎的方式(参见 Yeting Ge 和 Leonardo de Moura 的完整量词实例化)。
Z3 不会对模型中的表达式进行 beta 归约,如果需要,它会留给应用程序来执行 beta 归约。您可以通过将参数插入函数的参数(使用 API 公开的替换例程)来让 Z3 beta 减少其他分支,然后调用模型评估器来减少关于模型的结果表达式.
我正在使用 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。
这是一个很好的问题和非常有见地的分析。是的,您可以使用量词控制默认值。 Z3别无选择,只能同意。 然而,模型的编码是基于量词实例化引擎的方式(参见 Yeting Ge 和 Leonardo de Moura 的完整量词实例化)。 Z3 不会对模型中的表达式进行 beta 归约,如果需要,它会留给应用程序来执行 beta 归约。您可以通过将参数插入函数的参数(使用 API 公开的替换例程)来让 Z3 beta 减少其他分支,然后调用模型评估器来减少关于模型的结果表达式.