【发布时间】：2019-12-15 16:45:17
【问题描述】：
好吧，我可以用Java绑定在eclipse中运行z3 solver，使用语言是Java，但是我需要使用SMT-LIB格式在eclipse中运行z3 solver，我该怎么做呢？
我对诸如 jSMTLIB 项目之类的东西进行了研究，我不知道它是否有效。 还有这个网How to run Z3 in Java from SMT-Lib standard?，看起来很像，但不是重点。
【问题讨论】：
【发布时间】：2019-12-15 16:45:17
【问题描述】：
SMTLib 是 z3（和其他 SMT 求解器）理解的基于文本的格式。问“如何使用 Eclipse 和使用 SMT-Lib 格式”真的没有意义。它只是一个 ASCII 文本文件。
如果你描述你想要达到的目标，你可以获得更好的答案；听起来您可能遇到了经典的 XY 问题，请参见此处：https://mywiki.wooledge.org/XyProblem
【讨论】：