module Language.Fixpoint.Smt.Theories
(
smt2App
, smt2Sort
, smt2Symbol
, preamble
, isBv, sizeBv
, isTheorySymbol
, theoryEnv
, theorySymbols
, setEmpty, setEmp, setCap, setSub, setAdd, setMem
, setCom, setCup, setDif, setSng, mapSel, mapSto
) where
import Prelude hiding (map)
import Language.Fixpoint.Types.Config
import Language.Fixpoint.Types
import Language.Fixpoint.Smt.Types
import qualified Data.HashMap.Strict as M
import qualified Data.Text as T
import Data.Text.Format hiding (format)
elt, set, map :: Raw
elt = "Elt"
set = "Set"
map = "Map"
emp, add, cup, cap, mem, dif, sub, com, sel, sto :: Raw
emp = "smt_set_emp"
add = "smt_set_add"
cup = "smt_set_cup"
cap = "smt_set_cap"
mem = "smt_set_mem"
dif = "smt_set_dif"
sub = "smt_set_sub"
com = "smt_set_com"
sel = "smt_map_sel"
sto = "smt_map_sto"
setEmpty, setEmp, setCap, setSub, setAdd, setMem, setCom, setCup, setDif, setSng, mapSel, mapSto :: Symbol
setEmpty = "Set_empty"
setEmp = "Set_emp"
setCap = "Set_cap"
setSub = "Set_sub"
setAdd = "Set_add"
setMem = "Set_mem"
setCom = "Set_com"
setCup = "Set_cup"
setDif = "Set_dif"
setSng = "Set_sng"
mapSel = "Map_select"
mapSto = "Map_store"
z3Preamble :: Bool -> [T.Text]
z3Preamble u
= [ format "(define-sort {} () Int)"
(Only elt)
, format "(define-sort {} () (Array {} Bool))"
(set, elt)
, format "(define-fun {} () {} ((as const {}) false))"
(emp, set, set)
, format "(define-fun {} ((x {}) (s {})) Bool (select s x))"
(mem, elt, set)
, format "(define-fun {} ((s {}) (x {})) {} (store s x true))"
(add, set, elt, set)
, format "(define-fun {} ((s1 {}) (s2 {})) {} ((_ map or) s1 s2))"
(cup, set, set, set)
, format "(define-fun {} ((s1 {}) (s2 {})) {} ((_ map and) s1 s2))"
(cap, set, set, set)
, format "(define-fun {} ((s {})) {} ((_ map not) s))"
(com, set, set)
, format "(define-fun {} ((s1 {}) (s2 {})) {} ({} s1 ({} s2)))"
(dif, set, set, set, cap, com)
, format "(define-fun {} ((s1 {}) (s2 {})) Bool (= {} ({} s1 s2)))"
(sub, set, set, emp, dif)
, format "(define-sort {} () (Array {} {}))"
(map, elt, elt)
, format "(define-fun {} ((m {}) (k {})) {} (select m k))"
(sel, map, elt, elt)
, format "(define-fun {} ((m {}) (k {}) (v {})) {} (store m k v))"
(sto, map, elt, elt, map)
, uifDef u (symbolText mulFuncName) ("*"::T.Text)
, uifDef u (symbolText divFuncName) ("div"::T.Text)
]
uifDef u f op | u = format "(declare-fun {} (Int Int) Int)" (Only f)
| otherwise = format "(define-fun {} ((x Int) (y Int)) Int ({} x y))" (f, op)
cvc4Preamble :: Bool -> [T.Text]
cvc4Preamble _
= [ "(set-logic ALL_SUPPORTED)"
, format "(define-sort {} () Int)" (Only elt)
, format "(define-sort {} () Int)" (Only set)
, format "(declare-fun {} () {})" (emp, set)
, format "(declare-fun {} ({} {}) {})" (add, set, elt, set)
, format "(declare-fun {} ({} {}) {})" (cup, set, set, set)
, format "(declare-fun {} ({} {}) {})" (cap, set, set, set)
, format "(declare-fun {} ({} {}) {})" (dif, set, set, set)
, format "(declare-fun {} ({} {}) Bool)" (sub, set, set)
, format "(declare-fun {} ({} {}) Bool)" (mem, elt, set)
, format "(define-sort {} () (Array {} {}))"
(map, elt, elt)
, format "(define-fun {} ((m {}) (k {})) {} (select m k))"
(sel, map, elt, elt)
, format "(define-fun {} ((m {}) (k {}) (v {})) {} (store m k v))"
(sto, map, elt, elt, map)
]
smtlibPreamble :: Bool -> [T.Text]
smtlibPreamble _
= [
format "(define-sort {} () Int)" (Only elt)
, format "(define-sort {} () Int)" (Only set)
, format "(declare-fun {} () {})" (emp, set)
, format "(declare-fun {} ({} {}) {})" (add, set, elt, set)
, format "(declare-fun {} ({} {}) {})" (cup, set, set, set)
, format "(declare-fun {} ({} {}) {})" (cap, set, set, set)
, format "(declare-fun {} ({} {}) {})" (dif, set, set, set)
, format "(declare-fun {} ({} {}) Bool)" (sub, set, set)
, format "(declare-fun {} ({} {}) Bool)" (mem, elt, set)
, format "(define-sort {} () Int)" (Only map)
, format "(declare-fun {} ({} {}) {})" (sel, map, elt, elt)
, format "(declare-fun {} ({} {} {}) {})" (sto, map, elt, elt, map)
]
isTheorySymbol :: Symbol -> Bool
isTheorySymbol x = M.member x theorySymbols
theoryEnv = M.map tsSort theorySymbols
theorySymbols :: M.HashMap Symbol TheorySymbol
theorySymbols = M.fromList
[ tSym setEmp emp (FAbs 0 $ FFunc (setSort $ FVar 0) boolSort)
, tSym setEmpty emp (FAbs 0 $ FFunc intSort (setSort $ FVar 0))
, tSym setAdd add setbopSort
, tSym setCup cup setbopSort
, tSym setCap cap setbopSort
, tSym setMem mem setmemSort
, tSym setDif dif setbopSort
, tSym setSub sub setcmpSort
, tSym setCom com setcmpSort
, tSym mapSel sel mapselSort
, tSym mapSto sto mapstoSort
, tSym bvOrName "bvor" bvbopSort
, tSym bvAndName "bvand" bvbopSort
]
where
setbopSort = FAbs 0 $ FFunc (setSort $ FVar 0) $ FFunc (setSort $ FVar 0) (setSort $ FVar 0)
setmemSort = FAbs 0 $ FFunc (FVar 0) $ FFunc (setSort $ FVar 0) boolSort
setcmpSort = FAbs 0 $ FFunc (setSort $ FVar 0) $ FFunc (setSort $ FVar 0) boolSort
mapselSort = FAbs 0 $ FAbs 1 $ FFunc (mapSort (FVar 0) (FVar 1)) $ FFunc (FVar 0) (FVar 0)
mapstoSort = FAbs 0 $ FAbs 1 $ FFunc (mapSort (FVar 0) (FVar 1))
$ FFunc (FVar 0)
$ FFunc (FVar 1)
(mapSort (FVar 0) (FVar 1))
bvbopSort = FFunc bitVecSort $ FFunc bitVecSort bitVecSort
tSym :: Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
tSym x n t = (x, Thy x n t)
isBv :: FTycon -> Bool
isBv = (bitVecName ==) . val . fTyconSymbol
sizeBv :: FTycon -> Maybe Int
sizeBv tc
| s == size32Name = Just 32
| s == size64Name = Just 64
| otherwise = Nothing
where
s = val $ fTyconSymbol tc
smt2Symbol :: Symbol -> Maybe T.Text
smt2Symbol x = tsRaw <$> M.lookup x theorySymbols
smt2Sort :: Sort -> Maybe T.Text
smt2Sort (FApp (FTC c) _)
| fTyconSymbol c == "Set_Set" = Just $ format "{}" (Only set)
smt2Sort (FApp (FApp (FTC c) _) _)
| fTyconSymbol c == "Map_t" = Just $ format "{}" (Only map)
smt2Sort (FApp (FTC bv) (FTC s))
| isBv bv
, Just n <- sizeBv s = Just $ format "(_ BitVec {})" (Only n)
smt2Sort _ = Nothing
smt2App :: Expr -> [T.Text] -> Maybe T.Text
smt2App (EVar f) [d]
| f == setEmpty = Just $ format "{}" (Only emp)
| f == setEmp = Just $ format "(= {} {})" (emp, d)
| f == setSng = Just $ format "({} {} {})" (add, emp, d)
smt2App (EVar f) ds
| Just s <- M.lookup f theorySymbols
= Just $ format "({} {})" (tsRaw s, T.intercalate " " ds)
smt2App _ _ = Nothing
preamble :: Bool -> SMTSolver -> [T.Text]
preamble u Z3 = z3Preamble u
preamble u Cvc4 = cvc4Preamble u
preamble u _ = smtlibPreamble u