Как ограничить сортировку индекса для массива в Z3? - PullRequest
Новая
       13

Как ограничить сортировку индекса для массива в Z3?

0 голосов
/ 06 марта 2019

Я пытаюсь представить массив из 9 символов в виде массива в Z3, чтобы перечислить все комбинации этих символов, которые будут удовлетворять определенным ограничениям (которые были сгенерированы KLEE).

Сгенерированные выражения приведены ниже: 

(set-logic QF_AUFBV)
(declare-fun ascii_buf () (Array (_ BitVec 32) (_ BitVec 8) ) )

(assert
    (let (
        (?B1 ((_ sign_extend 24)  (select  ascii_buf (_ bv8 32) ) ) )
        (?B2 ((_ sign_extend 24)  (select  ascii_buf (_ bv6 32) ) ) )
        (?B3 ((_ sign_extend 24)  (select  ascii_buf (_ bv7 32) ) ) )
        (?B4 ((_ sign_extend 24)  (select  ascii_buf (_ bv1 32) ) ) )
        (?B5 ((_ sign_extend 24)  (select  ascii_buf (_ bv2 32) ) ) )
        (?B6 ((_ sign_extend 24)  (select  ascii_buf (_ bv0 32) ) ) )
        (?B7 ((_ sign_extend 24)  (select  ascii_buf (_ bv5 32) ) ) )
        (?B8 ((_ sign_extend 24)  (select  ascii_buf (_ bv3 32) ) ) )
        (?B9 ((_ sign_extend 24)  (select  ascii_buf (_ bv4 32) ) ) ))

        (let (
            (?B11 (bvadd  (_ bv4294967248 32) ?B5 ) )
            (?B10 (bvadd  (_ bv4294967248 32) ?B4 ) ) )

            (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and

                (=  false (bvslt  ?B6 (_ bv48 32) ) )   # ASCII number constraints ("0" = 48, "9" = 57)
                (=  false (bvslt  (_ bv57 32) ?B6 ) ) )
                (=  false (bvslt  ?B4 (_ bv48 32) ) ) )
                (=  false (bvslt  (_ bv57 32) ?B4 ) ) )
                (=  false (bvslt  ?B5 (_ bv48 32) ) ) )
                (=  false (bvslt  (_ bv57 32) ?B5 ) ) )
                (=  false (bvslt  ?B8 (_ bv48 32) ) ) )
                (=  false (bvslt  (_ bv57 32) ?B8 ) ) )
                (=  false (bvslt  ?B9 (_ bv48 32) ) ) )
                (=  false (bvslt  (_ bv57 32) ?B9 ) ) )
                (=  false (bvslt  ?B7 (_ bv48 32) ) ) )
                (=  false (bvslt  (_ bv57 32) ?B7 ) ) )
                (=  false (bvslt  ?B2 (_ bv48 32) ) ) )
                (=  false (bvslt  (_ bv57 32) ?B2 ) ) )
                (=  false (bvslt  ?B3 (_ bv48 32) ) ) )
                (=  false (bvslt  (_ bv57 32) ?B3 ) ) )
                (=  false (bvslt  ?B1 (_ bv48 32) ) ) )
                (=  false (bvslt  (_ bv57 32) ?B1 ) ) )

                (bvslt  ?B10 (_ bv9 32) ) )             # other constraints (autogenerated)
                (=  false (bvslt  ?B11 ?B10 ) ) )
                (bvslt  (bvadd  (_ bv4294967248 32) ?B8 ) (_ bv9 32) ) )
                (=  false (bvslt  (bvadd  (_ bv4294967200 32) (bvadd  ?B4 ?B8 ) ) (bvadd  (_ bv4294967248 32) ?B6 ) ) ) )
                (=  false (bvslt  (bvadd  (_ bv4294967248 32) ?B9 ) (_ bv9 32) ) ) )
                (bvslt  (bvadd  (_ bv4294967248 32) ?B7 ) (_ bv9 32) ) )
                (=  false (bvslt  (bvadd  (_ bv4294967200 32) (bvadd  ?B4 ?B7 ) ) ?B11 ) ) )
                (=  false (bvslt  ?B11 (_ bv9 32) ) )

            ) # outer and

        ) # end inner let

    ) # end outer let

) # end assert

Когда я пытаюсь перечислить различные решения, используя метод, описанный здесь , я начинаю получать неожиданные модели, подобные этой (первые 2, как и ожидалось, с ограниченными индексами <9): </p> 

[ascii_buf = Lambda(k!0,
                    If(k!0 == 3,
                       56,
                       If(k!0 == 0,
                          51,
                          If(k!0 == 4,
                             57,
                             If(k!0 == 1,
                                56,
                                If(k!0 == 5,
                                   56,
                                   If(k!0 == 2, 57, 50)))))))]
[ascii_buf = Lambda(k!0,
                    If(k!0 == 3,
                       56,
                       If(k!0 == 4,
                          57,
                          If(k!0 == 1,
                             56,
                             If(k!0 == 5,
                                56,
                                If(k!0 == 2, 57, 50))))))]
[ascii_buf = Lambda(k!0,
                    If(k!0 == 3,
                       56,
                       If(k!0 == 1073741824,
                          48,
                          If(k!0 == 4,
                             57,
                             If(k!0 == 1,
                                56,
                                If(k!0 == 5,
                                   56,
                                   If(k!0 == 2, 57, 50)))))))]
[ascii_buf = Lambda(k!0,
                    If(k!0 == 3,
                       56,
                       If(k!0 == 1073741824,
                          48,
                          If(k!0 == 4,
                             57,
                             If(k!0 == 1,
                                56,
                                If(k!0 == 5,
                                   56,
                                   If(k!0 == 32768,
                                      51,
                                      If(k!0 == 2, 57, 50))))))))]

Я не слишком знаком с Z3, но я думаю, что если бы я мог ограничить сортировку индекса массива (вместо 32-битного битового вектора), это могло бы решить проблему. Но любые / все предложения будут оценены!

...