Z3 Java应用程序开发

Question

我正在使用Java、MySQL DB和开发一个基于规则的系统应用程序。基本上，我需要建立一个系统，将规则存储在数据库中，然后检查数据库中规则的可满足性。我对此进行了研究，发现Z3是实现这一目的的合适工具。我的目标是用java编写一个脚本，以生成一个z3可以理解的https://rise4fun.com/z3类型的输出。对于这一点，正如用户在另一个答案中所建议的那样，有人建议，最简单的方法是用java编写我的脚本来生成z3代码，然后将它提供给z3，以检查它是sat还是unsat。现在我搞不懂如何将它集成到我的项目中？处理这个问题的唯一方法是尝试运行z3 java绑定，这会使使用起来非常困难吗？我基本上需要一个独立的服务，比如https://rise4fun.com/z3，它接受我的输入并给我输出，并且可以集成到我的项目中。甚至一个jar文件也行。一些可以与eclipse集成的东西

Answer 1

你的问题没有一个明显的答案，因为这“取决于”你的项目参数是什么。

Z3绑定有不同的风格。C/C++/Java是相当低级的.您可以使用它们来访问所有SMTLib功能，以及额外的功能。您可以构建独立的可执行文件并将它们发送出去。太棒了。但是它的代价是很低，很难编程和正确，调试和维护。我强烈警告不要使用他们，特别是如果你是新的SMT解决一般。

另一方面，Python绑定的级别相当高。它确实需要在目标计算机上安装Z3。如果您可以使用它，我建议这样做，因为它是最容易使用的。

如果您必须坚持使用Java，如果您是新手，我建议您坚持SMTLib格式:生成包含输入的文本文件，通过文件系统管道发送到Z3，或者调用system之类的方式，然后解析结果。这将确保您建立了正确的框架。一旦您对此感到满意，您就可以直接使用Java绑定来获得速度，并摆脱需要在目标计算机上安装z3的要求。

作为检验不同样式的一个例子：https://stackoverflow.com/a/50576844/936310在那里，首先使用C绑定来解决浮点SMT问题，然后使用Python和Haskell；您可以看到两者之间的区别。您的Java解决方案将非常类似于C版本。