{-# LANGUAGE CPP                  #-}
{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE OverloadedStrings    #-}
{-# LANGUAGE PatternGuards        #-}
{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE DoAndIfThenElse      #-}

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

-- | This module contains the code for serializing Haskell values
--   into SMTLIB2 format, that is, the instances for the @SMTLIB2@
--   typeclass. We split it into a separate module as it depends on
--   Theories (see @smt2App@).

module Language.Fixpoint.Smt.Serialize (smt2SortMono) where

import           Data.ByteString.Builder (Builder)
import           Language.Fixpoint.SortCheck
import           Language.Fixpoint.Types
import qualified Language.Fixpoint.Types.Visitor as Vis
import           Language.Fixpoint.Smt.Types
import qualified Language.Fixpoint.Smt.Theories as Thy

-- import           Data.Text.Format
import           Language.Fixpoint.Misc (sortNub, errorstar)
import           Language.Fixpoint.Utils.Builder as Builder
-- import Debug.Trace (trace)

instance SMTLIB2 (Symbol, Sort) where
  smt2 :: SymEnv -> (Symbol, Sort) -> Builder
smt2 SymEnv
env c :: (Symbol, Sort)
c@(Symbol
sym, Sort
t) = -- build "({} {})" (smt2 env sym, smt2SortMono c env t)
                        [Builder] -> Builder
parenSeqs [forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Symbol
sym, forall a. PPrint a => a -> SymEnv -> Sort -> Builder
smt2SortMono (Symbol, Sort)
c SymEnv
env Sort
t]

smt2SortMono, smt2SortPoly :: (PPrint a) => a -> SymEnv -> Sort -> Builder
smt2SortMono :: forall a. PPrint a => a -> SymEnv -> Sort -> Builder
smt2SortMono = forall a. PPrint a => Bool -> a -> SymEnv -> Sort -> Builder
smt2Sort Bool
False
smt2SortPoly :: forall a. PPrint a => a -> SymEnv -> Sort -> Builder
smt2SortPoly = forall a. PPrint a => Bool -> a -> SymEnv -> Sort -> Builder
smt2Sort Bool
True

smt2Sort :: (PPrint a) => Bool -> a -> SymEnv -> Sort -> Builder
smt2Sort :: forall a. PPrint a => Bool -> a -> SymEnv -> Sort -> Builder
smt2Sort Bool
poly a
_ SymEnv
env Sort
t = forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env (Bool -> SEnv DataDecl -> Sort -> SmtSort
Thy.sortSmtSort Bool
poly (SymEnv -> SEnv DataDecl
seData SymEnv
env) Sort
t)

smt2data :: SymEnv -> [DataDecl] -> Builder
smt2data :: SymEnv -> [DataDecl] -> Builder
smt2data SymEnv
env = SymEnv -> [DataDecl] -> Builder
smt2data' SymEnv
env forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map DataDecl -> DataDecl
padDataDecl

smt2data' :: SymEnv -> [DataDecl] -> Builder
smt2data' :: SymEnv -> [DataDecl] -> Builder
smt2data' SymEnv
env [DataDecl]
ds = [Builder] -> Builder
seqs [ Builder -> Builder
parens forall a b. (a -> b) -> a -> b
$ [Builder] -> Builder
smt2many (SymEnv -> DataDecl -> Builder
smt2dataname SymEnv
env forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DataDecl]
ds)
                         , Builder -> Builder
parens forall a b. (a -> b) -> a -> b
$ [Builder] -> Builder
smt2many (SymEnv -> DataDecl -> Builder
smt2datactors SymEnv
env forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DataDecl]
ds)
                         ]


smt2dataname :: SymEnv -> DataDecl -> Builder
smt2dataname :: SymEnv -> DataDecl -> Builder
smt2dataname SymEnv
env (DDecl FTycon
tc Int
as [DataCtor]
_) = [Builder] -> Builder
parenSeqs [Builder
name, Builder
n]
  where
    name :: Builder
name  = forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env (forall a. Symbolic a => a -> Symbol
symbol FTycon
tc)
    n :: Builder
n     = forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Int
as


smt2datactors :: SymEnv -> DataDecl -> Builder
smt2datactors :: SymEnv -> DataDecl -> Builder
smt2datactors SymEnv
env (DDecl FTycon
_ Int
as [DataCtor]
cs) = [Builder] -> Builder
parenSeqs [Builder
"par", Builder -> Builder
parens Builder
tvars, Builder -> Builder
parens Builder
ds]
  where
    tvars :: Builder
tvars        = [Builder] -> Builder
smt2many (Int -> Builder
smt2TV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
0..(Int
asforall a. Num a => a -> a -> a
-Int
1)])
    smt2TV :: Int -> Builder
smt2TV       = forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> SmtSort
SVar
    ds :: Builder
ds           = [Builder] -> Builder
smt2many (SymEnv -> Int -> DataCtor -> Builder
smt2ctor SymEnv
env Int
as forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DataCtor]
cs)

smt2ctor :: SymEnv -> Int -> DataCtor -> Builder
smt2ctor :: SymEnv -> Int -> DataCtor -> Builder
smt2ctor SymEnv
env Int
_  (DCtor LocSymbol
c [])  = forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env LocSymbol
c
smt2ctor SymEnv
env Int
as (DCtor LocSymbol
c [DataField]
fs)  = [Builder] -> Builder
parenSeqs [forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env LocSymbol
c, Builder
fields]

  where
    fields :: Builder
fields                 = [Builder] -> Builder
smt2many (SymEnv -> Int -> DataField -> Builder
smt2field SymEnv
env Int
as forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DataField]
fs)

smt2field :: SymEnv -> Int -> DataField -> Builder
smt2field :: SymEnv -> Int -> DataField -> Builder
smt2field SymEnv
env Int
as d :: DataField
d@(DField LocSymbol
x Sort
t) = [Builder] -> Builder
parenSeqs [forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env LocSymbol
x, forall a. PPrint a => a -> SymEnv -> Sort -> Builder
smt2SortPoly DataField
d SymEnv
env forall a b. (a -> b) -> a -> b
$ Int -> Sort -> Sort
mkPoly Int
as Sort
t]

-- | SMTLIB/Z3 don't like "unused" type variables; they get pruned away and
--   cause wierd hassles. See tests/pos/adt_poly_dead.fq for an example.
--   'padDataDecl' adds a junk constructor that "uses" up all the tyvars just
--   to avoid this pruning problem.

padDataDecl :: DataDecl -> DataDecl
padDataDecl :: DataDecl -> DataDecl
padDataDecl d :: DataDecl
d@(DDecl FTycon
tc Int
n [DataCtor]
cs)
  | Bool
hasDead    = FTycon -> Int -> [DataCtor] -> DataDecl
DDecl FTycon
tc Int
n (FTycon -> Int -> DataCtor
junkDataCtor FTycon
tc Int
n forall a. a -> [a] -> [a]
: [DataCtor]
cs)
  | Bool
otherwise  = DataDecl
d
  where
    hasDead :: Bool
hasDead    = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
usedVars forall a. Ord a => a -> a -> Bool
< Int
n
    usedVars :: [Int]
usedVars   = DataDecl -> [Int]
declUsedVars DataDecl
d

junkDataCtor :: FTycon -> Int -> DataCtor
junkDataCtor :: FTycon -> Int -> DataCtor
junkDataCtor FTycon
c Int
n = LocSymbol -> [DataField] -> DataCtor
DCtor (forall l b. Loc l => l -> b -> Located b
atLoc FTycon
c Symbol
junkc) [LocSymbol -> Sort -> DataField
DField (forall {a}. Show a => a -> LocSymbol
junkFld Int
i) (Int -> Sort
FVar Int
i) | Int
i <- [Int
0..(Int
nforall a. Num a => a -> a -> a
-Int
1)]]
  where
    junkc :: Symbol
junkc        = Symbol -> Symbol -> Symbol
suffixSymbol Symbol
"junk" (forall a. Symbolic a => a -> Symbol
symbol FTycon
c)
    junkFld :: a -> LocSymbol
junkFld a
i    = forall l b. Loc l => l -> b -> Located b
atLoc FTycon
c    (forall a. Show a => Symbol -> a -> Symbol
intSymbol Symbol
junkc a
i)

declUsedVars :: DataDecl -> [Int]
declUsedVars :: DataDecl -> [Int]
declUsedVars = forall a. Ord a => [a] -> [a]
sortNub forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Sort -> a) -> a -> DataDecl -> a
Vis.foldDataDecl [Int] -> Sort -> [Int]
go []
  where
    go :: [Int] -> Sort -> [Int]
go [Int]
is (FVar Int
i) = Int
i forall a. a -> [a] -> [a]
: [Int]
is
    go [Int]
is Sort
_        = [Int]
is

instance SMTLIB2 Symbol where
  smt2 :: SymEnv -> Symbol -> Builder
smt2 SymEnv
env Symbol
s
    | Just Builder
t <- SymEnv -> Symbol -> Maybe Builder
Thy.smt2Symbol SymEnv
env Symbol
s = Builder
t
  smt2 SymEnv
_ Symbol
s                           = forall a. Symbolic a => a -> Builder
symbolBuilder Symbol
s

instance SMTLIB2 Int where
  smt2 :: SymEnv -> Int -> Builder
smt2 SymEnv
_ = forall a. IsString a => [Char] -> a
Builder.fromString forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show

instance SMTLIB2 LocSymbol where
  smt2 :: SymEnv -> LocSymbol -> Builder
smt2 SymEnv
env = forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Located a -> a
val

instance SMTLIB2 SymConst where
  smt2 :: SymEnv -> SymConst -> Builder
smt2 SymEnv
env = forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Symbolic a => a -> Symbol
symbol

instance SMTLIB2 Constant where
  smt2 :: SymEnv -> Constant -> Builder
smt2 SymEnv
_ (I Integer
n)   = forall a. Show a => a -> Builder
bShow Integer
n
  smt2 SymEnv
_ (R Double
d)   = forall a. RealFloat a => a -> Builder
bFloat Double
d
  smt2 SymEnv
_ (L Text
t Sort
_) = Text -> Builder
fromText Text
t

instance SMTLIB2 Bop where
  smt2 :: SymEnv -> Bop -> Builder
smt2 SymEnv
_ Bop
Plus   = Builder
"+"
  smt2 SymEnv
_ Bop
Minus  = Builder
"-"
  smt2 SymEnv
_ Bop
Times  = forall a. Symbolic a => a -> Builder
symbolBuilder Symbol
mulFuncName
  smt2 SymEnv
_ Bop
Div    = forall a. Symbolic a => a -> Builder
symbolBuilder Symbol
divFuncName
  smt2 SymEnv
_ Bop
RTimes = Builder
"*"
  smt2 SymEnv
_ Bop
RDiv   = Builder
"/"
  smt2 SymEnv
_ Bop
Mod    = Builder
"mod"

instance SMTLIB2 Brel where
  smt2 :: SymEnv -> Brel -> Builder
smt2 SymEnv
_ Brel
Eq    = Builder
"="
  smt2 SymEnv
_ Brel
Ueq   = Builder
"="
  smt2 SymEnv
_ Brel
Gt    = Builder
">"
  smt2 SymEnv
_ Brel
Ge    = Builder
">="
  smt2 SymEnv
_ Brel
Lt    = Builder
"<"
  smt2 SymEnv
_ Brel
Le    = Builder
"<="
  smt2 SymEnv
_ Brel
_     = forall a. (?callStack::CallStack) => [Char] -> a
errorstar [Char]
"SMTLIB2 Brel"

-- NV TODO: change the way EApp is printed
instance SMTLIB2 Expr where
  smt2 :: SymEnv -> Expr -> Builder
smt2 SymEnv
env (ESym SymConst
z)         = forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env SymConst
z
  smt2 SymEnv
env (ECon Constant
c)         = forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Constant
c
  smt2 SymEnv
env (EVar Symbol
x)         = forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Symbol
x
  smt2 SymEnv
env e :: Expr
e@(EApp Expr
_ Expr
_)     = SymEnv -> Expr -> Builder
smt2App SymEnv
env Expr
e
  smt2 SymEnv
env (ENeg Expr
e)         = [Builder] -> Builder
parenSeqs [Builder
"-", forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
e]
  smt2 SymEnv
env (EBin Bop
o Expr
e1 Expr
e2)   = [Builder] -> Builder
parenSeqs [forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Bop
o, forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
e1, forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
e2]
  smt2 SymEnv
env (EIte Expr
e1 Expr
e2 Expr
e3)  = [Builder] -> Builder
parenSeqs [Builder
"ite", forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
e1, forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
e2, forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
e3]
  smt2 SymEnv
env (ECst Expr
e Sort
t)       = SymEnv -> Expr -> Sort -> Builder
smt2Cast SymEnv
env Expr
e Sort
t
  smt2 SymEnv
_   Expr
PTrue            = Builder
"true"
  smt2 SymEnv
_   Expr
PFalse           = Builder
"false"
  smt2 SymEnv
_   (PAnd [])        = Builder
"true"
  smt2 SymEnv
env (PAnd [Expr]
ps)        = [Builder] -> Builder
parenSeqs [Builder
"and", forall a. SMTLIB2 a => SymEnv -> [a] -> Builder
smt2s SymEnv
env [Expr]
ps]
  smt2 SymEnv
_   (POr [])         = Builder
"false"
  smt2 SymEnv
env (POr [Expr]
ps)         = [Builder] -> Builder
parenSeqs [Builder
"or", forall a. SMTLIB2 a => SymEnv -> [a] -> Builder
smt2s SymEnv
env [Expr]
ps]
  smt2 SymEnv
env (PNot Expr
p)         = [Builder] -> Builder
parenSeqs [Builder
"not", forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2  SymEnv
env Expr
p]
  smt2 SymEnv
env (PImp Expr
p Expr
q)       = [Builder] -> Builder
parenSeqs [Builder
"=>", forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
p, forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
q]
  smt2 SymEnv
env (PIff Expr
p Expr
q)       = [Builder] -> Builder
parenSeqs [Builder
"=", forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
p, forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
q]
  smt2 SymEnv
env (PExist [] Expr
p)    = forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
p
  smt2 SymEnv
env (PExist [(Symbol, Sort)]
bs Expr
p)    = [Builder] -> Builder
parenSeqs [Builder
"exists", Builder -> Builder
parens (forall a. SMTLIB2 a => SymEnv -> [a] -> Builder
smt2s SymEnv
env [(Symbol, Sort)]
bs), forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
p]
  smt2 SymEnv
env (PAll   [] Expr
p)    = forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
p
  smt2 SymEnv
env (PAll   [(Symbol, Sort)]
bs Expr
p)    = [Builder] -> Builder
parenSeqs [Builder
"forall", Builder -> Builder
parens (forall a. SMTLIB2 a => SymEnv -> [a] -> Builder
smt2s SymEnv
env [(Symbol, Sort)]
bs), forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
p]
  smt2 SymEnv
env (PAtom Brel
r Expr
e1 Expr
e2)  = SymEnv -> Brel -> Expr -> Expr -> Builder
mkRel SymEnv
env Brel
r Expr
e1 Expr
e2
  smt2 SymEnv
env (ELam (Symbol, Sort)
b Expr
e)       = SymEnv -> (Symbol, Sort) -> Expr -> Builder
smt2Lam   SymEnv
env (Symbol, Sort)
b Expr
e
  smt2 SymEnv
env (ECoerc Sort
t1 Sort
t2 Expr
e) = SymEnv -> Sort -> Sort -> Expr -> Builder
smt2Coerc SymEnv
env Sort
t1 Sort
t2 Expr
e
  smt2 SymEnv
_   Expr
e                = forall a. [Char] -> a
panic ([Char]
"smtlib2 Pred  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Expr
e)



-- | smt2Cast uses the 'as x T' pattern needed for polymorphic ADT constructors
--   like Nil, see `tests/pos/adt_list_1.fq`

smt2Cast :: SymEnv -> Expr -> Sort -> Builder
smt2Cast :: SymEnv -> Expr -> Sort -> Builder
smt2Cast SymEnv
env (EVar Symbol
x) Sort
t = SymEnv -> Symbol -> Sort -> Builder
smt2Var SymEnv
env Symbol
x Sort
t
smt2Cast SymEnv
env Expr
e        Sort
_ = forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2    SymEnv
env Expr
e

smt2Var :: SymEnv -> Symbol -> Sort -> Builder
smt2Var :: SymEnv -> Symbol -> Sort -> Builder
smt2Var SymEnv
env Symbol
x Sort
t
  | Symbol -> Bool
isLamArgSymbol Symbol
x            = SymEnv -> Symbol -> Sort -> Builder
smtLamArg SymEnv
env Symbol
x Sort
t
  | Just Sort
s <- Symbol -> SymEnv -> Maybe Sort
symEnvSort Symbol
x SymEnv
env
  , Sort -> Sort -> Bool
isPolyInst Sort
s Sort
t              = SymEnv -> Symbol -> Sort -> Builder
smt2VarAs SymEnv
env Symbol
x Sort
t
  | Bool
otherwise                   = forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Symbol
x

smtLamArg :: SymEnv -> Symbol -> Sort -> Builder
smtLamArg :: SymEnv -> Symbol -> Sort -> Builder
smtLamArg SymEnv
env Symbol
x Sort
t = Text -> Builder
Builder.fromText forall a b. (a -> b) -> a -> b
$ forall a. PPrint a => Symbol -> SymEnv -> a -> Sort -> Text
symbolAtName Symbol
x SymEnv
env () (Sort -> Sort -> Sort
FFunc Sort
t Sort
FInt)

smt2VarAs :: SymEnv -> Symbol -> Sort -> Builder
smt2VarAs :: SymEnv -> Symbol -> Sort -> Builder
smt2VarAs SymEnv
env Symbol
x Sort
t = [Builder] -> Builder
parenSeqs [Builder
"as", forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Symbol
x, forall a. PPrint a => a -> SymEnv -> Sort -> Builder
smt2SortMono Symbol
x SymEnv
env Sort
t]

smt2Lam :: SymEnv -> (Symbol, Sort) -> Expr -> Builder
smt2Lam :: SymEnv -> (Symbol, Sort) -> Expr -> Builder
smt2Lam SymEnv
env (Symbol
x, Sort
xT) (ECst Expr
e Sort
eT) = [Builder] -> Builder
parenSeqs [Text -> Builder
Builder.fromText Text
lambda, Builder
x', forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
e]
  where
    x' :: Builder
x'                          = SymEnv -> Symbol -> Sort -> Builder
smtLamArg SymEnv
env Symbol
x Sort
xT
    lambda :: Text
lambda                      = forall a. PPrint a => Symbol -> SymEnv -> a -> Sort -> Text
symbolAtName Symbol
lambdaName SymEnv
env () (Sort -> Sort -> Sort
FFunc Sort
xT Sort
eT)

smt2Lam SymEnv
_ (Symbol, Sort)
_ Expr
e
  = forall a. [Char] -> a
panic ([Char]
"smtlib2: Cannot serialize unsorted lambda: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp Expr
e)

smt2App :: SymEnv -> Expr -> Builder
smt2App :: SymEnv -> Expr -> Builder
smt2App SymEnv
env e :: Expr
e@(EApp (EApp Expr
f Expr
e1) Expr
e2)
  | Just Sort
t <- Expr -> Maybe Sort
unApplyAt Expr
f
  = [Builder] -> Builder
parenSeqs [Text -> Builder
Builder.fromText (forall a. PPrint a => Symbol -> SymEnv -> a -> Sort -> Text
symbolAtName Symbol
applyName SymEnv
env Expr
e Sort
t), forall a. SMTLIB2 a => SymEnv -> [a] -> Builder
smt2s SymEnv
env [Expr
e1, Expr
e2]]
smt2App SymEnv
env Expr
e
  | Just Builder
b <- (SymEnv -> Symbol -> Sort -> Builder)
-> SymEnv -> Expr -> [Builder] -> Maybe Builder
Thy.smt2App SymEnv -> Symbol -> Sort -> Builder
smt2VarAs SymEnv
env Expr
f (forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es)
  = Builder
b
  | Bool
otherwise
  = [Builder] -> Builder
parenSeqs [forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
f, forall a. SMTLIB2 a => SymEnv -> [a] -> Builder
smt2s SymEnv
env [Expr]
es]
  where
    (Expr
f, [Expr]
es)   = Expr -> (Expr, [Expr])
splitEApp' Expr
e

smt2Coerc :: SymEnv -> Sort -> Sort -> Expr -> Builder
smt2Coerc :: SymEnv -> Sort -> Sort -> Expr -> Builder
smt2Coerc SymEnv
env Sort
t1 Sort
t2 Expr
e
  | Sort
t1 forall a. Eq a => a -> a -> Bool
== Sort
t2  = forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
e
  | Bool
otherwise = [Builder] -> Builder
parenSeqs [Text -> Builder
Builder.fromText Text
coerceFn , forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
e]
  where
    coerceFn :: Text
coerceFn  = forall a. PPrint a => Symbol -> SymEnv -> a -> Sort -> Text
symbolAtName Symbol
coerceName SymEnv
env (Sort -> Sort -> Expr -> Expr
ECoerc Sort
t1 Sort
t2 Expr
e) Sort
t
    t :: Sort
t         = Sort -> Sort -> Sort
FFunc Sort
t1 Sort
t2

splitEApp' :: Expr -> (Expr, [Expr])
splitEApp' :: Expr -> (Expr, [Expr])
splitEApp'            = [Expr] -> Expr -> (Expr, [Expr])
go []
  where
    go :: [Expr] -> Expr -> (Expr, [Expr])
go [Expr]
acc (EApp Expr
f Expr
e) = [Expr] -> Expr -> (Expr, [Expr])
go (Expr
eforall a. a -> [a] -> [a]
:[Expr]
acc) Expr
f
  --   go acc (ECst e _) = go acc e
    go [Expr]
acc Expr
e          = (Expr
e, [Expr]
acc)

mkRel :: SymEnv -> Brel -> Expr -> Expr -> Builder
mkRel :: SymEnv -> Brel -> Expr -> Expr -> Builder
mkRel SymEnv
env Brel
Ne  Expr
e1 Expr
e2 = SymEnv -> Expr -> Expr -> Builder
mkNe SymEnv
env Expr
e1 Expr
e2
mkRel SymEnv
env Brel
Une Expr
e1 Expr
e2 = SymEnv -> Expr -> Expr -> Builder
mkNe SymEnv
env Expr
e1 Expr
e2
mkRel SymEnv
env Brel
r   Expr
e1 Expr
e2 = [Builder] -> Builder
parenSeqs [forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Brel
r, forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
e1, forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
e2]

mkNe :: SymEnv -> Expr -> Expr -> Builder
mkNe :: SymEnv -> Expr -> Expr -> Builder
mkNe SymEnv
env Expr
e1 Expr
e2      = Builder -> Builder -> Builder
key Builder
"not" ([Builder] -> Builder
parenSeqs [Builder
"=",  forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
e1, forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
e2])

instance SMTLIB2 Command where
  smt2 :: SymEnv -> Command -> Builder
smt2 SymEnv
env (DeclData [DataDecl]
ds)       = Builder -> Builder -> Builder
key Builder
"declare-datatypes" (SymEnv -> [DataDecl] -> Builder
smt2data SymEnv
env [DataDecl]
ds)
  smt2 SymEnv
env (Declare Text
x [SmtSort]
ts SmtSort
t)    = [Builder] -> Builder
parenSeqs [Builder
"declare-fun", Text -> Builder
Builder.fromText Text
x, Builder -> Builder
parens ([Builder] -> Builder
smt2many (forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SmtSort]
ts)), forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env SmtSort
t]
  smt2 SymEnv
env c :: Command
c@(Define Sort
t)        = Builder -> Builder -> Builder
key Builder
"declare-sort" (forall a. PPrint a => a -> SymEnv -> Sort -> Builder
smt2SortMono Command
c SymEnv
env Sort
t)
  smt2 SymEnv
env (DefineFunc Symbol
name [(Symbol, SmtSort)]
params SmtSort
rsort Expr
e) =
    let bParams :: [Builder]
bParams = [ [Builder] -> Builder
parenSeqs [forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Symbol
s, forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env SmtSort
t] | (Symbol
s, SmtSort
t) <- [(Symbol, SmtSort)]
params]
     in [Builder] -> Builder
parenSeqs [Builder
"define-fun", forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Symbol
name, [Builder] -> Builder
parenSeqs [Builder]
bParams, forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env SmtSort
rsort, forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
e]
  smt2 SymEnv
env (Assert Maybe Int
Nothing Expr
p)  = {-# SCC "smt2-assert" #-} Builder -> Builder -> Builder
key Builder
"assert" (forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
p)
  smt2 SymEnv
env (Assert (Just Int
i) Expr
p) = {-# SCC "smt2-assert" #-} Builder -> Builder -> Builder
key Builder
"assert" (Builder -> Builder
parens (Builder
"!"Builder -> Builder -> Builder
<+> forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
p Builder -> Builder -> Builder
<+> Builder
":named p-" forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> Builder
bShow Int
i))
  smt2 SymEnv
env (Distinct [Expr]
az)
    | forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
az forall a. Ord a => a -> a -> Bool
< Int
2            = Builder
""
    | Bool
otherwise                = Builder -> Builder -> Builder
key Builder
"assert" (Builder -> Builder -> Builder
key Builder
"distinct" (forall a. SMTLIB2 a => SymEnv -> [a] -> Builder
smt2s SymEnv
env [Expr]
az))
  smt2 SymEnv
env (AssertAx Triggered Expr
t)        = Builder -> Builder -> Builder
key Builder
"assert" (forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Triggered Expr
t)
  smt2 SymEnv
_   Command
Push                = Builder
"(push 1)"
  smt2 SymEnv
_   Command
Pop                 = Builder
"(pop 1)"
  smt2 SymEnv
_   Command
CheckSat            = Builder
"(check-sat)"
  smt2 SymEnv
env (GetValue [Symbol]
xs)       = Builder -> Builder -> Builder
key Builder
"key-value" (Builder -> Builder
parens (forall a. SMTLIB2 a => SymEnv -> [a] -> Builder
smt2s SymEnv
env [Symbol]
xs))
  smt2 SymEnv
env (CMany [Command]
cmds)        = [Builder] -> Builder
smt2many (forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Command]
cmds)
  smt2 SymEnv
_   Command
Exit                = Builder
"(exit)"
  smt2 SymEnv
_   Command
SetMbqi             = Builder
"(set-option :smt.mbqi true)"

instance SMTLIB2 (Triggered Expr) where
  smt2 :: SymEnv -> Triggered Expr -> Builder
smt2 SymEnv
env (TR Trigger
NoTrigger Expr
e)       = forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
e
  smt2 SymEnv
env (TR Trigger
_ (PExist [] Expr
p))   = forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
p
  smt2 SymEnv
env t :: Triggered Expr
t@(TR Trigger
_ (PExist [(Symbol, Sort)]
bs Expr
p)) = SymEnv
-> Builder -> [(Symbol, Sort)] -> Expr -> Triggered Expr -> Builder
smtTr SymEnv
env Builder
"exists" [(Symbol, Sort)]
bs Expr
p Triggered Expr
t
  smt2 SymEnv
env (TR Trigger
_ (PAll   [] Expr
p))   = forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
p
  smt2 SymEnv
env t :: Triggered Expr
t@(TR Trigger
_ (PAll   [(Symbol, Sort)]
bs Expr
p)) = SymEnv
-> Builder -> [(Symbol, Sort)] -> Expr -> Triggered Expr -> Builder
smtTr SymEnv
env Builder
"forall" [(Symbol, Sort)]
bs Expr
p Triggered Expr
t
  smt2 SymEnv
env (TR Trigger
_ Expr
e)               = forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
e

{-# INLINE smtTr #-}
smtTr :: SymEnv -> Builder -> [(Symbol, Sort)] -> Expr -> Triggered Expr -> Builder
smtTr :: SymEnv
-> Builder -> [(Symbol, Sort)] -> Expr -> Triggered Expr -> Builder
smtTr SymEnv
env Builder
q [(Symbol, Sort)]
bs Expr
p Triggered Expr
t = Builder -> Builder -> Builder
key Builder
q (Builder -> Builder
parens (forall a. SMTLIB2 a => SymEnv -> [a] -> Builder
smt2s SymEnv
env [(Symbol, Sort)]
bs) Builder -> Builder -> Builder
<+> Builder -> Builder -> Builder
key Builder
"!" (forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
p Builder -> Builder -> Builder
<+> Builder
":pattern" forall a. Semigroup a => a -> a -> a
<> Builder -> Builder
parens (forall a. SMTLIB2 a => SymEnv -> [a] -> Builder
smt2s SymEnv
env (Triggered Expr -> [Expr]
makeTriggers Triggered Expr
t))))

{-# INLINE smt2s #-}
smt2s    :: SMTLIB2 a => SymEnv -> [a] -> Builder
smt2s :: forall a. SMTLIB2 a => SymEnv -> [a] -> Builder
smt2s SymEnv
env [a]
as = [Builder] -> Builder
smt2many (forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
as)

{-# INLINE smt2many #-}
smt2many :: [Builder] -> Builder
smt2many :: [Builder] -> Builder
smt2many = [Builder] -> Builder
seqs