a datatype contains a set in Z3

Question

how can I make a datatype that contains a set of another objects. Basically, I am doing the following code:

(define-sort Set(T) (Array Int T))
(declare-datatypes () ((A f1 (cons (value Int) (b (Set B))))
  (B f2 (cons (id Int) (a  (Set A))))
 ))

But Z3 tells me unknown sort for A and B. If I remove "Set" it works just as the guide states. I was trying to use List instead but it does not work. Anyone knows how to make it work?

Answer 1

You are addressing a question that comes up on a regular basis: how can I mix data-types and arrays (as sets, multi-sets or data-types in the range)?

As stated above Z3 does not support mixing data-types and arrays in a single declaration. A solution is to develop a custom solver for the mixed datatype + array theory. Z3 contains programmatic APIs for developing custom solvers.

It is still useful to develop this example to illustrate the capabilities and limitations of encoding theories with quantifiers and triggers. Let me simplify your example by just using A. As a work-around you can define an auxiliary sort. The workaround is not ideal, though. It illustrates some axiom 'hacking'. It relies on the operational semantics of how quantifiers are instantiated during search.

(set-option :model true) ; We are going to display models.
(set-option :auto-config false)
(set-option :mbqi false) ; Model-based quantifier instantiation is too powerful here


(declare-sort SetA)      ; Declare a custom fresh sort SetA
(declare-datatypes () ((A f1 (cons (value Int) (a SetA)))))

(define-sort Set (T) (Array T Bool))

Then define bijections between (Set A), SetA.

(declare-fun injSA ((Set A)) SetA)
(declare-fun projSA (SetA) (Set A))
(assert (forall ((x SetA)) (= (injSA (projSA x)) x)))
(assert (forall ((x (Set A))) (= (projSA (injSA x)) x)))

This is almost what the data-type declaration states. To enforce well-foundedness you can associate an ordinal with members of A and enforce that members of SetA are smaller in the well-founded ordering:

(declare-const v Int)
(declare-const s1 SetA)
(declare-const a1 A)
(declare-const sa1 (Set A))
(declare-const s2 SetA)
(declare-const a2 A)
(declare-const sa2 (Set A))

With the axioms so far, a1 can be a member of itself.

(push)
(assert (select sa1 a1))
(assert (= s1 (injSA sa1)))
(assert (= a1 (cons v s1)))
(check-sat)
(get-model)
(pop)

We now associate an ordinal number with the members of A.

(declare-fun ord (A) Int)
(assert (forall ((x SetA) (v Int) (a A))
    (=> (select (projSA x) a)
        (> (ord (cons v x)) (ord a)))))
(assert (forall ((x A)) (> (ord x) 0)))

By default quantifier instantiation in Z3 is pattern-based. The first quantified assert above will not be instantiated on all relevant instances. One can instead assert:

(assert (forall ((x1 SetA) (x2 (Set A)) (v Int) (a A))
    (! (=> (and (= (projSA x1) x2) (select x2 a))
        (> (ord (cons v x1)) (ord a)))
       :pattern ((select x2 a) (cons v x1)))))

Axioms like these, that use two patterns (called a multi-pattern) are quite expensive. They produce instantiations for every pair of (select x2 a) and (cons v x1)

The membership constraint from before is now unsatisfiable.

(push)
(assert (select sa1 a1))
(assert (= s1 (injSA sa1)))
(assert (= a1 (cons v s1)))
(check-sat)
(pop)

but models are not necessarily well formed yet. the default value of the set is 'true', which would mean that the model implies there is a membership cycle when there isn't one.

(push)
(assert (not (= (cons v s1) a1)))
(assert (= (projSA s1) sa1))
(assert (select sa1 a1))
(check-sat)
(get-model)
(pop)

We can approximate more faithful models by using the following approach to enforce that sets that are used in data-types are finite. For example, whenever there is a membership check on a set x2, we enforce that the 'default' value of the set is 'false'.

(assert (forall ((x2 (Set A)) (a A))
    (! (not (default x2))
        :pattern ((select x2 a)))))

Alternatively, whenever a set occurs in a data-type constructor it is finite

(assert (forall ((v Int) (x1 SetA))
    (! (not (default (projSA x1)))
        :pattern ((cons v x1)))))


(push)
(assert (not (= (cons v s1) a1)))
(assert (= (projSA s1) sa1))
(assert (select sa1 a1))
(check-sat)
(get-model)
(pop)

Throughout the inclusion of additional axioms, Z3 produces the answer 'unknown' and furthermore the model that is produced indicates that the domain SetA is finite (a singleton). So while we could patch the defaults this model still does not satisfy the axioms. It satisfies the axioms modulo instantiation only.

Answer 2

This is not supported in Z3. You can use arrays in datatype declarations, but they can't contain "references" to the datatypes you are declaring. For example, it is ok to use (Set Int).