У меня проблема с использованием Java-API Z3 для сравнения строки с регулярным выражением.
Для некоторых целевых регулярных выражений:
"^[a-zA-Z]"
Когда я пытаюсь сопоставить строки с регулярными выражениями, он все равно распознается как строка.Например:
SeqExpr c1 = ctx.mkString("^[a-zA-Z]");
ReExpr c2 = ctx.mkToRe(ctx.mkString("abc"));
s.add(ctx.mkInRe(c1, c2));
s.check();
System.out.println("c1 = " + c1);
System.out.println("mkInRe = " + ctx.mkInRe(c1, c2));
System.out.println(s.check());
Результат:
c1 = "^[a-zA-Z]"
mkInRe = (str.in.re "^[a-zA-Z]" (str.to.re "abc"))
UNSATISFIABLE
Вся часть «^ [a-zA-Z]» распознается как строка, но не является регулярным выражением.
И я обнаружил, что Определяя ограничения в Z3 с помощью булевых операторов , этот вопрос будет сильно связан. Может ли нечто подобное с регулярным выражением быть сделано в Z3 Java?
Спасибо!