当在命令行上使用 Z3 并使用“-T”开关时，有没有办法将超时设置为小于一秒？
我知道您可以将超时设置为小于使用 API 的超时，但由于各种愚蠢的原因，我一直在循环中将包含 SMT-LIBv2 脚本的文本文件传递给 Z3(请不要生气)，认为它也会同样有效。我刚刚注意到这种方法似乎创建了一秒的超时下限。如果我使用 Z3 检查数千个短文件，这会大大减慢速度。
我理解事情是否就是这样，并且我承认，当 Z3 已经有一个完美的 API 时，我所做的事情是不明智的。
最佳答案
有两个选项:
您可以使用“软超时”。它们不如超时/T 可靠，因为仅定期检查软超时到期时间。然而，选项“smt.soft_timeout=10”将设置超时为 10 毫秒(而不是 10 秒)。您可以使用 (set-option :smt.soft_timeout 10) 从命令行和 SMT-LIB2 文件中设置这些选项。有关使用策略/求解器的教程还解释了如何使用更高级的功能(策略)，您还可以使用文本界面中的选项(例如超时)来控制这些高级功能。
您可以从编程 API 加载 SMT-LIB2 文件。文件中的断言存储在连词中。然后，您可以调用求解器(再次从 API)并使用求解器对象的“软超时”选项。没有真正的理由使用选项 2，除非您需要加快管道速度或使用软超时功能以外的其他功能，因为它已经合理地暴露于 SMT-LIB 级别。
关于Z3 命令行超时，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/25452861/