Как типизировать String в тип BoolExpr, используя Z3 JAVA API? - PullRequest
Новая
       76

Как типизировать String в тип BoolExpr, используя Z3 JAVA API?

0 голосов
/ 01 июня 2019

Я пишу оболочку для ввода общего выражения (в общем виде, x + y> 20 (не в формате SMT2LIB)) в Z3 SAT Solver. В настоящее время я борюсь с типом строки в BoolExpr. Как в приведенном примере, 

String tr = "ctx.mkLt(ctx.mkIntConst(\"x\"),ctx.mkInt(100))";

Я хочу преобразовать приведенную выше строку в BoolExpr, а затем добавить ее в решатель, как: 

final Context ctx = new Context();
final Solver solver = ctx.mkSimpleSolver();
BoolExpr t2 =  ctx.mkBoolConst(tr);
solver.add(t2);
solver.check()

Я получаю ошибку при типизации String в BoolExpr. Я попытался использовать BoolExpr t2 = ctx.mkBoolConst(tr);, а затем добавить его в решатель, но это приводит к func-декларации.

Есть ли способ преобразовать строку в BoolExpr с использованием Z3 JAVA API , чтобы выражение можно было добавить и затем оценить с помощью Z3 Solver?

Пожалуйста, помогите и предложите.

...