Как получить значение из лямбда-выражения? - PullRequest
Новая
       18

Как получить значение из лямбда-выражения?

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

Я экспериментирую с z3 в python. У меня есть следующая модель: 

(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  (=  false (=  (_ bv77 32) (concat  (select  a (_ bv3 32) ) (concat  (select  a (_ bv2 32) ) (concat  (select  a (_ bv1 32) ) (select  a (_ bv0 32) ) ) ) ) ) ) (=  false (=  (_ bv12 32) (concat  (select  another (_ bv3 32) ) (concat  (select  another (_ bv2 32) ) (concat  (select  another (_ bv1 32) ) (select  another (_ bv0 32) ) ) ) ) ) ) ) )

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

import z3
s = z3.Solver()
s.from_file("first.smt")
"""
s
[And(False ==
     (77 == Concat(a[3], Concat(a[2], Concat(a[1], a[0])))),
     False ==
     (12 ==
      Concat(another[3],
             Concat(another[2],
                    Concat(another[1], another[0])))))]
"""
s.check()
"""
sat
"""
m = s.model()
m
[a = Lambda(k!0, 1), another = Lambda(k!0, 1)]

Спасибо

1 Ответ

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

Z3 по умолчанию создает Lambda абстракций для массивов; которые полезны, но трудно понять, что происходит в модели. Я бы порекомендовал отключить это, добавив следующую строку в вашу программу на Python: 

z3.set_param('model_compress', False)

Вы должны сделать это сразу после того, как import z3.

При этом, если вы напечатаете модель в своей программе, вы получите: 

>>> m
[a = [3 -> 1, else -> 1],
 another = [1 -> 1, else -> 1],
 k!0 = [3 -> 1, else -> 1],
 k!1 = [1 -> 1, else -> 1]]

, который должен быть более читабельным. (По сути, это говорит о том, что и a, и another - это массивы, которые отображают все в 1; хотя и немного запутанные.)

...