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

Я пытаюсь использовать 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?


z3 smt
person Katie    schedule 19.08.2011    source источник
comment
Пробовал воспроизвести описанную вами проблему, но безуспешно. Какую версию Z3 вы используете? Я попытался использовать Z3 2.19 (Windows и Linux) и Z3 3.0 (доступен на веб-сайте SMT-COMP), и все они вернули соответствие запросу выше. Спасибо, Лео.   -  person Leonardo de Moura    schedule 20.08.2011
comment
Спасибо за комментарий, Лео, и вы заставили меня понять, что я кое-что упустил из виду. Кажется, что поведение, которое я испытал, происходит только тогда, когда между командами push и pop появляются финальное утверждение и check-sat, которые я использовал, чтобы попробовать различные эксперименты в одном и том же наборе утверждений. Я соответствующим образом изменил вопрос, хотя теперь кажется, что проблема связана с областью действия. Если push и pop опущены, то вы правы, 'sat' возвращается во всех случаях.   -  person Katie    schedule 21.08.2011
comment
Возможно, вы ищете это: cs.purdue.edu/homes/zheng16/str   -  person user    schedule 16.01.2014

Ответы (1)


arrow_upward
6
arrow_downward

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

Z3 содержит множество процедур и эвристик для обработки квантификаторов. Z3 использует метод, называемый созданием квантификаторов на основе моделей (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 описаны основные возможности и ограничения модуля MBQI. Он содержит множество разрешимых фрагментов, которые может обрабатывать Z3. Кстати, обратите внимание, что отказ от теории массивов не будет большой проблемой, если у вас есть квантификаторы. В руководстве показано, как кодировать массивы с помощью квантификаторов и функций.

Дополнительную информацию о том, как работает MBQI, можно найти в следующих документах:

person Leonardo de Moura    schedule 22.08.2011