Можно ли использовать Z3 для анализа подстрок? - PullRequest
Новая
       26

Можно ли использовать Z3 для анализа подстрок?

9 голосов
/ 20 августа 2011

Я пытаюсь использовать Z3 для рассуждений о подстроках и столкнулся с неинтуитивным поведением. Z3 возвращает «sat», когда его просят определить, присутствует ли «xy» в «xy», но возвращает «неизвестно», когда его спрашивают, находится ли «x» в «x» или «x» в «xy».

Я прокомментировал следующий код, чтобы проиллюстрировать это поведение: 

(set-logic AUFLIA)
(declare-sort Char 0)

;characters to build strings are _x_ and _y_
(declare-fun _x_ () Char)
(declare-fun _y_ () Char)
(assert (distinct _x_ _y_))

;string literals
(declare-fun findMeX () (Array Int Char))  
(declare-fun findMeXY () (Array Int Char))  
(declare-fun x () (Array Int Char))
(declare-fun xy () (Array Int Char))
(declare-fun length ( (Array Int Char) ) Int )

;set findMeX = 'x'
(assert (= (select findMeX 0) _x_))
(assert (= (length findMeX) 1))

;set findMeXY = 'xy'
(assert (= (select findMeXY 0) _x_))
(assert (= (select findMeXY 1) _y_))
(assert (= (length findMeXY) 2))

;set x = 'x'
(assert (= (select x 0) _x_))
(assert (= (length x) 1))

;set xy = 'xy'
(assert (= (select xy 0) _x_))
(assert (= (select xy 1) _y_))
(assert (= (length xy) 2))

Теперь, когда проблема установлена, мы пытаемся найти подстроки: 

;search for findMeX='x' in x='x' 

(push 1)
(assert 
  (exists 
    ((offset Int)) 
    (and 
      (<= offset (- (length x) (length findMeX))) 
      (>= offset 0) 
      (forall 
        ((index Int)) 
        (=> 
          (and 
            (< index (length findMeX)) 
            (>= index 0)) 
          (= 
            (select x (+ index offset)) 
            (select findMeX index)))))))

(check-sat) ;'sat' expected, 'unknown' returned
(pop 1)

Если вместо этого мы ищем findMeXY в xy, решатель возвращает sat, как и ожидалось. Казалось бы, поскольку решатель может обрабатывать этот запрос для «xy», он должен иметь возможность обрабатывать его для «x». Кроме того, при поиске findMeX='x' в 'xy='xy' возвращается «неизвестно».

Может ли кто-нибудь предложить объяснение или, возможно, альтернативную модель для выражения этой проблемы в SMT-решателе?

1 Ответ

5 голосов
/ 23 августа 2011

Короткий ответ для наблюдаемого поведения: Z3 возвращает «неизвестно», потому что ваши утверждения содержат квантификаторы.

Z3 содержит много процедур и эвристик для обработки квантификаторов. Z3 использует технику, которая называется Insttiation Quantifier на основе модели (MBQI), для построения моделей для удовлетворения запросов, подобных вашему. Первый шаг состоит в том, что эта процедура состоит в создании возможной интерпретации, основанной на интерпретации, которая удовлетворяет утверждениям без квантификатора. К сожалению, в текущем Z3 этот шаг не взаимодействует гладко с теорией массива. Основная проблема заключается в том, что интерпретация, построенная на основе теории массивов, не может быть изменена этим модулем.

Справедливый вопрос: почему это работает, когда мы удаляем команды push / pop? Это работает, потому что Z3 использует более агрессивные шаги упрощения (предварительной обработки), когда команды инкрементного решения (такие как команды push и pop) не используются.

Я вижу два возможных решения вашей проблемы.

  • Вы можете избежать квантификаторов и продолжать использовать теорию массивов. Это возможно в вашем примере, так как вы знаете длину всех «строк». Таким образом, вы можете расширить квантификатор. Хотя этот подход может показаться неудобным, он используется на практике и во многих инструментах проверки и тестирования.

  • Вы можете избежать теории массивов. Вы объявляете строку как неинтерпретируемую сортировку, как вы сделали для Char. Затем вы объявляете функцию char-of, которая должна возвращать i-й символ строки. Вы можете аксиоматизировать эту операцию. Например, вы можете сказать, что две строки равны, если они имеют одинаковую длину и содержат одинаковые символы: 


(assert (forall ((s1 String) (s2 String))
                (=> (and 
                     (= (length s1) (length s2))
                     (forall ((i Int))
                             (=> (and (<= 0 i) (< i (length s1)))
                                 (= (char-of s1 i) (char-of s2 i)))))
                    (= s1 s2))))

Следующая ссылка содержит ваш скрипт, закодированный с использованием второго подхода: http://rise4fun.com/Z3/yD3

Второй подход более привлекателен и позволит вам доказать более сложные свойства строк. Тем не менее, очень легко написать выполнимые количественные формулы, что Z3 не сможет построить модель. Z3 Guide описывает основные возможности и ограничения модуля MBQI. Он может содержать разрешимые фрагменты, которые могут обрабатываться Z3. Кстати, обратите внимание, что теория отбрасывания массива не будет большой проблемой, если у вас есть квантификаторы. В руководстве показано, как кодировать массивы с помощью квантификаторов и функций.

Подробнее о том, как работает MBQI, можно узнать из следующих статей:

...