{-# LANGUAGE CPP                       #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings         #-}
{-# LANGUAGE UndecidableInstances      #-}
{-# LANGUAGE PatternGuards             #-}
{-# LANGUAGE ViewPatterns              #-}

{-# OPTIONS_GHC -Wno-orphans           #-}
{-# OPTIONS_GHC -Wno-name-shadowing    #-}

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, setCap, setSub, setAdd, setMem
     , setCom, setCup, setDif, setSng, mapSel, mapCup, mapSto, mapDef

      -- * Query Theories
     , isSmt2App
     , axiomLiterals
     , maxLamArg
     ) where

import           Prelude hiding (map)
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 qualified Data.Text.Lazy           as T
-- import           Data.Text.Format
import qualified Data.Text
import           Data.String                 (IsString(..))
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 ------------------------------------------------------------
--------------------------------------------------------------------------------

-- "set" is currently \"LSet\" instead of just \"Set\" because Z3 has its own
-- \"Set\" since 4.8.5
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, mprj :: Raw
mToSet, mshift, mmax, mmin :: 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"
mmax :: Raw
mmax  = Raw
"smt_map_max"
mmin :: Raw
mmin  = Raw
"smt_map_min"
mdef :: Raw
mdef  = Raw
"smt_map_def"
mprj :: Raw
mprj  = Raw
"smt_map_prj"
mshift :: Raw
mshift = Raw
"smt_map_shift"
mToSet :: Raw
mToSet = Raw
"smt_map_to_set"


setEmpty, setEmp, setCap, setSub, setAdd, setMem, setCom, setCup :: Symbol
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, mapPrj, mapToSet :: Symbol
mapMax, mapMin, mapShift :: Symbol
mapSel :: Symbol
mapSel   = Symbol
"Map_select"
mapSto :: Symbol
mapSto   = Symbol
"Map_store"
mapCup :: Symbol
mapCup   = Symbol
"Map_union"
mapMax :: Symbol
mapMax   = Symbol
"Map_union_max"
mapMin :: Symbol
mapMin   = Symbol
"Map_union_min"
mapDef :: Symbol
mapDef   = Symbol
"Map_default"
mapPrj :: Symbol
mapPrj   = Symbol
"Map_project"
mapShift :: Symbol
mapShift = Symbol
"Map_shift" -- See [Map key shift]
mapToSet :: Symbol
mapToSet = Symbol
"Map_to_set"

-- [Interaction between Map and Set]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- Function mapToSet: Convert a map to a set. The map's key may be of
-- any type and is preserved as the set's element type. More precisely:
--   mapToSet : Map k Int -> Set k
-- The element type must be Int. All non-positive elements are mapped
-- to False, and all positive elements are mapped to True. In practice,
-- negative elements should not exist because Map is intended to be used
-- as a bag, so the element is a non-negative number representing
-- the occurrences of its corresponding key.
--
-- Function mapPrj: Project a subset of a map. Type signature:
--   mapPrj : Set k -> Map k Int -> Map k Int
-- If the key is present in both the argument set and the argument map,
-- then the key (along with its associated value in the map) are preserved
-- in the output. Keys not present in the set are mapped to zero. Keys not
-- present in the set are mapped to zero.
--
-- [Map key shift]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- Function mapShift: Add an integer to all keys in a map. Type signature:
--   mapShift : Int -> Map Int v -> Map Int v
-- Let's call the first argument (the shift amount) N, the second argument K1,
-- and the result K2. For all indices i, we have K2[i] = K1[i - N].
-- This is implemented with Z3's lambda, which lets us construct an array
-- from a function.
--
-- [Map max and min]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- Functions mapMax and mapMin: Union two maps, combining the elements by
-- taking either the greatest (mapMax) or the least (mapMin) of them.
--   mapMax, mapMin : Map v Int -> Map v Int -> Map v Int

strLen, strSubstr, strConcat :: (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"

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 = 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 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 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 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 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"))

    -- Maps
    , 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
mprj -- See [Interaction Between Map and Set]
        [(Builder
"s", Raw -> Builder
bb Raw
set), (Builder
"m", Raw -> Builder
bb Raw
map)]
        (Raw -> Builder
bb Raw
map)
        (Builder -> Builder -> Builder -> Builder -> Builder
key3
          (Builder -> Builder -> Builder
key Builder
"_ map"
            (Builder -> Builder -> Builder -> Builder
key2 Builder
"ite"
              (Builder -> Builder
parens (Builder
"Bool" Builder -> Builder -> Builder
<+> Raw -> Builder
bb Raw
elt Builder -> Builder -> Builder
<+> Raw -> Builder
bb Raw
elt))
              (Raw -> Builder
bb Raw
elt)
            )
          )
          Builder
"s"
          Builder
"m"
          (Builder -> Builder
parens (Builder -> Builder -> Builder
key Builder
"as const" (Builder -> Builder -> Builder -> Builder
key2 Builder
"Array" (Raw -> Builder
bb Raw
elt) (Raw -> Builder
bb Raw
elt)) Builder -> Builder -> Builder
<+> Builder
"0"))
        )
    , Raw -> [(Builder, Builder)] -> Builder -> Builder -> Raw
bFun Raw
mToSet -- See [Interaction Between Map and Set]
        [(Builder
"m", Raw -> Builder
bb Raw
map)]
        (Raw -> Builder
bb Raw
set)
        (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))
              Builder
"Bool"
            )
          )
          Builder
"m"
          (Builder -> Builder
parens (Builder -> Builder -> Builder
key Builder
"as const" (Builder -> Builder -> Builder -> Builder
key2 Builder
"Array" (Raw -> Builder
bb Raw
elt) (Raw -> Builder
bb Raw
elt)) Builder -> Builder -> Builder
<+> Builder
"0"))
        )
    , Raw -> [(Builder, Builder)] -> Builder -> Builder -> Raw
bFun Raw
mmax -- See [Map max and min]
        [(Builder
"m1", Raw -> Builder
bb Raw
map),(Builder
"m2", Raw -> Builder
bb Raw
map)]
        (Raw -> Builder
bb Raw
map)
        Builder
"(lambda ((i Int)) (ite (> (select m1 i) (select m2 i)) (select m1 i) (select m2 i)))"
    , Raw -> [(Builder, Builder)] -> Builder -> Builder -> Raw
bFun Raw
mmin -- See [Map max and min]
        [(Builder
"m1", Raw -> Builder
bb Raw
map),(Builder
"m2", Raw -> Builder
bb Raw
map)]
        (Raw -> Builder
bb Raw
map)
        Builder
"(lambda ((i Int)) (ite (< (select m1 i) (select m2 i)) (select m1 i) (select m2 i)))"
    , Raw -> [(Builder, Builder)] -> Builder -> Builder -> Raw
bFun Raw
mshift -- See [Map key shift]
        [(Builder
"n", Builder
"Int"),(Builder
"m", Raw -> Builder
bb Raw
map)]
        (Raw -> Builder
bb Raw
map)
        Builder
"(lambda ((i Int)) (select m (- i n)))"
    , 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 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Text
symbolText

-- 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 -> 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 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)"]
  forall a. [a] -> [a] -> [a]
++ Config -> [Raw]
commonPreamble Config
z
  forall a. [a] -> [a] -> [a]
++ Config -> [Raw]
cvc4MapPreamble Config
z

commonPreamble :: Config -> [T.Text]
commonPreamble :: Config -> [Raw]
commonPreamble Config
_ --TODO use uif flag u (see z3Preamble)
  = [ 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 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 --TODO use uif flag u (see z3Preamble)
  = Config -> [Raw]
commonPreamble Config
z
 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 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 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 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' forall a. IsString a => a
strLen [Raw -> Builder
bb Raw
string] Builder
"Int"
    , Raw -> [Builder] -> Builder -> Raw
bFun' 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' forall a. IsString a => a
strConcat [Raw -> Builder
bb Raw
string, Raw -> Builder
bb Raw
string] (Raw -> Builder
bb Raw
string)
    ]

--------------------------------------------------------------------------------
-- | Exported API --------------------------------------------------------------
--------------------------------------------------------------------------------
smt2Symbol :: SymEnv -> Symbol -> Maybe Builder
smt2Symbol :: SymEnv -> Symbol -> Maybe Builder
smt2Symbol SymEnv
env Symbol
x = Raw -> Builder
fromLazyText forall b c a. (b -> c) -> (a -> b) -> a -> c
. TheorySymbol -> Raw
tsRaw 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" (forall a. Show a => a -> Builder
bShow Int
n)
smt2SmtSort (SVar Int
n)     = Builder
"T" forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> Builder
bShow Int
n
smt2SmtSort (SData FTycon
c []) = forall a. Symbolic a => a -> Builder
symbolBuilder FTycon
c
smt2SmtSort (SData FTycon
c [SmtSort]
ts) = [Builder] -> Builder
parenSeqs [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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
_ (Expr -> Expr
dropECst -> EVar Symbol
f) [Builder
d]
  | Symbol
f forall a. Eq a => a -> a -> Bool
== Symbol
setEmpty = forall a. a -> Maybe a
Just (Raw -> Builder
bb Raw
emp)
  | Symbol
f forall a. Eq a => a -> a -> Bool
== Symbol
setEmp   = forall a. a -> Maybe a
Just (Builder -> Builder -> Builder -> Builder
key2 Builder
"=" (Raw -> Builder
bb Raw
emp) Builder
d)
  | Symbol
f forall a. Eq a => a -> a -> Bool
== Symbol
setSng   = forall a. a -> Maybe a
Just (Builder -> Builder -> Builder
key (Raw -> Builder
bb Raw
sng) Builder
d) -- Just (key2 (bb add) (bb emp) 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
  = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Builder -> Builder -> Builder
key Builder
fb (Builder
d forall a. Semigroup a => a -> a -> a
<> forall a. Monoid a => [a] -> a
mconcat [ Builder
" " forall a. Semigroup a => a -> a -> a
<> Builder
d | Builder
d <- [Builder]
ds])

smt2App VarAs
_ SymEnv
_ Expr
_ [Builder]
_    = forall a. Maybe a
Nothing

smt2AppArg :: VarAs -> SymEnv -> Expr -> Maybe Builder
smt2AppArg :: VarAs -> SymEnv -> Expr -> Maybe Builder
smt2AppArg VarAs
k SymEnv
env (ECst (Expr -> Expr
dropECst -> EVar Symbol
f) Sort
t)
  | Just TheorySymbol
fThy <- Symbol -> SymEnv -> Maybe TheorySymbol
symEnvTheory Symbol
f SymEnv
env
  = forall a. a -> Maybe a
Just 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
_
  = 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 forall a. Eq a => a -> a -> Bool
== Sem
Ctor

ffuncOut :: Sort -> Sort
ffuncOut :: Sort -> Sort
ffuncOut Sort
t = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Sort
t (forall a. [a] -> a
last forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
f forall a. Eq a => a -> a -> Bool
== Symbol
setEmpty = forall a. a -> Maybe a
Just Int
1
  | Symbol
f forall a. Eq a => a -> a -> Bool
== Symbol
setEmp   = forall a. a -> Maybe a
Just Int
1
  | Symbol
f forall a. Eq a => a -> a -> Bool
== Symbol
setSng   = forall a. a -> Maybe a
Just Int
1
  | Bool
otherwise     = forall a. Symbol -> SEnv a -> Maybe a
lookupSEnv Symbol
f SEnv TheorySymbol
g forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= TheorySymbol -> Maybe Int
thyAppInfo
isSmt2App SEnv TheorySymbol
_ Expr
_     = 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    -> 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) -> forall a. a -> Maybe a
Just (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Sort]
ts forall a. Num a => a -> a -> a
- Int
1)
  Maybe (Int, [Sort])
Nothing      -> 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

--------------------------------------------------------------------------------
-- | 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.
--------------------------------------------------------------------------------

-- | `theorySymbols` contains the list of ALL SMT symbols with interpretations,
--   i.e. which are given via `define-fun` (as opposed to `declare-fun`)
theorySymbols :: [DataDecl] -> SEnv TheorySymbol -- M.HashMap Symbol TheorySymbol
theorySymbols :: [DataDecl] -> SEnv TheorySymbol
theorySymbols [DataDecl]
ds = forall a. [(Symbol, a)] -> SEnv a
fromListSEnv forall a b. (a -> b) -> a -> b
$  -- SHIFTLAM uninterpSymbols
                                  [(Symbol, TheorySymbol)]
interpSymbols
                               forall a. [a] -> [a] -> [a]
++ 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 forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort
setSort 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 forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
intSort (Sort -> Sort
setSort 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 forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
0) (Sort -> Sort
setSort 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
mapMax   Raw
mmax  Sort
mapMaxSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
mapMin   Raw
mmin  Sort
mapMinSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
mapDef   Raw
mdef  Sort
mapDefSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
mapPrj   Raw
mprj  Sort
mapPrjSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
mapShift Raw
mshift Sort
mapShiftSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym Symbol
mapToSet Raw
mToSet Sort
mapToSetSort
  , 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 forall a. IsString a => a
strLen    forall a. IsString a => a
strLen    Sort
strLenSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym forall a. IsString a => a
strSubstr forall a. IsString a => a
strSubstr Sort
substrSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym forall a. IsString a => a
strConcat forall a. IsString a => a
strConcat Sort
concatstrSort
  , Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
interpSym forall a. IsString a => a
boolInt   forall a. IsString a => a
boolInt   (Sort -> Sort -> Sort
FFunc Sort
boolSort Sort
intSort)
  ]
  where
    boolInt :: a
boolInt    = forall a. IsString a => a
boolToIntName
    setAddSort :: Sort
setAddSort = Int -> Sort -> Sort
FAbs Int
0 forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort
setSort forall a b. (a -> b) -> a -> b
$ Int -> Sort
FVar Int
0) forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
0)           (Sort -> Sort
setSort forall a b. (a -> b) -> a -> b
$ Int -> Sort
FVar Int
0)
    setBopSort :: Sort
setBopSort = Int -> Sort -> Sort
FAbs Int
0 forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort
setSort forall a b. (a -> b) -> a -> b
$ Int -> Sort
FVar Int
0) forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort
setSort forall a b. (a -> b) -> a -> b
$ Int -> Sort
FVar Int
0) (Sort -> Sort
setSort forall a b. (a -> b) -> a -> b
$ Int -> Sort
FVar Int
0)
    setMemSort :: Sort
setMemSort = Int -> Sort -> Sort
FAbs Int
0 forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
0) forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort
setSort forall a b. (a -> b) -> a -> b
$ Int -> Sort
FVar Int
0) Sort
boolSort
    setCmpSort :: Sort
setCmpSort = Int -> Sort -> Sort
FAbs Int
0 forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort
setSort forall a b. (a -> b) -> a -> b
$ Int -> Sort
FVar Int
0) forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort
setSort forall a b. (a -> b) -> a -> b
$ Int -> Sort
FVar Int
0) Sort
boolSort
    mapSelSort :: Sort
mapSelSort = Int -> Sort -> Sort
FAbs Int
0 forall a b. (a -> b) -> a -> b
$ Int -> Sort -> Sort
FAbs Int
1 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))
                                 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          forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort -> Sort
mapSort (Int -> Sort
FVar Int
0) Sort
intSort)
                                 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)
    mapMaxSort :: Sort
mapMaxSort = Sort
mapCupSort
    mapMinSort :: Sort
mapMinSort = Sort
mapCupSort
    mapPrjSort :: Sort
mapPrjSort = Int -> Sort -> Sort
FAbs Int
0          forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort
setSort (Int -> Sort
FVar Int
0))
                                 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)
    mapShiftSort :: Sort
mapShiftSort = Int -> Sort -> Sort
FAbs Int
0        forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc Sort
intSort
                                 forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort -> Sort
mapSort Sort
intSort (Int -> Sort
FVar Int
0))
                                         (Sort -> Sort -> Sort
mapSort Sort
intSort (Int -> Sort
FVar Int
0))
    mapToSetSort :: Sort
mapToSetSort = Int -> Sort -> Sort
FAbs Int
0        forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Sort -> Sort -> Sort
mapSort (Int -> Sort
FVar Int
0) Sort
intSort) (Sort -> Sort
setSort (Int -> Sort
FVar Int
0))
    mapStoSort :: Sort
mapStoSort = Int -> Sort -> Sort
FAbs Int
0 forall a b. (a -> b) -> a -> b
$ Int -> Sort -> Sort
FAbs Int
1 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))
                                 forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
FFunc (Int -> Sort
FVar Int
0)
                                 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 forall a b. (a -> b) -> a -> b
$ Int -> Sort -> Sort
FAbs Int
1 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 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 = forall a. [Maybe a] -> [a]
catMaybes [ forall {a} {a}. (Expression a, Expression a) => a -> a -> Expr
lenAxiom Symbol
l 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 (forall a. Expression a => a -> Expr
expr (forall a. IsString a => a
strLen :: Symbol)) (forall a. Expression a => a -> Expr
expr a
l)) (forall a. Expression a => a -> Expr
expr a
n Expr -> Sort -> Expr
`ECst` Sort
intSort)
    litLen :: Symbol -> Maybe Int
litLen        = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Text -> Int
Data.Text.length forall b c a. (b -> c) -> (a -> b) -> a -> c
.  Symbol -> Text
symbolText) 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 forall a. [a] -> [a] -> [a]
++ DataDecl -> [(Symbol, TheorySymbol)]
testSymbols DataDecl
d 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
0..(Int
nforall 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 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 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           = forall a. Symbolic a => a -> Symbol
symbol DataCtor
ctor
    t :: Sort
t           = Int -> [Sort] -> Sort
mkFFunc Int
n ([Sort]
ts 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataField -> Sort
dfSort 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Symbolic a => a -> Symbol
symbol 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-" forall a. Semigroup a => a -> a -> a
<> Symbol -> Raw
symbolRaw Symbol
x

symbolRaw :: Symbol -> T.Text
symbolRaw :: Symbol -> Raw
symbolRaw = Text -> Raw
T.fromStrict 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 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 = (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 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)])

-}