z3 - 调整Z3中的 `simplify`策略

Question

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

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

2. 此外，在 <、<=、>、>= 中，希望在简化公式中的所有整数谓词中只使用一种类型的不等式，例如 <=。这能做到吗？

3. :som 是什么意思？ simplify 的参数做？我可以看到描述说它用于将多项式置于单项式的形式中，但也许我没有做对。您能否举例说明使用 :som 进行简化的不同行为？设置为真假？

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-solver-simplify 在文件 src/smt/tactic/ctx-solver-simplify 中实现。*代码可读性很强。我们可以添加跟踪消息以查看它在特定示例上的工作方式。

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