Как получить пример значения из модели z3 для массивов? - PullRequest
Новая
       8

Как получить пример значения из модели z3 для массивов?

0 голосов
/ 13 ноября 2018

Благодаря этот вопрос Я знаю, как проще увидеть модель. На данный момент, как я могу получить ожидаемые значения для a и another?

Если возможно, я бы хотел, чтобы пример кода использовал pyz3.

Пояснение:

Имеет следующий файл smt: 

(set-option :produce-models true)
(set-logic QF_AUFBV )
(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8) ) )
(declare-fun another () (Array (_ BitVec 32) (_ BitVec 8) ) )
(assert (and  (=  true (=  (_ bv77 32) (concat  (select  a (_ bv3 32) 
) (concat  (select  a (_ bv2 32) ) (concat  (select  a (_ bv1 32) ) 
(select  a (_ bv0 32) ) ) ) ) ) ) (=  true (=  (_ bv12 32) (concat  
(select  another (_ bv3 32) ) (concat  (select  another (_ bv2 32) ) 
(concat  (select  another (_ bv1 32) ) (select  another (_ bv0 32) ) ) 
) ) ) ) ) )

Я хотел бы иметь значение для a и another, которые 77 и 12

Какой самый лучший способ?

На данный момент мой подход: 

import z3
import binascii

z3.set_param('model_compress', False)
s = z3.Solver()
s.from_file("first.smt")

s.check()

m = s.model()

print(m)


a = m[m.decls()[0]]

print(a)

b = bytearray(a.num_entries())

for x in range(a.num_entries()):
    index = a.entry(x).as_list()[0]
    value = a.entry(x).as_list()[1]

    print(index, value)
    b[a.num_entries()-index.as_long()-1] = value.as_long()

expected = int(binascii.hexlify(b),16)

print(expected)

Вывод 77, как и ожидалось:)

Спасибо

Ответы [ 2 ]

0 голосов
/ 14 ноября 2018

Вид использования, который вы здесь используете, чрезвычайно хрупок.Строка: 

a = m[m.decls()[0]]

предполагает, что модель будет иметь значение a в самом первом слоте.Это может работать для этого конкретного файла SMT;но нет гарантии, что он будет всегда.

Ваш код может быть упрощен.Но я думаю, что упускает момент, что это не правильный способ использования z3.Я бы порекомендовал либо придерживаться только SMTLib, либо напрямую писать в z3py.Смешивание этих двух интерфейсов просто добавит путаницы без очевидной выгоды, и, как я уже говорил, будет чрезвычайно хрупким.

Поскольку у вас уже есть что-то, генерирующее SMTLib;почему бы просто не придерживаться этого формата?Вы можете использовать команду SMTLib eval для извлечения произвольных значений из вашей модели.Или перекодируйте все в z3py и используйте эти возможности напрямую.Кроме того, неясно, почему вы моделируете a и another как массивы для начала: Похоже, вы заинтересованы только в [0] '-ом элементе этих массивов?Если это так, просто используйте 32-битный вектор вместо массива.

0 голосов
/ 13 ноября 2018

Как показано в исходном вопросе, значения модели для массивов являются функциями, которые отображают индексы в значения.Так, примерным значением для a является [3 -> 1, else -> 1], то есть функция, которая отображает индекс 3 на значение 1 и все другие индексы на значение 1.

...