有什麼辦法從SMT表達式中獲得係數值？

Question

我想知道是否有一些SMT命令來獲取相關聯的表達係數值爲以下

(assert (>= (+ x (* (/ -1 2) y)) 0.0)) 

因此獲得值1和-0.5。

謝謝你的任何提示。

Answer 1

SMT-LIB2命令語言通常具有用於編程的任何設施。 Z3公開了一個python API，使您能夠以可讀的方式記錄公式。 此外，您可以使用python和API編寫用於執行表達式的函數。 在http://rise4fun.com/z3py 上有一個在線版本的Python API，並且有一個關聯該教程的主要功能。