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

Question

Z3 输入格式是 SMT-LIB 2.0 standard. The input expressions need to write in prefix form. As for example 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 ）以给出最终表达式求解器。

是否有parser/library/API（最好是JAVA或任何其他语言）用算术运算符（+，-，<，>，=），命题逻辑连接符（ And, OR), Quantifiers(ForAll, Exists) 然后将输入提供给 Z3 求解器 ?

请提出建议和帮助。

Answer 1

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

z3 的官方 Python 接口：https://ericpony.github.io/z3py-tutorial/guide-examples.htm 这是 Microsoft 直接支持的，可能是最容易使用的。
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.

这些 "wrappers" 的目标是从复杂绑定的所有细节中精确地保存 end-user，并提供更容易和 less-error 易于使用的东西。另一方面，它们要求您学习另一个库。根据我的经验，如果您选择的宿主语言有这样的实现，那么使用它会带来很好的回报。如果没有，你应该建一个！

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

Is there way to give input as normal expression to Z3 Solver?

sat-solvers

smt

z3

sat

pysmt