I previously used Z3's API to define an enumerated type like so
let T = ctx.MkEnumSort("T", [| "a"; "b"; "c"|])
which enumerates the elements of a type T as being "a" "b" and "c" (and nothing else). However I am now trying to do something similar but via SMT-LIB rather than the API and I am running into a problem of Z3 complaining about quantifiers. The program I am using (Boogie) generates the following smt
...
(declare-sort T@T 0)
(declare-fun a() T@T)
(declare-fun b() T@T)
(declare-fun c() T@T)
(assert (forall ((x T@T) )
(! (or
(= x a)
(= x b)
(= x c)
)
:qid |gen.28:15|
:skolemid |1|
)))
...
The assertion is the type closure axiom that asserts that the type has no other members. But when I send this (along with other stuff) to Z3, after thinking about it a bit, returns
WARNING: relevacy must be enabled to use option CASE_SPLIT=3, 4 or 5
unknown
(:reason-unknown (incomplete quantifiers))
Notes: 1. I have MBQI turned on. 2. Boogie has an option called "z3types" but it doesn't seem to make any difference
What is the SMT-LIB equivalent of the MkEnumSort API call?
thanks
P.S. I have tried with RELEVANCY set to both 1 and 2 and I still get the warning about relevancy (CASE_SPLIT is set to 3)
Use
(declare-datatypes () ((T@T (a) (b) (c)))
There is a tutorial with more details: https://microsoft.github.io/z3guide/docs/theories/Datatypes#scalars-enumeration-types