    {-|
    This module defines types and operations for generating SMTLIB2 files.

    It does not depend on the rest of What4 so that it can be used
    directly by clients interested in generating SMTLIB without depending
    on the What4 formula interface.  All the type constructors are exposed
    so that clients can generate new values that are not exposed through
    this interface.
    -}

    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE DeriveDataTypeable #-}
    {-# LANGUAGE DeriveGeneric #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE GeneralizedNewtypeDeriving #-}
    {-# LANGUAGE LambdaCase #-}
    {-# LANGUAGE OverloadedStrings #-}
    {-# LANGUAGE TypeApplications #-}
    {-# LANGUAGE TypeOperators #-}
    module What4.Protocol.SMTLib2.Syntax
      ( -- * Commands
        Command(..)
      , setLogic
      , setOption
      , setProduceModels
      , SMTInfoFlag(..)
      , getInfo
      , getVersion
      , getName
      , getErrorBehavior
      , exit
         -- * Declarations
      , declareSort
      , defineSort
      , declareConst
      , declareFun
      , defineFun
      , Symbol
        -- * Assertions and checking
      , checkSat
      , checkSatAssuming
      , checkSatWithAssumptions
      , getModel
      , getValue
      , push
      , pop
      , resetAssertions
      , assert
      , assertNamed
      , getUnsatAssumptions
      , getUnsatCore
      , getAbduct
      , getAbductNext
        -- * SyGuS
      , synthFun
      , declareVar
      , constraint
      , checkSynth
        -- * Logic
      , Logic(..)
      , qf_bv
      , allSupported
      , allLogic
      , hornLogic
        -- * Sort
      , Sort(..)
      , boolSort
      , bvSort
      , intSort
      , realSort
      , varSort
        -- * Term
      , Term(..)
      , un_app
      , bin_app
      , term_app
      , pairwise_app
      , namedTerm
      , builder_list
        -- * Core theory
      , true
      , false
      , not
      , implies
      , and
      , or
      , xor
      , eq
      , distinct
      , ite
      , forall_
      , exists_
      , letBinder
        -- * @Ints@, @Reals@, @Reals_Ints@ theories
      , negate
      , numeral
      , decimal
      , sub
      , add
      , mul
      , div
      , (./)
      , mod
      , abs
      , le
      , lt
      , ge
      , gt
      , toReal
      , toInt
      , isInt
        -- * Bitvector theory and extensions
      , concat
      , extract
      , bvnot
      , bvand
      , bvor
      , bvxor
      , bvneg
      , bvadd
      , bvsub
      , bvmul
      , bvudiv
      , bvurem
      , bvshl
      , bvlshr
      , bvult
        -- ** Extensions provided by QF_BV
      , bit0
      , bit1
      , bvbinary
      , bvdecimal
      , bvhexadecimal
      , bvashr
      , bvslt
      , bvsle
      , bvule
      , bvsgt
      , bvsge
      , bvugt
      , bvuge
      , bvsdiv
      , bvsrem
      , bvsignExtend
      , bvzeroExtend
        -- * Array theory
      , 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
    "(" Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Builder
    o Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> [Builder] -> Builder
    forall {a}. (IsString a, Semigroup a) => [a] -> a
    go [Builder]
    args
      where go :: [a] -> a
    go [] = a
    ")"
            go (a
    f:[a]
    r) = a
    " " a -> a -> a
    forall a. Semigroup a => a -> a -> a
    <> a
    f a -> a -> a
    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

    ------------------------------------------------------------------------
    -- Logic

    -- | Identifies the set of predefined sorts and operators available.
    newtype Logic = Logic Builder

    -- | Use the QF_BV logic
    qf_bv :: Logic
    qf_bv :: Logic
    qf_bv = Builder -> Logic
    Logic Builder
    "QF_BV"

    -- | Set the logic to all supported logics.
    allSupported :: Logic
    allSupported :: Logic
    allSupported = Builder -> Logic
    Logic Builder
    "ALL_SUPPORTED"
    {-# DEPRECATED allSupported "Use allLogic instead" #-}

    -- | Set the logic to all supported logics.
    allLogic :: Logic
    allLogic :: Logic
    allLogic = Builder -> Logic
    Logic Builder
    "ALL"

    -- | Use the Horn logic
    hornLogic :: Logic
    hornLogic :: Logic
    hornLogic = Builder -> Logic
    Logic Builder
    "HORN"

    ------------------------------------------------------------------------
    -- Symbol

    type Symbol = Text

    ------------------------------------------------------------------------
    -- Sort

    -- | Sort for SMTLIB expressions
    newtype Sort = Sort { Sort -> Builder
    unSort :: Builder }

    -- | Create a sort from a symbol name
    varSort :: Symbol -> Sort
    varSort :: Text -> Sort
    varSort = Builder -> Sort
    Sort (Builder -> Sort) -> (Text -> Builder) -> Text -> Sort
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Text -> Builder
    Builder.fromText

    -- | Booleans
    boolSort :: Sort
    boolSort :: Sort
    boolSort = Builder -> Sort
    Sort Builder
    "Bool"

    -- | Bitvectors with the given number of bits.
    bvSort :: Natural -> Sort
    bvSort :: Natural -> Sort
    bvSort Natural
    w | Natural
    w Natural -> Natural -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Natural
    1 = Builder -> Sort
    Sort (Builder -> Sort) -> Builder -> Sort
    forall a b. (a -> b) -> a -> b
    $ Builder
    "(_ BitVec " Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> [Char] -> Builder
    forall a. IsString a => [Char] -> a
    fromString (Natural -> [Char]
    forall a. Show a => a -> [Char]
    show Natural
    w) Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Builder
    ")"
             | Bool
    otherwise = [Char] -> Sort
    forall a. HasCallStack => [Char] -> a
    error [Char]
    "bvSort expects a positive number."

    -- | Integers
    intSort :: Sort
    intSort :: Sort
    intSort = Builder -> Sort
    Sort Builder
    "Int"

    -- | Real numbers
    realSort :: Sort
    realSort :: Sort
    realSort = Builder -> Sort
    Sort Builder
    "Real"

    -- | @arraySort a b@ denotes the set of functions from @a@ to be @b@.
    arraySort :: Sort -> Sort -> Sort
    arraySort :: Sort -> Sort -> Sort
    arraySort (Sort Builder
    i) (Sort Builder
    v) = Builder -> Sort
    Sort (Builder -> Sort) -> Builder -> Sort
    forall a b. (a -> b) -> a -> b
    $ Builder
    "(Array " Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Builder
    i Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Builder
    " " Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Builder
    v Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Builder
    ")"

    ------------------------------------------------------------------------
    -- Term

    -- | Denotes an expression in the SMT solver
    newtype Term = T { Term -> Builder
    renderTerm :: Builder }
      deriving ([Char] -> Term
    ([Char] -> Term) -> IsString Term
    forall a. ([Char] -> a) -> IsString a
    $cfromString :: [Char] -> Term
    fromString :: [Char] -> Term
    IsString, Semigroup Term
    Term
    Semigroup Term =>
    Term -> (Term -> Term -> Term) -> ([Term] -> Term) -> Monoid Term
    [Term] -> Term
    Term -> Term -> Term
    forall a.
    Semigroup a =>
    a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
    $cmempty :: Term
    mempty :: Term
    $cmappend :: Term -> Term -> Term
    mappend :: Term -> Term -> Term
    $cmconcat :: [Term] -> Term
    mconcat :: [Term] -> Term
    Monoid, NonEmpty Term -> Term
    Term -> Term -> Term
    (Term -> Term -> Term)
    -> (NonEmpty Term -> Term)
    -> (forall b. Integral b => b -> Term -> Term)
    -> Semigroup 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
    $c<> :: Term -> Term -> Term
    <> :: Term -> Term -> Term
    $csconcat :: NonEmpty Term -> Term
    sconcat :: NonEmpty Term -> Term
    $cstimes :: forall b. Integral b => b -> Term -> Term
    stimes :: forall b. Integral b => b -> Term -> Term
    Semigroup)

    -- | Construct an expression with the given operator and list of arguments.
    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 (Term -> Builder) -> [Term] -> [Builder]
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Term]
    args))

    -- | Construct an expression with the given operator and single argument.
    un_app :: Builder -> Term -> Term
    un_app :: Builder -> Term -> Term
    un_app Builder
    o (T Builder
    x) = Builder -> Term
    T (Builder -> Term) -> Builder -> Term
    forall a b. (a -> b) -> a -> b
    $ [Builder] -> Builder
    forall a. Monoid a => [a] -> a
    mconcat [Builder
    "(", Builder
    o, Builder
    " ", Builder
    x, Builder
    ")"]

    -- | Construct an expression with the given operator and two arguments.
    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 (Builder -> Term) -> Builder -> Term
    forall a b. (a -> b) -> a -> b
    $ [Builder] -> Builder
    forall a. Monoid a => [a] -> a
    mconcat [Builder
    "(", Builder
    o, Builder
    " ", Builder
    x, Builder
    " ", Builder
    y, Builder
    ")"]

    -- | Construct a chainable term with the given relation
    --
    -- @chain_app p [x1, x2, ..., xn]@ is equivalent to
    -- @p x1 x2 /\ p x2 x3 /\ ... /\ p x(n-1) xn@.
    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]
    _ = [Char] -> Term
    forall a. HasCallStack => [Char] -> a
    error ([Char] -> Term) -> [Char] -> Term
    forall a b. (a -> b) -> a -> b
    $ Builder -> [Char]
    forall a. Show a => a -> [Char]
    show Builder
    f [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " expects two or more arguments."

    -- | Build a term for a left-associative operator.
    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
    tTerm -> [Term] -> [Term]
    forall a. a -> [a] -> [a]
    :[Term]
    l)

    -- | Append a "name" to a term so that it will be printed when
    -- @(get-assignment)@ is called.
    namedTerm :: Term -> Text -> Term
    namedTerm :: Term -> Text -> Term
    namedTerm (T Builder
    x) Text
    nm = Builder -> Term
    T (Builder -> Term) -> Builder -> Term
    forall a b. (a -> b) -> a -> b
    $ Builder
    "(! " Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Builder
    x Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Builder
    " :named " Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Text -> Builder
    Builder.fromText Text
    nm Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Builder
    ")"

    ------------------------------------------------------------------------
    -- Core theory

    -- | @true@ Boolean term
    true :: Term
    true :: Term
    true = Builder -> Term
    T Builder
    "true"

    -- | @false@ Boolean term
    false :: Term
    false :: Term
    false = Builder -> Term
    T Builder
    "false"

    -- | Complement a Boolean
    not :: Term -> Term
    not :: Term -> Term
    not = Builder -> Term -> Term
    un_app Builder
    "not"

    -- | @implies c r@ is equivalent to @c1 => c2 => .. cn => r@.
    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 [Term] -> [Term] -> [Term]
    forall a. [a] -> [a] -> [a]
    ++ [Term
    t])

    -- | Conjunction of all terms
    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

    -- | Disjunction of all terms
    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 of all terms
    xor :: [Term] -> Term
    xor :: [Term] -> Term
    xor l :: [Term]
    l@(Term
    _:Term
    _:[Term]
    _) = Builder -> [Term] -> Term
    term_app Builder
    "xor" [Term]
    l
    xor [Term]
    _ = [Char] -> Term
    forall a. HasCallStack => [Char] -> a
    error [Char]
    "xor expects two or more arguments."

    -- | Return true if all terms are equal.
    eq :: [Term] -> Term
    eq :: [Term] -> Term
    eq = Builder -> [Term] -> Term
    chain_app Builder
    "="

    -- | Construct a chainable term with the given relation
    --
    -- @pairwise_app p [x1, x2, ..., xn]@ is equivalent to
    -- \forall_{i,j} p x_i x_j@.
    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

    -- | Asserts that each term in the list is unique.
    distinct :: [Term] -> Term
    distinct :: [Term] -> Term
    distinct = Builder -> [Term] -> Term
    pairwise_app Builder
    "distinct"

    -- | Create an if-then-else expression.
    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
    "(" Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Text -> Builder
    Builder.fromText Text
    nm Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Builder
    " " Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Sort -> Builder
    unSort Sort
    tp Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Builder
    ")"

    -- | @forall_ vars t@ denotes a predicate that holds if @t@ for every valuation of the
    -- variables in @vars@.
    forall_ :: [(Text, Sort)] -> Term -> Term
    forall_ :: [(Text, Sort)] -> Term -> Term
    forall_ [] Term
    r = Term
    r
    forall_ [(Text, Sort)]
    vars Term
    r =
      Builder -> Term
    T (Builder -> Term) -> Builder -> Term
    forall a b. (a -> b) -> a -> b
    $ Builder -> [Builder] -> Builder
    app Builder
    "forall" [[Builder] -> Builder
    builder_list ((Text, Sort) -> Builder
    varBinding ((Text, Sort) -> Builder) -> [(Text, Sort)] -> [Builder]
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> [(Text, Sort)]
    vars), Term -> Builder
    renderTerm Term
    r]

    -- | @exists_ vars t@ denotes a predicate that holds if @t@ for some valuation of the
    -- variables in @vars@.
    exists_ :: [(Text, Sort)] -> Term -> Term
    exists_ :: [(Text, Sort)] -> Term -> Term
    exists_ [] Term
    r = Term
    r
    exists_ [(Text, Sort)]
    vars Term
    r =
      Builder -> Term
    T (Builder -> Term) -> Builder -> Term
    forall a b. (a -> b) -> a -> b
    $ Builder -> [Builder] -> Builder
    app Builder
    "exists" [[Builder] -> Builder
    builder_list ((Text, Sort) -> Builder
    varBinding ((Text, Sort) -> Builder) -> [(Text, Sort)] -> [Builder]
    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]

    -- | Create a let binding.  NOTE: SMTLib2 defines this to be
    --   a \"parallel\" let, which means that the bound variables
    --   are NOT in scope in the right-hand sides of other
    --   bindings, even syntactically-later ones.
    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 ((Text, Term) -> Builder) -> [(Text, Term)] -> [Builder]
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> [(Text, Term)]
    vars), Term -> Builder
    renderTerm Term
    r])

    ------------------------------------------------------------------------
    -- Reals/Int/Real_Ints theories

    -- | Negate an integer or real number.
    negate :: Term -> Term
    negate :: Term -> Term
    negate = Builder -> Term -> Term
    un_app Builder
    "-"

    -- | Create a numeral literal from the given integer.
    numeral :: Integer -> Term
    numeral :: Integer -> Term
    numeral Integer
    i | Integer
    i Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Integer
    0 = Builder -> Term
    T (Builder -> Term) -> Builder -> Term
    forall a b. (a -> b) -> a -> b
    $ Integer -> Builder
    forall a. Integral a => a -> Builder
    Builder.decimal Integer
    i
              | Bool
    otherwise = Term -> Term
    negate (Builder -> Term
    T (Integer -> Builder
    forall a. Integral a => a -> Builder
    Builder.decimal (Integer -> Integer
    forall a. Num a => a -> a
    Prelude.negate Integer
    i)))

    -- | Create a literal as a real from the given integer.
    decimal :: Integer -> Term
    decimal :: Integer -> Term
    decimal Integer
    i | Integer
    i Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Integer
    0 = Builder -> Term
    T (Builder -> Term) -> Builder -> Term
    forall a b. (a -> b) -> a -> b
    $ Integer -> Builder
    forall a. Integral a => a -> Builder
    Builder.decimal Integer
    i Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Builder
    ".0"
              | Bool
    otherwise = Term -> Term
    negate (Term -> Term) -> Term -> Term
    forall a b. (a -> b) -> a -> b
    $ Builder -> Term
    T (Builder -> Term) -> Builder -> Term
    forall a b. (a -> b) -> a -> b
    $ Integer -> Builder
    forall a. Integral a => a -> Builder
    Builder.decimal (Integer -> Integer
    forall a. Num a => a -> a
    Prelude.negate Integer
    i) Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Builder
    ".0"

    -- | @sub x1 [x2, ..., xn]@ with n >= 1 returns
    -- @x1@ minus @x2 + ... + xn@.
    --
    -- The terms are expected to have type @Int@ or @Real@.
    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
    xTerm -> [Term] -> [Term]
    forall a. a -> [a] -> [a]
    :[Term]
    l)

    -- | @add [x1, x2, ..., xn]@ with n >= 2 returns
    -- @x1@ minus @x2 + ... + xn@.
    --
    -- The terms are expected to have type @Int@ or @Real@.
    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

    -- | @add [x1, x2, ..., xn]@ with n >= 2 returns
    -- @x1@ minus @x2 + ... + xn@.
    --
    -- The terms are expected to have type @Int@ or @Real@.
    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 x1 [x2, ..., xn]@ with n >= 1 returns
    -- @x1@ div @x2 * ... * xn@.
    --
    -- The terms are expected to have type @Int@.
    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
    xTerm -> [Term] -> [Term]
    forall a. a -> [a] -> [a]
    :[Term]
    l)

    -- | @x1 ./ [x2, ..., xn]@ with n >= 1 returns
    -- @x1@ / @x2 * ... * xn@.
    (./) :: Term -> [Term] -> Term
    Term
    x ./ :: Term -> [Term] -> Term
    ./ [] = Term
    x
    Term
    x ./ [Term]
    l = Builder -> [Term] -> Term
    term_app Builder
    "/" (Term
    xTerm -> [Term] -> [Term]
    forall a. a -> [a] -> [a]
    :[Term]
    l)

    -- | @mod x1 x2@ returns x1 - x2 * (x1 `div` [x2])@.
    --
    -- The terms are expected to have type @Int@.
    mod :: Term -> Term -> Term
    mod :: Term -> Term -> Term
    mod = Builder -> Term -> Term -> Term
    bin_app Builder
    "mod"

    -- | @abs x1@ returns the absolute value of @x1@.
    --
    -- The term is expected to have type @Int@.
    abs :: Term -> Term
    abs :: Term -> Term
    abs = Builder -> Term -> Term
    un_app Builder
    "abs"

    -- | Less than or equal over a chained list of terms.
    --
    -- @le [x1, x2, ..., xn]@ is equivalent to
    -- @x1 <= x2 /\ x2 <= x3 /\ ... /\ x(n-1) <= xn@.
    --
    -- This is defined in the Reals, Ints, and Reals_Ints theories,
    -- and the number of elements must be at least 2.
    --
    -- With a strict interpretation of the SMTLIB standard, the terms should
    -- be all of the same type (i.e. "Int" or Real"), but existing solvers appear
    -- to implicitly all mixed terms.
    le :: [Term] -> Term
    le :: [Term] -> Term
    le = Builder -> [Term] -> Term
    chain_app Builder
    "<="

    -- | Less than over a chained list of terms.
    --
    -- @lt [x1, x2, ..., xn]@ is equivalent to
    -- @x1 < x2 /\ x2 < x3 /\ ... /\ x(n-1) < xn@.
    --
    -- With a strict interpretation of the SMTLIB standard, the terms should
    -- be all of the same type (i.e. "Int" or Real"), but existing solvers appear
    -- to implicitly all mixed terms.
    lt :: [Term] -> Term
    lt :: [Term] -> Term
    lt = Builder -> [Term] -> Term
    chain_app Builder
    "<"

    -- | Greater than or equal over a chained list of terms.
    --
    -- @ge [x1, x2, ..., xn]@ is equivalent to
    -- @x1 >= x2 /\ x2 >= x3 /\ ... /\ x(n-1) >= xn@.
    --
    -- With a strict interpretation of the SMTLIB standard, the terms should
    -- be all of the same type (i.e. "Int" or Real"), but existing solvers appear
    -- to implicitly all mixed terms.
    ge :: [Term] -> Term
    ge :: [Term] -> Term
    ge = Builder -> [Term] -> Term
    chain_app Builder
    ">="

    -- | Greater than over a chained list of terms.
    --
    -- @gt [x1, x2, ..., xn]@ is equivalent to
    -- @x1 > x2 /\ x2 > x3 /\ ... /\ x(n-1) > xn@.
    --
    -- With a strict interpretation of the SMTLIB standard, the terms should
    -- be all of the same type (i.e. "Int" or Real"), but existing solvers appear
    -- to implicitly all mixed terms.
    gt :: [Term] -> Term
    gt :: [Term] -> Term
    gt = Builder -> [Term] -> Term
    chain_app Builder
    ">"

    -- | Maps a term with type @Int@ to @Real@.
    toReal :: Term -> Term
    toReal :: Term -> Term
    toReal = Builder -> Term -> Term
    un_app Builder
    "to_real"

    -- | Returns the largest integer not larger than the given real term.
    toInt :: Term -> Term
    toInt :: Term -> Term
    toInt = Builder -> Term -> Term
    un_app Builder
    "to_int"

    -- | Returns true if this is an integer.
    isInt :: Term -> Term
    isInt :: Term -> Term
    isInt = Builder -> Term -> Term
    un_app Builder
    "is_int"

    ------------------------------------------------------------------------
    -- Array theory

    -- | @arrayConst t1 t2 c@ generates an array with index type `t1` and
    -- value type `t2` that always returns `c`.
    --
    -- This uses the non-standard SMTLIB2 syntax
    -- @((as const (Array t1 t2)) c)@ which is supported by CVC4, CVC5, and Z3
    -- (and perhaps others).
    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 a i@ denotes the value of @a@ at @i@.
    select :: Term -> Term -> Term
    select :: Term -> Term -> Term
    select = Builder -> Term -> Term -> Term
    bin_app Builder
    "select"

    -- | @store a i v@ denotes the array whose valuation is @v@ at index @i@ and
    -- @select a j@ at every other index @j@.
    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]

    ------------------------------------------------------------------------
    -- Bitvector theory

    -- | A 1-bit bitvector representing @0@.
    bit0 :: Term
    bit0 :: Term
    bit0 = Builder -> Term
    T Builder
    "#b0"

    -- | A 1-bit bitvector representing @1@.
    bit1 :: Term
    bit1 :: Term
    bit1 = Builder -> Term
    T Builder
    "#b1"

    -- | @bvbinary w x@ constructs a bitvector term with width @w@ equal
    -- to @x `mod` 2^w@.
    --
    -- The width @w@ must be positive.
    --
    -- The literal uses a binary notation.
    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 (Builder -> Term) -> Builder -> Term
    forall a b. (a -> b) -> a -> b
    $ Builder
    "#b" Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Natural -> Builder
    go (NatRepr w -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    natValue NatRepr w
    w0)
      where go :: Natural -> Builder
            go :: Natural -> Builder
    go Natural
    0 = Builder
    forall a. Monoid a => a
    mempty
            go Natural
    w =
              let i :: Natural
    i = Natural
    w Natural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    - Natural
    1
                  b :: Builder
                  b :: Builder
    b = if Natural -> BV w -> Bool
    forall (w :: Natural). Natural -> BV w -> Bool
    BV.testBit' Natural
    i BV w
    u then Builder
    "1" else Builder
    "0"
               in Builder
    b Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Natural -> Builder
    go Natural
    i

    -- | @bvdecimal x w@ constructs a bitvector term with width @w@ equal to @x `mod` 2^w@.
    --
    -- The width @w@ must be positive.
    --
    -- The literal uses a decimal notation.
    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 (Builder -> Term) -> Builder -> Term
    forall a b. (a -> b) -> a -> b
    $ [Builder] -> Builder
    forall a. Monoid a => [a] -> a
    mconcat [ Builder
    "(_ bv"
                                , Integer -> Builder
    forall a. Integral a => a -> Builder
    Builder.decimal Integer
    d
                                , Builder
    " "
                                , Natural -> Builder
    forall a. Integral a => a -> Builder
    Builder.decimal (NatRepr w -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    natValue NatRepr w
    w)
                                , Builder
    ")"]
      where d :: Integer
    d = BV w -> Integer
    forall (w :: Natural). BV w -> Integer
    BV.asUnsigned BV w
    u

    -- | @bvhexadecimal x w@ constructs a bitvector term with width @w@ equal to @x `mod` 2^w@.
    --
    -- The width @w@ must be a positive multiple of 4.
    --
    -- The literal uses hex notation.
    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 (Builder -> Term) -> Builder -> Term
    forall a b. (a -> b) -> a -> b
    $ Builder
    "#x" Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Natural -> Builder
    go (NatRepr w -> Natural
    forall (n :: Natural). NatRepr n -> Natural
    natValue NatRepr w
    w0)
      where go :: Natural -> Builder
            go :: Natural -> Builder
    go Natural
    0 = Builder
    forall a. Monoid a => a
    mempty
            go Natural
    w | Natural
    w Natural -> Natural -> Bool
    forall a. Ord a => a -> a -> Bool
    < Natural
    4 = [Char] -> Builder
    forall a. HasCallStack => [Char] -> a
    error [Char]
    "bvhexadecimal width must be a multiple of 4."
            go Natural
    w =
              let i :: Natural
    i = Natural
    w Natural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    - Natural
    4
                  charBits :: Integer
    charBits = BV 4 -> Integer
    forall (w :: Natural). BV w -> Integer
    BV.asUnsigned (Natural -> NatRepr 4 -> BV w -> BV 4
    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 (Int -> Char) -> Int -> Char
    forall a b. (a -> b) -> a -> b
    $ Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    charBits
               in Char -> Builder
    Builder.singleton Char
    c Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Natural -> Builder
    go Natural
    i

    -- | @concat x y@ returns the bitvector with the bits of @x@ followed by the bits of @y@.
    concat :: Term -> Term -> Term
    concat :: Term -> Term -> Term
    concat = Builder -> Term -> Term -> Term
    bin_app Builder
    "concat"

    -- | @extract i j x@ returns the bitvector containing the bits @[j..i]@.
    extract :: Natural -> Natural -> Term -> Term
    extract :: Natural -> Natural -> Term -> Term
    extract Natural
    i Natural
    j Term
    x
      | Natural
    i Natural -> Natural -> Bool
    forall a. Ord a => a -> a -> Bool
    < Natural
    j = [Char] -> Term
    forall a. HasCallStack => [Char] -> a
    error ([Char] -> Term) -> [Char] -> Term
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "End of extract (" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Natural -> [Char]
    forall a. Show a => a -> [Char]
    show Natural
    i [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ") less than beginning (" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Natural -> [Char]
    forall a. Show a => a -> [Char]
    show Natural
    j [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ")."
      | Bool
    otherwise = -- We cannot check that j is small enough.
        let e :: Builder
    e = Builder
    "(_ extract " Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Natural -> Builder
    forall a. Integral a => a -> Builder
    Builder.decimal Natural
    i Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Builder
    " " Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Natural -> Builder
    forall a. Integral a => a -> Builder
    Builder.decimal Natural
    j Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Builder
    ")"
         in Builder -> Term -> Term
    un_app Builder
    e Term
    x

    -- | Bitwise negation of term.
    bvnot :: Term -> Term
    bvnot :: Term -> Term
    bvnot = Builder -> Term -> Term
    un_app Builder
    "bvnot"

    -- | Bitwise and of all arguments.
    bvand :: Term -> [Term] -> Term
    bvand :: Term -> [Term] -> Term
    bvand = Builder -> Term -> [Term] -> Term
    assoc_app Builder
    "bvand"

    -- | Bitwise include or of all arguments.
    bvor :: Term -> [Term] -> Term
    bvor :: Term -> [Term] -> Term
    bvor = Builder -> Term -> [Term] -> Term
    assoc_app Builder
    "bvor"

    -- | Bitvector exclusive or of all arguments.
    bvxor :: Term -> [Term] -> Term
    bvxor :: Term -> [Term] -> Term
    bvxor = Builder -> Term -> [Term] -> Term
    assoc_app Builder
    "bvxor"

    -- | Negate the bitvector
    bvneg :: Term -> Term
    bvneg :: Term -> Term
    bvneg = Builder -> Term -> Term
    un_app Builder
    "bvneg"

    -- | Bitvector addition
    bvadd :: Term -> [Term] -> Term
    bvadd :: Term -> [Term] -> Term
    bvadd = Builder -> Term -> [Term] -> Term
    assoc_app Builder
    "bvadd"

    -- | Bitvector subtraction
    bvsub :: Term -> Term -> Term
    bvsub :: Term -> Term -> Term
    bvsub = Builder -> Term -> Term -> Term
    bin_app Builder
    "bvsub"

    -- | Bitvector multiplication
    bvmul :: Term -> [Term] -> Term
    bvmul :: Term -> [Term] -> Term
    bvmul = Builder -> Term -> [Term] -> Term
    assoc_app Builder
    "bvmul"

    -- | @bvudiv x y@ returns @floor (to_nat x / to_nat y)@ when @y != 0@.
    --
    -- When @y = 0@, this returns @not (from_nat 0)@.
    bvudiv :: Term -> Term -> Term
    bvudiv :: Term -> Term -> Term
    bvudiv = Builder -> Term -> Term -> Term
    bin_app Builder
    "bvudiv"

    -- | @bvurem x y@ returns @x - y * bvudiv x y@ when @y != 0@.
    --
    -- When @y = 0@, this returns @from_nat 0@.
    bvurem :: Term -> Term -> Term
    bvurem :: Term -> Term -> Term
    bvurem = Builder -> Term -> Term -> Term
    bin_app Builder
    "bvurem"

    -- | @bvshl x y@ shifts the bits in @x@ to the left by @to_nat u@ bits.
    --
    -- The new bits are zeros (false)
    bvshl :: Term -> Term -> Term
    bvshl :: Term -> Term -> Term
    bvshl = Builder -> Term -> Term -> Term
    bin_app Builder
    "bvshl"

    -- | @bvlshr x y@ shifts the bits in @x@ to the right by @to_nat u@ bits.
    --
    -- The new bits are zeros (false)
    bvlshr :: Term -> Term -> Term
    bvlshr :: Term -> Term -> Term
    bvlshr = Builder -> Term -> Term -> Term
    bin_app Builder
    "bvlshr"

    -- | @bvult x y@ returns a Boolean term that is true if @to_nat x < to_nat y@.
    bvult :: Term -> Term -> Term
    bvult :: Term -> Term -> Term
    bvult = Builder -> Term -> Term -> Term
    bin_app Builder
    "bvult"

    -- | @bvule x y@ returns a Boolean term that is true if @to_nat x <= to_nat y@.
    --
    -- Note. This is in @QF_BV@, but not the bitvector theory.
    bvule :: Term -> Term -> Term
    bvule :: Term -> Term -> Term
    bvule = Builder -> Term -> Term -> Term
    bin_app Builder
    "bvule"

    -- | @bvsle x y@ returns a Boolean term that is true if @to_int x <= to_int y@.
    --
    -- Note. This is in @QF_BV@, but not the bitvector theory.
    bvsle :: Term -> Term -> Term
    bvsle :: Term -> Term -> Term
    bvsle = Builder -> Term -> Term -> Term
    bin_app Builder
    "bvsle"

    -- | @bvslt x y@ returns a Boolean term that is true if @to_int x < to_int y@.
    --
    -- Note. This is in @QF_BV@, but not the bitvector theory.
    bvslt :: Term -> Term -> Term
    bvslt :: Term -> Term -> Term
    bvslt = Builder -> Term -> Term -> Term
    bin_app Builder
    "bvslt"

    -- | @bvuge x y@ returns a Boolean term that is true if @to_nat x <= to_nat y@.
    --
    -- Note. This is in @QF_BV@, but not the bitvector theory.
    bvuge :: Term -> Term -> Term
    bvuge :: Term -> Term -> Term
    bvuge = Builder -> Term -> Term -> Term
    bin_app Builder
    "bvuge"

    -- | @bvugt x y@ returns a Boolean term that is true if @to_nat x < to_nat y@.
    --
    -- Note. This is in @QF_BV@, but not the bitvector theory.
    bvugt :: Term -> Term -> Term
    bvugt :: Term -> Term -> Term
    bvugt = Builder -> Term -> Term -> Term
    bin_app Builder
    "bvugt"

    -- | @bvsge x y@ returns a Boolean term that is true if @to_int x <= to_int y@.
    --
    -- Note. This is in @QF_BV@, but not the bitvector theory.
    bvsge :: Term -> Term -> Term
    bvsge :: Term -> Term -> Term
    bvsge = Builder -> Term -> Term -> Term
    bin_app Builder
    "bvsge"

    -- | @bvsgt x y@ returns a Boolean term that is true if @to_int x < to_int y@.
    --
    -- Note. This is in @QF_BV@, but not the bitvector theory.
    bvsgt :: Term -> Term -> Term
    bvsgt :: Term -> Term -> Term
    bvsgt = Builder -> Term -> Term -> Term
    bin_app Builder
    "bvsgt"

    -- | @bvashr x y@ shifts the bits in @x@ to the right by @to_nat u@ bits.
    --
    -- The new bits are the same as the most-significant bit of @x@.
    --
    -- Note. This is in @QF_BV@, but not the bitvector theory.
    bvashr :: Term -> Term -> Term
    bvashr :: Term -> Term -> Term
    bvashr = Builder -> Term -> Term -> Term
    bin_app Builder
    "bvashr"

    -- | @bvsdiv x y@ returns @round_to_zero (to_int x / to_int y)@ when @y != 0@.
    --
    -- When @y = 0@, this returns @not (from_nat 0)@.
    --
    -- Note. This is in @QF_BV@, but not the bitvector theory.
    bvsdiv :: Term -> Term -> Term
    bvsdiv :: Term -> Term -> Term
    bvsdiv = Builder -> Term -> Term -> Term
    bin_app Builder
    "bvsdiv"

    -- | @bvsrem x y@ returns @x - y * bvsdiv x y@ when @y != 0@.
    --
    -- When @y = 0@, this returns @from_nat 0@.
    --
    -- Note. This is in @QF_BV@, but not the bitvector theory.
    bvsrem :: Term -> Term -> Term
    bvsrem :: Term -> Term -> Term
    bvsrem = Builder -> Term -> Term -> Term
    bin_app Builder
    "bvsrem"

    -- | @bvsignExtend w x@ adds an additional @w@ bits to the most
    -- significant bits of @x@ by sign extending @x@.
    --
    -- Note. This is in @QF_BV@, but not the bitvector theory.
    bvsignExtend :: Integer -> Term -> Term
    bvsignExtend :: Integer -> Term -> Term
    bvsignExtend Integer
    w Term
    x =
      let e :: Builder
    e = Builder
    "(_ sign_extend " Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Integer -> Builder
    forall a. Integral a => a -> Builder
    Builder.decimal Integer
    w Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Builder
    ")"
       in Builder -> Term -> Term
    un_app Builder
    e Term
    x

    -- | @bvzeroExtend w x@ adds an additional @w@ zero bits to the most
    -- significant bits of @x@.
    --
    -- Note. This is in @QF_BV@, but not the bitvector theory.
    bvzeroExtend :: Integer -> Term -> Term
    bvzeroExtend :: Integer -> Term -> Term
    bvzeroExtend Integer
    w Term
    x =
      let e :: Builder
    e = Builder
    "(_ zero_extend " Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Integer -> Builder
    forall a. Integral a => a -> Builder
    Builder.decimal Integer
    w Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Builder
    ")"
       in Builder -> Term -> Term
    un_app Builder
    e Term
    x

    ------------------------------------------------------------------------
    -- Command

    -- | This represents a command to be sent to the SMT solver.
    newtype Command = Cmd Builder

    -- | Set the logic of the SMT solver
    setLogic :: Logic -> Command
    setLogic :: Logic -> Command
    setLogic (Logic Builder
    nm) = Builder -> Command
    Cmd (Builder -> Command) -> Builder -> Command
    forall a b. (a -> b) -> a -> b
    $ Builder
    "(set-logic " Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Builder
    nm Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Builder
    ")"

    -- | Set an option in the SMT solver
    --
    -- The name should not need to be prefixed with a colon."
    setOption :: Text -> Text -> Command
    setOption :: Text -> Text -> Command
    setOption Text
    nm Text
    val = Builder -> Command
    Cmd (Builder -> Command) -> Builder -> Command
    forall a b. (a -> b) -> a -> b
    $ Builder -> [Builder] -> Builder
    app_list Builder
    "set-option" [Builder
    ":" Builder -> Builder -> 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"

    -- | Set option to produce models
    --
    -- This is a widely used option so, we we have a custom command to
    -- make it.
    setProduceModels :: Bool -> Command
    setProduceModels :: Bool -> Command
    setProduceModels Bool
    b = Text -> Text -> Command
    setOption Text
    "produce-models" (Bool -> Text
    ppBool Bool
    b)

    -- | Request the SMT solver to exit
    exit :: Command
    exit :: Command
    exit = Builder -> Command
    Cmd Builder
    "(exit)"

    -- | Declare an uninterpreted sort with the given number of sort parameters.
    declareSort :: Symbol -> Integer -> Command
    declareSort :: Text -> Integer -> Command
    declareSort Text
    v Integer
    n = Builder -> Command
    Cmd (Builder -> Command) -> Builder -> Command
    forall a b. (a -> b) -> a -> b
    $ Builder -> [Builder] -> Builder
    app Builder
    "declare-sort" [Text -> Builder
    Builder.fromText Text
    v, [Char] -> Builder
    forall a. IsString a => [Char] -> a
    fromString (Integer -> [Char]
    forall a. Show a => a -> [Char]
    show Integer
    n)]

    -- | Define a sort in terms of other sorts
    --
    defineSort :: Symbol -- ^ Name of new sort
               -> [Symbol] -- ^ Parameters for polymorphic sorts
               -> Sort -- ^ Definition
               -> Command
    defineSort :: Text -> [Text] -> Sort -> Command
    defineSort Text
    v [Text]
    params Sort
    d =
      Builder -> Command
    Cmd (Builder -> Command) -> Builder -> Command
    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 (Text -> Builder) -> [Text] -> [Builder]
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Text]
    params)
                              , Sort -> Builder
    unSort Sort
    d
                              ]

    -- | Declare a constant with the given name and return types.
    declareConst :: Text -> Sort -> Command
    declareConst :: Text -> Sort -> Command
    declareConst Text
    v Sort
    tp = Builder -> Command
    Cmd (Builder -> Command) -> Builder -> Command
    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]

    -- | Declare a function with the given name, argument types, and
    -- return type.
    declareFun :: Text -> [Sort] -> Sort -> Command
    declareFun :: Text -> [Sort] -> Sort -> Command
    declareFun Text
    v [Sort]
    argSorts Sort
    retSort = Builder -> Command
    Cmd (Builder -> Command) -> Builder -> Command
    forall a b. (a -> b) -> a -> b
    $
      Builder -> [Builder] -> Builder
    app Builder
    "declare-fun" [ Text -> Builder
    Builder.fromText Text
    v
                        , [Builder] -> Builder
    builder_list ([Builder] -> Builder) -> [Builder] -> Builder
    forall a b. (a -> b) -> a -> b
    $ Sort -> Builder
    unSort (Sort -> Builder) -> [Sort] -> [Builder]
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Sort]
    argSorts
                        , Sort -> Builder
    unSort Sort
    retSort
                        ]

    -- | Declare a function with the given name, argument types, and
    -- return type.
    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 (Builder -> Command) -> Builder -> Command
    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 ((Text, Sort) -> Builder) -> [(Text, Sort)] -> [Builder]
    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 the predicate holds in the current context.
    assert :: Term -> Command
    assert :: Term -> Command
    assert Term
    p = Builder -> Command
    Cmd (Builder -> Command) -> Builder -> Command
    forall a b. (a -> b) -> a -> b
    $ Builder -> [Builder] -> Builder
    app Builder
    "assert" [Term -> Builder
    renderTerm Term
    p]

    -- | Assert the predicate holds in the current context, and assign
    --   it a name so it can appear in unsatisfiable core results.
    assertNamed :: Term -> Text -> Command
    assertNamed :: Term -> Text -> Command
    assertNamed Term
    p Text
    nm =
      Builder -> Command
    Cmd (Builder -> Command) -> Builder -> Command
    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]]

    -- | Check the satisfiability of the current assertions
    checkSat :: Command
    checkSat :: Command
    checkSat = Builder -> Command
    Cmd Builder
    "(check-sat)"

    -- | Check the satisfiability of the current assertions and the additional ones in the list.
    checkSatAssuming :: [Term] -> Command
    checkSatAssuming :: [Term] -> Command
    checkSatAssuming [Term]
    l = Builder -> Command
    Cmd (Builder -> Command) -> Builder -> Command
    forall a b. (a -> b) -> a -> b
    $ Builder
    "(check-sat-assuming " Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> [Builder] -> Builder
    builder_list (Term -> Builder
    renderTerm (Term -> Builder) -> [Term] -> [Builder]
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Term]
    l) Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Builder
    ")"

    -- | Check satisfiability of the given atomic assumptions in the current context.
    --
    --   NOTE! The names of variables passed to this function MUST be generated using
    --   a `declare-fun` statement, and NOT a `define-fun` statement.  Thus, if you
    --   want to bind an arbitrary term, you must declare a new term and assert that
    --   it is equal to it's definition. Yes, this is quite irritating.
    checkSatWithAssumptions :: [Text] -> Command
    checkSatWithAssumptions :: [Text] -> Command
    checkSatWithAssumptions [Text]
    nms = Builder -> Command
    Cmd (Builder -> Command) -> Builder -> Command
    forall a b. (a -> b) -> a -> b
    $ Builder -> [Builder] -> Builder
    app Builder
    "check-sat-assuming" [[Builder] -> Builder
    builder_list ((Text -> Builder) -> [Text] -> [Builder]
    forall a b. (a -> b) -> [a] -> [b]
    map Text -> Builder
    Builder.fromText [Text]
    nms)]

    -- | Get the model associated with the last call to @check-sat@.
    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)"

    -- | Get an abduct that entails the formula, and bind it to the name
    getAbduct :: Text -> Term -> Command
    getAbduct :: Text -> Term -> Command
    getAbduct Text
    nm Term
    p = Builder -> Command
    Cmd (Builder -> Command) -> Builder -> Command
    forall a b. (a -> b) -> a -> b
    $ Builder
    "(get-abduct " Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Text -> Builder
    Builder.fromText Text
    nm Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Builder
    " " Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Term -> Builder
    renderTerm Term
    p Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Builder
    ")"

    -- | Get the next command, called after a get-abduct command
    getAbductNext :: Command
    getAbductNext :: Command
    getAbductNext = Builder -> Command
    Cmd Builder
    "(get-abduct-next)"

    -- | Declare a SyGuS function to synthesize with the given name, arguments, and
    -- return type.
    synthFun :: Text -> [(Text, Sort)] -> Sort -> Command
    synthFun :: Text -> [(Text, Sort)] -> Sort -> Command
    synthFun Text
    f [(Text, Sort)]
    args Sort
    ret_tp = Builder -> Command
    Cmd (Builder -> Command) -> Builder -> Command
    forall a b. (a -> b) -> a -> b
    $ Builder -> [Builder] -> Builder
    app Builder
    "synth-fun"
      [ Text -> Builder
    Builder.fromText Text
    f
      , [Builder] -> Builder
    builder_list ([Builder] -> Builder) -> [Builder] -> Builder
    forall a b. (a -> b) -> a -> b
    $ ((Text, Sort) -> Builder) -> [(Text, Sort)] -> [Builder]
    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
      ]

    -- | Declare a SyGuS variable with the given name and type.
    declareVar :: Text -> Sort -> Command
    declareVar :: Text -> Sort -> Command
    declareVar Text
    v Sort
    tp = Builder -> Command
    Cmd (Builder -> Command) -> Builder -> Command
    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]

    -- | Add the SyGuS constraint to the current synthesis problem.
    constraint :: Term -> Command
    constraint :: Term -> Command
    constraint Term
    p = Builder -> Command
    Cmd (Builder -> Command) -> Builder -> Command
    forall a b. (a -> b) -> a -> b
    $ Builder -> [Builder] -> Builder
    app Builder
    "constraint" [Term -> Builder
    renderTerm Term
    p]

    -- | Ask the SyGuS solver to find a solution for the synthesis problem
    -- corresponding to the current functions-to-synthesize, variables and
    -- constraints.
    checkSynth :: Command
    checkSynth :: Command
    checkSynth = Builder -> Command
    Cmd Builder
    "(check-synth)\n"

    -- | Get the values associated with the terms from the last call to @check-sat@.
    getValue :: [Term] -> Command
    getValue :: [Term] -> Command
    getValue [Term]
    values = Builder -> Command
    Cmd (Builder -> Command) -> Builder -> Command
    forall a b. (a -> b) -> a -> b
    $ Builder -> [Builder] -> Builder
    app Builder
    "get-value" [[Builder] -> Builder
    builder_list (Term -> Builder
    renderTerm (Term -> Builder) -> [Term] -> [Builder]
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Term]
    values)]

    -- | Empties the assertion stack and remove all global assertions and declarations.
    resetAssertions :: Command
    resetAssertions :: Command
    resetAssertions = Builder -> Command
    Cmd Builder
    "(reset-assertions)"

    -- | Push the given number of scope frames to the SMT solver.
    push :: Integer -> Command
    push :: Integer -> Command
    push Integer
    n =  Builder -> Command
    Cmd (Builder -> Command) -> Builder -> Command
    forall a b. (a -> b) -> a -> b
    $ Builder
    "(push " Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Integer -> Builder
    forall a. Integral a => a -> Builder
    Builder.decimal Integer
    n Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Builder
    ")"

    -- | Pop the given number of scope frames to the SMT solver.
    pop :: Integer -> Command
    pop :: Integer -> Command
    pop Integer
    n =  Builder -> Command
    Cmd (Builder -> Command) -> Builder -> Command
    forall a b. (a -> b) -> a -> b
    $ Builder
    "(pop " Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Integer -> Builder
    forall a. Integral a => a -> Builder
    Builder.decimal Integer
    n Builder -> Builder -> Builder
    forall a. Semigroup a => a -> a -> a
    <> Builder
    ")"

    -- | This is a subtype of the type of the same name in Data.SBV.Control.
    data SMTInfoFlag =
        Name
      | Version
      | ErrorBehavior
      | InfoKeyword Text
      deriving (Typeable SMTInfoFlag
    Typeable 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 (c :: Type -> Type).
        (forall b r. Data b => c (b -> r) -> c r)
        -> (forall r. r -> c r) -> Constr -> c SMTInfoFlag)
    -> (SMTInfoFlag -> Constr)
    -> (SMTInfoFlag -> DataType)
    -> (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))
    -> ((forall b. Data b => b -> b) -> SMTInfoFlag -> SMTInfoFlag)
    -> (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 u. (forall d. Data d => d -> u) -> SMTInfoFlag -> [u])
    -> (forall u.
        Int -> (forall d. Data d => d -> u) -> SMTInfoFlag -> u)
    -> (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 (m :: Type -> Type).
        MonadPlus m =>
        (forall d. Data d => d -> m d) -> SMTInfoFlag -> m SMTInfoFlag)
    -> Data SMTInfoFlag
    SMTInfoFlag -> Constr
    SMTInfoFlag -> DataType
    (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)
    $cgfoldl :: forall (c :: Type -> Type).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> SMTInfoFlag -> 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
    $cgunfold :: forall (c :: Type -> Type).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c SMTInfoFlag
    gunfold :: forall (c :: Type -> Type).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c SMTInfoFlag
    $ctoConstr :: SMTInfoFlag -> Constr
    toConstr :: SMTInfoFlag -> Constr
    $cdataTypeOf :: SMTInfoFlag -> DataType
    dataTypeOf :: SMTInfoFlag -> DataType
    $cdataCast1 :: forall (t :: Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c SMTInfoFlag)
    dataCast1 :: forall (t :: Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d. Data d => c (t d)) -> 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)
    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)
    $cgmapT :: (forall b. Data b => b -> b) -> SMTInfoFlag -> SMTInfoFlag
    gmapT :: (forall b. Data b => b -> b) -> SMTInfoFlag -> SMTInfoFlag
    $cgmapQl :: 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
    $cgmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> SMTInfoFlag -> r
    gmapQr :: forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> SMTInfoFlag -> r
    $cgmapQ :: forall u. (forall d. Data d => d -> u) -> SMTInfoFlag -> [u]
    gmapQ :: forall u. (forall d. Data d => d -> u) -> SMTInfoFlag -> [u]
    $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SMTInfoFlag -> u
    gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SMTInfoFlag -> u
    $cgmapM :: forall (m :: Type -> Type).
    Monad 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
    $cgmapMp :: 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
    $cgmapMo :: forall (m :: Type -> Type).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SMTInfoFlag -> m SMTInfoFlag
    gmapMo :: forall (m :: Type -> Type).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SMTInfoFlag -> m SMTInfoFlag
    Data, SMTInfoFlag -> SMTInfoFlag -> Bool
    (SMTInfoFlag -> SMTInfoFlag -> Bool)
    -> (SMTInfoFlag -> SMTInfoFlag -> Bool) -> Eq SMTInfoFlag
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: SMTInfoFlag -> SMTInfoFlag -> Bool
    == :: SMTInfoFlag -> SMTInfoFlag -> Bool
    $c/= :: SMTInfoFlag -> SMTInfoFlag -> Bool
    /= :: SMTInfoFlag -> SMTInfoFlag -> Bool
    Eq, Eq SMTInfoFlag
    Eq SMTInfoFlag =>
    (SMTInfoFlag -> SMTInfoFlag -> Ordering)
    -> (SMTInfoFlag -> SMTInfoFlag -> Bool)
    -> (SMTInfoFlag -> SMTInfoFlag -> Bool)
    -> (SMTInfoFlag -> SMTInfoFlag -> Bool)
    -> (SMTInfoFlag -> SMTInfoFlag -> Bool)
    -> (SMTInfoFlag -> SMTInfoFlag -> SMTInfoFlag)
    -> (SMTInfoFlag -> SMTInfoFlag -> SMTInfoFlag)
    -> Ord 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
    $ccompare :: SMTInfoFlag -> SMTInfoFlag -> Ordering
    compare :: SMTInfoFlag -> SMTInfoFlag -> Ordering
    $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
    >= :: SMTInfoFlag -> SMTInfoFlag -> Bool
    $cmax :: SMTInfoFlag -> SMTInfoFlag -> SMTInfoFlag
    max :: SMTInfoFlag -> SMTInfoFlag -> SMTInfoFlag
    $cmin :: SMTInfoFlag -> SMTInfoFlag -> SMTInfoFlag
    min :: SMTInfoFlag -> SMTInfoFlag -> SMTInfoFlag
    Ord, (forall x. SMTInfoFlag -> Rep SMTInfoFlag x)
    -> (forall x. Rep SMTInfoFlag x -> SMTInfoFlag)
    -> Generic SMTInfoFlag
    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
    $cfrom :: forall x. SMTInfoFlag -> Rep SMTInfoFlag x
    from :: forall x. SMTInfoFlag -> Rep SMTInfoFlag x
    $cto :: forall x. Rep SMTInfoFlag x -> SMTInfoFlag
    to :: forall x. Rep SMTInfoFlag x -> SMTInfoFlag
    Generic, Int -> SMTInfoFlag -> [Char] -> [Char]
    [SMTInfoFlag] -> [Char] -> [Char]
    SMTInfoFlag -> [Char]
    (Int -> SMTInfoFlag -> [Char] -> [Char])
    -> (SMTInfoFlag -> [Char])
    -> ([SMTInfoFlag] -> [Char] -> [Char])
    -> Show SMTInfoFlag
    forall a.
    (Int -> a -> [Char] -> [Char])
    -> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
    $cshowsPrec :: Int -> SMTInfoFlag -> [Char] -> [Char]
    showsPrec :: Int -> SMTInfoFlag -> [Char] -> [Char]
    $cshow :: SMTInfoFlag -> [Char]
    show :: SMTInfoFlag -> [Char]
    $cshowList :: [SMTInfoFlag] -> [Char] -> [Char]
    showList :: [SMTInfoFlag] -> [Char] -> [Char]
    Show, Typeable)

    flagToSExp :: SMTInfoFlag -> Text
    flagToSExp :: SMTInfoFlag -> Text
    flagToSExp = (Char -> Text -> Text
    cons Char
    ':') (Text -> Text) -> (SMTInfoFlag -> Text) -> SMTInfoFlag -> Text
    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

    -- | A @get-info@ command
    getInfo :: SMTInfoFlag -> Command
    getInfo :: SMTInfoFlag -> Command
    getInfo SMTInfoFlag
    flag = Builder -> Command
    Cmd (Builder -> Command) -> Builder -> Command
    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