CODEWITHSUNDEEP
syntaxpattern-matchingz3smt
vijrox
vijrox

Reputation: 1156

Z3 pattern matching syntax

I'm trying to use pattern matching in z3 to work with algebraic datatypes. I'm exactly following the syntax given in the SMTLib standard on page 27, but z3 is giving me a syntax error. For example in the following program:

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

it gives me the error "line 4 column 7: variable symbol expected". As far as I can tell I'm following the specified syntax exactly. How do I fix this?

Upvotes: 0

Views: 583

Answers (1)

alias
alias

Reputation: 30448

I don't think you're doing anything wrong! Looks like this is a z3 bug that you should report at https://github.com/Z3Prover/z3/issues/

There's one little problem with your assert statement right before (check-sat). It should read:

(assert (= (foo a) 1))

i.e., without any parenthesis around 1. But your use of the match command is syntactically correct and should be reported as a z3 bug.

Upvotes: 1

Related Questions