Z3中未記錄的三角函數可修復？

Question

正式的，Z3沒有三角支持。例如，請參閱this question或this one。但是，在Z3中有沒有記載的三角函數運算符 - 它們在例如regression tests中使用。甚至還有一個內置符號pi。 Z3甚至可以做一些瑣碎的證據與這些運營商，例如：

(declare-fun x() Real) 
(assert (= (cos pi) x)) 
(check-sat) 
(get-value (x)) 

與回來：

sat 
((x (- 1.0))) 

這些運營商沒有很好地工作。例如，這個小輸入文件將導致賽格故障與Z3 4.4.1，或導致內存使用率迅速爆炸與主分支爲this commit（現在）：

(declare-fun x() Real) 
(assert (< (sin x) -1.0)) 
(check-sat) 

我並不感到驚訝，一個該團隊所說的不存在的未記錄功能不起作用。我的問題是：他們有可能解決嗎？什麼樣的性能水平會成爲Z3的合理補充？我知道我可以用Z3使用未解釋的函數和三角函數來做一些三角函數證明。 Z3團隊對此有興趣嗎？

Answer 1

感謝，Z3不應該在這樣的情況下崩潰。處理這些操作應該更加優雅。我現在檢查了一下這個問題，9b91e6f..cb29c07。 OTOH，這樣的操作員基本上沒有理論推理。例如，Z3不知道罪的界限。你必須自己公理化這些屬性。當您使用沒有（部分）決策程序支持的內置函數時，Z3會返回「未知」（或「不滿足」，但不是「已坐」）。