{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE PatternGuards #-}
module Language.Fixpoint.Smt.Theories
(
smt2App
, sortSmtSort
, smt2Symbol
, preamble
, sizeBv
, theorySymbols
, dataDeclSymbols
, setEmpty, setEmp, setCap, setSub, setAdd, setMem
, setCom, setCup, setDif, setSng, mapSel, mapCup, mapSto, mapDef
, isSmt2App
, axiomLiterals
, maxLamArg
) where
import Prelude hiding (map)
#if !MIN_VERSION_base(4,14,0)
import Data.Semigroup (Semigroup (..))
#endif
import Language.Fixpoint.Types.Sorts
import Language.Fixpoint.Types.Config
import Language.Fixpoint.Types
import Language.Fixpoint.Smt.Types
import Data.Maybe (catMaybes)
import qualified Data.Text.Lazy as T
import qualified Data.Text
import Data.String (IsString(..))
import Language.Fixpoint.Utils.Builder
elt, set, map :: Raw
elt :: Raw
elt = Raw
"Elt"
set :: Raw
set = Raw
"LSet"
map :: Raw
map = Raw
"Map"
emp, sng, add, cup, cap, mem, dif, sub, com, sel, sto, mcup, mdef :: Raw
emp :: Raw
emp = Raw
"smt_set_emp"
sng :: Raw
sng = Raw
"smt_set_sng"
add :: Raw
add = Raw
"smt_set_add"
cup :: Raw
cup = Raw
"smt_set_cup"
cap :: Raw
cap = Raw
"smt_set_cap"
mem :: Raw
mem = Raw
"smt_set_mem"
dif :: Raw
dif = Raw
"smt_set_dif"
sub :: Raw
sub = Raw
"smt_set_sub"
com :: Raw
com = Raw
"smt_set_com"
sel :: Raw
sel = Raw
"smt_map_sel"
sto :: Raw
sto = Raw
"smt_map_sto"
mcup :: Raw
mcup = Raw
"smt_map_cup"
mdef :: Raw
mdef = Raw
"smt_map_def"
setEmpty, setEmp, setCap, setSub, setAdd, setMem, setCom, setCup, setDif, setSng :: Symbol
setEmpty :: Symbol
setEmpty = Symbol
"Set_empty"
setEmp :: Symbol
setEmp = Symbol
"Set_emp"
setCap :: Symbol
setCap = Symbol
"Set_cap"
setSub :: Symbol
setSub = Symbol
"Set_sub"
setAdd :: Symbol
setAdd = Symbol
"Set_add"
setMem :: Symbol
setMem = Symbol
"Set_mem"
setCom :: Symbol
setCom = Symbol
"Set_com"
setCup :: Symbol
setCup = Symbol
"Set_cup"
setDif :: Symbol
setDif = Symbol
"Set_dif"
setSng :: Symbol
setSng = Symbol
"Set_sng"
mapSel, mapSto, mapCup, mapDef :: Symbol
mapSel :: Symbol
mapSel = Symbol
"Map_select"
mapSto :: Symbol
mapSto = Symbol
"Map_store"
mapCup :: Symbol
mapCup = Symbol
"Map_union"
mapDef :: Symbol
mapDef = Symbol
"Map_default"
strLen, strSubstr, strConcat :: (IsString a) => a
strLen :: a
strLen = a
"strLen"
strSubstr :: a
strSubstr = a
"subString"
strConcat :: a
strConcat = a
"concatString"
z3strlen, z3strsubstr, z3strconcat :: Raw
z3strlen :: Raw
z3strlen = Raw
"str.len"
z3strsubstr :: Raw
z3strsubstr = Raw
"str.substr"
z3strconcat :: Raw
z3strconcat = Raw
"str.++"
strLenSort, substrSort, concatstrSort :: 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]
string :: Raw
string :: Raw
string = Raw
forall a. IsString a => a
strConName
bFun :: Raw -> [(Builder, Builder)] -> Builder -> Builder -> T.Text
bFun :: Raw -> [(Builder, Builder)] -> Builder -> Builder -> Raw
bFun Raw
name [(Builder, Builder)]
xts Builder
out Builder
body = Builder -> Raw
blt (Builder -> Raw) -> Builder -> Raw
forall a b. (a -> b) -> a -> b
$ Builder -> Builder -> Builder
key Builder
"define-fun" ([Builder] -> Builder
seqs [Raw -> Builder
bb 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 -> T.Text
bFun' :: Raw -> [Builder] -> Builder -> Raw
bFun' Raw
name [Builder]
ts Builder
out = Builder -> Raw
blt (Builder -> Raw) -> Builder -> Raw
forall a b. (a -> b) -> a -> b
$ Builder -> Builder -> Builder
key Builder
"declare-fun" ([Builder] -> Builder
seqs [Raw -> Builder
bb Raw
name, Builder
args, Builder
out])
where
args :: Builder
args = [Builder] -> Builder
parenSeqs [Builder]
ts
bSort :: Raw -> Builder -> T.Text
bSort :: Raw -> Builder -> Raw
bSort Raw
name Builder
def = Builder -> Raw
blt (Builder -> Raw) -> Builder -> Raw
forall a b. (a -> b) -> a -> b
$ Builder -> Builder -> Builder
key Builder
"define-sort" (Raw -> Builder
bb Raw
name Builder -> Builder -> Builder
<+> Builder
"()" Builder -> Builder -> Builder
<+> Builder
def)
z3Preamble :: Config -> [T.Text]
z3Preamble :: Config -> [Raw]
z3Preamble Config
u
= Config -> [Raw]
stringPreamble Config
u [Raw] -> [Raw] -> [Raw]
forall a. [a] -> [a] -> [a]
++
[ Raw -> Builder -> Raw
bSort Raw
elt
Builder
"Int"
, Raw -> Builder -> Raw
bSort Raw
set
(Builder -> Builder -> Builder -> Builder
key2 Builder
"Array" (Raw -> Builder
bb Raw
elt) Builder
"Bool")
, Raw -> [(Builder, Builder)] -> Builder -> Builder -> Raw
bFun Raw
emp
[]
(Raw -> Builder
bb Raw
set)
(Builder -> Builder
parens (Builder -> Builder -> Builder
key Builder
"as const" (Raw -> Builder
bb Raw
set) Builder -> Builder -> Builder
<+> Builder
"false"))
, Raw -> [(Builder, Builder)] -> Builder -> Builder -> Raw
bFun Raw
sng
[(Builder
"x", Raw -> Builder
bb Raw
elt)]
(Raw -> Builder
bb Raw
set)
(Builder -> Builder -> Builder -> Builder -> Builder
key3 Builder
"store" (Builder -> Builder
parens (Builder -> Builder -> Builder
key Builder
"as const" (Raw -> Builder
bb Raw
set) Builder -> Builder -> Builder
<+> Builder
"false")) Builder
"x" Builder
"true")
, Raw -> [(Builder, Builder)] -> Builder -> Builder -> Raw
bFun Raw
mem
[(Builder
"x", Raw -> Builder
bb Raw
elt), (Builder
"s", Raw -> Builder
bb Raw
set)]
Builder
"Bool"
Builder
"(select s x)"
, Raw -> [(Builder, Builder)] -> Builder -> Builder -> Raw
bFun Raw
add
[(Builder
"s", Raw -> Builder
bb Raw
set), (Builder
"x", Raw -> Builder
bb Raw
elt)]
(Raw -> Builder
bb Raw
set)
Builder
"(store s x true)"
, Raw -> [(Builder, Builder)] -> Builder -> Builder -> Raw
bFun Raw
cup
[(Builder
"s1", Raw -> Builder
bb Raw
set), (Builder
"s2", Raw -> Builder
bb Raw
set)]
(Raw -> Builder
bb Raw
set)
Builder
"((_ map or) s1 s2)"
, Raw -> [(Builder, Builder)] -> Builder -> Builder -> Raw
bFun Raw
cap
[(Builder
"s1", Raw -> Builder
bb Raw
set), (Builder
"s2", Raw -> Builder
bb Raw
set)]
(Raw -> Builder
bb Raw
set)
Builder
"((_ map and) s1 s2)"
, Raw -> [(Builder, Builder)] -> Builder -> Builder -> Raw
bFun Raw
com
[(Builder
"s", Raw -> Builder
bb Raw
set)]
(Raw -> Builder
bb Raw
set)
Builder
"((_ map not) s)"
, Raw -> [(Builder, Builder)] -> Builder -> Builder -> Raw
bFun Raw
dif
[(Builder
"s1", Raw -> Builder
bb Raw
set), (Builder
"s2", Raw -> Builder
bb Raw
set)]
(Raw -> Builder
bb Raw
set)
(Builder -> Builder -> Builder -> Builder
key2 (Raw -> Builder
bb Raw
cap) Builder
"s1" (Builder -> Builder -> Builder
key (Raw -> Builder
bb Raw
com) Builder
"s2"))
, Raw -> [(Builder, Builder)] -> Builder -> Builder -> Raw
bFun Raw
sub
[(Builder
"s1", Raw -> Builder
bb Raw
set), (Builder
"s2", Raw -> Builder
bb Raw
set)]
Builder
"Bool"
(Builder -> Builder -> Builder -> Builder
key2 Builder
"=" (Raw -> Builder
bb Raw
emp) (Builder -> Builder -> Builder -> Builder
key2 (Raw -> Builder
bb Raw
dif) Builder
"s1" Builder
"s2"))
, Raw -> Builder -> Raw
bSort Raw
map
(Builder -> Builder -> Builder -> Builder
key2 Builder
"Array" (Raw -> Builder
bb Raw
elt) (Raw -> Builder
bb Raw
elt))
, Raw -> [(Builder, Builder)] -> Builder -> Builder -> Raw
bFun Raw
sel
[(Builder
"m", Raw -> Builder
bb Raw
map), (Builder
"k", Raw -> Builder
bb Raw
elt)]
(Raw -> Builder
bb Raw
elt)
Builder
"(select m k)"
, Raw -> [(Builder, Builder)] -> Builder -> Builder -> Raw
bFun Raw
sto
[(Builder
"m", Raw -> Builder
bb Raw
map), (Builder
"k", Raw -> Builder
bb Raw
elt), (Builder
"v", Raw -> Builder
bb Raw
elt)]
(Raw -> Builder
bb Raw
map)
Builder
"(store m k v)"
, Raw -> [(Builder, Builder)] -> Builder -> Builder -> Raw
bFun Raw
mcup
[(Builder
"m1", Raw -> Builder
bb Raw
map), (Builder
"m2", Raw -> Builder
bb Raw
map)]
(Raw -> Builder
bb Raw
map)
(Builder -> Builder -> Builder -> Builder
key2 (Builder -> Builder -> Builder
key Builder
"_ map" (Builder -> Builder -> Builder -> Builder
key2 Builder
"+" (Builder -> Builder
parens (Raw -> Builder
bb Raw
elt Builder -> Builder -> Builder
<+> Raw -> Builder
bb Raw
elt)) (Raw -> Builder
bb Raw
elt))) Builder
"m1" Builder
"m2")
, Raw -> [(Builder, Builder)] -> Builder -> Builder -> Raw
bFun Raw
mdef
[(Builder
"v", Raw -> Builder
bb Raw
elt)]
(Raw -> Builder
bb Raw
map)
(Builder -> Builder -> Builder
key (Builder -> Builder -> Builder
key Builder
"as const" (Builder -> Builder
parens (Raw -> Builder
bb Raw
map))) Builder
"v")
, Raw -> [(Builder, Builder)] -> Builder -> Builder -> Raw
bFun Raw
forall a. IsString a => a
boolToIntName
[(Builder
"b", Builder
"Bool")]
Builder
"Int"
Builder
"(ite b 1 0)"
, Config -> Raw -> Raw -> Raw
uifDef Config
u (Symbol -> Raw
symbolLText Symbol
mulFuncName) Raw
"*"
, Config -> Raw -> Raw -> Raw
uifDef Config
u (Symbol -> Raw
symbolLText Symbol
divFuncName) Raw
"div"
]
symbolLText :: Symbol -> T.Text
symbolLText :: Symbol -> Raw
symbolLText = Text -> Raw
T.fromStrict (Text -> Raw) -> (Symbol -> Text) -> Symbol -> Raw
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Text
symbolText
uifDef :: Config -> T.Text -> T.Text -> T.Text
uifDef :: Config -> Raw -> Raw -> Raw
uifDef Config
cfg Raw
f Raw
op
| Config -> Bool
linear Config
cfg Bool -> Bool -> Bool
|| SMTSolver
Z3 SMTSolver -> SMTSolver -> Bool
forall a. Eq a => a -> a -> Bool
/= Config -> SMTSolver
solver Config
cfg
= Raw -> [Builder] -> Builder -> Raw
bFun' Raw
f [Builder
"Int", Builder
"Int"] Builder
"Int"
| Bool
otherwise
= Raw -> [(Builder, Builder)] -> Builder -> Builder -> Raw
bFun Raw
f [(Builder
"x", Builder
"Int"), (Builder
"y", Builder
"Int")] Builder
"Int" (Builder -> Builder -> Builder -> Builder
key2 (Raw -> Builder
bb Raw
op) Builder
"x" Builder
"y")
cvc4Preamble :: Config -> [T.Text]
cvc4Preamble :: Config -> [Raw]
cvc4Preamble Config
z
= [ Raw
"(set-logic ALL_SUPPORTED)"]
[Raw] -> [Raw] -> [Raw]
forall a. [a] -> [a] -> [a]
++ Config -> [Raw]
commonPreamble Config
z
[Raw] -> [Raw] -> [Raw]
forall a. [a] -> [a] -> [a]
++ Config -> [Raw]
cvc4MapPreamble Config
z
commonPreamble :: Config -> [T.Text]
commonPreamble :: Config -> [Raw]
commonPreamble Config
_
= [ Raw -> Builder -> Raw
bSort Raw
elt Builder
"Int"
, Raw -> Builder -> Raw
bSort Raw
set Builder
"Int"
, Raw -> Builder -> Raw
bSort Raw
string Builder
"Int"
, Raw -> [Builder] -> Builder -> Raw
bFun' Raw
emp [] (Raw -> Builder
bb Raw
set)
, Raw -> [Builder] -> Builder -> Raw
bFun' Raw
sng [Raw -> Builder
bb Raw
elt] (Raw -> Builder
bb Raw
set)
, Raw -> [Builder] -> Builder -> Raw
bFun' Raw
add [Raw -> Builder
bb Raw
set, Raw -> Builder
bb Raw
elt] (Raw -> Builder
bb Raw
set)
, Raw -> [Builder] -> Builder -> Raw
bFun' Raw
cup [Raw -> Builder
bb Raw
set, Raw -> Builder
bb Raw
set] (Raw -> Builder
bb Raw
set)
, Raw -> [Builder] -> Builder -> Raw
bFun' Raw
cap [Raw -> Builder
bb Raw
set, Raw -> Builder
bb Raw
set] (Raw -> Builder
bb Raw
set)
, Raw -> [Builder] -> Builder -> Raw
bFun' Raw
dif [Raw -> Builder
bb Raw
set, Raw -> Builder
bb Raw
set] (Raw -> Builder
bb Raw
set)
, Raw -> [Builder] -> Builder -> Raw
bFun' Raw
sub [Raw -> Builder
bb Raw
set, Raw -> Builder
bb Raw
set] Builder
"Bool"
, Raw -> [Builder] -> Builder -> Raw
bFun' Raw
mem [Raw -> Builder
bb Raw
elt, Raw -> Builder
bb Raw
set] Builder
"Bool"
, Raw -> [(Builder, Builder)] -> Builder -> Builder -> Raw
bFun Raw
forall a. IsString a => a
boolToIntName [(Builder
"b", Builder
"Bool")] Builder
"Int" Builder
"(ite b 1 0)"
]
cvc4MapPreamble :: Config -> [T.Text]
cvc4MapPreamble :: Config -> [Raw]
cvc4MapPreamble Config
_ =
[ Raw -> Builder -> Raw
bSort Raw
map (Builder -> Builder -> Builder -> Builder
key2 Builder
"Array" (Raw -> Builder
bb Raw
elt) (Raw -> Builder
bb Raw
elt))
, Raw -> [(Builder, Builder)] -> Builder -> Builder -> Raw
bFun Raw
sel [(Builder
"m", Raw -> Builder
bb Raw
map), (Builder
"k", Raw -> Builder
bb Raw
elt)] (Raw -> Builder
bb Raw
elt) Builder
"(select m k)"
, Raw -> [(Builder, Builder)] -> Builder -> Builder -> Raw
bFun Raw
sto [(Builder
"m", Raw -> Builder
bb Raw
map), (Builder
"k", Raw -> Builder
bb Raw
elt), (Builder
"v", Raw -> Builder
bb Raw
elt)] (Raw -> Builder
bb Raw
map) Builder
"(store m k v)"
]
smtlibPreamble :: Config -> [T.Text]
smtlibPreamble :: Config -> [Raw]
smtlibPreamble Config
z
= Config -> [Raw]
commonPreamble Config
z
[Raw] -> [Raw] -> [Raw]
forall a. [a] -> [a] -> [a]
++ [ Raw -> Builder -> Raw
bSort Raw
map Builder
"Int"
, Raw -> [Builder] -> Builder -> Raw
bFun' Raw
sel [Raw -> Builder
bb Raw
map, Raw -> Builder
bb Raw
elt] (Raw -> Builder
bb Raw
elt)
, Raw -> [Builder] -> Builder -> Raw
bFun' Raw
sto [Raw -> Builder
bb Raw
map, Raw -> Builder
bb Raw
elt, Raw -> Builder
bb Raw
elt] (Raw -> Builder
bb Raw
map)
]
stringPreamble :: Config -> [T.Text]
stringPreamble :: Config -> [Raw]
stringPreamble Config
cfg | Config -> Bool
stringTheory Config
cfg
= [ Raw -> Builder -> Raw
bSort Raw
string Builder
"String"
, Raw -> [(Builder, Builder)] -> Builder -> Builder -> Raw
bFun Raw
forall a. IsString a => a
strLen [(Builder
"s", Raw -> Builder
bb Raw
string)] Builder
"Int" (Builder -> Builder -> Builder
key (Raw -> Builder
bb Raw
z3strlen) Builder
"s")
, Raw -> [(Builder, Builder)] -> Builder -> Builder -> Raw
bFun Raw
forall a. IsString a => a
strSubstr [(Builder
"s", Raw -> Builder
bb Raw
string), (Builder
"i", Builder
"Int"), (Builder
"j", Builder
"Int")] (Raw -> Builder
bb Raw
string) (Builder -> Builder -> Builder
key (Raw -> Builder
bb Raw
z3strsubstr) Builder
"s i j")
, Raw -> [(Builder, Builder)] -> Builder -> Builder -> Raw
bFun Raw
forall a. IsString a => a
strConcat [(Builder
"x", Raw -> Builder
bb Raw
string), (Builder
"y", Raw -> Builder
bb Raw
string)] (Raw -> Builder
bb Raw
string) (Builder -> Builder -> Builder
key (Raw -> Builder
bb Raw
z3strconcat) Builder
"x y")
]
stringPreamble Config
_
= [ Raw -> Builder -> Raw
bSort Raw
string Builder
"Int"
, Raw -> [Builder] -> Builder -> Raw
bFun' Raw
forall a. IsString a => a
strLen [Raw -> Builder
bb Raw
string] Builder
"Int"
, Raw -> [Builder] -> Builder -> Raw
bFun' Raw
forall a. IsString a => a
strSubstr [Raw -> Builder
bb Raw
string, Builder
"Int", Builder
"Int"] (Raw -> Builder
bb Raw
string)
, Raw -> [Builder] -> Builder -> Raw
bFun' Raw
forall a. IsString a => a
strConcat [Raw -> Builder
bb Raw
string, Raw -> Builder
bb Raw
string] (Raw -> Builder
bb Raw
string)
]
smt2Symbol :: SymEnv -> Symbol -> Maybe Builder
smt2Symbol :: SymEnv -> Symbol -> Maybe Builder
smt2Symbol SymEnv
env Symbol
x = Raw -> Builder
fromLazyText (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 :: SymEnv -> SmtSort -> Builder
smt2 SymEnv
_ = SmtSort -> Builder
smt2SmtSort
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
bb Raw
string
smt2SmtSort SmtSort
SSet = Raw -> Builder
bb Raw
set
smt2SmtSort SmtSort
SMap = Raw -> Builder
bb Raw
map
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]
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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SmtSort -> Builder
smt2SmtSort
type VarAs = SymEnv -> Symbol -> Sort -> Builder
smt2App :: VarAs -> SymEnv -> Expr -> [Builder] -> Maybe Builder
smt2App :: VarAs -> SymEnv -> Expr -> [Builder] -> Maybe Builder
smt2App VarAs
_ SymEnv
_ (ECst (EVar Symbol
f) Sort
_) [Builder
d]
| Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
setEmpty = Builder -> Maybe Builder
forall a. a -> Maybe a
Just (Raw -> Builder
bb Raw
emp)
| Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
setEmp = Builder -> Maybe Builder
forall a. a -> Maybe a
Just (Builder -> Builder -> Builder -> Builder
key2 Builder
"=" (Raw -> Builder
bb Raw
emp) Builder
d)
| Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
setSng = Builder -> Maybe Builder
forall a. a -> Maybe a
Just (Builder -> Builder -> Builder
key (Raw -> Builder
bb Raw
sng) Builder
d)
smt2App VarAs
k SymEnv
env Expr
f (Builder
d:[Builder]
ds)
| Just Builder
fb <- VarAs -> SymEnv -> Expr -> Maybe Builder
smt2AppArg VarAs
k SymEnv
env Expr
f
= 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
fb (Builder
d 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]
ds])
smt2App VarAs
_ SymEnv
_ Expr
_ [Builder]
_ = Maybe Builder
forall a. Maybe a
Nothing
smt2AppArg :: VarAs -> SymEnv -> Expr -> Maybe Builder
smt2AppArg :: VarAs -> SymEnv -> Expr -> Maybe Builder
smt2AppArg VarAs
k SymEnv
env (ECst (EVar Symbol
f) Sort
t)
| Just TheorySymbol
fThy <- Symbol -> SymEnv -> Maybe TheorySymbol
symEnvTheory Symbol
f SymEnv
env
= Builder -> Maybe Builder
forall a. a -> Maybe a
Just (Builder -> Maybe Builder) -> Builder -> Maybe Builder
forall a b. (a -> b) -> a -> b
$ if TheorySymbol -> Sort -> Bool
isPolyCtor TheorySymbol
fThy Sort
t
then (VarAs
k SymEnv
env Symbol
f (Sort -> Sort
ffuncOut Sort
t))
else Raw -> Builder
bb (TheorySymbol -> Raw
tsRaw TheorySymbol
fThy)
smt2AppArg VarAs
_ SymEnv
_ Expr
_
= 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. [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 (EVar Symbol
f)
| Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
setEmpty = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
1
| Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
setEmp = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
1
| Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
setSng = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
1
| Bool
otherwise = 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 (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 (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
preamble :: Config -> SMTSolver -> [T.Text]
preamble :: Config -> SMTSolver -> [Raw]
preamble Config
u SMTSolver
Z3 = Config -> [Raw]
z3Preamble Config
u
preamble Config
u SMTSolver
Cvc4 = Config -> [Raw]
cvc4Preamble Config
u
preamble Config
u SMTSolver
_ = Config -> [Raw]
smtlibPreamble Config
u
theorySymbols :: [DataDecl] -> SEnv TheorySymbol
theorySymbols :: [DataDecl] -> SEnv TheorySymbol
theorySymbols [DataDecl]
ds = [(Symbol, TheorySymbol)] -> SEnv TheorySymbol
forall a. [(Symbol, a)] -> SEnv a
fromListSEnv ([(Symbol, TheorySymbol)] -> SEnv TheorySymbol)
-> [(Symbol, TheorySymbol)] -> SEnv TheorySymbol
forall a b. (a -> b) -> a -> b
$
[(Symbol, TheorySymbol)]
interpSymbols
[(Symbol, TheorySymbol)]
-> [(Symbol, TheorySymbol)] -> [(Symbol, TheorySymbol)]
forall a. [a] -> [a] -> [a]
++ (DataDecl -> [(Symbol, TheorySymbol)])
-> [DataDecl] -> [(Symbol, TheorySymbol)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap DataDecl -> [(Symbol, TheorySymbol)]
dataDeclSymbols [DataDecl]
ds
interpSymbols :: [(Symbol, TheorySymbol)]
interpSymbols :: [(Symbol, TheorySymbol)]
interpSymbols =
[ Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
setEmp Raw
emp (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
setEmpty Raw
emp (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
setSng Raw
sng (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
setAdd Raw
add Sort
setAddSort
, Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
setCup Raw
cup Sort
setBopSort
, Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
setCap Raw
cap Sort
setBopSort
, Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
setMem Raw
mem Sort
setMemSort
, Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
setDif Raw
dif Sort
setBopSort
, Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
setSub Raw
sub Sort
setCmpSort
, Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
setCom Raw
com Sort
setCmpSort
, Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
mapSel Raw
sel Sort
mapSelSort
, Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
mapSto Raw
sto Sort
mapStoSort
, Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
mapCup Raw
mcup Sort
mapCupSort
, Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
mapDef Raw
mdef Sort
mapDefSort
, Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
bvOrName Raw
"bvor" Sort
bvBopSort
, Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
bvAndName Raw
"bvand" Sort
bvBopSort
, 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
boolInt Raw
forall a. IsString a => a
boolInt (Sort -> Sort -> Sort
FFunc Sort
boolSort Sort
intSort)
]
where
boolInt :: a
boolInt = a
forall a. IsString a => a
boolToIntName
setAddSort :: Sort
setAddSort = 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 (Int -> Sort
FVar Int
0) (Sort -> Sort
setSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort
FVar Int
0)
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)
setMemSort :: Sort
setMemSort = 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
setCmpSort :: Sort
setCmpSort = 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
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)
mapCupSort :: Sort
mapCupSort = Int -> Sort -> Sort
FAbs Int
0 (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort -> Sort
mapSort (Int -> Sort
FVar Int
0) Sort
intSort)
(Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort -> Sort
mapSort (Int -> Sort
FVar Int
0) Sort
intSort)
(Sort -> Sort -> Sort
mapSort (Int -> Sort
FVar Int
0) Sort
intSort)
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))
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))
bvBopSort :: Sort
bvBopSort = Sort -> Sort -> Sort
FFunc Sort
bitVecSort (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
bitVecSort Sort
bitVecSort
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)
maxLamArg :: Int
maxLamArg :: Int
maxLamArg = Int
7
axiomLiterals :: [(Symbol, Sort)] -> [Expr]
axiomLiterals :: [(Symbol, Sort)] -> [Expr]
axiomLiterals [(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
EEq (Expr -> Expr -> Expr
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
`ECst` Sort
intSort)
litLen :: Symbol -> Maybe Int
litLen = (Symbol -> Int) -> Maybe Symbol -> Maybe Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Text -> Int
Data.Text.length (Text -> Int) -> (Symbol -> Text) -> Symbol -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Text
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
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 :: 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 :: 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 -> T.Text
symbolRaw :: Symbol -> Raw
symbolRaw = Text -> Raw
T.fromStrict (Text -> Raw) -> (Symbol -> Text) -> Symbol -> Raw
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Text
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 :: (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