z3 MaxSAT示例错误

我有兴趣使用z3（Microsoft Research）网站上提供的MaxSAT/MaxSMT c示例（特别是maxsat.c）。使用Visual Studio 2010，我最终得到了编译示例（使用全新安装的z3 4.0）。但是，我无法使用我的（SMT 2.0）模型来运行它们。此外，我无法获得发布在this问题中的示例。z3 MaxSAT示例错误

在第一种情况下，当我编译的程序试图调用文件get_hard_constraints中的Z3_get_smtlib_num_formulas时崩溃。我不知道为什么，而是我得到标准的Windows 7“这个程序已停止工作”弹出。

在第二种情况下，它报告unsupported ;benchmark。

为了帮助我完成这项工作，我在想如果（a）编译此代码时是否有人遇到过类似的问题？如果是的话，您是如何解决这些问题的？（b）如何调试文件的编译（假设它是正确的）？也就是说，是否有人可以枚举正确的库（和库版本 - 例如z3 4.0？）以包含在编译器选项中以使此示例正常工作？

在任何一种情况下，第二种情况中报告的错误信息也将被赞赏：它究竟意味着什么？关键字无效？ SMT输入是错误的版本？或者是其他东西？

谢谢。

来源

2012-09-27 Jan Gorzny

MaxSAT示例尚未更新为SMTLIB 2.0。它使用函数Z3_parse_smtlib_file来解析输入，这意味着它目前仅支持SMTLIB 1.0。

本例与Z3一起发布，即您应该收到Z3-4.0/examples/maxsat/的副本，其中也包含编译和执行脚本。

通过在Visual Studio命令提示符下运行build.cmd或在Linux上运行build.sh，编译应该很简单。

来源

2012-09-27 18:46:46

感谢您的回答。这个例子也不起作用（我之前忘了提及这个），但我解决了这个问题（一些环境变量没有设置）。你知道是否有可能用新的函数调用（也可能是其他任何特定于旧标准的函数调用），并让它在SMTLIB 2.0上工作？ –

是的，还有一个SMT2函数，它被称为Z3_parse_smtlib2_file。该示例将需要进一步修改，因为此函数仅返回单个表达式，而不是一组假设和一组公式。所以，目前还不清楚如何区分SMT2中的软硬件限制（也许这可以通过注释完成）。 –

z3 MaxSAT示例错误

回答

相关问题