調整Z3中的簡化策略

Question

我有幾個關於Z3策略的問題，其中大部分都涉及simplify。

1. 我注意到，應用simplify後直線inequalites經常否定。 例如，(> x y)由simplify轉換成(not (<= x y))。理想情況下，我希望整數[in]的平等不被否定，以便(not (<= x y))轉換爲(<= y x)。我可以保證這樣的行爲嗎？

2. 另外，當中<，< =，>，> =，將期望具有在簡化公式中的所有整數謂詞中使用僅一種類型的不等式，例如< =。這可以做到嗎？

3. :som參數simplify是做什麼用的？我可以看到這樣的描述：它用於將多項式放在單數形式中，但也許我沒有把它做對。你能舉一個簡單的例子嗎？:som設置爲true和false？

4. 我是否正確的施加simplify算術表達式將總是在形式a1*t1+...+an*tn來表示，其中ai是常數，ti是不同的術語（變量，未解釋的常量或功能符號）之後？特別是總是減法操作沒有出現在結果中？

5. 是否有任何可用的描述ctx-solver-simplify策略？從表面上看，我知道這是一個昂貴的算法，因爲它使用求解器，但是學習更多關於底層算法的知識會很有趣，這樣我就可以知道我可能會有多少求解器調用等等。也許你可以給出一個參考一篇論文或給出算法的簡要概述？

6. 最後，here有人提到，有關如何在Z3代碼庫內編寫策略的教程可能會出現。還有嗎？

謝謝。

Answer 1

下面是一個試圖回答問題1-4的例子（帶有評論）。它也可以在線here。

(declare-const x Int) 
(declare-const y Int) 

;; 1. and 2. 
;; The simplifier will map strict inequalities (<, >) into non-strict ones (>=, <=) 
;; Example: x < y ===> not x >= y 
;; As suggested by you, for integer inequalities, we can also use 
;;   x < y ==> x <= y - 1 
;; This choice was made because it is convenient for solvers implemented in Z3 
;; Other normal forms can be used. 
;; It is possible to map everything to a single inequality. This is a straightforward modificiation 
;; in the Z3 simplifier. The relevant files are src/ast/rewriter/arith_rewriter.* and src/ast/rewriter/poly_rewriter.* 
(simplify (<= x y)) 
(simplify (< x y)) 
(simplify (>= x y)) 
(simplify (> x y)) 

;; 3. 
;; :som stands for sum-of-monomials. It is a normal form for polynomials. 
;; It is essentially a big sum of products. 
;; The simplifier applies distributivity to put a polynomial into this form. 
(simplify (<= (* (+ y 2) (+ x 2)) (+ (* y y) 2))) 
(simplify (<= (* (+ y 2) (+ x 2)) (+ (* y y) 2)) :som true) 

;; Another relevant option is :arith-lhs. It will move all non-constant monomials to the left-hand-side. 
(simplify (<= (* (+ y 2) (+ x 2)) (+ (* y y) 2)) :som true :arith-lhs true) 

;; 4. Yes, you are correct. 
;; The polynomials are encoded using just * and +. 
(simplify (- x y)) 

5）CTX-求解器簡化文件src/SMT /策略/ CTX-求解器簡化。* 的代碼非常可讀被實現。我們可以添加跟蹤消息來了解它是如何在特定示例上運行的。

6）目前還沒有關於如何寫策略的教程。但是，代碼庫有很多例子。 目錄src/tactic/core有基本的。