{-# 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 :: Symbol
bvConcatName   = Symbol
"concat"
bvExtractName :: Symbol
bvExtractName  = Symbol
"extract"
bvRepeatName :: Symbol
bvRepeatName   = Symbol
"repeat"
bvZeroExtName :: Symbol
bvZeroExtName  = Symbol
"zero_extend"
bvSignExtName :: Symbol
bvSignExtName  = Symbol
"sign_extend"

-- Unary Logic
bvNotName, bvNegName :: Symbol
bvNotName :: Symbol
bvNotName = Symbol
"bvnot"
bvNegName :: Symbol
bvNegName = Symbol
"bvneg"

-- Binary Logic
bvAndName, bvNandName, bvOrName, bvNorName, bvXorName, bvXnorName :: Symbol
bvAndName :: Symbol
bvAndName  = Symbol
"bvand"
bvNandName :: Symbol
bvNandName = Symbol
"bvnand"
bvOrName :: Symbol
bvOrName   = Symbol
"bvor"
bvNorName :: Symbol
bvNorName  = Symbol
"bvnor"
bvXorName :: Symbol
bvXorName  = Symbol
"bvxor"
bvXnorName :: Symbol
bvXnorName = Symbol
"bvxnor"

-- Shifts
bvShlName, bvLShrName, bvAShrName, bvLRotName, bvRRotName :: Symbol
bvShlName :: Symbol
bvShlName  = Symbol
"bvshl"
bvLShrName :: Symbol
bvLShrName = Symbol
"bvlshr"
bvAShrName :: Symbol
bvAShrName = Symbol
"bvashr"
bvLRotName :: Symbol
bvLRotName = Symbol
"rotate_left"
bvRRotName :: Symbol
bvRRotName = Symbol
"rotate_right"

-- Arithmetic
bvAddName, bvSubName, bvMulName, bvUDivName :: Symbol
bvURemName, bvSDivName, bvSRemName, bvSModName :: Symbol
bvAddName :: Symbol
bvAddName  = Symbol
"bvadd"
bvSubName :: Symbol
bvSubName  = Symbol
"bvsub"
bvMulName :: Symbol
bvMulName  = Symbol
"bvmul"
bvUDivName :: Symbol
bvUDivName = Symbol
"bvudiv"
bvURemName :: Symbol
bvURemName = Symbol
"bvurem"
bvSDivName :: Symbol
bvSDivName = Symbol
"bvsdiv"
bvSRemName :: Symbol
bvSRemName = Symbol
"bvsrem"
bvSModName :: Symbol
bvSModName = Symbol
"bvsmod"

-- Comparisons
bvCompName, bvULtName, bvULeName, bvUGtName, bvUGeName :: Symbol
bvSLtName, bvSLeName, bvSGtName, bvSGeName :: Symbol
bvCompName :: Symbol
bvCompName = Symbol
"bvcomp"
bvULtName :: Symbol
bvULtName  = Symbol
"bvult"
bvULeName :: Symbol
bvULeName  = Symbol
"bvule"
bvUGtName :: Symbol
bvUGtName  = Symbol
"bvugt"
bvUGeName :: Symbol
bvUGeName  = Symbol
"bvuge"
bvSLtName :: Symbol
bvSLtName  = Symbol
"bvslt"
bvSLeName :: Symbol
bvSLeName  = Symbol
"bvsle"
bvSGtName :: Symbol
bvSGtName  = Symbol
"bvsgt"
bvSGeName :: Symbol
bvSGeName  = Symbol
"bvsge"

mapDef, mapSel, mapSto :: (IsString a) => a
mapDef :: forall a. IsString a => a
mapDef   = a
"Map_default"
mapSel :: forall a. IsString a => a
mapSel   = a
"Map_select"
mapSto :: forall a. IsString a => a
mapSto   = a
"Map_store"

setCard, setEmpty, setEmp, setCap, setSub, setAdd, setMem, setCom, setCup, setDif, setSng :: (IsString a) => a
setCard :: forall a. IsString a => a
setCard  = a
"Set_card"
setEmpty :: forall a. IsString a => a
setEmpty = a
"Set_empty"
setEmp :: forall a. IsString a => a
setEmp   = a
"Set_emp"
setCap :: forall a. IsString a => a
setCap   = a
"Set_cap"
setSub :: forall a. IsString a => a
setSub   = a
"Set_sub"
setAdd :: forall a. IsString a => a
setAdd   = a
"Set_add"
setMem :: forall a. IsString a => a
setMem   = a
"Set_mem"
setCom :: forall a. IsString a => a
setCom   = a
"Set_com"
setCup :: forall a. IsString a => a
setCup   = a
"Set_cup"
setDif :: forall a. IsString a => a
setDif   = a
"Set_dif"
setSng :: forall a. IsString a => a
setSng   = a
"Set_sng"

bagEmpty, bagSng, bagCount, bagSub, bagCup, bagMax, bagMin :: (IsString a) => a
bagEmpty :: forall a. IsString a => a
bagEmpty = a
"Bag_empty"
bagSng :: forall a. IsString a => a
bagSng   = a
"Bag_sng"
bagCount :: forall a. IsString a => a
bagCount = a
"Bag_count"
bagSub :: forall a. IsString a => a
bagSub   = a
"Bag_sub"
bagCup :: forall a. IsString a => a
bagCup   = a
"Bag_union"
bagMax :: forall a. IsString a => a
bagMax   = a
"Bag_union_max" -- See [Bag max and min]
bagMin :: forall a. IsString a => a
bagMin   = a
"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 :: Symbol
arrConstM  = Symbol
"arr_const_m"
arrStoreM :: Symbol
arrStoreM  = Symbol
"arr_store_m"
arrSelectM :: Symbol
arrSelectM = Symbol
"arr_select_m"

--- Array operations for sets (Z3)
arrConstS, arrStoreS, arrSelectS, arrMapNotS, arrMapOrS, arrMapAndS, arrMapImpS :: Symbol
arrConstS :: Symbol
arrConstS  = Symbol
"arr_const_s"
arrStoreS :: Symbol
arrStoreS  = Symbol
"arr_store_s"
arrSelectS :: Symbol
arrSelectS = Symbol
"arr_select_s"

arrMapNotS :: Symbol
arrMapNotS = Symbol
"arr_map_not"
arrMapOrS :: Symbol
arrMapOrS  = Symbol
"arr_map_or"
arrMapAndS :: Symbol
arrMapAndS = Symbol
"arr_map_and"
arrMapImpS :: Symbol
arrMapImpS = Symbol
"arr_map_imp"

--- Array operations for bags (Z3)
arrConstB, arrStoreB, arrSelectB :: Symbol
arrConstB :: Symbol
arrConstB  = Symbol
"arr_const_b"
arrStoreB :: Symbol
arrStoreB  = Symbol
"arr_store_b"
arrSelectB :: Symbol
arrSelectB = Symbol
"arr_select_b"

arrMapPlusB, arrMapLeB, arrMapGtB, arrMapIteB :: Symbol
arrMapPlusB :: Symbol
arrMapPlusB = Symbol
"arr_map_plus"
arrMapLeB :: Symbol
arrMapLeB   = Symbol
"arr_map_le"
arrMapGtB :: Symbol
arrMapGtB   = Symbol
"arr_map_gt"
arrMapIteB :: Symbol
arrMapIteB   = Symbol
"arr_map_ite"

-- Finite field operations
ffVal, ffAdd, ffMul :: (IsString a) => a -- Symbol
ffVal :: forall a. IsString a => a
ffVal = a
"FF_val"
ffAdd :: forall a. IsString a => a
ffAdd = a
"FF_add"
ffMul :: forall a. IsString a => a
ffMul = a
"FF_mul"

strLen, strSubstr, strConcat, strConcat', strPrefixOf, strSuffixOf, strContains :: (IsString a) => a -- Symbol
strLen :: forall a. IsString a => a
strLen    = a
"strLen"
strSubstr :: forall a. IsString a => a
strSubstr = a
"subString"
strConcat :: forall a. IsString a => a
strConcat = a
"concatString"
strConcat' :: forall a. IsString a => a
strConcat' = a
"strConcat"
strPrefixOf :: forall a. IsString a => a
strPrefixOf  = a
"strPrefixOf"
strSuffixOf :: forall a. IsString a => a
strSuffixOf = a
"strSuffixOf"
strContains :: forall a. IsString a => a
strContains = a
"strContains"

smtlibStrLen, smtlibStrSubstr, smtlibStrConcat, smtlibStrPrefixOf, smtlibStrSuffixOf, smtlibStrContains :: Raw
smtlibStrLen :: Raw
smtlibStrLen    = Raw
"str.len"
smtlibStrSubstr :: Raw
smtlibStrSubstr = Raw
"str.substr"
smtlibStrConcat :: Raw
smtlibStrConcat = Raw
"str.++"
smtlibStrPrefixOf :: Raw
smtlibStrPrefixOf = Raw
"str.prefixof"
smtlibStrSuffixOf :: Raw
smtlibStrSuffixOf = Raw
"str.suffixof"
smtlibStrContains :: Raw
smtlibStrContains = Raw
"str.contains"

strLenSort, substrSort, concatstrSort, strCompareSort :: Sort
strLenSort :: Sort
strLenSort    = Sort -> Sort -> Sort
FFunc Sort
strSort Sort
intSort
substrSort :: Sort
substrSort    = Int -> [Sort] -> Sort
mkFFunc Int
0 [Sort
strSort, Sort
intSort, Sort
intSort, Sort
strSort]
concatstrSort :: Sort
concatstrSort = Int -> [Sort] -> Sort
mkFFunc Int
0 [Sort
strSort, Sort
strSort, Sort
strSort]
strCompareSort :: Sort
strCompareSort = Int -> [Sort] -> Sort
mkFFunc Int
0 [Sort
strSort, Sort
strSort, Sort
boolSort]

string :: Raw
string :: Raw
string = Raw
forall a. IsString a => a
strConName

bFun :: Raw -> [(Builder, Builder)] -> Builder -> Builder -> Builder
bFun :: Raw -> [(Builder, Builder)] -> Builder -> Builder -> Builder
bFun Raw
name [(Builder, Builder)]
xts Builder
out Builder
body = Builder -> Builder -> Builder
key Builder
"define-fun" ([Builder] -> Builder
seqs [Raw -> Builder
fromText Raw
name, Builder
args, Builder
out, Builder
body])
  where
    args :: Builder
args = [Builder] -> Builder
parenSeqs [Builder -> Builder
parens (Builder
x Builder -> Builder -> Builder
<+> Builder
t) | (Builder
x, Builder
t) <- [(Builder, Builder)]
xts]

bFun' :: Raw -> [Builder] -> Builder -> Builder
bFun' :: Raw -> [Builder] -> Builder -> Builder
bFun' Raw
name [Builder]
ts Builder
out = Builder -> Builder -> Builder
key Builder
"declare-fun" ([Builder] -> Builder
seqs [Raw -> Builder
fromText Raw
name, Builder
args, Builder
out])
  where
    args :: Builder
args = [Builder] -> Builder
parenSeqs [Builder]
ts

bSort :: Raw -> Builder -> Builder
bSort :: Raw -> Builder -> Builder
bSort Raw
name Builder
def = Builder -> Builder -> Builder
key Builder
"define-sort" (Raw -> Builder
fromText Raw
name Builder -> Builder -> Builder
<+> Builder
"()" Builder -> Builder -> Builder
<+> Builder
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 :: Config -> Raw -> Raw -> Builder
uifDef Config
cfg Raw
f Raw
op
  | Config -> Bool
onlyLinearArith Config
cfg -- linear cfg || Z3 /= solver cfg
  = Raw -> [Builder] -> Builder -> Builder
bFun' Raw
f [Builder
"Int", Builder
"Int"] Builder
"Int"
  | Bool
otherwise
  = Raw -> [(Builder, Builder)] -> Builder -> Builder -> Builder
bFun Raw
f [(Builder
"x", Builder
"Int"), (Builder
"y", Builder
"Int")] Builder
"Int" (Builder -> Builder -> Builder -> Builder
key2 (Raw -> Builder
fromText Raw
op) Builder
"x" Builder
"y")

onlyLinearArith :: Config -> Bool
onlyLinearArith :: Config -> Bool
onlyLinearArith Config
cfg = Config -> Bool
linear Config
cfg Bool -> Bool -> Bool
|| Config -> SMTSolver
solver Config
cfg SMTSolver -> [SMTSolver] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [SMTSolver
Z3, SMTSolver
Z3mem, SMTSolver
Cvc5]

preamble :: Config -> SMTSolver -> [Builder]
preamble :: Config -> SMTSolver -> [Builder]
preamble Config
cfg SMTSolver
s = (PreambleCondition, Builder) -> Builder
forall a b. (a, b) -> b
snd ((PreambleCondition, Builder) -> Builder)
-> [(PreambleCondition, Builder)] -> [Builder]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((PreambleCondition, Builder) -> Bool)
-> [(PreambleCondition, Builder)] -> [(PreambleCondition, Builder)]
forall a. (a -> Bool) -> [a] -> [a]
filter (SMTSolver -> PreambleCondition -> Bool
matchesCondition SMTSolver
s (PreambleCondition -> Bool)
-> ((PreambleCondition, Builder) -> PreambleCondition)
-> (PreambleCondition, Builder)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PreambleCondition, Builder) -> PreambleCondition
forall a b. (a, b) -> a
fst) (Config -> [(PreambleCondition, Builder)]
solverPreamble Config
cfg)


matchesCondition :: SMTSolver -> PreambleCondition -> Bool
matchesCondition :: SMTSolver -> PreambleCondition -> Bool
matchesCondition SMTSolver
_ PreambleCondition
SAll       = Bool
True
matchesCondition SMTSolver
s (SOnly [SMTSolver]
ss) = SMTSolver
s SMTSolver -> [SMTSolver] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [SMTSolver]
ss

solverPreamble :: Config -> [Preamble]
solverPreamble :: Config -> [(PreambleCondition, Builder)]
solverPreamble Config
cfg
  =  [ ([SMTSolver] -> PreambleCondition
SOnly [SMTSolver
Z3, SMTSolver
Z3mem],  Builder
"(set-option :auto-config false)")
     , ([SMTSolver] -> PreambleCondition
SOnly [SMTSolver
Z3, SMTSolver
Z3mem],  Builder
"(set-option :model true)")
     , ([SMTSolver] -> PreambleCondition
SOnly [SMTSolver
Cvc4],       Builder
"(set-logic ALL_SUPPORTED)")
     , ([SMTSolver] -> PreambleCondition
SOnly [SMTSolver
Cvc5],       Builder
"(set-logic ALL)")
     , ([SMTSolver] -> PreambleCondition
SOnly [SMTSolver
Cvc4, SMTSolver
Cvc5], Builder
"(set-option :incremental true)")
     ]
  [(PreambleCondition, Builder)]
-> [(PreambleCondition, Builder)] -> [(PreambleCondition, Builder)]
forall a. [a] -> [a] -> [a]
++ Config -> [(PreambleCondition, Builder)]
setPreamble Config
cfg
  [(PreambleCondition, Builder)]
-> [(PreambleCondition, Builder)] -> [(PreambleCondition, Builder)]
forall a. [a] -> [a] -> [a]
++ Config -> [(PreambleCondition, Builder)]
boolPreamble Config
cfg
  [(PreambleCondition, Builder)]
-> [(PreambleCondition, Builder)] -> [(PreambleCondition, Builder)]
forall a. [a] -> [a] -> [a]
++ Config -> [(PreambleCondition, Builder)]
arithPreamble Config
cfg
  [(PreambleCondition, Builder)]
-> [(PreambleCondition, Builder)] -> [(PreambleCondition, Builder)]
forall a. [a] -> [a] -> [a]
++ Config -> [(PreambleCondition, Builder)]
stringPreamble Config
cfg

type Preamble = (PreambleCondition, Builder)

data PreambleCondition = SAll | SOnly [SMTSolver]
  deriving (PreambleCondition -> PreambleCondition -> Bool
(PreambleCondition -> PreambleCondition -> Bool)
-> (PreambleCondition -> PreambleCondition -> Bool)
-> Eq PreambleCondition
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PreambleCondition -> PreambleCondition -> Bool
== :: PreambleCondition -> PreambleCondition -> Bool
$c/= :: PreambleCondition -> PreambleCondition -> Bool
/= :: PreambleCondition -> PreambleCondition -> Bool
Eq, Int -> PreambleCondition -> ShowS
[PreambleCondition] -> ShowS
PreambleCondition -> String
(Int -> PreambleCondition -> ShowS)
-> (PreambleCondition -> String)
-> ([PreambleCondition] -> ShowS)
-> Show PreambleCondition
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PreambleCondition -> ShowS
showsPrec :: Int -> PreambleCondition -> ShowS
$cshow :: PreambleCondition -> String
show :: PreambleCondition -> String
$cshowList :: [PreambleCondition] -> ShowS
showList :: [PreambleCondition] -> ShowS
Show)

setPreamble :: Config -> [Preamble]
-- Z3 does not support cardinality on sets, which is defined to be uninterpreted function
setPreamble :: Config -> [(PreambleCondition, Builder)]
setPreamble Config
_
  = [ ([SMTSolver] -> PreambleCondition
SOnly [SMTSolver
Z3, SMTSolver
Z3mem],  Raw -> [Builder] -> Builder -> Builder
bFun' Raw
"set.card" [Builder
"(Array Int Bool)"] Builder
"Int") ]

boolPreamble :: Config -> [Preamble]
boolPreamble :: Config -> [(PreambleCondition, Builder)]
boolPreamble Config
_
  = [ (PreambleCondition
SAll, Raw -> [(Builder, Builder)] -> Builder -> Builder -> Builder
bFun Raw
forall a. IsString a => a
boolToIntName [(Builder
"b", Builder
"Bool")] Builder
"Int" Builder
"(ite b 1 0)") ]

arithPreamble :: Config -> [Preamble]
arithPreamble :: Config -> [(PreambleCondition, Builder)]
arithPreamble Config
cfg = (PreambleCondition
SAll,) (Builder -> (PreambleCondition, Builder))
-> [Builder] -> [(PreambleCondition, Builder)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
 [ Config -> Raw -> Raw -> Builder
uifDef Config
cfg (Symbol -> Raw
symbolText Symbol
mulFuncName) Raw
"*"
 , Config -> Raw -> Raw -> Builder
uifDef Config
cfg (Symbol -> Raw
symbolText Symbol
divFuncName) Raw
"div"
 ]

stringPreamble :: Config -> [Preamble]
stringPreamble :: Config -> [(PreambleCondition, Builder)]
stringPreamble Config
cfg | Bool -> Bool
not (Config -> Bool
noStringTheory Config
cfg)
  = [ (PreambleCondition
SAll, Raw -> Builder -> Builder
bSort Raw
string Builder
"String")
    , (PreambleCondition
SAll, Raw -> [(Builder, Builder)] -> Builder -> Builder -> Builder
bFun Raw
forall a. IsString a => a
strLen [(Builder
"s", Raw -> Builder
fromText Raw
string)] Builder
"Int" (Builder -> Builder -> Builder
key (Raw -> Builder
fromText Raw
smtlibStrLen) Builder
"s"))
    , (PreambleCondition
SAll, Raw -> [(Builder, Builder)] -> Builder -> Builder -> Builder
bFun Raw
forall a. IsString a => a
strSubstr [(Builder
"s", Raw -> Builder
fromText Raw
string), (Builder
"i", Builder
"Int"), (Builder
"j", Builder
"Int")] (Raw -> Builder
fromText Raw
string) (Builder -> Builder -> Builder
key (Raw -> Builder
fromText Raw
smtlibStrSubstr) Builder
"s i j"))
    , (PreambleCondition
SAll, Raw -> [(Builder, Builder)] -> Builder -> Builder -> Builder
bFun Raw
forall a. IsString a => a
strConcat [(Builder
"x", Raw -> Builder
fromText Raw
string), (Builder
"y", Raw -> Builder
fromText Raw
string)] (Raw -> Builder
fromText Raw
string) (Builder -> Builder -> Builder
key (Raw -> Builder
fromText Raw
smtlibStrConcat) Builder
"x y"))
    ]

stringPreamble Config
_
  = [ (PreambleCondition
SAll, Raw -> Builder -> Builder
bSort Raw
string Builder
"Int")
    , (PreambleCondition
SAll, Raw -> [Builder] -> Builder -> Builder
bFun' Raw
forall a. IsString a => a
strLen [Raw -> Builder
fromText Raw
string] Builder
"Int")
    , (PreambleCondition
SAll, Raw -> [Builder] -> Builder -> Builder
bFun' Raw
forall a. IsString a => a
strSubstr [Raw -> Builder
fromText Raw
string, Builder
"Int", Builder
"Int"] (Raw -> Builder
fromText Raw
string))
    , (PreambleCondition
SAll, Raw -> [Builder] -> Builder -> Builder
bFun' Raw
forall a. IsString a => a
strConcat [Raw -> Builder
fromText Raw
string, Raw -> Builder
fromText Raw
string] (Raw -> Builder
fromText Raw
string))
    ]

--------------------------------------------------------------------------------
-- | Exported API --------------------------------------------------------------
--------------------------------------------------------------------------------
smt2Symbol :: SymEnv -> Symbol -> Maybe Builder
smt2Symbol :: SymEnv -> Symbol -> Maybe Builder
smt2Symbol SymEnv
env Symbol
x = Raw -> Builder
fromText (Raw -> Builder)
-> (TheorySymbol -> Raw) -> TheorySymbol -> Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TheorySymbol -> Raw
tsRaw (TheorySymbol -> Builder) -> Maybe TheorySymbol -> Maybe Builder
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Symbol -> SymEnv -> Maybe TheorySymbol
symEnvTheory Symbol
x SymEnv
env

instance SMTLIB2 SmtSort where
  smt2 :: SmtSort -> SymM Builder
smt2 SmtSort
s = Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ SmtSort -> Builder
smt2SmtSort SmtSort
s

smt2SmtSort :: SmtSort -> Builder
smt2SmtSort :: SmtSort -> Builder
smt2SmtSort SmtSort
SInt         = Builder
"Int"
smt2SmtSort SmtSort
SReal        = Builder
"Real"
smt2SmtSort SmtSort
SBool        = Builder
"Bool"
smt2SmtSort SmtSort
SString      = Raw -> Builder
fromText Raw
string
smt2SmtSort (SSet SmtSort
a)     = Builder -> Builder -> Builder
key Builder
"Set" (SmtSort -> Builder
smt2SmtSort SmtSort
a)
smt2SmtSort (SBag SmtSort
a)     = Builder -> Builder -> Builder
key Builder
"Bag" (SmtSort -> Builder
smt2SmtSort SmtSort
a)
smt2SmtSort (SArray SmtSort
a SmtSort
b) = Builder -> Builder -> Builder -> Builder
key2 Builder
"Array" (SmtSort -> Builder
smt2SmtSort SmtSort
a) (SmtSort -> Builder
smt2SmtSort SmtSort
b)
smt2SmtSort (SFFld Integer
n)    = Builder -> Builder -> Builder
key Builder
"_ FiniteField" (Integer -> Builder
forall a. Show a => a -> Builder
bShow Integer
n)
smt2SmtSort (SBitVec Int
n)  = Builder -> Builder -> Builder
key Builder
"_ BitVec" (Int -> Builder
forall a. Show a => a -> Builder
bShow Int
n)
smt2SmtSort (SVar Int
n)     = Builder
"T" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Int -> Builder
forall a. Show a => a -> Builder
bShow Int
n
smt2SmtSort (SData FTycon
c []) = FTycon -> Builder
forall a. Symbolic a => a -> Builder
symbolBuilder FTycon
c
smt2SmtSort (SData FTycon
c [SmtSort]
ts) = [Builder] -> Builder
parenSeqs [FTycon -> Builder
forall a. Symbolic a => a -> Builder
symbolBuilder FTycon
c, [SmtSort] -> Builder
smt2SmtSorts [SmtSort]
ts]

-- smt2SmtSort (SApp ts)    = build "({} {})" (symbolBuilder tyAppName, smt2SmtSorts ts)

smt2SmtSorts :: [SmtSort] -> Builder
smt2SmtSorts :: [SmtSort] -> Builder
smt2SmtSorts = [Builder] -> Builder
seqs ([Builder] -> Builder)
-> ([SmtSort] -> [Builder]) -> [SmtSort] -> Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SmtSort -> Builder) -> [SmtSort] -> [Builder]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SmtSort -> Builder
smt2SmtSort

type VarAs = Symbol -> Sort -> SymM Builder
--------------------------------------------------------------------------------
smt2App :: VarAs -> Expr -> [Builder] -> SymM (Maybe Builder)
--------------------------------------------------------------------------------
smt2App :: VarAs -> Expr -> [Builder] -> SymM (Maybe Builder)
smt2App VarAs
_ ex :: Expr
ex@(Expr -> Expr
dropECst -> EVar Symbol
f) [Builder
d]
  | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
arrConstS Bool -> Bool -> Bool
|| Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
arrConstB Bool -> Bool -> Bool
|| Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
arrConstM =
      do SymEnv
env <- StateT SymEnv Identity SymEnv
forall s (m :: * -> *). MonadState s m => m s
get
         Maybe Builder -> SymM (Maybe Builder)
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Builder -> SymM (Maybe Builder))
-> Maybe Builder -> SymM (Maybe Builder)
forall a b. (a -> b) -> a -> b
$ Builder -> Maybe Builder
forall a. a -> Maybe a
Just (Builder -> Maybe Builder) -> Builder -> Maybe Builder
forall a b. (a -> b) -> a -> b
$ Builder -> Builder -> Builder
key (Builder -> Builder -> Builder
key Builder
"as const" (SymEnv -> Expr -> Builder
getTarget SymEnv
env Expr
ex)) Builder
d
  | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
forall a. IsString a => a
setEmpty  =
      do SymEnv
env <- StateT SymEnv Identity SymEnv
forall s (m :: * -> *). MonadState s m => m s
get
         Maybe Builder -> SymM (Maybe Builder)
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Builder -> SymM (Maybe Builder))
-> Maybe Builder -> SymM (Maybe Builder)
forall a b. (a -> b) -> a -> b
$ Builder -> Maybe Builder
forall a. a -> Maybe a
Just (Builder -> Maybe Builder) -> Builder -> Maybe Builder
forall a b. (a -> b) -> a -> b
$ Builder -> Builder -> Builder
key Builder
"as set.empty" (SymEnv -> Expr -> Builder
getTarget SymEnv
env Expr
ex)
  | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
forall a. IsString a => a
bagEmpty  =
      do SymEnv
env <- StateT SymEnv Identity SymEnv
forall s (m :: * -> *). MonadState s m => m s
get
         Maybe Builder -> SymM (Maybe Builder)
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Builder -> SymM (Maybe Builder))
-> Maybe Builder -> SymM (Maybe Builder)
forall a b. (a -> b) -> a -> b
$ Builder -> Maybe Builder
forall a. a -> Maybe a
Just (Builder -> Maybe Builder) -> Builder -> Maybe Builder
forall a b. (a -> b) -> a -> b
$ Builder -> Builder -> Builder
key Builder
"as bag.empty" (SymEnv -> Expr -> Builder
getTarget SymEnv
env Expr
ex)
  | Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
forall a. IsString a => a
ffVal  =
      do SymEnv
env <- StateT SymEnv Identity SymEnv
forall s (m :: * -> *). MonadState s m => m s
get
         Maybe Builder -> SymM (Maybe Builder)
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Builder -> SymM (Maybe Builder))
-> Maybe Builder -> SymM (Maybe Builder)
forall a b. (a -> b) -> a -> b
$ Builder -> Maybe Builder
forall a. a -> Maybe a
Just (Builder -> Maybe Builder) -> Builder -> Maybe Builder
forall a b. (a -> b) -> a -> b
$ Builder -> Builder -> Builder
key (Builder
"as ff" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
d) (SymEnv -> Expr -> Builder
getTarget SymEnv
env Expr
ex)
  where
    getTarget :: SymEnv -> Expr -> Builder
    -- const is a function, but SMT expects only the output sort
    getTarget :: SymEnv -> Expr -> Builder
getTarget SymEnv
env (ECst Expr
_ Sort
t) = SmtSort -> Builder
smt2SmtSort (SmtSort -> Builder) -> SmtSort -> Builder
forall a b. (a -> b) -> a -> b
$ Bool -> SEnv DataDecl -> Sort -> SmtSort
sortSmtSort Bool
True (SymEnv -> SEnv DataDecl
seData SymEnv
env) (Sort -> Sort
ffuncOut Sort
t)
    getTarget SymEnv
_ Expr
e = Expr -> Builder
forall a. Show a => a -> Builder
bShow Expr
e

smt2App VarAs
k Expr
ex (Builder
builder:[Builder]
builders) =
  do Maybe Builder
a <- VarAs -> Expr -> SymM (Maybe Builder)
smt2AppArg VarAs
k Expr
ex
     Maybe Builder -> SymM (Maybe Builder)
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Builder -> SymM (Maybe Builder))
-> Maybe Builder -> SymM (Maybe Builder)
forall a b. (a -> b) -> a -> b
$ (\Builder
fb -> Builder -> Builder -> Builder
key Builder
fb (Builder
builder Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> [Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat [ Builder
" " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
d | Builder
d <- [Builder]
builders])) (Builder -> Builder) -> Maybe Builder -> Maybe Builder
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Builder
a
smt2App VarAs
_ Expr
_ [] = Maybe Builder -> SymM (Maybe Builder)
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Builder
forall a. Maybe a
Nothing

smt2AppArg :: VarAs -> Expr -> SymM (Maybe Builder)
smt2AppArg :: VarAs -> Expr -> SymM (Maybe Builder)
smt2AppArg VarAs
k (ECst (Expr -> Expr
dropECst -> EVar Symbol
f) Sort
t)
  = do SymEnv
env <- StateT SymEnv Identity SymEnv
forall s (m :: * -> *). MonadState s m => m s
get
       case Symbol -> SymEnv -> Maybe TheorySymbol
symEnvTheory Symbol
f SymEnv
env of
         Just TheorySymbol
fThy -> if TheorySymbol -> Sort -> Bool
isPolyCtor TheorySymbol
fThy Sort
t
                           then Builder -> Maybe Builder
forall a. a -> Maybe a
Just (Builder -> Maybe Builder) -> SymM Builder -> SymM (Maybe Builder)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VarAs
k Symbol
f (Sort -> Sort
ffuncOut Sort
t)
                           else Maybe Builder -> SymM (Maybe Builder)
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Builder -> SymM (Maybe Builder))
-> Maybe Builder -> SymM (Maybe Builder)
forall a b. (a -> b) -> a -> b
$ Builder -> Maybe Builder
forall a. a -> Maybe a
Just (Builder -> Maybe Builder) -> Builder -> Maybe Builder
forall a b. (a -> b) -> a -> b
$ Raw -> Builder
fromText (TheorySymbol -> Raw
tsRaw TheorySymbol
fThy)
         Maybe TheorySymbol
Nothing   -> Maybe Builder -> SymM (Maybe Builder)
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Builder
forall a. Maybe a
Nothing
smt2AppArg VarAs
_ Expr
_
  = Maybe Builder -> SymM (Maybe Builder)
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Builder
forall a. Maybe a
Nothing

isPolyCtor :: TheorySymbol -> Sort -> Bool
isPolyCtor :: TheorySymbol -> Sort -> Bool
isPolyCtor TheorySymbol
fThy Sort
t = Sort -> Sort -> Bool
isPolyInst (TheorySymbol -> Sort
tsSort TheorySymbol
fThy) Sort
t Bool -> Bool -> Bool
&& TheorySymbol -> Sem
tsInterp TheorySymbol
fThy Sem -> Sem -> Bool
forall a. Eq a => a -> a -> Bool
== Sem
Ctor

ffuncOut :: Sort -> Sort
ffuncOut :: Sort -> Sort
ffuncOut Sort
t = Sort -> ((Int, [Sort]) -> Sort) -> Maybe (Int, [Sort]) -> Sort
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Sort
t ([Sort] -> Sort
forall a. HasCallStack => [a] -> a
last ([Sort] -> Sort)
-> ((Int, [Sort]) -> [Sort]) -> (Int, [Sort]) -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, [Sort]) -> [Sort]
forall a b. (a, b) -> b
snd) (Sort -> Maybe (Int, [Sort])
bkFFunc Sort
t)

--------------------------------------------------------------------------------
isSmt2App :: SEnv TheorySymbol -> Expr -> Maybe Int
--------------------------------------------------------------------------------
isSmt2App :: SEnv TheorySymbol -> Expr -> Maybe Int
isSmt2App SEnv TheorySymbol
g (Expr -> Expr
dropECst -> EVar Symbol
f) = Symbol -> SEnv TheorySymbol -> Maybe TheorySymbol
forall a. Symbol -> SEnv a -> Maybe a
lookupSEnv Symbol
f SEnv TheorySymbol
g Maybe TheorySymbol -> (TheorySymbol -> Maybe Int) -> Maybe Int
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= TheorySymbol -> Maybe Int
thyAppInfo
isSmt2App SEnv TheorySymbol
_  Expr
_                   = Maybe Int
forall a. Maybe a
Nothing

thyAppInfo :: TheorySymbol -> Maybe Int
thyAppInfo :: TheorySymbol -> Maybe Int
thyAppInfo TheorySymbol
ti = case TheorySymbol -> Sem
tsInterp TheorySymbol
ti of
  Sem
Field    -> Int -> Maybe Int
forall a. a -> Maybe a
Just Int
1
  Sem
_        -> Sort -> Maybe Int
sortAppInfo (TheorySymbol -> Sort
tsSort TheorySymbol
ti)

sortAppInfo :: Sort -> Maybe Int
sortAppInfo :: Sort -> Maybe Int
sortAppInfo Sort
t = case Sort -> Maybe (Int, [Sort])
bkFFunc Sort
t of
  Just (Int
_, [Sort]
ts) -> Int -> Maybe Int
forall a. a -> Maybe a
Just ([Sort] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Sort]
ts Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
  Maybe (Int, [Sort])
Nothing      -> Maybe Int
forall a. Maybe a
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 :: SMTSolver -> SEnv TheorySymbol
theorySymbols = [(Symbol, TheorySymbol)] -> SEnv TheorySymbol
forall a. [(Symbol, a)] -> SEnv a
fromListSEnv ([(Symbol, TheorySymbol)] -> SEnv TheorySymbol)
-> (SMTSolver -> [(Symbol, TheorySymbol)])
-> SMTSolver
-> SEnv TheorySymbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SMTSolver -> [(Symbol, TheorySymbol)]
interpSymbols

instance TheorySymbols [DataDecl] where
  theorySymbols :: [DataDecl] -> SEnv TheorySymbol
  theorySymbols :: [DataDecl] -> SEnv TheorySymbol
theorySymbols = [(Symbol, TheorySymbol)] -> SEnv TheorySymbol
forall a. [(Symbol, a)] -> SEnv a
fromListSEnv ([(Symbol, TheorySymbol)] -> SEnv TheorySymbol)
-> ([DataDecl] -> [(Symbol, TheorySymbol)])
-> [DataDecl]
-> SEnv TheorySymbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DataDecl -> [(Symbol, TheorySymbol)])
-> [DataDecl] -> [(Symbol, TheorySymbol)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap DataDecl -> [(Symbol, TheorySymbol)]
dataDeclSymbols


instance TheorySymbols [Equation] where
  theorySymbols :: [Equation] -> SEnv TheorySymbol
theorySymbols = [(Symbol, TheorySymbol)] -> SEnv TheorySymbol
forall a. [(Symbol, a)] -> SEnv a
fromListSEnv ([(Symbol, TheorySymbol)] -> SEnv TheorySymbol)
-> ([Equation] -> [(Symbol, TheorySymbol)])
-> [Equation]
-> SEnv TheorySymbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Equation -> (Symbol, TheorySymbol))
-> [Equation] -> [(Symbol, TheorySymbol)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Equation -> (Symbol, TheorySymbol)
equationSymbol

instance TheorySymbols DefinedFuns where
  theorySymbols :: DefinedFuns -> SEnv TheorySymbol
theorySymbols (MkDefinedFuns [Equation]
eqns) = [Equation] -> SEnv TheorySymbol
forall a. TheorySymbols a => a -> SEnv TheorySymbol
theorySymbols [Equation]
eqns

equationSymbol :: Equation -> (Symbol, TheorySymbol)
equationSymbol :: Equation -> (Symbol, TheorySymbol)
equationSymbol Equation
eq = (Symbol
sym, Symbol -> Raw -> Sort -> Sem -> TheorySymbol
Thy Symbol
sym (Symbol -> Raw
symbolRaw Symbol
sym) Sort
sort Sem
Defined)
  where
    sym :: Symbol
sym  = Equation -> Symbol
forall v. EquationV v -> Symbol
eqName Equation
eq
    sort :: Sort
sort = Int -> [Sort] -> Sort
mkFFunc Int
0 (((Symbol, Sort) -> Sort
forall a b. (a, b) -> b
snd ((Symbol, Sort) -> Sort) -> [(Symbol, Sort)] -> [Sort]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Equation -> [(Symbol, Sort)]
forall v. EquationV v -> [(Symbol, Sort)]
eqArgs Equation
eq) [Sort] -> [Sort] -> [Sort]
forall a. Semigroup a => a -> a -> a
<> [Equation -> Sort
forall v. EquationV v -> Sort
eqSort Equation
eq])

--------------------------------------------------------------------------------
interpSymbols :: SMTSolver -> [(Symbol, TheorySymbol)]
--------------------------------------------------------------------------------
interpSymbols :: SMTSolver -> [(Symbol, TheorySymbol)]
interpSymbols SMTSolver
cfg =
  [
    -- maps

    Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
mapDef   Raw
forall a. IsString a => a
mapDef  Sort
mapDefSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
mapSel   Raw
forall a. IsString a => a
mapSel  Sort
mapSelSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
mapSto   Raw
forall a. IsString a => a
mapSto  Sort
mapStoSort

  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
arrConstM  Raw
"const"  (Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
1) Sort
mapArrSort)
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
arrSelectM Raw
"select" (Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
mapArrSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
0) (Int -> Sort
FVar Int
1))
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
arrStoreM  Raw
"store"  (Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
mapArrSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
0) (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
1) Sort
mapArrSort)

  -- CVC5 sets

  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
setCard  Raw
"set.card"       (Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort
setSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort
FVar Int
0) Sort
intSort)
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
setEmp   Raw
"set.is_empty"   (Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort
setSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort
FVar Int
0) Sort
boolSort)
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
setEmpty Raw
"set.empty"      (Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
intSort (Sort -> Sort
setSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort
FVar Int
0))
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
setSng   Raw
"set.singleton"  (Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
0) (Sort -> Sort
setSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort
FVar Int
0))
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
setAdd   Raw
"set.insert"     (Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
0) (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort
setSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort
FVar Int
0) (Sort -> Sort
setSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort
FVar Int
0))
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
setMem   Raw
"set.member"     (Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
0) (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort
setSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort
FVar Int
0) Sort
boolSort)
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
setCup   Raw
"set.union"      Sort
setBopSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
setCap   Raw
"set.inter"      Sort
setBopSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
setDif   Raw
"set.minus"      Sort
setBopSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
setSub   Raw
"set.subset"     (Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort
setSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort
FVar Int
0) (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort
setSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort
FVar Int
0) Sort
boolSort)
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
setCom   Raw
"set.complement" (Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort
setSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort
FVar Int
0) (Sort -> Sort
setSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort
FVar Int
0))

  -- CVC5 bags

  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
bagEmpty Raw
"bag.empty"          (Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
intSort (Sort -> Sort
bagSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort
FVar Int
0))
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
bagSng   Raw
"bag"                (Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
0) (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
intSort (Sort -> Sort
bagSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort
FVar Int
0))
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
bagCount Raw
"bag.count"          (Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
0) (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort
bagSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort
FVar Int
0) Sort
intSort)
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
bagCup   Raw
"bag.union_disjoint" Sort
bagBopSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
bagMax   Raw
"bag.union_max"      Sort
bagBopSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
bagMin   Raw
"bag.inter_min"      Sort
bagBopSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
bagSub   Raw
"bag.subbag"         (Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort
bagSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort
FVar Int
0) (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort
bagSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort
FVar Int
0) Sort
boolSort)

  -- Strings
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
strLen     Raw
forall a. IsString a => a
strLen    Sort
strLenSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
strSubstr  Raw
forall a. IsString a => a
strSubstr Sort
substrSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
strConcat  Raw
forall a. IsString a => a
strConcat Sort
concatstrSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
strConcat' Raw
smtlibStrConcat Sort
concatstrSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
strPrefixOf Raw
smtlibStrPrefixOf Sort
strCompareSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
strSuffixOf Raw
smtlibStrSuffixOf Sort
strCompareSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
strContains Raw
smtlibStrContains Sort
strCompareSort

  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
boolInt   Raw
forall a. IsString a => a
boolInt   (Sort -> Sort -> Sort
FFunc Sort
boolSort Sort
intSort)

  -- Function mappings for indexed identifier functions
  , Symbol -> Sort -> (Symbol, TheorySymbol)
interpSym' Symbol
"_" Sort
iiSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
"app" Raw
"" Sort
appSort

  , Symbol -> Sort -> (Symbol, TheorySymbol)
interpSym' Symbol
bvConcatName Sort
bvConcatSort
  , Symbol -> Sort -> (Symbol, TheorySymbol)
interpSym' Symbol
bvExtractName (Sort -> Sort -> Sort
FFunc Sort
FInt Sort
bvExtendSort)
  , Symbol -> (Symbol, TheorySymbol)
interpBvExt Symbol
bvRepeatName
  , Symbol -> (Symbol, TheorySymbol)
interpBvExt Symbol
bvZeroExtName
  , Symbol -> (Symbol, TheorySymbol)
interpBvExt Symbol
bvSignExtName

  , Symbol -> (Symbol, TheorySymbol)
interpBvUop Symbol
bvNotName
  , Symbol -> (Symbol, TheorySymbol)
interpBvUop Symbol
bvNegName

  , Symbol -> (Symbol, TheorySymbol)
interpBvBop Symbol
bvAndName
  , Symbol -> (Symbol, TheorySymbol)
interpBvBop Symbol
bvNandName
  , Symbol -> (Symbol, TheorySymbol)
interpBvBop Symbol
bvOrName
  , Symbol -> (Symbol, TheorySymbol)
interpBvBop Symbol
bvNorName
  , Symbol -> (Symbol, TheorySymbol)
interpBvBop Symbol
bvXorName
  , Symbol -> (Symbol, TheorySymbol)
interpBvBop Symbol
bvXnorName

  , Symbol -> (Symbol, TheorySymbol)
interpBvBop Symbol
bvShlName
  , Symbol -> (Symbol, TheorySymbol)
interpBvBop Symbol
bvLShrName
  , Symbol -> (Symbol, TheorySymbol)
interpBvBop Symbol
bvAShrName
  , Symbol -> (Symbol, TheorySymbol)
interpBvRot Symbol
bvLRotName
  , Symbol -> (Symbol, TheorySymbol)
interpBvRot Symbol
bvRRotName

  , Symbol -> (Symbol, TheorySymbol)
interpBvBop Symbol
bvAddName
  , Symbol -> (Symbol, TheorySymbol)
interpBvBop Symbol
bvSubName
  , Symbol -> (Symbol, TheorySymbol)
interpBvBop Symbol
bvMulName
  , Symbol -> (Symbol, TheorySymbol)
interpBvBop Symbol
bvUDivName
  , Symbol -> (Symbol, TheorySymbol)
interpBvBop Symbol
bvURemName
  , Symbol -> (Symbol, TheorySymbol)
interpBvBop Symbol
bvSDivName
  , Symbol -> (Symbol, TheorySymbol)
interpBvBop Symbol
bvSRemName
  , Symbol -> (Symbol, TheorySymbol)
interpBvBop Symbol
bvSModName

  , Symbol -> Sort -> (Symbol, TheorySymbol)
interpSym' Symbol
bvCompName Sort
bvEqSort
  , Symbol -> (Symbol, TheorySymbol)
interpBvCmp Symbol
bvULtName
  , Symbol -> (Symbol, TheorySymbol)
interpBvCmp Symbol
bvULeName
  , Symbol -> (Symbol, TheorySymbol)
interpBvCmp Symbol
bvUGtName
  , Symbol -> (Symbol, TheorySymbol)
interpBvCmp Symbol
bvUGeName
  , Symbol -> (Symbol, TheorySymbol)
interpBvCmp Symbol
bvSLtName
  , Symbol -> (Symbol, TheorySymbol)
interpBvCmp Symbol
bvSLeName
  , Symbol -> (Symbol, TheorySymbol)
interpBvCmp Symbol
bvSGtName
  , Symbol -> (Symbol, TheorySymbol)
interpBvCmp Symbol
bvSGeName

  -- int to bv Conversions

  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
intbv32Name   Raw
"(_ int2bv 32)" (Sort -> Sort -> Sort
FFunc Sort
intSort Sort
bv32)
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
intbv64Name   Raw
"(_ int2bv 64)" (Sort -> Sort -> Sort
FFunc Sort
intSort Sort
bv64)
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
bv32intName   (SMTSolver -> Int -> Raw
bv2i SMTSolver
cfg Int
32)   (Sort -> Sort -> Sort
FFunc Sort
bv32    Sort
intSort)
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
bv64intName   (SMTSolver -> Int -> Raw
bv2i SMTSolver
cfg Int
64)   (Sort -> Sort -> Sort
FFunc Sort
bv64    Sort
intSort)

  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
intbv8Name    Raw
"(_ int2bv 8)"  (Sort -> Sort -> Sort
FFunc Sort
intSort Sort
bv8)
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
intbv16Name   Raw
"(_ int2bv 16)" (Sort -> Sort -> Sort
FFunc Sort
intSort Sort
bv16)
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
bv8intName    (SMTSolver -> Int -> Raw
bv2i SMTSolver
cfg Int
32)   (Sort -> Sort -> Sort
FFunc Sort
bv8    Sort
intSort)
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
bv16intName   (SMTSolver -> Int -> Raw
bv2i SMTSolver
cfg Int
64)   (Sort -> Sort -> Sort
FFunc Sort
bv16    Sort
intSort)
  ]
  [(Symbol, TheorySymbol)]
-> [(Symbol, TheorySymbol)] -> [(Symbol, TheorySymbol)]
forall a. [a] -> [a] -> [a]
++
  if SMTSolver
cfg SMTSolver -> SMTSolver -> Bool
forall a. Eq a => a -> a -> Bool
== SMTSolver
Z3 Bool -> Bool -> Bool
|| SMTSolver
cfg SMTSolver -> SMTSolver -> Bool
forall a. Eq a => a -> a -> Bool
== SMTSolver
Z3mem
  then
  [
    -- Z3 sets (arrays of bools)

    Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
arrConstS  Raw
"const"  (Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
boolSort Sort
setArrSort)
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
arrSelectS Raw
"select" (Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
setArrSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
0) Sort
boolSort)
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
arrStoreS  Raw
"store"  (Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
setArrSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
0) (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
boolSort Sort
setArrSort)

  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
arrMapNotS Raw
"(_ map not)" (Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
setArrSort Sort
setArrSort)
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
arrMapOrS  Raw
"(_ map or)"  (Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
setArrSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
setArrSort Sort
setArrSort)
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
arrMapAndS Raw
"(_ map and)" (Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
setArrSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
setArrSort Sort
setArrSort)
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
arrMapImpS Raw
"(_ map =>)"  (Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
setArrSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
setArrSort Sort
setArrSort)

    -- Z3 bags (arrays of ints)

  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
arrConstB  Raw
"const"  (Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
intSort Sort
bagArrSort)
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
arrSelectB Raw
"select" (Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
bagArrSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
0) Sort
intSort)
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
arrStoreB  Raw
"store"  (Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
bagArrSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
0) (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
intSort Sort
bagArrSort)

  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
arrMapPlusB Raw
"(_ map (+ (Int Int) Int))"        (Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
bagArrSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
bagArrSort Sort
bagArrSort)
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
arrMapLeB   Raw
"(_ map (<= (Int Int) Bool))"      (Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
bagArrSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
bagArrSort Sort
setArrSort)
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
arrMapGtB   Raw
"(_ map (> (Int Int) Bool))"       (Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
bagArrSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
bagArrSort Sort
setArrSort)
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
arrMapIteB  Raw
"(_ map (ite (Bool Int Int) Int))" (Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
setArrSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
bagArrSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
bagArrSort Sort
bagArrSort)
  ] else if SMTSolver
cfg SMTSolver -> SMTSolver -> Bool
forall a. Eq a => a -> a -> Bool
== SMTSolver
Cvc5
  then
  [
    -- CVC5 finite fields

    Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
ffVal Raw
forall a. IsString a => a
ffVal     (Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
intSort (Sort -> Sort
finfieldSort (Int -> Sort
FVar Int
0)))
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
ffAdd Raw
"ff.add" (Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort
finfieldSort (Int -> Sort
FVar Int
0)) (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort
finfieldSort (Int -> Sort
FVar Int
0)) (Sort -> Sort
finfieldSort (Int -> Sort
FVar Int
0)))
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
forall a. IsString a => a
ffMul Raw
"ff.mul" (Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort
finfieldSort (Int -> Sort
FVar Int
0)) (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort
finfieldSort (Int -> Sort
FVar Int
0)) (Sort -> Sort
finfieldSort (Int -> Sort
FVar Int
0)))
  ] else []
  where

    mapArrSort :: Sort
mapArrSort = Sort -> Sort -> Sort
arraySort (Int -> Sort
FVar Int
0) (Int -> Sort
FVar Int
1)
    setArrSort :: Sort
setArrSort = Sort -> Sort -> Sort
arraySort (Int -> Sort
FVar Int
0) Sort
boolSort
    bagArrSort :: Sort
bagArrSort = Sort -> Sort -> Sort
arraySort (Int -> Sort
FVar Int
0) Sort
intSort
    bv8 :: Sort
bv8        = Symbol -> Sort
sizedBitVecSort Symbol
"Size8"
    bv16 :: Sort
bv16       = Symbol -> Sort
sizedBitVecSort Symbol
"Size16"
    bv32 :: Sort
bv32       = Symbol -> Sort
sizedBitVecSort Symbol
"Size32"
    bv64 :: Sort
bv64       = Symbol -> Sort
sizedBitVecSort Symbol
"Size64"
    boolInt :: a
boolInt    = a
forall a. IsString a => a
boolToIntName

    mapDefSort :: Sort
mapDefSort = Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort -> Sort
FAbs Int
1 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
1)
                                         (Sort -> Sort -> Sort
mapSort (Int -> Sort
FVar Int
0) (Int -> Sort
FVar Int
1))
    -- select :: forall k v. Map k v -> k -> v
    mapSelSort :: Sort
mapSelSort = Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort -> Sort
FAbs Int
1 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort -> Sort
mapSort (Int -> Sort
FVar Int
0) (Int -> Sort
FVar Int
1))
                                 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
0) (Int -> Sort
FVar Int
1)
    -- store :: forall k v. Map k v -> k -> v -> Map k v
    mapStoSort :: Sort
mapStoSort = Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort -> Sort
FAbs Int
1 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort -> Sort
mapSort (Int -> Sort
FVar Int
0) (Int -> Sort
FVar Int
1))
                                 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
0)
                                 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
1)
                                         (Sort -> Sort -> Sort
mapSort (Int -> Sort
FVar Int
0) (Int -> Sort
FVar Int
1))

    setBopSort :: Sort
setBopSort = Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort
setSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort
FVar Int
0) (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort
setSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort
FVar Int
0) (Sort -> Sort
setSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort
FVar Int
0)
    bagBopSort :: Sort
bagBopSort = Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort
bagSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort
FVar Int
0) (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort
bagSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort
FVar Int
0) (Sort -> Sort
bagSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort
FVar Int
0)

bv2i :: SMTSolver -> Int -> Raw
bv2i :: SMTSolver -> Int -> Raw
bv2i SMTSolver
Cvc4 Int
_ = Raw
"bv2nat"
bv2i SMTSolver
Cvc5 Int
_ = Raw
"bv2nat"
bv2i SMTSolver
_    Int
n = String -> Raw
Data.Text.pack (String -> Raw) -> String -> Raw
forall a b. (a -> b) -> a -> b
$ String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"(_ bv2nat %d)" Int
n

interpBvUop :: Symbol -> (Symbol, TheorySymbol)
interpBvUop :: Symbol -> (Symbol, TheorySymbol)
interpBvUop Symbol
name = Symbol -> Sort -> (Symbol, TheorySymbol)
interpSym' Symbol
name Sort
bvUopSort
interpBvBop :: Symbol -> (Symbol, TheorySymbol)
interpBvBop :: Symbol -> (Symbol, TheorySymbol)
interpBvBop Symbol
name = Symbol -> Sort -> (Symbol, TheorySymbol)
interpSym' Symbol
name Sort
bvBopSort
interpBvCmp :: Symbol -> (Symbol, TheorySymbol)
interpBvCmp :: Symbol -> (Symbol, TheorySymbol)
interpBvCmp Symbol
name = Symbol -> Sort -> (Symbol, TheorySymbol)
interpSym' Symbol
name Sort
bvCmpSort
interpBvExt :: Symbol -> (Symbol, TheorySymbol)
interpBvExt :: Symbol -> (Symbol, TheorySymbol)
interpBvExt Symbol
name = Symbol -> Sort -> (Symbol, TheorySymbol)
interpSym' Symbol
name Sort
bvExtendSort
interpBvRot :: Symbol -> (Symbol, TheorySymbol)
interpBvRot :: Symbol -> (Symbol, TheorySymbol)
interpBvRot Symbol
name = Symbol -> Sort -> (Symbol, TheorySymbol)
interpSym' Symbol
name Sort
bvRotSort

interpSym' :: Symbol -> Sort -> (Symbol, TheorySymbol)
interpSym' :: Symbol -> Sort -> (Symbol, TheorySymbol)
interpSym' Symbol
name = Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
name (String -> Raw
Data.Text.pack (String -> Raw) -> String -> Raw
forall a b. (a -> b) -> a -> b
$ Symbol -> String
symbolString Symbol
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 :: Sort
iiSort = Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort -> Sort
FAbs Int
1 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort -> Sort
FAbs Int
2 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc
               (Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
0) (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
1) (Int -> Sort
FVar Int
2))
               (Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
0) (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
1) (Int -> Sort
FVar Int
2))

-- Simple application, used for indexed identifier function, check '_'.
--
-- app :: forall a b. (a -> b) -> a -> b
appSort :: Sort
appSort :: Sort
appSort = Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort -> Sort
FAbs Int
1 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc
                (Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
0) (Int -> Sort
FVar Int
1))
                (Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
0) (Int -> Sort
FVar Int
1))

-- Indexed identifier operation, purposely didn't place FAbs!
--
-- extend :: Int -> BitVec a -> BitVec b
bvExtendSort :: Sort
bvExtendSort :: Sort
bvExtendSort  = Sort -> Sort -> Sort
FFunc Sort
FInt (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
bitVecSort Int
1) (Int -> Sort
bitVecSort Int
2)

-- Indexed identifier operation, purposely didn't place FAbs!
--
-- rot :: Int -> BitVec a -> BitVec a
bvRotSort :: Sort
bvRotSort :: Sort
bvRotSort  = Sort -> Sort -> Sort
FFunc Sort
FInt (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
bitVecSort Int
0) (Int -> Sort
bitVecSort Int
0)

-- uOp :: forall a. BitVec a -> BitVec a
bvUopSort :: Sort
bvUopSort :: Sort
bvUopSort = Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
bitVecSort Int
0) (Int -> Sort
bitVecSort Int
0)

-- bOp :: forall a. BitVec a -> BitVec a -> BitVec a
bvBopSort :: Sort
bvBopSort :: Sort
bvBopSort = Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
bitVecSort Int
0) (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
bitVecSort Int
0) (Int -> Sort
bitVecSort Int
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 :: Sort
bvCmpSort = Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
bitVecSort Int
0) (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
bitVecSort Int
0) Sort
boolSort

-- eq :: forall a. BitVec a -> BitVec a -> BitVec 1
bvEqSort :: Sort
bvEqSort :: Sort
bvEqSort = Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
bitVecSort Int
0) (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
bitVecSort Int
0) (Symbol -> Sort
sizedBitVecSort Symbol
"Size1")

-- concat :: forall a b c. BitVec a -> BitVec b -> BitVec c
bvConcatSort :: Sort
bvConcatSort :: Sort
bvConcatSort = Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort -> Sort
FAbs Int
1 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort -> Sort
FAbs Int
2 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$
                     Sort -> Sort -> Sort
FFunc (Int -> Sort
bitVecSort Int
0) (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
bitVecSort Int
1) (Int -> Sort
bitVecSort Int
2)

interpSym :: Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym :: Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
x Raw
n Sort
t = (Symbol
x, Symbol -> Raw -> Sort -> Sem -> TheorySymbol
Thy Symbol
x Raw
n Sort
t Sem
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 :: Int
maxLamArg = Int
20

axiomLiterals :: Config -> [(Symbol, Sort)] -> [Expr]
axiomLiterals :: Config -> [(Symbol, Sort)] -> [Expr]
axiomLiterals Config
cfg
  | Config -> Bool
noStringTheory Config
cfg = [(Symbol, Sort)] -> [Expr]
lenAxiomLiterals
  | Bool
otherwise          = [(Symbol, Sort)] -> [Expr]
strAxiomLiterals

strAxiomLiterals :: [(Symbol, Sort)] -> [Expr]
strAxiomLiterals :: [(Symbol, Sort)] -> [Expr]
strAxiomLiterals [(Symbol, Sort)]
lts = [Maybe Expr] -> [Expr]
forall a. [Maybe a] -> [a]
catMaybes [ Symbol -> Maybe Expr
strAxiom Symbol
l | (Symbol
l, Sort
t) <- [(Symbol, Sort)]
lts, Sort -> Bool
isString Sort
t ]
  where
    strAxiom :: Symbol -> Maybe Expr
strAxiom Symbol
l = do
      Symbol
sym <- Symbol -> Maybe Symbol
unLitSymbol Symbol
l
      Expr -> Maybe Expr
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EEq (Symbol -> Expr
forall a. Expression a => a -> Expr
expr Symbol
l) (Constant -> Expr
forall v. Constant -> ExprV v
ECon (Constant -> Expr) -> Constant -> Expr
forall a b. (a -> b) -> a -> b
$ Raw -> Sort -> Constant
L (Symbol -> Raw
symbolText Symbol
sym) Sort
strSort))

lenAxiomLiterals :: [(Symbol, Sort)] -> [Expr]
lenAxiomLiterals :: [(Symbol, Sort)] -> [Expr]
lenAxiomLiterals [(Symbol, Sort)]
lts = [Maybe Expr] -> [Expr]
forall a. [Maybe a] -> [a]
catMaybes [ Symbol -> Int -> Expr
forall {a} {a}. (Expression a, Expression a) => a -> a -> Expr
lenAxiom Symbol
l (Int -> Expr) -> Maybe Int -> Maybe Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Symbol -> Maybe Int
litLen Symbol
l | (Symbol
l, Sort
t) <- [(Symbol, Sort)]
lts, Sort -> Bool
isString Sort
t ]
  where
    lenAxiom :: a -> a -> Expr
lenAxiom a
l a
n  = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EEq (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall a. Expression a => a -> Expr
expr (Symbol
forall a. IsString a => a
strLen :: Symbol)) (a -> Expr
forall a. Expression a => a -> Expr
expr a
l)) (a -> Expr
forall a. Expression a => a -> Expr
expr a
n Expr -> Sort -> Expr
forall v. ExprV v -> Sort -> ExprV v
`ECst` Sort
intSort)
    litLen :: Symbol -> Maybe Int
litLen        = (Symbol -> Int) -> Maybe Symbol -> Maybe Int
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Raw -> Int
Data.Text.length (Raw -> Int) -> (Symbol -> Raw) -> Symbol -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  Symbol -> Raw
symbolText) (Maybe Symbol -> Maybe Int)
-> (Symbol -> Maybe Symbol) -> Symbol -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Maybe Symbol
unLitSymbol

--------------------------------------------------------------------------------
-- | Constructors, Selectors and Tests from 'DataDecl'arations.
--------------------------------------------------------------------------------
dataDeclSymbols :: DataDecl -> [(Symbol, TheorySymbol)]
dataDeclSymbols :: DataDecl -> [(Symbol, TheorySymbol)]
dataDeclSymbols DataDecl
d = DataDecl -> [(Symbol, TheorySymbol)]
ctorSymbols DataDecl
d [(Symbol, TheorySymbol)]
-> [(Symbol, TheorySymbol)] -> [(Symbol, TheorySymbol)]
forall a. [a] -> [a] -> [a]
++ DataDecl -> [(Symbol, TheorySymbol)]
testSymbols DataDecl
d [(Symbol, TheorySymbol)]
-> [(Symbol, TheorySymbol)] -> [(Symbol, TheorySymbol)]
forall a. [a] -> [a] -> [a]
++ DataDecl -> [(Symbol, TheorySymbol)]
selectSymbols DataDecl
d

-- | 'selfSort d' returns the _self-sort_ of 'd' :: 'DataDecl'.
--   See [NOTE:DataDecl] for details.

selfSort :: DataDecl -> Sort
selfSort :: DataDecl -> Sort
selfSort (DDecl FTycon
c Int
n [DataCtor]
_) = FTycon -> [Sort] -> Sort
fAppTC FTycon
c (Int -> Sort
FVar (Int -> Sort) -> [Int] -> [Sort]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
0..(Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
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 :: DataDecl -> Sort -> Sort
fldSort DataDecl
d (FTC FTycon
c)
  | FTycon
c FTycon -> FTycon -> Bool
forall a. Eq a => a -> a -> Bool
== DataDecl -> FTycon
ddTyCon DataDecl
d = DataDecl -> Sort
selfSort DataDecl
d
fldSort DataDecl
_ Sort
s        = Sort
s

--------------------------------------------------------------------------------
ctorSymbols :: DataDecl -> [(Symbol, TheorySymbol)]
--------------------------------------------------------------------------------
ctorSymbols :: DataDecl -> [(Symbol, TheorySymbol)]
ctorSymbols DataDecl
d = DataDecl -> DataCtor -> (Symbol, TheorySymbol)
ctorSort DataDecl
d (DataCtor -> (Symbol, TheorySymbol))
-> [DataCtor] -> [(Symbol, TheorySymbol)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DataDecl -> [DataCtor]
ddCtors DataDecl
d

ctorSort :: DataDecl -> DataCtor -> (Symbol, TheorySymbol)
ctorSort :: DataDecl -> DataCtor -> (Symbol, TheorySymbol)
ctorSort DataDecl
d DataCtor
ctor = (Symbol
x, Symbol -> Raw -> Sort -> Sem -> TheorySymbol
Thy Symbol
x (Symbol -> Raw
symbolRaw Symbol
x) Sort
t Sem
Ctor)
  where
    x :: Symbol
x           = DataCtor -> Symbol
forall a. Symbolic a => a -> Symbol
symbol DataCtor
ctor
    t :: Sort
t           = Int -> [Sort] -> Sort
mkFFunc Int
n ([Sort]
ts [Sort] -> [Sort] -> [Sort]
forall a. [a] -> [a] -> [a]
++ [DataDecl -> Sort
selfSort DataDecl
d])
    n :: Int
n           = DataDecl -> Int
ddVars DataDecl
d
    ts :: [Sort]
ts          = DataDecl -> Sort -> Sort
fldSort DataDecl
d (Sort -> Sort) -> (DataField -> Sort) -> DataField -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataField -> Sort
dfSort (DataField -> Sort) -> [DataField] -> [Sort]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DataCtor -> [DataField]
dcFields DataCtor
ctor

--------------------------------------------------------------------------------
testSymbols :: DataDecl -> [(Symbol, TheorySymbol)]
--------------------------------------------------------------------------------
testSymbols :: DataDecl -> [(Symbol, TheorySymbol)]
testSymbols DataDecl
d = Sort -> Symbol -> (Symbol, TheorySymbol)
testTheory Sort
t (Symbol -> (Symbol, TheorySymbol))
-> (DataCtor -> Symbol) -> DataCtor -> (Symbol, TheorySymbol)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCtor -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (DataCtor -> (Symbol, TheorySymbol))
-> [DataCtor] -> [(Symbol, TheorySymbol)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DataDecl -> [DataCtor]
ddCtors DataDecl
d
  where
    t :: Sort
t         = Int -> [Sort] -> Sort
mkFFunc (DataDecl -> Int
ddVars DataDecl
d) [DataDecl -> Sort
selfSort DataDecl
d, Sort
boolSort]

testTheory :: Sort -> Symbol -> (Symbol, TheorySymbol)
testTheory :: Sort -> Symbol -> (Symbol, TheorySymbol)
testTheory Sort
t Symbol
x = (Symbol
sx, Symbol -> Raw -> Sort -> Sem -> TheorySymbol
Thy Symbol
sx Raw
raw Sort
t Sem
Test)
  where
    sx :: Symbol
sx         = Symbol -> Symbol
testSymbol Symbol
x
    raw :: Raw
raw        = Raw
"is-" Raw -> Raw -> Raw
forall a. Semigroup a => a -> a -> a
<> Symbol -> Raw
symbolRaw Symbol
x

symbolRaw :: Symbol -> Data.Text.Text
symbolRaw :: Symbol -> Raw
symbolRaw = Symbol -> Raw
symbolSafeText

--------------------------------------------------------------------------------
selectSymbols :: DataDecl -> [(Symbol, TheorySymbol)]
--------------------------------------------------------------------------------
selectSymbols :: DataDecl -> [(Symbol, TheorySymbol)]
selectSymbols DataDecl
d = (Symbol, Sort) -> (Symbol, TheorySymbol)
theorify ((Symbol, Sort) -> (Symbol, TheorySymbol))
-> [(Symbol, Sort)] -> [(Symbol, TheorySymbol)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (DataCtor -> [(Symbol, Sort)]) -> [DataCtor] -> [(Symbol, Sort)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (DataDecl -> DataCtor -> [(Symbol, Sort)]
ctorSelectors DataDecl
d) (DataDecl -> [DataCtor]
ddCtors DataDecl
d)

-- | 'theorify' converts the 'Sort' into a full 'TheorySymbol'
theorify :: (Symbol, Sort) -> (Symbol, TheorySymbol)
theorify :: (Symbol, Sort) -> (Symbol, TheorySymbol)
theorify (Symbol
x, Sort
t) = (Symbol
x, Symbol -> Raw -> Sort -> Sem -> TheorySymbol
Thy Symbol
x (Symbol -> Raw
symbolRaw Symbol
x) Sort
t Sem
Field)

ctorSelectors :: DataDecl -> DataCtor -> [(Symbol, Sort)]
ctorSelectors :: DataDecl -> DataCtor -> [(Symbol, Sort)]
ctorSelectors DataDecl
d DataCtor
ctor = DataDecl -> DataField -> (Symbol, Sort)
fieldSelector DataDecl
d (DataField -> (Symbol, Sort)) -> [DataField] -> [(Symbol, Sort)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DataCtor -> [DataField]
dcFields DataCtor
ctor

fieldSelector :: DataDecl -> DataField -> (Symbol, Sort)
fieldSelector :: DataDecl -> DataField -> (Symbol, Sort)
fieldSelector DataDecl
d DataField
f = (DataField -> Symbol
forall a. Symbolic a => a -> Symbol
symbol DataField
f, Int -> [Sort] -> Sort
mkFFunc Int
n [DataDecl -> Sort
selfSort DataDecl
d, Sort
ft])
  where
    ft :: Sort
ft            = DataDecl -> Sort -> Sort
fldSort DataDecl
d (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ DataField -> Sort
dfSort DataField
f
    n :: Int
n             = DataDecl -> Int
ddVars  DataDecl
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)])

-}