Microsoft Z3：將表達式轉換爲特定變量

我正在使用Microsoft的Z3進行動態觀察的一些簡單分析。作爲其中的一部分，如果我可以將某些公式從一組變量轉換爲另一組目標變量，將會有所幫助。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)命令（除非我失去了一些東西......）。

我真的沒有想要做任何複雜的事情 - 只是簡單的替換/消除不在目標集合中的符號......我想知道是否有某種方法可以讓工具變成這樣做？

來源

2012-06-19 Sean

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))))

來源

2012-06-19 18:59:29

Microsoft Z3：將表達式轉換爲特定變量

回答

相關問題