微软Z3:将表达式转换为特定变量

Question

我正在使用微软的Z3进行一些简单的动态观察分析。作为其中的一部分，如果我可以将一些公式从使用一组变量转换为另一组目标变量，这将是很有帮助的。

我对Z3真的很陌生，但我知道它有一些内部简化规则和其他转换公式的方法……基本上，我想知道是否有可能进行一些转换，比如：

(declare-const local Real)
(declare-const x Real)
(declare-const y Real)
(declare-const midstep Real)
(declare-const local_1 Real)
(declare-const foo_ret Real)

(assert (= local (/ x y)))
(assert (= midstep local))
(assert (= local_1 (+ midstep 1.0)))

(assert (= foo_ret local_1) :name toTransform)

; this is what I'd love to do - give Z3 a formula and a target set of variables
(special-simplify (= foo_ret local_1) (foo_ret x y))
; and have Z3 do the appropriate substitutions, etc to spit back 
; a "simplified" version in terms of foo_ret, x, and y, e.g.: 
;    (= foo_ret (+ (/ x y) 1.0))

我认识到这并不是Z3的主要目标，但我知道它已经具备了一些简化/解决问题的能力……从帮助文本判断，我得到的印象是，有方法可以设计目标状态和实现它们的策略，但我真的找不到基于Z3的(help)命令如何做到这一点的信息(除非我遗漏了什么……)。

我真的不想做任何复杂的事情--只是简单地替换/消除不在目标集合中的符号……我想知道有没有什么方法可以让这个工具这么做？

Answer 1

Z3 4.0支持战术。它们可用于预处理公式并应用多个转换。tutorial http://rise4fun.com/z3/tutorial/guide包含有关此新功能的更多信息。命令(help-tactic)将显示Z3中所有可用的战术。

也就是说，现有的策略都不能完全满足您的要求。我认为最接近的是量词剔除策略/命令。在您的示例中，我们可以使用量词消除过程来消除local、local_1和midsep。当然，这个过程可能非常昂贵，而且它所做的不仅仅是替换变量。下面是一个例子。我使用的是elim-quantifiers命令，而不是qe。此外，正如您可以观察到的，结果不一定是我们称之为“简化”的格式。量词消除过程提供的唯一保证是:如果成功，则结果公式等同于输入公式。我们可以使用Z3来证明elim-quantifiers产生的结果确实等价于公式(= foo_ret (+ (/ x y) 1.0)))。

http://rise4fun.com/Z3/jzZF

(declare-const x Real)
(declare-const y Real)
(declare-const foo_ret Real)

(set-option :pp-max-depth 100)

(elim-quantifiers 
  (exists ((local Real) (midstep Real) (local_1 Real))
    (and (= local (/ x y))
         (= midstep local)
         (= local_1 (+ midstep 1.0))
         (= foo_ret local_1))))