Encoding partial maps in Z3

Question

I wanted to encode partial maps in Z3, with support for asking whether the map is defined for a certain key.

It should also support the operation (update_map m1 m2), which updates m1 with the mappings in m2 such that the mappings of m2 override those of m1.

I tried to encode it using arrays, and a custom option datatype, and I axiomatically specified the update_map function. However, it seems that Z3 can not even deal with my specification of update_map: It returns unknown on the following code:

(declare-datatypes (T) ((option None (Some (option-value T)))))
(define-sort map (K V) (Array K (option V)))

(declare-sort V)
(declare-sort K)

(define-const empty_map (map K V)
  ((as const (Array K (option V))) None))

(define-fun get ((m (map K V)) (k K)) (option V)
  (select m k))

(define-fun put ((m (map K V)) (k K) (v V)) (map K V)
  (store m k (Some v)))

(declare-fun update_map ((map K V) (map K V)) (map K V))

(assert (forall ((m1 (map K V)) (m2 (map K V)) (k K))
    (=> (= (get m2 k) None)
        (= (get (update_map m1 m2) k) (get m1 k)))))
(assert (forall ((m1 (map K V)) (m2 (map K V)) (k K) (v V))
    (=> (= (get m2 k) (Some v))
        (= (get (update_map m1 m2) k) (Some v)))))

(check-sat)

So I have two questions:

1. Is there a better way to encode maps which would enable me to prove facts about update_map?
2. Can anyone share some intuition on why Z3 doesn't understand this specification? As in, what's the "core feature" making this hard for Z3? [I already know that quantifiers are considered hard and that first-order logic is undecidable, I'm looking for something more specific ;-)]

Answer 1

Z3 fails to prove satisfiability, i.e. it fails to construct a model for your formula. I unfortunately don't know a more precise reason for this — might be a limitation of Z3's model finding abilities for arrays, quantifiers, or the combination therefore.

If you are ultimately not interested in finding models, but rather counterexamples (unsat cores), then add on an unsatisfiable formula and try to get unsat instead. I.e. try something such as the following (disclaimer: I didn't actually try it, but I am sure you get the idea):

(assert (not
  (=
    (get
      (update_map
        (put empty_map 2 -2)
        (put empty_map 1 -1))
      -1))))

As an alternative to axiomatising maps on top of arrays, have a look at Dafny's map axiomatisation. The axioms are provided in the Boogie language, but a translation to Z3 is typically straight-forward.