如何在z3中添加Index Of Result的偏移量

Question

如何为从IndexOf表达式获得的值添加偏移量？也就是说，我该怎么做？

> import z3
> s = 'hello'
> t = 'e'
> z3.simplify(z3.IndexOf(s, t, 0) + z3.IntVal(1))
z3.z3types.Z3Exception: Non-sequence passed as a sequence

我希望得到的位置比e。

另一方面，切换订单按预期工作

> z3.simplify(z3.IntVal(1) + z3.IndexOf(s, t, 0))
2

Answer 1

您在z3py中发现了一个错误！

错误就在这条线上：https://github.com/Z3Prover/z3/blob/master/src/api/python/z3/z3.py#L10150

其中包括：

    return SeqRef(Z3_mk_seq_index(s.ctx_ref(), s.as_ast(), substr.as_ast(), offset.as_ast()), s.ctx)

相反，它应该说：

    return ArithRef(Z3_mk_seq_index(s.ctx_ref(), s.as_ast(), substr.as_ast(), offset.as_ast()), s.ctx)

我已经在他们的bug追踪器上报告了这个问题：https://github.com/Z3Prover/z3/issues/2159

在z3.py的本地副本中进行更改后，您的程序应该按原样运行。或者你可以等到他们发布修复程序。