用Z3/SMT-LIB2定義集合的理論我試圖用ZTL3接口爲Z3定義集合的理論（聯合，交點等）

Question

。不幸的是，我目前的 定義掛起z3一個微不足道的查詢，所以我想我錯過了 一些簡單的選項/標誌。

這裏的永久鏈接：http://rise4fun.com/Z3/JomY

 
(declare-sort Set) 
(declare-fun emp() Set) 
(declare-fun add (Set Int) Set) 
(declare-fun cup (Set Set) Set) 
(declare-fun cap (Set Set) Set) 
(declare-fun dif (Set Set) Set) 
(declare-fun sub (Set Set) Bool) 
(declare-fun mem (Int Set) Bool) 
(assert (forall ((x Int)) (not (mem x emp)))) 
(assert (forall ((x Int) (s1 Set) (s2 Set)) 
      (= (mem x (cup s1 s2)) (or (mem x s1) (mem x s2))))) 
(assert (forall ((x Int) (s1 Set) (s2 Set)) 
      (= (mem x (cap s1 s2)) (and (mem x s1) (mem x s2))))) 
(assert (forall ((x Int) (s1 Set) (s2 Set)) 
      (= (mem x (dif s1 s2)) (and (mem x s1) (not (mem x s2)))))) 
(assert (forall ((x Int) (s Set) (y Int)) 
      (= (mem x (add s y)) (or (mem x s) (= x y))))) 

(declare-fun z3v8() Bool) 
(assert (not z3v8)) 
(check-sat) 

任何暗示，以我缺少的是什麼？另外，根據我所知，沒有標準SMT-LIB2 編碼的設置操作，例如， Z3.mk_set_{add,del,empty,...} （這就是我試圖通過量詞獲得該功能的原因。） 這是正確的嗎？還是有另一條路線？

謝謝！

Ranjit。

Answer 1

你的公式是可以滿足的，Z3不能爲這種公式生成模型。請注意，它必須爲未解釋的排序Set生成解釋。有幾種選擇你可以考慮。

1-禁用基於模型的量化器實例化（MBQI）模塊。順便說一句，所有基於Boogie的工具（VCC，Dafny，Coral等）都是這樣做的。要禁用MBQI模塊，我們必須使用

(set-option :auto-config false) 
(set-option :mbqi false) 

備註：在工作進行中的分支，選擇:mbqi已更名爲:smt.mbqi。

缺點：當MBQI模塊被禁用時，Z3通常會返回unknown用於包含量詞的可滿足公式。

2-將T的集合從T編碼爲布爾值。 Z3支持擴展陣列理論。擴展理論有兩個新運算符：((_ const T) a)常量數組，((_ map f) a b)映射運算符。 This paper描述了擴展數組理論，以及如何使用它對諸如聯合和交集等集合運算進行編碼。 rise4fun網站有例子。 這是一個很好的選擇，如果這些是你問題中唯一的量詞，因爲問題現在在一個可判定的片段中。另一方面，如果您有其他含有集合的量化公式，那麼這可能表現不佳。問題是由陣列理論建立的模型不知道附加量詞的存在。

例如如何編碼中使用const上述運營商和地圖看到：http://rise4fun.com/Z3/DWYC

3-代表組的T作爲在T函數爲BOOL。如果我們沒有集合或者以集合作爲參數的未解釋函數，這種方法通常可以很好地工作。 Z3在線教程有一個例子（量詞部分）。