Использование массива в Z3PY

Question

Я использую z3 для своего исследования, и у меня есть следующая проблема. Я анализирую модель выполнимой формулы, которая содержит массивы, но я не понимаю результатов модели. Например, у меня есть две переменные 'pkgcounter' и 'rxlen' и два предложения p1 и p2. Моя цель - выяснить, существует ли модель, которая удовлетворяет обоим положениям.

 pkgcounter = Array('pkgcounter',IntSort(),BitVecSort(8))

 rxlen = Array('rxlen',IntSort(),BitVecSort(8))

 s = Solver()

 p1 = (pkgcounter < rxlen)

 p2 = (pkgcounter == rxlen)


 s.add(p1,p2)

 if s.check() == sat:

    print s.model()

В результате получается следующая модель: [rxlen = [else -> 0], pkgcounter = [else -> 0], k!0 = [else -> 0]]

Может ли кто-нибудь помочь мне интерпретировать этот результат? Потому что если rxlen и pkgcounter имеют все поля, равные нулю, предложение p1 не имеет модели.

Answer 1

В зависимости от версий Z3 и Python, которые вы используете, эта проблема будет давать разные результаты, все они вызваны

p1 = (pkgcounter < rxlen)

В Python 2.7 (pkgcounter < rxlen) упрощает до False, так как ArrayRef объекты не имеют < оператор и объекты разные. И наоборот, Python 3.5 жалуется на то, что эти объекты не упорядочены (TypeError: unorderable types: ArrayRef() < ArrayRef()).

Обратите внимание, что массивы в Z3 не имеют размера; если они индексируются целыми числами, они действительно имеют бесконечный размер. Так, (pkgcounter < rxlen) не имеет смысла в этом контексте, так как эти массивы нельзя сравнивать таким образом. (См. Также Теория SMT ArraysEx).

Причина того, что этот тестовый сценарий был удовлетворительным, вероятно, в том, что использовалась старая версия Z3. В последней версии (главная ветка на GitHub) это неудовлетворительно, но опять же, это потому, что p1 является False,

В общем, модели для переменных Array сообщаются, например, как определения функций rxlen = [else -> 0] означает, что функция для поиска элемента в массиве rxlen это функция, которая всегда возвращает 0, Добавляя

p3 = (rxlen[0] == 1)

Мы можем заставить rxlen иметь другое значение в первой позиции, и модель будет сообщена как rxlen = [0 -> 1, else -> 1]; т.е. 1 на позиции 0 а также 1 где-либо еще.