{-# 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)])

-}