Microsoft Z3：将表达式转换为特定变量答案

【问题标题】：Microsoft Z3: Convert expressions to specific variablesMicrosoft Z3：将表达式转换为特定变量
【发布时间】：2012-06-19 18:07:30
【问题描述】：

我正在使用 Microsoft 的 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) 命令找到有关如何做到这一点的信息（除非我遗漏了什么......）。

我并不想做任何复杂的事情 - 只是简单地替换/消除不在目标集中的符号...我想知道是否有某种方法可以诱使该工具执行此操作？

【问题讨论】：

标签： z3 solver smt

【解决方案1】：

Z3 4.0 支持战术。它们可用于预处理公式并应用多种转换。教程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))))

【讨论】：