3

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

  1. 我注意到应用后的线性不等式simplify经常被否定。例如(> 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. 最后，这里提到可能会出现一个关于如何在 Z3 代码库中编写战术的教程。有吗？

谢谢你。

4

1 回答 1

4

这是一个尝试回答问题 1-4 的示例（带有注释）。它也可以在这里在线获得。

(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具有基本目录。

于 2013-04-08T15:40:36.817 回答