使用文本文件输入 Z3 模型 [英] Using a text file to input the Z3 model

问题描述

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

I am using Z3 through its .Net Api. I build models which have considerably huge number of constraints. Until now I have been using the respective Z3 commands (in the .Net Api) to build my model line by line. But now that the model has increased in size the time it takes to create the model is very considerable. I was thinking is there a way to build the model as a text file and input the completed model to a Z3 solver in one go?

推荐答案

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

Your question is rather cryptic, but all SMT-solvers support the so called SMTLib2 input format: http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf

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

So, at least in theory, you can write your constraints to a file in the SMTLib format as described in the above document and then call z3 on that file.

但这并不一定比直接使用 API 更快:事实上，我希望通过其 API 调用 z3 会更快，因为它避免了写入文件，读取 -档案"步;但如果您可以在多次调用中重用这些约束中的一些，它可能在您的特定用例中效果更好.

But this isn't necessarily going to be faster than using the API directly: In fact, I'd expect calling z3 via its API to be faster since it avoids the "write-to-file, read-from-file" step; but it might work well better in your particular use case if you can reuse some of these constraints over many calls.

这篇关于使用文本文件输入 Z3 模型的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！