通過z3 python api和直接從可執行文件調用smtlib2求解器時的輸出差異？

Question

我正在使用z3 python api。當我使用z3 python api解決約束條件時，求解器運行無限且不會引發錯誤。但是，當相同的約束以smtlib2格式轉儲並通過z3可執行文件解決時，它幾乎可以立即給出sat或not。 smtlib2轉儲非常大（大約1000行）。雖然對於少數的約束，z3 api工作正常。 z3 python api中是否存在處理大量約束的錯誤？

Answer 1

例如，當兩種方法之間的配置不同（甚至略有不同）時，或者當問題不完全相同（例如約束的不同順序）時，可能發生這種情況。一些策略也是非確定性的（例如，它們在預處理中使用定時器），並且可執行文件稍微更快/更慢。要診斷導致差異的原因，我們需要查看一些問題，或者至少是某些診斷輸出，例如，在命令行中添加-v：10並將全局「verbosity」選項設置爲10.