调整 Z3 中的“简化"策略 [英] Adjusting `simplify` tactic in Z3

问题描述

我有几个关于 Z3 策略的问题，其中大部分与 simplify 相关.

I've got several questions about Z3 tactics, most of them concern simplify .

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

1. I noticed that linear inequalites after applying simplify are often negated. For example (> x y) is transformed by simplify into (not (<= x y)). Ideally, I would want integer [in]equalities not to be negated, so that (not (<= x y)) is transformed into (<= y x).  I can I ensure such a behavior?

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

Also, among  <, <=, >, >= it would be desirable to have only one type of inequalities to be used in all integer predicates in the simplified formula, for example <=.   Can this be done?

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

What does :som parameter of simplify do? I can see the description that says that it is used to put polynomials in som-of-monomials form, but maybe I'm not getting it right.  Could you please give an example of different behavior of simplify with :som set to true and false?

在应用 simplify 后，算术表达式总是以 a1*t1+...+an*tn 的形式表示，其中 ai 是常量而 ti 是不同的术语(变量、未解释的常量或函数符号)?特别是结果中总是没有出现减法运算的情况?

Am I right that after applying simplify arithmetical expressions would always be represented in the form a1*t1+...+an*tn, where ai are constants and ti are distinct terms (variables, uninterpreted constants or function symbols)? In particular is always the case that subtraction operation doesn't appear in the result?

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

Is there any available description of the ctx-solver-simplify tactic? Superficially, I understand that this is an expensive algorithm because it uses the solver, but it would be interesting to learn more about the underlying algorithm so that I have an idea on how many solver calls I may expect, etc. Maybe you could give a refernce to a paper or give a brief sketch of the algorithm?

最后，这里提到了一个关于如何在 Z3 代码中编写策略的教程基地可能会出现.还有吗?

Finally, here it was mentioned that a tutorial on how to write tactics inside the Z3 code base might appear. Is there any yet?

谢谢.

推荐答案

这是一个尝试回答问题 1-4 的示例(带注释).它也可以在此处在线获得.

Here is an example (with comments) that tries to answer questions 1-4. It is also available online 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.* 中实现代码可读性很强.我们可以添加跟踪消息以查看它在特定示例上的工作方式.

5) ctx-solver-simplify is implemented in the file src/smt/tactic/ctx-solver-simplify.* The code is very readable. We can add trace messages to see how it works on particular examples.

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

6) There is no tutorial yet on how to write tactics. However, the code base has many examples. The directory src/tactic/core has the basic ones.

这篇关于调整 Z3 中的“简化"策略的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！