Как добавить смещение для результата IndexOf в z3 - PullRequest
Новая
       16

Как добавить смещение для результата IndexOf в z3

0 голосов
/ 28 февраля 2019

Как добавить смещение к значению, полученному из выражения 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

1 Ответ

0 голосов
/ 28 февраля 2019

Вы нашли ошибку в 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, ваша программа должна работать как есть.Или вы можете подождать, пока они выпустят исправление.

...