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

-- | 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           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
#if !MIN_VERSION_base(4,14,0)
import           Data.Semigroup                 (Semigroup (..))
#endif

import qualified Data.Text.Lazy.Builder         as Builder
import           Data.Text.Format
import           Language.Fixpoint.Misc (sortNub, errorstar)
-- 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) = Format -> (Builder, Builder) -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"({} {})" (SymEnv -> Symbol -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Symbol
sym, (Symbol, Sort) -> SymEnv -> Sort -> Builder
forall a. PPrint a => a -> SymEnv -> Sort -> Builder
smt2SortMono (Symbol, Sort)
c SymEnv
env Sort
t)

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

smt2Sort :: (PPrint a) => Bool -> a -> SymEnv -> Sort -> Builder.Builder
smt2Sort :: Bool -> a -> SymEnv -> Sort -> Builder
smt2Sort Bool
poly a
_ SymEnv
env Sort
t = SymEnv -> SmtSort -> Builder
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.Builder
smt2data :: SymEnv -> [DataDecl] -> Builder
smt2data SymEnv
env = SymEnv -> [DataDecl] -> Builder
smt2data' SymEnv
env ([DataDecl] -> Builder)
-> ([DataDecl] -> [DataDecl]) -> [DataDecl] -> Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DataDecl -> DataDecl) -> [DataDecl] -> [DataDecl]
forall a b. (a -> b) -> [a] -> [b]
map DataDecl -> DataDecl
padDataDecl

smt2data' :: SymEnv -> [DataDecl] -> Builder.Builder
smt2data' :: SymEnv -> [DataDecl] -> Builder
smt2data' SymEnv
env [DataDecl]
ds = Format -> (Builder, Builder) -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"({}) ({})" ([Builder] -> Builder
smt2many (SymEnv -> DataDecl -> Builder
smt2dataname SymEnv
env (DataDecl -> Builder) -> [DataDecl] -> [Builder]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DataDecl]
ds), [Builder] -> Builder
smt2many (SymEnv -> DataDecl -> Builder
smt2datactors SymEnv
env (DataDecl -> Builder) -> [DataDecl] -> [Builder]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DataDecl]
ds))
 
smt2dataname :: SymEnv -> DataDecl -> Builder.Builder
smt2dataname :: SymEnv -> DataDecl -> Builder
smt2dataname SymEnv
env (DDecl FTycon
tc Int
as [DataCtor]
_) = Format -> (Builder, Builder) -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"({} {})" (Builder
name, Builder
n)
  where
    name :: Builder
name  = SymEnv -> Symbol -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env (FTycon -> Symbol
forall a. Symbolic a => a -> Symbol
symbol FTycon
tc)
    n :: Builder
n     = SymEnv -> Int -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Int
as 


smt2datactors :: SymEnv -> DataDecl -> Builder.Builder
smt2datactors :: SymEnv -> DataDecl -> Builder
smt2datactors SymEnv
env (DDecl FTycon
_ Int
as [DataCtor]
cs) = Format -> (Builder, Builder) -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"(par ({}) ({}))" (Builder
tvars,Builder
ds) 
  where
    tvars :: Builder
tvars        = [Builder] -> Builder
smt2many (Int -> Builder
smt2TV (Int -> Builder) -> [Int] -> [Builder]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
0..(Int
asInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)])
    smt2TV :: Int -> Builder
smt2TV       = SymEnv -> SmtSort -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env (SmtSort -> Builder) -> (Int -> SmtSort) -> Int -> Builder
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 (DataCtor -> Builder) -> [DataCtor] -> [Builder]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DataCtor]
cs) 

{- 
smt2data' :: SymEnv -> DataDecl -> Builder.Builder
smt2data' env (DDecl tc n cs) = build "({}) (({} {}))" (tvars, name, ctors)
  where
    tvars                    = smt2many (smt2TV <$> [0..(n-1)])
    name                     = smt2 env (symbol tc)
    ctors                    = smt2many (smt2ctor env <$> cs)
    smt2TV                   = smt2 env . SVar
-}

{- 
    (declare-datatypes (T) ((Tree leaf (node (value T) (children TreeList)))
    (TreeList nil (cons (car Tree) (cdr TreeList)))))
-}

smt2ctor :: SymEnv -> Int -> DataCtor -> Builder.Builder
smt2ctor :: SymEnv -> Int -> DataCtor -> Builder
smt2ctor SymEnv
env Int
_  (DCtor LocSymbol
c [])  = SymEnv -> LocSymbol -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env LocSymbol
c
smt2ctor SymEnv
env Int
as (DCtor LocSymbol
c [DataField]
fs)  = Format -> (Builder, Builder) -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"({} {})" (SymEnv -> LocSymbol -> Builder
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 (DataField -> Builder) -> [DataField] -> [Builder]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DataField]
fs)

smt2field :: SymEnv -> Int -> DataField -> Builder.Builder
smt2field :: SymEnv -> Int -> DataField -> Builder
smt2field SymEnv
env Int
as d :: DataField
d@(DField LocSymbol
x Sort
t) = Format -> (Builder, Builder) -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"({} {})" (SymEnv -> LocSymbol -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env LocSymbol
x, DataField -> SymEnv -> Sort -> Builder
forall a. PPrint a => a -> SymEnv -> Sort -> Builder
smt2SortPoly DataField
d SymEnv
env (Sort -> Builder) -> Sort -> Builder
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 DataCtor -> [DataCtor] -> [DataCtor]
forall a. a -> [a] -> [a]
: [DataCtor]
cs)
  | Bool
otherwise  = DataDecl
d
  where
    hasDead :: Bool
hasDead    = [Int] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
usedVars Int -> Int -> Bool
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 (FTycon -> Symbol -> LocSymbol
forall l b. Loc l => l -> b -> Located b
atLoc FTycon
c Symbol
junkc) [LocSymbol -> Sort -> DataField
DField (Int -> LocSymbol
forall a. Show a => a -> LocSymbol
junkFld Int
i) (Int -> Sort
FVar Int
i) | Int
i <- [Int
0..(Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)]]
  where
    junkc :: Symbol
junkc        = Symbol -> Symbol -> Symbol
suffixSymbol Symbol
"junk" (FTycon -> Symbol
forall a. Symbolic a => a -> Symbol
symbol FTycon
c)
    junkFld :: a -> LocSymbol
junkFld a
i    = FTycon -> Symbol -> LocSymbol
forall l b. Loc l => l -> b -> Located b
atLoc FTycon
c    (Symbol -> a -> Symbol
forall a. Show a => Symbol -> a -> Symbol
intSymbol Symbol
junkc a
i)

declUsedVars :: DataDecl -> [Int]
declUsedVars :: DataDecl -> [Int]
declUsedVars = [Int] -> [Int]
forall a. Ord a => [a] -> [a]
sortNub ([Int] -> [Int]) -> (DataDecl -> [Int]) -> DataDecl -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Int] -> Sort -> [Int]) -> [Int] -> DataDecl -> [Int]
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 Int -> [Int] -> [Int]
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                           = Symbol -> Builder
forall a. Symbolic a => a -> Builder
symbolBuilder Symbol
s

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

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

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

instance SMTLIB2 Constant where
  smt2 :: SymEnv -> Constant -> Builder
smt2 SymEnv
_ (I Integer
n)   = Format -> Only Integer -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"{}" (Integer -> Only Integer
forall a. a -> Only a
Only Integer
n)
  smt2 SymEnv
_ (R Double
d)   = Format -> Only Double -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"{}" (Double -> Only Double
forall a. a -> Only a
Only Double
d)
  smt2 SymEnv
_ (L Text
t Sort
_) = Format -> Only Text -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"{}" (Text -> Only Text
forall a. a -> Only a
Only Text
t)


instance SMTLIB2 Bop where
  smt2 :: SymEnv -> Bop -> Builder
smt2 SymEnv
_ Bop
Plus   = Builder
"+"
  smt2 SymEnv
_ Bop
Minus  = Builder
"-"
  smt2 SymEnv
_ Bop
Times  = Symbol -> Builder
forall a. Symbolic a => a -> Builder
symbolBuilder Symbol
mulFuncName
  smt2 SymEnv
_ Bop
Div    = Symbol -> Builder
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
_     = String -> Builder
forall a. (?callStack::CallStack) => String -> a
errorstar String
"SMTLIB2 Brel"

-- NV TODO: change the way EApp is printed
instance SMTLIB2 Expr where
  smt2 :: SymEnv -> Expr -> Builder
smt2 SymEnv
env (ESym SymConst
z)         = SymEnv -> SymConst -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env SymConst
z
  smt2 SymEnv
env (ECon Constant
c)         = SymEnv -> Constant -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Constant
c
  smt2 SymEnv
env (EVar Symbol
x)         = SymEnv -> Symbol -> Builder
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)         = Format -> Only Builder -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"(- {})" (Builder -> Only Builder
forall a. a -> Only a
Only (Builder -> Only Builder) -> Builder -> Only Builder
forall a b. (a -> b) -> a -> b
$ SymEnv -> Expr -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
e)
  smt2 SymEnv
env (EBin Bop
o Expr
e1 Expr
e2)   = Format -> (Builder, Builder, Builder) -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"({} {} {})" (SymEnv -> Bop -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Bop
o, SymEnv -> Expr -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
e1, SymEnv -> Expr -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
e2)
  smt2 SymEnv
env (EIte Expr
e1 Expr
e2 Expr
e3)  = Format -> (Builder, Builder, Builder) -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"(ite {} {} {})" (SymEnv -> Expr -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
e1, SymEnv -> Expr -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
e2, SymEnv -> Expr -> Builder
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)        = Format -> Only Builder -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"(and {})"   (Builder -> Only Builder
forall a. a -> Only a
Only (Builder -> Only Builder) -> Builder -> Only Builder
forall a b. (a -> b) -> a -> b
$ SymEnv -> [Expr] -> Builder
forall a. SMTLIB2 a => SymEnv -> [a] -> Builder
smt2s SymEnv
env [Expr]
ps)
  smt2 SymEnv
_   (POr [])         = Builder
"false"
  smt2 SymEnv
env (POr [Expr]
ps)         = Format -> Only Builder -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"(or  {})"   (Builder -> Only Builder
forall a. a -> Only a
Only (Builder -> Only Builder) -> Builder -> Only Builder
forall a b. (a -> b) -> a -> b
$ SymEnv -> [Expr] -> Builder
forall a. SMTLIB2 a => SymEnv -> [a] -> Builder
smt2s SymEnv
env [Expr]
ps)
  smt2 SymEnv
env (PNot Expr
p)         = Format -> Only Builder -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"(not {})"   (Builder -> Only Builder
forall a. a -> Only a
Only (Builder -> Only Builder) -> Builder -> Only Builder
forall a b. (a -> b) -> a -> b
$ SymEnv -> Expr -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2  SymEnv
env Expr
p)
  smt2 SymEnv
env (PImp Expr
p Expr
q)       = Format -> (Builder, Builder) -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"(=> {} {})" (SymEnv -> Expr -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
p, SymEnv -> Expr -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
q)
  smt2 SymEnv
env (PIff Expr
p Expr
q)       = Format -> (Builder, Builder) -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"(= {} {})"  (SymEnv -> Expr -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
p, SymEnv -> Expr -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
q)
  smt2 SymEnv
env (PExist [] Expr
p)    = SymEnv -> Expr -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
p
  smt2 SymEnv
env (PExist [(Symbol, Sort)]
bs Expr
p)    = Format -> (Builder, Builder) -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"(exists ({}) {})"  (SymEnv -> [(Symbol, Sort)] -> Builder
forall a. SMTLIB2 a => SymEnv -> [a] -> Builder
smt2s SymEnv
env [(Symbol, Sort)]
bs, SymEnv -> Expr -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
p)
  smt2 SymEnv
env (PAll   [] Expr
p)    = SymEnv -> Expr -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
p
  smt2 SymEnv
env (PAll   [(Symbol, Sort)]
bs Expr
p)    = Format -> (Builder, Builder) -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"(forall ({}) {})"  (SymEnv -> [(Symbol, Sort)] -> Builder
forall a. SMTLIB2 a => SymEnv -> [a] -> Builder
smt2s SymEnv
env [(Symbol, Sort)]
bs, SymEnv -> Expr -> Builder
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                = String -> Builder
forall a. String -> a
panic (String
"smtlib2 Pred  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. Show a => a -> String
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.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
_ = SymEnv -> Expr -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2    SymEnv
env Expr
e

smt2Var :: SymEnv -> Symbol -> Sort -> Builder.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                   = SymEnv -> Symbol -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Symbol
x

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

smt2VarAs :: SymEnv -> Symbol -> Sort -> Builder.Builder
smt2VarAs :: SymEnv -> Symbol -> Sort -> Builder
smt2VarAs SymEnv
env Symbol
x Sort
t = Format -> (Builder, Builder) -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"(as {} {})" (SymEnv -> Symbol -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Symbol
x, Symbol -> SymEnv -> Sort -> Builder
forall a. PPrint a => a -> SymEnv -> Sort -> Builder
smt2SortMono Symbol
x SymEnv
env Sort
t)

smt2Lam :: SymEnv -> (Symbol, Sort) -> Expr -> Builder.Builder
smt2Lam :: SymEnv -> (Symbol, Sort) -> Expr -> Builder
smt2Lam SymEnv
env (Symbol
x, Sort
xT) (ECst Expr
e Sort
eT) = Format -> (Builder, Builder, Builder) -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"({} {} {})" (SymEnv -> Symbol -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Symbol
lambda, Builder
x', SymEnv -> Expr -> Builder
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 :: Symbol
lambda                      = Symbol -> SymEnv -> () -> Sort -> Symbol
forall a. PPrint a => Symbol -> SymEnv -> a -> Sort -> Symbol
symbolAtName Symbol
lambdaName SymEnv
env () (Sort -> Sort -> Sort
FFunc Sort
xT Sort
eT)

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

smt2App :: SymEnv -> Expr -> Builder.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
  = Format -> (Builder, Builder) -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"({} {})" (Symbol -> Builder
forall a. Symbolic a => a -> Builder
symbolBuilder (Symbol -> SymEnv -> Expr -> Sort -> Symbol
forall a. PPrint a => Symbol -> SymEnv -> a -> Sort -> Symbol
symbolAtName Symbol
applyName SymEnv
env Expr
e Sort
t), SymEnv -> [Expr] -> Builder
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 (SymEnv -> Expr -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env (Expr -> Builder) -> [Expr] -> [Builder]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es)
  = Builder
b
  | Bool
otherwise
  = Format -> (Builder, Builder) -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"({} {})" (SymEnv -> Expr -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
f, SymEnv -> [Expr] -> Builder
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.Builder
smt2Coerc :: SymEnv -> Sort -> Sort -> Expr -> Builder
smt2Coerc SymEnv
env Sort
t1 Sort
t2 Expr
e 
  | Builder
t1' Builder -> Builder -> Bool
forall a. Eq a => a -> a -> Bool
== Builder
t2'  = SymEnv -> Expr -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
e
  | Bool
otherwise = Format -> (Builder, Builder) -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"({} {})" (Symbol -> Builder
forall a. Symbolic a => a -> Builder
symbolBuilder Symbol
coerceFn , SymEnv -> Expr -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
e)
  where 
    coerceFn :: Symbol
coerceFn  = Symbol -> SymEnv -> Expr -> Sort -> Symbol
forall a. PPrint a => Symbol -> SymEnv -> a -> Sort -> Symbol
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
    t1' :: Builder
t1'       = Expr -> SymEnv -> Sort -> Builder
forall a. PPrint a => a -> SymEnv -> Sort -> Builder
smt2SortMono Expr
e SymEnv
env Sort
t1 
    t2' :: Builder
t2'       = Expr -> SymEnv -> Sort -> Builder
forall a. PPrint a => a -> SymEnv -> Sort -> Builder
smt2SortMono Expr
e SymEnv
env 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
eExpr -> [Expr] -> [Expr]
forall 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.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 = Format -> (Builder, Builder, Builder) -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"({} {} {})" (SymEnv -> Brel -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Brel
r, SymEnv -> Expr -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
e1, SymEnv -> Expr -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
e2)

mkNe :: SymEnv -> Expr -> Expr -> Builder.Builder
mkNe :: SymEnv -> Expr -> Expr -> Builder
mkNe SymEnv
env Expr
e1 Expr
e2      = Format -> (Builder, Builder) -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"(not (= {} {}))" (SymEnv -> Expr -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
e1, SymEnv -> Expr -> Builder
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)       = Format -> Only Builder -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"(declare-datatypes {})"       (Builder -> Only Builder
forall a. a -> Only a
Only (Builder -> Only Builder) -> Builder -> Only Builder
forall a b. (a -> b) -> a -> b
$ SymEnv -> [DataDecl] -> Builder
smt2data SymEnv
env [DataDecl]
ds)
  smt2 SymEnv
env (Declare Symbol
x [SmtSort]
ts SmtSort
t)    = Format -> (Builder, Builder, Builder) -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"(declare-fun {} ({}) {})"     (SymEnv -> Symbol -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Symbol
x, [Builder] -> Builder
smt2many (SymEnv -> SmtSort -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env (SmtSort -> Builder) -> [SmtSort] -> [Builder]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SmtSort]
ts), SymEnv -> SmtSort -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env SmtSort
t)
  smt2 SymEnv
env c :: Command
c@(Define Sort
t)        = Format -> Only Builder -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"(declare-sort {})"            (Builder -> Only Builder
forall a. a -> Only a
Only (Builder -> Only Builder) -> Builder -> Only Builder
forall a b. (a -> b) -> a -> b
$ Command -> SymEnv -> Sort -> Builder
forall a. PPrint a => a -> SymEnv -> Sort -> Builder
smt2SortMono Command
c SymEnv
env Sort
t)
  smt2 SymEnv
env (Assert Maybe Int
Nothing Expr
p)  = Format -> Only Builder -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"(assert {})"                  (Builder -> Only Builder
forall a. a -> Only a
Only (Builder -> Only Builder) -> Builder -> Only Builder
forall a b. (a -> b) -> a -> b
$ SymEnv -> Expr -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
p)
  smt2 SymEnv
env (Assert (Just Int
i) Expr
p) = Format -> (Builder, Int) -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"(assert (! {} :named p-{}))"  (SymEnv -> Expr -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
p, Int
i)
  smt2 SymEnv
env (Distinct [Expr]
az)
    | [Expr] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
az Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
2            = Builder
""
    | Bool
otherwise                = Format -> Only Builder -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"(assert (distinct {}))"       (Builder -> Only Builder
forall a. a -> Only a
Only (Builder -> Only Builder) -> Builder -> Only Builder
forall a b. (a -> b) -> a -> b
$ SymEnv -> [Expr] -> Builder
forall a. SMTLIB2 a => SymEnv -> [a] -> Builder
smt2s SymEnv
env [Expr]
az)
  smt2 SymEnv
env (AssertAx Triggered Expr
t)        = Format -> Only Builder -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"(assert {})"                  (Builder -> Only Builder
forall a. a -> Only a
Only (Builder -> Only Builder) -> Builder -> Only Builder
forall a b. (a -> b) -> a -> b
$ SymEnv -> Triggered Expr -> Builder
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
"(get-value (" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> SymEnv -> [Symbol] -> Builder
forall a. SMTLIB2 a => SymEnv -> [a] -> Builder
smt2s SymEnv
env [Symbol]
xs Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
"))"
  smt2 SymEnv
env (CMany [Command]
cmds)        = [Builder] -> Builder
smt2many (SymEnv -> Command -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env (Command -> Builder) -> [Command] -> [Builder]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Command]
cmds)

instance SMTLIB2 (Triggered Expr) where
  smt2 :: SymEnv -> Triggered Expr -> Builder
smt2 SymEnv
env (TR Trigger
NoTrigger Expr
e)       = SymEnv -> Expr -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
e
  smt2 SymEnv
env (TR Trigger
_ (PExist [] Expr
p))   = SymEnv -> Expr -> Builder
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)) = Format -> (Builder, Builder, Builder) -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"(exists ({}) (! {} :pattern({})))"  (SymEnv -> [(Symbol, Sort)] -> Builder
forall a. SMTLIB2 a => SymEnv -> [a] -> Builder
smt2s SymEnv
env [(Symbol, Sort)]
bs, SymEnv -> Expr -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
p, SymEnv -> [Expr] -> Builder
forall a. SMTLIB2 a => SymEnv -> [a] -> Builder
smt2s SymEnv
env (Triggered Expr -> [Expr]
makeTriggers Triggered Expr
t))
  smt2 SymEnv
env (TR Trigger
_ (PAll   [] Expr
p))   = SymEnv -> Expr -> Builder
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)) = Format -> (Builder, Builder, Builder) -> Builder
forall ps. Params ps => Format -> ps -> Builder
build Format
"(forall ({}) (! {} :pattern({})))"  (SymEnv -> [(Symbol, Sort)] -> Builder
forall a. SMTLIB2 a => SymEnv -> [a] -> Builder
smt2s SymEnv
env [(Symbol, Sort)]
bs, SymEnv -> Expr -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
p, SymEnv -> [Expr] -> Builder
forall a. SMTLIB2 a => SymEnv -> [a] -> Builder
smt2s SymEnv
env (Triggered Expr -> [Expr]
makeTriggers Triggered Expr
t))
  smt2 SymEnv
env (TR Trigger
_ Expr
e)               = SymEnv -> Expr -> Builder
forall a. SMTLIB2 a => SymEnv -> a -> Builder
smt2 SymEnv
env Expr
e

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

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