0

Z3 で C++ API を使用してメンバーシップ関係を定義したいと考えていました。私は次の方法でそれを行うことを考えました：

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 初心者です。誰もが最高のものを知っていますか？

4

1 に答える 1

2

Z3では、セットは通常、述語（あなたが行ったように）またはブール値の配列を使用してエンコードされます。Z3_mk_set_sortZ3 C API には、セット式Z3_mk_empty_setを作成するための関数がいくつかありますZ3_mk_set_union。これらは からまでのブール値Tの配列としてのセットを表します。この記事Tで説明されているエンコーディングを使用します。

備考: 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)。

述語に基づくアプローチでは、通常、量指定子を使用する必要があります。あなたの例では、2and3がセットの要素であると言っていますが、他に何も要素ではないと言うには、数量詞が必要です。set は set と の和集合にA等しいなどのプロパティを示す量指定子も必要です。量指定子に基づくアプローチはより柔軟です。たとえば、 と の間のすべての要素を含むセットであると言えます。欠点は、Z3 が処理できる決定可能なフラグメントではない数式を作成するのが非常に簡単であることです。Z3 チュートリアルでは、これらのフラグメントの一部について説明しています。これはチュートリアルの例です。BCA1n

;; 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)
于 2013-04-22T15:27:15.697 に答える