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

{-# OPTIONS_GHC -Wno-orphans        #-}

-- | 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           Control.Monad.State
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 :: (Symbol, Sort) -> SymM Builder
smt2 c :: (Symbol, Sort)
c@(Symbol
sym, Sort
t) =
    -- build "({} {})" (smt2 env sym, smt2SortMono c env t)
    do Builder
s <- Symbol -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 Symbol
sym
       Builder
ss <- (Symbol, Sort) -> Sort -> SymM Builder
forall a. PPrint a => a -> Sort -> SymM Builder
smt2SortMono (Symbol, Sort)
c Sort
t
       Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ [Builder] -> Builder
parenSeqs [Builder
s , Builder
ss]

instance SMTLIB2 (Symbol, Expr) where
  smt2 :: (Symbol, Expr) -> SymM Builder
smt2 (Symbol
sym, Expr
e) =
    do Builder
s <- Symbol -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 Symbol
sym
       Builder
ss <- Expr -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 Expr
e
       Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ [Builder] -> Builder
parenSeqs [Builder
s, Builder
ss]

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

smt2Sort :: (PPrint a) => Bool -> a -> Sort -> SymM Builder
smt2Sort :: forall a. PPrint a => Bool -> a -> Sort -> SymM Builder
smt2Sort Bool
poly a
_ Sort
t =
  do SymEnv
env <- StateT SymEnv Identity SymEnv
forall s (m :: * -> *). MonadState s m => m s
get
     SmtSort -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 (Bool -> SEnv DataDecl -> Sort -> SmtSort
Thy.sortSmtSort Bool
poly (SymEnv -> SEnv DataDecl
seData SymEnv
env) Sort
t)

smt2data :: [DataDecl] -> SymM Builder
smt2data :: [DataDecl] -> SymM Builder
smt2data = [DataDecl] -> SymM Builder
smt2data' ([DataDecl] -> SymM Builder)
-> ([DataDecl] -> [DataDecl]) -> [DataDecl] -> SymM 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' :: [DataDecl] -> SymM Builder
smt2data' :: [DataDecl] -> SymM Builder
smt2data' [DataDecl]
ds =
  do [Builder]
n <- (DataDecl -> SymM Builder)
-> [DataDecl] -> StateT SymEnv Identity [Builder]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse DataDecl -> SymM Builder
smt2dataname [DataDecl]
ds
     [Builder]
d <- (DataDecl -> SymM Builder)
-> [DataDecl] -> StateT SymEnv Identity [Builder]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse DataDecl -> SymM Builder
smt2datactors [DataDecl]
ds
     Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ [Builder] -> Builder
seqs [ Builder -> Builder
parens (Builder -> Builder) -> Builder -> Builder
forall a b. (a -> b) -> a -> b
$ [Builder] -> Builder
smt2many [Builder]
n , Builder -> Builder
parens (Builder -> Builder) -> Builder -> Builder
forall a b. (a -> b) -> a -> b
$ [Builder] -> Builder
smt2many [Builder]
d ]


smt2dataname :: DataDecl -> SymM Builder
smt2dataname :: DataDecl -> SymM Builder
smt2dataname (DDecl FTycon
tc Int
as [DataCtor]
_) =
  do Builder
name <- Symbol -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 (FTycon -> Symbol
forall a. Symbolic a => a -> Symbol
symbol FTycon
tc)
     Builder
n    <- Int -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 Int
as
     Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ [Builder] -> Builder
parenSeqs [Builder
name, Builder
n]


smt2datactors :: DataDecl -> SymM Builder
smt2datactors :: DataDecl -> SymM Builder
smt2datactors (DDecl FTycon
_ Int
as [DataCtor]
cs) =
  do [Builder]
ds <- (DataCtor -> SymM Builder)
-> [DataCtor] -> StateT SymEnv Identity [Builder]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (Int -> DataCtor -> SymM Builder
smt2ctor Int
as) [DataCtor]
cs
     if Int
as Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0
      then do [Builder]
tvars <- (Int -> SymM Builder) -> [Int] -> StateT SymEnv Identity [Builder]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Int -> SymM Builder
smt2TV [Int
0..(Int
asInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)]
              Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ [Builder] -> Builder
parenSeqs [Builder
"par", Builder -> Builder
parens ([Builder] -> Builder
smt2many [Builder]
tvars), Builder -> Builder
parens ([Builder] -> Builder
smt2many [Builder]
ds)]
      else Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$                                               Builder -> Builder
parens ([Builder] -> Builder
smt2many [Builder]
ds)
  where
    smt2TV :: Int -> SymM Builder
smt2TV = SmtSort -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 (SmtSort -> SymM Builder)
-> (Int -> SmtSort) -> Int -> SymM Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> SmtSort
SVar

smt2ctor :: Int -> DataCtor -> SymM Builder
smt2ctor :: Int -> DataCtor -> SymM Builder
smt2ctor Int
as (DCtor LocSymbol
c [DataField]
fs) =
  do Builder
h <- LocSymbol -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 LocSymbol
c
     [Builder]
t <- (DataField -> SymM Builder)
-> [DataField] -> StateT SymEnv Identity [Builder]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (Int -> DataField -> SymM Builder
smt2field Int
as) [DataField]
fs
     Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ [Builder] -> Builder
parenSeqs (Builder
h Builder -> [Builder] -> [Builder]
forall a. a -> [a] -> [a]
: [Builder]
t)

smt2field :: Int -> DataField -> SymM Builder
smt2field :: Int -> DataField -> SymM Builder
smt2field Int
as d :: DataField
d@(DField LocSymbol
x Sort
t) =
  do Builder
s <- LocSymbol -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 LocSymbol
x
     Builder
ss <- DataField -> Sort -> SymM Builder
forall a. PPrint a => a -> Sort -> SymM Builder
smt2SortPoly DataField
d (Sort -> SymM Builder) -> Sort -> SymM Builder
forall a b. (a -> b) -> a -> b
$ Int -> Sort -> Sort
mkPoly Int
as Sort
t
     Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ [Builder] -> Builder
parenSeqs [Builder
s , Builder
ss]

-- | 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 a. [a] -> 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 :: Symbol -> SymM Builder
smt2 Symbol
s = do SymEnv
env <- StateT SymEnv Identity SymEnv
forall s (m :: * -> *). MonadState s m => m s
get
              case SymEnv -> Symbol -> Maybe Builder
Thy.smt2Symbol SymEnv
env Symbol
s of
                Just Builder
t  -> Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Builder
t
                Maybe Builder
Nothing -> Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ Symbol -> Builder
forall a. Symbolic a => a -> Builder
symbolBuilder Symbol
s
instance SMTLIB2 Int where
  smt2 :: Int -> SymM Builder
smt2 Int
i = Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ [Char] -> Builder
forall a. IsString a => [Char] -> a
Builder.fromString ([Char] -> Builder) -> [Char] -> Builder
forall a b. (a -> b) -> a -> b
$ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
i

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

instance SMTLIB2 SymConst where
  smt2 :: SymConst -> SymM Builder
smt2 = Symbol -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 (Symbol -> SymM Builder)
-> (SymConst -> Symbol) -> SymConst -> SymM 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 :: Constant -> SymM Builder
smt2 (I Integer
n)   = Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ Integer -> Builder
forall a. Show a => a -> Builder
bShow Integer
n
  smt2 (R Double
d)   = Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ Double -> Builder
forall a. RealFloat a => a -> Builder
bFloat Double
d
  smt2 (L Text
t Sort
s)
    | Sort -> Bool
isString Sort
s = Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ Builder -> Builder
quotes (Builder -> Builder) -> Builder -> Builder
forall a b. (a -> b) -> a -> b
$ Text -> Builder
fromText Text
t
    | Bool
otherwise  = Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ Text -> Builder
fromText Text
t

instance SMTLIB2 Bop where
  smt2 :: Bop -> SymM Builder
smt2 Bop
Plus   = Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Builder
"+"
  smt2 Bop
Minus  = Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Builder
"-"
  smt2 Bop
Times  = Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ Symbol -> Builder
forall a. Symbolic a => a -> Builder
symbolBuilder Symbol
mulFuncName
  smt2 Bop
Div    = Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ Symbol -> Builder
forall a. Symbolic a => a -> Builder
symbolBuilder Symbol
divFuncName
  smt2 Bop
RTimes = Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Builder
"*"
  smt2 Bop
RDiv   = Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Builder
"/"
  smt2 Bop
Mod    = Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Builder
"mod"

instance SMTLIB2 Brel where
  smt2 :: Brel -> SymM Builder
smt2 Brel
Eq  = Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Builder
"="
  smt2 Brel
Ueq = Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Builder
"="
  smt2 Brel
Gt  = Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Builder
">"
  smt2 Brel
Ge  = Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Builder
">="
  smt2 Brel
Lt  = Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Builder
"<"
  smt2 Brel
Le  = Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Builder
"<="
  smt2 Brel
_   = [Char] -> SymM Builder
forall a. HasCallStack => [Char] -> a
errorstar [Char]
"SMTLIB2 Brel"

-- NV TODO: change the way EApp is printed
instance SMTLIB2 Expr where
  smt2 :: Expr -> SymM Builder
smt2 (ESym SymConst
z)         = SymConst -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 SymConst
z
  smt2 (ECon Constant
c)         = Constant -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 Constant
c
  smt2 (EVar Symbol
x)         = Symbol -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 Symbol
x
  smt2 e :: Expr
e@(EApp Expr
_ Expr
_)     = Expr -> SymM Builder
smt2App Expr
e
  smt2 (ENeg Expr
e)         = do Builder
s <- Expr -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 Expr
e
                             Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ [Builder] -> Builder
parenSeqs [Builder
"-", Builder
s]
  smt2 (EBin Bop
o Expr
e1 Expr
e2)   = do Builder
so <- Bop -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 Bop
o
                             Builder
s1 <- Expr -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 Expr
e1
                             Builder
s2 <- Expr -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 Expr
e2
                             Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ [Builder] -> Builder
parenSeqs [Builder
so, Builder
s1, Builder
s2]
  smt2 (ELet Symbol
x Expr
e1 Expr
e2)   = do Builder
s1 <- (Symbol, Expr) -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 (Symbol
x, Expr
e1)
                             Builder
s2 <- Expr -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 Expr
e2
                             Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ [Builder] -> Builder
parenSeqs [Builder
"let", Builder -> Builder
parens Builder
s1, Builder
s2]
  smt2 (EIte Expr
e1 Expr
e2 Expr
e3)  = do Builder
s1 <- Expr -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 Expr
e1
                             Builder
s2 <- Expr -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 Expr
e2
                             Builder
s3 <- Expr -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 Expr
e3
                             Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ [Builder] -> Builder
parenSeqs [Builder
"ite", Builder
s1, Builder
s2, Builder
s3]
  smt2 (ECst Expr
e Sort
t)       = Expr -> Sort -> SymM Builder
smt2Cast Expr
e Sort
t
  smt2 Expr
PTrue            = Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Builder
"true"
  smt2 Expr
PFalse           = Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Builder
"false"
  smt2 (PAnd [])        = Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Builder
"true"
  smt2 (PAnd [Expr]
ps)        = do Builder
s <- [Expr] -> SymM Builder
forall a. SMTLIB2 a => [a] -> SymM Builder
smt2s [Expr]
ps
                             Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ [Builder] -> Builder
parenSeqs [Builder
"and", Builder
s]
  smt2 (POr [])         = Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Builder
"false"
  smt2 (POr [Expr]
ps)         = do Builder
s <- [Expr] -> SymM Builder
forall a. SMTLIB2 a => [a] -> SymM Builder
smt2s [Expr]
ps
                             Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ [Builder] -> Builder
parenSeqs [Builder
"or", Builder
s]
  smt2 (PNot Expr
p)         = do Builder
s <- Expr -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 Expr
p
                             Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ [Builder] -> Builder
parenSeqs [Builder
"not", Builder
s]
  smt2 (PImp Expr
p Expr
q)       = do Builder
s1 <- Expr -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 Expr
p
                             Builder
s2 <- Expr -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 Expr
q
                             Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ [Builder] -> Builder
parenSeqs [Builder
"=>", Builder
s1, Builder
s2]
  smt2 (PIff Expr
p Expr
q)       = do Builder
s1 <- Expr -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 Expr
p
                             Builder
s2 <- Expr -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 Expr
q
                             Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ [Builder] -> Builder
parenSeqs [Builder
"=", Builder
s1, Builder
s2]
  smt2 (PExist [] Expr
p)    = Expr -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 Expr
p
  smt2 (PExist [(Symbol, Sort)]
xs Expr
p)    = do Builder
s <- [(Symbol, Sort)] -> SymM Builder
forall a. SMTLIB2 a => [a] -> SymM Builder
smt2s [(Symbol, Sort)]
xs
                             Builder
s1 <- Expr -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 Expr
p
                             Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ [Builder] -> Builder
parenSeqs [Builder
"exists", Builder -> Builder
parens Builder
s, Builder
s1]
  smt2 (PAll   [] Expr
p)    = Expr -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 Expr
p
  smt2 (PAll   [(Symbol, Sort)]
xs Expr
p)    = do Builder
s <- [(Symbol, Sort)] -> SymM Builder
forall a. SMTLIB2 a => [a] -> SymM Builder
smt2s [(Symbol, Sort)]
xs
                             Builder
s1 <- Expr -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 Expr
p
                             Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ [Builder] -> Builder
parenSeqs [Builder
"forall", Builder -> Builder
parens Builder
s, Builder
s1]
  smt2 (PAtom Brel
r Expr
e1 Expr
e2)  = Brel -> Expr -> Expr -> SymM Builder
mkRel Brel
r Expr
e1 Expr
e2
  smt2 (ELam (Symbol, Sort)
b Expr
e)       = (Symbol, Sort) -> Expr -> SymM Builder
smt2Lam (Symbol, Sort)
b Expr
e
  smt2 (ECoerc Sort
t1 Sort
t2 Expr
e) = Sort -> Sort -> Expr -> SymM Builder
smt2Coerc Sort
t1 Sort
t2 Expr
e
  smt2 Expr
e                = [Char] -> SymM Builder
forall a. HasCallStack => [Char] -> a
panic ([Char]
"smtlib2 Pred  " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Expr -> [Char]
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 :: Expr -> Sort -> SymM Builder
smt2Cast :: Expr -> Sort -> SymM Builder
smt2Cast (EVar Symbol
x) Sort
t = Symbol -> Sort -> SymM Builder
smt2Var Symbol
x Sort
t
smt2Cast Expr
e        Sort
_ = Expr -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2    Expr
e

smt2Var :: Symbol -> Sort -> SymM Builder
smt2Var :: Symbol -> Sort -> SymM Builder
smt2Var Symbol
x Sort
t
  | Symbol -> Bool
isLamArgSymbol Symbol
x = Symbol -> Sort -> SymM Builder
smtLamArg Symbol
x Sort
t
  | Bool
otherwise        = do SymEnv
env <- StateT SymEnv Identity SymEnv
forall s (m :: * -> *). MonadState s m => m s
get
                          case Symbol -> SymEnv -> Maybe Sort
symEnvSort Symbol
x SymEnv
env of
                            Just Sort
s | Sort -> Sort -> Bool
isPolyInst Sort
s Sort
t -> Symbol -> Sort -> SymM Builder
smt2VarAs Symbol
x Sort
t
                            Maybe Sort
_                       -> Symbol -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 Symbol
x

smt2VarAs :: Symbol -> Sort -> SymM Builder
smt2VarAs :: Symbol -> Sort -> SymM Builder
smt2VarAs Symbol
x Sort
t =
  do Builder
s <- Symbol -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 Symbol
x
     Builder
s1 <- Symbol -> Sort -> SymM Builder
forall a. PPrint a => a -> Sort -> SymM Builder
smt2SortMono Symbol
x Sort
t
     Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ [Builder] -> Builder
parenSeqs [Builder
"as", Builder
s, Builder
s1]

-- the next four functions (ones containing a call to `symbolAtName`) can trigger
-- an expansion of the "nursery" tag table ('seApplsCur' in 'SymEnv') when processing
-- a fresh function sort
smtLamArg :: Symbol -> Sort -> SymM Builder
smtLamArg :: Symbol -> Sort -> SymM Builder
smtLamArg Symbol
x Sort
t =
  do Text
s <- Symbol -> Sort -> SymM Text
symbolAtName Symbol
x (Sort -> Sort -> Sort
FFunc Sort
t Sort
FInt)
     Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ Text -> Builder
Builder.fromText Text
s

smt2Lam :: (Symbol, Sort) -> Expr -> SymM Builder
smt2Lam :: (Symbol, Sort) -> Expr -> SymM Builder
smt2Lam (Symbol
x, Sort
xT) full :: Expr
full@(ECst Expr
_ Sort
eT) =
  do Builder
x' <- Symbol -> Sort -> SymM Builder
smtLamArg Symbol
x Sort
xT
     Text
lambda <- Symbol -> Sort -> SymM Text
symbolAtName Symbol
lambdaName (Sort -> Sort -> Sort
FFunc Sort
xT Sort
eT)
     Builder
f <- Expr -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 Expr
full
     Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ [Builder] -> Builder
parenSeqs [Text -> Builder
Builder.fromText Text
lambda, Builder
x', Builder
f]
smt2Lam (Symbol, Sort)
_ Expr
e
  = [Char] -> SymM Builder
forall a. HasCallStack => [Char] -> a
panic ([Char]
"smtlib2: Cannot serialize unsorted lambda: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Expr -> [Char]
forall a. PPrint a => a -> [Char]
showpp Expr
e)

smt2App :: Expr -> SymM Builder
smt2App :: Expr -> SymM Builder
smt2App (EApp (EApp Expr
f Expr
e1) Expr
e2)
  | Just Sort
t <- Expr -> Maybe Sort
unApplyAt Expr
f
  = do Text
a <- Symbol -> Sort -> SymM Text
symbolAtName Symbol
applyName Sort
t
       Builder
s <- [Expr] -> SymM Builder
forall a. SMTLIB2 a => [a] -> SymM Builder
smt2s [Expr
e1, Expr
e2]
       Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ [Builder] -> Builder
parenSeqs [Text -> Builder
Builder.fromText Text
a, Builder
s]
smt2App Expr
e = do [Builder]
s0 <- (Expr -> SymM Builder)
-> [Expr] -> StateT SymEnv Identity [Builder]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Expr -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 [Expr]
es
               Maybe Builder
s1 <- (Symbol -> Sort -> SymM Builder)
-> Expr -> [Builder] -> SymM (Maybe Builder)
Thy.smt2App Symbol -> Sort -> SymM Builder
smt2VarAs Expr
f [Builder]
s0
               case Maybe Builder
s1 of
                 Just Builder
b -> Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Builder
b
                 Maybe Builder
Nothing -> do Builder
s2 <- Expr -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 Expr
f
                               Builder
s3 <- [Expr] -> SymM Builder
forall a. SMTLIB2 a => [a] -> SymM Builder
smt2s [Expr]
es
                               Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ [Builder] -> Builder
parenSeqs [Builder
s2, Builder
s3]
  where
    (Expr
f, [Expr]
es) = Expr -> (Expr, [Expr])
splitEApp' Expr
e

smt2Coerc :: Sort -> Sort -> Expr -> SymM Builder
smt2Coerc :: Sort -> Sort -> Expr -> SymM Builder
smt2Coerc Sort
t1 Sort
t2 Expr
e
  | Sort
t1 Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
t2  = Expr -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 Expr
e
  | Bool
otherwise = do Text
coerceFn <- Symbol -> Sort -> SymM Text
symbolAtName Symbol
coerceName (Sort -> Sort -> Sort
FFunc Sort
t1 Sort
t2)
                   Builder
s <- Expr -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 Expr
e
                   Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ [Builder] -> Builder
parenSeqs [Text -> Builder
Builder.fromText Text
coerceFn , Builder
s]

splitEApp' :: Expr -> (Expr, [Expr])
splitEApp' :: Expr -> (Expr, [Expr])
splitEApp'            = [Expr] -> Expr -> (Expr, [Expr])
forall {v}. [ExprV v] -> ExprV v -> (ExprV v, [ExprV v])
go []
  where
    go :: [ExprV v] -> ExprV v -> (ExprV v, [ExprV v])
go [ExprV v]
acc (EApp ExprV v
f ExprV v
e) = [ExprV v] -> ExprV v -> (ExprV v, [ExprV v])
go (ExprV v
eExprV v -> [ExprV v] -> [ExprV v]
forall a. a -> [a] -> [a]
:[ExprV v]
acc) ExprV v
f
  --   go acc (ECst e _) = go acc e
    go [ExprV v]
acc ExprV v
e          = (ExprV v
e, [ExprV v]
acc)

mkRel :: Brel -> Expr -> Expr -> SymM Builder
mkRel :: Brel -> Expr -> Expr -> SymM Builder
mkRel Brel
Ne  Expr
e1 Expr
e2 = Expr -> Expr -> SymM Builder
mkNe Expr
e1 Expr
e2
mkRel Brel
Une Expr
e1 Expr
e2 = Expr -> Expr -> SymM Builder
mkNe Expr
e1 Expr
e2
mkRel Brel
r   Expr
e1 Expr
e2 = do Builder
s <- Brel -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 Brel
r
                     Builder
s1 <- Expr -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 Expr
e1
                     Builder
s2 <- Expr -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 Expr
e2
                     Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ [Builder] -> Builder
parenSeqs [Builder
s, Builder
s1, Builder
s2]

mkNe :: Expr -> Expr -> SymM Builder
mkNe :: Expr -> Expr -> SymM Builder
mkNe Expr
e1 Expr
e2 = do Builder
s1 <- Expr -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 Expr
e1
                Builder
s2 <- Expr -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 Expr
e2
                Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ Builder -> Builder -> Builder
key Builder
"not" ([Builder] -> Builder
parenSeqs [Builder
"=", Builder
s1, Builder
s2])
instance SMTLIB2 Command where
  smt2 :: Command -> SymM Builder
smt2     (DeclData [DataDecl]
ds)       = do Builder
s <- [DataDecl] -> SymM Builder
smt2data [DataDecl]
ds
                                    Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ Builder -> Builder -> Builder
key Builder
"declare-datatypes" Builder
s
  smt2     (Declare Text
x [SmtSort]
ts SmtSort
t)    = do Builder
s <- [SmtSort] -> SymM Builder
forall a. SMTLIB2 a => [a] -> SymM Builder
smt2s [SmtSort]
ts
                                    Builder
s1 <- SmtSort -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 SmtSort
t
                                    Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ [Builder] -> Builder
parenSeqs [Builder
"declare-fun", Text -> Builder
Builder.fromText Text
x, Builder -> Builder
parens Builder
s, Builder
s1]
  smt2     c :: Command
c@(Define Sort
t)        = do Builder
s <- Command -> Sort -> SymM Builder
forall a. PPrint a => a -> Sort -> SymM Builder
smt2SortMono Command
c Sort
t
                                    Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ Builder -> Builder -> Builder
key Builder
"declare-sort" Builder
s
  smt2     (DefineFunc Symbol
name [(Symbol, SmtSort)]
paramxs SmtSort
rsort Expr
e) =
    do Builder
n <- Symbol -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 Symbol
name
       [Builder]
bParams <- ((Symbol, SmtSort) -> SymM Builder)
-> [(Symbol, SmtSort)] -> StateT SymEnv Identity [Builder]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (\(Symbol
s, SmtSort
t) -> do Builder
s0 <- Symbol -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 Symbol
s
                                          Builder
s1 <- SmtSort -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 SmtSort
t
                                          Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ [Builder] -> Builder
parenSeqs [Builder
s0 , Builder
s1]) [(Symbol, SmtSort)]
paramxs
       Builder
r <- SmtSort -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 SmtSort
rsort
       Builder
e' <- Expr -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 Expr
e
       Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ [Builder] -> Builder
parenSeqs [Builder
"define-fun", Builder
n, [Builder] -> Builder
parenSeqs [Builder]
bParams, Builder
r, Builder
e']

  smt2     (Assert Maybe Int
Nothing Expr
p)  = {-# SCC "smt2-assert" #-}
                                  do Builder
s <- Expr -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 Expr
p
                                     Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ Builder -> Builder -> Builder
key Builder
"assert" Builder
s
  smt2     (Assert (Just Int
i) Expr
p) = {-# SCC "smt2-assert" #-}
                                  do Builder
s <- Expr -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 Expr
p
                                     Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ Builder -> Builder -> Builder
key Builder
"assert" (Builder -> Builder
parens (Builder
"!"Builder -> Builder -> Builder
<+> Builder
s Builder -> Builder -> Builder
<+> Builder
":named p-" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Int -> Builder
forall a. Show a => a -> Builder
bShow Int
i))
  smt2     (Distinct [Expr]
az)
    | [Expr] -> Int
forall a. [a] -> 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 -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Builder
""
    | Bool
otherwise                = do Builder
s <- [Expr] -> SymM Builder
forall a. SMTLIB2 a => [a] -> SymM Builder
smt2s [Expr]
az
                                    Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ Builder -> Builder -> Builder
key Builder
"assert" (Builder -> Builder) -> Builder -> Builder
forall a b. (a -> b) -> a -> b
$ Builder -> Builder -> Builder
key Builder
"distinct" Builder
s
  smt2     (AssertAx Triggered Expr
t)        = do Builder
s <- Triggered Expr -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 Triggered Expr
t
                                    Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ Builder -> Builder -> Builder
key Builder
"assert" Builder
s
  smt2     Command
Push                = Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Builder
"(push 1)"
  smt2     Command
Pop                 = Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Builder
"(pop 1)"
  smt2     Command
CheckSat            = Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Builder
"(check-sat)"
  smt2     (GetValue [Symbol]
xs)       = do Builder
s <- [Symbol] -> SymM Builder
forall a. SMTLIB2 a => [a] -> SymM Builder
smt2s [Symbol]
xs
                                    Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ Builder -> Builder -> Builder
key Builder
"key-value" (Builder -> Builder
parens Builder
s)
  smt2     (CMany [Command]
cmds)        = [Command] -> SymM Builder
forall a. SMTLIB2 a => [a] -> SymM Builder
smt2s [Command]
cmds
  smt2     Command
Exit                = Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Builder
"(exit)"
  smt2     Command
SetMbqi             = Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Builder
"(set-option :smt.mbqi true)"
  smt2     (Comment Text
t)         = Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ Text -> Builder
fromText (Text
"; " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
t Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\n")

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

{-# INLINE smtTr #-}
smtTr :: Builder -> [(Symbol, Sort)] -> Expr -> Triggered Expr -> SymM Builder
smtTr :: Builder
-> [(Symbol, Sort)] -> Expr -> Triggered Expr -> SymM Builder
smtTr Builder
q [(Symbol, Sort)]
xs Expr
p Triggered Expr
t =
  do Builder
s <- [(Symbol, Sort)] -> SymM Builder
forall a. SMTLIB2 a => [a] -> SymM Builder
smt2s [(Symbol, Sort)]
xs
     Builder
s1 <- Expr -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 Expr
p
     Builder
s2 <- [Expr] -> SymM Builder
forall a. SMTLIB2 a => [a] -> SymM Builder
smt2s (Triggered Expr -> [Expr]
makeTriggers Triggered Expr
t)
     Builder -> SymM Builder
forall a. a -> StateT SymEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Builder -> SymM Builder) -> Builder -> SymM Builder
forall a b. (a -> b) -> a -> b
$ Builder -> Builder -> Builder
key Builder
q (Builder -> Builder
parens Builder
s Builder -> Builder -> Builder
<+> Builder -> Builder -> Builder
key Builder
"!" (Builder
s1 Builder -> Builder -> Builder
<+> Builder
":pattern" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder -> Builder
parens Builder
s2))

{-# INLINE smt2s #-}
smt2s :: SMTLIB2 a => [a] -> SymM Builder
smt2s :: forall a. SMTLIB2 a => [a] -> SymM Builder
smt2s [a]
as = [Builder] -> Builder
smt2many ([Builder] -> Builder)
-> StateT SymEnv Identity [Builder] -> SymM Builder
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> SymM Builder) -> [a] -> StateT SymEnv Identity [Builder]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse a -> SymM Builder
forall a. SMTLIB2 a => a -> SymM Builder
smt2 [a]
as

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