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


-- | A monad for interfacing with external SMT solvers
--   
--   Hasmtlib is a library for generating SMTLib2-problems using a monad.
--   It takes care of encoding your problem, marshaling the data to an
--   external solver and parsing and interpreting the result into Haskell
--   types. It is highly inspired by ekmett/ersatz which does the same for
--   QSAT. Communication with external solvers is handled by
--   tweag/smtlib-backends.
@package hasmtlib
@version 2.5.1

module Language.Hasmtlib.Boolean
class Boolean b

-- | Lift a <a>Bool</a>.
bool :: Boolean b => Bool -> b

-- | The true constant. <tt><a>true</a> = <a>bool</a> <a>True</a></tt>
true :: Boolean b => b

-- | The false constant. <tt><a>false</a> = <a>bool</a> <a>False</a></tt>
false :: Boolean b => b

-- | Logical conjunction.
(&&) :: Boolean b => b -> b -> b

-- | Logical disjunction (inclusive or).
(||) :: Boolean b => b -> b -> b

-- | Logical implication.
(==>) :: Boolean b => b -> b -> b

-- | Logical implication with arrow reversed.
--   
--   <pre>
--   forall x y. (x ==&gt; y) === (y &lt;== x)
--   </pre>
(<==) :: Boolean b => b -> b -> b

-- | Logical equivalence.
(<==>) :: Boolean b => b -> b -> b

-- | Logical negation.
not :: Boolean b => b -> b

-- | Exclusive-or.
xor :: Boolean b => b -> b -> b
infixr 3 &&
infixr 2 ||
infixr 0 ==>
infixl 0 <==
infixr 4 <==>
infix 4 `xor`

-- | The logical conjunction of several values.
and :: (Foldable t, Boolean b) => t b -> b

-- | The logical disjunction of several values.
or :: (Foldable t, Boolean b) => t b -> b

-- | The negated logical conjunction of several values.
--   
--   <pre>
--   <a>nand</a> = <a>not</a> . <a>and</a>
--   </pre>
nand :: (Foldable t, Boolean b) => t b -> b

-- | The negated logical disjunction of several values.
--   
--   <pre>
--   <a>nor</a> = <a>not</a> . <a>or</a>
--   </pre>
nor :: (Foldable t, Boolean b) => t b -> b

-- | The logical conjunction of the mapping of a function over several
--   values.
all :: (Foldable t, Boolean b) => (a -> b) -> t a -> b

-- | The logical disjunction of the mapping of a function over several
--   values.
any :: (Foldable t, Boolean b) => (a -> b) -> t a -> b
instance Language.Hasmtlib.Boolean.Boolean GHC.Types.Bool
instance Language.Hasmtlib.Boolean.Boolean Data.Bit.Internal.Bit
instance GHC.TypeNats.KnownNat n => Language.Hasmtlib.Boolean.Boolean (Data.Vector.Unboxed.Sized.Vector n Data.Bit.Internal.Bit)

module Language.Hasmtlib.Internal.Constraint

-- | AllC ensures that a list of constraints is applied to a poly-kinded
--   <a>Type</a> k
--   
--   <pre>
--   AllC '[]       k = ()
--   AllC (c ': cs) k = (c k, AllC cs k)
--   </pre>
type family AllC cs k :: Constraint

module Language.Hasmtlib.Internal.Render

-- | Render values to their SMTLib2-Lisp form, represented as
--   <a>Builder</a>.
class Render a
render :: Render a => a -> Builder
renderUnary :: Render a => Builder -> a -> Builder
renderBinary :: (Render a, Render b) => Builder -> a -> b -> Builder
renderTernary :: (Render a, Render b, Render c) => Builder -> a -> b -> c -> Builder
renderNary :: Render a => Builder -> [a] -> Builder

-- | Render values to their sequential SMTLib2-Lisp form, represented as a
--   <a>Seq</a> <a>Builder</a>.
class RenderSeq a
renderSeq :: RenderSeq a => a -> Seq Builder
instance Language.Hasmtlib.Internal.Render.Render GHC.Types.Bool
instance Language.Hasmtlib.Internal.Render.Render GHC.TypeNats.Nat
instance Language.Hasmtlib.Internal.Render.Render GHC.Num.Integer.Integer
instance Language.Hasmtlib.Internal.Render.Render GHC.Types.Double
instance Language.Hasmtlib.Internal.Render.Render GHC.Types.Char
instance Language.Hasmtlib.Internal.Render.Render GHC.Base.String
instance Language.Hasmtlib.Internal.Render.Render Data.ByteString.Builder.Internal.Builder
instance Language.Hasmtlib.Internal.Render.Render Data.Text.Internal.Text

module Language.Hasmtlib.Internal.Bitvec

-- | Unsigned and length-indexed bitvector with MSB first.
newtype Bitvec (n :: Nat)
Bitvec :: Vector n Bit -> Bitvec (n :: Nat)
[unBitvec] :: Bitvec (n :: Nat) -> Vector n Bit
bvReverse :: Bitvec n -> Bitvec n
bvReplicate :: forall n. KnownNat n => Bit -> Bitvec n
bvReplicate' :: forall n proxy. KnownNat n => proxy n -> Bit -> Bitvec n
bvGenerate :: forall n. KnownNat n => (Finite n -> Bit) -> Bitvec n
bvConcat :: Bitvec n -> Bitvec m -> Bitvec (n + m)
bvTake' :: forall n m proxy. KnownNat n => proxy n -> Bitvec (n + m) -> Bitvec n
bvDrop' :: forall n m proxy. KnownNat n => proxy n -> Bitvec (n + m) -> Bitvec m
bvSplitAt' :: forall n m proxy. KnownNat n => proxy n -> Bitvec (n + m) -> (Bitvec n, Bitvec m)
bvToList :: Bitvec n -> [Bit]
bvFromListN :: forall n. KnownNat n => [Bit] -> Maybe (Bitvec n)
bvFromListN' :: forall n. KnownNat n => Proxy n -> [Bit] -> Maybe (Bitvec n)
bvShL :: KnownNat n => Bitvec n -> Bitvec n -> Maybe (Bitvec n)
bvLShR :: KnownNat n => Bitvec n -> Bitvec n -> Maybe (Bitvec n)
bvZeroExtend :: KnownNat i => Proxy i -> Bitvec n -> Bitvec (n + i)
bvExtract :: forall n i j. (KnownNat i, KnownNat ((j - i) + 1), (i + (n - i)) ~ n, (((j - i) + 1) + ((n - i) - ((j - i) + 1))) ~ (n - i)) => Proxy i -> Proxy j -> Bitvec n -> Bitvec ((j - i) + 1)
instance GHC.TypeNats.KnownNat n => Language.Hasmtlib.Boolean.Boolean (Language.Hasmtlib.Internal.Bitvec.Bitvec n)
instance GHC.Classes.Ord (Language.Hasmtlib.Internal.Bitvec.Bitvec n)
instance GHC.Classes.Eq (Language.Hasmtlib.Internal.Bitvec.Bitvec n)
instance GHC.TypeNats.KnownNat n => GHC.Bits.Bits (Language.Hasmtlib.Internal.Bitvec.Bitvec n)
instance GHC.Show.Show (Language.Hasmtlib.Internal.Bitvec.Bitvec n)
instance Language.Hasmtlib.Internal.Render.Render (Language.Hasmtlib.Internal.Bitvec.Bitvec n)
instance GHC.TypeNats.KnownNat n => GHC.Num.Num (Language.Hasmtlib.Internal.Bitvec.Bitvec n)
instance GHC.TypeNats.KnownNat n => GHC.Enum.Bounded (Language.Hasmtlib.Internal.Bitvec.Bitvec n)
instance GHC.TypeNats.KnownNat n => GHC.Enum.Enum (Language.Hasmtlib.Internal.Bitvec.Bitvec n)
instance GHC.TypeNats.KnownNat n => GHC.Real.Real (Language.Hasmtlib.Internal.Bitvec.Bitvec n)
instance GHC.TypeNats.KnownNat n => GHC.Real.Integral (Language.Hasmtlib.Internal.Bitvec.Bitvec n)

module Language.Hasmtlib.Internal.Uniplate1
class Uniplate1 f cs | f -> cs
uniplate1 :: (Uniplate1 f cs, Applicative m, AllC cs b) => (forall a. AllC cs a => f a -> m (f a)) -> f b -> m (f b)
transformM1 :: (Monad m, Uniplate1 f cs, AllC cs b) => (forall a. AllC cs a => f a -> m (f a)) -> f b -> m (f b)
lazyParaM1 :: (Monad m, Uniplate1 f cs, AllC cs b) => (forall a. AllC cs a => f a -> m (f a) -> m (f a)) -> f b -> m (f b)

module Language.Hasmtlib.Solver.Bitwuzla

-- | A <a>Config</a> for Bitwuzla. Requires binary <tt>bitwuzla</tt> to be
--   in path.
--   
--   As of v0.5 Bitwuzla uses Cadical as SAT-Solver by default. Make sure
--   it's default SAT-Solver binary - probably <tt>cadical</tt> - is in
--   path too.
bitwuzla :: Config

module Language.Hasmtlib.Solver.CVC5

-- | A <a>Config</a> for CVC5. Requires binary <tt>cvc5</tt> to be in path.
cvc5 :: Config

module Language.Hasmtlib.Solver.MathSAT

-- | A <a>Config</a> for MathSAT. Requires binary <tt>mathsat</tt> to be in
--   path.
mathsat :: Config

-- | A <a>Config</a> for OptiMathSAT. Requires binary <tt>optimathsat</tt>
--   to be in path.
optimathsat :: Config

module Language.Hasmtlib.Solver.OpenSMT

-- | A <a>Config</a> for OpenSMT. Requires binary <tt>opensmt</tt> to be in
--   path.
opensmt :: Config

module Language.Hasmtlib.Solver.Yices

-- | A <a>Config</a> for Yices. Requires binary <tt>yices-smt2</tt> to be
--   in path.
yices :: Config

module Language.Hasmtlib.Solver.Z3

-- | A <a>Config</a> for Z3. Requires binary <tt>z3</tt> to be in path.
z3 :: Config

module Language.Hasmtlib.Type.ArrayMap

-- | Class that allows access to a map-like array where any value is either
--   the default value or an overwritten values. Every index has a value by
--   default. Values at indices can be overwritten manually.
--   
--   Based on McCarthy`s basic array theory.
--   
--   Therefore the following axioms must hold:
--   
--   <ol>
--   <li>forall A i x: arrSelect (store A i x) == x</li>
--   <li>forall A i j x: i /= j ==&gt; (arrSelect (arrStore A i x) j ===
--   arrSelect A j)</li>
--   </ol>
class ArrayMap f k v
asConst' :: ArrayMap f k v => Proxy f -> Proxy k -> v -> f k v
viewConst :: ArrayMap f k v => f k v -> v
arrSelect :: ArrayMap f k v => f k v -> k -> v
arrStore :: ArrayMap f k v => f k v -> k -> v -> f k v

-- | Wrapper for <a>asConst'</a> which hides the <a>Proxy</a>
asConst :: forall f k v. ArrayMap f k v => v -> f k v

-- | A map-like array with a default constant value and partially
--   overwritten values.
data ConstArray k v
ConstArray :: v -> Map k v -> ConstArray k v
[_arrConst] :: ConstArray k v -> v
[_stored] :: ConstArray k v -> Map k v
stored :: forall k_aj8g v_aj8h k_akAD. Lens (ConstArray k_aj8g v_aj8h) (ConstArray k_akAD v_aj8h) (Map k_aj8g v_aj8h) (Map k_akAD v_aj8h)
arrConst :: forall k_aj8g v_aj8h. Lens' (ConstArray k_aj8g v_aj8h) v_aj8h
instance GHC.Classes.Ord k => Language.Hasmtlib.Type.ArrayMap.ArrayMap Language.Hasmtlib.Type.ArrayMap.ConstArray k v
instance Data.Traversable.Traversable (Language.Hasmtlib.Type.ArrayMap.ConstArray k)
instance Data.Foldable.Foldable (Language.Hasmtlib.Type.ArrayMap.ConstArray k)
instance GHC.Base.Functor (Language.Hasmtlib.Type.ArrayMap.ConstArray k)
instance (GHC.Classes.Ord v, GHC.Classes.Ord k) => GHC.Classes.Ord (Language.Hasmtlib.Type.ArrayMap.ConstArray k v)
instance (GHC.Classes.Eq v, GHC.Classes.Eq k) => GHC.Classes.Eq (Language.Hasmtlib.Type.ArrayMap.ConstArray k v)
instance (GHC.Show.Show v, GHC.Show.Show k) => GHC.Show.Show (Language.Hasmtlib.Type.ArrayMap.ConstArray k v)

module Language.Hasmtlib.Type.Option

-- | Options for SMT-Solvers.
data SMTOption

-- | Print "success" after each operation
PrintSuccess :: Bool -> SMTOption

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

-- | Incremental solving
Incremental :: Bool -> SMTOption

-- | Custom options. First String is the option, second its value.
Custom :: String -> String -> SMTOption
instance Data.Data.Data Language.Hasmtlib.Type.Option.SMTOption
instance GHC.Classes.Ord Language.Hasmtlib.Type.Option.SMTOption
instance GHC.Classes.Eq Language.Hasmtlib.Type.Option.SMTOption
instance GHC.Show.Show Language.Hasmtlib.Type.Option.SMTOption
instance Language.Hasmtlib.Internal.Render.Render Language.Hasmtlib.Type.Option.SMTOption

module Language.Hasmtlib.Type.SMTSort

-- | Sorts in SMTLib2 - used as promoted type (data-kind).
data SMTSort

-- | Sort of Bool
BoolSort :: SMTSort

-- | Sort of Int
IntSort :: SMTSort

-- | Sort of Real
RealSort :: SMTSort

-- | Sort of BitVec with length n
BvSort :: Nat -> SMTSort

-- | Sort of Array with indices k and values v
ArraySort :: SMTSort -> SMTSort -> SMTSort

-- | Sort of String
StringSort :: SMTSort

-- | Injective type-family that computes the Haskell <a>Type</a> of an
--   <a>SMTSort</a>.
type family HaskellType (t :: SMTSort) = (r :: Type) | r -> t

-- | Singleton for <a>SMTSort</a>.
data SSMTSort (t :: SMTSort)
[SIntSort] :: SSMTSort IntSort
[SRealSort] :: SSMTSort RealSort
[SBoolSort] :: SSMTSort BoolSort
[SBvSort] :: KnownNat n => Proxy n -> SSMTSort (BvSort n)
[SArraySort] :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k), Ord (HaskellType v)) => Proxy k -> Proxy v -> SSMTSort (ArraySort k v)
[SStringSort] :: SSMTSort StringSort

-- | Compute singleton <a>SSMTSort</a> from it's promoted type
--   <a>SMTSort</a>.
class KnownSMTSort (t :: SMTSort)
sortSing :: KnownSMTSort t => SSMTSort t

-- | Wrapper for <a>sortSing</a> which takes a <a>Proxy</a>
sortSing' :: forall prxy t. KnownSMTSort t => prxy t -> SSMTSort t

-- | An existential wrapper that hides some <a>SMTSort</a> and a list of
--   <a>Constraint</a>s holding for it.
data SomeSMTSort cs f
[SomeSMTSort] :: forall cs f (t :: SMTSort). AllC cs t => f t -> SomeSMTSort cs f

-- | An existential wrapper that hides some known <a>SMTSort</a>.
type SomeKnownSMTSort f = SomeSMTSort '[KnownSMTSort] f
instance GHC.Show.Show (Language.Hasmtlib.Type.SMTSort.SSMTSort t)
instance GHC.Classes.Eq (Language.Hasmtlib.Type.SMTSort.SSMTSort t)
instance GHC.Classes.Ord (Language.Hasmtlib.Type.SMTSort.SSMTSort t)
instance (forall (t :: Language.Hasmtlib.Type.SMTSort.SMTSort). GHC.Show.Show (f t)) => GHC.Show.Show (Language.Hasmtlib.Type.SMTSort.SomeSMTSort cs f)
instance Data.GADT.Internal.GEq Language.Hasmtlib.Type.SMTSort.SSMTSort
instance Data.GADT.Internal.GCompare Language.Hasmtlib.Type.SMTSort.SSMTSort
instance Language.Hasmtlib.Type.SMTSort.KnownSMTSort 'Language.Hasmtlib.Type.SMTSort.IntSort
instance Language.Hasmtlib.Type.SMTSort.KnownSMTSort 'Language.Hasmtlib.Type.SMTSort.RealSort
instance Language.Hasmtlib.Type.SMTSort.KnownSMTSort 'Language.Hasmtlib.Type.SMTSort.BoolSort
instance GHC.TypeNats.KnownNat n => Language.Hasmtlib.Type.SMTSort.KnownSMTSort ('Language.Hasmtlib.Type.SMTSort.BvSort n)
instance (Language.Hasmtlib.Type.SMTSort.KnownSMTSort k, Language.Hasmtlib.Type.SMTSort.KnownSMTSort v, GHC.Classes.Ord (Language.Hasmtlib.Type.SMTSort.HaskellType k), GHC.Classes.Ord (Language.Hasmtlib.Type.SMTSort.HaskellType v)) => Language.Hasmtlib.Type.SMTSort.KnownSMTSort ('Language.Hasmtlib.Type.SMTSort.ArraySort k v)
instance Language.Hasmtlib.Type.SMTSort.KnownSMTSort 'Language.Hasmtlib.Type.SMTSort.StringSort
instance Language.Hasmtlib.Internal.Render.Render (Language.Hasmtlib.Type.SMTSort.SSMTSort t)

module Language.Hasmtlib.Type.Value

-- | A wrapper for values of <a>SMTSort</a>s. This wraps a Haskell-value
--   into the SMT-Context.
data Value (t :: SMTSort)
[IntValue] :: HaskellType IntSort -> Value IntSort
[RealValue] :: HaskellType RealSort -> Value RealSort
[BoolValue] :: HaskellType BoolSort -> Value BoolSort
[BvValue] :: KnownNat n => HaskellType (BvSort n) -> Value (BvSort n)
[ArrayValue] :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k), Ord (HaskellType v)) => HaskellType (ArraySort k v) -> Value (ArraySort k v)
[StringValue] :: HaskellType StringSort -> Value StringSort

-- | Wraps a Haskell-value into the SMT-Context-<a>Value</a>.
wrapValue :: forall t. KnownSMTSort t => HaskellType t -> Value t

-- | Unwraps a Haskell-value from the SMT-Context-<a>Value</a>.
unwrapValue :: Value t -> HaskellType t
instance GHC.Classes.Eq (Language.Hasmtlib.Type.SMTSort.HaskellType t) => GHC.Classes.Eq (Language.Hasmtlib.Type.Value.Value t)
instance GHC.Classes.Ord (Language.Hasmtlib.Type.SMTSort.HaskellType t) => GHC.Classes.Ord (Language.Hasmtlib.Type.Value.Value t)
instance Data.GADT.Internal.GEq Language.Hasmtlib.Type.Value.Value
instance Data.GADT.Internal.GCompare Language.Hasmtlib.Type.Value.Value

module Language.Hasmtlib.Type.Expr

-- | An internal SMT variable with a phantom-type which holds an <a>Int</a>
--   as it's identifier.
newtype SMTVar (t :: SMTSort)
SMTVar :: Int -> SMTVar (t :: SMTSort)
[_varId] :: SMTVar (t :: SMTSort) -> Int
varId :: forall t_au4I t_av0e. Iso (SMTVar t_au4I) (SMTVar t_av0e) Int Int

-- | A wrapper for values of <a>SMTSort</a>s. This wraps a Haskell-value
--   into the SMT-Context.
data Value (t :: SMTSort)
[IntValue] :: HaskellType IntSort -> Value IntSort
[RealValue] :: HaskellType RealSort -> Value RealSort
[BoolValue] :: HaskellType BoolSort -> Value BoolSort
[BvValue] :: KnownNat n => HaskellType (BvSort n) -> Value (BvSort n)
[ArrayValue] :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k), Ord (HaskellType v)) => HaskellType (ArraySort k v) -> Value (ArraySort k v)
[StringValue] :: HaskellType StringSort -> Value StringSort

-- | Unwraps a Haskell-value from the SMT-Context-<a>Value</a>.
unwrapValue :: Value t -> HaskellType t

-- | Wraps a Haskell-value into the SMT-Context-<a>Value</a>.
wrapValue :: forall t. KnownSMTSort t => HaskellType t -> Value t

-- | An SMT-Expression. For building expressions use the corresponding
--   instances: <a>Boolean</a>, <a>Num</a>, <a>Equatable</a>, ...
--   
--   With a lot of criminal energy you may build invalid expressions
--   regarding the SMTLib Version 2.6 - Specification. Therefore it is
--   highly recommended to rely on the instances.
data Expr (t :: SMTSort)
[Var] :: KnownSMTSort t => SMTVar t -> Expr t
[Constant] :: Value t -> Expr t
[Plus] :: Num (HaskellType t) => Expr t -> Expr t -> Expr t
[Minus] :: Num (HaskellType t) => Expr t -> Expr t -> Expr t
[Neg] :: Num (HaskellType t) => Expr t -> Expr t
[Mul] :: Num (HaskellType t) => Expr t -> Expr t -> Expr t
[Abs] :: Num (HaskellType t) => Expr t -> Expr t
[Mod] :: Integral (HaskellType t) => Expr t -> Expr t -> Expr t
[IDiv] :: Integral (HaskellType t) => Expr t -> Expr t -> Expr t
[Div] :: Expr RealSort -> Expr RealSort -> Expr RealSort
[LTH] :: (Ord (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort
[LTHE] :: (Ord (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort
[EQU] :: (Eq (HaskellType t), KnownSMTSort t, KnownNat n) => Vector (n + 2) (Expr t) -> Expr BoolSort
[Distinct] :: (Eq (HaskellType t), KnownSMTSort t, KnownNat n) => Vector (n + 2) (Expr t) -> Expr BoolSort
[GTHE] :: (Ord (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort
[GTH] :: (Ord (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort
[Not] :: Boolean (HaskellType t) => Expr t -> Expr t
[And] :: Boolean (HaskellType t) => Expr t -> Expr t -> Expr t
[Or] :: Boolean (HaskellType t) => Expr t -> Expr t -> Expr t
[Impl] :: Boolean (HaskellType t) => Expr t -> Expr t -> Expr t
[Xor] :: Boolean (HaskellType t) => Expr t -> Expr t -> Expr t
[Pi] :: Expr RealSort
[Sqrt] :: Expr RealSort -> Expr RealSort
[Exp] :: Expr RealSort -> Expr RealSort
[Sin] :: Expr RealSort -> Expr RealSort
[Cos] :: Expr RealSort -> Expr RealSort
[Tan] :: Expr RealSort -> Expr RealSort
[Asin] :: Expr RealSort -> Expr RealSort
[Acos] :: Expr RealSort -> Expr RealSort
[Atan] :: Expr RealSort -> Expr RealSort
[ToReal] :: Expr IntSort -> Expr RealSort
[ToInt] :: Expr RealSort -> Expr IntSort
[IsInt] :: Expr RealSort -> Expr BoolSort
[Ite] :: Expr BoolSort -> Expr t -> Expr t -> Expr t
[BvNand] :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
[BvNor] :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
[BvShL] :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
[BvLShR] :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
[BvConcat] :: (KnownNat n, KnownNat m) => Expr (BvSort n) -> Expr (BvSort m) -> Expr (BvSort (n + m))
[BvRotL] :: (KnownNat n, Integral a) => a -> Expr (BvSort n) -> Expr (BvSort n)
[BvRotR] :: (KnownNat n, Integral a) => a -> Expr (BvSort n) -> Expr (BvSort n)
[ArrSelect] :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k), Ord (HaskellType v)) => Expr (ArraySort k v) -> Expr k -> Expr v
[ArrStore] :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Expr (ArraySort k v) -> Expr k -> Expr v -> Expr (ArraySort k v)
[StrConcat] :: Expr StringSort -> Expr StringSort -> Expr StringSort
[StrLength] :: Expr StringSort -> Expr IntSort
[StrLT] :: Expr StringSort -> Expr StringSort -> Expr BoolSort
[StrLTHE] :: Expr StringSort -> Expr StringSort -> Expr BoolSort
[StrAt] :: Expr StringSort -> Expr IntSort -> Expr StringSort
[StrSubstring] :: Expr StringSort -> Expr IntSort -> Expr IntSort -> Expr StringSort
[StrPrefixOf] :: Expr StringSort -> Expr StringSort -> Expr BoolSort
[StrSuffixOf] :: Expr StringSort -> Expr StringSort -> Expr BoolSort
[StrContains] :: Expr StringSort -> Expr StringSort -> Expr BoolSort
[StrIndexOf] :: Expr StringSort -> Expr StringSort -> Expr IntSort -> Expr IntSort
[StrReplace] :: Expr StringSort -> Expr StringSort -> Expr StringSort -> Expr StringSort
[StrReplaceAll] :: Expr StringSort -> Expr StringSort -> Expr StringSort -> Expr StringSort

-- | Just v if quantified var has been created already, Nothing otherwise
[ForAll] :: KnownSMTSort t => Maybe (SMTVar t) -> (Expr t -> Expr BoolSort) -> Expr BoolSort

-- | Just v if quantified var has been created already, Nothing otherwise
[Exists] :: KnownSMTSort t => Maybe (SMTVar t) -> (Expr t -> Expr BoolSort) -> Expr BoolSort
isLeaf :: Expr t -> Bool

-- | If condition (p :: b) then (t :: a) else (f :: a)
--   
--   <pre>
--   &gt;&gt;&gt; ite true "1" "2"
--       "1"
--   
--   &gt;&gt;&gt; ite false 100 42
--       42
--   </pre>
class Iteable b a
ite :: Iteable b a => b -> a -> a -> a
ite :: (Iteable b a, Iteable b c, Applicative f, f c ~ a) => b -> a -> a -> a

-- | Test two as on equality as SMT-Expression.
--   
--   You can derive an instance of this class if your type is
--   <a>Generic</a>.
--   
--   <pre>
--   x &lt;- var @RealType
--   y &lt;- var
--   assert $ y === x &amp;&amp; not (y /== x)
--   </pre>
class Equatable a

-- | Test whether two values are equal in the SMT-Problem.
(===) :: Equatable a => a -> a -> Expr BoolSort

-- | Test whether two values are equal in the SMT-Problem.
(===) :: (Equatable a, Generic a, GEquatable (Rep a)) => a -> a -> Expr BoolSort

-- | Test whether two values are not equal in the SMT-Problem.
(/==) :: Equatable a => a -> a -> Expr BoolSort
infix 4 ===
infix 4 /==

-- | Compare two as as SMT-Expression.
--   
--   You can derive an instance of this class if your type is
--   <a>Generic</a>.
--   
--   <pre>
--   x &lt;- var @RealSort
--   y &lt;- var
--   assert $ x &gt;? y
--   assert $ x === min' 42 100
--   </pre>
class Equatable a => Orderable a
(<=?) :: Orderable a => a -> a -> Expr BoolSort
(<=?) :: (Orderable a, Generic a, GOrderable (Rep a)) => a -> a -> Expr BoolSort
(>=?) :: Orderable a => a -> a -> Expr BoolSort
(<?) :: Orderable a => a -> a -> Expr BoolSort
(>?) :: Orderable a => a -> a -> Expr BoolSort
infix 4 <=?
infix 4 >=?
infix 4 <?
infix 4 >?

-- | Minimum of two as SMT-Expression.
min' :: (Orderable a, Iteable (Expr BoolSort) a) => a -> a -> a

-- | Maximum of two as SMT-Expression.
max' :: (Orderable a, Iteable (Expr BoolSort) a) => a -> a -> a

-- | Test multiple expressions on equality within in the
--   <tt>SMT</tt>-Problem.
equal :: (Eq (HaskellType t), KnownSMTSort t, Foldable f) => f (Expr t) -> Expr BoolSort

-- | Test multiple expressions on distinctness within in the
--   <tt>SMT</tt>-Problem.
distinct :: (Eq (HaskellType t), KnownSMTSort t, Foldable f) => f (Expr t) -> Expr BoolSort

-- | A universal quantification for any specific <a>SMTSort</a>. If the
--   type cannot be inferred, apply a type-annotation. Nested quantifiers
--   are also supported.
--   
--   Usage:
--   
--   <pre>
--   assert $
--      for_all @IntSort $ x -&gt;
--         x + 0 === x &amp;&amp; 0 + x === x
--   
--   </pre>
--   
--   The lambdas <tt>x</tt> is all-quantified here. It will only be scoped
--   for the lambdas body.
for_all :: forall t. KnownSMTSort t => (Expr t -> Expr BoolSort) -> Expr BoolSort

-- | An existential quantification for any specific <a>SMTSort</a> If the
--   type cannot be inferred, apply a type-annotation. Nested quantifiers
--   are also supported.
--   
--   Usage:
--   
--   <pre>
--   assert $
--      for_all @(BvSort 8) $ x -&gt;
--          exists $ y -&gt;
--            x - y === 0
--   
--   </pre>
--   
--   The lambdas <tt>y</tt> is existentially quantified here. It will only
--   be scoped for the lambdas body.
exists :: forall t. KnownSMTSort t => (Expr t -> Expr BoolSort) -> Expr BoolSort

-- | Select a value from an array.
select :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k), Ord (HaskellType v)) => Expr (ArraySort k v) -> Expr k -> Expr v

-- | Store a value in an array.
store :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Expr (ArraySort k v) -> Expr k -> Expr v -> Expr (ArraySort k v)

-- | Bitvector shift left
bvShL :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)

-- | Bitvector logical shift right
bvLShR :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)

-- | Concat two bitvectors
bvConcat :: (KnownNat n, KnownNat m) => Expr (BvSort n) -> Expr (BvSort m) -> Expr (BvSort (n + m))

-- | Converts an expression of type <a>IntSort</a> to type <a>RealSort</a>.
toRealSort :: Expr IntSort -> Expr RealSort

-- | Converts an expression of type <a>RealSort</a> to type <a>IntSort</a>.
toIntSort :: Expr RealSort -> Expr IntSort

-- | Checks whether an expression of type <a>RealSort</a> may be safely
--   converted to type <a>IntSort</a>.
isIntSort :: Expr RealSort -> Expr BoolSort

-- | Length of a string.
strLength :: Expr StringSort -> Expr IntSort

-- | Singleton string containing a character at given position or empty
--   string when position is out of range. The leftmost position is 0.
strAt :: Expr StringSort -> Expr IntSort -> Expr StringSort

-- | <tt>(strSubstring s i n)</tt> evaluates to the longest (unscattered)
--   substring of <tt>s</tt> of length at most <tt>n</tt> starting at
--   position <tt>i</tt>. It evaluates to the empty string if <tt>n</tt> is
--   negative or <tt>i</tt> is not in the interval <tt>[0,l-1]</tt> where
--   <tt>l</tt> is the length of <tt>s</tt>.
strSubstring :: Expr StringSort -> Expr IntSort -> Expr IntSort -> Expr StringSort

-- | First string is a prefix of second one. <tt>(str.prefixof s t)</tt> is
--   <tt>true</tt> iff <tt>s</tt> is a prefix of <tt>t</tt>.
strPrefixOf :: Expr StringSort -> Expr StringSort -> Expr BoolSort

-- | First string is a suffix of second one. <tt>(str.suffixof s t)</tt> is
--   <tt>true</tt> iff <tt>s</tt> is a suffix of <tt>t</tt>.
strSuffixOf :: Expr StringSort -> Expr StringSort -> Expr BoolSort

-- | First string contains second one <tt>(str.contains s t)</tt> iff
--   <tt>s</tt> contains <tt>t</tt>.
strContains :: Expr StringSort -> Expr StringSort -> Expr BoolSort

-- | Index of first occurrence of second string in first one starting at
--   the position specified by the third argument. <tt>(str.indexof s t
--   i)</tt>, with <tt>0 &lt;= i &lt;= |s|</tt> is the position of the
--   first occurrence of <tt>t</tt> in <tt>s</tt> at or after position
--   <tt>i</tt>, if any. Otherwise, it is <tt>-1</tt>. Note that the result
--   is <tt>i</tt> whenever <tt>i</tt> is within the range <tt>[0,
--   |s|]</tt> and <tt>t</tt> is empty.
strIndexOf :: Expr StringSort -> Expr StringSort -> Expr IntSort -> Expr IntSort

-- | <tt>(str.replace s t t')</tt> is the string obtained by replacing the
--   first occurrence of <tt>t</tt> in <tt>s</tt>, if any, by <tt>t'</tt>.
--   Note that if <tt>t</tt> is empty, the result is to prepend <tt>t'</tt>
--   to <tt>s</tt>; also, if <tt>t</tt> does not occur in <tt>s</tt> then
--   the result is <tt>s</tt>.
strReplace :: Expr StringSort -> Expr StringSort -> Expr StringSort -> Expr StringSort

-- | <tt>(str.replace_all s t t’)</tt> is <tt>s</tt> if <tt>t</tt> is the
--   empty string. Otherwise, it is the string obtained from <tt>s</tt> by
--   replacing all occurrences of <tt>t</tt> in <tt>s</tt> by <tt>t’</tt>,
--   starting with the first occurrence and proceeding in left-to-right
--   order.
strReplaceAll :: Expr StringSort -> Expr StringSort -> Expr StringSort -> Expr StringSort
instance Language.Hasmtlib.Type.Expr.Orderable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.IntSort)
instance Language.Hasmtlib.Type.Expr.Orderable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.RealSort)
instance GHC.TypeNats.KnownNat n => Language.Hasmtlib.Type.Expr.Orderable (Language.Hasmtlib.Type.Expr.Expr ('Language.Hasmtlib.Type.SMTSort.BvSort n))
instance Language.Hasmtlib.Type.Expr.Orderable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.StringSort)
instance Language.Hasmtlib.Type.Expr.Orderable a => Language.Hasmtlib.Type.Expr.GOrderable (GHC.Generics.K1 i a)
instance Language.Hasmtlib.Type.Expr.Orderable ()
instance Language.Hasmtlib.Type.Expr.Orderable GHC.Base.Void
instance Language.Hasmtlib.Type.Expr.Orderable GHC.Types.Int
instance Language.Hasmtlib.Type.Expr.Orderable GHC.Num.Integer.Integer
instance Language.Hasmtlib.Type.Expr.Orderable GHC.Num.Natural.Natural
instance Language.Hasmtlib.Type.Expr.Orderable GHC.Types.Word
instance Language.Hasmtlib.Type.Expr.Orderable GHC.Word.Word8
instance Language.Hasmtlib.Type.Expr.Orderable GHC.Word.Word16
instance Language.Hasmtlib.Type.Expr.Orderable GHC.Word.Word32
instance Language.Hasmtlib.Type.Expr.Orderable GHC.Word.Word64
instance Language.Hasmtlib.Type.Expr.Orderable GHC.Int.Int8
instance Language.Hasmtlib.Type.Expr.Orderable GHC.Int.Int16
instance Language.Hasmtlib.Type.Expr.Orderable GHC.Int.Int32
instance Language.Hasmtlib.Type.Expr.Orderable GHC.Int.Int64
instance Language.Hasmtlib.Type.Expr.Orderable GHC.Types.Char
instance Language.Hasmtlib.Type.Expr.Orderable GHC.Types.Float
instance Language.Hasmtlib.Type.Expr.Orderable GHC.Types.Double
instance Language.Hasmtlib.Type.Expr.Orderable GHC.Types.Ordering
instance Language.Hasmtlib.Type.Expr.Orderable GHC.Types.Bool
instance (Language.Hasmtlib.Type.Expr.Orderable a, Language.Hasmtlib.Type.Expr.Orderable b) => Language.Hasmtlib.Type.Expr.Orderable (a, b)
instance (Language.Hasmtlib.Type.Expr.Orderable a, Language.Hasmtlib.Type.Expr.Orderable b, Language.Hasmtlib.Type.Expr.Orderable c) => Language.Hasmtlib.Type.Expr.Orderable (a, b, c)
instance (Language.Hasmtlib.Type.Expr.Orderable a, Language.Hasmtlib.Type.Expr.Orderable b, Language.Hasmtlib.Type.Expr.Orderable c, Language.Hasmtlib.Type.Expr.Orderable d) => Language.Hasmtlib.Type.Expr.Orderable (a, b, c, d)
instance (Language.Hasmtlib.Type.Expr.Orderable a, Language.Hasmtlib.Type.Expr.Orderable b, Language.Hasmtlib.Type.Expr.Orderable c, Language.Hasmtlib.Type.Expr.Orderable d, Language.Hasmtlib.Type.Expr.Orderable e) => Language.Hasmtlib.Type.Expr.Orderable (a, b, c, d, e)
instance (Language.Hasmtlib.Type.Expr.Orderable a, Language.Hasmtlib.Type.Expr.Orderable b, Language.Hasmtlib.Type.Expr.Orderable c, Language.Hasmtlib.Type.Expr.Orderable d, Language.Hasmtlib.Type.Expr.Orderable e, Language.Hasmtlib.Type.Expr.Orderable f) => Language.Hasmtlib.Type.Expr.Orderable (a, b, c, d, e, f)
instance (Language.Hasmtlib.Type.Expr.Orderable a, Language.Hasmtlib.Type.Expr.Orderable b, Language.Hasmtlib.Type.Expr.Orderable c, Language.Hasmtlib.Type.Expr.Orderable d, Language.Hasmtlib.Type.Expr.Orderable e, Language.Hasmtlib.Type.Expr.Orderable f, Language.Hasmtlib.Type.Expr.Orderable g) => Language.Hasmtlib.Type.Expr.Orderable (a, b, c, d, e, f, g)
instance (Language.Hasmtlib.Type.Expr.Orderable a, Language.Hasmtlib.Type.Expr.Orderable b, Language.Hasmtlib.Type.Expr.Orderable c, Language.Hasmtlib.Type.Expr.Orderable d, Language.Hasmtlib.Type.Expr.Orderable e, Language.Hasmtlib.Type.Expr.Orderable f, Language.Hasmtlib.Type.Expr.Orderable g, Language.Hasmtlib.Type.Expr.Orderable h) => Language.Hasmtlib.Type.Expr.Orderable (a, b, c, d, e, f, g, h)
instance Language.Hasmtlib.Type.Expr.Orderable a => Language.Hasmtlib.Type.Expr.Orderable [a]
instance Language.Hasmtlib.Type.Expr.Orderable a => Language.Hasmtlib.Type.Expr.Orderable (Data.Tree.Tree a)
instance Language.Hasmtlib.Type.Expr.Orderable a => Language.Hasmtlib.Type.Expr.Orderable (GHC.Maybe.Maybe a)
instance (Language.Hasmtlib.Type.Expr.Orderable a, Language.Hasmtlib.Type.Expr.Orderable b) => Language.Hasmtlib.Type.Expr.Orderable (Data.Either.Either a b)
instance Language.Hasmtlib.Type.Expr.Orderable a => Language.Hasmtlib.Type.Expr.Orderable (Data.Semigroup.Internal.Sum a)
instance Language.Hasmtlib.Type.Expr.Orderable a => Language.Hasmtlib.Type.Expr.Orderable (Data.Semigroup.Internal.Product a)
instance Language.Hasmtlib.Type.Expr.Orderable a => Language.Hasmtlib.Type.Expr.Orderable (Data.Monoid.First a)
instance Language.Hasmtlib.Type.Expr.Orderable a => Language.Hasmtlib.Type.Expr.Orderable (Data.Monoid.Last a)
instance Language.Hasmtlib.Type.Expr.Orderable a => Language.Hasmtlib.Type.Expr.Orderable (Data.Semigroup.Internal.Dual a)
instance Language.Hasmtlib.Type.Expr.Orderable a => Language.Hasmtlib.Type.Expr.Orderable (Data.Functor.Identity.Identity a)
instance GHC.Num.Num (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.IntSort)
instance GHC.Num.Num (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.RealSort)
instance Control.Lens.Cons.Cons (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.StringSort) (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.StringSort) (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.StringSort) (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.StringSort)
instance Control.Lens.Cons.Snoc (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.StringSort) (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.StringSort) (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.StringSort) (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.StringSort)
instance Language.Hasmtlib.Type.Expr.GOrderable GHC.Generics.U1
instance Language.Hasmtlib.Type.Expr.GOrderable GHC.Generics.V1
instance forall k (f :: k -> *) (g :: k -> *). (Language.Hasmtlib.Type.Expr.GOrderable f, Language.Hasmtlib.Type.Expr.GOrderable g) => Language.Hasmtlib.Type.Expr.GOrderable (f GHC.Generics.:*: g)
instance forall k (f :: k -> *) (g :: k -> *). (Language.Hasmtlib.Type.Expr.GOrderable f, Language.Hasmtlib.Type.Expr.GOrderable g) => Language.Hasmtlib.Type.Expr.GOrderable (f GHC.Generics.:+: g)
instance forall k (f :: k -> *) i (c :: GHC.Generics.Meta). Language.Hasmtlib.Type.Expr.GOrderable f => Language.Hasmtlib.Type.Expr.GOrderable (GHC.Generics.M1 i c f)
instance (Language.Hasmtlib.Type.SMTSort.KnownSMTSort t, GHC.Classes.Eq (Language.Hasmtlib.Type.SMTSort.HaskellType t)) => Language.Hasmtlib.Type.Expr.Equatable (Language.Hasmtlib.Type.Expr.Expr t)
instance Language.Hasmtlib.Type.Expr.Equatable a => Language.Hasmtlib.Type.Expr.GEquatable (GHC.Generics.K1 i a)
instance Language.Hasmtlib.Type.Expr.Equatable ()
instance Language.Hasmtlib.Type.Expr.Equatable GHC.Base.Void
instance Language.Hasmtlib.Type.Expr.Equatable GHC.Types.Int
instance Language.Hasmtlib.Type.Expr.Equatable GHC.Num.Integer.Integer
instance Language.Hasmtlib.Type.Expr.Equatable GHC.Num.Natural.Natural
instance Language.Hasmtlib.Type.Expr.Equatable GHC.Types.Word
instance Language.Hasmtlib.Type.Expr.Equatable GHC.Word.Word8
instance Language.Hasmtlib.Type.Expr.Equatable GHC.Word.Word16
instance Language.Hasmtlib.Type.Expr.Equatable GHC.Word.Word32
instance Language.Hasmtlib.Type.Expr.Equatable GHC.Word.Word64
instance Language.Hasmtlib.Type.Expr.Equatable GHC.Int.Int8
instance Language.Hasmtlib.Type.Expr.Equatable GHC.Int.Int16
instance Language.Hasmtlib.Type.Expr.Equatable GHC.Int.Int32
instance Language.Hasmtlib.Type.Expr.Equatable GHC.Int.Int64
instance Language.Hasmtlib.Type.Expr.Equatable GHC.Types.Char
instance Language.Hasmtlib.Type.Expr.Equatable GHC.Types.Float
instance Language.Hasmtlib.Type.Expr.Equatable GHC.Types.Double
instance Language.Hasmtlib.Type.Expr.Equatable GHC.Types.Ordering
instance Language.Hasmtlib.Type.Expr.Equatable GHC.Types.Bool
instance (Language.Hasmtlib.Type.Expr.Equatable a, Language.Hasmtlib.Type.Expr.Equatable b) => Language.Hasmtlib.Type.Expr.Equatable (a, b)
instance (Language.Hasmtlib.Type.Expr.Equatable a, Language.Hasmtlib.Type.Expr.Equatable b, Language.Hasmtlib.Type.Expr.Equatable c) => Language.Hasmtlib.Type.Expr.Equatable (a, b, c)
instance (Language.Hasmtlib.Type.Expr.Equatable a, Language.Hasmtlib.Type.Expr.Equatable b, Language.Hasmtlib.Type.Expr.Equatable c, Language.Hasmtlib.Type.Expr.Equatable d) => Language.Hasmtlib.Type.Expr.Equatable (a, b, c, d)
instance (Language.Hasmtlib.Type.Expr.Equatable a, Language.Hasmtlib.Type.Expr.Equatable b, Language.Hasmtlib.Type.Expr.Equatable c, Language.Hasmtlib.Type.Expr.Equatable d, Language.Hasmtlib.Type.Expr.Equatable e) => Language.Hasmtlib.Type.Expr.Equatable (a, b, c, d, e)
instance (Language.Hasmtlib.Type.Expr.Equatable a, Language.Hasmtlib.Type.Expr.Equatable b, Language.Hasmtlib.Type.Expr.Equatable c, Language.Hasmtlib.Type.Expr.Equatable d, Language.Hasmtlib.Type.Expr.Equatable e, Language.Hasmtlib.Type.Expr.Equatable f) => Language.Hasmtlib.Type.Expr.Equatable (a, b, c, d, e, f)
instance (Language.Hasmtlib.Type.Expr.Equatable a, Language.Hasmtlib.Type.Expr.Equatable b, Language.Hasmtlib.Type.Expr.Equatable c, Language.Hasmtlib.Type.Expr.Equatable d, Language.Hasmtlib.Type.Expr.Equatable e, Language.Hasmtlib.Type.Expr.Equatable f, Language.Hasmtlib.Type.Expr.Equatable g) => Language.Hasmtlib.Type.Expr.Equatable (a, b, c, d, e, f, g)
instance (Language.Hasmtlib.Type.Expr.Equatable a, Language.Hasmtlib.Type.Expr.Equatable b, Language.Hasmtlib.Type.Expr.Equatable c, Language.Hasmtlib.Type.Expr.Equatable d, Language.Hasmtlib.Type.Expr.Equatable e, Language.Hasmtlib.Type.Expr.Equatable f, Language.Hasmtlib.Type.Expr.Equatable g, Language.Hasmtlib.Type.Expr.Equatable h) => Language.Hasmtlib.Type.Expr.Equatable (a, b, c, d, e, f, g, h)
instance Language.Hasmtlib.Type.Expr.Equatable a => Language.Hasmtlib.Type.Expr.Equatable [a]
instance Language.Hasmtlib.Type.Expr.Equatable a => Language.Hasmtlib.Type.Expr.Equatable (Data.Tree.Tree a)
instance Language.Hasmtlib.Type.Expr.Equatable a => Language.Hasmtlib.Type.Expr.Equatable (GHC.Maybe.Maybe a)
instance (Language.Hasmtlib.Type.Expr.Equatable a, Language.Hasmtlib.Type.Expr.Equatable b) => Language.Hasmtlib.Type.Expr.Equatable (Data.Either.Either a b)
instance Language.Hasmtlib.Type.Expr.Equatable a => Language.Hasmtlib.Type.Expr.Equatable (Data.Semigroup.Internal.Sum a)
instance Language.Hasmtlib.Type.Expr.Equatable a => Language.Hasmtlib.Type.Expr.Equatable (Data.Semigroup.Internal.Product a)
instance Language.Hasmtlib.Type.Expr.Equatable a => Language.Hasmtlib.Type.Expr.Equatable (Data.Monoid.First a)
instance Language.Hasmtlib.Type.Expr.Equatable a => Language.Hasmtlib.Type.Expr.Equatable (Data.Monoid.Last a)
instance Language.Hasmtlib.Type.Expr.Equatable a => Language.Hasmtlib.Type.Expr.Equatable (Data.Semigroup.Internal.Dual a)
instance Language.Hasmtlib.Type.Expr.Equatable a => Language.Hasmtlib.Type.Expr.Equatable (Data.Functor.Identity.Identity a)
instance Language.Hasmtlib.Boolean.Boolean (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort)
instance Control.Lens.Empty.AsEmpty (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.StringSort)
instance Language.Hasmtlib.Type.Expr.GEquatable GHC.Generics.U1
instance Language.Hasmtlib.Type.Expr.GEquatable GHC.Generics.V1
instance forall k (f :: k -> *) (g :: k -> *). (Language.Hasmtlib.Type.Expr.GEquatable f, Language.Hasmtlib.Type.Expr.GEquatable g) => Language.Hasmtlib.Type.Expr.GEquatable (f GHC.Generics.:*: g)
instance forall k (f :: k -> *) (g :: k -> *). (Language.Hasmtlib.Type.Expr.GEquatable f, Language.Hasmtlib.Type.Expr.GEquatable g) => Language.Hasmtlib.Type.Expr.GEquatable (f GHC.Generics.:+: g)
instance forall k (f :: k -> *) i (c :: GHC.Generics.Meta). Language.Hasmtlib.Type.Expr.GEquatable f => Language.Hasmtlib.Type.Expr.GEquatable (GHC.Generics.M1 i c f)
instance Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) (Language.Hasmtlib.Type.Expr.Expr t)
instance Language.Hasmtlib.Type.Expr.Iteable GHC.Types.Bool a
instance Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) a => Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) [a]
instance Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) a => Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) (GHC.Maybe.Maybe a)
instance Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) a => Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) (Data.Sequence.Internal.Seq a)
instance Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) a => Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) (Data.Tree.Tree a)
instance Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) a => Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) (Data.Semigroup.Internal.Sum a)
instance Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) a => Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) (Data.Semigroup.Internal.Product a)
instance Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) a => Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) (Data.Monoid.First a)
instance Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) a => Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) (Data.Monoid.Last a)
instance Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) a => Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) (Data.Semigroup.Internal.Dual a)
instance Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) a => Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) (Data.Functor.Identity.Identity a)
instance Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) ()
instance (Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) a, Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) b) => Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) (a, b)
instance (Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) a, Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) b, Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) c) => Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) (a, b, c)
instance (Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) a, Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) b, Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) c, Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) d) => Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) (a, b, c, d)
instance (Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) a, Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) b, Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) c, Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) d, Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) e) => Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) (a, b, c, d, e)
instance (Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) a, Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) b, Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) c, Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) d, Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) e, Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) f) => Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) (a, b, c, d, e, f)
instance (Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) a, Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) b, Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) c, Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) d, Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) e, Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) f, Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) g) => Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) (a, b, c, d, e, f, g)
instance (Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) a, Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) b, Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) c, Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) d, Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) e, Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) f, Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) g, Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) h) => Language.Hasmtlib.Type.Expr.Iteable (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) (a, b, c, d, e, f, g, h)
instance Control.Lens.Prism.Prefixed (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.StringSort)
instance Control.Lens.Prism.Suffixed (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.StringSort)
instance GHC.TypeNats.KnownNat n => GHC.Num.Num (Language.Hasmtlib.Type.Expr.Expr ('Language.Hasmtlib.Type.SMTSort.BvSort n))
instance GHC.Real.Fractional (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.RealSort)
instance GHC.Float.Floating (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.RealSort)
instance GHC.Real.Real (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.IntSort)
instance GHC.Enum.Enum (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.IntSort)
instance GHC.Real.Integral (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.IntSort)
instance GHC.Real.Real (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.RealSort)
instance GHC.Enum.Enum (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.RealSort)
instance GHC.TypeNats.KnownNat n => GHC.Real.Real (Language.Hasmtlib.Type.Expr.Expr ('Language.Hasmtlib.Type.SMTSort.BvSort n))
instance GHC.TypeNats.KnownNat n => GHC.Enum.Enum (Language.Hasmtlib.Type.Expr.Expr ('Language.Hasmtlib.Type.SMTSort.BvSort n))
instance GHC.TypeNats.KnownNat n => GHC.Real.Integral (Language.Hasmtlib.Type.Expr.Expr ('Language.Hasmtlib.Type.SMTSort.BvSort n))
instance GHC.TypeNats.KnownNat n => Language.Hasmtlib.Boolean.Boolean (Language.Hasmtlib.Type.Expr.Expr ('Language.Hasmtlib.Type.SMTSort.BvSort n))
instance GHC.Enum.Bounded (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort)
instance GHC.TypeNats.KnownNat n => GHC.Enum.Bounded (Language.Hasmtlib.Type.Expr.Expr ('Language.Hasmtlib.Type.SMTSort.BvSort n))
instance GHC.Bits.Bits (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort)
instance GHC.TypeNats.KnownNat n => GHC.Bits.Bits (Language.Hasmtlib.Type.Expr.Expr ('Language.Hasmtlib.Type.SMTSort.BvSort n))
instance GHC.Base.Semigroup (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.StringSort)
instance GHC.Base.Monoid (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.StringSort)
instance Data.String.IsString (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.StringSort)
instance Language.Hasmtlib.Internal.Render.Render (Language.Hasmtlib.Type.Value.Value t)
instance Language.Hasmtlib.Type.SMTSort.KnownSMTSort t => Language.Hasmtlib.Internal.Render.Render (Language.Hasmtlib.Type.Expr.Expr t)
instance Language.Hasmtlib.Type.SMTSort.KnownSMTSort t => GHC.Show.Show (Language.Hasmtlib.Type.Expr.Expr t)
instance Control.Lens.At.Ixed (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.StringSort)
instance (Language.Hasmtlib.Type.SMTSort.KnownSMTSort k, Language.Hasmtlib.Type.SMTSort.KnownSMTSort v, GHC.Classes.Ord (Language.Hasmtlib.Type.SMTSort.HaskellType k), GHC.Classes.Ord (Language.Hasmtlib.Type.SMTSort.HaskellType v)) => Control.Lens.At.Ixed (Language.Hasmtlib.Type.Expr.Expr ('Language.Hasmtlib.Type.SMTSort.ArraySort k v))
instance Language.Hasmtlib.Internal.Uniplate1.Uniplate1 Language.Hasmtlib.Type.Expr.Expr '[Language.Hasmtlib.Type.SMTSort.KnownSMTSort]
instance Language.Hasmtlib.Type.SMTSort.KnownSMTSort t => Control.Lens.Plated.Plated (Language.Hasmtlib.Type.Expr.Expr t)
instance Data.GADT.DeepSeq.GNFData Language.Hasmtlib.Type.Expr.Expr
instance GHC.Classes.Eq (Language.Hasmtlib.Type.Expr.Expr t)
instance GHC.Classes.Ord (Language.Hasmtlib.Type.Expr.Expr t)
instance Data.GADT.Internal.GEq Language.Hasmtlib.Type.Expr.Expr
instance Data.GADT.Internal.GCompare Language.Hasmtlib.Type.Expr.Expr
instance Language.Hasmtlib.Internal.Render.Render (Language.Hasmtlib.Type.Expr.SMTVar t)
instance GHC.Show.Show (Language.Hasmtlib.Type.Value.Value t)
instance GHC.Classes.Ord (Language.Hasmtlib.Type.Expr.SMTVar t)
instance GHC.Classes.Eq (Language.Hasmtlib.Type.Expr.SMTVar t)
instance GHC.Generics.Generic (Language.Hasmtlib.Type.Expr.SMTVar t)
instance GHC.Show.Show (Language.Hasmtlib.Type.Expr.SMTVar t)

module Language.Hasmtlib.Type.Solution

-- | Function that turns a state into a result and a solution.
type Solver s m = s -> m (Result, Solution)

-- | Results of check-sat commands.
data Result
Unsat :: Result
Unknown :: Result
Sat :: Result

-- | A Solution is a dependent map <a>DMap</a> from <a>SSMTSort</a>s t to
--   <a>IntMap</a> t.
type Solution = DMap SSMTSort IntValueMap

-- | Newtype for <a>IntMap</a> <a>Value</a> so we can use it as
--   right-hand-side of <a>DMap</a>.
newtype IntValueMap t
IntValueMap :: IntMap (Value t) -> IntValueMap t

-- | A solution for a single variable.
data SMTVarSol (t :: SMTSort)
SMTVarSol :: SMTVar t -> Value t -> SMTVarSol (t :: SMTSort)

-- | A variable in the SMT-Problem
[_solVar] :: SMTVarSol (t :: SMTSort) -> SMTVar t

-- | An assignment for this variable in a solution
[_solVal] :: SMTVarSol (t :: SMTSort) -> Value t
solVar :: forall t_a19at. Lens' (SMTVarSol t_a19at) (SMTVar t_a19at)
solVal :: forall t_a19at. Lens' (SMTVarSol t_a19at) (Value t_a19at)

-- | Alias class for constraint <a>Ord</a> (<a>HaskellType</a> t)
class Ord (HaskellType t) => OrdHaskellType t

-- | An existential wrapper that hides some known <a>SMTSort</a> with an
--   <a>Ord</a> <a>HaskellType</a>
type SomeKnownOrdSMTSort f = SomeSMTSort '[KnownSMTSort, OrdHaskellType] f

-- | Create a <a>Solution</a> from some <a>SMTVarSol</a>s.
fromSomeVarSols :: [SomeKnownOrdSMTSort SMTVarSol] -> Solution
instance GHC.Classes.Ord (Language.Hasmtlib.Type.SMTSort.HaskellType t) => Language.Hasmtlib.Type.Solution.OrdHaskellType t
instance GHC.Classes.Ord Language.Hasmtlib.Type.Solution.Result
instance GHC.Classes.Eq Language.Hasmtlib.Type.Solution.Result
instance GHC.Show.Show Language.Hasmtlib.Type.Solution.Result
instance GHC.Base.Monoid (Language.Hasmtlib.Type.Solution.IntValueMap t)
instance GHC.Base.Semigroup (Language.Hasmtlib.Type.Solution.IntValueMap t)
instance GHC.Show.Show (Language.Hasmtlib.Type.Solution.IntValueMap t)
instance GHC.Show.Show (Language.Hasmtlib.Type.Solution.SMTVarSol t)

module Language.Hasmtlib.Counting

-- | Wrapper for <a>count</a> which takes a <a>Proxy</a>.
count' :: forall t f. (Functor f, Foldable f, Num (Expr t)) => Proxy t -> f (Expr BoolSort) -> Expr t

-- | Out of many bool-expressions build a formula which encodes how many of
--   them are <tt>true</tt>.
count :: forall t f. (Functor f, Foldable f, Num (Expr t)) => f (Expr BoolSort) -> Expr t

-- | Out of many bool-expressions build a formula which encodes that <b>at
--   most</b> <tt>k</tt> of them are <tt>true</tt>.
atMost :: forall t f. (Functor f, Foldable f, Num (Expr t), Orderable (Expr t)) => Expr t -> f (Expr BoolSort) -> Expr BoolSort

-- | Out of many bool-expressions build a formula which encodes that <b>at
--   least</b> <tt>k</tt> of them are <tt>true</tt>.
atLeast :: forall t f. (Functor f, Foldable f, Num (Expr t), Orderable (Expr t)) => Expr t -> f (Expr BoolSort) -> Expr BoolSort

-- | Out of many bool-expressions build a formula which encodes that
--   <b>exactly</b> <tt>k</tt> of them are <tt>true</tt>.
exactly :: forall t f. (Functor f, Foldable f, Num (Expr t), Orderable (Expr t)) => Expr t -> f (Expr BoolSort) -> Expr BoolSort

module Language.Hasmtlib.Codec

-- | Computes a default <a>Decoded</a> <a>Type</a> by distributing
--   <a>Decoded</a> to it's type arguments.
type family DefaultDecoded a :: Type

-- | Lift values to SMT-Values or decode them.
--   
--   You can derive an instance of this class if your type is
--   <a>Generic</a>.
class Codec a where {
    
    -- | Result of decoding <tt>a</tt>.
    type Decoded a :: Type;
    type Decoded a = DefaultDecoded a;
}

-- | Decode a value using given solution.
decode :: Codec a => Solution -> a -> Maybe (Decoded a)

-- | Decode a value using given solution.
decode :: (Codec a, Generic a, Generic (Decoded a), GCodec (Rep a), GDecoded (Rep a) x ~ Rep (Decoded a) x) => Solution -> a -> Maybe (Decoded a)

-- | Encode a value as constant.
encode :: Codec a => Decoded a -> a

-- | Encode a value as constant.
encode :: (Codec a, Generic a, Generic (Decoded a), GCodec (Rep a), GDecoded (Rep a) x ~ Rep (Decoded a) x) => Decoded a -> a
class GCodec f where {
    type GDecoded f :: Type -> Type;
}
gdecode :: GCodec f => Solution -> f a -> Maybe (GDecoded f a)
gencode :: GCodec f => GDecoded f a -> f a
instance Language.Hasmtlib.Type.SMTSort.KnownSMTSort t => Language.Hasmtlib.Codec.Codec (Language.Hasmtlib.Type.Expr.Expr t)
instance Language.Hasmtlib.Codec.Codec ()
instance (Language.Hasmtlib.Codec.Codec a, Language.Hasmtlib.Codec.Codec b) => Language.Hasmtlib.Codec.Codec (a, b)
instance (Language.Hasmtlib.Codec.Codec a, Language.Hasmtlib.Codec.Codec b, Language.Hasmtlib.Codec.Codec c) => Language.Hasmtlib.Codec.Codec (a, b, c)
instance (Language.Hasmtlib.Codec.Codec a, Language.Hasmtlib.Codec.Codec b, Language.Hasmtlib.Codec.Codec c, Language.Hasmtlib.Codec.Codec d) => Language.Hasmtlib.Codec.Codec (a, b, c, d)
instance (Language.Hasmtlib.Codec.Codec a, Language.Hasmtlib.Codec.Codec b, Language.Hasmtlib.Codec.Codec c, Language.Hasmtlib.Codec.Codec d, Language.Hasmtlib.Codec.Codec e) => Language.Hasmtlib.Codec.Codec (a, b, c, d, e)
instance (Language.Hasmtlib.Codec.Codec a, Language.Hasmtlib.Codec.Codec b, Language.Hasmtlib.Codec.Codec c, Language.Hasmtlib.Codec.Codec d, Language.Hasmtlib.Codec.Codec e, Language.Hasmtlib.Codec.Codec f) => Language.Hasmtlib.Codec.Codec (a, b, c, d, e, f)
instance (Language.Hasmtlib.Codec.Codec a, Language.Hasmtlib.Codec.Codec b, Language.Hasmtlib.Codec.Codec c, Language.Hasmtlib.Codec.Codec d, Language.Hasmtlib.Codec.Codec e, Language.Hasmtlib.Codec.Codec f, Language.Hasmtlib.Codec.Codec g) => Language.Hasmtlib.Codec.Codec (a, b, c, d, e, f, g)
instance (Language.Hasmtlib.Codec.Codec a, Language.Hasmtlib.Codec.Codec b, Language.Hasmtlib.Codec.Codec c, Language.Hasmtlib.Codec.Codec d, Language.Hasmtlib.Codec.Codec e, Language.Hasmtlib.Codec.Codec f, Language.Hasmtlib.Codec.Codec g, Language.Hasmtlib.Codec.Codec h) => Language.Hasmtlib.Codec.Codec (a, b, c, d, e, f, g, h)
instance Language.Hasmtlib.Codec.Codec a => Language.Hasmtlib.Codec.Codec [a]
instance Language.Hasmtlib.Codec.Codec a => Language.Hasmtlib.Codec.Codec (GHC.Maybe.Maybe a)
instance Language.Hasmtlib.Codec.Codec a => Language.Hasmtlib.Codec.Codec (Data.Tree.Tree a)
instance (Language.Hasmtlib.Codec.Codec a, Language.Hasmtlib.Codec.Codec b) => Language.Hasmtlib.Codec.Codec (Data.Either.Either a b)
instance Language.Hasmtlib.Codec.Codec a => Language.Hasmtlib.Codec.Codec (Data.Semigroup.Internal.Sum a)
instance Language.Hasmtlib.Codec.Codec a => Language.Hasmtlib.Codec.Codec (Data.Semigroup.Internal.Product a)
instance Language.Hasmtlib.Codec.Codec a => Language.Hasmtlib.Codec.Codec (Data.Monoid.First a)
instance Language.Hasmtlib.Codec.Codec a => Language.Hasmtlib.Codec.Codec (Data.Monoid.Last a)
instance Language.Hasmtlib.Codec.Codec a => Language.Hasmtlib.Codec.Codec (Data.Semigroup.Internal.Dual a)
instance Language.Hasmtlib.Codec.Codec a => Language.Hasmtlib.Codec.Codec (Data.Functor.Identity.Identity a)
instance Language.Hasmtlib.Codec.Codec a => Language.Hasmtlib.Codec.Codec (Data.IntMap.Internal.IntMap a)
instance Language.Hasmtlib.Codec.Codec a => Language.Hasmtlib.Codec.Codec (Data.Sequence.Internal.Seq a)
instance Language.Hasmtlib.Codec.Codec a => Language.Hasmtlib.Codec.Codec (Data.Map.Internal.Map k a)
instance Language.Hasmtlib.Codec.Codec a => Language.Hasmtlib.Codec.GCodec (GHC.Generics.K1 i a)
instance Language.Hasmtlib.Codec.GCodec GHC.Generics.U1
instance Language.Hasmtlib.Codec.GCodec GHC.Generics.V1
instance (Language.Hasmtlib.Codec.GCodec f, Language.Hasmtlib.Codec.GCodec g) => Language.Hasmtlib.Codec.GCodec (f GHC.Generics.:*: g)
instance (Language.Hasmtlib.Codec.GCodec f, Language.Hasmtlib.Codec.GCodec g) => Language.Hasmtlib.Codec.GCodec (f GHC.Generics.:+: g)
instance Language.Hasmtlib.Codec.GCodec f => Language.Hasmtlib.Codec.GCodec (GHC.Generics.M1 i c f)

module Language.Hasmtlib.Type.MonadSMT

-- | A <a>MonadState</a> that holds an SMT-Problem.
class MonadState s m => MonadSMT s m

-- | Construct a variable. This is mainly intended for internal use. In the
--   API use <a>var'</a> instead.
--   
--   <pre>
--   x :: SMTVar RealType &lt;- smtvar' (Proxy @RealType)
--   </pre>
smtvar' :: forall t. (MonadSMT s m, KnownSMTSort t) => Proxy t -> m (SMTVar t)

-- | Construct a variable as expression.
--   
--   <pre>
--   x :: Expr RealType &lt;- var' (Proxy @RealType)
--   </pre>
var' :: forall t. (MonadSMT s m, KnownSMTSort t) => Proxy t -> m (Expr t)

-- | Assert a boolean expression.
--   
--   <pre>
--   x :: Expr IntType &lt;- var @IntType
--   assert $ x + 5 === 42
--   </pre>
assert :: MonadSMT s m => Expr BoolSort -> m ()

-- | Set an SMT-Solver-Option.
--   
--   <pre>
--   setOption $ Incremental True
--   </pre>
setOption :: MonadSMT s m => SMTOption -> m ()

-- | Set the logic for the SMT-Solver to use.
--   
--   <pre>
--   setLogic "QF_LRA"
--   </pre>
setLogic :: MonadSMT s m => String -> m ()

-- | Wrapper for <a>var'</a> which hides the <a>Proxy</a>.
var :: forall t s m. (KnownSMTSort t, MonadSMT s m) => m (Expr t)

-- | Wrapper for <a>smtvar'</a> which hides the <a>Proxy</a>. This is
--   mainly intended for internal use. In the API use <a>var</a> instead.
smtvar :: forall t s m. (KnownSMTSort t, MonadSMT s m) => m (SMTVar t)

-- | Create a constant.
--   
--   <pre>
--   &gt;&gt;&gt; constant True
--       Constant (BoolValue True)
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; let x :: Integer = 10 ; constant x
--       Constant (IntValue 10)
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; constant @IntType 5
--       Constant (IntValue 5)
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; constant @(BvType 8) 5
--       Constant (BvValue 0000101)
--   </pre>
constant :: KnownSMTSort t => HaskellType t -> Expr t

-- | Maybe assert a boolean expression. Asserts given expression if
--   <a>Maybe</a> is a <a>Just</a>. Does nothing otherwise.
assertMaybe :: MonadSMT s m => Maybe (Expr BoolSort) -> m ()

-- | Assign quantified variables to all quantified subexpressions of an
--   expression. This shall only be used internally. Usually before
--   rendering an assert.
quantify :: MonadSMT s m => KnownSMTSort t => Expr t -> m (Expr t)

-- | A <a>MonadSMT</a> that allows incremental solving.
class MonadSMT s m => MonadIncrSMT s m

-- | Push a new context (one) to the solvers context-stack.
push :: MonadIncrSMT s m => m ()

-- | Pop the solvers context-stack by one.
pop :: MonadIncrSMT s m => m ()

-- | Run check-sat on the current problem.
checkSat :: MonadIncrSMT s m => m Result

-- | Run get-model on the current problem. This can be used to decode
--   temporary models within the SMT-Problem.
--   
--   <pre>
--   x &lt;- var @RealSort
--   y &lt;- var
--   assert $ x &gt;? y &amp;&amp; y &lt;? (-1)
--   res &lt;- checkSat
--   case res of
--     Unsat -&gt; print "Unsat. Cannot get model."
--     r     -&gt; do
--       model &lt;- getModel
--       liftIO $ print $ decode model x
--   </pre>
getModel :: MonadIncrSMT s m => m Solution

-- | Evaluate any expressions value in the solvers model. Requires a
--   <a>Sat</a> or <a>Unknown</a> check-sat response beforehand.
--   
--   <pre>
--   x &lt;- var @RealSort
--   assert $ x &gt;? 10
--   res &lt;- checkSat
--   case res of
--     Unsat -&gt; print "Unsat. Cannot get value for <tt>x</tt>."
--     r     -&gt; do
--       x' &lt;- getValue x
--       liftIO $ print $ show r ++ ": x = " ++ show x'
--   </pre>
getValue :: (MonadIncrSMT s m, KnownSMTSort t) => Expr t -> m (Maybe (Decoded (Expr t)))

-- | First run <a>checkSat</a> and then <a>getModel</a> on the current
--   problem.
solve :: (MonadIncrSMT s m, MonadIO m) => m (Result, Solution)

-- | A <a>MonadState</a> that holds an OMT-Problem. An OMT-Problem is a
--   'SMT-Problem' with additional optimization targets.
class MonadSMT s m => MonadOMT s m

-- | Minimizes a numerical expression within the OMT-Problem.
--   
--   For example, below minimization:
--   
--   <pre>
--   x &lt;- var @IntSort
--   assert $ x &gt;? -2
--   minimize x
--   </pre>
--   
--   will give <tt>x := -1</tt> as solution.
minimize :: (MonadOMT s m, KnownSMTSort t, Num (Expr t)) => Expr t -> m ()

-- | Maximizes a numerical expression within the OMT-Problem.
--   
--   For example, below maximization:
--   
--   <pre>
--   x &lt;- var @(BvSort 8)
--   maximize x
--   </pre>
--   
--   will give <tt>x := 11111111</tt> as solution.
maximize :: (MonadOMT s m, KnownSMTSort t, Num (Expr t)) => Expr t -> m ()

-- | Asserts a soft boolean expression. May take a weight and an identifier
--   for grouping.
--   
--   For example, below a soft constraint with weight 2.0 and identifier
--   "myId" for grouping:
--   
--   <pre>
--   x &lt;- var @BoolSort
--   assertSoft x (Just 2.0) (Just "myId")
--   </pre>
--   
--   Omitting the weight will default it to 1.0.
--   
--   <pre>
--   x &lt;- var <tt>BoolSort
--   y &lt;- var </tt>BoolSort
--   assertSoft x
--   assertSoft y (Just "myId")
--   </pre>
assertSoft :: MonadOMT s m => Expr BoolSort -> Maybe Double -> Maybe String -> m ()

-- | Like <a>assertSoft</a> but forces a weight and omits the group-id.
assertSoftWeighted :: MonadOMT s m => Expr BoolSort -> Double -> m ()

module Language.Hasmtlib.Internal.Sharing

-- | States that can share expressions by comparing their
--   <a>StableName</a>s.
class Sharing s where {
    
    -- | A constraint on the monad used when asserting the shared node in
    --   <a>assertSharedNode</a>.
    type SharingMonad s :: (Type -> Type) -> Constraint;
}

-- | A <a>Lens'</a> on a mapping between a <a>StableName</a> and it's
--   <a>Expr</a> we may share.
stableMap :: Sharing s => Lens' s (HashMap (StableName ()) (SomeKnownSMTSort Expr))

-- | Asserts that a node-expression is represented by it's auxiliary
--   node-variable: <tt>nodeExpr :: Expr t === nodeVar</tt>. Also gives
--   access to the <a>StableName</a> of the original expression.
assertSharedNode :: (Sharing s, MonadState s m, SharingMonad s m) => StableName () -> Expr BoolSort -> m ()

-- | Sets the mode used for sharing common expressions. Defaults to
--   <a>StableNames</a>.
setSharingMode :: (Sharing s, MonadState s m) => SharingMode -> m ()

-- | Mode used for sharing.
data SharingMode

-- | Common expressions are not shared at all
None :: SharingMode

-- | Expressions that resolve to the same <a>StableName</a> are shared
StableNames :: SharingMode

-- | Shares all possible sub-expressions in given expression. Replaces each
--   node in the expression-tree with an auxiliary variable. All nodes
--   <tt>x</tt> <tt>y</tt> where <tt>makeStableName x == makeStableName
--   y</tt> are replaced with the same auxiliary variable. Therefore this
--   creates a DAG.
runSharing :: (KnownSMTSort t, MonadSMT s m, Sharing s, SharingMonad s m) => SharingMode -> Expr t -> m (Expr t)

-- | Returns an auxiliary variable representing this expression node. If
--   such a shared auxiliary variable exists already, returns that.
--   Otherwise creates one and returns it.
share :: (Equatable (Expr t), KnownSMTSort t, MonadSMT s m, Sharing s, SharingMonad s m) => Expr t -> m (Expr t) -> m (Expr t)
instance GHC.Show.Show Language.Hasmtlib.Internal.Sharing.SharingMode
instance Data.Default.Class.Default Language.Hasmtlib.Internal.Sharing.SharingMode

module Language.Hasmtlib.Type.SMT

-- | The state of the SMT-problem.
data SMT
SMT :: {-# UNPACK #-} !Int -> !Seq (SomeKnownSMTSort SMTVar) -> !Seq (Expr BoolSort) -> Maybe String -> [SMTOption] -> !SharingMode -> !HashMap (StableName ()) (SomeKnownSMTSort Expr) -> SMT

-- | Last Id assigned to a new var
[_lastVarId] :: SMT -> {-# UNPACK #-} !Int

-- | All constructed variables
[_vars] :: SMT -> !Seq (SomeKnownSMTSort SMTVar)

-- | All asserted formulas
[_formulas] :: SMT -> !Seq (Expr BoolSort)

-- | Logic for the SMT-Solver
[_mlogic] :: SMT -> Maybe String

-- | All manually configured SMT-Solver-Options
[_options] :: SMT -> [SMTOption]

-- | How to share common expressions
[_sharingMode] :: SMT -> !SharingMode

-- | Mapping between a <a>StableName</a> and it's <a>Expr</a> we may share
[_stableMap] :: SMT -> !HashMap (StableName ()) (SomeKnownSMTSort Expr)
vars :: Lens' SMT (Seq (SomeKnownSMTSort SMTVar))
stableMap :: Lens' SMT (HashMap (StableName ()) (SomeKnownSMTSort Expr))
sharingMode :: Lens' SMT SharingMode
options :: Lens' SMT [SMTOption]
mlogic :: Lens' SMT (Maybe String)
lastVarId :: Lens' SMT Int
formulas :: Lens' SMT (Seq (Expr 'BoolSort))
renderSetLogic :: Builder -> Builder
renderDeclareVar :: forall t. KnownSMTSort t => SMTVar t -> Builder
renderAssert :: Expr BoolSort -> Builder
renderVars :: Seq (SomeKnownSMTSort SMTVar) -> Seq Builder
instance Data.Default.Class.Default Language.Hasmtlib.Type.SMT.SMT
instance Language.Hasmtlib.Internal.Sharing.Sharing Language.Hasmtlib.Type.SMT.SMT
instance Control.Monad.State.Class.MonadState Language.Hasmtlib.Type.SMT.SMT m => Language.Hasmtlib.Type.MonadSMT.MonadSMT Language.Hasmtlib.Type.SMT.SMT m
instance Language.Hasmtlib.Internal.Render.RenderSeq Language.Hasmtlib.Type.SMT.SMT

module Language.Hasmtlib.Type.OMT

-- | An assertion of a booolean expression in OMT that may be weighted.
data SoftFormula
SoftFormula :: Expr BoolSort -> Maybe Double -> Maybe String -> SoftFormula

-- | The underlying soft formula
[_formula] :: SoftFormula -> Expr BoolSort

-- | Weight of the soft formula
[_mWeight] :: SoftFormula -> Maybe Double

-- | Group-Id of the soft formula
[_mGroupId] :: SoftFormula -> Maybe String
mWeight :: Lens' SoftFormula (Maybe Double)
mGroupId :: Lens' SoftFormula (Maybe String)
formula :: Lens' SoftFormula (Expr 'BoolSort)

-- | A newtype for numerical expressions that are target of a minimization.
newtype Minimize t
Minimize :: Expr t -> Minimize t
[_targetMin] :: Minimize t -> Expr t

-- | A newtype for numerical expressions that are target of a maximization.
newtype Maximize t
Maximize :: Expr t -> Maximize t
[_targetMax] :: Maximize t -> Expr t

-- | The state of the OMT-problem.
data OMT
OMT :: !SMT -> !Seq (SomeKnownSMTSort Minimize) -> !Seq (SomeKnownSMTSort Maximize) -> !Seq SoftFormula -> OMT

-- | The underlying <a>SMT</a>-Problem
[_smt] :: OMT -> !SMT

-- | All expressions to minimize
[_targetMinimize] :: OMT -> !Seq (SomeKnownSMTSort Minimize)

-- | All expressions to maximize
[_targetMaximize] :: OMT -> !Seq (SomeKnownSMTSort Maximize)

-- | All soft assertions of boolean expressions
[_softFormulas] :: OMT -> !Seq SoftFormula
targetMinimize :: Lens' OMT (Seq (SomeKnownSMTSort Minimize))
targetMaximize :: Lens' OMT (Seq (SomeKnownSMTSort Maximize))
softFormulas :: Lens' OMT (Seq SoftFormula)
smt :: Lens' OMT SMT
instance Data.Default.Class.Default Language.Hasmtlib.Type.OMT.OMT
instance Language.Hasmtlib.Internal.Sharing.Sharing Language.Hasmtlib.Type.OMT.OMT
instance Control.Monad.State.Class.MonadState Language.Hasmtlib.Type.OMT.OMT m => Language.Hasmtlib.Type.MonadSMT.MonadSMT Language.Hasmtlib.Type.OMT.OMT m
instance Language.Hasmtlib.Type.MonadSMT.MonadSMT Language.Hasmtlib.Type.OMT.OMT m => Language.Hasmtlib.Type.MonadSMT.MonadOMT Language.Hasmtlib.Type.OMT.OMT m
instance Language.Hasmtlib.Internal.Render.Render Language.Hasmtlib.Type.OMT.SoftFormula
instance Language.Hasmtlib.Type.SMTSort.KnownSMTSort t => Language.Hasmtlib.Internal.Render.Render (Language.Hasmtlib.Type.OMT.Minimize t)
instance Language.Hasmtlib.Type.SMTSort.KnownSMTSort t => Language.Hasmtlib.Internal.Render.Render (Language.Hasmtlib.Type.OMT.Maximize t)
instance Language.Hasmtlib.Internal.Render.RenderSeq Language.Hasmtlib.Type.OMT.OMT
instance GHC.Show.Show Language.Hasmtlib.Type.OMT.SoftFormula

module Language.Hasmtlib.Internal.Parser
answerParser :: Parser (Result, Solution)
resultParser :: Parser Result
anyModelParser :: Parser Solution
defaultModelParser :: Parser Solution
smt2ModelParser :: Parser Solution
parseSomeSol :: Parser (SomeKnownOrdSMTSort SMTVarSol)
parseSomeSort :: Parser (SomeKnownOrdSMTSort SSMTSort)
parseSomeBitVecSort :: Parser (SomeKnownOrdSMTSort SSMTSort)
parseSomeArraySort :: Parser (SomeKnownOrdSMTSort SSMTSort)
parseExpr' :: forall prxy t. KnownSMTSort t => prxy t -> Parser (Expr t)
parseExpr :: forall t. KnownSMTSort t => Parser (Expr t)
var :: KnownSMTSort t => Parser (Expr t)
constant :: forall t. KnownSMTSort t => Parser (HaskellType t)
constantExpr :: forall t. KnownSMTSort t => Parser (Expr t)
anyBitvector :: KnownNat n => Proxy n -> Parser (Bitvec n)
binBitvector :: KnownNat n => Proxy n -> Parser (Bitvec n)
hexBitvector :: KnownNat n => Proxy n -> Parser (Bitvec n)
literalBitvector :: KnownNat n => Proxy n -> Parser (Bitvec n)
constArray :: forall k v. (KnownSMTSort v, Ord (HaskellType k)) => Proxy k -> Proxy v -> Parser (ConstArray (HaskellType k) (HaskellType v))
parseSmtString :: Parser Text
unary :: forall t r. KnownSMTSort t => ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
binary :: forall t u r. (KnownSMTSort t, KnownSMTSort u) => ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
ternary :: forall t u v r. (KnownSMTSort t, KnownSMTSort u, KnownSMTSort v) => ByteString -> (Expr t -> Expr u -> Expr v -> Expr r) -> Parser (Expr r)
nary :: forall t r. KnownSMTSort t => ByteString -> ([Expr t] -> Expr r) -> Parser (Expr r)
smtPi :: Parser (Expr RealSort)
anyValue :: Num a => Parser a -> Parser a
negativeValue :: Num a => Parser a -> Parser a
parseRatioDouble :: Parser Double
parseToRealDouble :: Parser Double
parseBool :: Parser Bool
getValueParser :: KnownSMTSort t => SMTVar t -> Parser (SMTVarSol t)

module Language.Hasmtlib.Type.Pipe

-- | A pipe to the solver. If <a>Solver</a> is <a>Queuing</a> then all
--   commands that do not expect an answer are sent to the queue. All
--   commands that expect an answer have the queue to be sent to the solver
--   before sending the command itself. If <a>Solver</a> is not
--   <a>Queuing</a>, all commands are sent to the solver immediately.
data Pipe
Pipe :: {-# UNPACK #-} !Int -> Maybe String -> !SharingMode -> !HashMap (StableName ()) (SomeKnownSMTSort Expr) -> !Seq (Seq (StableName ())) -> !Solver -> !Bool -> Pipe

-- | Last Id assigned to a new var
[_lastPipeVarId] :: Pipe -> {-# UNPACK #-} !Int

-- | Logic for the SMT-Solver
[_mPipeLogic] :: Pipe -> Maybe String

-- | How to share common expressions
[_pipeSharingMode] :: Pipe -> !SharingMode

-- | Mapping between a <a>StableName</a> and it's <a>Expr</a> we may share
[_pipeStableMap] :: Pipe -> !HashMap (StableName ()) (SomeKnownSMTSort Expr)

-- | Index of each <a>Seq</a> (<a>StableName</a> ()) is incremental stack
--   height where <a>StableName</a> representing auxiliary var that has
--   been shared
[_incrSharedAuxs] :: Pipe -> !Seq (Seq (StableName ()))

-- | Active pipe to the backend
[_pipeSolver] :: Pipe -> !Solver

-- | Flag if pipe shall debug
[_isDebugging] :: Pipe -> !Bool
pipeStableMap :: Lens' Pipe (HashMap (StableName ()) (SomeKnownSMTSort Expr))
pipeSolver :: Lens' Pipe Solver
pipeSharingMode :: Lens' Pipe SharingMode
mPipeLogic :: Lens' Pipe (Maybe String)
lastPipeVarId :: Lens' Pipe Int
isDebugging :: Lens' Pipe Bool
incrSharedAuxs :: Lens' Pipe (Seq (Seq (StableName ())))
instance Language.Hasmtlib.Internal.Sharing.Sharing Language.Hasmtlib.Type.Pipe.Pipe
instance (Control.Monad.State.Class.MonadState Language.Hasmtlib.Type.Pipe.Pipe m, Control.Monad.IO.Class.MonadIO m) => Language.Hasmtlib.Type.MonadSMT.MonadSMT Language.Hasmtlib.Type.Pipe.Pipe m
instance (Control.Monad.State.Class.MonadState Language.Hasmtlib.Type.Pipe.Pipe m, Control.Monad.IO.Class.MonadIO m) => Language.Hasmtlib.Type.MonadSMT.MonadIncrSMT Language.Hasmtlib.Type.Pipe.Pipe m
instance (Language.Hasmtlib.Type.MonadSMT.MonadSMT Language.Hasmtlib.Type.Pipe.Pipe m, Control.Monad.IO.Class.MonadIO m) => Language.Hasmtlib.Type.MonadSMT.MonadOMT Language.Hasmtlib.Type.Pipe.Pipe m

module Language.Hasmtlib.Type.Solver

-- | Data that can have a <a>Solver</a> which may be debugged.
class WithSolver a

-- | Create a datum with a <a>Solver</a> and a 'Bool for whether to debug
--   the <a>Solver</a>.
withSolver :: WithSolver a => Solver -> Bool -> a

-- | <tt><a>solveWith</a> solver prob</tt> solves a SMT problem
--   <tt>prob</tt> with the given <tt>solver</tt>. It returns a pair
--   consisting of:
--   
--   <ol>
--   <li>A <a>Result</a> that indicates if <tt>prob</tt> is satisfiable
--   (<a>Sat</a>), unsatisfiable (<a>Unsat</a>), or if the solver could not
--   determine any results (<a>Unknown</a>).</li>
--   <li>A <a>Decoded</a> answer that was decoded using the solution to
--   <tt>prob</tt>. Note that this answer is only meaningful if the
--   <a>Result</a> is <a>Sat</a> or <a>Unknown</a> and the answer value is
--   in a <a>Just</a>.</li>
--   </ol>
--   
--   Here is a small example of how to use <a>solveWith</a>:
--   
--   <pre>
--   import Language.Hasmtlib
--   
--   main :: IO ()
--   main = do
--     res &lt;- solveWith <tt>SMT (solver cvc5) $ do
--       setLogic "QF_LIA"
--   
--       x &lt;- var </tt>IntSort
--   
--       assert $ x &gt;? 0
--   
--       return x
--   
--     print res
--   </pre>
solveWith :: (Default s, Monad m, Codec a) => Solver s m -> StateT s m a -> m (Result, Maybe (Decoded a))

-- | Pipes an SMT-problem interactively to the solver. Enables incremental
--   solving by default. Here is a small example of how to use it for
--   solving a problem utilizing the solvers incremental stack:
--   
--   <pre>
--   import Language.Hasmtlib
--   import Control.Monad.IO.Class
--   
--   main :: IO ()
--   main = do
--     cvc5Living &lt;- interactiveSolver cvc5
--     interactiveWith <tt>Pipe cvc5Living $ do
--       setOption $ Incremental True
--       setOption $ ProduceModels True
--       setLogic "QF_LIA"
--   
--       x &lt;- var </tt>IntSort
--   
--       assert $ x &gt;? 0
--   
--       (res, sol) &lt;- solve
--       liftIO $ print res
--       liftIO $ print $ decode sol x
--   
--       push
--       y &lt;- var @IntSort
--   
--       assert $ y &lt;? 0
--       assert $ x === y
--   
--       res' &lt;- checkSat
--       liftIO $ print res'
--       pop
--   
--       res'' &lt;- checkSat
--       liftIO $ print res''
--   
--     return ()
--   </pre>
interactiveWith :: (WithSolver s, MonadIO m) => (Solver, Handle) -> StateT s m () -> m ()

-- | Like <a>interactiveWith</a> but it prints all communication with the
--   solver to console.
debugInteractiveWith :: (WithSolver s, MonadIO m) => (Solver, Handle) -> StateT s m () -> m ()

-- | Solves the current problem with respect to a minimal solution for a
--   given numerical expression.
--   
--   Does not rely on MaxSMT/OMT. Instead uses iterative refinement.
--   
--   If you want access to intermediate results, use
--   <a>solveMinimizedDebug</a> instead.
solveMinimized :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t, Orderable (Expr t)) => Expr t -> m (Result, Solution)

-- | Like <a>solveMinimized</a> but with access to intermediate results.
solveMinimizedDebug :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t, Orderable (Expr t)) => (Solution -> IO ()) -> Expr t -> m (Result, Solution)

-- | Solves the current problem with respect to a maximal solution for a
--   given numerical expression.
--   
--   Does not rely on MaxSMT/OMT. Instead uses iterative refinement.
--   
--   If you want access to intermediate results, use
--   <a>solveMaximizedDebug</a> instead.
solveMaximized :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t, Orderable (Expr t)) => Expr t -> m (Result, Solution)

-- | Like <a>solveMaximized</a> but with access to intermediate results.
solveMaximizedDebug :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t, Orderable (Expr t)) => (Solution -> IO ()) -> Expr t -> m (Result, Solution)
instance Language.Hasmtlib.Type.Solver.WithSolver Language.Hasmtlib.Type.Pipe.Pipe

module Language.Hasmtlib.Solver.Common

-- | Creates a <a>Solver</a> from a <a>Config</a>.
solver :: (RenderSeq s, MonadIO m) => Config -> Solver s m

-- | Creates a debugging <a>Solver</a> from a <a>Config</a>.
debug :: (RenderSeq s, MonadIO m) => Config -> Debugger s -> Solver s m

-- | Creates an interactive session with a solver by creating and returning
--   an alive process-handle <a>Handle</a>. Queues commands by default, see
--   <a>Queuing</a>.
interactiveSolver :: MonadIO m => Config -> m (Solver, Handle)

-- | A type holding actions for debugging states.
data Debugger s
Debugger :: (s -> IO ()) -> (Seq Builder -> IO ()) -> (ByteString -> IO ()) -> (ByteString -> IO ()) -> Debugger s

-- | Debug the entire state
[debugState] :: Debugger s -> s -> IO ()

-- | Debug the linewise-rendered problem
[debugProblem] :: Debugger s -> Seq Builder -> IO ()

-- | Debug the solvers raw response for <tt>(check-sat)</tt>
[debugResultResponse] :: Debugger s -> ByteString -> IO ()

-- | Debug the solvers raw response for <tt>(get-model)</tt>
[debugModelResponse] :: Debugger s -> ByteString -> IO ()

-- | A <a>Solver</a> which holds an external process with a SMT-Solver.
--   This will:
--   
--   <ol>
--   <li>Encode the <a>SMT</a>-problem,</li>
--   <li>Start a new external process for the SMT-Solver,</li>
--   <li>Send the problem to the SMT-Solver,</li>
--   <li>Wait for an answer and parse it and</li>
--   <li>close the process and clean up all resources.</li>
--   </ol>
processSolver :: (RenderSeq s, MonadIO m) => Config -> Maybe (Debugger s) -> Solver s m
instance Data.Default.Class.Default (Language.Hasmtlib.Solver.Common.Debugger Language.Hasmtlib.Type.SMT.SMT)
instance Data.Default.Class.Default (Language.Hasmtlib.Solver.Common.Debugger Language.Hasmtlib.Type.OMT.OMT)

module Language.Hasmtlib.Variable

-- | Construct a variable datum of a data-type by creating variables for
--   all its fields.
--   
--   You can derive an instance of this class if your type is
--   <a>Generic</a> and has exactly one constructor.
--   
--   <pre>
--   data V3 a = V3 a a a deriving Generic
--   instance Variable a =&gt; V3 a
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; varV3 :: V3 (Expr RealType) &lt;- variable ; varV3
--       V3 (Expr RealType) (Expr RealType) (Expr RealType)
--   </pre>
class Variable a
variable :: (Variable a, MonadSMT s m) => m a
variable :: (Variable a, MonadSMT s m, Generic a, GVariable (Rep a)) => m a

-- | Wrapper for <a>variable</a> which takes a <a>Proxy</a>
variable' :: forall s m a. (MonadSMT s m, Variable a) => Proxy a -> m a
class GVariable f
gvariable :: (GVariable f, MonadSMT s m) => m (f a)
instance Language.Hasmtlib.Type.SMTSort.KnownSMTSort t => Language.Hasmtlib.Variable.Variable (Language.Hasmtlib.Type.Expr.Expr t)
instance Language.Hasmtlib.Variable.Variable ()
instance (Language.Hasmtlib.Variable.Variable a, Language.Hasmtlib.Variable.Variable b) => Language.Hasmtlib.Variable.Variable (a, b)
instance (Language.Hasmtlib.Variable.Variable a, Language.Hasmtlib.Variable.Variable b, Language.Hasmtlib.Variable.Variable c) => Language.Hasmtlib.Variable.Variable (a, b, c)
instance (Language.Hasmtlib.Variable.Variable a, Language.Hasmtlib.Variable.Variable b, Language.Hasmtlib.Variable.Variable c, Language.Hasmtlib.Variable.Variable d) => Language.Hasmtlib.Variable.Variable (a, b, c, d)
instance (Language.Hasmtlib.Variable.Variable a, Language.Hasmtlib.Variable.Variable b, Language.Hasmtlib.Variable.Variable c, Language.Hasmtlib.Variable.Variable d, Language.Hasmtlib.Variable.Variable e) => Language.Hasmtlib.Variable.Variable (a, b, c, d, e)
instance (Language.Hasmtlib.Variable.Variable a, Language.Hasmtlib.Variable.Variable b, Language.Hasmtlib.Variable.Variable c, Language.Hasmtlib.Variable.Variable d, Language.Hasmtlib.Variable.Variable e, Language.Hasmtlib.Variable.Variable f) => Language.Hasmtlib.Variable.Variable (a, b, c, d, e, f)
instance (Language.Hasmtlib.Variable.Variable a, Language.Hasmtlib.Variable.Variable b, Language.Hasmtlib.Variable.Variable c, Language.Hasmtlib.Variable.Variable d, Language.Hasmtlib.Variable.Variable e, Language.Hasmtlib.Variable.Variable f, Language.Hasmtlib.Variable.Variable g) => Language.Hasmtlib.Variable.Variable (a, b, c, d, e, f, g)
instance (Language.Hasmtlib.Variable.Variable a, Language.Hasmtlib.Variable.Variable b, Language.Hasmtlib.Variable.Variable c, Language.Hasmtlib.Variable.Variable d, Language.Hasmtlib.Variable.Variable e, Language.Hasmtlib.Variable.Variable f, Language.Hasmtlib.Variable.Variable g, Language.Hasmtlib.Variable.Variable h) => Language.Hasmtlib.Variable.Variable (a, b, c, d, e, f, g, h)
instance Language.Hasmtlib.Variable.Variable a => Language.Hasmtlib.Variable.Variable (Data.Semigroup.Internal.Sum a)
instance Language.Hasmtlib.Variable.Variable a => Language.Hasmtlib.Variable.Variable (Data.Semigroup.Internal.Product a)
instance Language.Hasmtlib.Variable.Variable a => Language.Hasmtlib.Variable.Variable (Data.Monoid.First a)
instance Language.Hasmtlib.Variable.Variable a => Language.Hasmtlib.Variable.Variable (Data.Monoid.Last a)
instance Language.Hasmtlib.Variable.Variable a => Language.Hasmtlib.Variable.Variable (Data.Semigroup.Internal.Dual a)
instance Language.Hasmtlib.Variable.Variable a => Language.Hasmtlib.Variable.Variable (Data.Functor.Identity.Identity a)
instance forall k m (a :: k). Language.Hasmtlib.Variable.Variable m => Language.Hasmtlib.Variable.Variable (Data.Functor.Const.Const m a)
instance forall k (f :: k -> *) (a :: k). Language.Hasmtlib.Variable.Variable (f a) => Language.Hasmtlib.Variable.Variable (Data.Semigroup.Internal.Alt f a)
instance forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1). Language.Hasmtlib.Variable.Variable (f (g a)) => Language.Hasmtlib.Variable.Variable (Data.Functor.Compose.Compose f g a)
instance Language.Hasmtlib.Variable.Variable a => Language.Hasmtlib.Variable.Variable (GHC.Maybe.Maybe a)
instance Language.Hasmtlib.Variable.Variable b => Language.Hasmtlib.Variable.Variable (Data.Either.Either a b)
instance Language.Hasmtlib.Variable.Variable a => Language.Hasmtlib.Variable.GVariable (GHC.Generics.K1 i a)
instance Language.Hasmtlib.Variable.GVariable GHC.Generics.U1
instance forall k (f :: k -> *) (g :: k -> *). (Language.Hasmtlib.Variable.GVariable f, Language.Hasmtlib.Variable.GVariable g) => Language.Hasmtlib.Variable.GVariable (f GHC.Generics.:*: g)
instance forall k (f :: k -> *) i (c :: GHC.Generics.Meta). Language.Hasmtlib.Variable.GVariable f => Language.Hasmtlib.Variable.GVariable (GHC.Generics.M1 i c f)

module Language.Hasmtlib

-- | Mode used for sharing.
data SharingMode

-- | Common expressions are not shared at all
None :: SharingMode

-- | Expressions that resolve to the same <a>StableName</a> are shared
StableNames :: SharingMode

-- | Sets the mode used for sharing common expressions. Defaults to
--   <a>StableNames</a>.
setSharingMode :: (Sharing s, MonadState s m) => SharingMode -> m ()