縮小量詞的範圍在Z3

有是可用於通過結合分配通用量詞一個distribute-forall戰術。我對通用量詞和存在量詞都有一個更一般化的程序感興趣，它們儘可能地縮小了量詞的範圍。例如，我想式縮小量詞的範圍在Z3

(exists ((x Int)) (and (= z (* 2 x)) (<= z y)))被轉化成

(and (exists ((x Int)) (= z (* 2 x)) (<= z y)))。

這可以通過一些其他的戰術（S）來完成？

2013-04-08 Egbert

在Z3代碼庫的分支mcsat有一個名爲miniscope新戰術。它做你想要的。我們可以使用these instructions建立mcsat分支。我們只需要將替換爲mcsat。

下面是使用這種戰術的一些例子。

(declare-const z Int) 
(declare-const x Int) 
(declare-const y Int) 

(assert (exists ((x Int)) (and (= z (* 2 x)) (<= z y)))) 

(apply miniscope)

和所產生的輸出

(goals 
(goal 
    (<= z y) 
    (exists ((x!1 Int)) (= z (* 2 x!1))) 
    :precision precise :depth 3) 
)

下面是一個更復雜的例子：

(set-option :pp.max-depth 100) 
(declare-fun p (Int) Bool) 
(declare-fun q1 (Int Real) Bool) 
(declare-fun q2 (Real Real) Bool) 
(declare-fun q3 (Int Int) Bool) 

(assert (forall ((x1 Int) (x2 Real)) 
       (or (q2 x2 x2) (exists ((y Real)) (and (q1 y x2) (q1 x1 x2)))))) 

(apply miniscope)

和所產生的輸出

(goals 
(goal 
    (forall ((x2 Real)) 
    (or (q2 x2 x2) 
     (and (forall ((x1 Int)) (q1 x1 x2)) 
      (exists ((y Real)) (q1 (to_int y) x2))))) 
    :precision precise :depth 3) 
)

EDIT

mcsat分支包含正在進行的工作，最終將合併到master分支中。但是，下一次正式發佈（v4.3.2）可能不會發生合併。當我們發佈新版本時，我們將unstable和contrib分支合併到master分支中。

的mcsat分支基本上是增加新的功能。它與unstable和contrib分支不兼容。

我們鼓勵高級用戶（熟悉的git）使用非官方發佈和選擇分支。當然，在報告錯誤/問題時，應該使用與提交相關聯的git散列，而不是版本號。

編輯完

來源

2013-04-08 16:38:44

謝謝。「miniscope」戰術是一個特定分支的戰術嗎？我的意思是，你認爲可以用較低的努力將它與主分支的源代碼「集成」嗎？我只是不知道mcsat分支如何與主分支不同，所以我不知道切換到該分支可能會有什麼影響。你是否計劃最終在主要分支中添加策略？ – Egbert 2013-04-09 08:55:35

我擴展了有關'mcsat'分支的更多信息。 – 2013-04-09 17:14:52

縮小量詞的範圍在Z3

回答

相關問題