在z3中設置成員關係

Question

我想用C++ API在Z3中定義成員關係。我想通過以下方式做的：

z3::context C; 
z3::sort I = C.int_sort(); 
z3::sort B = C.bool_sort(); 
z3::func_decl InSet = C.function("f", I, B); 

z3::expr e1 = InSet(C.int_val(2)) == C.bool_val(true); 
z3::expr e2 = InSet(C.int_val(3)) == C.bool_val(true); 
z3::expr ite = to_expr(C, Z3_mk_ite(C, e1, C.bool_val(true), 
    Z3_mk_ite(C,e2,C.bool_val(true),C.bool_val(false)))); 
errs() << Z3_ast_to_string(C,ite); 

在這個例子中，一組由整數2和3由我肯定有一個更好的方式來定義的關係，特別是一組成員關係，但我真的是一名Z3新秀。有誰知道最好的？

Answer 1

在Z3中，集合通常使用謂詞（如您所做的）或布爾數組進行編碼。在Z3 C API中，有幾個用於創建設置表達式的函數：Z3_mk_set_sort,Z3_mk_empty_set,Z3_mk_set_union，...實際上，這些函數正在創建數組表達式。它們代表一組T作爲從T到布爾的數組。他們使用this article中描述的編碼。

備註：在Z3中，InSet(C.int_val(2)) == C.bool_val(true)相當於InSet(C.int_val(2))。 InSet函數是一個謂詞。我們可以寫std::cout << ite而不是std::cout << Z3_ast_to_string(C, ite)。

在基於謂詞的方法中，我們通常需要使用量詞。 在你的例子中，你所說的2和3是該集合的元素，但要說沒有其他元素是一個元素，我們需要一個量詞。我們還需要量詞來表示屬性，例如：set A等於集合B和C的並集。基於量詞的方法更靈活，例如我們可以說A是包含1和n之間的所有元素的集合。 缺點是創建不在Z3可處理的可判斷片段中的公式非常簡單。 Z3教程介紹了其中的一些片段。這裏是一個來自教程的例子。

;; A, B, C and D are sets of Int 
(declare-fun A (Int) Bool) 
(declare-fun B (Int) Bool) 
(declare-fun C (Int) Bool) 
(declare-fun D (Int) Bool) 

;; A union B is a subset of C 
(assert (forall ((x Int)) (=> (or (A x) (B x)) (C x)))) 

;; B minus A is not empty 
;; That is, there exists an integer e that is B but not in A 
(declare-const e Int) 
(assert (and (B e) (not (A e)))) 

;; D is equal to C 
(assert (forall ((x Int)) (iff (D x) (C x)))) 

;; 0, 1 and 2 are in B 
(assert (B 0)) 
(assert (B 1)) 
(assert (B 2)) 

(check-sat) 
(get-model) 
(echo "Is e an element of D?") 
(eval (D e)) 

(echo "Now proving that A is a strict subset of D") 
;; This is true if the negation is unsatisfiable 
(push) 
(assert (not (and 
       ;; A is a subset of D 
       (forall ((x Int)) (=> (A x) (D x))) 
       ;; but, D has an element that is not in A. 
       (exists ((x Int)) (and (D x) (not (A x))))))) 
(check-sat) 
(pop)