如何向从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
我想在 than of 之后获取位置e
。
另一方面,切换顺序按预期工作
> z3.simplify(z3.IntVal(1) + z3.IndexOf(s, t, 0))
2
您在 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)
我已经在他们的错误跟踪器上报告了这一点:https : //github.com/Z3Prover/z3/issues/2159
一旦在 z3.py 的本地副本中进行了更改,您的程序应该可以正常工作。或者你可以等到他们发布修复程序。
本文收集自互联网,转载请注明来源。
如有侵权,请联系[email protected] 删除。
我来说两句