Подсчитайте их в BitVec в Z3 с форматом ввода SMT 2 - PullRequest
Новая
       38

Подсчитайте их в BitVec в Z3 с форматом ввода SMT 2

0 голосов
/ 02 июля 2018

Существует ли компактный способ подсчета количества битов, которые установлены в 1 в BitVec в Z3, с использованием формата ввода SMT 2?

Принятый ответ на этот вопрос: Сумма всех битов в битовом векторе Z3 показывает способ сделать это с помощью Python.

1 Ответ

0 голосов
/ 02 июля 2018

На самом деле пока нет простого способа сделать это непосредственно в SMTLib. Лучшее, что вы можете сделать на самом деле, это свернуть свои собственные для каждого размера битового вектора; довольно некрасивый, но легко генерируемый код: 

(set-logic QF_BV)
(set-option :produce-models true)

(define-fun popCount8 ((x (_ BitVec 8))) (_ BitVec 8)
                      (bvadd (ite (= #b1 ((_ extract 0 0) x)) #x01 #x00)
                             (ite (= #b1 ((_ extract 1 1) x)) #x01 #x00)
                             (ite (= #b1 ((_ extract 2 2) x)) #x01 #x00)
                             (ite (= #b1 ((_ extract 3 3) x)) #x01 #x00)
                             (ite (= #b1 ((_ extract 4 4) x)) #x01 #x00)
                             (ite (= #b1 ((_ extract 5 5) x)) #x01 #x00)
                             (ite (= #b1 ((_ extract 6 6) x)) #x01 #x00)
                             (ite (= #b1 ((_ extract 7 7) x)) #x01 #x00)))


; test
(define-fun x () (_ BitVec 8) #xAB)
(declare-fun result () (_ BitVec 8))
(assert (= result (popCount8 x)))
(check-sat)
; Should be 5!
(get-value (result))

Это печатает: 

sat
((result #x05))

Использование рекурсии

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

(set-logic BV)
(set-option :produce-models true)

(define-fun-rec popCount8_rec ((x (_ BitVec 8)) (i (_ BitVec 8)) (accum (_ BitVec 8))) (_ BitVec 8)
    (ite (= i #x08)
         accum
         (popCount8_rec (bvshl x #x01)
                        (bvadd i #x01)
                        (bvadd accum (ite (= #b1 ((_ extract 7 7) x)) #x01 #x00)))))

(define-fun popCount8 ((x (_ BitVec 8))) (_ BitVec 8) (popCount8_rec x #x00 #x00))

; test
(define-fun x () (_ BitVec 8) #xAB)
(declare-fun result () (_ BitVec 8))
(assert (= result (popCount8 x)))
(check-sat)
; Should be 5!
(get-value (result))

Это также печатает: 

sat
((result #x05))

Параметрический полиморфизм

Обратите внимание, что какой бы метод вы ни выбрали, вы должны написать отдельную функцию для каждого размера N в popCountN. SMTLib не позволяет пользователям определять функции, которые работают с «параметрическими» типами. Это является фундаментальным ограничением логики, а также одной из основных причин (хотя определенно не единственной!) Того, почему многие люди предпочитают создавать сценарии SMT-решателей из языков более высокого уровня, чтобы избежать такого стандартного кода.

Трюк с питоном

Лучше всего развернуть собственную версию, как описано выше. Обычный прием в Z3 заключается в том, что вы можете использовать программу Python, которую вы связали, и print s.sexpr() в какой-то момент и посмотреть, что сгенерировал генератор. Затем вы можете вырезать и вставить его в SMTLib, если хотите; хотя, конечно, остерегайтесь обычных ошибок вырезания и вставки.

...