Использование массива в 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 = [еще -> 0], pkgcounter = [еще -> 0], к 0 = [еще -> 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 Theory).

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

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

p3 = (rxlen[0] == 1) 

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