You are addressing a question that arises on a regular basis: how can I mix data types and arrays (in the form of sets, multisets, or data types in a range)?
As stated above, Z3 does not support mixing data types and arrays in the same declaration. The solution is to develop a custom solver for a mixed data type + array theory. Z3 contains software APIs for developing custom solvers.
It is still useful to develop this example to illustrate the possibilities and limitations of coding theories with quantifiers and triggers. Let me simplify your example by simply using A. In the process, you can define helper sorting. A workaround is not ideal. This illustrates some of the axioms of "hacking." It relies on operational semantics as quantifiers are created during a 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 the bijection 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 a data type declaration states. To ensure validity, you can associate a sequence number with members of A and ensure that SetA members are smaller in a reasonable manner:
(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 axioms, a1 can still be a member of itself.
(push) (assert (select sa1 a1)) (assert (= s1 (injSA sa1))) (assert (= a1 (cons v s1))) (check-sat) (get-model) (pop)
Now we compare the sequence 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 vx)) (ord a))))) (assert (forall ((x A)) (> (ord x) 0)))
By default, instantiating a quantifier in Z3 is based on templates. The first quantitative statement above will not be instantiated on all relevant cases. Instead, one could argue:
(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 multi-patterns) are pretty expensive. They create instances for each pair (select x2 a) and (cons v x1)
The limitation of membership from previously became unsatisfactory.
(push) (assert (select sa1 a1)) (assert (= s1 (injSA sa1))) (assert (= a1 (cons v s1))) (check-sat) (pop)
but patterns are not always well formed. the default value for the set is "true", which will mean that the model assumes that there is a membership cycle when it is not.
(push) (assert (not (= (cons v s1) a1))) (assert (= (projSA s1) sa1)) (assert (select sa1 a1)) (check-sat) (get-model) (pop)
We can approximate more accurate models by using the following approach to enforce such sets that are used in data types are finite. For example, whenever there is a membership check on the set x2, we state that the default value for this set is false.
(assert (forall ((x2 (Set A)) (a A)) (! (not (default x2)) :pattern ((select x2 a)))))
Alternatively, whenever a collection occurs in a data type constructor of course
(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)
During the inclusion of additional axioms, Z3 gives the answer "unknown" and, in addition, the model being created indicates that the SetA domain is finite (singleton). Therefore, although we could correct the default values, this model still does not satisfy the axioms. It satisfies axioms only modulo.