#regex #z3
Вопрос:
У меня есть набор таких строк:
{«01», «001», 000111″, 01111″}
Теперь мне интересно, могу ли я попросить Microsoft Z3 найти минимальное регулярное выражение, удовлетворяющее строкам. Например, выходные данные для этого конкретного набора должны быть примерно такими 0*1* .
Комментарии:
1. Зачем, учитывая фиксированное количество строк, пытаться получить регулярное выражение, сгенерированное машиной? сомнительно, что вы получите одно регулярное выражение, которое соответствует только этим строкам, например
^0(?:1(?:111)?|0(?:011)?1)$2. На самом деле мне нужен минимальный.
3. @MojtabaValizadeh Какое понятие «минимального» вы имеете в виду? Существует много возможных определений (например, длина RE в виде строки или *-высота)?
4. @MartinBerger Длина RE в виде строки на этом этапе подходит.
Ответ №1:
В теории, да. На практике-да, но, вероятно, не так, как вы хотели. По крайней мере, пока нет.
Строго говоря, легко закодировать то, что вы хотите. Вот как вы бы закодировали проблему для нужного вам набора:
(set-logic QF_S)
(set-option :produce-models true)
(define-fun re1 () RegLan (str.to_re "01"))
(define-fun re2 () RegLan (str.to_re "001"))
(define-fun re3 () RegLan (str.to_re "000111"))
(define-fun re4 () RegLan (str.to_re "01111"))
(define-fun re5 () RegLan (re.union re1 re2 re3 re4))
(check-sat)
(get-value (re5))
И действительно, z3 говорит:
sat
((re5 (re.union (str.to_re "01")
(re.union (str.to_re "001")
(re.union (str.to_re "000111") (str.to_re "01111"))))))
Но я слышу, как ты стонешь и говоришь: «Но это не то, чего я хочу!» И действительно, хотя это правильное решение, это, вероятно, не то, что вы хотели. Это ни в коем случае не «минимально» в каком-либо удовлетворительном смысле.
Чтобы действительно сделать то, что вам нужно, вы хотите иметь возможность записывать переменные, которые сами могут соответствовать регулярным выражениям. И действительно, SMTLib и, следовательно, z3 позволяют регулярным выражениям быть символическими. Подробности смотрите здесь: https://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml. Однако вот прямая цитата с этой страницы о том, какие типы регулярных выражений разрешены:
Функция str.to_re позволяет писать символьные регулярные выражения, например, термины RegLan с подстроками, такими как (str.to_re x), где x-переменная. Такие термины обладают большей выразительной силой, чем регулярные выражения. Это сделано намеренно, для будущих разработок. Ограничение на фактические регулярные выражения будет наложено в логике, где str.to_re будет применим только к строковым константам.
И, насколько я знаю, пока нет SMT-решателя, включая z3, который поддерживал бы символические регулярные выражения. Вот простой эксперимент:
(set-logic QF_S)
(declare-fun x () RegLan)
(assert (str.in_re "0" x))
(check-sat)
Когда я передаю это z3, я получаю:
unknown
т. е. это действительно проблема, но z3 не может с ней справиться. Если вы передадите его в cvc4, он будет более громко говорить о проблеме:
(error "Regular expression variables are not supported.")
Итак, подведем итог: то, что вы пытаетесь сделать, возможно в SMTLib, но в настоящее время оно не поддерживается ни одним решателем, по крайней мере, не так, как вы хотели бы, чтобы оно работало. Надеюсь, в будущем это может измениться, хотя я бы не стал задерживать дыхание.
Учитывая это, что вы можете сделать? Я думаю, что использовать для этого SMT-решатель-это немного перебор. Для каждой постоянной строки вы можете построить регулярное выражение, которое ее распознает. Превратите это в DFA. А затем возьмите союз всех этих DFA. Наконец, превратите его в минимальный DFA и считайте регулярное выражение, которое от него исходит. Это довольно большая работа, но она должна хорошо работать на практике, т. е. все части этой стратегии хорошо известны, как ее реализовать, и должны быть довольно дешевыми с точки зрения сложности выполнения.
Комментарии:
1. Каковы основные препятствия, мешающие решателям SMT поддерживать эту функцию?
2. Я не знаю о каких-либо процедурах принятия решений, которые существуют, когда r.e. может быть символическим. Отсутствие такого алгоритма заставило бы разработчиков SMT уклоняться от чисто эвристических подходов. Предполагая, что такого результата не существует, я бы сказал, что это было бы достойно исследований на уровне аспирантов по разработке такого алгоритма или демонстрации того, что его не существует.