使用文本文件输入 Z3 模型答案

【问题标题】：Using a text file to input the Z3 model使用文本文件输入 Z3 模型
【发布时间】：2020-09-21 20:23:37
【问题描述】：

我通过其 .Net Api 使用 Z3。我构建的模型具有相当多的约束。到目前为止，我一直在使用相应的 Z3 命令（在 .Net Api 中）逐行构建我的模型。但是现在模型的大小已经增加，创建模型所需的时间非常可观。我在想有没有办法将模型构建为文本文件并将完成的模型一次性输入到 Z3 求解器？

【问题讨论】：

标签： .net z3

【解决方案1】：

您的问题相当神秘，但所有 SMT 求解器都支持所谓的 SMTLib2 输入格式：http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf

因此，至少在理论上，您可以将约束写入上述文档中描述的 SMTLib 格式的文件，然后对该文件调用 z3。

但这并不一定比直接使用 API 更快：事实上，我希望通过其 API 调用 z3 更快，因为它避免了“写入文件，从文件读取” “ 步;但如果您可以在多次调用中重用这些约束中的一些，它可能会在您的特定用例中更好地工作。

【讨论】：

【解决方案2】：

如果您使用的是 python api，如果您正在处理文本文件或字符串输入，则可以使用这两个函数：

parse_smt2_file() 和 parse_smt2_string() 你可以找到文档here

【讨论】：