liquid-fixpoint-0.9.6.3.4: src/Language/Fixpoint/Smt/Theories.hs
{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wno-orphans #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE InstanceSigs #-}
module Language.Fixpoint.Smt.Theories
(
-- * Convert theory applications TODO: merge with smt2symbol
smt2App
-- * Convert theory sorts
, sortSmtSort
-- * Convert theory symbols
, smt2Symbol
-- * Preamble to initialize SMT
, preamble
-- * Bit Vector Operations
, sizeBv
-- , toInt
-- * Theory Symbols
, theorySymbols
, dataDeclSymbols
-- * Theories
, setEmpty, setEmp, setSng, setAdd, setMem, setCard
, setCom, setCap, setCup, setDif, setSub
, mapDef, mapSel, mapSto
, bagEmpty, bagSng, bagCount, bagSub, bagCup, bagMax, bagMin
-- * Z3 theory array encodings
, arrConstM, arrStoreM, arrSelectM
, arrConstS, arrStoreS, arrSelectS
, arrMapNotS, arrMapOrS, arrMapAndS, arrMapImpS
, arrConstB, arrStoreB, arrSelectB
, arrMapPlusB, arrMapLeB, arrMapGtB, arrMapIteB
-- * CVC5 finite fields
, ffVal, ffAdd, ffMul
-- * Query Theories
, isSmt2App
, axiomLiterals
, maxLamArg
) where
import Prelude hiding (map)
import Control.Monad.State
import Data.ByteString.Builder (Builder)
import Language.Fixpoint.Types.Sorts
import Language.Fixpoint.Types.Config
import Language.Fixpoint.Types
import Language.Fixpoint.Smt.Types
-- import qualified Data.HashMap.Strict as M
import Data.Maybe (catMaybes)
-- import Data.Text.Format
import qualified Data.Text
import Data.String (IsString(..))
import Text.Printf (printf)
import Language.Fixpoint.Utils.Builder
{- | [NOTE:Adding-Theories] To add new (SMTLIB supported) theories to
liquid-fixpoint and upstream, grep for "Map_default" and then add
your corresponding symbol in all those places.
This is currently far more complicated than it needs to be.
-}
--------------------------------------------------------------------------------
-- | Theory Symbols ------------------------------------------------------------
--------------------------------------------------------------------------------
---- Size changes
bvConcatName, bvExtractName, bvRepeatName, bvZeroExtName, bvSignExtName :: Symbol
bvConcatName = "concat"
bvExtractName = "extract"
bvRepeatName = "repeat"
bvZeroExtName = "zero_extend"
bvSignExtName = "sign_extend"
-- Unary Logic
bvNotName, bvNegName :: Symbol
bvNotName = "bvnot"
bvNegName = "bvneg"
-- Binary Logic
bvAndName, bvNandName, bvOrName, bvNorName, bvXorName, bvXnorName :: Symbol
bvAndName = "bvand"
bvNandName = "bvnand"
bvOrName = "bvor"
bvNorName = "bvnor"
bvXorName = "bvxor"
bvXnorName = "bvxnor"
-- Shifts
bvShlName, bvLShrName, bvAShrName, bvLRotName, bvRRotName :: Symbol
bvShlName = "bvshl"
bvLShrName = "bvlshr"
bvAShrName = "bvashr"
bvLRotName = "rotate_left"
bvRRotName = "rotate_right"
-- Arithmetic
bvAddName, bvSubName, bvMulName, bvUDivName :: Symbol
bvURemName, bvSDivName, bvSRemName, bvSModName :: Symbol
bvAddName = "bvadd"
bvSubName = "bvsub"
bvMulName = "bvmul"
bvUDivName = "bvudiv"
bvURemName = "bvurem"
bvSDivName = "bvsdiv"
bvSRemName = "bvsrem"
bvSModName = "bvsmod"
-- Comparisons
bvCompName, bvULtName, bvULeName, bvUGtName, bvUGeName :: Symbol
bvSLtName, bvSLeName, bvSGtName, bvSGeName :: Symbol
bvCompName = "bvcomp"
bvULtName = "bvult"
bvULeName = "bvule"
bvUGtName = "bvugt"
bvUGeName = "bvuge"
bvSLtName = "bvslt"
bvSLeName = "bvsle"
bvSGtName = "bvsgt"
bvSGeName = "bvsge"
mapDef, mapSel, mapSto :: (IsString a) => a
mapDef = "Map_default"
mapSel = "Map_select"
mapSto = "Map_store"
setCard, setEmpty, setEmp, setCap, setSub, setAdd, setMem, setCom, setCup, setDif, setSng :: (IsString a) => a
setCard = "Set_card"
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"
bagEmpty, bagSng, bagCount, bagSub, bagCup, bagMax, bagMin :: (IsString a) => a
bagEmpty = "Bag_empty"
bagSng = "Bag_sng"
bagCount = "Bag_count"
bagSub = "Bag_sub"
bagCup = "Bag_union"
bagMax = "Bag_union_max" -- See [Bag max and min]
bagMin = "Bag_inter_min"
-- [Bag max and min]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- Functions bagMax and bagMin: Union/intersect two bags, combining the elements by
-- taking either the greatest (bagMax) or the least (bagMin) of them.
-- bagMax, bagMin : Map v Int -> Map v Int -> Map v Int
--- Array operations for polymorphic maps
arrConstM, arrStoreM, arrSelectM :: Symbol
arrConstM = "arr_const_m"
arrStoreM = "arr_store_m"
arrSelectM = "arr_select_m"
--- Array operations for sets (Z3)
arrConstS, arrStoreS, arrSelectS, arrMapNotS, arrMapOrS, arrMapAndS, arrMapImpS :: Symbol
arrConstS = "arr_const_s"
arrStoreS = "arr_store_s"
arrSelectS = "arr_select_s"
arrMapNotS = "arr_map_not"
arrMapOrS = "arr_map_or"
arrMapAndS = "arr_map_and"
arrMapImpS = "arr_map_imp"
--- Array operations for bags (Z3)
arrConstB, arrStoreB, arrSelectB :: Symbol
arrConstB = "arr_const_b"
arrStoreB = "arr_store_b"
arrSelectB = "arr_select_b"
arrMapPlusB, arrMapLeB, arrMapGtB, arrMapIteB :: Symbol
arrMapPlusB = "arr_map_plus"
arrMapLeB = "arr_map_le"
arrMapGtB = "arr_map_gt"
arrMapIteB = "arr_map_ite"
-- Finite field operations
ffVal, ffAdd, ffMul :: (IsString a) => a -- Symbol
ffVal = "FF_val"
ffAdd = "FF_add"
ffMul = "FF_mul"
strLen, strSubstr, strConcat, strConcat', strPrefixOf, strSuffixOf, strContains :: (IsString a) => a -- Symbol
strLen = "strLen"
strSubstr = "subString"
strConcat = "concatString"
strConcat' = "strConcat"
strPrefixOf = "strPrefixOf"
strSuffixOf = "strSuffixOf"
strContains = "strContains"
smtlibStrLen, smtlibStrSubstr, smtlibStrConcat, smtlibStrPrefixOf, smtlibStrSuffixOf, smtlibStrContains :: Raw
smtlibStrLen = "str.len"
smtlibStrSubstr = "str.substr"
smtlibStrConcat = "str.++"
smtlibStrPrefixOf = "str.prefixof"
smtlibStrSuffixOf = "str.suffixof"
smtlibStrContains = "str.contains"
strLenSort, substrSort, concatstrSort, strCompareSort :: Sort
strLenSort = FFunc strSort intSort
substrSort = mkFFunc 0 [strSort, intSort, intSort, strSort]
concatstrSort = mkFFunc 0 [strSort, strSort, strSort]
strCompareSort = mkFFunc 0 [strSort, strSort, boolSort]
string :: Raw
string = strConName
bFun :: Raw -> [(Builder, Builder)] -> Builder -> Builder -> Builder
bFun name xts out body = key "define-fun" (seqs [fromText name, args, out, body])
where
args = parenSeqs [parens (x <+> t) | (x, t) <- xts]
bFun' :: Raw -> [Builder] -> Builder -> Builder
bFun' name ts out = key "declare-fun" (seqs [fromText name, args, out])
where
args = parenSeqs ts
bSort :: Raw -> Builder -> Builder
bSort name def = key "define-sort" (fromText name <+> "()" <+> def)
-- RJ: Am changing this to `Int` not `Real` as (1) we usually want `Int` and
-- (2) have very different semantics. TODO: proper overloading, post genEApp
uifDef :: Config -> Data.Text.Text -> Data.Text.Text -> Builder
uifDef cfg f op
| onlyLinearArith cfg -- linear cfg || Z3 /= solver cfg
= bFun' f ["Int", "Int"] "Int"
| otherwise
= bFun f [("x", "Int"), ("y", "Int")] "Int" (key2 (fromText op) "x" "y")
onlyLinearArith :: Config -> Bool
onlyLinearArith cfg = linear cfg || solver cfg `notElem` [Z3, Z3mem, Cvc5]
preamble :: Config -> SMTSolver -> [Builder]
preamble cfg s = snd <$> filter (matchesCondition s . fst) (solverPreamble cfg)
matchesCondition :: SMTSolver -> PreambleCondition -> Bool
matchesCondition _ SAll = True
matchesCondition s (SOnly ss) = s `elem` ss
solverPreamble :: Config -> [Preamble]
solverPreamble cfg
= [ (SOnly [Z3, Z3mem], "(set-option :auto-config false)")
, (SOnly [Z3, Z3mem], "(set-option :model true)")
, (SOnly [Cvc4], "(set-logic ALL_SUPPORTED)")
, (SOnly [Cvc5], "(set-logic ALL)")
, (SOnly [Cvc4, Cvc5], "(set-option :incremental true)")
]
++ setPreamble cfg
++ boolPreamble cfg
++ arithPreamble cfg
++ stringPreamble cfg
type Preamble = (PreambleCondition, Builder)
data PreambleCondition = SAll | SOnly [SMTSolver]
deriving (Eq, Show)
setPreamble :: Config -> [Preamble]
-- Z3 does not support cardinality on sets, which is defined to be uninterpreted function
setPreamble _
= [ (SOnly [Z3, Z3mem], bFun' "set.card" ["(Array Int Bool)"] "Int") ]
boolPreamble :: Config -> [Preamble]
boolPreamble _
= [ (SAll, bFun boolToIntName [("b", "Bool")] "Int" "(ite b 1 0)") ]
arithPreamble :: Config -> [Preamble]
arithPreamble cfg = (SAll,) <$>
[ uifDef cfg (symbolText mulFuncName) "*"
, uifDef cfg (symbolText divFuncName) "div"
]
stringPreamble :: Config -> [Preamble]
stringPreamble cfg | not (noStringTheory cfg)
= [ (SAll, bSort string "String")
, (SAll, bFun strLen [("s", fromText string)] "Int" (key (fromText smtlibStrLen) "s"))
, (SAll, bFun strSubstr [("s", fromText string), ("i", "Int"), ("j", "Int")] (fromText string) (key (fromText smtlibStrSubstr) "s i j"))
, (SAll, bFun strConcat [("x", fromText string), ("y", fromText string)] (fromText string) (key (fromText smtlibStrConcat) "x y"))
]
stringPreamble _
= [ (SAll, bSort string "Int")
, (SAll, bFun' strLen [fromText string] "Int")
, (SAll, bFun' strSubstr [fromText string, "Int", "Int"] (fromText string))
, (SAll, bFun' strConcat [fromText string, fromText string] (fromText string))
]
--------------------------------------------------------------------------------
-- | Exported API --------------------------------------------------------------
--------------------------------------------------------------------------------
smt2Symbol :: SymEnv -> Symbol -> Maybe Builder
smt2Symbol env x = fromText . tsRaw <$> symEnvTheory x env
instance SMTLIB2 SmtSort where
smt2 s = pure $ smt2SmtSort s
smt2SmtSort :: SmtSort -> Builder
smt2SmtSort SInt = "Int"
smt2SmtSort SReal = "Real"
smt2SmtSort SBool = "Bool"
smt2SmtSort SString = fromText string
smt2SmtSort (SSet a) = key "Set" (smt2SmtSort a)
smt2SmtSort (SBag a) = key "Bag" (smt2SmtSort a)
smt2SmtSort (SArray a b) = key2 "Array" (smt2SmtSort a) (smt2SmtSort b)
smt2SmtSort (SFFld n) = key "_ FiniteField" (bShow n)
smt2SmtSort (SBitVec n) = key "_ BitVec" (bShow n)
smt2SmtSort (SVar n) = "T" <> bShow n
smt2SmtSort (SData c []) = symbolBuilder c
smt2SmtSort (SData c ts) = parenSeqs [symbolBuilder c, smt2SmtSorts ts]
-- smt2SmtSort (SApp ts) = build "({} {})" (symbolBuilder tyAppName, smt2SmtSorts ts)
smt2SmtSorts :: [SmtSort] -> Builder
smt2SmtSorts = seqs . fmap smt2SmtSort
type VarAs = Symbol -> Sort -> SymM Builder
--------------------------------------------------------------------------------
smt2App :: VarAs -> Expr -> [Builder] -> SymM (Maybe Builder)
--------------------------------------------------------------------------------
smt2App _ ex@(dropECst -> EVar f) [d]
| f == arrConstS || f == arrConstB || f == arrConstM =
do env <- get
pure $ Just $ key (key "as const" (getTarget env ex)) d
| f == setEmpty =
do env <- get
pure $ Just $ key "as set.empty" (getTarget env ex)
| f == bagEmpty =
do env <- get
pure $ Just $ key "as bag.empty" (getTarget env ex)
| f == ffVal =
do env <- get
pure $ Just $ key ("as ff" <> d) (getTarget env ex)
where
getTarget :: SymEnv -> Expr -> Builder
-- const is a function, but SMT expects only the output sort
getTarget env (ECst _ t) = smt2SmtSort $ sortSmtSort True (seData env) (ffuncOut t)
getTarget _ e = bShow e
smt2App k ex (builder:builders) =
do a <- smt2AppArg k ex
pure $ (\fb -> key fb (builder <> mconcat [ " " <> d | d <- builders])) <$> a
smt2App _ _ [] = pure Nothing
smt2AppArg :: VarAs -> Expr -> SymM (Maybe Builder)
smt2AppArg k (ECst (dropECst -> EVar f) t)
= do env <- get
case symEnvTheory f env of
Just fThy -> if isPolyCtor fThy t
then Just <$> k f (ffuncOut t)
else pure $ Just $ fromText (tsRaw fThy)
Nothing -> pure Nothing
smt2AppArg _ _
= pure Nothing
isPolyCtor :: TheorySymbol -> Sort -> Bool
isPolyCtor fThy t = isPolyInst (tsSort fThy) t && tsInterp fThy == Ctor
ffuncOut :: Sort -> Sort
ffuncOut t = maybe t (last . snd) (bkFFunc t)
--------------------------------------------------------------------------------
isSmt2App :: SEnv TheorySymbol -> Expr -> Maybe Int
--------------------------------------------------------------------------------
isSmt2App g (dropECst -> EVar f) = lookupSEnv f g >>= thyAppInfo
isSmt2App _ _ = Nothing
thyAppInfo :: TheorySymbol -> Maybe Int
thyAppInfo ti = case tsInterp ti of
Field -> Just 1
_ -> sortAppInfo (tsSort ti)
sortAppInfo :: Sort -> Maybe Int
sortAppInfo t = case bkFFunc t of
Just (_, ts) -> Just (length ts - 1)
Nothing -> Nothing
--------------------------------------------------------------------------------
-- | Theory Symbols : `uninterpSEnv` should be disjoint from see `interpSEnv`
-- to avoid duplicate SMT definitions. `uninterpSEnv` is for uninterpreted
-- symbols, and `interpSEnv` is for interpreted symbols.
--------------------------------------------------------------------------------
instance TheorySymbols SMTSolver where
theorySymbols :: SMTSolver -> SEnv TheorySymbol
theorySymbols = fromListSEnv . interpSymbols
instance TheorySymbols [DataDecl] where
theorySymbols :: [DataDecl] -> SEnv TheorySymbol
theorySymbols = fromListSEnv . concatMap dataDeclSymbols
instance TheorySymbols [Equation] where
theorySymbols = fromListSEnv . fmap equationSymbol
instance TheorySymbols DefinedFuns where
theorySymbols (MkDefinedFuns eqns) = theorySymbols eqns
equationSymbol :: Equation -> (Symbol, TheorySymbol)
equationSymbol eq = (sym, Thy sym (symbolRaw sym) sort Defined)
where
sym = eqName eq
sort = mkFFunc 0 ((snd <$> eqArgs eq) <> [eqSort eq])
--------------------------------------------------------------------------------
interpSymbols :: SMTSolver -> [(Symbol, TheorySymbol)]
--------------------------------------------------------------------------------
interpSymbols cfg =
[
-- maps
interpSym mapDef mapDef mapDefSort
, interpSym mapSel mapSel mapSelSort
, interpSym mapSto mapSto mapStoSort
, interpSym arrConstM "const" (FAbs 0 $ FFunc (FVar 1) mapArrSort)
, interpSym arrSelectM "select" (FAbs 0 $ FFunc mapArrSort $ FFunc (FVar 0) (FVar 1))
, interpSym arrStoreM "store" (FAbs 0 $ FFunc mapArrSort $ FFunc (FVar 0) $ FFunc (FVar 1) mapArrSort)
-- CVC5 sets
, interpSym setCard "set.card" (FAbs 0 $ FFunc (setSort $ FVar 0) intSort)
, interpSym setEmp "set.is_empty" (FAbs 0 $ FFunc (setSort $ FVar 0) boolSort)
, interpSym setEmpty "set.empty" (FAbs 0 $ FFunc intSort (setSort $ FVar 0))
, interpSym setSng "set.singleton" (FAbs 0 $ FFunc (FVar 0) (setSort $ FVar 0))
, interpSym setAdd "set.insert" (FAbs 0 $ FFunc (FVar 0) $ FFunc (setSort $ FVar 0) (setSort $ FVar 0))
, interpSym setMem "set.member" (FAbs 0 $ FFunc (FVar 0) $ FFunc (setSort $ FVar 0) boolSort)
, interpSym setCup "set.union" setBopSort
, interpSym setCap "set.inter" setBopSort
, interpSym setDif "set.minus" setBopSort
, interpSym setSub "set.subset" (FAbs 0 $ FFunc (setSort $ FVar 0) $ FFunc (setSort $ FVar 0) boolSort)
, interpSym setCom "set.complement" (FAbs 0 $ FFunc (setSort $ FVar 0) (setSort $ FVar 0))
-- CVC5 bags
, interpSym bagEmpty "bag.empty" (FAbs 0 $ FFunc intSort (bagSort $ FVar 0))
, interpSym bagSng "bag" (FAbs 0 $ FFunc (FVar 0) $ FFunc intSort (bagSort $ FVar 0))
, interpSym bagCount "bag.count" (FAbs 0 $ FFunc (FVar 0) $ FFunc (bagSort $ FVar 0) intSort)
, interpSym bagCup "bag.union_disjoint" bagBopSort
, interpSym bagMax "bag.union_max" bagBopSort
, interpSym bagMin "bag.inter_min" bagBopSort
, interpSym bagSub "bag.subbag" (FAbs 0 $ FFunc (bagSort $ FVar 0) $ FFunc (bagSort $ FVar 0) boolSort)
-- Strings
, interpSym strLen strLen strLenSort
, interpSym strSubstr strSubstr substrSort
, interpSym strConcat strConcat concatstrSort
, interpSym strConcat' smtlibStrConcat concatstrSort
, interpSym strPrefixOf smtlibStrPrefixOf strCompareSort
, interpSym strSuffixOf smtlibStrSuffixOf strCompareSort
, interpSym strContains smtlibStrContains strCompareSort
, interpSym boolInt boolInt (FFunc boolSort intSort)
-- Function mappings for indexed identifier functions
, interpSym' "_" iiSort
, interpSym "app" "" appSort
, interpSym' bvConcatName bvConcatSort
, interpSym' bvExtractName (FFunc FInt bvExtendSort)
, interpBvExt bvRepeatName
, interpBvExt bvZeroExtName
, interpBvExt bvSignExtName
, interpBvUop bvNotName
, interpBvUop bvNegName
, interpBvBop bvAndName
, interpBvBop bvNandName
, interpBvBop bvOrName
, interpBvBop bvNorName
, interpBvBop bvXorName
, interpBvBop bvXnorName
, interpBvBop bvShlName
, interpBvBop bvLShrName
, interpBvBop bvAShrName
, interpBvRot bvLRotName
, interpBvRot bvRRotName
, interpBvBop bvAddName
, interpBvBop bvSubName
, interpBvBop bvMulName
, interpBvBop bvUDivName
, interpBvBop bvURemName
, interpBvBop bvSDivName
, interpBvBop bvSRemName
, interpBvBop bvSModName
, interpSym' bvCompName bvEqSort
, interpBvCmp bvULtName
, interpBvCmp bvULeName
, interpBvCmp bvUGtName
, interpBvCmp bvUGeName
, interpBvCmp bvSLtName
, interpBvCmp bvSLeName
, interpBvCmp bvSGtName
, interpBvCmp bvSGeName
-- int to bv Conversions
, interpSym intbv32Name "(_ int2bv 32)" (FFunc intSort bv32)
, interpSym intbv64Name "(_ int2bv 64)" (FFunc intSort bv64)
, interpSym bv32intName (bv2i cfg 32) (FFunc bv32 intSort)
, interpSym bv64intName (bv2i cfg 64) (FFunc bv64 intSort)
, interpSym intbv8Name "(_ int2bv 8)" (FFunc intSort bv8)
, interpSym intbv16Name "(_ int2bv 16)" (FFunc intSort bv16)
, interpSym bv8intName (bv2i cfg 32) (FFunc bv8 intSort)
, interpSym bv16intName (bv2i cfg 64) (FFunc bv16 intSort)
]
++
if cfg == Z3 || cfg == Z3mem
then
[
-- Z3 sets (arrays of bools)
interpSym arrConstS "const" (FAbs 0 $ FFunc boolSort setArrSort)
, interpSym arrSelectS "select" (FAbs 0 $ FFunc setArrSort $ FFunc (FVar 0) boolSort)
, interpSym arrStoreS "store" (FAbs 0 $ FFunc setArrSort $ FFunc (FVar 0) $ FFunc boolSort setArrSort)
, interpSym arrMapNotS "(_ map not)" (FAbs 0 $ FFunc setArrSort setArrSort)
, interpSym arrMapOrS "(_ map or)" (FAbs 0 $ FFunc setArrSort $ FFunc setArrSort setArrSort)
, interpSym arrMapAndS "(_ map and)" (FAbs 0 $ FFunc setArrSort $ FFunc setArrSort setArrSort)
, interpSym arrMapImpS "(_ map =>)" (FAbs 0 $ FFunc setArrSort $ FFunc setArrSort setArrSort)
-- Z3 bags (arrays of ints)
, interpSym arrConstB "const" (FAbs 0 $ FFunc intSort bagArrSort)
, interpSym arrSelectB "select" (FAbs 0 $ FFunc bagArrSort $ FFunc (FVar 0) intSort)
, interpSym arrStoreB "store" (FAbs 0 $ FFunc bagArrSort $ FFunc (FVar 0) $ FFunc intSort bagArrSort)
, interpSym arrMapPlusB "(_ map (+ (Int Int) Int))" (FAbs 0 $ FFunc bagArrSort $ FFunc bagArrSort bagArrSort)
, interpSym arrMapLeB "(_ map (<= (Int Int) Bool))" (FAbs 0 $ FFunc bagArrSort $ FFunc bagArrSort setArrSort)
, interpSym arrMapGtB "(_ map (> (Int Int) Bool))" (FAbs 0 $ FFunc bagArrSort $ FFunc bagArrSort setArrSort)
, interpSym arrMapIteB "(_ map (ite (Bool Int Int) Int))" (FAbs 0 $ FFunc setArrSort $ FFunc bagArrSort $ FFunc bagArrSort bagArrSort)
] else if cfg == Cvc5
then
[
-- CVC5 finite fields
interpSym ffVal ffVal (FAbs 0 $ FFunc intSort (finfieldSort (FVar 0)))
, interpSym ffAdd "ff.add" (FAbs 0 $ FFunc (finfieldSort (FVar 0)) $ FFunc (finfieldSort (FVar 0)) (finfieldSort (FVar 0)))
, interpSym ffMul "ff.mul" (FAbs 0 $ FFunc (finfieldSort (FVar 0)) $ FFunc (finfieldSort (FVar 0)) (finfieldSort (FVar 0)))
] else []
where
mapArrSort = arraySort (FVar 0) (FVar 1)
setArrSort = arraySort (FVar 0) boolSort
bagArrSort = arraySort (FVar 0) intSort
bv8 = sizedBitVecSort "Size8"
bv16 = sizedBitVecSort "Size16"
bv32 = sizedBitVecSort "Size32"
bv64 = sizedBitVecSort "Size64"
boolInt = boolToIntName
mapDefSort = FAbs 0 $ FAbs 1 $ FFunc (FVar 1)
(mapSort (FVar 0) (FVar 1))
-- select :: forall k v. Map k v -> k -> v
mapSelSort = FAbs 0 $ FAbs 1 $ FFunc (mapSort (FVar 0) (FVar 1))
$ FFunc (FVar 0) (FVar 1)
-- store :: forall k v. Map k v -> k -> v -> Map k v
mapStoSort = FAbs 0 $ FAbs 1 $ FFunc (mapSort (FVar 0) (FVar 1))
$ FFunc (FVar 0)
$ FFunc (FVar 1)
(mapSort (FVar 0) (FVar 1))
setBopSort = FAbs 0 $ FFunc (setSort $ FVar 0) $ FFunc (setSort $ FVar 0) (setSort $ FVar 0)
bagBopSort = FAbs 0 $ FFunc (bagSort $ FVar 0) $ FFunc (bagSort $ FVar 0) (bagSort $ FVar 0)
bv2i :: SMTSolver -> Int -> Raw
bv2i Cvc4 _ = "bv2nat"
bv2i Cvc5 _ = "bv2nat"
bv2i _ n = Data.Text.pack $ printf "(_ bv2nat %d)" n
interpBvUop :: Symbol -> (Symbol, TheorySymbol)
interpBvUop name = interpSym' name bvUopSort
interpBvBop :: Symbol -> (Symbol, TheorySymbol)
interpBvBop name = interpSym' name bvBopSort
interpBvCmp :: Symbol -> (Symbol, TheorySymbol)
interpBvCmp name = interpSym' name bvCmpSort
interpBvExt :: Symbol -> (Symbol, TheorySymbol)
interpBvExt name = interpSym' name bvExtendSort
interpBvRot :: Symbol -> (Symbol, TheorySymbol)
interpBvRot name = interpSym' name bvRotSort
interpSym' :: Symbol -> Sort -> (Symbol, TheorySymbol)
interpSym' name = interpSym name (Data.Text.pack $ symbolString name)
-- Indexed Identifier sort.
-- Together with 'app', this allows one to write indexed identifier
-- functions (smtlib2 specific functions). (e.g. ((_ sign_extend 1) bv))
--
-- The idea here is that 'app' is elaborated to the empty string,
-- and '_' does the typelit application as it does in smtlib2.
--
-- Then if we write, (app (_ sign_extend 1) bv), LF will elaborate
-- it as ( (_ sign_extend 1) bv). Fitting the smtlib2 format exactly!
--
-- One thing to note, is that any indexed identifier function (like
-- sign_extend) has to have no FAbs in it. Otherwise, they will be
-- elaborated like e.g. ( (_ (as sign_extend Int) 1) bv), which is wrong!
--
-- _ :: forall a b c. (a -> b -> c) -> a -> (b -> c)
iiSort :: Sort
iiSort = FAbs 0 $ FAbs 1 $ FAbs 2 $ FFunc
(FFunc (FVar 0) $ FFunc (FVar 1) (FVar 2))
(FFunc (FVar 0) $ FFunc (FVar 1) (FVar 2))
-- Simple application, used for indexed identifier function, check '_'.
--
-- app :: forall a b. (a -> b) -> a -> b
appSort :: Sort
appSort = FAbs 0 $ FAbs 1 $ FFunc
(FFunc (FVar 0) (FVar 1))
(FFunc (FVar 0) (FVar 1))
-- Indexed identifier operation, purposely didn't place FAbs!
--
-- extend :: Int -> BitVec a -> BitVec b
bvExtendSort :: Sort
bvExtendSort = FFunc FInt $ FFunc (bitVecSort 1) (bitVecSort 2)
-- Indexed identifier operation, purposely didn't place FAbs!
--
-- rot :: Int -> BitVec a -> BitVec a
bvRotSort :: Sort
bvRotSort = FFunc FInt $ FFunc (bitVecSort 0) (bitVecSort 0)
-- uOp :: forall a. BitVec a -> BitVec a
bvUopSort :: Sort
bvUopSort = FAbs 0 $ FFunc (bitVecSort 0) (bitVecSort 0)
-- bOp :: forall a. BitVec a -> BitVec a -> BitVec a
bvBopSort :: Sort
bvBopSort = FAbs 0 $ FFunc (bitVecSort 0) $ FFunc (bitVecSort 0) (bitVecSort 0)
-- bvBopSort = FAbs 0 $ FFunc (bitVecSort (FVar 0)) (FFunc (bitVecSort (FVar 0)) (bitVecSort (FVar 0)))
-- cmp :: forall a. BitVec a -> BitVec a -> Bool
bvCmpSort :: Sort
bvCmpSort = FAbs 0 $ FFunc (bitVecSort 0) $ FFunc (bitVecSort 0) boolSort
-- eq :: forall a. BitVec a -> BitVec a -> BitVec 1
bvEqSort :: Sort
bvEqSort = FAbs 0 $ FFunc (bitVecSort 0) $ FFunc (bitVecSort 0) (sizedBitVecSort "Size1")
-- concat :: forall a b c. BitVec a -> BitVec b -> BitVec c
bvConcatSort :: Sort
bvConcatSort = FAbs 0 $ FAbs 1 $ FAbs 2 $
FFunc (bitVecSort 0) $ FFunc (bitVecSort 1) (bitVecSort 2)
interpSym :: Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym x n t = (x, Thy x n t Theory)
-- This variable is used to generate the lambda names `lam_arg$n` in
-- `Interface.hs` that will be used during defunctionalization in
-- `Defunctionalize.hs`, is a pretty gross hack as if the user types in the
-- program or PLE generates a term that has more than `maxLamArg` lambda binders
-- one inside the other, the SMT will crash complaining that
-- `lam_arg${maxLamArg + k}` was not declared.
maxLamArg :: Int
maxLamArg = 20
axiomLiterals :: Config -> [(Symbol, Sort)] -> [Expr]
axiomLiterals cfg
| noStringTheory cfg = lenAxiomLiterals
| otherwise = strAxiomLiterals
strAxiomLiterals :: [(Symbol, Sort)] -> [Expr]
strAxiomLiterals lts = catMaybes [ strAxiom l | (l, t) <- lts, isString t ]
where
strAxiom l = do
sym <- unLitSymbol l
pure (EEq (expr l) (ECon $ L (symbolText sym) strSort))
lenAxiomLiterals :: [(Symbol, Sort)] -> [Expr]
lenAxiomLiterals lts = catMaybes [ lenAxiom l <$> litLen l | (l, t) <- lts, isString t ]
where
lenAxiom l n = EEq (EApp (expr (strLen :: Symbol)) (expr l)) (expr n `ECst` intSort)
litLen = fmap (Data.Text.length . symbolText) . unLitSymbol
--------------------------------------------------------------------------------
-- | Constructors, Selectors and Tests from 'DataDecl'arations.
--------------------------------------------------------------------------------
dataDeclSymbols :: DataDecl -> [(Symbol, TheorySymbol)]
dataDeclSymbols d = ctorSymbols d ++ testSymbols d ++ selectSymbols d
-- | 'selfSort d' returns the _self-sort_ of 'd' :: 'DataDecl'.
-- See [NOTE:DataDecl] for details.
selfSort :: DataDecl -> Sort
selfSort (DDecl c n _) = fAppTC c (FVar <$> [0..(n-1)])
-- | 'fldSort d t' returns the _real-sort_ of 'd' if 't' is the _self-sort_
-- and otherwise returns 't'. See [NOTE:DataDecl] for details.
fldSort :: DataDecl -> Sort -> Sort
fldSort d (FTC c)
| c == ddTyCon d = selfSort d
fldSort _ s = s
--------------------------------------------------------------------------------
ctorSymbols :: DataDecl -> [(Symbol, TheorySymbol)]
--------------------------------------------------------------------------------
ctorSymbols d = ctorSort d <$> ddCtors d
ctorSort :: DataDecl -> DataCtor -> (Symbol, TheorySymbol)
ctorSort d ctor = (x, Thy x (symbolRaw x) t Ctor)
where
x = symbol ctor
t = mkFFunc n (ts ++ [selfSort d])
n = ddVars d
ts = fldSort d . dfSort <$> dcFields ctor
--------------------------------------------------------------------------------
testSymbols :: DataDecl -> [(Symbol, TheorySymbol)]
--------------------------------------------------------------------------------
testSymbols d = testTheory t . symbol <$> ddCtors d
where
t = mkFFunc (ddVars d) [selfSort d, boolSort]
testTheory :: Sort -> Symbol -> (Symbol, TheorySymbol)
testTheory t x = (sx, Thy sx raw t Test)
where
sx = testSymbol x
raw = "is-" <> symbolRaw x
symbolRaw :: Symbol -> Data.Text.Text
symbolRaw = symbolSafeText
--------------------------------------------------------------------------------
selectSymbols :: DataDecl -> [(Symbol, TheorySymbol)]
--------------------------------------------------------------------------------
selectSymbols d = theorify <$> concatMap (ctorSelectors d) (ddCtors d)
-- | 'theorify' converts the 'Sort' into a full 'TheorySymbol'
theorify :: (Symbol, Sort) -> (Symbol, TheorySymbol)
theorify (x, t) = (x, Thy x (symbolRaw x) t Field)
ctorSelectors :: DataDecl -> DataCtor -> [(Symbol, Sort)]
ctorSelectors d ctor = fieldSelector d <$> dcFields ctor
fieldSelector :: DataDecl -> DataField -> (Symbol, Sort)
fieldSelector d f = (symbol f, mkFFunc n [selfSort d, ft])
where
ft = fldSort d $ dfSort f
n = ddVars d
{- | [NOTE:DataDecl] This note explains the set of symbols generated
for the below data-declaration:
data Vec 1 = [
| nil { }
| cons { vHead : @(0), vTail : Vec}
]
We call 'Vec' the _self-sort_ of the data-type, and we want to ensure that
in all constructors, tests and selectors, the _self-sort_ is replaced with
the actual sort, namely, 'Vec @(0)'.
Constructors // ctor : (fld-sorts) => me
nil : func(1, [Vec @(0)])
cons : func(1, [@(0); Vec @(0); Vec @(0)])
Tests // is#ctor : (me) => bool
is#nil : func(1, [Vec @(0); bool])
is#cons : func(1, [Vec @(0); bool])
Selectors // fld : (me) => fld-sort
vHead : func(1, [Vec @(0); @(0)])
vTail : func(1, [Vec @(0); Vec @(0)])
-}