z3 - 有没有办法将输入作为正常表达式提供给 Z3 求解器？

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 求解器 ?

请提出建议和帮助。

Answer 1

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

• z3 的官方 Python 接口(interface):https://ericpony.github.io/z3py-tutorial/guide-examples.htm这是由 Microsoft 直接支持的，并且可能是最容易使用的。

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

• Scala 绑定(bind):https://github.com/epfl-lara/ScalaZ3

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

• 许多其他人在 Racket、Go、Lisp 等方面处于不同的成熟度级别。应有尽有。您可以在 github 上找到其中的许多内容。

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