3

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 或任何其他语言）使用算术运算符（+、-、<、>、=）、命题逻辑连接器（And、OR）、量词（ForAll、存在）然后向 Z3 Solvers 提供输入？

请建议和帮助。

4

1 回答 1

3

这正是人们为 SMT 求解器构建高级接口的原因。z3 这里有很多选择：

这些“包装器”的目标是准确地将最终用户从复杂绑定的所有细节中解救出来，并提供更容易使用且不易出错的东西。另一方面，它们要求您学习另一个库。根据我的经验，如果您选择的宿主语言有这样的实现，那么使用它会得到很好的回报。如果没有，你应该建立一个！

于 2019-05-30T00:55:56.737 回答