有没有办法将输入作为正常表达式提供给 Z3 Solver？

Question

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, Exists) 然后向 Z3 Solvers 提供输入？

请提出建议和帮助。

Answer 1

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

• z3 的官方 Python 接口：https://ericpony.github.io/z3py-tutorial/guide-examples.htm 这是微软直接支持的，可能是最容易使用的。

• PySMT，旨在涵盖尽可能多的 SMT 求解器：https://github.com/pysmt/pysmt

• Scala 绑定：https://github.com/epfl-lara/ScalaZ3

• Haskell SBV：http://hackage.haskell.org/package/sbv

• 许多其他处于不同成熟度级别的 Racket、Go、Lisp.. 你可以说出来。你可以在 github 上找到其中的许多。

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