{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
module What4.Protocol.SMTLib2.Syntax
(
Command(..)
, setLogic
, setOption
, setProduceModels
, SMTInfoFlag(..)
, getInfo
, getVersion
, getName
, getErrorBehavior
, exit
, declareSort
, defineSort
, declareConst
, declareFun
, defineFun
, Symbol
, checkSat
, checkSatAssuming
, checkSatWithAssumptions
, getModel
, getValue
, push
, pop
, resetAssertions
, assert
, assertNamed
, getUnsatAssumptions
, getUnsatCore
, getAbduct
, getAbductNext
, synthFun
, declareVar
, constraint
, checkSynth
, Logic(..)
, qf_bv
, allSupported
, allLogic
, hornLogic
, Sort(..)
, boolSort
, bvSort
, intSort
, realSort
, varSort
, Term(..)
, un_app
, bin_app
, term_app
, pairwise_app
, namedTerm
, builder_list
, true
, false
, not
, implies
, and
, or
, xor
, eq
, distinct
, ite
, forall_
, exists_
, letBinder
, negate
, numeral
, decimal
, sub
, add
, mul
, div
, (./)
, mod
, abs
, le
, lt
, ge
, gt
, toReal
, toInt
, isInt
, concat
, extract
, bvnot
, bvand
, bvor
, bvxor
, bvneg
, bvadd
, bvsub
, bvmul
, bvudiv
, bvurem
, bvshl
, bvlshr
, bvult
, bit0
, bit1
, bvbinary
, bvdecimal
, bvhexadecimal
, bvashr
, bvslt
, bvsle
, bvule
, bvsgt
, bvsge
, bvugt
, bvuge
, bvsdiv
, bvsrem
, bvsignExtend
, bvzeroExtend
, arraySort
, arrayConst
, select
, store
) where
import qualified Data.BitVector.Sized as BV
import Data.Char (intToDigit)
import Data.Parameterized.NatRepr
import Data.String
import Data.Text (Text, cons)
import Data.Text.Lazy.Builder (Builder)
import qualified Data.Text.Lazy.Builder as Builder
import qualified Data.Text.Lazy.Builder.Int as Builder
import Numeric.Natural
import GHC.Generics (Generic)
import Data.Data (Data)
import Data.Typeable (Typeable)
import qualified Prelude
import Prelude hiding (and, or, concat, negate, div, mod, abs, not)
app_list :: Builder -> [Builder] -> Builder
app_list :: Builder -> [Builder] -> Builder
app_list Builder
o [Builder]
args = Builder
"(" forall a. Semigroup a => a -> a -> a
<> Builder
o forall a. Semigroup a => a -> a -> a
<> forall {a}. (IsString a, Semigroup a) => [a] -> a
go [Builder]
args
where go :: [a] -> a
go [] = a
")"
go (a
f:[a]
r) = a
" " forall a. Semigroup a => a -> a -> a
<> a
f forall a. Semigroup a => a -> a -> a
<> [a] -> a
go [a]
r
app :: Builder -> [Builder] -> Builder
app :: Builder -> [Builder] -> Builder
app Builder
o [] = Builder
o
app Builder
o [Builder]
args = Builder -> [Builder] -> Builder
app_list Builder
o [Builder]
args
builder_list :: [Builder] -> Builder
builder_list :: [Builder] -> Builder
builder_list [] = Builder
"()"
builder_list (Builder
h:[Builder]
l) = Builder -> [Builder] -> Builder
app_list Builder
h [Builder]
l
newtype Logic = Logic Builder
qf_bv :: Logic
qf_bv :: Logic
qf_bv = Builder -> Logic
Logic Builder
"QF_BV"
allSupported :: Logic
allSupported :: Logic
allSupported = Builder -> Logic
Logic Builder
"ALL_SUPPORTED"
{-# DEPRECATED allSupported "Use allLogic instead" #-}
allLogic :: Logic
allLogic :: Logic
allLogic = Builder -> Logic
Logic Builder
"ALL"
hornLogic :: Logic
hornLogic :: Logic
hornLogic = Builder -> Logic
Logic Builder
"HORN"
type Symbol = Text
newtype Sort = Sort { Sort -> Builder
unSort :: Builder }
varSort :: Symbol -> Sort
varSort :: Text -> Sort
varSort = Builder -> Sort
Sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Builder
Builder.fromText
boolSort :: Sort
boolSort :: Sort
boolSort = Builder -> Sort
Sort Builder
"Bool"
bvSort :: Natural -> Sort
bvSort :: Natural -> Sort
bvSort Natural
w | Natural
w forall a. Ord a => a -> a -> Bool
>= Natural
1 = Builder -> Sort
Sort forall a b. (a -> b) -> a -> b
$ Builder
"(_ BitVec " forall a. Semigroup a => a -> a -> a
<> forall a. IsString a => [Char] -> a
fromString (forall a. Show a => a -> [Char]
show Natural
w) forall a. Semigroup a => a -> a -> a
<> Builder
")"
| Bool
otherwise = forall a. HasCallStack => [Char] -> a
error [Char]
"bvSort expects a positive number."
intSort :: Sort
intSort :: Sort
intSort = Builder -> Sort
Sort Builder
"Int"
realSort :: Sort
realSort :: Sort
realSort = Builder -> Sort
Sort Builder
"Real"
arraySort :: Sort -> Sort -> Sort
arraySort :: Sort -> Sort -> Sort
arraySort (Sort Builder
i) (Sort Builder
v) = Builder -> Sort
Sort forall a b. (a -> b) -> a -> b
$ Builder
"(Array " forall a. Semigroup a => a -> a -> a
<> Builder
i forall a. Semigroup a => a -> a -> a
<> Builder
" " forall a. Semigroup a => a -> a -> a
<> Builder
v forall a. Semigroup a => a -> a -> a
<> Builder
")"
newtype Term = T { Term -> Builder
renderTerm :: Builder }
deriving ([Char] -> Term
forall a. ([Char] -> a) -> IsString a
fromString :: [Char] -> Term
$cfromString :: [Char] -> Term
IsString, Semigroup Term
Term
[Term] -> Term
Term -> Term -> Term
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
mconcat :: [Term] -> Term
$cmconcat :: [Term] -> Term
mappend :: Term -> Term -> Term
$cmappend :: Term -> Term -> Term
mempty :: Term
$cmempty :: Term
Monoid, NonEmpty Term -> Term
Term -> Term -> Term
forall b. Integral b => b -> Term -> Term
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
stimes :: forall b. Integral b => b -> Term -> Term
$cstimes :: forall b. Integral b => b -> Term -> Term
sconcat :: NonEmpty Term -> Term
$csconcat :: NonEmpty Term -> Term
<> :: Term -> Term -> Term
$c<> :: Term -> Term -> Term
Semigroup)
term_app :: Builder -> [Term] -> Term
term_app :: Builder -> [Term] -> Term
term_app Builder
o [Term]
args = Builder -> Term
T (Builder -> [Builder] -> Builder
app Builder
o (Term -> Builder
renderTerm forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Term]
args))
un_app :: Builder -> Term -> Term
un_app :: Builder -> Term -> Term
un_app Builder
o (T Builder
x) = Builder -> Term
T forall a b. (a -> b) -> a -> b
$ forall a. Monoid a => [a] -> a
mconcat [Builder
"(", Builder
o, Builder
" ", Builder
x, Builder
")"]
bin_app :: Builder -> Term -> Term -> Term
bin_app :: Builder -> Term -> Term -> Term
bin_app Builder
o (T Builder
x) (T Builder
y) = Builder -> Term
T forall a b. (a -> b) -> a -> b
$ forall a. Monoid a => [a] -> a
mconcat [Builder
"(", Builder
o, Builder
" ", Builder
x, Builder
" ", Builder
y, Builder
")"]
chain_app :: Builder -> [Term] -> Term
chain_app :: Builder -> [Term] -> Term
chain_app Builder
f l :: [Term]
l@(Term
_:Term
_:[Term]
_) = Builder -> [Term] -> Term
term_app Builder
f [Term]
l
chain_app Builder
f [Term]
_ = forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> [Char]
show Builder
f forall a. [a] -> [a] -> [a]
++ [Char]
" expects two or more arguments."
assoc_app :: Builder -> Term -> [Term] -> Term
assoc_app :: Builder -> Term -> [Term] -> Term
assoc_app Builder
_ Term
t [] = Term
t
assoc_app Builder
f Term
t [Term]
l = Builder -> [Term] -> Term
term_app Builder
f (Term
tforall a. a -> [a] -> [a]
:[Term]
l)
namedTerm :: Term -> Text -> Term
namedTerm :: Term -> Text -> Term
namedTerm (T Builder
x) Text
nm = Builder -> Term
T forall a b. (a -> b) -> a -> b
$ Builder
"(! " forall a. Semigroup a => a -> a -> a
<> Builder
x forall a. Semigroup a => a -> a -> a
<> Builder
" :named " forall a. Semigroup a => a -> a -> a
<> Text -> Builder
Builder.fromText Text
nm forall a. Semigroup a => a -> a -> a
<> Builder
")"
true :: Term
true :: Term
true = Builder -> Term
T Builder
"true"
false :: Term
false :: Term
false = Builder -> Term
T Builder
"false"
not :: Term -> Term
not :: Term -> Term
not = Builder -> Term -> Term
un_app Builder
"not"
implies :: [Term] -> Term -> Term
implies :: [Term] -> Term -> Term
implies [] Term
t = Term
t
implies [Term]
l Term
t = Builder -> [Term] -> Term
term_app Builder
"=>" ([Term]
l forall a. [a] -> [a] -> [a]
++ [Term
t])
and :: [Term] -> Term
and :: [Term] -> Term
and [] = Term
true
and [Term
x] = Term
x
and [Term]
l = Builder -> [Term] -> Term
term_app Builder
"and" [Term]
l
or :: [Term] -> Term
or :: [Term] -> Term
or [] = Term
true
or [Term
x] = Term
x
or [Term]
l = Builder -> [Term] -> Term
term_app Builder
"or" [Term]
l
xor :: [Term] -> Term
xor :: [Term] -> Term
xor l :: [Term]
l@(Term
_:Term
_:[Term]
_) = Builder -> [Term] -> Term
term_app Builder
"xor" [Term]
l
xor [Term]
_ = forall a. HasCallStack => [Char] -> a
error [Char]
"xor expects two or more arguments."
eq :: [Term] -> Term
eq :: [Term] -> Term
eq = Builder -> [Term] -> Term
chain_app Builder
"="
pairwise_app :: Builder -> [Term] -> Term
pairwise_app :: Builder -> [Term] -> Term
pairwise_app Builder
_ [] = Term
true
pairwise_app Builder
_ [Term
_] = Term
true
pairwise_app Builder
f l :: [Term]
l@(Term
_:Term
_:[Term]
_) = Builder -> [Term] -> Term
term_app Builder
f [Term]
l
distinct :: [Term] -> Term
distinct :: [Term] -> Term
distinct = Builder -> [Term] -> Term
pairwise_app Builder
"distinct"
ite :: Term -> Term -> Term -> Term
ite :: Term -> Term -> Term -> Term
ite Term
c Term
x Term
y = Builder -> [Term] -> Term
term_app Builder
"ite" [Term
c, Term
x, Term
y]
varBinding :: (Text,Sort) -> Builder
varBinding :: (Text, Sort) -> Builder
varBinding (Text
nm, Sort
tp) = Builder
"(" forall a. Semigroup a => a -> a -> a
<> Text -> Builder
Builder.fromText Text
nm forall a. Semigroup a => a -> a -> a
<> Builder
" " forall a. Semigroup a => a -> a -> a
<> Sort -> Builder
unSort Sort
tp forall a. Semigroup a => a -> a -> a
<> Builder
")"
forall_ :: [(Text, Sort)] -> Term -> Term
forall_ :: [(Text, Sort)] -> Term -> Term
forall_ [] Term
r = Term
r
forall_ [(Text, Sort)]
vars Term
r =
Builder -> Term
T forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"forall" [[Builder] -> Builder
builder_list ((Text, Sort) -> Builder
varBinding forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Text, Sort)]
vars), Term -> Builder
renderTerm Term
r]
exists_ :: [(Text, Sort)] -> Term -> Term
exists_ :: [(Text, Sort)] -> Term -> Term
exists_ [] Term
r = Term
r
exists_ [(Text, Sort)]
vars Term
r =
Builder -> Term
T forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"exists" [[Builder] -> Builder
builder_list ((Text, Sort) -> Builder
varBinding forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Text, Sort)]
vars), Term -> Builder
renderTerm Term
r]
letBinding :: (Text, Term) -> Builder
letBinding :: (Text, Term) -> Builder
letBinding (Text
nm, Term
t) = Builder -> [Builder] -> Builder
app_list (Text -> Builder
Builder.fromText Text
nm) [Term -> Builder
renderTerm Term
t]
letBinder :: [(Text, Term)] -> Term -> Term
letBinder :: [(Text, Term)] -> Term -> Term
letBinder [] Term
r = Term
r
letBinder [(Text, Term)]
vars Term
r =
Builder -> Term
T (Builder -> [Builder] -> Builder
app Builder
"let" [[Builder] -> Builder
builder_list ((Text, Term) -> Builder
letBinding forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Text, Term)]
vars), Term -> Builder
renderTerm Term
r])
negate :: Term -> Term
negate :: Term -> Term
negate = Builder -> Term -> Term
un_app Builder
"-"
numeral :: Integer -> Term
numeral :: Integer -> Term
numeral Integer
i | Integer
i forall a. Ord a => a -> a -> Bool
>= Integer
0 = Builder -> Term
T forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> Builder
Builder.decimal Integer
i
| Bool
otherwise = Term -> Term
negate (Builder -> Term
T (forall a. Integral a => a -> Builder
Builder.decimal (forall a. Num a => a -> a
Prelude.negate Integer
i)))
decimal :: Integer -> Term
decimal :: Integer -> Term
decimal Integer
i | Integer
i forall a. Ord a => a -> a -> Bool
>= Integer
0 = Builder -> Term
T forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> Builder
Builder.decimal Integer
i forall a. Semigroup a => a -> a -> a
<> Builder
".0"
| Bool
otherwise = Term -> Term
negate forall a b. (a -> b) -> a -> b
$ Builder -> Term
T forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> Builder
Builder.decimal (forall a. Num a => a -> a
Prelude.negate Integer
i) forall a. Semigroup a => a -> a -> a
<> Builder
".0"
sub :: Term -> [Term] -> Term
sub :: Term -> [Term] -> Term
sub Term
x [] = Term
x
sub Term
x [Term]
l = Builder -> [Term] -> Term
term_app Builder
"-" (Term
xforall a. a -> [a] -> [a]
:[Term]
l)
add :: [Term] -> Term
add :: [Term] -> Term
add [] = Builder -> Term
T Builder
"0"
add [Term
x] = Term
x
add [Term]
l = Builder -> [Term] -> Term
term_app Builder
"+" [Term]
l
mul :: [Term] -> Term
mul :: [Term] -> Term
mul [] = Builder -> Term
T Builder
"1"
mul [Term
x] = Term
x
mul [Term]
l = Builder -> [Term] -> Term
term_app Builder
"*" [Term]
l
div :: Term -> [Term] -> Term
div :: Term -> [Term] -> Term
div Term
x [] = Term
x
div Term
x [Term]
l = Builder -> [Term] -> Term
term_app Builder
"div" (Term
xforall a. a -> [a] -> [a]
:[Term]
l)
(./) :: Term -> [Term] -> Term
Term
x ./ :: Term -> [Term] -> Term
./ [] = Term
x
Term
x ./ [Term]
l = Builder -> [Term] -> Term
term_app Builder
"/" (Term
xforall a. a -> [a] -> [a]
:[Term]
l)
mod :: Term -> Term -> Term
mod :: Term -> Term -> Term
mod = Builder -> Term -> Term -> Term
bin_app Builder
"mod"
abs :: Term -> Term
abs :: Term -> Term
abs = Builder -> Term -> Term
un_app Builder
"abs"
le :: [Term] -> Term
le :: [Term] -> Term
le = Builder -> [Term] -> Term
chain_app Builder
"<="
lt :: [Term] -> Term
lt :: [Term] -> Term
lt = Builder -> [Term] -> Term
chain_app Builder
"<"
ge :: [Term] -> Term
ge :: [Term] -> Term
ge = Builder -> [Term] -> Term
chain_app Builder
">="
gt :: [Term] -> Term
gt :: [Term] -> Term
gt = Builder -> [Term] -> Term
chain_app Builder
">"
toReal :: Term -> Term
toReal :: Term -> Term
toReal = Builder -> Term -> Term
un_app Builder
"to_real"
toInt :: Term -> Term
toInt :: Term -> Term
toInt = Builder -> Term -> Term
un_app Builder
"to_int"
isInt :: Term -> Term
isInt :: Term -> Term
isInt = Builder -> Term -> Term
un_app Builder
"is_int"
arrayConst :: Sort -> Sort -> Term -> Term
arrayConst :: Sort -> Sort -> Term -> Term
arrayConst Sort
itp Sort
rtp Term
c =
let tp :: Sort
tp = Sort -> Sort -> Sort
arraySort Sort
itp Sort
rtp
cast_app :: Builder
cast_app = [Builder] -> Builder
builder_list [ Builder
"as" , Builder
"const" , Sort -> Builder
unSort Sort
tp ]
in Builder -> [Term] -> Term
term_app Builder
cast_app [ Term
c ]
select :: Term -> Term -> Term
select :: Term -> Term -> Term
select = Builder -> Term -> Term -> Term
bin_app Builder
"select"
store :: Term -> Term -> Term -> Term
store :: Term -> Term -> Term -> Term
store Term
a Term
i Term
v = Builder -> [Term] -> Term
term_app Builder
"store" [Term
a,Term
i,Term
v]
bit0 :: Term
bit0 :: Term
bit0 = Builder -> Term
T Builder
"#b0"
bit1 :: Term
bit1 :: Term
bit1 = Builder -> Term
T Builder
"#b1"
bvbinary :: 1 <= w => NatRepr w -> BV.BV w -> Term
bvbinary :: forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Term
bvbinary NatRepr w
w0 BV w
u
| Bool
otherwise = Builder -> Term
T forall a b. (a -> b) -> a -> b
$ Builder
"#b" forall a. Semigroup a => a -> a -> a
<> Natural -> Builder
go (forall (n :: Natural). NatRepr n -> Natural
natValue NatRepr w
w0)
where go :: Natural -> Builder
go :: Natural -> Builder
go Natural
0 = forall a. Monoid a => a
mempty
go Natural
w =
let i :: Natural
i = Natural
w forall a. Num a => a -> a -> a
- Natural
1
b :: Builder
b :: Builder
b = if forall (w :: Natural). Natural -> BV w -> Bool
BV.testBit' Natural
i BV w
u then Builder
"1" else Builder
"0"
in Builder
b forall a. Semigroup a => a -> a -> a
<> Natural -> Builder
go Natural
i
bvdecimal :: 1 <= w => NatRepr w -> BV.BV w -> Term
bvdecimal :: forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Term
bvdecimal NatRepr w
w BV w
u = Builder -> Term
T forall a b. (a -> b) -> a -> b
$ forall a. Monoid a => [a] -> a
mconcat [ Builder
"(_ bv"
, forall a. Integral a => a -> Builder
Builder.decimal Integer
d
, Builder
" "
, forall a. Integral a => a -> Builder
Builder.decimal (forall (n :: Natural). NatRepr n -> Natural
natValue NatRepr w
w)
, Builder
")"]
where d :: Integer
d = forall (w :: Natural). BV w -> Integer
BV.asUnsigned BV w
u
bvhexadecimal :: 1 <= w => NatRepr w -> BV.BV w -> Term
bvhexadecimal :: forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Term
bvhexadecimal NatRepr w
w0 BV w
u
| Bool
otherwise = Builder -> Term
T forall a b. (a -> b) -> a -> b
$ Builder
"#x" forall a. Semigroup a => a -> a -> a
<> Natural -> Builder
go (forall (n :: Natural). NatRepr n -> Natural
natValue NatRepr w
w0)
where go :: Natural -> Builder
go :: Natural -> Builder
go Natural
0 = forall a. Monoid a => a
mempty
go Natural
w | Natural
w forall a. Ord a => a -> a -> Bool
< Natural
4 = forall a. HasCallStack => [Char] -> a
error [Char]
"bvhexadecimal width must be a multiple of 4."
go Natural
w =
let i :: Natural
i = Natural
w forall a. Num a => a -> a -> a
- Natural
4
charBits :: Integer
charBits = forall (w :: Natural). BV w -> Integer
BV.asUnsigned (forall (w' :: Natural) (w :: Natural).
Natural -> NatRepr w' -> BV w -> BV w'
BV.select' Natural
i (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @4) BV w
u)
c :: Char
c :: Char
c = Int -> Char
intToDigit forall a b. (a -> b) -> a -> b
$ forall a. Num a => Integer -> a
fromInteger Integer
charBits
in Char -> Builder
Builder.singleton Char
c forall a. Semigroup a => a -> a -> a
<> Natural -> Builder
go Natural
i
concat :: Term -> Term -> Term
concat :: Term -> Term -> Term
concat = Builder -> Term -> Term -> Term
bin_app Builder
"concat"
extract :: Natural -> Natural -> Term -> Term
Natural
i Natural
j Term
x
| Natural
i forall a. Ord a => a -> a -> Bool
< Natural
j = forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"End of extract (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Natural
i forall a. [a] -> [a] -> [a]
++ [Char]
") less than beginning (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Natural
j forall a. [a] -> [a] -> [a]
++ [Char]
")."
| Bool
otherwise =
let e :: Builder
e = Builder
"(_ extract " forall a. Semigroup a => a -> a -> a
<> forall a. Integral a => a -> Builder
Builder.decimal Natural
i forall a. Semigroup a => a -> a -> a
<> Builder
" " forall a. Semigroup a => a -> a -> a
<> forall a. Integral a => a -> Builder
Builder.decimal Natural
j forall a. Semigroup a => a -> a -> a
<> Builder
")"
in Builder -> Term -> Term
un_app Builder
e Term
x
bvnot :: Term -> Term
bvnot :: Term -> Term
bvnot = Builder -> Term -> Term
un_app Builder
"bvnot"
bvand :: Term -> [Term] -> Term
bvand :: Term -> [Term] -> Term
bvand = Builder -> Term -> [Term] -> Term
assoc_app Builder
"bvand"
bvor :: Term -> [Term] -> Term
bvor :: Term -> [Term] -> Term
bvor = Builder -> Term -> [Term] -> Term
assoc_app Builder
"bvor"
bvxor :: Term -> [Term] -> Term
bvxor :: Term -> [Term] -> Term
bvxor = Builder -> Term -> [Term] -> Term
assoc_app Builder
"bvxor"
bvneg :: Term -> Term
bvneg :: Term -> Term
bvneg = Builder -> Term -> Term
un_app Builder
"bvneg"
bvadd :: Term -> [Term] -> Term
bvadd :: Term -> [Term] -> Term
bvadd = Builder -> Term -> [Term] -> Term
assoc_app Builder
"bvadd"
bvsub :: Term -> Term -> Term
bvsub :: Term -> Term -> Term
bvsub = Builder -> Term -> Term -> Term
bin_app Builder
"bvsub"
bvmul :: Term -> [Term] -> Term
bvmul :: Term -> [Term] -> Term
bvmul = Builder -> Term -> [Term] -> Term
assoc_app Builder
"bvmul"
bvudiv :: Term -> Term -> Term
bvudiv :: Term -> Term -> Term
bvudiv = Builder -> Term -> Term -> Term
bin_app Builder
"bvudiv"
bvurem :: Term -> Term -> Term
bvurem :: Term -> Term -> Term
bvurem = Builder -> Term -> Term -> Term
bin_app Builder
"bvurem"
bvshl :: Term -> Term -> Term
bvshl :: Term -> Term -> Term
bvshl = Builder -> Term -> Term -> Term
bin_app Builder
"bvshl"
bvlshr :: Term -> Term -> Term
bvlshr :: Term -> Term -> Term
bvlshr = Builder -> Term -> Term -> Term
bin_app Builder
"bvlshr"
bvult :: Term -> Term -> Term
bvult :: Term -> Term -> Term
bvult = Builder -> Term -> Term -> Term
bin_app Builder
"bvult"
bvule :: Term -> Term -> Term
bvule :: Term -> Term -> Term
bvule = Builder -> Term -> Term -> Term
bin_app Builder
"bvule"
bvsle :: Term -> Term -> Term
bvsle :: Term -> Term -> Term
bvsle = Builder -> Term -> Term -> Term
bin_app Builder
"bvsle"
bvslt :: Term -> Term -> Term
bvslt :: Term -> Term -> Term
bvslt = Builder -> Term -> Term -> Term
bin_app Builder
"bvslt"
bvuge :: Term -> Term -> Term
bvuge :: Term -> Term -> Term
bvuge = Builder -> Term -> Term -> Term
bin_app Builder
"bvuge"
bvugt :: Term -> Term -> Term
bvugt :: Term -> Term -> Term
bvugt = Builder -> Term -> Term -> Term
bin_app Builder
"bvugt"
bvsge :: Term -> Term -> Term
bvsge :: Term -> Term -> Term
bvsge = Builder -> Term -> Term -> Term
bin_app Builder
"bvsge"
bvsgt :: Term -> Term -> Term
bvsgt :: Term -> Term -> Term
bvsgt = Builder -> Term -> Term -> Term
bin_app Builder
"bvsgt"
bvashr :: Term -> Term -> Term
bvashr :: Term -> Term -> Term
bvashr = Builder -> Term -> Term -> Term
bin_app Builder
"bvashr"
bvsdiv :: Term -> Term -> Term
bvsdiv :: Term -> Term -> Term
bvsdiv = Builder -> Term -> Term -> Term
bin_app Builder
"bvsdiv"
bvsrem :: Term -> Term -> Term
bvsrem :: Term -> Term -> Term
bvsrem = Builder -> Term -> Term -> Term
bin_app Builder
"bvsrem"
bvsignExtend :: Integer -> Term -> Term
bvsignExtend :: Integer -> Term -> Term
bvsignExtend Integer
w Term
x =
let e :: Builder
e = Builder
"(_ sign_extend " forall a. Semigroup a => a -> a -> a
<> forall a. Integral a => a -> Builder
Builder.decimal Integer
w forall a. Semigroup a => a -> a -> a
<> Builder
")"
in Builder -> Term -> Term
un_app Builder
e Term
x
bvzeroExtend :: Integer -> Term -> Term
bvzeroExtend :: Integer -> Term -> Term
bvzeroExtend Integer
w Term
x =
let e :: Builder
e = Builder
"(_ zero_extend " forall a. Semigroup a => a -> a -> a
<> forall a. Integral a => a -> Builder
Builder.decimal Integer
w forall a. Semigroup a => a -> a -> a
<> Builder
")"
in Builder -> Term -> Term
un_app Builder
e Term
x
newtype Command = Cmd Builder
setLogic :: Logic -> Command
setLogic :: Logic -> Command
setLogic (Logic Builder
nm) = Builder -> Command
Cmd forall a b. (a -> b) -> a -> b
$ Builder
"(set-logic " forall a. Semigroup a => a -> a -> a
<> Builder
nm forall a. Semigroup a => a -> a -> a
<> Builder
")"
setOption :: Text -> Text -> Command
setOption :: Text -> Text -> Command
setOption Text
nm Text
val = Builder -> Command
Cmd forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app_list Builder
"set-option" [Builder
":" forall a. Semigroup a => a -> a -> a
<> Text -> Builder
Builder.fromText Text
nm, Text -> Builder
Builder.fromText Text
val]
ppBool :: Bool -> Text
ppBool :: Bool -> Text
ppBool Bool
b = if Bool
b then Text
"true" else Text
"false"
setProduceModels :: Bool -> Command
setProduceModels :: Bool -> Command
setProduceModels Bool
b = Text -> Text -> Command
setOption Text
"produce-models" (Bool -> Text
ppBool Bool
b)
exit :: Command
exit :: Command
exit = Builder -> Command
Cmd Builder
"(exit)"
declareSort :: Symbol -> Integer -> Command
declareSort :: Text -> Integer -> Command
declareSort Text
v Integer
n = Builder -> Command
Cmd forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"declare-sort" [Text -> Builder
Builder.fromText Text
v, forall a. IsString a => [Char] -> a
fromString (forall a. Show a => a -> [Char]
show Integer
n)]
defineSort :: Symbol
-> [Symbol]
-> Sort
-> Command
defineSort :: Text -> [Text] -> Sort -> Command
defineSort Text
v [Text]
params Sort
d =
Builder -> Command
Cmd forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"define-sort" [ Text -> Builder
Builder.fromText Text
v
, [Builder] -> Builder
builder_list (Text -> Builder
Builder.fromText forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Text]
params)
, Sort -> Builder
unSort Sort
d
]
declareConst :: Text -> Sort -> Command
declareConst :: Text -> Sort -> Command
declareConst Text
v Sort
tp = Builder -> Command
Cmd forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"declare-const" [Text -> Builder
Builder.fromText Text
v, Sort -> Builder
unSort Sort
tp]
declareFun :: Text -> [Sort] -> Sort -> Command
declareFun :: Text -> [Sort] -> Sort -> Command
declareFun Text
v [Sort]
argSorts Sort
retSort = Builder -> Command
Cmd forall a b. (a -> b) -> a -> b
$
Builder -> [Builder] -> Builder
app Builder
"declare-fun" [ Text -> Builder
Builder.fromText Text
v
, [Builder] -> Builder
builder_list forall a b. (a -> b) -> a -> b
$ Sort -> Builder
unSort forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Sort]
argSorts
, Sort -> Builder
unSort Sort
retSort
]
defineFun :: Text -> [(Text,Sort)] -> Sort -> Term -> Command
defineFun :: Text -> [(Text, Sort)] -> Sort -> Term -> Command
defineFun Text
f [(Text, Sort)]
args Sort
return_type Term
e =
let resolveArg :: (Text, Sort) -> Builder
resolveArg (Text
var, Sort
tp) = Builder -> [Builder] -> Builder
app (Text -> Builder
Builder.fromText Text
var) [Sort -> Builder
unSort Sort
tp]
in Builder -> Command
Cmd forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"define-fun" [ Text -> Builder
Builder.fromText Text
f
, [Builder] -> Builder
builder_list ((Text, Sort) -> Builder
resolveArg forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Text, Sort)]
args)
, Sort -> Builder
unSort Sort
return_type
, Term -> Builder
renderTerm Term
e
]
assert :: Term -> Command
assert :: Term -> Command
assert Term
p = Builder -> Command
Cmd forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"assert" [Term -> Builder
renderTerm Term
p]
assertNamed :: Term -> Text -> Command
assertNamed :: Term -> Text -> Command
assertNamed Term
p Text
nm =
Builder -> Command
Cmd forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"assert"
[[Builder] -> Builder
builder_list [Text -> Builder
Builder.fromText Text
"!", Term -> Builder
renderTerm Term
p, Text -> Builder
Builder.fromText Text
":named", Text -> Builder
Builder.fromText Text
nm]]
checkSat :: Command
checkSat :: Command
checkSat = Builder -> Command
Cmd Builder
"(check-sat)"
checkSatAssuming :: [Term] -> Command
checkSatAssuming :: [Term] -> Command
checkSatAssuming [Term]
l = Builder -> Command
Cmd forall a b. (a -> b) -> a -> b
$ Builder
"(check-sat-assuming " forall a. Semigroup a => a -> a -> a
<> [Builder] -> Builder
builder_list (Term -> Builder
renderTerm forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Term]
l) forall a. Semigroup a => a -> a -> a
<> Builder
")"
checkSatWithAssumptions :: [Text] -> Command
checkSatWithAssumptions :: [Text] -> Command
checkSatWithAssumptions [Text]
nms = Builder -> Command
Cmd forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"check-sat-assuming" [[Builder] -> Builder
builder_list (forall a b. (a -> b) -> [a] -> [b]
map Text -> Builder
Builder.fromText [Text]
nms)]
getModel :: Command
getModel :: Command
getModel = Builder -> Command
Cmd Builder
"(get-model)"
getUnsatAssumptions :: Command
getUnsatAssumptions :: Command
getUnsatAssumptions = Builder -> Command
Cmd Builder
"(get-unsat-assumptions)"
getUnsatCore :: Command
getUnsatCore :: Command
getUnsatCore = Builder -> Command
Cmd Builder
"(get-unsat-core)"
getAbduct :: Text -> Term -> Command
getAbduct :: Text -> Term -> Command
getAbduct Text
nm Term
p = Builder -> Command
Cmd forall a b. (a -> b) -> a -> b
$ Builder
"(get-abduct " forall a. Semigroup a => a -> a -> a
<> Text -> Builder
Builder.fromText Text
nm forall a. Semigroup a => a -> a -> a
<> Builder
" " forall a. Semigroup a => a -> a -> a
<> Term -> Builder
renderTerm Term
p forall a. Semigroup a => a -> a -> a
<> Builder
")"
getAbductNext :: Command
getAbductNext :: Command
getAbductNext = Builder -> Command
Cmd Builder
"(get-abduct-next)"
synthFun :: Text -> [(Text, Sort)] -> Sort -> Command
synthFun :: Text -> [(Text, Sort)] -> Sort -> Command
synthFun Text
f [(Text, Sort)]
args Sort
ret_tp = Builder -> Command
Cmd forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"synth-fun"
[ Text -> Builder
Builder.fromText Text
f
, [Builder] -> Builder
builder_list forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\(Text
var, Sort
tp) -> Builder -> [Builder] -> Builder
app (Text -> Builder
Builder.fromText Text
var) [Sort -> Builder
unSort Sort
tp]) [(Text, Sort)]
args
, Sort -> Builder
unSort Sort
ret_tp
]
declareVar :: Text -> Sort -> Command
declareVar :: Text -> Sort -> Command
declareVar Text
v Sort
tp = Builder -> Command
Cmd forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"declare-var" [Text -> Builder
Builder.fromText Text
v, Sort -> Builder
unSort Sort
tp]
constraint :: Term -> Command
constraint :: Term -> Command
constraint Term
p = Builder -> Command
Cmd forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"constraint" [Term -> Builder
renderTerm Term
p]
checkSynth :: Command
checkSynth :: Command
checkSynth = Builder -> Command
Cmd Builder
"(check-synth)\n"
getValue :: [Term] -> Command
getValue :: [Term] -> Command
getValue [Term]
values = Builder -> Command
Cmd forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"get-value" [[Builder] -> Builder
builder_list (Term -> Builder
renderTerm forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Term]
values)]
resetAssertions :: Command
resetAssertions :: Command
resetAssertions = Builder -> Command
Cmd Builder
"(reset-assertions)"
push :: Integer -> Command
push :: Integer -> Command
push Integer
n = Builder -> Command
Cmd forall a b. (a -> b) -> a -> b
$ Builder
"(push " forall a. Semigroup a => a -> a -> a
<> forall a. Integral a => a -> Builder
Builder.decimal Integer
n forall a. Semigroup a => a -> a -> a
<> Builder
")"
pop :: Integer -> Command
pop :: Integer -> Command
pop Integer
n = Builder -> Command
Cmd forall a b. (a -> b) -> a -> b
$ Builder
"(pop " forall a. Semigroup a => a -> a -> a
<> forall a. Integral a => a -> Builder
Builder.decimal Integer
n forall a. Semigroup a => a -> a -> a
<> Builder
")"
data SMTInfoFlag =
Name
| Version
| ErrorBehavior
| InfoKeyword Text
deriving (Typeable SMTInfoFlag
SMTInfoFlag -> DataType
SMTInfoFlag -> Constr
(forall b. Data b => b -> b) -> SMTInfoFlag -> SMTInfoFlag
forall a.
Typeable a
-> (forall (c :: Type -> Type).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: Type -> Type).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: Type -> Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: Type -> Type).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> SMTInfoFlag -> u
forall u. (forall d. Data d => d -> u) -> SMTInfoFlag -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SMTInfoFlag -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SMTInfoFlag -> r
forall (m :: Type -> Type).
Monad m =>
(forall d. Data d => d -> m d) -> SMTInfoFlag -> m SMTInfoFlag
forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SMTInfoFlag -> m SMTInfoFlag
forall (c :: Type -> Type).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SMTInfoFlag
forall (c :: Type -> Type).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SMTInfoFlag -> c SMTInfoFlag
forall (t :: Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SMTInfoFlag)
forall (t :: Type -> Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SMTInfoFlag)
gmapMo :: forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SMTInfoFlag -> m SMTInfoFlag
$cgmapMo :: forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SMTInfoFlag -> m SMTInfoFlag
gmapMp :: forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SMTInfoFlag -> m SMTInfoFlag
$cgmapMp :: forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SMTInfoFlag -> m SMTInfoFlag
gmapM :: forall (m :: Type -> Type).
Monad m =>
(forall d. Data d => d -> m d) -> SMTInfoFlag -> m SMTInfoFlag
$cgmapM :: forall (m :: Type -> Type).
Monad m =>
(forall d. Data d => d -> m d) -> SMTInfoFlag -> m SMTInfoFlag
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SMTInfoFlag -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SMTInfoFlag -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> SMTInfoFlag -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> SMTInfoFlag -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SMTInfoFlag -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SMTInfoFlag -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SMTInfoFlag -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SMTInfoFlag -> r
gmapT :: (forall b. Data b => b -> b) -> SMTInfoFlag -> SMTInfoFlag
$cgmapT :: (forall b. Data b => b -> b) -> SMTInfoFlag -> SMTInfoFlag
dataCast2 :: forall (t :: Type -> Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SMTInfoFlag)
$cdataCast2 :: forall (t :: Type -> Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SMTInfoFlag)
dataCast1 :: forall (t :: Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SMTInfoFlag)
$cdataCast1 :: forall (t :: Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SMTInfoFlag)
dataTypeOf :: SMTInfoFlag -> DataType
$cdataTypeOf :: SMTInfoFlag -> DataType
toConstr :: SMTInfoFlag -> Constr
$ctoConstr :: SMTInfoFlag -> Constr
gunfold :: forall (c :: Type -> Type).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SMTInfoFlag
$cgunfold :: forall (c :: Type -> Type).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SMTInfoFlag
gfoldl :: forall (c :: Type -> Type).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SMTInfoFlag -> c SMTInfoFlag
$cgfoldl :: forall (c :: Type -> Type).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SMTInfoFlag -> c SMTInfoFlag
Data, SMTInfoFlag -> SMTInfoFlag -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SMTInfoFlag -> SMTInfoFlag -> Bool
$c/= :: SMTInfoFlag -> SMTInfoFlag -> Bool
== :: SMTInfoFlag -> SMTInfoFlag -> Bool
$c== :: SMTInfoFlag -> SMTInfoFlag -> Bool
Eq, Eq SMTInfoFlag
SMTInfoFlag -> SMTInfoFlag -> Bool
SMTInfoFlag -> SMTInfoFlag -> Ordering
SMTInfoFlag -> SMTInfoFlag -> SMTInfoFlag
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: SMTInfoFlag -> SMTInfoFlag -> SMTInfoFlag
$cmin :: SMTInfoFlag -> SMTInfoFlag -> SMTInfoFlag
max :: SMTInfoFlag -> SMTInfoFlag -> SMTInfoFlag
$cmax :: SMTInfoFlag -> SMTInfoFlag -> SMTInfoFlag
>= :: SMTInfoFlag -> SMTInfoFlag -> Bool
$c>= :: SMTInfoFlag -> SMTInfoFlag -> Bool
> :: SMTInfoFlag -> SMTInfoFlag -> Bool
$c> :: SMTInfoFlag -> SMTInfoFlag -> Bool
<= :: SMTInfoFlag -> SMTInfoFlag -> Bool
$c<= :: SMTInfoFlag -> SMTInfoFlag -> Bool
< :: SMTInfoFlag -> SMTInfoFlag -> Bool
$c< :: SMTInfoFlag -> SMTInfoFlag -> Bool
compare :: SMTInfoFlag -> SMTInfoFlag -> Ordering
$ccompare :: SMTInfoFlag -> SMTInfoFlag -> Ordering
Ord, forall x. Rep SMTInfoFlag x -> SMTInfoFlag
forall x. SMTInfoFlag -> Rep SMTInfoFlag x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep SMTInfoFlag x -> SMTInfoFlag
$cfrom :: forall x. SMTInfoFlag -> Rep SMTInfoFlag x
Generic, Int -> SMTInfoFlag -> ShowS
[SMTInfoFlag] -> ShowS
SMTInfoFlag -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [SMTInfoFlag] -> ShowS
$cshowList :: [SMTInfoFlag] -> ShowS
show :: SMTInfoFlag -> [Char]
$cshow :: SMTInfoFlag -> [Char]
showsPrec :: Int -> SMTInfoFlag -> ShowS
$cshowsPrec :: Int -> SMTInfoFlag -> ShowS
Show, Typeable)
flagToSExp :: SMTInfoFlag -> Text
flagToSExp :: SMTInfoFlag -> Text
flagToSExp = (Char -> Text -> Text
cons Char
':') forall b c a. (b -> c) -> (a -> b) -> a -> c
.
\case
SMTInfoFlag
Name -> Text
"name"
SMTInfoFlag
Version -> Text
"version"
SMTInfoFlag
ErrorBehavior -> Text
"error-behavior"
InfoKeyword Text
s -> Text
s
getInfo :: SMTInfoFlag -> Command
getInfo :: SMTInfoFlag -> Command
getInfo SMTInfoFlag
flag = Builder -> Command
Cmd forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"get-info" [Text -> Builder
Builder.fromText (SMTInfoFlag -> Text
flagToSExp SMTInfoFlag
flag)]
getVersion :: Command
getVersion :: Command
getVersion = SMTInfoFlag -> Command
getInfo SMTInfoFlag
Version
getName :: Command
getName :: Command
getName = SMTInfoFlag -> Command
getInfo SMTInfoFlag
Name
getErrorBehavior :: Command
getErrorBehavior :: Command
getErrorBehavior = SMTInfoFlag -> Command
getInfo SMTInfoFlag
ErrorBehavior