Skip to content

Add MapMerge construct

Viktor Kuncak requested to merge add-map-merge into master

Created by: gsps

This PR adds a new tree MapMerge(mask, map1, map2) which takes a set mask : Set[K] and two maps map1, map2 : Map[K, V]. It produces a map combining map1 and map2, picking values from map1 whenever k elemOf mask.

This is encoded efficiently in the extended array theory of Z3. For other solvers we encode MapMerge(mask, map1, map2) as Choose(m:Map[K,V] => forall x:K. m(k) = if (mask(k)) map1(k) else map2(k)). In practice, CVC4 and Princess seem to simply return Unknown in the presence of MapMerge.

I added a few (very basic) tests for nativez3, unrollz3 and smt-z3.

Merge request reports