-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | A type-safe interface to communicate with an SMT solver.
--   
--   A type-safe interface to communicate with an SMT solver.
@package smtlib2
@version 1.0

module Language.SMTLib2.Strategy
data Tactic
Skip :: Tactic
AndThen :: [Tactic] -> Tactic
OrElse :: [Tactic] -> Tactic
ParOr :: [Tactic] -> Tactic
ParThen :: Tactic -> Tactic -> Tactic
TryFor :: Tactic -> Integer -> Tactic
If :: (Probe Bool) -> Tactic -> Tactic -> Tactic
FailIf :: (Probe Bool) -> Tactic
UsingParams :: (BuiltInTactic p) -> [p] -> Tactic
data Probe a
[ProbeBoolConst] :: Bool -> Probe Bool
[ProbeIntConst] :: Integer -> Probe Integer
[ProbeAnd] :: [Probe Bool] -> Probe Bool
[ProbeOr] :: [Probe Bool] -> Probe Bool
[ProbeNot] :: Probe Bool -> Probe Bool
[ProbeEq] :: Show a => Probe a -> Probe a -> Probe Bool
[ProbeGt] :: Probe Integer -> Probe Integer -> Probe Bool
[ProbeGe] :: Probe Integer -> Probe Integer -> Probe Bool
[ProbeLt] :: Probe Integer -> Probe Integer -> Probe Bool
[ProbeLe] :: Probe Integer -> Probe Integer -> Probe Bool
[IsPB] :: Probe Bool
[ArithMaxDeg] :: Probe Integer
[ArithAvgDeg] :: Probe Integer
[ArithMaxBW] :: Probe Integer
[ArithAvgBW] :: Probe Integer
[IsQFLIA] :: Probe Bool
[IsQFLRA] :: Probe Bool
[IsQFLIRA] :: Probe Bool
[IsILP] :: Probe Bool
[IsQFNIA] :: Probe Bool
[IsQFNRA] :: Probe Bool
[IsNIA] :: Probe Bool
[IsNRA] :: Probe Bool
[IsUnbounded] :: Probe Bool
[Memory] :: Probe Integer
[Depth] :: Probe Integer
[Size] :: Probe Integer
[NumExprs] :: Probe Integer
[NumConsts] :: Probe Integer
[NumBoolConsts] :: Probe Integer
[NumArithConsts] :: Probe Integer
[NumBVConsts] :: Probe Integer
[ProduceProofs] :: Probe Bool
[ProduceModel] :: Probe Bool
[ProduceUnsatCores] :: Probe Bool
[HasPatterns] :: Probe Bool
[IsPropositional] :: Probe Bool
[IsQFBV] :: Probe Bool
[IsQFBVEQ] :: Probe Bool
data AnyPar
ParBool :: Bool -> AnyPar
ParInt :: Integer -> AnyPar
ParDouble :: Double -> AnyPar
data BuiltInTactic p
[QFLRATactic] :: BuiltInTactic QFLRATacticP
[CustomTactic] :: String -> BuiltInTactic (String, AnyPar)
data QFLRATacticP
ArithBranchCutRatio :: Integer -> QFLRATacticP
instance GHC.Show.Show Language.SMTLib2.Strategy.QFLRATacticP
instance GHC.Show.Show Language.SMTLib2.Strategy.AnyPar
instance GHC.Show.Show Language.SMTLib2.Strategy.Tactic
instance GHC.Show.Show (Language.SMTLib2.Strategy.BuiltInTactic p)
instance GHC.Show.Show a => GHC.Show.Show (Language.SMTLib2.Strategy.Probe a)

module Language.SMTLib2.Internals.Type.Nat

-- | Natural numbers on the type-level.
data Nat
Z :: Nat
S :: Nat -> Nat

-- | A concrete representation of the <a>Nat</a> type.
data Natural (n :: Nat)
[Zero] :: Natural Z
[Succ] :: Natural n -> Natural (S n)
naturalToInteger :: Natural n -> Integer
naturalAdd :: Natural n -> Natural m -> Natural (n + m)
naturalSub :: Natural (n + m) -> Natural n -> Natural m
naturalSub' :: Natural n -> Natural m -> (forall diff. ((m + diff) ~ n) => Natural diff -> a) -> a
naturalLEQ :: Natural n -> Natural m -> Maybe (Dict ((n <= m) ~ True))

-- | Get a static representation for a dynamically created natural number.
--   
--   Example:
--   
--   <pre>
--   &gt;&gt;&gt; reifyNat (S (S Z)) show
--   "2"
--   </pre>
reifyNat :: Nat -> (forall n. Natural n -> r) -> r
nat :: (Num a, Ord a) => a -> ExpQ

-- | A template haskell function to create nicer looking number types.
--   
--   Example:
--   
--   <pre>
--   &gt;&gt;&gt; $(nat 5) :: Natural $(natT 5)
--   5
--   </pre>
natT :: (Num a, Ord a) => a -> TypeQ
type N0 = Z
type N1 = S N0
type N2 = S N1
type N3 = S N2
type N4 = S N3
type N5 = S N4
type N6 = S N5
type N7 = S N6
type N8 = S N7
type N9 = S N8
type N10 = S N9
type N11 = S N10
type N12 = S N11
type N13 = S N12
type N14 = S N13
type N15 = S N14
type N16 = S N15
type N17 = S N16
type N18 = S N17
type N19 = S N18
type N20 = S N19
type N21 = S N20
type N22 = S N21
type N23 = S N22
type N24 = S N23
type N25 = S N24
type N26 = S N25
type N27 = S N26
type N28 = S N27
type N29 = S N28
type N30 = S N29
type N31 = S N30
type N32 = S N31
type N33 = S N32
type N34 = S N33
type N35 = S N34
type N36 = S N35
type N37 = S N36
type N38 = S N37
type N39 = S N38
type N40 = S N39
type N41 = S N40
type N42 = S N41
type N43 = S N42
type N44 = S N43
type N45 = S N44
type N46 = S N45
type N47 = S N46
type N48 = S N47
type N49 = S N48
type N50 = S N49
type N51 = S N50
type N52 = S N51
type N53 = S N52
type N54 = S N53
type N55 = S N54
type N56 = S N55
type N57 = S N56
type N58 = S N57
type N59 = S N58
type N60 = S N59
type N61 = S N60
type N62 = S N61
type N63 = S N62
type N64 = S N63
class IsNatural n
getNatural :: IsNatural n => Natural n
deriveIsNatural :: Natural n -> Dict (IsNatural n)
instance GHC.Show.Show (Language.SMTLib2.Internals.Type.Nat.Natural n)
instance GHC.Classes.Eq (Language.SMTLib2.Internals.Type.Nat.Natural n)
instance GHC.Classes.Ord (Language.SMTLib2.Internals.Type.Nat.Natural n)
instance GHC.Classes.Eq Language.SMTLib2.Internals.Type.Nat.Nat
instance GHC.Classes.Ord Language.SMTLib2.Internals.Type.Nat.Nat
instance GHC.Num.Num Language.SMTLib2.Internals.Type.Nat.Nat
instance GHC.Enum.Enum Language.SMTLib2.Internals.Type.Nat.Nat
instance GHC.Real.Real Language.SMTLib2.Internals.Type.Nat.Nat
instance GHC.Real.Integral Language.SMTLib2.Internals.Type.Nat.Nat
instance Data.GADT.Compare.GEq Language.SMTLib2.Internals.Type.Nat.Nat Language.SMTLib2.Internals.Type.Nat.Natural
instance Data.GADT.Compare.GCompare Language.SMTLib2.Internals.Type.Nat.Nat Language.SMTLib2.Internals.Type.Nat.Natural
instance Data.GADT.Show.GShow Language.SMTLib2.Internals.Type.Nat.Nat Language.SMTLib2.Internals.Type.Nat.Natural
instance Language.SMTLib2.Internals.Type.Nat.IsNatural 'Language.SMTLib2.Internals.Type.Nat.Z
instance Language.SMTLib2.Internals.Type.Nat.IsNatural n => Language.SMTLib2.Internals.Type.Nat.IsNatural ('Language.SMTLib2.Internals.Type.Nat.S n)

module Language.SMTLib2.Internals.Type.List

-- | Strongly typed heterogenous lists.
--   
--   A <i>List e '[tp1,tp2,tp3]</i> contains 3 elements of types <i>e
--   tp1</i>, <i>e tp2</i> and <i>e tp3</i> respectively.
--   
--   As an example, the following list contains two types:
--   
--   <pre>
--   &gt;&gt;&gt; int ::: bool ::: Nil :: List Repr '[IntType,BoolType]
--   [IntRepr,BoolRepr]
--   </pre>
data List e (tp :: [a])
[Nil] :: List e '[]
[:::] :: e x -> List e xs -> List e (x : xs)
list :: [ExpQ] -> ExpQ
nil :: List e '[]
list1 :: e t1 -> List e '[t1]
list2 :: e t1 -> e t2 -> List e '[t1, t2]
list3 :: e t1 -> e t2 -> e t3 -> List e '[t1, t2, t3]

-- | Get a static representation of a dynamic list.
--   
--   For example, to convert a list of strings into a list of types:
--   
--   <pre>
--   &gt;&gt;&gt; reifyList (\name f -&gt; case name of { "int" -&gt; f int ; "bool" -&gt; f bool }) ["bool","int"] show
--   "[BoolRepr,IntRepr]"
--   </pre>
reifyList :: (forall r'. a -> (forall tp. e tp -> r') -> r') -> [a] -> (forall tp. List e tp -> r) -> r
access :: Monad m => List e lst -> Natural idx -> (e (Index lst idx) -> m (a, e tp)) -> m (a, List e (Insert lst idx tp))
access' :: Monad m => List e lst -> Natural idx -> (e (Index lst idx) -> m (a, e (Index lst idx))) -> m (a, List e lst)
head :: List e lst -> e (Head lst)
tail :: List e lst -> List e (Tail lst)
index :: List e lst -> Natural idx -> e (Index lst idx)
indexDyn :: Integral i => List e tps -> i -> (forall tp. e tp -> a) -> a
insert :: List e lst -> Natural idx -> e tp -> List e (Insert lst idx tp)
remove :: List e lst -> Natural idx -> List e (Remove lst idx)
mapM :: Monad m => (forall x. e x -> m (e' x)) -> List e lst -> m (List e' lst)
mapIndexM :: Monad m => (forall n. Natural n -> e (Index lst n) -> m (e' (Index lst n))) -> List e lst -> m (List e' lst)
traverse :: Applicative f => (forall x. e x -> f (e' x)) -> List e lst -> f (List e' lst)
cons :: e x -> List e xs -> List e (x : xs)
append :: List e xs -> e x -> List e (Append xs x)
length :: List e lst -> Natural (Length lst)
drop :: List e lst -> Natural i -> List e (Drop lst i)
take :: List e lst -> Natural i -> List e (Take lst i)
last :: List e lst -> e (Last lst)
dropLast :: List e lst -> List e (DropLast lst)
stripPrefix :: GEq e => List e lst -> List e pre -> Maybe (List e (StripPrefix lst pre))
reverse :: List e lst -> List e (Reverse lst)
map :: List e lst -> (forall x. e x -> e (f x)) -> List e (Map lst f)
unmap :: List p lst -> List e (Map lst f) -> (forall x. e (f x) -> e x) -> List e lst
unmapM :: Monad m => List p lst -> List e (Map lst f) -> (forall x. e (f x) -> m (e x)) -> m (List e lst)
mapM' :: Monad m => List e lst -> (forall x. e x -> m (e (f x))) -> m (List e (Map lst f))
concat :: List e xs -> List e ys -> List e (Concat xs ys)
replicate :: Natural n -> e x -> List e (Replicate n x)
toList :: Monad m => (forall x. e x -> m a) -> List e lst -> m [a]
toListIndex :: Monad m => (forall n. Natural n -> e (Index lst n) -> m a) -> List e lst -> m [a]
foldM :: Monad m => (forall x. s -> e x -> m s) -> s -> List e lst -> m s
zipWithM :: Monad m => (forall x. e1 x -> e2 x -> m (e3 x)) -> List e1 lst -> List e2 lst -> m (List e3 lst)
zipToListM :: Monad m => (forall x. e1 x -> e2 x -> m a) -> List e1 lst -> List e2 lst -> m [a]
mapAccumM :: Monad m => (forall x. s -> e x -> m (s, e' x)) -> s -> List e xs -> m (s, List e' xs)
instance forall a (e :: a -> *) (lst :: [a]). Data.GADT.Compare.GEq a e => GHC.Classes.Eq (Language.SMTLib2.Internals.Type.List.List a e lst)
instance forall a (e :: a -> *). Data.GADT.Compare.GEq a e => Data.GADT.Compare.GEq [a] (Language.SMTLib2.Internals.Type.List.List a e)
instance forall a (e :: a -> *) (lst :: [a]). Data.GADT.Compare.GCompare a e => GHC.Classes.Ord (Language.SMTLib2.Internals.Type.List.List a e lst)
instance forall a (e :: a -> *). Data.GADT.Compare.GCompare a e => Data.GADT.Compare.GCompare [a] (Language.SMTLib2.Internals.Type.List.List a e)
instance forall a (e :: a -> *) (lst :: [a]). Data.GADT.Show.GShow a e => GHC.Show.Show (Language.SMTLib2.Internals.Type.List.List a e lst)
instance forall a (e :: a -> *). Data.GADT.Show.GShow a e => Data.GADT.Show.GShow [a] (Language.SMTLib2.Internals.Type.List.List a e)

module Language.SMTLib2.Internals.Type.Struct
data Tree a
Leaf :: a -> Tree a
Node :: [Tree a] -> Tree a
data Struct e tp
[Singleton] :: e t -> Struct e (Leaf t)
[Struct] :: List (Struct e) ts -> Struct e (Node ts)
access :: Monad m => Struct e tp -> List Natural idx -> (e (ElementIndex tp idx) -> m (a, e (ElementIndex tp idx))) -> m (a, Struct e tp)
accessElement :: Monad m => Struct e tp -> List Natural idx -> (e (ElementIndex tp idx) -> m (a, e ntp)) -> m (a, Struct e (Insert tp idx (Leaf ntp)))
index :: Struct e tp -> List Natural idx -> Struct e (Index tp idx)
elementIndex :: Struct e tp -> List Natural idx -> e (ElementIndex tp idx)
insert :: Struct e tps -> List Natural idx -> Struct e tp -> Struct e (Insert tps idx tp)
remove :: Struct e tps -> List Natural idx -> Struct e (Remove tps idx)
mapM :: Monad m => (forall x. e x -> m (e' x)) -> Struct e tps -> m (Struct e' tps)
mapIndexM :: Monad m => (forall idx. List Natural idx -> e (ElementIndex tps idx) -> m (e' (ElementIndex tps idx))) -> Struct e tps -> m (Struct e' tps)
map :: (forall x. e x -> e' x) -> Struct e tps -> Struct e' tps
size :: Struct e tps -> Natural (Size tps)
flatten :: Monad m => (forall x. e x -> m a) -> ([a] -> m a) -> Struct e tps -> m a
flattenIndex :: Monad m => (forall idx. List Natural idx -> e (ElementIndex tps idx) -> m a) -> ([a] -> m a) -> Struct e tps -> m a
zipWithM :: Monad m => (forall x. e1 x -> e2 x -> m (e3 x)) -> Struct e1 tps -> Struct e2 tps -> m (Struct e3 tps)
zipFlatten :: Monad m => (forall x. e1 x -> e2 x -> m a) -> ([a] -> m a) -> Struct e1 tps -> Struct e2 tps -> m a
instance forall a (e :: a -> *) (tps :: Language.SMTLib2.Internals.Type.Struct.Tree a). Data.GADT.Compare.GEq a e => GHC.Classes.Eq (Language.SMTLib2.Internals.Type.Struct.Struct a e tps)
instance forall a (e :: a -> *). Data.GADT.Compare.GEq a e => Data.GADT.Compare.GEq (Language.SMTLib2.Internals.Type.Struct.Tree a) (Language.SMTLib2.Internals.Type.Struct.Struct a e)
instance forall a (e :: a -> *) (tps :: Language.SMTLib2.Internals.Type.Struct.Tree a). Data.GADT.Compare.GCompare a e => GHC.Classes.Ord (Language.SMTLib2.Internals.Type.Struct.Struct a e tps)
instance forall a (e :: a -> *). Data.GADT.Compare.GCompare a e => Data.GADT.Compare.GCompare (Language.SMTLib2.Internals.Type.Struct.Tree a) (Language.SMTLib2.Internals.Type.Struct.Struct a e)
instance forall a (e :: a -> *) (tps :: Language.SMTLib2.Internals.Type.Struct.Tree a). Data.GADT.Show.GShow a e => GHC.Show.Show (Language.SMTLib2.Internals.Type.Struct.Struct a e tps)
instance forall a (e :: a -> *). Data.GADT.Show.GShow a e => Data.GADT.Show.GShow (Language.SMTLib2.Internals.Type.Struct.Tree a) (Language.SMTLib2.Internals.Type.Struct.Struct a e)

module Language.SMTLib2.Internals.Type

-- | Describes the kind of all SMT types. It is only used in promoted form,
--   for a concrete representation see <a>Repr</a>.
data Type
BoolType :: Type
IntType :: Type
RealType :: Type
BitVecType :: Nat -> Type
ArrayType :: [Type] -> Type -> Type
DataType :: a -> [Type] -> Type
ParameterType :: Nat -> Type
class Unlift (tps :: [Type]) (idx :: [Type])
unliftType :: Unlift tps idx => List Repr (Lifted tps idx) -> (List Repr tps, List Repr idx)
unliftTypeWith :: Unlift tps idx => List Repr (Lifted tps idx) -> List Repr tps -> List Repr idx
class (Typeable dt, Ord (Datatype dt), GCompare (Constr dt), GCompare (Field dt)) => IsDatatype (dt :: [Type] -> (Type -> *) -> *) where type Parameters dt :: Nat type Signature dt :: [[Type]] data Datatype dt :: * data Constr dt (csig :: [Type]) data Field dt (tp :: Type) where {
    type family Parameters dt :: Nat;
    type family Signature dt :: [[Type]];
    data family Datatype dt :: *;
    data family Constr dt (csig :: [Type]);
    data family Field dt (tp :: Type);
}

-- | Get the data type from a value
datatypeGet :: (IsDatatype dt, GetType e, Length par ~ Parameters dt) => dt par e -> (Datatype dt, List Repr par)

-- | How many polymorphic parameters does this datatype have
parameters :: IsDatatype dt => Datatype dt -> Natural (Parameters dt)

-- | The name of the datatype. Must be unique.
datatypeName :: IsDatatype dt => Datatype dt -> String

-- | Get all of the constructors of this datatype
constructors :: IsDatatype dt => Datatype dt -> List (Constr dt) (Signature dt)

-- | Get the name of a constructor
constrName :: IsDatatype dt => Constr dt csig -> String

-- | Test if a value is constructed using a specific constructor
test :: IsDatatype dt => dt par e -> Constr dt csig -> Bool

-- | Get all the fields of a constructor
fields :: IsDatatype dt => Constr dt csig -> List (Field dt) csig

-- | Construct a value using a constructor
construct :: (IsDatatype dt, Length par ~ Parameters dt) => List Repr par -> Constr dt csig -> List e (Instantiated csig par) -> dt par e

-- | Deconstruct a value into a constructor and a list of arguments
deconstruct :: (IsDatatype dt, GetType e) => dt par e -> ConApp dt par e

-- | Get the name of a field
fieldName :: IsDatatype dt => Field dt tp -> String

-- | Get the type of a field
fieldType :: IsDatatype dt => Field dt tp -> Repr tp

-- | Extract a field value from a value
fieldGet :: IsDatatype dt => dt par e -> Field dt tp -> e (CType tp par)
data ConApp dt par e
ConApp :: List Repr par -> Constr dt csig -> List e (Instantiated csig par) -> ConApp dt par e
[parameters'] :: ConApp dt par e -> List Repr par
[constructor] :: ConApp dt par e -> Constr dt csig
[arguments] :: ConApp dt par e -> List e (Instantiated csig par)
data AnyDatatype
AnyDatatype :: (Datatype dt) -> AnyDatatype
data AnyConstr
AnyConstr :: (Datatype dt) -> (Constr dt csig) -> AnyConstr
data AnyField
AnyField :: (Datatype dt) -> (Field dt tp) -> AnyField
data TypeRegistry dt con field
TypeRegistry :: Map dt AnyDatatype -> Map AnyDatatype dt -> Map con AnyConstr -> Map AnyConstr con -> Map field AnyField -> Map AnyField field -> TypeRegistry dt con field
[allDatatypes] :: TypeRegistry dt con field -> Map dt AnyDatatype
[revDatatypes] :: TypeRegistry dt con field -> Map AnyDatatype dt
[allConstructors] :: TypeRegistry dt con field -> Map con AnyConstr
[revConstructors] :: TypeRegistry dt con field -> Map AnyConstr con
[allFields] :: TypeRegistry dt con field -> Map field AnyField
[revFields] :: TypeRegistry dt con field -> Map AnyField field
emptyTypeRegistry :: TypeRegistry dt con field
dependencies :: IsDatatype dt => Set String -> Datatype dt -> (Set String, [[AnyDatatype]])
signature :: IsDatatype dt => Datatype dt -> List (List Repr) (Signature dt)
constrSig :: IsDatatype dt => Constr dt sig -> List Repr sig
instantiate :: List Repr sig -> List Repr par -> (List Repr (Instantiated sig par), Length sig :~: Length (Instantiated sig par))
ctype :: Repr tp -> List Repr par -> Repr (CType tp par)
determines :: IsDatatype dt => Datatype dt -> Constr dt sig -> Bool
containedParameter :: Repr tp -> Set Integer -> Set Integer
typeInference :: Repr atp -> Repr ctp -> (forall n ntp. Natural n -> Repr ntp -> a -> Maybe a) -> a -> Maybe a
typeInferences :: List Repr atps -> List Repr ctps -> (forall n ntp. Natural n -> Repr ntp -> a -> Maybe a) -> a -> Maybe a
partialInstantiation :: Repr tp -> (forall n a. Natural n -> (forall ntp. Repr ntp -> a) -> Maybe a) -> (forall rtp. Repr rtp -> a) -> a
partialInstantiations :: List Repr tp -> (forall n a. Natural n -> (forall ntp. Repr ntp -> a) -> Maybe a) -> (forall rtp. Length tp ~ Length rtp => List Repr rtp -> a) -> a
registerType :: (Monad m, IsDatatype tp, Ord dt, Ord con, Ord field) => dt -> (forall sig. Constr tp sig -> m con) -> (forall sig tp'. Field tp tp' -> m field) -> Datatype tp -> TypeRegistry dt con field -> m (TypeRegistry dt con field)
registerTypeName :: IsDatatype dt => Datatype dt -> TypeRegistry String String String -> TypeRegistry String String String
data DynamicDatatype (par :: Nat) (sig :: [[Type]])
DynDatatype :: Natural par -> List (DynamicConstructor sig) sig -> String -> DynamicDatatype
[dynDatatypeParameters] :: DynamicDatatype -> Natural par
[dynDatatypeSig] :: DynamicDatatype -> List (DynamicConstructor sig) sig
[dynDatatypeName] :: DynamicDatatype -> String
data DynamicConstructor (sig :: [[Type]]) (csig :: [Type])
[DynConstructor] :: Natural idx -> String -> List (DynamicField sig) (Index sig idx) -> DynamicConstructor sig (Index sig idx)
data DynamicField (sig :: [[Type]]) (tp :: Type)
[DynField] :: Natural idx -> Natural fidx -> String -> Repr (Index (Index sig idx) fidx) -> DynamicField sig (Index (Index sig idx) fidx)
data DynamicValue (plen :: Nat) (sig :: [[Type]]) (par :: [Type]) e
[DynValue] :: DynamicDatatype (Length par) sig -> List Repr par -> DynamicConstructor sig csig -> List e (Instantiated csig par) -> DynamicValue (Length par) sig par e
newtype BitWidth (bw :: Nat)
BitWidth :: Integer -> BitWidth
[bwSize] :: BitWidth -> Integer
getBw :: Integer -> (forall bw. KnownNat bw => BitWidth bw -> a) -> a

-- | Values that can be used as constants in expressions.
data Value (a :: Type)
[BoolValue] :: Bool -> Value BoolType
[IntValue] :: Integer -> Value IntType
[RealValue] :: Rational -> Value RealType
[BitVecValue] :: Integer -> BitWidth bw -> Value (BitVecType bw)
[DataValue] :: (IsDatatype dt, Length par ~ Parameters dt) => dt par Value -> Value (DataType dt par)
data AnyValue
AnyValue :: (Value t) -> AnyValue

-- | A concrete representation of an SMT type. For aesthetic reasons, it's
--   recommended to use the functions <a>bool</a>, <a>int</a>, <a>real</a>,
--   <a>bitvec</a> or <a>array</a>.
data Repr (t :: Type)
[BoolRepr] :: Repr BoolType
[IntRepr] :: Repr IntType
[RealRepr] :: Repr RealType
[BitVecRepr] :: BitWidth bw -> Repr (BitVecType bw)
[ArrayRepr] :: List Repr idx -> Repr val -> Repr (ArrayType idx val)
[DataRepr] :: (IsDatatype dt, Length par ~ Parameters dt) => Datatype dt -> List Repr par -> Repr (DataType dt par)
[ParameterRepr] :: Natural p -> Repr (ParameterType p)
data NumRepr (t :: Type)
[NumInt] :: NumRepr IntType
[NumReal] :: NumRepr RealType
data FunRepr (sig :: ([Type], Type))
[FunRepr] :: List Repr arg -> Repr tp -> FunRepr '(arg, tp)
class GetType v
getType :: GetType v => v tp -> Repr tp
class GetFunType fun
getFunType :: GetFunType fun => fun '(arg, res) -> (List Repr arg, Repr res)
bw :: KnownNat bw => Proxy bw -> BitWidth bw

-- | A representation of the SMT Bool type. Holds the values <a>true</a> or
--   <a>false</a>. Constants can be created using <a>cbool</a>.
bool :: Repr BoolType

-- | A representation of the SMT Int type. Holds the unbounded positive and
--   negative integers. Constants can be created using <a>cint</a>.
int :: Repr IntType

-- | A representation of the SMT Real type. Holds positive and negative
--   reals x/y where x and y are integers. Constants can be created using
--   <a>creal</a>.
real :: Repr RealType

-- | A typed representation of the SMT BitVec type. Holds bitvectors (a
--   vector of booleans) of a certain bitwidth. Constants can be created
--   using <a>cbv</a>.
bitvec :: BitWidth bw -> Repr (BitVecType bw)

-- | A representation of the SMT Array type. Has a list of index types and
--   an element type. Stores one value of the element type for each
--   combination of the index types. Constants can be created using
--   <a>constArray</a>.
array :: List Repr idx -> Repr el -> Repr (ArrayType idx el)

-- | A representation of a user-defined datatype without parameters.
dt :: (IsDatatype dt, Parameters dt ~ Z) => Datatype dt -> Repr (DataType dt '[])

-- | A representation of a user-defined datatype with parameters.
dt' :: (IsDatatype dt, Length par ~ Parameters dt) => Datatype dt -> List Repr par -> Repr (DataType dt par)
showBitVec :: Int -> Integer -> Integer -> ShowS
valueType :: Value tp -> Repr tp
liftType :: List Repr tps -> List Repr idx -> List Repr (Lifted tps idx)
numRepr :: NumRepr tp -> Repr tp
asNumRepr :: Repr tp -> Maybe (NumRepr tp)
getTypes :: GetType e => List e tps -> List Repr tps

-- | Determine the number of elements a type contains. <a>Nothing</a> means
--   the type has infinite elements.
typeSize :: Maybe (List Repr par) -> Repr tp -> Maybe Integer
typeFiniteDomain :: Repr tp -> Maybe [Value tp]
withBW :: KnownNat bw => (Proxy bw -> res (BitVecType bw)) -> res (BitVecType bw)
bvAdd :: Value (BitVecType bw) -> Value (BitVecType bw) -> Value (BitVecType bw)
bvSub :: Value (BitVecType bw) -> Value (BitVecType bw) -> Value (BitVecType bw)
bvMul :: Value (BitVecType bw) -> Value (BitVecType bw) -> Value (BitVecType bw)
bvDiv :: Value (BitVecType bw) -> Value (BitVecType bw) -> Value (BitVecType bw)
bvMod :: Value (BitVecType bw) -> Value (BitVecType bw) -> Value (BitVecType bw)
bvNegate :: Value (BitVecType bw) -> Value (BitVecType bw)
bvSignum :: Value (BitVecType bw) -> Value (BitVecType bw)

-- | Get the smallest bitvector value that is bigger than the given one.
--   Also known as the successor.
bvSucc :: Value (BitVecType bw) -> Value (BitVecType bw)

-- | Get the largest bitvector value that is smaller than the given one.
--   Also known as the predecessor.
bvPred :: Value (BitVecType bw) -> Value (BitVecType bw)

-- | Get the minimal value for a bitvector. If unsigned, the value is 0,
--   otherwise 2^(bw-1).
bvMinValue :: Bool -> Repr (BitVecType bw) -> Value (BitVecType bw)

-- | Get the maximal value for a bitvector. If unsigned, the value is
--   2^(bw-1)-1, otherwise 2^bw-1.
bvMaxValue :: Bool -> Repr (BitVecType bw) -> Value (BitVecType bw)
bwAdd :: BitWidth bw1 -> BitWidth bw2 -> BitWidth (bw1 + bw2)
datatypeEq :: (IsDatatype dt1, IsDatatype dt2) => Datatype dt1 -> Datatype dt2 -> Maybe (dt1 :~: dt2)
datatypeCompare :: (IsDatatype dt1, IsDatatype dt2) => Datatype dt1 -> Datatype dt2 -> GOrdering dt1 dt2
instance GHC.Classes.Ord (Language.SMTLib2.Internals.Type.DynamicDatatype par sig)
instance GHC.Classes.Eq (Language.SMTLib2.Internals.Type.DynamicDatatype par sig)
instance GHC.Classes.Ord (Language.SMTLib2.Internals.Type.Datatype (Language.SMTLib2.Internals.Type.DynamicValue l sig))
instance GHC.Classes.Eq (Language.SMTLib2.Internals.Type.Datatype (Language.SMTLib2.Internals.Type.DynamicValue l sig))
instance GHC.Show.Show (Language.SMTLib2.Internals.Type.NumRepr t)
instance Language.SMTLib2.Internals.Type.Unlift ((':) Language.SMTLib2.Internals.Type.Type tp ('[] Language.SMTLib2.Internals.Type.Type)) idx
instance Language.SMTLib2.Internals.Type.Unlift ((':) Language.SMTLib2.Internals.Type.Type t2 ts) idx => Language.SMTLib2.Internals.Type.Unlift ((':) Language.SMTLib2.Internals.Type.Type t1 ((':) Language.SMTLib2.Internals.Type.Type t2 ts)) idx
instance GHC.Classes.Eq Language.SMTLib2.Internals.Type.AnyDatatype
instance GHC.Classes.Eq Language.SMTLib2.Internals.Type.AnyConstr
instance GHC.Classes.Eq Language.SMTLib2.Internals.Type.AnyField
instance GHC.Classes.Ord Language.SMTLib2.Internals.Type.AnyDatatype
instance GHC.Classes.Ord Language.SMTLib2.Internals.Type.AnyConstr
instance GHC.Classes.Ord Language.SMTLib2.Internals.Type.AnyField
instance (Data.Typeable.Internal.Typeable Language.SMTLib2.Internals.Type.Nat.Nat l, Data.Typeable.Internal.Typeable [[Language.SMTLib2.Internals.Type.Type]] sig) => Language.SMTLib2.Internals.Type.IsDatatype (Language.SMTLib2.Internals.Type.DynamicValue l sig)
instance GHC.Show.Show (Language.SMTLib2.Internals.Type.Datatype (Language.SMTLib2.Internals.Type.DynamicValue l sig))
instance Data.GADT.Compare.GEq [Language.SMTLib2.Internals.Type.Type] (Language.SMTLib2.Internals.Type.DynamicConstructor sig)
instance Data.GADT.Compare.GCompare [Language.SMTLib2.Internals.Type.Type] (Language.SMTLib2.Internals.Type.DynamicConstructor sig)
instance Data.GADT.Compare.GEq [Language.SMTLib2.Internals.Type.Type] (Language.SMTLib2.Internals.Type.Constr (Language.SMTLib2.Internals.Type.DynamicValue l sig))
instance Data.GADT.Compare.GCompare [Language.SMTLib2.Internals.Type.Type] (Language.SMTLib2.Internals.Type.Constr (Language.SMTLib2.Internals.Type.DynamicValue l sig))
instance Data.GADT.Compare.GEq Language.SMTLib2.Internals.Type.Type (Language.SMTLib2.Internals.Type.Field (Language.SMTLib2.Internals.Type.DynamicValue l sig))
instance Data.GADT.Compare.GCompare Language.SMTLib2.Internals.Type.Type (Language.SMTLib2.Internals.Type.Field (Language.SMTLib2.Internals.Type.DynamicValue l sig))
instance GHC.Classes.Eq (Language.SMTLib2.Internals.Type.BitWidth bw)
instance Data.GADT.Compare.GEq GHC.Types.Nat Language.SMTLib2.Internals.Type.BitWidth
instance Data.GADT.Compare.GCompare GHC.Types.Nat Language.SMTLib2.Internals.Type.BitWidth
instance Language.SMTLib2.Internals.Type.GetType Language.SMTLib2.Internals.Type.Repr
instance Language.SMTLib2.Internals.Type.GetType Language.SMTLib2.Internals.Type.Value
instance Data.GADT.Compare.GEq Language.SMTLib2.Internals.Type.Type Language.SMTLib2.Internals.Type.Value
instance GHC.Classes.Eq (Language.SMTLib2.Internals.Type.Value t)
instance Data.GADT.Compare.GCompare Language.SMTLib2.Internals.Type.Type Language.SMTLib2.Internals.Type.Value
instance GHC.Classes.Ord (Language.SMTLib2.Internals.Type.Value t)
instance Data.GADT.Compare.GEq Language.SMTLib2.Internals.Type.Type Language.SMTLib2.Internals.Type.Repr
instance GHC.Classes.Eq (Language.SMTLib2.Internals.Type.Repr tp)
instance Data.GADT.Compare.GEq Language.SMTLib2.Internals.Type.Type Language.SMTLib2.Internals.Type.NumRepr
instance Data.GADT.Compare.GEq ([Language.SMTLib2.Internals.Type.Type], Language.SMTLib2.Internals.Type.Type) Language.SMTLib2.Internals.Type.FunRepr
instance Data.GADT.Compare.GCompare Language.SMTLib2.Internals.Type.Type Language.SMTLib2.Internals.Type.Repr
instance GHC.Classes.Ord (Language.SMTLib2.Internals.Type.Repr tp)
instance Data.GADT.Compare.GCompare Language.SMTLib2.Internals.Type.Type Language.SMTLib2.Internals.Type.NumRepr
instance Data.GADT.Compare.GCompare ([Language.SMTLib2.Internals.Type.Type], Language.SMTLib2.Internals.Type.Type) Language.SMTLib2.Internals.Type.FunRepr
instance GHC.Show.Show (Language.SMTLib2.Internals.Type.Value tp)
instance Data.GADT.Show.GShow Language.SMTLib2.Internals.Type.Type Language.SMTLib2.Internals.Type.Value
instance GHC.Show.Show (Language.SMTLib2.Internals.Type.Repr t)
instance Data.GADT.Show.GShow Language.SMTLib2.Internals.Type.Type Language.SMTLib2.Internals.Type.Repr
instance Data.GADT.Show.GShow Language.SMTLib2.Internals.Type.Type Language.SMTLib2.Internals.Type.NumRepr
instance GHC.Enum.Enum (Language.SMTLib2.Internals.Type.Value 'Language.SMTLib2.Internals.Type.BoolType)
instance GHC.Enum.Bounded (Language.SMTLib2.Internals.Type.Value 'Language.SMTLib2.Internals.Type.BoolType)
instance GHC.Num.Num (Language.SMTLib2.Internals.Type.Value 'Language.SMTLib2.Internals.Type.IntType)
instance GHC.Enum.Enum (Language.SMTLib2.Internals.Type.Value 'Language.SMTLib2.Internals.Type.IntType)
instance GHC.Real.Real (Language.SMTLib2.Internals.Type.Value 'Language.SMTLib2.Internals.Type.IntType)
instance GHC.Real.Integral (Language.SMTLib2.Internals.Type.Value 'Language.SMTLib2.Internals.Type.IntType)
instance GHC.Num.Num (Language.SMTLib2.Internals.Type.Value 'Language.SMTLib2.Internals.Type.RealType)
instance GHC.Real.Real (Language.SMTLib2.Internals.Type.Value 'Language.SMTLib2.Internals.Type.RealType)
instance GHC.Real.Fractional (Language.SMTLib2.Internals.Type.Value 'Language.SMTLib2.Internals.Type.RealType)
instance GHC.Real.RealFrac (Language.SMTLib2.Internals.Type.Value 'Language.SMTLib2.Internals.Type.RealType)
instance GHC.TypeLits.KnownNat bw => GHC.Num.Num (Language.SMTLib2.Internals.Type.Value ('Language.SMTLib2.Internals.Type.BitVecType bw))
instance GHC.TypeLits.KnownNat bw => GHC.Enum.Enum (Language.SMTLib2.Internals.Type.Value ('Language.SMTLib2.Internals.Type.BitVecType bw))
instance GHC.TypeLits.KnownNat bw => GHC.Enum.Bounded (Language.SMTLib2.Internals.Type.Value ('Language.SMTLib2.Internals.Type.BitVecType bw))
instance GHC.TypeLits.KnownNat bw => Data.Bits.Bits (Language.SMTLib2.Internals.Type.Value ('Language.SMTLib2.Internals.Type.BitVecType bw))
instance GHC.TypeLits.KnownNat bw => Data.Bits.FiniteBits (Language.SMTLib2.Internals.Type.Value ('Language.SMTLib2.Internals.Type.BitVecType bw))
instance GHC.TypeLits.KnownNat bw => GHC.Real.Real (Language.SMTLib2.Internals.Type.Value ('Language.SMTLib2.Internals.Type.BitVecType bw))
instance GHC.TypeLits.KnownNat bw => GHC.Real.Integral (Language.SMTLib2.Internals.Type.Value ('Language.SMTLib2.Internals.Type.BitVecType bw))
instance Language.SMTLib2.Internals.Type.GetType Language.SMTLib2.Internals.Type.NumRepr
instance GHC.Show.Show (Language.SMTLib2.Internals.Type.BitWidth bw)

module Language.SMTLib2.Internals.Expression
allEqToList :: Natural n -> List a (AllEq tp n) -> [a tp]
allEqFromList :: [a tp] -> (forall n. Natural n -> List a (AllEq tp n) -> r) -> r
allEqOf :: Repr tp -> Natural n -> List Repr (AllEq tp n)
mapAllEq :: Monad m => (e1 tp -> m (e2 tp)) -> Natural n -> List e1 (AllEq tp n) -> m (List e2 (AllEq tp n))
data Function (fun :: ([Type], Type) -> *) (sig :: ([Type], Type))
[Fun] :: fun '(arg, res) -> Function fun '(arg, res)
[Eq] :: Repr tp -> Natural n -> Function fun '(AllEq tp n, BoolType)
[Distinct] :: Repr tp -> Natural n -> Function fun '(AllEq tp n, BoolType)
[Map] :: List Repr idx -> Function fun '(arg, res) -> Function fun '(Lifted arg idx, ArrayType idx res)
[Ord] :: NumRepr tp -> OrdOp -> Function fun '('[tp, tp], BoolType)
[Arith] :: NumRepr tp -> ArithOp -> Natural n -> Function fun '(AllEq tp n, tp)
[ArithIntBin] :: ArithOpInt -> Function fun '('[IntType, IntType], IntType)
[Divide] :: Function fun '('[RealType, RealType], RealType)
[Abs] :: NumRepr tp -> Function fun '('[tp], tp)
[Not] :: Function fun '('[BoolType], BoolType)
[Logic] :: LogicOp -> Natural n -> Function fun '(AllEq BoolType n, BoolType)
[ToReal] :: Function fun '('[IntType], RealType)
[ToInt] :: Function fun '('[RealType], IntType)
[ITE] :: Repr a -> Function fun '('[BoolType, a, a], a)
[BVComp] :: BVCompOp -> BitWidth a -> Function fun '('[BitVecType a, BitVecType a], BoolType)
[BVBin] :: BVBinOp -> BitWidth a -> Function fun '('[BitVecType a, BitVecType a], BitVecType a)
[BVUn] :: BVUnOp -> BitWidth a -> Function fun '('[BitVecType a], BitVecType a)
[Select] :: List Repr idx -> Repr val -> Function fun '(ArrayType idx val : idx, val)
[Store] :: List Repr idx -> Repr val -> Function fun '(ArrayType idx val : (val : idx), ArrayType idx val)
[ConstArray] :: List Repr idx -> Repr val -> Function fun '('[val], ArrayType idx val)
[Concat] :: BitWidth n1 -> BitWidth n2 -> Function fun '('[BitVecType n1, BitVecType n2], BitVecType (n1 + n2))
[Extract] :: BitWidth bw -> BitWidth start -> BitWidth len -> Function fun '('[BitVecType bw], BitVecType len)
[Constructor] :: (IsDatatype dt, Length par ~ Parameters dt) => Datatype dt -> List Repr par -> Constr dt sig -> Function fun '(Instantiated sig par, DataType dt par)
[Test] :: (IsDatatype dt, Length par ~ Parameters dt) => Datatype dt -> List Repr par -> Constr dt sig -> Function fun '('[DataType dt par], BoolType)
[Field] :: (IsDatatype dt, Length par ~ Parameters dt) => Datatype dt -> List Repr par -> Field dt t -> Function fun '('[DataType dt par], CType t par)
[Divisible] :: Integer -> Function fun '('[IntType], BoolType)
data AnyFunction (fun :: ([Type], Type) -> *)
[AnyFunction] :: Function fun '(arg, t) -> AnyFunction fun
data OrdOp
Ge :: OrdOp
Gt :: OrdOp
Le :: OrdOp
Lt :: OrdOp
data ArithOp
Plus :: ArithOp
Mult :: ArithOp
Minus :: ArithOp
data ArithOpInt
Div :: ArithOpInt
Mod :: ArithOpInt
Rem :: ArithOpInt
data LogicOp
And :: LogicOp
Or :: LogicOp
XOr :: LogicOp
Implies :: LogicOp
data BVCompOp
BVULE :: BVCompOp
BVULT :: BVCompOp
BVUGE :: BVCompOp
BVUGT :: BVCompOp
BVSLE :: BVCompOp
BVSLT :: BVCompOp
BVSGE :: BVCompOp
BVSGT :: BVCompOp
data BVBinOp
BVAdd :: BVBinOp
BVSub :: BVBinOp
BVMul :: BVBinOp
BVURem :: BVBinOp
BVSRem :: BVBinOp
BVUDiv :: BVBinOp
BVSDiv :: BVBinOp
BVSHL :: BVBinOp
BVLSHR :: BVBinOp
BVASHR :: BVBinOp
BVXor :: BVBinOp
BVAnd :: BVBinOp
BVOr :: BVBinOp
data BVUnOp
BVNot :: BVUnOp
BVNeg :: BVUnOp
data LetBinding (v :: Type -> *) (e :: Type -> *) (t :: Type)
LetBinding :: v t -> e t -> LetBinding
[letVar] :: LetBinding -> v t
[letExpr] :: LetBinding -> e t
data Quantifier
Forall :: Quantifier
Exists :: Quantifier
data Expression (v :: Type -> *) (qv :: Type -> *) (fun :: ([Type], Type) -> *) (fv :: Type -> *) (lv :: Type -> *) (e :: Type -> *) (res :: Type)

-- | Free variable.
[Var] :: v res -> Expression v qv fun fv lv e res

-- | Quantified variable, i.e. a variable that's bound by a forall/exists
--   quantor.
[QVar] :: qv res -> Expression v qv fun fv lv e res

-- | A function argument variable. Only used in function bodies.
[FVar] :: fv res -> Expression v qv fun fv lv e res

-- | A variable bound by a let binding.
[LVar] :: lv res -> Expression v qv fun fv lv e res

-- | Function application
[App] :: Function fun '(arg, res) -> List e arg -> Expression v qv fun fv lv e res

-- | Constant
[Const] :: Value a -> Expression v qv fun fv lv e a

-- | AsArray converts a function into an array by using the function
--   arguments as array indices and the return type as array element.
[AsArray] :: Function fun '(arg, res) -> Expression v qv fun fv lv e (ArrayType arg res)

-- | Bind variables using a forall or exists quantor.
[Quantification] :: Quantifier -> List qv arg -> e BoolType -> Expression v qv fun fv lv e BoolType

-- | Bind variables to expressions.
[Let] :: List (LetBinding lv e) arg -> e res -> Expression v qv fun fv lv e res
class SMTOrd (t :: Type)
lt :: SMTOrd t => Function fun '('[t, t], BoolType)
le :: SMTOrd t => Function fun '('[t, t], BoolType)
gt :: SMTOrd t => Function fun '('[t, t], BoolType)
ge :: SMTOrd t => Function fun '('[t, t], BoolType)
class SMTArith t
arithFromInteger :: SMTArith t => Integer -> Value t
arith :: SMTArith t => ArithOp -> Natural n -> Function fun '(AllEq t n, t)
plus :: SMTArith t => Natural n -> Function fun '(AllEq t n, t)
minus :: SMTArith t => Natural n -> Function fun '(AllEq t n, t)
mult :: SMTArith t => Natural n -> Function fun '(AllEq t n, t)
abs' :: SMTArith t => Function fun '('[t], t)
functionType :: Monad m => (forall arg t. fun '(arg, t) -> m (List Repr arg, Repr t)) -> Function fun '(arg, res) -> m (List Repr arg, Repr res)
expressionType :: (Monad m, Functor m) => (forall t. v t -> m (Repr t)) -> (forall t. qv t -> m (Repr t)) -> (forall arg t. fun '(arg, t) -> m (List Repr arg, Repr t)) -> (forall t. fv t -> m (Repr t)) -> (forall t. lv t -> m (Repr t)) -> (forall t. e t -> m (Repr t)) -> Expression v qv fun fv lv e res -> m (Repr res)
mapExpr :: (Functor m, Monad m) => (forall t. v1 t -> m (v2 t)) -> (forall t. qv1 t -> m (qv2 t)) -> (forall arg t. fun1 '(arg, t) -> m (fun2 '(arg, t))) -> (forall t. fv1 t -> m (fv2 t)) -> (forall t. lv1 t -> m (lv2 t)) -> (forall t. e1 t -> m (e2 t)) -> Expression v1 qv1 fun1 fv1 lv1 e1 r -> m (Expression v2 qv2 fun2 fv2 lv2 e2 r)
mapFunction :: (Functor m, Monad m) => (forall arg t. fun1 '(arg, t) -> m (fun2 '(arg, t))) -> Function fun1 '(arg, res) -> m (Function fun2 '(arg, res))
data RenderMode
SMTRendering :: RenderMode
renderExprDefault :: (GetType qv, GShow v, GShow qv, GShow fun, GShow fv, GShow lv, GShow e) => RenderMode -> Expression v qv fun fv lv e tp -> ShowS
renderExpr :: (GetType qv) => RenderMode -> (forall tp. v tp -> ShowS) -> (forall tp. qv tp -> ShowS) -> (forall arg res. fun '(arg, res) -> ShowS) -> (forall tp. fv tp -> ShowS) -> (forall tp. lv tp -> ShowS) -> (forall tp. e tp -> ShowS) -> Expression v qv fun fv lv e tp -> ShowS
renderValue :: RenderMode -> Value tp -> ShowS
renderFunction :: RenderMode -> (forall arg res. fun '(arg, res) -> ShowS) -> Function fun '(arg, res) -> ShowS
renderType :: RenderMode -> Repr tp -> ShowS
renderTypes :: List Repr tps -> ShowS
data NoVar (t :: Type)
NoVar' :: NoVar
data NoFun (sig :: ([Type], Type))
NoFun' :: NoFun
data NoCon (sig :: ([Type], *))
NoCon' :: NoCon
data NoField (sig :: (*, Type))
NoField' :: NoField
instance GHC.Show.Show Language.SMTLib2.Internals.Expression.RenderMode
instance GHC.Classes.Ord Language.SMTLib2.Internals.Expression.RenderMode
instance GHC.Classes.Eq Language.SMTLib2.Internals.Expression.RenderMode
instance GHC.Show.Show Language.SMTLib2.Internals.Expression.Quantifier
instance GHC.Classes.Ord Language.SMTLib2.Internals.Expression.Quantifier
instance GHC.Classes.Eq Language.SMTLib2.Internals.Expression.Quantifier
instance GHC.Show.Show Language.SMTLib2.Internals.Expression.BVUnOp
instance GHC.Classes.Ord Language.SMTLib2.Internals.Expression.BVUnOp
instance GHC.Classes.Eq Language.SMTLib2.Internals.Expression.BVUnOp
instance GHC.Show.Show Language.SMTLib2.Internals.Expression.BVBinOp
instance GHC.Classes.Ord Language.SMTLib2.Internals.Expression.BVBinOp
instance GHC.Classes.Eq Language.SMTLib2.Internals.Expression.BVBinOp
instance GHC.Show.Show Language.SMTLib2.Internals.Expression.BVCompOp
instance GHC.Classes.Ord Language.SMTLib2.Internals.Expression.BVCompOp
instance GHC.Classes.Eq Language.SMTLib2.Internals.Expression.BVCompOp
instance GHC.Show.Show Language.SMTLib2.Internals.Expression.LogicOp
instance GHC.Classes.Ord Language.SMTLib2.Internals.Expression.LogicOp
instance GHC.Classes.Eq Language.SMTLib2.Internals.Expression.LogicOp
instance GHC.Show.Show Language.SMTLib2.Internals.Expression.ArithOpInt
instance GHC.Classes.Ord Language.SMTLib2.Internals.Expression.ArithOpInt
instance GHC.Classes.Eq Language.SMTLib2.Internals.Expression.ArithOpInt
instance GHC.Show.Show Language.SMTLib2.Internals.Expression.ArithOp
instance GHC.Classes.Ord Language.SMTLib2.Internals.Expression.ArithOp
instance GHC.Classes.Eq Language.SMTLib2.Internals.Expression.ArithOp
instance GHC.Show.Show Language.SMTLib2.Internals.Expression.OrdOp
instance GHC.Classes.Ord Language.SMTLib2.Internals.Expression.OrdOp
instance GHC.Classes.Eq Language.SMTLib2.Internals.Expression.OrdOp
instance Data.GADT.Compare.GEq ([Language.SMTLib2.Internals.Type.Type], Language.SMTLib2.Internals.Type.Type) fun => GHC.Classes.Eq (Language.SMTLib2.Internals.Expression.Function fun sig)
instance Language.SMTLib2.Internals.Expression.SMTOrd 'Language.SMTLib2.Internals.Type.IntType
instance Language.SMTLib2.Internals.Expression.SMTOrd 'Language.SMTLib2.Internals.Type.RealType
instance Language.SMTLib2.Internals.Expression.SMTArith 'Language.SMTLib2.Internals.Type.IntType
instance Language.SMTLib2.Internals.Expression.SMTArith 'Language.SMTLib2.Internals.Type.RealType
instance (Data.GADT.Show.GShow Language.SMTLib2.Internals.Type.Type v, Data.GADT.Show.GShow Language.SMTLib2.Internals.Type.Type qv, Data.GADT.Show.GShow ([Language.SMTLib2.Internals.Type.Type], Language.SMTLib2.Internals.Type.Type) fun, Data.GADT.Show.GShow Language.SMTLib2.Internals.Type.Type fv, Data.GADT.Show.GShow Language.SMTLib2.Internals.Type.Type lv, Data.GADT.Show.GShow Language.SMTLib2.Internals.Type.Type e) => GHC.Show.Show (Language.SMTLib2.Internals.Expression.Expression v qv fun fv lv e r)
instance (Data.GADT.Show.GShow Language.SMTLib2.Internals.Type.Type v, Data.GADT.Show.GShow Language.SMTLib2.Internals.Type.Type qv, Data.GADT.Show.GShow ([Language.SMTLib2.Internals.Type.Type], Language.SMTLib2.Internals.Type.Type) fun, Data.GADT.Show.GShow Language.SMTLib2.Internals.Type.Type fv, Data.GADT.Show.GShow Language.SMTLib2.Internals.Type.Type lv, Data.GADT.Show.GShow Language.SMTLib2.Internals.Type.Type e) => Data.GADT.Show.GShow Language.SMTLib2.Internals.Type.Type (Language.SMTLib2.Internals.Expression.Expression v qv fun fv lv e)
instance Data.GADT.Show.GShow ([Language.SMTLib2.Internals.Type.Type], Language.SMTLib2.Internals.Type.Type) fun => GHC.Show.Show (Language.SMTLib2.Internals.Expression.Function fun sig)
instance Data.GADT.Show.GShow ([Language.SMTLib2.Internals.Type.Type], Language.SMTLib2.Internals.Type.Type) fun => Data.GADT.Show.GShow ([Language.SMTLib2.Internals.Type.Type], Language.SMTLib2.Internals.Type.Type) (Language.SMTLib2.Internals.Expression.Function fun)
instance (Data.GADT.Compare.GEq Language.SMTLib2.Internals.Type.Type v, Data.GADT.Compare.GEq Language.SMTLib2.Internals.Type.Type e) => Data.GADT.Compare.GEq Language.SMTLib2.Internals.Type.Type (Language.SMTLib2.Internals.Expression.LetBinding v e)
instance (Data.GADT.Compare.GCompare Language.SMTLib2.Internals.Type.Type v, Data.GADT.Compare.GCompare Language.SMTLib2.Internals.Type.Type e) => Data.GADT.Compare.GCompare Language.SMTLib2.Internals.Type.Type (Language.SMTLib2.Internals.Expression.LetBinding v e)
instance (Data.GADT.Compare.GEq Language.SMTLib2.Internals.Type.Type v, Data.GADT.Compare.GEq Language.SMTLib2.Internals.Type.Type qv, Data.GADT.Compare.GEq ([Language.SMTLib2.Internals.Type.Type], Language.SMTLib2.Internals.Type.Type) fun, Data.GADT.Compare.GEq Language.SMTLib2.Internals.Type.Type fv, Data.GADT.Compare.GEq Language.SMTLib2.Internals.Type.Type lv, Data.GADT.Compare.GEq Language.SMTLib2.Internals.Type.Type e) => Data.GADT.Compare.GEq Language.SMTLib2.Internals.Type.Type (Language.SMTLib2.Internals.Expression.Expression v qv fun fv lv e)
instance (Data.GADT.Compare.GEq Language.SMTLib2.Internals.Type.Type v, Data.GADT.Compare.GEq Language.SMTLib2.Internals.Type.Type qv, Data.GADT.Compare.GEq ([Language.SMTLib2.Internals.Type.Type], Language.SMTLib2.Internals.Type.Type) fun, Data.GADT.Compare.GEq Language.SMTLib2.Internals.Type.Type fv, Data.GADT.Compare.GEq Language.SMTLib2.Internals.Type.Type lv, Data.GADT.Compare.GEq Language.SMTLib2.Internals.Type.Type e) => GHC.Classes.Eq (Language.SMTLib2.Internals.Expression.Expression v qv fun fv lv e t)
instance (Data.GADT.Compare.GCompare Language.SMTLib2.Internals.Type.Type v, Data.GADT.Compare.GCompare Language.SMTLib2.Internals.Type.Type qv, Data.GADT.Compare.GCompare ([Language.SMTLib2.Internals.Type.Type], Language.SMTLib2.Internals.Type.Type) fun, Data.GADT.Compare.GCompare Language.SMTLib2.Internals.Type.Type fv, Data.GADT.Compare.GCompare Language.SMTLib2.Internals.Type.Type lv, Data.GADT.Compare.GCompare Language.SMTLib2.Internals.Type.Type e) => Data.GADT.Compare.GCompare Language.SMTLib2.Internals.Type.Type (Language.SMTLib2.Internals.Expression.Expression v qv fun fv lv e)
instance (Data.GADT.Compare.GCompare Language.SMTLib2.Internals.Type.Type v, Data.GADT.Compare.GCompare Language.SMTLib2.Internals.Type.Type qv, Data.GADT.Compare.GCompare ([Language.SMTLib2.Internals.Type.Type], Language.SMTLib2.Internals.Type.Type) fun, Data.GADT.Compare.GCompare Language.SMTLib2.Internals.Type.Type fv, Data.GADT.Compare.GCompare Language.SMTLib2.Internals.Type.Type lv, Data.GADT.Compare.GCompare Language.SMTLib2.Internals.Type.Type e) => GHC.Classes.Ord (Language.SMTLib2.Internals.Expression.Expression v qv fun fv lv e t)
instance Data.GADT.Compare.GEq ([Language.SMTLib2.Internals.Type.Type], Language.SMTLib2.Internals.Type.Type) fun => Data.GADT.Compare.GEq ([Language.SMTLib2.Internals.Type.Type], Language.SMTLib2.Internals.Type.Type) (Language.SMTLib2.Internals.Expression.Function fun)
instance Data.GADT.Compare.GCompare ([Language.SMTLib2.Internals.Type.Type], Language.SMTLib2.Internals.Type.Type) fun => Data.GADT.Compare.GCompare ([Language.SMTLib2.Internals.Type.Type], Language.SMTLib2.Internals.Type.Type) (Language.SMTLib2.Internals.Expression.Function fun)
instance Data.GADT.Compare.GEq Language.SMTLib2.Internals.Type.Type Language.SMTLib2.Internals.Expression.NoVar
instance Data.GADT.Compare.GEq ([Language.SMTLib2.Internals.Type.Type], Language.SMTLib2.Internals.Type.Type) Language.SMTLib2.Internals.Expression.NoFun
instance Data.GADT.Compare.GEq ([Language.SMTLib2.Internals.Type.Type], GHC.Types.*) Language.SMTLib2.Internals.Expression.NoCon
instance Data.GADT.Compare.GEq (GHC.Types.*, Language.SMTLib2.Internals.Type.Type) Language.SMTLib2.Internals.Expression.NoField
instance Data.GADT.Compare.GCompare Language.SMTLib2.Internals.Type.Type Language.SMTLib2.Internals.Expression.NoVar
instance Data.GADT.Compare.GCompare ([Language.SMTLib2.Internals.Type.Type], Language.SMTLib2.Internals.Type.Type) Language.SMTLib2.Internals.Expression.NoFun
instance Data.GADT.Compare.GCompare ([Language.SMTLib2.Internals.Type.Type], GHC.Types.*) Language.SMTLib2.Internals.Expression.NoCon
instance Data.GADT.Compare.GCompare (GHC.Types.*, Language.SMTLib2.Internals.Type.Type) Language.SMTLib2.Internals.Expression.NoField
instance GHC.Classes.Eq (Language.SMTLib2.Internals.Expression.NoVar t)
instance GHC.Classes.Eq (Language.SMTLib2.Internals.Expression.NoFun t)
instance GHC.Classes.Eq (Language.SMTLib2.Internals.Expression.NoCon t)
instance GHC.Classes.Eq (Language.SMTLib2.Internals.Expression.NoField t)
instance GHC.Classes.Ord (Language.SMTLib2.Internals.Expression.NoVar t)
instance GHC.Classes.Ord (Language.SMTLib2.Internals.Expression.NoFun t)
instance GHC.Classes.Ord (Language.SMTLib2.Internals.Expression.NoCon t)
instance GHC.Classes.Ord (Language.SMTLib2.Internals.Expression.NoField t)
instance GHC.Show.Show (Language.SMTLib2.Internals.Expression.NoVar t)
instance Data.GADT.Show.GShow Language.SMTLib2.Internals.Type.Type Language.SMTLib2.Internals.Expression.NoVar
instance GHC.Show.Show (Language.SMTLib2.Internals.Expression.NoFun t)
instance Data.GADT.Show.GShow ([Language.SMTLib2.Internals.Type.Type], Language.SMTLib2.Internals.Type.Type) Language.SMTLib2.Internals.Expression.NoFun
instance GHC.Show.Show (Language.SMTLib2.Internals.Expression.NoCon t)
instance Data.GADT.Show.GShow ([Language.SMTLib2.Internals.Type.Type], GHC.Types.*) Language.SMTLib2.Internals.Expression.NoCon
instance GHC.Show.Show (Language.SMTLib2.Internals.Expression.NoField t)
instance Data.GADT.Show.GShow (GHC.Types.*, Language.SMTLib2.Internals.Type.Type) Language.SMTLib2.Internals.Expression.NoField
instance Language.SMTLib2.Internals.Type.GetType Language.SMTLib2.Internals.Expression.NoVar
instance Language.SMTLib2.Internals.Type.GetFunType Language.SMTLib2.Internals.Expression.NoFun
instance (Language.SMTLib2.Internals.Type.GetType v, Language.SMTLib2.Internals.Type.GetType qv, Language.SMTLib2.Internals.Type.GetFunType fun, Language.SMTLib2.Internals.Type.GetType fv, Language.SMTLib2.Internals.Type.GetType lv, Language.SMTLib2.Internals.Type.GetType e) => Language.SMTLib2.Internals.Type.GetType (Language.SMTLib2.Internals.Expression.Expression v qv fun fv lv e)
instance Language.SMTLib2.Internals.Type.GetFunType fun => Language.SMTLib2.Internals.Type.GetFunType (Language.SMTLib2.Internals.Expression.Function fun)

module Language.SMTLib2.Internals.Proof
data ProofResult (e :: Type -> *)
ProofExpr :: (e BoolType) -> ProofResult
EquivSat :: (e BoolType) -> (e BoolType) -> ProofResult
data Proof r (e :: Type -> *) p
Rule :: r -> [p] -> (ProofResult e) -> Proof r p
verifyProof :: (Monad m, Ord p, Show r, Show p) => (p -> m (Proof r e p)) -> (r -> [ProofResult e] -> ProofResult e -> ExceptT String m ()) -> p -> StateT (Map p (ProofResult e)) (ExceptT String m) (ProofResult e)
renderProof :: (Monad m, Ord p, Show r) => (forall tp. e tp -> ShowS) -> (p -> m (Proof r e p)) -> p -> m ShowS
renderProof' :: (Monad m, Ord p, Show r) => (forall tp. e tp -> ShowS) -> (p -> m (Proof r e p)) -> p -> StateT (Map p Int) (WriterT (Endo String) m) Int
renderProofResult :: (forall tp. e tp -> ShowS) -> ProofResult e -> ShowS
mapProof :: (forall tp. e tp -> e' tp) -> Proof r e p -> Proof r e' p
instance Data.GADT.Show.GShow Language.SMTLib2.Internals.Type.Type e => GHC.Show.Show (Language.SMTLib2.Internals.Proof.ProofResult e)

module Language.SMTLib2.Internals.Evaluate
data EvalResult fun res
[ValueResult] :: Value res -> EvalResult fun res
[ArrayResult] :: ArrayModel fun idx el -> EvalResult fun (ArrayType idx el)
data ArrayModel fun idx el
[ArrayConst] :: EvalResult fun el -> List Repr idx -> ArrayModel fun idx el
[ArrayFun] :: Function fun '(idx, res) -> ArrayModel fun idx res
[ArrayMap] :: Function fun '(arg, res) -> List (ArrayModel fun idx) arg -> List Repr idx -> ArrayModel fun idx res
[ArrayStore] :: List (EvalResult fun) idx -> EvalResult fun el -> ArrayModel fun idx el -> ArrayModel fun idx el
type FunctionEval m fun = forall tps r. fun '(tps, r) -> List (EvalResult fun) tps -> m (EvalResult fun r)
type FieldEval m fun = forall dt par args tp. (IsDatatype dt) => List Repr par -> Field dt tp -> List Value args -> m (EvalResult fun (CType tp par))
evalResultType :: (GetFunType fun) => EvalResult fun res -> Repr res
arrayModelType :: (GetFunType fun) => ArrayModel fun idx res -> (List Repr idx, Repr res)
evaluateArray :: (Monad m, GetFunType fun) => FunctionEval m fun -> FieldEval m fun -> ArrayModel fun idx el -> List (EvalResult fun) idx -> m (EvalResult fun el)
typeNumElements :: Repr t -> Maybe Integer
evalResultEq :: (Monad m, GetFunType fun) => FunctionEval m fun -> FieldEval m fun -> EvalResult fun res -> EvalResult fun res -> m Bool
arrayModelEq :: (Monad m, GetFunType fun) => FunctionEval m fun -> FieldEval m fun -> ArrayModel fun idx t -> ArrayModel fun idx t -> [List (EvalResult fun) idx] -> m Bool
evaluateExpr :: (Monad m, GCompare lv, GetFunType fun) => (forall t. v t -> m (EvalResult fun t)) -> (forall t. qv t -> m (EvalResult fun t)) -> (forall t. fv t -> m (EvalResult fun t)) -> FunctionEval m fun -> FieldEval m fun -> (forall arg. Quantifier -> List qv arg -> e BoolType -> m (EvalResult fun BoolType)) -> DMap lv (EvalResult fun) -> (forall t. DMap lv (EvalResult fun) -> e t -> m (EvalResult fun t)) -> Expression v qv fun fv lv e res -> m (EvalResult fun res)
evaluateFun :: forall m fun arg res. (Monad m, GetFunType fun) => FunctionEval m fun -> FieldEval m fun -> Function fun '(arg, res) -> List (EvalResult fun) arg -> m (EvalResult fun res)
getArrayModelType :: GetFunType fun => ArrayModel fun idx el -> (List Repr idx, Repr el)
geqArrayModel :: GEq fun => ArrayModel fun idx1 el1 -> ArrayModel fun idx2 el2 -> Maybe (idx1 :~: idx2, el1 :~: el2)
gcompareArrayModel :: GCompare fun => ArrayModel fun idx1 el1 -> ArrayModel fun idx2 el2 -> (GOrdering idx1 idx2, GOrdering el1 el2)
instance Language.SMTLib2.Internals.Type.GetFunType fun => Language.SMTLib2.Internals.Type.GetType (Language.SMTLib2.Internals.Evaluate.EvalResult fun)
instance Data.GADT.Show.GShow ([Language.SMTLib2.Internals.Type.Type], Language.SMTLib2.Internals.Type.Type) fun => GHC.Show.Show (Language.SMTLib2.Internals.Evaluate.EvalResult fun res)
instance Data.GADT.Show.GShow ([Language.SMTLib2.Internals.Type.Type], Language.SMTLib2.Internals.Type.Type) fun => GHC.Show.Show (Language.SMTLib2.Internals.Evaluate.ArrayModel fun idx el)
instance Data.GADT.Show.GShow ([Language.SMTLib2.Internals.Type.Type], Language.SMTLib2.Internals.Type.Type) fun => Data.GADT.Show.GShow Language.SMTLib2.Internals.Type.Type (Language.SMTLib2.Internals.Evaluate.EvalResult fun)
instance Data.GADT.Show.GShow ([Language.SMTLib2.Internals.Type.Type], Language.SMTLib2.Internals.Type.Type) fun => Data.GADT.Show.GShow Language.SMTLib2.Internals.Type.Type (Language.SMTLib2.Internals.Evaluate.ArrayModel fun idx)
instance Data.GADT.Compare.GEq ([Language.SMTLib2.Internals.Type.Type], Language.SMTLib2.Internals.Type.Type) fun => Data.GADT.Compare.GEq Language.SMTLib2.Internals.Type.Type (Language.SMTLib2.Internals.Evaluate.EvalResult fun)
instance Data.GADT.Compare.GCompare ([Language.SMTLib2.Internals.Type.Type], Language.SMTLib2.Internals.Type.Type) fun => Data.GADT.Compare.GCompare Language.SMTLib2.Internals.Type.Type (Language.SMTLib2.Internals.Evaluate.EvalResult fun)

module Language.SMTLib2.Internals.Backend
type SMTAction b r = b -> SMTMonad b (r, b)
mapAction :: Backend b => (r -> r') -> SMTAction b r -> SMTAction b r'

-- | A backend represents a specific type of SMT solver.
class (Typeable b, Functor (SMTMonad b), Monad (SMTMonad b), GetType (Expr b), GetType (Var b), GetType (QVar b), GetFunType (Fun b), GetType (FunArg b), GetType (LVar b), Typeable (Expr b), Typeable (Var b), Typeable (QVar b), Typeable (Fun b), Typeable (FunArg b), Typeable (LVar b), Typeable (ClauseId b), GCompare (Expr b), GShow (Expr b), GCompare (Var b), GShow (Var b), GCompare (QVar b), GShow (QVar b), GCompare (Fun b), GShow (Fun b), GCompare (FunArg b), GShow (FunArg b), GCompare (LVar b), GShow (LVar b), Ord (ClauseId b), Show (ClauseId b), Ord (Proof b), Show (Proof b), Show (Model b)) => Backend b where type SMTMonad b :: * -> * data Expr b :: Type -> * type Var b :: Type -> * type QVar b :: Type -> * type Fun b :: ([Type], Type) -> * type FunArg b :: Type -> * type LVar b :: Type -> * type ClauseId b :: * type Model b :: * type Proof b :: * comment _ b = return ((), b) where {
    type family SMTMonad b :: * -> *;
    data family Expr b :: Type -> *;
    type family Var b :: Type -> *;
    type family QVar b :: Type -> *;
    type family Fun b :: ([Type], Type) -> *;
    type family FunArg b :: Type -> *;
    type family LVar b :: Type -> *;
    type family ClauseId b :: *;
    type family Model b :: *;
    type family Proof b :: *;
}
setOption :: Backend b => SMTOption -> SMTAction b ()
getInfo :: Backend b => SMTInfo i -> SMTAction b i
comment :: Backend b => String -> SMTAction b ()
push :: Backend b => SMTAction b ()
pop :: Backend b => SMTAction b ()
declareVar :: Backend b => Repr t -> Maybe String -> SMTAction b (Var b t)
createQVar :: Backend b => Repr t -> Maybe String -> SMTAction b (QVar b t)
createFunArg :: Backend b => Repr t -> Maybe String -> SMTAction b (FunArg b t)
defineVar :: Backend b => Maybe String -> Expr b t -> SMTAction b (Var b t)
declareFun :: Backend b => List Repr arg -> Repr t -> Maybe String -> SMTAction b (Fun b '(arg, t))
defineFun :: Backend b => Maybe String -> List (FunArg b) arg -> Expr b r -> SMTAction b (Fun b '(arg, r))
assert :: Backend b => Expr b BoolType -> SMTAction b ()
assertId :: Backend b => Expr b BoolType -> SMTAction b (ClauseId b)
assertPartition :: Backend b => Expr b BoolType -> Partition -> SMTAction b ()
checkSat :: Backend b => Maybe Tactic -> CheckSatLimits -> SMTAction b CheckSatResult
getUnsatCore :: Backend b => SMTAction b [ClauseId b]
getValue :: Backend b => Expr b t -> SMTAction b (Value t)
getModel :: Backend b => SMTAction b (Model b)
modelEvaluate :: Backend b => Model b -> Expr b t -> SMTAction b (Value t)
getProof :: Backend b => SMTAction b (Proof b)
analyzeProof :: Backend b => b -> Proof b -> Proof String (Expr b) (Proof b)
simplify :: Backend b => Expr b t -> SMTAction b (Expr b t)
toBackend :: Backend b => Expression (Var b) (QVar b) (Fun b) (FunArg b) (LVar b) (Expr b) t -> SMTAction b (Expr b t)
fromBackend :: Backend b => b -> Expr b t -> Expression (Var b) (QVar b) (Fun b) (FunArg b) (LVar b) (Expr b) t
declareDatatypes :: Backend b => [AnyDatatype] -> SMTAction b ()
interpolate :: Backend b => SMTAction b (Expr b BoolType)
exit :: Backend b => SMTAction b ()

-- | The interpolation partition
data Partition
PartitionA :: Partition
PartitionB :: Partition

-- | The result of a check-sat query
data CheckSatResult

-- | The formula is satisfiable
Sat :: CheckSatResult

-- | The formula is unsatisfiable
Unsat :: CheckSatResult

-- | The solver cannot determine the satisfiability of a formula
Unknown :: CheckSatResult

-- | Describe limits on the ressources that an SMT-solver can use
data CheckSatLimits
CheckSatLimits :: Maybe Integer -> Maybe Integer -> CheckSatLimits

-- | A limit on the amount of time the solver can spend on the problem (in
--   milliseconds)
[limitTime] :: CheckSatLimits -> Maybe Integer

-- | A limit on the amount of memory the solver can use (in megabytes)
[limitMemory] :: CheckSatLimits -> Maybe Integer
newtype AssignmentModel b
AssignmentModel :: [Assignment b] -> AssignmentModel b
[assignments] :: AssignmentModel b -> [Assignment b]
data Assignment b
VarAssignment :: (Var b t) -> (Expr b t) -> Assignment b
FunAssignment :: (Fun b '(arg, t)) -> (List (FunArg b) arg) -> (Expr b t) -> Assignment b

-- | Options controling the behaviour of the SMT solver
data SMTOption

-- | Whether or not to print "success" after each operation
PrintSuccess :: Bool -> SMTOption

-- | Produce a satisfying assignment after each successful checkSat
ProduceModels :: Bool -> SMTOption

-- | Produce a proof of unsatisfiability after each failed checkSat
ProduceProofs :: Bool -> SMTOption

-- | Enable the querying of unsatisfiable cores after a failed checkSat
ProduceUnsatCores :: Bool -> SMTOption

-- | Enable the generation of craig interpolants
ProduceInterpolants :: Bool -> SMTOption
SMTLogic :: String -> SMTOption

-- | Solver information query type. Used with <a>getInfo</a>.
data SMTInfo i
[SMTSolverName] :: SMTInfo String
[SMTSolverVersion] :: SMTInfo String
data UntypedVar v (t :: Type)
UntypedVar :: v -> (Repr t) -> UntypedVar v
data UntypedFun v (sig :: ([Type], Type))
[UntypedFun] :: v -> List Repr arg -> Repr ret -> UntypedFun v '(arg, ret)
data RenderedSubExpr t
RenderedSubExpr :: (Int -> ShowS) -> RenderedSubExpr t
showsBackendExpr :: (Backend b) => b -> Int -> Expr b t -> ShowS
instance GHC.Classes.Ord Language.SMTLib2.Internals.Backend.SMTOption
instance GHC.Classes.Eq Language.SMTLib2.Internals.Backend.SMTOption
instance GHC.Show.Show Language.SMTLib2.Internals.Backend.SMTOption
instance GHC.Classes.Ord Language.SMTLib2.Internals.Backend.CheckSatLimits
instance GHC.Classes.Eq Language.SMTLib2.Internals.Backend.CheckSatLimits
instance GHC.Show.Show Language.SMTLib2.Internals.Backend.CheckSatLimits
instance GHC.Classes.Ord Language.SMTLib2.Internals.Backend.CheckSatResult
instance GHC.Classes.Eq Language.SMTLib2.Internals.Backend.CheckSatResult
instance GHC.Show.Show Language.SMTLib2.Internals.Backend.CheckSatResult
instance GHC.Classes.Ord Language.SMTLib2.Internals.Backend.Partition
instance GHC.Classes.Eq Language.SMTLib2.Internals.Backend.Partition
instance GHC.Show.Show Language.SMTLib2.Internals.Backend.Partition
instance Data.GADT.Show.GShow k (Language.SMTLib2.Internals.Backend.RenderedSubExpr k)
instance GHC.Classes.Eq v => GHC.Classes.Eq (Language.SMTLib2.Internals.Backend.UntypedVar v t)
instance GHC.Classes.Eq v => GHC.Classes.Eq (Language.SMTLib2.Internals.Backend.UntypedFun v sig)
instance GHC.Classes.Ord v => GHC.Classes.Ord (Language.SMTLib2.Internals.Backend.UntypedVar v t)
instance GHC.Classes.Ord v => GHC.Classes.Ord (Language.SMTLib2.Internals.Backend.UntypedFun v sig)
instance GHC.Classes.Eq v => Data.GADT.Compare.GEq Language.SMTLib2.Internals.Type.Type (Language.SMTLib2.Internals.Backend.UntypedVar v)
instance GHC.Classes.Eq v => Data.GADT.Compare.GEq ([Language.SMTLib2.Internals.Type.Type], Language.SMTLib2.Internals.Type.Type) (Language.SMTLib2.Internals.Backend.UntypedFun v)
instance GHC.Classes.Ord v => Data.GADT.Compare.GCompare Language.SMTLib2.Internals.Type.Type (Language.SMTLib2.Internals.Backend.UntypedVar v)
instance GHC.Classes.Ord v => Data.GADT.Compare.GCompare ([Language.SMTLib2.Internals.Type.Type], Language.SMTLib2.Internals.Type.Type) (Language.SMTLib2.Internals.Backend.UntypedFun v)
instance GHC.Show.Show v => GHC.Show.Show (Language.SMTLib2.Internals.Backend.UntypedVar v t)
instance GHC.Show.Show v => GHC.Show.Show (Language.SMTLib2.Internals.Backend.UntypedFun v sig)
instance GHC.Show.Show v => Data.GADT.Show.GShow Language.SMTLib2.Internals.Type.Type (Language.SMTLib2.Internals.Backend.UntypedVar v)
instance GHC.Show.Show v => Data.GADT.Show.GShow ([Language.SMTLib2.Internals.Type.Type], Language.SMTLib2.Internals.Type.Type) (Language.SMTLib2.Internals.Backend.UntypedFun v)
instance Language.SMTLib2.Internals.Type.GetType (Language.SMTLib2.Internals.Backend.UntypedVar v)
instance Language.SMTLib2.Internals.Type.GetFunType (Language.SMTLib2.Internals.Backend.UntypedFun v)
instance (Data.GADT.Show.GShow Language.SMTLib2.Internals.Type.Type (Language.SMTLib2.Internals.Backend.Var b), Data.GADT.Show.GShow Language.SMTLib2.Internals.Type.Type (Language.SMTLib2.Internals.Backend.Expr b), Data.GADT.Show.GShow ([Language.SMTLib2.Internals.Type.Type], Language.SMTLib2.Internals.Type.Type) (Language.SMTLib2.Internals.Backend.Fun b), Data.GADT.Show.GShow Language.SMTLib2.Internals.Type.Type (Language.SMTLib2.Internals.Backend.FunArg b)) => GHC.Show.Show (Language.SMTLib2.Internals.Backend.Assignment b)
instance (Data.GADT.Show.GShow Language.SMTLib2.Internals.Type.Type (Language.SMTLib2.Internals.Backend.Var b), Data.GADT.Show.GShow Language.SMTLib2.Internals.Type.Type (Language.SMTLib2.Internals.Backend.Expr b), Data.GADT.Show.GShow ([Language.SMTLib2.Internals.Type.Type], Language.SMTLib2.Internals.Type.Type) (Language.SMTLib2.Internals.Backend.Fun b), Data.GADT.Show.GShow Language.SMTLib2.Internals.Type.Type (Language.SMTLib2.Internals.Backend.FunArg b)) => GHC.Show.Show (Language.SMTLib2.Internals.Backend.AssignmentModel b)

module Language.SMTLib2.Internals.Monad

-- | The SMT monad is used to perform communication with the SMT solver.
--   The type of solver is given by the <i>b</i> parameter.
newtype SMT b a
SMT :: StateT (SMTState b) (SMTMonad b) a -> SMT b a
[runSMT] :: SMT b a -> StateT (SMTState b) (SMTMonad b) a
data SMTState b
SMTState :: !b -> !(Set String) -> SMTState b
[backend] :: SMTState b -> !b
[datatypes] :: SMTState b -> !(Set String)

-- | Execute an SMT action on a given backend.
withBackend :: Backend b => SMTMonad b b -> SMT b a -> SMTMonad b a

-- | Like <a>withBackend</a> but specialized to the <a>IO</a> monad so
--   exeptions can be handled by gracefully exiting the solver.
withBackendExitCleanly :: (Backend b, SMTMonad b ~ IO) => IO b -> SMT b a -> IO a
liftSMT :: Backend b => SMTMonad b a -> SMT b a
embedSMT :: Backend b => (b -> SMTMonad b (a, b)) -> SMT b a
embedSMT' :: Backend b => (b -> SMTMonad b b) -> SMT b ()
registerDatatype :: (Backend b, IsDatatype dt) => Datatype dt -> SMT b ()
defineVar' :: (Backend b) => Expr b t -> SMT b (Var b t)
defineVarNamed' :: (Backend b) => String -> Expr b t -> SMT b (Var b t)
declareVar' :: Backend b => Repr t -> SMT b (Var b t)
declareVarNamed' :: Backend b => Repr t -> String -> SMT b (Var b t)
instance Language.SMTLib2.Internals.Backend.Backend b => GHC.Base.Functor (Language.SMTLib2.Internals.Monad.SMT b)
instance Language.SMTLib2.Internals.Backend.Backend b => GHC.Base.Applicative (Language.SMTLib2.Internals.Monad.SMT b)
instance Language.SMTLib2.Internals.Backend.Backend b => GHC.Base.Monad (Language.SMTLib2.Internals.Monad.SMT b)
instance Language.SMTLib2.Internals.Backend.Backend b => Control.Monad.State.Class.MonadState (Language.SMTLib2.Internals.Monad.SMTState b) (Language.SMTLib2.Internals.Monad.SMT b)
instance (Language.SMTLib2.Internals.Backend.Backend b, Control.Monad.IO.Class.MonadIO (Language.SMTLib2.Internals.Backend.SMTMonad b)) => Control.Monad.IO.Class.MonadIO (Language.SMTLib2.Internals.Monad.SMT b)

module Language.SMTLib2.Internals.Embed
type EmbedExpr m e tp = Expression (EmVar m e) (EmQVar m e) (EmFun m e) (EmFunArg m e) (EmLVar m e) e tp

-- | A class of <a>Monad</a>s that can be used to form SMTLib expressions.
--   The default instance of this class is the <a>SMT</a> monad, together
--   with its associated <a>Expr</a> type. An interesting instance is the
--   <a>Identity</a> monad with the <a>Value</a> type, which allows
--   evaluation of SMTLib expressions.
class (Applicative m, GCompare (EmVar m e), GCompare (EmQVar m e), GCompare (EmFun m e), GCompare (EmFunArg m e), GCompare (EmLVar m e)) => Embed m e where type EmVar m e :: Type -> * type EmQVar m e :: Type -> * type EmFun m e :: ([Type], Type) -> * type EmFunArg m e :: Type -> * type EmLVar m e :: Type -> * where {
    type family EmVar m e :: Type -> *;
    type family EmQVar m e :: Type -> *;
    type family EmFun m e :: ([Type], Type) -> *;
    type family EmFunArg m e :: Type -> *;
    type family EmLVar m e :: Type -> *;
}
embed :: Embed m e => m (EmbedExpr m e tp) -> m (e tp)
embedQuantifier :: Embed m e => Quantifier -> List Repr arg -> (forall m e. (Embed m e, Monad m) => List (EmQVar m e) arg -> m (e BoolType)) -> m (e BoolType)
embedTypeOf :: Embed m e => m (e tp -> Repr tp)
class (GCompare (ExVar i e), GCompare (ExQVar i e), GCompare (ExFun i e), GCompare (ExFunArg i e), GCompare (ExLVar i e)) => Extract i e where type ExVar i e :: Type -> * type ExQVar i e :: Type -> * type ExFun i e :: ([Type], Type) -> * type ExFunArg i e :: Type -> * type ExLVar i e :: Type -> * where {
    type family ExVar i e :: Type -> *;
    type family ExQVar i e :: Type -> *;
    type family ExFun i e :: ([Type], Type) -> *;
    type family ExFunArg i e :: Type -> *;
    type family ExLVar i e :: Type -> *;
}
extract :: Extract i e => i -> e tp -> Maybe (Expression (ExVar i e) (ExQVar i e) (ExFun i e) (ExFunArg i e) (ExLVar i e) e tp)

-- | A user-supplied function. Can be used in embedding <a>Value</a>s or
--   <a>EvalResult</a>s. Since we don't have function equality in haskell,
--   an integer is provided to distinguish functions.
data UserFun (m :: * -> *) (e :: Type -> *) (sig :: ([Type], Type))
[UserFun] :: List Repr arg -> Repr res -> Int -> (List e arg -> m (e res)) -> UserFun m e '(arg, res)
newtype ValueExt m tp
ValueExt :: EvalResult (UserFun m (ValueExt m)) tp -> ValueExt m tp
[valueExt] :: ValueExt m tp -> EvalResult (UserFun m (ValueExt m)) tp
newtype BackendInfo b
BackendInfo :: b -> BackendInfo b
data SMTExpr var qvar fun farg lvar tp
[SMTExpr] :: Expression var qvar fun farg lvar (SMTExpr var qvar fun farg lvar) tp -> SMTExpr var qvar fun farg lvar tp
[SMTQuant] :: Quantifier -> List Repr args -> (List qvar args -> SMTExpr var qvar fun farg lvar BoolType) -> SMTExpr var qvar fun farg lvar BoolType
encodeExpr :: (Backend b) => SMTExpr (Var b) (QVar b) (Fun b) (FunArg b) (LVar b) tp -> SMT b (Expr b tp)
decodeExpr :: (Backend b) => Expr b tp -> SMT b (SMTExpr (Var b) (QVar b) (Fun b) (FunArg b) (LVar b) tp)
data AnalyzedExpr i e tp
AnalyzedExpr :: (Maybe (Expression (ExVar i e) (ExQVar i e) (ExFun i e) (ExFunArg i e) (ExLVar i e) (AnalyzedExpr i e) tp)) -> (e tp) -> AnalyzedExpr i e tp
analyze' :: (Extract i e) => i -> e tp -> AnalyzedExpr i e tp
analyze :: (Backend b) => Expr b tp -> SMT b (AnalyzedExpr (BackendInfo b) (Expr b) tp)
instance Language.SMTLib2.Internals.Backend.Backend b => Language.SMTLib2.Internals.Embed.Embed (Language.SMTLib2.Internals.Monad.SMT b) (Language.SMTLib2.Internals.Backend.Expr b)
instance Language.SMTLib2.Internals.Embed.Embed Data.Functor.Identity.Identity Language.SMTLib2.Internals.Type.Repr
instance Data.GADT.Compare.GEq ([Language.SMTLib2.Internals.Type.Type], Language.SMTLib2.Internals.Type.Type) (Language.SMTLib2.Internals.Embed.UserFun m e)
instance Data.GADT.Compare.GCompare ([Language.SMTLib2.Internals.Type.Type], Language.SMTLib2.Internals.Type.Type) (Language.SMTLib2.Internals.Embed.UserFun m e)
instance Language.SMTLib2.Internals.Type.GetFunType (Language.SMTLib2.Internals.Embed.UserFun m e)
instance Data.GADT.Show.GShow ([Language.SMTLib2.Internals.Type.Type], Language.SMTLib2.Internals.Type.Type) (Language.SMTLib2.Internals.Embed.UserFun m e)
instance Language.SMTLib2.Internals.Embed.Embed Data.Functor.Identity.Identity Language.SMTLib2.Internals.Type.Value
instance Language.SMTLib2.Internals.Type.GetType (Language.SMTLib2.Internals.Embed.ValueExt m)
instance Data.GADT.Show.GShow Language.SMTLib2.Internals.Type.Type (Language.SMTLib2.Internals.Embed.ValueExt m)
instance Data.GADT.Compare.GEq Language.SMTLib2.Internals.Type.Type (Language.SMTLib2.Internals.Embed.ValueExt m)
instance Data.GADT.Compare.GCompare Language.SMTLib2.Internals.Type.Type (Language.SMTLib2.Internals.Embed.ValueExt m)
instance Language.SMTLib2.Internals.Embed.Embed Data.Functor.Identity.Identity (Language.SMTLib2.Internals.Embed.ValueExt Data.Functor.Identity.Identity)
instance Language.SMTLib2.Internals.Backend.Backend b => Language.SMTLib2.Internals.Embed.Extract (Language.SMTLib2.Internals.Embed.BackendInfo b) (Language.SMTLib2.Internals.Backend.Expr b)
instance (Data.GADT.Compare.GCompare Language.SMTLib2.Internals.Type.Type var, Language.SMTLib2.Internals.Type.GetType var, Data.GADT.Compare.GCompare Language.SMTLib2.Internals.Type.Type qvar, Language.SMTLib2.Internals.Type.GetType qvar, Data.GADT.Compare.GCompare ([Language.SMTLib2.Internals.Type.Type], Language.SMTLib2.Internals.Type.Type) fun, Language.SMTLib2.Internals.Type.GetFunType fun, Data.GADT.Compare.GCompare Language.SMTLib2.Internals.Type.Type farg, Language.SMTLib2.Internals.Type.GetType farg, Data.GADT.Compare.GCompare Language.SMTLib2.Internals.Type.Type lvar, Language.SMTLib2.Internals.Type.GetType lvar) => Language.SMTLib2.Internals.Embed.Embed Data.Functor.Identity.Identity (Language.SMTLib2.Internals.Embed.SMTExpr var qvar fun farg lvar)
instance (Language.SMTLib2.Internals.Type.GetType var, Language.SMTLib2.Internals.Type.GetType qvar, Language.SMTLib2.Internals.Type.GetFunType fun, Language.SMTLib2.Internals.Type.GetType farg, Language.SMTLib2.Internals.Type.GetType lvar) => Language.SMTLib2.Internals.Type.GetType (Language.SMTLib2.Internals.Embed.SMTExpr var qvar fun farg lvar)
instance (Data.GADT.Compare.GCompare Language.SMTLib2.Internals.Type.Type var, Data.GADT.Compare.GCompare Language.SMTLib2.Internals.Type.Type qvar, Data.GADT.Compare.GCompare ([Language.SMTLib2.Internals.Type.Type], Language.SMTLib2.Internals.Type.Type) fun, Data.GADT.Compare.GCompare Language.SMTLib2.Internals.Type.Type farg, Data.GADT.Compare.GCompare Language.SMTLib2.Internals.Type.Type lvar) => Language.SMTLib2.Internals.Embed.Extract () (Language.SMTLib2.Internals.Embed.SMTExpr var qvar fun farg lvar)
instance (Language.SMTLib2.Internals.Embed.Embed m e, GHC.Base.Monad m) => Language.SMTLib2.Internals.Embed.Embed (Control.Monad.Trans.Except.ExceptT err m) e

module Language.SMTLib2.Internals.Interface

-- | All elements of this list must be of the same type
class Same (tps :: [Type])
class Num (Value tp) => IsSMTNumber (tp :: Type)
class HasMonad a where type MatchMonad a (m :: * -> *) :: Constraint type MonadResult a :: * where {
    type family MatchMonad a (m :: * -> *) :: Constraint;
    type family MonadResult a :: *;
}
embedM :: (HasMonad a, Applicative m, MatchMonad a m) => a -> m (MonadResult a)

-- | Matches constant boolean expressions (<a>true</a> or <a>false</a>).

-- | Create a constant, for example an integer:
--   
--   Example:
--   
--   <pre>
--   do
--     x &lt;- declareVar int
--     -- x is greater than 5
--     assert $ x .&gt;. constant (IntValue 5)
--     
--   </pre>
constant :: (Embed m e) => Value tp -> m (e tp)
asConstant :: Expression v qv fun fv lv e tp -> Maybe (Value tp)

-- | Create the boolean expression "true".
true :: Embed m e => m (e BoolType)

-- | Create the boolean expression "false".
false :: Embed m e => m (e BoolType)

-- | Create a boolean constant expression.
cbool :: Embed m e => Bool -> m (e BoolType)

-- | Create an integer constant expression.
cint :: Embed m e => Integer -> m (e IntType)

-- | Create a real constant expression.
--   
--   Example:
--   
--   <pre>
--   import Data.Ratio
--   
--   x = creal (5 % 4)
--     
--   </pre>
creal :: Embed m e => Rational -> m (e RealType)

-- | Create a constant bitvector expression.
cbv :: Embed m e => Integer -> BitWidth bw -> m (e (BitVecType bw))

-- | Create an untyped constant bitvector expression.
cbvUntyped :: (Embed m e, Monad m) => Integer -> Integer -> (forall bw. e (BitVecType bw) -> m b) -> m b
cdt :: (Embed m e, IsDatatype t, Length par ~ Parameters t) => t par Value -> m (e (DataType t par))
exists :: (Embed m e, Monad m) => List Repr tps -> (forall m e. (Embed m e, Monad m) => List e tps -> m (e BoolType)) -> m (e BoolType)
forall :: (Embed m e, Monad m) => List Repr tps -> (forall m e. (Embed m e, Monad m) => List e tps -> m (e BoolType)) -> m (e BoolType)

-- | Create an expression by applying a function to a list of arguments.
app :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ List e args) => Function (EmFun m e) '(args, res) -> a -> m (e res)
fun :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ List e args) => EmFun m e '(args, res) -> a -> m (e res)
eq :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp) => [a] -> m (e BoolType)

-- | Create a boolean expression that encodes that two expressions have the
--   same value.
--   
--   Example:
--   
--   <pre>
--   is5 :: <a>Backend</a> b =&gt; <a>Expr</a> b <a>IntType</a> -&gt; <a>SMT</a> b <a>BoolType</a>
--   is5 e = e <a>.==.</a> <a>cint</a> 5
--     
--   </pre>
(.==.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => a -> b -> m (e BoolType)
infix 4 .==.
distinct :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp) => [a] -> m (e BoolType)
(./=.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => a -> b -> m (e BoolType)
infix 4 ./=.
map' :: (Embed m e, HasMonad arg, MatchMonad arg m, MonadResult arg ~ List e (Lifted tps idx), Unlift tps idx, GetType e, GetFunType (EmFun m e)) => Function (EmFun m e) '(tps, res) -> arg -> m (e (ArrayType idx res))
ord :: (Embed m e, IsSMTNumber tp, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => OrdOp -> a -> b -> m (e BoolType)
(.>=.) :: (Embed m e, IsSMTNumber tp, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => a -> b -> m (e BoolType)
infix 4 .>=.
(.>.) :: (Embed m e, IsSMTNumber tp, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => a -> b -> m (e BoolType)
infix 4 .>.
(.<=.) :: (Embed m e, IsSMTNumber tp, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => a -> b -> m (e BoolType)
infix 4 .<=.
(.<.) :: (Embed m e, IsSMTNumber tp, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => a -> b -> m (e BoolType)
infix 4 .<.
arith :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => ArithOp -> [a] -> m (e tp)
plus :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => [a] -> m (e tp)
(.+.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp, IsSMTNumber tp) => a -> b -> m (e tp)
infixl 6 .+.
mult :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => [a] -> m (e tp)
(.*.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp, IsSMTNumber tp) => a -> b -> m (e tp)
infixl 7 .*.
minus :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => [a] -> m (e tp)
(.-.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp, IsSMTNumber tp) => a -> b -> m (e tp)
infixl 6 .-.
neg :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => a -> m (e tp)
div' :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e IntType, MonadResult b ~ e IntType) => a -> b -> m (e IntType)
infixl 7 `div'`
mod' :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e IntType, MonadResult b ~ e IntType) => a -> b -> m (e IntType)
infixl 7 `mod'`
rem' :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e IntType, MonadResult b ~ e IntType) => a -> b -> m (e IntType)
infixl 7 `rem'`
(./.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e RealType, MonadResult b ~ e RealType) => a -> b -> m (e RealType)
infixl 7 ./.
abs' :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => a -> m (e tp)
not' :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => a -> m (e BoolType)
logic :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => LogicOp -> [a] -> m (e BoolType)
and' :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => [a] -> m (e BoolType)
(.&.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e BoolType, MonadResult b ~ e BoolType) => a -> b -> m (e BoolType)
infixr 3 .&.
or' :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => [a] -> m (e BoolType)
(.|.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e BoolType, MonadResult b ~ e BoolType) => a -> b -> m (e BoolType)
infixr 2 .|.
xor' :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => [a] -> m (e BoolType)
implies :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => [a] -> m (e BoolType)
(.=>.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e BoolType, MonadResult b ~ e BoolType) => a -> b -> m (e BoolType)
infixr 2 .=>.
toReal :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e IntType) => a -> m (e RealType)
toInt :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e RealType) => a -> m (e IntType)
ite :: (Embed m e, HasMonad a, HasMonad b, HasMonad c, MatchMonad a m, MatchMonad b m, MatchMonad c m, MonadResult a ~ e BoolType, MonadResult b ~ e tp, MonadResult c ~ e tp) => a -> b -> c -> m (e tp)
bvcomp :: forall m e a b bw. (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => BVCompOp -> a -> b -> m (e BoolType)
bvule :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType)
bvult :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType)
bvuge :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType)
bvugt :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType)
bvsle :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType)
bvslt :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType)
bvsge :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType)
bvsgt :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType)
bvbin :: forall m e a b bw. (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => BVBinOp -> a -> b -> m (e (BitVecType bw))
bvadd :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))
bvsub :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))
bvmul :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))
bvurem :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))
bvsrem :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))
bvudiv :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))
bvsdiv :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))
bvshl :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))
bvlshr :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))
bvashr :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))
bvxor :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))
bvand :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))
bvor :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))
bvun :: forall m e a bw. (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e (BitVecType bw)) => BVUnOp -> a -> m (e (BitVecType bw))
bvnot :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e (BitVecType bw)) => a -> m (e (BitVecType bw))
bvneg :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e (BitVecType bw)) => a -> m (e (BitVecType bw))
concat' :: forall m e a b n1 n2. (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType n1), MonadResult b ~ e (BitVecType n2)) => a -> b -> m (e (BitVecType (n1 + n2)))
extract' :: forall m e a bw start len. (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e (BitVecType bw), (start + len) <= bw) => BitWidth start -> BitWidth len -> a -> m (e (BitVecType len))
extractChecked :: forall m e a bw start len. (Embed m e, HasMonad a, MatchMonad a m, KnownNat start, KnownNat len, MonadResult a ~ e (BitVecType bw)) => BitWidth start -> BitWidth len -> a -> m (e (BitVecType len))
extractUntypedStart :: forall m e a bw len. (Embed m e, HasMonad a, MatchMonad a m, KnownNat len, MonadResult a ~ e (BitVecType bw)) => Integer -> BitWidth len -> a -> m (e (BitVecType len))
extractUntyped :: forall m e a bw b. (Embed m e, Monad m, HasMonad a, MatchMonad a m, MonadResult a ~ e (BitVecType bw)) => Integer -> Integer -> a -> (forall len. e (BitVecType len) -> m b) -> m b

-- | Access an array element. The following law holds:
--   
--   <pre>
--   select (store arr i e) i .==. e
--   </pre>
select :: (Embed m e, HasMonad arr, MatchMonad arr m, MonadResult arr ~ e (ArrayType idx el), HasMonad i, MatchMonad i m, MonadResult i ~ List e idx) => arr -> i -> m (e el)

-- | A specialized version of <a>select</a> when the index is just a single
--   element.
select1 :: (Embed m e, HasMonad arr, HasMonad idx, MatchMonad arr m, MatchMonad idx m, MonadResult arr ~ e (ArrayType '[idx'] el), MonadResult idx ~ e idx') => arr -> idx -> m (e el)

-- | Write an element into an array and return the resulting array. The
--   following laws hold (forall i/=j):
--   
--   <pre>
--   select (store arr i e) i .==. e
--   select (store arr i e) j .==. select arr j
--   </pre>
store :: (Embed m e, HasMonad arr, MatchMonad arr m, MonadResult arr ~ e (ArrayType idx el), HasMonad i, MatchMonad i m, MonadResult i ~ List e idx, HasMonad nel, MatchMonad nel m, MonadResult nel ~ e el) => arr -> i -> nel -> m (e (ArrayType idx el))

-- | A specialized version of <a>store</a> when the index is just a single
--   element.
store1 :: (Embed m e, HasMonad arr, HasMonad idx, HasMonad el, MatchMonad arr m, MatchMonad idx m, MatchMonad el m, MonadResult arr ~ e (ArrayType '[idx'] el'), MonadResult idx ~ e idx', MonadResult el ~ e el') => arr -> idx -> el -> m (e (ArrayType '[idx'] el'))

-- | Create an array where every element is the same. The following holds:
--   
--   <pre>
--   select (constArray tp e) i .==. e
--   </pre>
constArray :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp) => List Repr idx -> a -> m (e (ArrayType idx tp))
mk :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ List e (Instantiated sig par), IsDatatype dt, Length par ~ Parameters dt) => Datatype dt -> List Repr par -> Constr dt sig -> a -> m (e (DataType dt par))
is :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e (DataType dt par), IsDatatype dt) => a -> Constr dt sig -> m (e BoolType)
(.#.) :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e (DataType dt par), IsDatatype dt) => a -> Field dt tp -> m (e (CType tp par))
divisible :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e IntType) => Integer -> a -> m (e BoolType)

-- | Create a typed list by appending an element to the front of another
--   list.
(.:.) :: (HasMonad a, MonadResult a ~ e tp, MatchMonad a m, Applicative m) => a -> m (List e tps) -> m (List e (tp : tps))
infixr 5 .:.

-- | Create an empty list.
nil :: Applicative m => m (List e '[])
instance Language.SMTLib2.Internals.Interface.Same ((':) Language.SMTLib2.Internals.Type.Type tp ('[] Language.SMTLib2.Internals.Type.Type))
instance (Language.SMTLib2.Internals.Interface.Same ((':) Language.SMTLib2.Internals.Type.Type tp tps), tp ~ Language.SMTLib2.Internals.Interface.SameType ((':) Language.SMTLib2.Internals.Type.Type tp tps)) => Language.SMTLib2.Internals.Interface.Same ((':) Language.SMTLib2.Internals.Type.Type tp ((':) Language.SMTLib2.Internals.Type.Type tp tps))
instance Language.SMTLib2.Internals.Interface.IsSMTNumber 'Language.SMTLib2.Internals.Type.IntType
instance Language.SMTLib2.Internals.Interface.IsSMTNumber 'Language.SMTLib2.Internals.Type.RealType
instance Language.SMTLib2.Internals.Interface.HasMonad (e tp)
instance Language.SMTLib2.Internals.Interface.HasMonad (m (e tp))
instance Language.SMTLib2.Internals.Interface.HasMonad (Language.SMTLib2.Internals.Type.List.List Language.SMTLib2.Internals.Type.Type e tp)
instance Language.SMTLib2.Internals.Interface.HasMonad (m (Language.SMTLib2.Internals.Type.List.List Language.SMTLib2.Internals.Type.Type e tp))


-- | Example usage: This program tries to find two numbers greater than
--   zero which sum up to 5.
--   
--   <pre>
--   import Language.SMTLib2
--   import Language.SMTLib2.Pipe
--   
--   program :: Backend b =&gt; SMT b (Integer,Integer)
--   program = do
--     x &lt;- declareVar int
--     y &lt;- declareVar int
--     assert $ x .+. y .==. cint 5
--     assert $ x .&gt;. cint 0
--     assert $ y .&gt;. cint 0
--     checkSat
--     IntValue vx &lt;- getValue x
--     IntValue vy &lt;- getValue y
--     return (vx,vy)
--   
--   main = withBackend (createPipe "z3" ["-smt2","-in"]) program &gt;&gt;= print
--        
--   </pre>
module Language.SMTLib2

-- | The SMT monad is used to perform communication with the SMT solver.
--   The type of solver is given by the <i>b</i> parameter.
data SMT b a

-- | A class of <a>Monad</a>s that can be used to form SMTLib expressions.
--   The default instance of this class is the <a>SMT</a> monad, together
--   with its associated <a>Expr</a> type. An interesting instance is the
--   <a>Identity</a> monad with the <a>Value</a> type, which allows
--   evaluation of SMTLib expressions.
class (Applicative m, GCompare (EmVar m e), GCompare (EmQVar m e), GCompare (EmFun m e), GCompare (EmFunArg m e), GCompare (EmLVar m e)) => Embed m e

-- | A backend represents a specific type of SMT solver.
class (Typeable b, Functor (SMTMonad b), Monad (SMTMonad b), GetType (Expr b), GetType (Var b), GetType (QVar b), GetFunType (Fun b), GetType (FunArg b), GetType (LVar b), Typeable (Expr b), Typeable (Var b), Typeable (QVar b), Typeable (Fun b), Typeable (FunArg b), Typeable (LVar b), Typeable (ClauseId b), GCompare (Expr b), GShow (Expr b), GCompare (Var b), GShow (Var b), GCompare (QVar b), GShow (QVar b), GCompare (Fun b), GShow (Fun b), GCompare (FunArg b), GShow (FunArg b), GCompare (LVar b), GShow (LVar b), Ord (ClauseId b), Show (ClauseId b), Ord (Proof b), Show (Proof b), Show (Model b)) => Backend b where type SMTMonad b :: * -> * data Expr b :: Type -> * type ClauseId b :: * type Model b :: * comment _ b = return ((), b) where {
    type family SMTMonad b :: * -> *;
    data family Expr b :: Type -> *;
    type family ClauseId b :: *;
    type family Model b :: *;
}

-- | Execute an SMT action on a given backend.
withBackend :: Backend b => SMTMonad b b -> SMT b a -> SMTMonad b a

-- | Like <a>withBackend</a> but specialized to the <a>IO</a> monad so
--   exeptions can be handled by gracefully exiting the solver.
withBackendExitCleanly :: (Backend b, SMTMonad b ~ IO) => IO b -> SMT b a -> IO a

-- | Set an option controlling the behaviour of the SMT solver. Many
--   solvers require you to specify what kind of queries you'll ask them
--   after the model is specified.
--   
--   For example, when using interpolation, it is often required to do the
--   following:
--   
--   <pre>
--   do
--     setOption (ProduceInterpolants True)
--     -- Declare model
--     interp &lt;- getInterpolant
--     -- Use interpolant
--     
--   </pre>
setOption :: Backend b => SMTOption -> SMT b ()

-- | Options controling the behaviour of the SMT solver
data SMTOption

-- | Whether or not to print "success" after each operation
PrintSuccess :: Bool -> SMTOption

-- | Produce a satisfying assignment after each successful checkSat
ProduceModels :: Bool -> SMTOption

-- | Produce a proof of unsatisfiability after each failed checkSat
ProduceProofs :: Bool -> SMTOption

-- | Enable the querying of unsatisfiable cores after a failed checkSat
ProduceUnsatCores :: Bool -> SMTOption

-- | Enable the generation of craig interpolants
ProduceInterpolants :: Bool -> SMTOption
SMTLogic :: String -> SMTOption

-- | Query the solver for information about itself.
--   
--   Example:
--   
--   <pre>
--   isZ3Solver :: Backend b =&gt; SMT b Bool
--   isZ3Solver = do
--     name &lt;- getInfo SMTSolverName
--     return $ name=="Z3"
--   </pre>
getInfo :: Backend b => SMTInfo i -> SMT b i

-- | Solver information query type. Used with <a>getInfo</a>.
data SMTInfo i
[SMTSolverName] :: SMTInfo String
[SMTSolverVersion] :: SMTInfo String

-- | Create a fresh variable of a given type.
--   
--   Example:
--   
--   <pre>
--   do
--     -- Declare a single integer variable
--     v &lt;- declareVar int
--     -- Use variable v
--     
--   </pre>
declareVar :: Backend b => Repr t -> SMT b (Expr b t)

-- | Create a fresh variable (like <a>declareVar</a>), but also give it a
--   name. Note that the name is a hint to the SMT solver that it may
--   ignore.
--   
--   Example:
--   
--   <pre>
--   do
--     -- Declare a single boolean variable called "x"
--     x &lt;- declareVarNamed bool "x"
--     -- Use variable x
--     
--   </pre>
declareVarNamed :: Backend b => Repr t -> String -> SMT b (Expr b t)

-- | Create a new variable that is defined by a given expression.
--   
--   Example:
--   
--   <pre>
--   do
--     -- x is an integer
--     x &lt;- declareVar int
--     -- y is defined to be x+5
--     y &lt;- defineVar $ x .+. cint 5
--     -- Use x and y
--     
--   </pre>
defineVar :: (Backend b, HasMonad expr, MatchMonad expr (SMT b), MonadResult expr ~ Expr b t) => expr -> SMT b (Expr b t)

-- | Create a new named variable that is defined by a given expression
--   (like <a>defineVar</a>).
defineVarNamed :: (Backend b, HasMonad expr, MatchMonad expr (SMT b), MonadResult expr ~ Expr b t) => String -> expr -> SMT b (Expr b t)

-- | Create a new uninterpreted function by specifying its signature.
--   
--   Example:
--   
--   <pre>
--   do
--     -- Create a function from (int,bool) to int
--     f &lt;- declareFun (int ::: bool ::: Nil) int
--     -- Use f
--     
--   </pre>
declareFun :: Backend b => List Repr args -> Repr res -> SMT b (Fun b '(args, res))

-- | Create a new uninterpreted function by specifying its signature (like
--   <a>declareFun</a>), but also give it a name.
declareFunNamed :: Backend b => List Repr args -> Repr res -> String -> SMT b (Fun b '(args, res))

-- | Create a new interpreted function with a definition. Given a signature
--   and a (haskell) function from the arguments to the resulting
--   expression.
--   
--   Example:
--   
--   <pre>
--   do
--     -- Create a function from (int,int) to int that calculates the maximum
--     max &lt;- defineFun (int ::: int ::: Nil) $
--              (x ::: y ::: Nil) -&gt; ite (x .&gt;. y) x y
--     -- Use max function
--     
--   </pre>
defineFun :: (Backend b, HasMonad def, MatchMonad def (SMT b), MonadResult def ~ Expr b res) => List Repr args -> (List (Expr b) args -> def) -> SMT b (Fun b '(args, res))

-- | Create a new interpreted function with a definition (like
--   <a>defineFun</a>) but also give it a name.
defineFunNamed :: (Backend b, HasMonad def, MatchMonad def (SMT b), MonadResult def ~ Expr b res) => String -> List Repr args -> (List (Expr b) args -> def) -> SMT b (Fun b '(args, res))

-- | Create a constant, for example an integer:
--   
--   Example:
--   
--   <pre>
--   do
--     x &lt;- declareVar int
--     -- x is greater than 5
--     assert $ x .&gt;. constant (IntValue 5)
--     
--   </pre>
constant :: (Embed m e) => Value tp -> m (e tp)

-- | Values that can be used as constants in expressions.
data Value (a :: Type)
[BoolValue] :: Bool -> Value BoolType
[IntValue] :: Integer -> Value IntType
[RealValue] :: Rational -> Value RealType
[BitVecValue] :: Integer -> BitWidth bw -> Value (BitVecType bw)
[DataValue] :: (IsDatatype dt, Length par ~ Parameters dt) => dt par Value -> Value (DataType dt par)

-- | Matches constant boolean expressions (<a>true</a> or <a>false</a>).

-- | Create a boolean constant expression.
cbool :: Embed m e => Bool -> m (e BoolType)

-- | Create the boolean expression "true".
true :: Embed m e => m (e BoolType)

-- | Create the boolean expression "false".
false :: Embed m e => m (e BoolType)

-- | Create an integer constant expression.
cint :: Embed m e => Integer -> m (e IntType)

-- | Create a real constant expression.
--   
--   Example:
--   
--   <pre>
--   import Data.Ratio
--   
--   x = creal (5 % 4)
--     
--   </pre>
creal :: Embed m e => Rational -> m (e RealType)
data BitWidth (bw :: Nat)
bw :: KnownNat bw => Proxy bw -> BitWidth bw

-- | Create a constant bitvector expression.
cbv :: Embed m e => Integer -> BitWidth bw -> m (e (BitVecType bw))

-- | Create an untyped constant bitvector expression.
cbvUntyped :: (Embed m e, Monad m) => Integer -> Integer -> (forall bw. e (BitVecType bw) -> m b) -> m b
cdt :: (Embed m e, IsDatatype t, Length par ~ Parameters t) => t par Value -> m (e (DataType t par))
exists :: (Embed m e, Monad m) => List Repr tps -> (forall m e. (Embed m e, Monad m) => List e tps -> m (e BoolType)) -> m (e BoolType)
forall :: (Embed m e, Monad m) => List Repr tps -> (forall m e. (Embed m e, Monad m) => List e tps -> m (e BoolType)) -> m (e BoolType)

-- | Create an expression by applying a function to a list of arguments.
app :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ List e args) => Function (EmFun m e) '(args, res) -> a -> m (e res)
fun :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ List e args) => EmFun m e '(args, res) -> a -> m (e res)
eq :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp) => [a] -> m (e BoolType)

-- | Create a boolean expression that encodes that two expressions have the
--   same value.
--   
--   Example:
--   
--   <pre>
--   is5 :: <a>Backend</a> b =&gt; <a>Expr</a> b <a>IntType</a> -&gt; <a>SMT</a> b <a>BoolType</a>
--   is5 e = e <a>.==.</a> <a>cint</a> 5
--     
--   </pre>
(.==.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => a -> b -> m (e BoolType)
infix 4 .==.
distinct :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp) => [a] -> m (e BoolType)
(./=.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => a -> b -> m (e BoolType)
infix 4 ./=.
map' :: (Embed m e, HasMonad arg, MatchMonad arg m, MonadResult arg ~ List e (Lifted tps idx), Unlift tps idx, GetType e, GetFunType (EmFun m e)) => Function (EmFun m e) '(tps, res) -> arg -> m (e (ArrayType idx res))
ord :: (Embed m e, IsSMTNumber tp, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => OrdOp -> a -> b -> m (e BoolType)
(.>=.) :: (Embed m e, IsSMTNumber tp, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => a -> b -> m (e BoolType)
infix 4 .>=.
(.>.) :: (Embed m e, IsSMTNumber tp, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => a -> b -> m (e BoolType)
infix 4 .>.
(.<=.) :: (Embed m e, IsSMTNumber tp, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => a -> b -> m (e BoolType)
infix 4 .<=.
(.<.) :: (Embed m e, IsSMTNumber tp, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => a -> b -> m (e BoolType)
infix 4 .<.
arith :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => ArithOp -> [a] -> m (e tp)
plus :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => [a] -> m (e tp)
(.+.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp, IsSMTNumber tp) => a -> b -> m (e tp)
infixl 6 .+.
mult :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => [a] -> m (e tp)
(.*.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp, IsSMTNumber tp) => a -> b -> m (e tp)
infixl 7 .*.
minus :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => [a] -> m (e tp)
(.-.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp, IsSMTNumber tp) => a -> b -> m (e tp)
infixl 6 .-.
neg :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => a -> m (e tp)
div' :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e IntType, MonadResult b ~ e IntType) => a -> b -> m (e IntType)
infixl 7 `div'`
mod' :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e IntType, MonadResult b ~ e IntType) => a -> b -> m (e IntType)
infixl 7 `mod'`
rem' :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e IntType, MonadResult b ~ e IntType) => a -> b -> m (e IntType)
infixl 7 `rem'`
(./.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e RealType, MonadResult b ~ e RealType) => a -> b -> m (e RealType)
infixl 7 ./.
abs' :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => a -> m (e tp)
not' :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => a -> m (e BoolType)
logic :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => LogicOp -> [a] -> m (e BoolType)
and' :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => [a] -> m (e BoolType)
(.&.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e BoolType, MonadResult b ~ e BoolType) => a -> b -> m (e BoolType)
infixr 3 .&.
or' :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => [a] -> m (e BoolType)
(.|.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e BoolType, MonadResult b ~ e BoolType) => a -> b -> m (e BoolType)
infixr 2 .|.
xor' :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => [a] -> m (e BoolType)
implies :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => [a] -> m (e BoolType)
(.=>.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e BoolType, MonadResult b ~ e BoolType) => a -> b -> m (e BoolType)
infixr 2 .=>.
toReal :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e IntType) => a -> m (e RealType)
toInt :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e RealType) => a -> m (e IntType)
ite :: (Embed m e, HasMonad a, HasMonad b, HasMonad c, MatchMonad a m, MatchMonad b m, MatchMonad c m, MonadResult a ~ e BoolType, MonadResult b ~ e tp, MonadResult c ~ e tp) => a -> b -> c -> m (e tp)
bvcomp :: forall m e a b bw. (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => BVCompOp -> a -> b -> m (e BoolType)
bvule :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType)
bvult :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType)
bvuge :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType)
bvugt :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType)
bvsle :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType)
bvslt :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType)
bvsge :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType)
bvsgt :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType)
bvbin :: forall m e a b bw. (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => BVBinOp -> a -> b -> m (e (BitVecType bw))
bvadd :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))
bvsub :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))
bvmul :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))
bvurem :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))
bvsrem :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))
bvudiv :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))
bvsdiv :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))
bvshl :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))
bvlshr :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))
bvashr :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))
bvxor :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))
bvand :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))
bvor :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw))
bvun :: forall m e a bw. (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e (BitVecType bw)) => BVUnOp -> a -> m (e (BitVecType bw))
bvnot :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e (BitVecType bw)) => a -> m (e (BitVecType bw))
bvneg :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e (BitVecType bw)) => a -> m (e (BitVecType bw))
concat' :: forall m e a b n1 n2. (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType n1), MonadResult b ~ e (BitVecType n2)) => a -> b -> m (e (BitVecType (n1 + n2)))
extract' :: forall m e a bw start len. (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e (BitVecType bw), (start + len) <= bw) => BitWidth start -> BitWidth len -> a -> m (e (BitVecType len))
extractChecked :: forall m e a bw start len. (Embed m e, HasMonad a, MatchMonad a m, KnownNat start, KnownNat len, MonadResult a ~ e (BitVecType bw)) => BitWidth start -> BitWidth len -> a -> m (e (BitVecType len))
extractUntypedStart :: forall m e a bw len. (Embed m e, HasMonad a, MatchMonad a m, KnownNat len, MonadResult a ~ e (BitVecType bw)) => Integer -> BitWidth len -> a -> m (e (BitVecType len))
extractUntyped :: forall m e a bw b. (Embed m e, Monad m, HasMonad a, MatchMonad a m, MonadResult a ~ e (BitVecType bw)) => Integer -> Integer -> a -> (forall len. e (BitVecType len) -> m b) -> m b

-- | Access an array element. The following law holds:
--   
--   <pre>
--   select (store arr i e) i .==. e
--   </pre>
select :: (Embed m e, HasMonad arr, MatchMonad arr m, MonadResult arr ~ e (ArrayType idx el), HasMonad i, MatchMonad i m, MonadResult i ~ List e idx) => arr -> i -> m (e el)

-- | A specialized version of <a>select</a> when the index is just a single
--   element.
select1 :: (Embed m e, HasMonad arr, HasMonad idx, MatchMonad arr m, MatchMonad idx m, MonadResult arr ~ e (ArrayType '[idx'] el), MonadResult idx ~ e idx') => arr -> idx -> m (e el)

-- | Write an element into an array and return the resulting array. The
--   following laws hold (forall i/=j):
--   
--   <pre>
--   select (store arr i e) i .==. e
--   select (store arr i e) j .==. select arr j
--   </pre>
store :: (Embed m e, HasMonad arr, MatchMonad arr m, MonadResult arr ~ e (ArrayType idx el), HasMonad i, MatchMonad i m, MonadResult i ~ List e idx, HasMonad nel, MatchMonad nel m, MonadResult nel ~ e el) => arr -> i -> nel -> m (e (ArrayType idx el))

-- | A specialized version of <a>store</a> when the index is just a single
--   element.
store1 :: (Embed m e, HasMonad arr, HasMonad idx, HasMonad el, MatchMonad arr m, MatchMonad idx m, MatchMonad el m, MonadResult arr ~ e (ArrayType '[idx'] el'), MonadResult idx ~ e idx', MonadResult el ~ e el') => arr -> idx -> el -> m (e (ArrayType '[idx'] el'))

-- | Create an array where every element is the same. The following holds:
--   
--   <pre>
--   select (constArray tp e) i .==. e
--   </pre>
constArray :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp) => List Repr idx -> a -> m (e (ArrayType idx tp))
mk :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ List e (Instantiated sig par), IsDatatype dt, Length par ~ Parameters dt) => Datatype dt -> List Repr par -> Constr dt sig -> a -> m (e (DataType dt par))
is :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e (DataType dt par), IsDatatype dt) => a -> Constr dt sig -> m (e BoolType)
(.#.) :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e (DataType dt par), IsDatatype dt) => a -> Field dt tp -> m (e (CType tp par))
divisible :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e IntType) => Integer -> a -> m (e BoolType)

-- | Convert an expression in the SMT solver-specific format into a more
--   general, pattern-matchable format.
--   
--   Example:
--   
--   <pre>
--   isGE :: Backend b =&gt; Expr b tp -&gt; SMT b Bool
--   isGE e = do
--     e' &lt;- getExpr e
--     case e' of
--       _ :&gt;=: _ -&gt; return True
--       _ -&gt; return False
--     
--   </pre>
getExpr :: (Backend b) => Expr b tp -> SMT b (Expression (Var b) (QVar b) (Fun b) (FunArg b) (LVar b) (Expr b) tp)

-- | Asserts a boolean expression to be true. A successive successful
--   <a>checkSat</a> calls mean that the generated model is consistent with
--   the assertion.
assert :: (Backend b, HasMonad expr, MatchMonad expr (SMT b), MonadResult expr ~ Expr b BoolType) => expr -> SMT b ()

-- | Checks if the set of asserted expressions is satisfiable.
checkSat :: Backend b => SMT b CheckSatResult

-- | The same as <a>checkSat</a>, but can specify an optional <a>Tactic</a>
--   that is used to give hints to the SMT solver on how to solve the
--   problem and limits on the amount of time and memory that the solver is
--   allowed to use. If the limits are exhausted, the solver must return
--   <tt>Unknown</tt>.
checkSatWith :: Backend b => Maybe Tactic -> CheckSatLimits -> SMT b CheckSatResult

-- | The result of a check-sat query
data CheckSatResult

-- | The formula is satisfiable
Sat :: CheckSatResult

-- | The formula is unsatisfiable
Unsat :: CheckSatResult

-- | The solver cannot determine the satisfiability of a formula
Unknown :: CheckSatResult

-- | Describe limits on the ressources that an SMT-solver can use
data CheckSatLimits
CheckSatLimits :: Maybe Integer -> Maybe Integer -> CheckSatLimits

-- | A limit on the amount of time the solver can spend on the problem (in
--   milliseconds)
[limitTime] :: CheckSatLimits -> Maybe Integer

-- | A limit on the amount of memory the solver can use (in megabytes)
[limitMemory] :: CheckSatLimits -> Maybe Integer
noLimits :: CheckSatLimits

-- | Works like <a>assert</a>, but additionally allows the user to find the
--   unsatisfiable core of a set of assignments using <a>getUnsatCore</a>.
assertId :: (Backend b, HasMonad expr, MatchMonad expr (SMT b), MonadResult expr ~ Expr b BoolType) => expr -> SMT b (ClauseId b)

-- | After a <a>checkSat</a> query that returned <tt>Unsat</tt>, we can ask
--   the SMT solver for a subset of the assertions that are enough to make
--   the specified problem unsatisfiable. These assertions have to be
--   created using <a>assertId</a>.
--   
--   Example:
--   
--   <pre>
--   do
--     setOption (ProduceUnsatCores True)
--     x &lt;- declareVar int
--     y &lt;- declareVar int
--     cl1 &lt;- assertId $ x .&gt;. y
--     cl2 &lt;- assertId $ x .&gt;. cint 5
--     cl3 &lt;- assertId $ y .&gt;. x
--     checkSat
--     core &lt;- getUnsatCore
--     -- core will contain cl1 and cl3
--   </pre>
getUnsatCore :: Backend b => SMT b [ClauseId b]

-- | When using interpolation, use this function to specify if an assertion
--   is part of the A-partition or the B-partition of the original formula.
assertPartition :: (Backend b, HasMonad expr, MatchMonad expr (SMT b), MonadResult expr ~ Expr b BoolType) => expr -> Partition -> SMT b ()

-- | The interpolation partition
data Partition
PartitionA :: Partition
PartitionB :: Partition

-- | After a <a>checkSat</a> query that returned <tt>Unsat</tt>, we can ask
--   the SMT solver for a formula <i>C</i> such that <i>A</i> (the
--   A-partition) and <i>(not C)</i> is unsatisfiable while <i>B</i> (the
--   B-partition) and <i>C</i> is unsatisfiable. Furthermore, <i>C</i> will
--   only mention variables that occur in both <i>A</i> and <i>B</i>.
--   
--   Example:
--   
--   <pre>
--   do
--     setOption (ProduceInterpolants True)
--     p &lt;- declareVar bool
--     q &lt;- declareVar bool
--     r &lt;- declareVar bool
--     t &lt;- declareVar bool
--     assertPartition ((not' (p .&amp;. q)) .=&gt;. ((not' r) .&amp;. q)) PartitionA
--     assertPartition t PartitionB
--     assertPartition r PartitionB
--     assertPartition (not' p) PartitionB
--     checkSat
--     getInterpolant
--     
--   </pre>
getInterpolant :: Backend b => SMT b (Expr b BoolType)

-- | After a <a>checkSat</a> query that returned <tt>Unsat</tt>, we can ask
--   the solver for a proof that the given instance is indeed
--   unsatisfiable.
getProof :: Backend b => SMT b (Proof b)

-- | Convert the solver-specific proof encoding into a more general,
--   pattern-matchable format.
analyzeProof :: Backend b => Proof b -> SMT b (Proof String (Expr b) (Proof b))

-- | Push a fresh frame on the solver stack. All variable definitions and
--   assertions made in a frame are forgotten when it is <a>pop</a>'ed.
push :: Backend b => SMT b ()

-- | Pop a frame from the solver stack.
pop :: Backend b => SMT b ()

-- | Perform an SMT action by executing it in a fresh stack frame. The
--   frame is <a>pop</a>'ed once the action has been performed.
stack :: Backend b => SMT b a -> SMT b a

-- | After a successful <a>checkSat</a> query, query the concrete value for
--   a given expression that the SMT solver assigned to it.
getValue :: (Backend b, HasMonad expr, MatchMonad expr (SMT b), MonadResult expr ~ Expr b t) => expr -> SMT b (Value t)

-- | After a successful <a>checkSat</a> query, return a satisfying
--   assignment that makes all asserted formula true.
getModel :: Backend b => SMT b (Model b)

-- | Evaluate an expression in a model, yielding a concrete value.
modelEvaluate :: (Backend b, HasMonad expr, MatchMonad expr (SMT b), MonadResult expr ~ Expr b t) => Model b -> expr -> SMT b (Value t)
registerDatatype :: (Backend b, IsDatatype dt) => Datatype dt -> SMT b ()

-- | Describes the kind of all SMT types. It is only used in promoted form,
--   for a concrete representation see <a>Repr</a>.
data Type
BoolType :: Type
IntType :: Type
RealType :: Type
BitVecType :: Nat -> Type
ArrayType :: [Type] -> Type -> Type
DataType :: a -> [Type] -> Type
ParameterType :: Nat -> Type

-- | A concrete representation of an SMT type. For aesthetic reasons, it's
--   recommended to use the functions <a>bool</a>, <a>int</a>, <a>real</a>,
--   <a>bitvec</a> or <a>array</a>.
data Repr (t :: Type)
[BoolRepr] :: Repr BoolType
[IntRepr] :: Repr IntType
[RealRepr] :: Repr RealType
[BitVecRepr] :: BitWidth bw -> Repr (BitVecType bw)
[ArrayRepr] :: List Repr idx -> Repr val -> Repr (ArrayType idx val)
[DataRepr] :: (IsDatatype dt, Length par ~ Parameters dt) => Datatype dt -> List Repr par -> Repr (DataType dt par)
[ParameterRepr] :: Natural p -> Repr (ParameterType p)
class GetType v
getType :: GetType v => v tp -> Repr tp

-- | A representation of the SMT Bool type. Holds the values <a>true</a> or
--   <a>false</a>. Constants can be created using <a>cbool</a>.
bool :: Repr BoolType

-- | A representation of the SMT Int type. Holds the unbounded positive and
--   negative integers. Constants can be created using <a>cint</a>.
int :: Repr IntType

-- | A representation of the SMT Real type. Holds positive and negative
--   reals x/y where x and y are integers. Constants can be created using
--   <a>creal</a>.
real :: Repr RealType

-- | A typed representation of the SMT BitVec type. Holds bitvectors (a
--   vector of booleans) of a certain bitwidth. Constants can be created
--   using <a>cbv</a>.
bitvec :: BitWidth bw -> Repr (BitVecType bw)

-- | A representation of the SMT Array type. Has a list of index types and
--   an element type. Stores one value of the element type for each
--   combination of the index types. Constants can be created using
--   <a>constArray</a>.
array :: List Repr idx -> Repr el -> Repr (ArrayType idx el)

-- | A representation of a user-defined datatype without parameters.
dt :: (IsDatatype dt, Parameters dt ~ Z) => Datatype dt -> Repr (DataType dt '[])

-- | A representation of a user-defined datatype with parameters.
dt' :: (IsDatatype dt, Length par ~ Parameters dt) => Datatype dt -> List Repr par -> Repr (DataType dt par)

-- | Natural numbers on the type-level.
data Nat
Z :: Nat
S :: Nat -> Nat

-- | A concrete representation of the <a>Nat</a> type.
data Natural (n :: Nat)
[Zero] :: Natural Z
[Succ] :: Natural n -> Natural (S n)
nat :: (Num a, Ord a) => a -> ExpQ

-- | A template haskell function to create nicer looking number types.
--   
--   Example:
--   
--   <pre>
--   &gt;&gt;&gt; $(nat 5) :: Natural $(natT 5)
--   5
--   </pre>
natT :: (Num a, Ord a) => a -> TypeQ

-- | Get a static representation for a dynamically created natural number.
--   
--   Example:
--   
--   <pre>
--   &gt;&gt;&gt; reifyNat (S (S Z)) show
--   "2"
--   </pre>
reifyNat :: Nat -> (forall n. Natural n -> r) -> r

-- | Strongly typed heterogenous lists.
--   
--   A <i>List e '[tp1,tp2,tp3]</i> contains 3 elements of types <i>e
--   tp1</i>, <i>e tp2</i> and <i>e tp3</i> respectively.
--   
--   As an example, the following list contains two types:
--   
--   <pre>
--   &gt;&gt;&gt; int ::: bool ::: Nil :: List Repr '[IntType,BoolType]
--   [IntRepr,BoolRepr]
--   </pre>
data List e (tp :: [a])
[Nil] :: List e '[]
[:::] :: e x -> List e xs -> List e (x : xs)

-- | Get a static representation of a dynamic list.
--   
--   For example, to convert a list of strings into a list of types:
--   
--   <pre>
--   &gt;&gt;&gt; reifyList (\name f -&gt; case name of { "int" -&gt; f int ; "bool" -&gt; f bool }) ["bool","int"] show
--   "[BoolRepr,IntRepr]"
--   </pre>
reifyList :: (forall r'. a -> (forall tp. e tp -> r') -> r') -> [a] -> (forall tp. List e tp -> r) -> r

-- | Create a typed list by appending an element to the front of another
--   list.
(.:.) :: (HasMonad a, MonadResult a ~ e tp, MatchMonad a m, Applicative m) => a -> m (List e tps) -> m (List e (tp : tps))
infixr 5 .:.

-- | Create an empty list.
nil :: Applicative m => m (List e '[])

-- | Inject a comment into the SMT command stream. Only useful when using
--   the <i>smtlib2-debug</i> package to inspect the command stream.
comment :: (Backend b) => String -> SMT b ()

-- | Use the SMT solver to simplify a given expression.
simplify :: Backend b => Expr b tp -> SMT b (Expr b tp)

module Language.SMTLib2.Internals.Proof.Verify
verifyZ3Proof :: Backend b => Proof b -> SMT b ()
verifyZ3Rule :: (GetType e, Extract i e, GEq e, Monad m, GShow e) => i -> String -> [ProofResult e] -> ProofResult e -> ExceptT String m ()