Styjun

Let's say I have a simple sum type in Z3 with several constructors of different arities:

(declare-datatypes ()
 ((Foo bar
 (baz (unbaz String))
 (quux (unquux1 String) (unquux2 Int)))))

How can I assert that I know value of type Foo is a quux? I could introduce an existential over quux1 and quux2 but I'm wary of introducing seemingly unnecessary quantifiers. Is there a better way to assert this?

Existentials are rather harmless when assumed because the existentially quantified variables are directly instantiated and thus only entail additional symbols. That is, the second half of the snippet

(declare-datatypes ()
 ((Foo bar
 (baz (unbaz String))
 (quux (unquux1 String) (unquux2 Int)))))

(declare-const f Foo)

(assert (exists ((s String) (i Int)) ;; Let f be a quux
 (= f (quux s i))
))

(assert (= f (baz "test"))) ;; Also let f be a baz
(check-sat) ;; UNSAT - as expected

is equivalent to

...
(declare-const _s String)
(declare-const _i Int)
(assert (= f (quux _s _i))) ;; Let f be a quux

(assert (= f (baz "test"))) ;; Also let f be a baz
(check-sat) ;; UNSAT - as expected

If you're wary of existentials but not of foralls, then you could tag Foo values by axiomatising a mapping from Foo constructors to distinct tags:

(set-option :smt.mbqi false)

(declare-datatypes ()
 ((Foo bar
 (baz (unbaz String))
 (quux (unquux1 String) (unquux2 Int)))))

;; Declare a finite sort Foo_tag with three distinct elements
(declare-datatypes () ((Foo_tag Foo_tag.bar Foo_tag.baz Foo_tag.quux)))

;; Alternatively, three distinct elements from an infinite sort such 
;; as Int can be used. Either by choosing distinct but unspecified 
;; values, as done below, or by directly choosing concrete values,
;; e.g. 1, 2, 3.
; (define-sort Foo_tag () Int)
; (declare-const Foo_tag.bar Foo_tag)
; (declare-const Foo_tag.baz Foo_tag)
; (declare-const Foo_tag.quux Foo_tag)
; (assert (distinct Foo_tag.bar Foo_tag.baz Foo_tag.quux))

;; Tagging function
(declare-fun tag_of (Foo) Foo_tag)

;; Tagging axiom for bar ...
(assert (= (tag_of bar) Foo_tag.bar))

;; ... baz ...
(assert (forall ((s String)) (! 
 (= (tag_of (baz s)) Foo_tag.baz)
 :pattern ((baz s))
)))

;; ... and quux
(assert (forall ((s String) (i Int)) (! 
 (= (tag_of (quux s i)) Foo_tag.quux)
 :pattern ((quux s i))
)))

;; Let's do some testing

(declare-const f Foo)

(assert (= (tag_of f) Foo_tag.quux)) ;; Tag f as a quux

(push)
 (assert (= f bar))
 (check-sat) ;; UNSAT - as expected
(pop)

(push)
 (assert (= f (baz "test")))
 (check-sat) ;; UNSAT - as expected
(pop)