Say I make a datatype A in z3:
(declare-datatypes () ((A (b (bx Int)) (c (cx Int)))))
Now, I can declare a variable t, and then, say, assert that t is a c type:
(declare-fun t () A)
(assert (exists ((x Int)) (= t (c x))))
However, this requires an existential quantifier. My question is: is it possible to do this without a quantifier?
Specifically, I'd like an expression, like is_c t or something, which is equivalent to (exists ((x Int)) (= t (c x))).
I had expected this to be straightforward, since in most functional programming languages with sum types, there's an elimination form for them, usually pattern matching, like match t of b x => false; c x => true. But I haven't been able to find anything of this nature in the z3 documentation. Is there something I'm missing?
You automatically get a tester, as an indexed identifier: (_ is c) for each constructor c.
See Section 4.2.3 of http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf. The relevant part is on page 61 (the second paragraph):
On successfully executing this command, for each constructor c in a declared datatype δ, the solver will also automatically declare a tester with rank δ Bool. The tester’s name is an indexed identifier (see Section 3.3) of the form (_ is c).