Как использовать Z3 Java-API для генерации констант строк? - PullRequest
Новая
       9

Как использовать Z3 Java-API для генерации констант строк?

0 голосов
/ 09 июля 2019

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

Если речь идет о числе, я могу использовать код как 

ctx.mkRealconst()
ctx.mkIntconst()

, чтобы сгенерировать const, затем используйте код, подобный 

ctx.mkEq()

чтобы добавить ограничения. Как 

RealExpr a = ctx.mkRealConst("a");  
RealExpr b = ctx.mkRealConst("b"); 
BoolExpr equation = ctx.mkEq(a, b);
s.add(equation);

Но когда он изменяется на Strings, использование ctx.mkString () может генерировать только реальные строки.

Например, 

SeqExpr a = ctx.mkString(“a”);

может быть только строкой «а», но не константой.

Также я пытаюсь использовать ctx.getStringSort () для создания строк, 

Sort string = ctx.getStringSort();
Expr a1 = ctx.mkConst("a1", string);
Expr a2 = ctx.mkConst("a2", string);

но когда я пытаюсь использовать его, сравните с ограничениями, 

SeqExpr s1 = ctx.mkString("a");
SeqExpr s2 = ctx.mkString("z");

ReExpr cc = ctx.mkRange(s1, s2);
ReExpr str = ctx.mkPlus(cc);

показывает, что сортировка не может сравниваться с регулярным выражением. 

Exception in thread "main" com.microsoft.z3.Z3Exception: Sorts String and (RegEx String) are incompatible

Что мне поменять на код? Или каким способом я должен использовать для генерации строки?

Спасибо!

...