调整 Z3 中的“简化”策略

Question

我有几个关于 Z3 战术的问题，其中大部分是关于 simplify 的。

1. 我注意到应用simplify 后的线性不等式经常被否定。 例如(> x y) 由simplify 转换为(not (<= x y))。理想情况下，我希望整数 [in] 等式不被否定，以便 (not (<= x y)) 转换为 (<= y x)。我能保证这样的行为吗？

2. 此外，在 、>= 中，最好在简化公式的所有整数谓词中只使用一种类型的不等式，例如

3. simplify 的:som 参数有什么作用？我可以看到描述说它用于将多项式以单项形式表示，但也许我没有做对。您能否举一个将 :som 设置为 true 和 false 的简化行为的示例？

4. 我是对的，在应用simplify 算术表达式后将始终以a1*t1+...+an*tn 的形式表示，其中ai 是常量，ti 是不同的术语（变量、未解释的常量或函数符号） ?特别是减法运算总是不会出现在结果中的情况？

5. 有没有关于ctx-solver-simplify 策略的可用描述？从表面上看，我知道这是一个昂贵的算法，因为它使用了求解器，但是了解更多关于底层算法的信息会很有趣，这样我就可以知道我可能期望有多少求解器调用等等。也许你可以给出一个参考论文或给出算法的简要草图？

6. 最后，here 提到可能会出现关于如何在 Z3 代码库中编写战术的教程。有吗？

谢谢。

Answer 1

这是一个尝试回答问题 1-4 的示例（使用 cmets）。也可在线获取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-solver-simplify 在文件 src/smt/tactic/ctx-solver-simplify.* 中实现 代码可读性很强。我们可以添加跟踪消息以查看它在特定示例中的工作方式。

6) 目前还没有关于如何编写战术的教程。但是，代码库有很多示例。 目录src/tactic/core 包含基本目录。