Синтаксис соответствия шаблону Z3

Question

Я пытаюсь использовать сопоставление с образцом в z3 для работы с алгебраическими типами данных.Я точно следую синтаксису, указанному в стандарте SMTLib на стр. 27, но z3 дает мне синтаксическую ошибку.Например, в следующей программе:

(declare-datatype Dyn ((a) (b)))
(define-fun foo ((x Dyn)) Int (
  match x (
    (a 1)
    (b 2)
  )
))
(assert (= (foo a) (1)))
(check-sat)

выдает ошибку «строка 4, столбец 7: ожидается переменный символ».Насколько я могу судить, я точно следую указанному синтаксису.Как мне это исправить?

Answer 1

Я не думаю, что вы делаете что-то не так!Похоже, что это ошибка z3, о которой вы должны сообщить https://github.com/Z3Prover/z3/issues/

Есть одна маленькая проблема с вашим оператором assert прямо перед (check-sat).Он должен читать:

(assert (= (foo a) 1))

т.е. без скобок вокруг 1.Но вы используете команду match синтаксически правильно и должны быть зарегистрированы как ошибка z3.