z3解决方案: Mac平台上的z3-SMT

Question

我需要为我的硕士论文工作的Z3 SMT解决方案。我已经检查了Z3-SMT的教程，这是基于SMT输入的。但是我只能安装z3-Py，它需要Python的知识。我想知道是否有可能在Mac上使用SMT前端安装z3。如果是的话，你能帮忙吗？

Answer 1

运行SMT脚本的最简单方法是使用rise4fun接口：http://rise4fun.com/Z3。

尽管如此，如果出现大问题或其他程序，您可能需要脱机运行Z3。听起来好像您已经安装了Z3，因为您已经使用了z3py。如果您成功地安装了z3py，那么您也可以运行Z3，因为z3py依赖于Z3 (从技术上讲是一个z3库，但是如果从codeplex获得源代码并编译了它，则可能同时安装了库和可执行文件)。有关所有平台的编译和安装说明，请参阅：https://z3.codeplex.com/SourceControl/latest#README

安装后，您可以在名为test.smt的SMT 2文件上使用test.smt执行./z3 -smt2 test.smt可执行文件(如果将其放置在路径上，则只执行z3 -smt2 test.smt )。