Как выразить членство в наборе в формате SMTLIB в Z3?

Я пытаюсь использовать формат SMTLIB для выражения членства в Z3:

(declare-const a (Set Int))

;; the next two lines parse correctly in CVC4, but not Z3:
(assert (= a (as emptyset (Set Int))))
(assert (member 12 a))

;; these work in both solvers
(assert (= a (union a a)))
(assert (subset a a))
(assert (= a (intersection a a)))
(check-sat)

Похоже, что функции emptyset и member анализируются, как и ожидалось, в CVC4, но не в Z3.

Из проверки API (например, здесь: https://z3prover.github.io/api/html/group__capi.html), Z3 поддерживает пустые наборы и членство программно, но как это выразить в синтаксисе SMTLIB?


z3 smt cvc4
person Stefan Ciobaca    schedule 25.11.2020    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Это действительно раздражает, так как z3 и CVC4 используют немного разные обозначения для наборов. В z3 набор — это, по сути, массив с диапазоном bool. Основываясь на этой аналогии, ваша программа закодирована как:

(declare-const a (Set Int))

(assert (= a ((as const (Set Int)) false)))
(assert (select a 12))

(assert (= a (union a a)))
(assert (subset a a))
(assert (= a (intersection a a)))
(check-sat)

который z3 принимает как есть и выдает unsat. Но вы обнаружите, что CVC4 теперь не любит эту программу.

Было бы здорово, если бы движение SMTLib стандартизировало теорию множеств (http://smtlib.cs.uiowa.edu/), и действительно было такое предложение (https://www.kroening.com/smt-lib-lsm.pdf), но я не думаю, что он был принят решателями или санкционирован комитетом SMTLib.

person alias    schedule 25.11.2020