Формат ввода Z3 является расширением формата, определенного стандартом SMT-LIB 2.0 . Входные выражения необходимо записать в виде префикса. Как например rise4fun ,
x + (y * 2) = 20 необходимо ввести в виде " (= (+ x (* 2 y)) 20)) ".
Z3 поддерживает JAVA API . В качестве примера рассмотрим приведенный ниже код, который оценивает и проверяет выражения выполнимости: x + y = 500 и x + (y * 2) = 20 .
final Context ctx = new Context();
final Solver solver = ctx.mkSimpleSolver();
IntExpr x = ctx.mkIntConst("x");
IntExpr y = ctx.mkIntConst("y");
IntExpr th = ctx.mkInt(500);
IntExpr th1 = ctx.mkInt(2);
IntExpr th2 = ctx.mkInt(20);
BoolExpr t1 = ctx.mkEq(ctx.mkAdd(x,y), th);
BoolExpr t2 = ctx.mkEq(ctx.mkAdd(x,ctx.mkMul(th1, y)), th2);
solver.add(t1);
solver.add(t2);
solver.check()
Проблема в том, что если внешний пользователь хочет дать входные данные для решающего устройства, он не может сделать это в форме общей формулы: «x + y = 500, x + (y * 2) = 20».
Входные данные должны быть проанализированы, а затем должны быть записаны вручную с использованием JAVA API в форме префикса (Примечание BoolExpr t2 в приведенном выше коде), чтобы дать окончательные выражения для Solver.
Существует ли какой-либо синтаксический анализатор / библиотека / API (предпочтительно JAVA или на любом другом языке), который анализирует общие выражения с арифметическими операторами (+, -, <,>, =), логическими коннекторами высказываний (И, ИЛИ), квантификаторами (ForAll, Exists) и затем вводит данные в Z3 Solvers?
Пожалуйста, предложите и помогите.