diff --git a/src/Language/Fixpoint/Smt/Theories.hs b/src/Language/Fixpoint/Smt/Theories.hs index 7af19f684..74a4ac144 100644 --- a/src/Language/Fixpoint/Smt/Theories.hs +++ b/src/Language/Fixpoint/Smt/Theories.hs @@ -71,7 +71,8 @@ elt = "Elt" set = "LSet" map = "Map" -emp, sng, add, cup, cap, mem, dif, sub, com, sel, sto, mcup, mdef :: Raw +emp, sng, add, cup, cap, mem, dif, sub, com, sel, sto, mcup, mdef, mprj :: Raw +mToSet, mshift, mmax, mmin :: Raw emp = "smt_set_emp" sng = "smt_set_sng" add = "smt_set_add" @@ -84,10 +85,16 @@ com = "smt_set_com" sel = "smt_map_sel" sto = "smt_map_sto" mcup = "smt_map_cup" +mmax = "smt_map_max" +mmin = "smt_map_min" mdef = "smt_map_def" +mprj = "smt_map_prj" +mshift = "smt_map_shift" +mToSet = "smt_map_to_set" -setEmpty, setEmp, setCap, setSub, setAdd, setMem, setCom, setCup, setDif, setSng :: Symbol +setEmpty, setEmp, setCap, setSub, setAdd, setMem, setCom, setCup :: Symbol +setDif, setSng :: Symbol setEmpty = "Set_empty" setEmp = "Set_emp" setCap = "Set_cap" @@ -99,11 +106,50 @@ setCup = "Set_cup" setDif = "Set_dif" setSng = "Set_sng" -mapSel, mapSto, mapCup, mapDef :: Symbol +mapSel, mapSto, mapCup, mapDef, mapPrj, mapToSet :: Symbol +mapMax, mapMin, mapShift :: Symbol mapSel = "Map_select" mapSto = "Map_store" mapCup = "Map_union" +mapMax = "Map_union_max" +mapMin = "Map_union_min" mapDef = "Map_default" +mapPrj = "Map_project" +mapShift = "Map_shift" -- See [Map key shift] +mapToSet = "Map_to_set" + +-- [Interaction between Map and Set] +-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +-- Function mapToSet: Convert a map to a set. The map's key may be of +-- any type and is preserved as the set's element type. More precisely: +-- mapToSet : Map k Int -> Set k +-- The element type must be Int. All non-positive elements are mapped +-- to False, and all positive elements are mapped to True. In practice, +-- negative elements should not exist because Map is intended to be used +-- as a bag, so the element is a non-negative number representing +-- the occurrences of its corresponding key. +-- +-- Function mapPrj: Project a subset of a map. Type signature: +-- mapPrj : Set k -> Map k Int -> Map k Int +-- If the key is present in both the argument set and the argument map, +-- then the key (along with its associated value in the map) are preserved +-- in the output. Keys not present in the set are mapped to zero. Keys not +-- present in the set are mapped to zero. +-- +-- [Map key shift] +-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +-- Function mapShift: Add an integer to all keys in a map. Type signature: +-- mapShift : Int -> Map Int v -> Map Int v +-- Let's call the first argument (the shift amount) N, the second argument K1, +-- and the result K2. For all indices i, we have K2[i] = K1[i - N]. +-- This is implemented with Z3's lambda, which lets us construct an array +-- from a function. +-- +-- [Map max and min] +-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +-- Functions mapMax and mapMin: Union two maps, combining the elements by +-- taking either the greatest (mapMax) or the least (mapMin) of them. +-- mapMax, mapMin : Map v Int -> Map v Int -> Map v Int strLen, strSubstr, strConcat :: (IsString a) => a -- Symbol strLen = "strLen" @@ -195,6 +241,45 @@ z3Preamble u [("m1", bb map), ("m2", bb map)] (bb map) (key2 (key "_ map" (key2 "+" (parens (bb elt <+> bb elt)) (bb elt))) "m1" "m2") + , bFun mprj -- See [Interaction Between Map and Set] + [("s", bb set), ("m", bb map)] + (bb map) + (key3 + (key "_ map" + (key2 "ite" + (parens ("Bool" <+> bb elt <+> bb elt)) + (bb elt) + ) + ) + "s" + "m" + (parens (key "as const" (key2 "Array" (bb elt) (bb elt)) <+> "0")) + ) + , bFun mToSet -- See [Interaction Between Map and Set] + [("m", bb map)] + (bb set) + (key2 + (key "_ map" + (key2 ">" + (parens (bb elt <+> bb elt)) + "Bool" + ) + ) + "m" + (parens (key "as const" (key2 "Array" (bb elt) (bb elt)) <+> "0")) + ) + , bFun mmax -- See [Map max and min] + [("m1", bb map),("m2", bb map)] + (bb map) + "(lambda ((i Int)) (ite (> (select m1 i) (select m2 i)) (select m1 i) (select m2 i)))" + , bFun mmin -- See [Map max and min] + [("m1", bb map),("m2", bb map)] + (bb map) + "(lambda ((i Int)) (ite (< (select m1 i) (select m2 i)) (select m1 i) (select m2 i)))" + , bFun mshift -- See [Map key shift] + [("n", "Int"),("m", bb map)] + (bb map) + "(lambda ((i Int)) (select m (- i n)))" , bFun mdef [("v", bb elt)] (bb map) @@ -385,7 +470,12 @@ interpSymbols = , interpSym mapSel sel mapSelSort , interpSym mapSto sto mapStoSort , interpSym mapCup mcup mapCupSort + , interpSym mapMax mmax mapMaxSort + , interpSym mapMin mmin mapMinSort , interpSym mapDef mdef mapDefSort + , interpSym mapPrj mprj mapPrjSort + , interpSym mapShift mshift mapShiftSort + , interpSym mapToSet mToSet mapToSetSort , interpSym bvOrName "bvor" bvBopSort , interpSym bvAndName "bvand" bvBopSort , interpSym strLen strLen strLenSort @@ -404,6 +494,15 @@ interpSymbols = mapCupSort = FAbs 0 $ FFunc (mapSort (FVar 0) intSort) $ FFunc (mapSort (FVar 0) intSort) (mapSort (FVar 0) intSort) + mapMaxSort = mapCupSort + mapMinSort = mapCupSort + mapPrjSort = FAbs 0 $ FFunc (setSort (FVar 0)) + $ FFunc (mapSort (FVar 0) intSort) + (mapSort (FVar 0) intSort) + mapShiftSort = FAbs 0 $ FFunc intSort + $ FFunc (mapSort intSort (FVar 0)) + (mapSort intSort (FVar 0)) + mapToSetSort = FAbs 0 $ FFunc (mapSort (FVar 0) intSort) (setSort (FVar 0)) mapStoSort = FAbs 0 $ FAbs 1 $ FFunc (mapSort (FVar 0) (FVar 1)) $ FFunc (FVar 0) $ FFunc (FVar 1) diff --git a/tests/neg/maps02.fq b/tests/neg/maps02.fq new file mode 100644 index 000000000..f99875536 --- /dev/null +++ b/tests/neg/maps02.fq @@ -0,0 +1,9 @@ +bind 1 m1 : {v : Map_t Int Int | v = Map_default 0} +bind 2 s1 : {v : Set_Set Int | v = (Set_cup (Set_sng 10) (Set_sng 30))} +bind 3 m2 : {v : Map_t Int Int | v = (Map_store (Map_store m1 10 1) 20 1) } + +constraint: + env [ 1; 2; 3 ] + lhs {v : Set_Set Int | v = Map_to_set m2 } + rhs {v : Set_Set Int | v = s1 } + id 1 tag [] diff --git a/tests/pos/maps02.fq b/tests/pos/maps02.fq new file mode 100644 index 000000000..e85a32eef --- /dev/null +++ b/tests/pos/maps02.fq @@ -0,0 +1,16 @@ +bind 1 m1 : {v : Map_t Int Int | v = Map_default 0} +bind 2 s1 : {v : Set_Set Int | v = (Set_cup (Set_sng 10) (Set_sng 20))} +bind 3 m2 : {v : Map_t Int Int | v = (Map_store (Map_store m1 10 1) 20 1) } +bind 4 m3 : {v : Map_t Int Int | v = (Map_store (Map_store m1 20 1) 10 1) } + +constraint: + env [ 1; 2; 3 ] + lhs {v : Set_Set Int | v = Map_to_set m2 } + rhs {v : Set_Set Int | v = s1 } + id 1 tag [] + +constraint: + env [ 1; 2; 3; 4 ] + lhs {v : Set_Set Int | v = Map_to_set m3 } + rhs {v : Set_Set Int | v = s1 } + id 2 tag [] diff --git a/tests/pos/maps03.fq b/tests/pos/maps03.fq new file mode 100644 index 000000000..fe91fb9c7 --- /dev/null +++ b/tests/pos/maps03.fq @@ -0,0 +1,10 @@ +bind 1 m1 : {v : Map_t Int Int | v = Map_default 0} +bind 2 m2 : {v : Map_t Int Int | v = (Map_store (Map_store (Map_store m1 30 3) 10 1) 20 2) } +bind 3 s1 : {v : Set_Set Int | v = (Set_cup (Set_sng 30) (Set_sng 20))} +bind 4 m3 : {v : Map_t Int Int | v = (Map_store (Map_store m1 20 2) 30 3) } + +constraint: + env [ 1; 2; 3; 4 ] + lhs {v : Map_t Int Int | v = Map_project s1 m2} + rhs {v : Map_t Int Int | v = m3 } + id 1 tag [] diff --git a/tests/pos/maps04.fq b/tests/pos/maps04.fq new file mode 100644 index 000000000..6a1d4b09d --- /dev/null +++ b/tests/pos/maps04.fq @@ -0,0 +1,39 @@ +bind 1 m1 : {v : Map_t Int Int | v = Map_default 0} +bind 2 m2 : {v : Map_t Int Int | v = (Map_store (Map_store (Map_store m1 30 3) 10 1) 20 2) } +bind 3 m3 : {v : Map_t Int Int | v = (Map_store (Map_store (Map_store m1 10 1) 20 1) 30 1) } + +constraint: + env [ 1; 2; 3 ] + lhs {v : Map_t Int Int | v = Map_union_max m2 m3} + rhs {v : Map_t Int Int | v = m2 } + id 1 tag [] + +constraint: + env [ 1; 2; 3 ] + lhs {v : Map_t Int Int | v = Map_union_max m1 m2} + rhs {v : Map_t Int Int | v = m2 } + id 2 tag [] + +constraint: + env [ 1; 2; 3 ] + lhs {v : Map_t Int Int | v = Map_union_max m1 m3} + rhs {v : Map_t Int Int | v = m3 } + id 3 tag [] + +constraint: + env [ 1; 2; 3 ] + lhs {v : Map_t Int Int | v = Map_union_min m2 m3} + rhs {v : Map_t Int Int | v = m3 } + id 4 tag [] + +constraint: + env [ 1; 2; 3 ] + lhs {v : Map_t Int Int | v = Map_union_min m1 m2} + rhs {v : Map_t Int Int | v = m1 } + id 5 tag [] + +constraint: + env [ 1; 2; 3 ] + lhs {v : Map_t Int Int | v = Map_union_min m1 m3} + rhs {v : Map_t Int Int | v = m1 } + id 6 tag [] diff --git a/tests/pos/maps05.fq b/tests/pos/maps05.fq new file mode 100644 index 000000000..85d8a91ca --- /dev/null +++ b/tests/pos/maps05.fq @@ -0,0 +1,9 @@ +bind 1 m1 : {v : Map_t Int Int | v = Map_default 0} +bind 2 m2 : {v : Map_t Int Int | v = (Map_store (Map_store (Map_store m1 30 3) 10 1) 20 2) } +bind 3 m3 : {v : Map_t Int Int | v = (Map_store (Map_store (Map_store m1 130 3) 110 1) 120 2) } + +constraint: + env [ 1; 2; 3 ] + lhs {v : Map_t Int Int | v = Map_shift 100 m2} + rhs {v : Map_t Int Int | v = m3 } + id 1 tag []