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