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 C API 中，有几个函数用于创建集合表达式：Z3_mk_set_sort, 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是集合的元素，但是要说没有其他元素是元素，我们需要一个量词。我们还需要量词来表示属性，例如：集合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)
于 2013-04-22T15:27:15.697 回答