1

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

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

4

1 回答 1

1

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

话虽如此，现有的策略都不能完全满足您的要求。我认为最接近的是量词消除策略/命令。在您的示例中，我们可以使用量词消除过程来消除local和。当然，这个过程可能非常昂贵，而且它所做的不仅仅是替换变量。这是一个例子。我使用的是 command而不是 tactic 。此外，如您所见，结果不一定采用我们称之为“简化”的格式。我们通过量词消除程序提供的唯一保证是：如果成功，则结果公式等价于输入公式。我们可以用 Z3 来证明由 产生的结果确实等价于公式。local_1midsepelim-quantifiersqeelim-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))))
于 2012-06-19T18:59:29.943 回答