Установить членские отношения в z3
Я хотел определить отношение членства в Z3 с API C ++. Я думал сделать это следующим образом:
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. Кто-нибудь знает лучший?
Решение
В Z3 наборы обычно кодируются с использованием предикатов (как вы это сделали) или массивов логических значений. В API Z3 C есть несколько функций для создания выражений множеств: 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),
В подходе, основанном на предикатах, мы обычно должны использовать квантификаторы.
В своем примере вы говорите, что 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)
Другие решения
Других решений пока нет …