線性運算證明

Question

鑑於以下SMT2腳本禁用引進斯科倫功能：

(set-option :produce-proofs true) 
(set-logic AUFLIRA) 
(declare-sort Complex$ 0) 
(declare-fun r$() Real) 
(declare-fun s$() Complex$) 
(declare-fun re$ (Complex$) Real) 
(declare-fun norm$ (Complex$) Real) 
(assert (! (not (=> (and (forall ((?v0 Complex$)) (<= (ite (< (re$ ?v0) 0.0) (- (re$ ?v0)) (re$ ?v0)) (norm$ ?v0))) (<= (norm$ s$) r$)) (<= (ite (< (re$ s$) 0.0) (- (re$ s$)) (re$ s$)) (+ r$ 1.0)))) :named a0)) 
(check-sat) 
(get-proof) 

Z3（不穩定版）產生包含斯科倫功能「規範$ 0」的證明。在重寫步驟中引入此功能：

(ALL v0. (if 0 <= Re v0 then Re v0 else - 1 * Re v0) <= cmod v0) = 
((ALL v0. cmod v0 = (if 0 <= Re v0 then Re v0 else - 1 * Re v0) + norm_0 v0) & (ALL v0. 0 <= norm_0 v0)) 

此行爲可以通過命令行開關抑制嗎？也就是說，有沒有這樣的選擇，使得Z3產生沒有這種Skolem函數的證明？原則上這應該是可能的，因爲Z3版本3.2找到了不需要Skolem函數的證明。

Answer 1

斯科爾姆常數由MBQI（基於模型的量詞實例化）模塊引入。這可能是使你看到不同行爲的「新部分」。 MBQI比基於模式的量詞實例化功能強大得多。 但是，對於您的示例，基於模式的量詞實例化策略起作用。所以你可以試試這個。

在運行Z3換句話說如下抑制MBQI：

Z3斯科倫-example.smt2 smt.mbqi =假自動配置=假