防止解決方案被簡化

我想使用let語句從z3中獲得解決方案而無需簡化。防止解決方案被簡化

例如，如果我給出如下：

(declare-const x Int) 
    (elim-quantifiers (exists ((x.1 Int)) 
    (and (or (and (= (- x.1 2) 0) (<= (- x.1 9) 0)) 
      (and (or (= (- x.1 2) 0) (and (<= (- x.1 4) 0) 
             (and (<= (- 4 x.1) 0) 
              (<= (- x.1 11) 0)))) (<= (- x.1 9) 0))) (= (- (+ x.1 2) x) 0))))

我回來瞭解決方案：

(let ((a!1 (and (or (and (<= x 4) (>= x 4)) (and (<= x 6) (>= x 6) (<= x 13))) 
       (<= x 11)))) 
    (or (and (<= x 4) (>= x 4) (<= x 11)) a!1))

有沒有辦法告訴Z3不提取一些複雜的表達式爲let語句？如果我在沒有發言權的情況下得到答案，我將更容易解析結果。

來源

2012-11-19 sriraj

我們可以設置下面的選項，以防止Z3相當打印機使用let小號

(set-option :pp-min-alias-size 1000000) 
(set-option :pp-max-depth  1000000)

任何大的數字就可以了。

我們必須記住，當我們避開let時，顯示一些包含大量共享子表達式的公式可能不太可行。在內部，Z3將公式存儲爲DAG而不是樹。如果我們不使用let，那麼這些公式的漂亮版本可能會比它們的內部表示呈指數級增長。所以，我們不應該濫用上述選項。

來源

2012-11-19 22:23:49

謝謝。這有很大幫助。 – sriraj

太好了。你能接受答案嗎？因此，其他用戶會知道答案可以解決問題中發佈的問題。謝謝 –

這些選項是否也可以使用C API設置，如果是的話，怎麼樣？ –

我正在使用z3-4.5.0，看起來選項名稱已經改變了一些。如果pp-max-depth不適用於您，請嘗試pp.max_depth和pp.min_alias_size。

我使用的Java API和與我下面的工作

com.microsoft.z3.Global.setParameter("pp.min_alias_size", "1000000"); 
com.microsoft.z3.Global.setParameter("pp.max_depth", "1000000");

來源

2017-06-29 21:26:04 Mohammed

防止解決方案被簡化

回答

相關問題