-- 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.0.0

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 ==>
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.Integraled

-- | <a>Integral</a>-like class for clean API. In context hide the Preludes
--   <a>Integral</a>.
class Integraled a
quot :: Integraled a => a -> a -> a
rem :: Integraled a => a -> a -> a
div :: Integraled a => a -> a -> a
mod :: Integraled a => a -> a -> a
quotRem :: Integraled a => a -> a -> (a, a)
quotRem :: (Integraled a, Integral a) => a -> a -> (a, a)
divMod :: Integraled a => a -> a -> (a, a)
divMod :: (Integraled a, Integral a) => a -> a -> (a, a)
instance Language.Hasmtlib.Integraled.Integraled GHC.Types.Int
instance Language.Hasmtlib.Integraled.Integraled GHC.Num.Integer.Integer
instance Language.Hasmtlib.Integraled.Integraled GHC.Types.Word
instance Language.Hasmtlib.Integraled.Integraled GHC.Num.Natural.Natural
instance Language.Hasmtlib.Integraled.Integraled GHC.Word.Word8
instance Language.Hasmtlib.Integraled.Integraled GHC.Word.Word16
instance Language.Hasmtlib.Integraled.Integraled GHC.Word.Word32
instance Language.Hasmtlib.Integraled.Integraled GHC.Word.Word64
instance GHC.Real.Integral a => Language.Hasmtlib.Integraled.Integraled (Data.Functor.Identity.Identity a)
instance forall k a (b :: k). GHC.Real.Integral a => Language.Hasmtlib.Integraled.Integraled (Data.Functor.Const.Const a b)

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

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)
bvRotL :: forall n i. KnownNat (Mod i n) => Proxy i -> Bitvec n -> Bitvec n
bvRotR :: forall n i. KnownNat (Mod i n) => Proxy i -> Bitvec n -> 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.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.Type.ArrayMap

-- | Class that allows access to a map-like array where specific values are
--   is the default value or 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_ajD3 v_ajD4 k_al5s. Lens (ConstArray k_ajD3 v_ajD4) (ConstArray k_al5s v_ajD4) (Map k_ajD3 v_ajD4) (Map k_al5s v_ajD4)
arrConst :: forall k_ajD3 v_ajD4. Lens' (ConstArray k_ajD3 v_ajD4) v_ajD4
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

-- | 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)) => Proxy k -> Proxy v -> SSMTSort (ArraySort k v)

-- | 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

-- | 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

-- | 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
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 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)) => Language.Hasmtlib.Type.SMTSort.KnownSMTSort ('Language.Hasmtlib.Type.SMTSort.ArraySort k v)
instance Language.Hasmtlib.Internal.Render.Render (Language.Hasmtlib.Type.SMTSort.SSMTSort t)

module Language.Hasmtlib.Iteable

-- | 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
instance Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) (Language.Hasmtlib.Internal.Expr.Expr t)
instance Language.Hasmtlib.Iteable.Iteable GHC.Types.Bool a
instance Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) a => Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) [a]
instance Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) a => Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) (GHC.Maybe.Maybe a)
instance Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) a => Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) (Data.Sequence.Internal.Seq a)
instance Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) a => Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) (Data.Tree.Tree a)
instance Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) ()
instance (Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) a, Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) b) => Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) (a, b)
instance (Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) a, Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) b, Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) c) => Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) (a, b, c)
instance (Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) a, Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) b, Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) c, Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) d) => Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) (a, b, c, d)
instance (Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) a, Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) b, Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) c, Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) d, Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) e) => Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) (a, b, c, d, e)
instance (Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) a, Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) b, Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) c, Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) d, Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) e, Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) f) => Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) (a, b, c, d, e, f)
instance (Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) a, Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) b, Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) c, Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) d, Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) e, Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) f, Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) g) => Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) (a, b, c, d, e, f, g)
instance (Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) a, Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) b, Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) c, Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) d, Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) e, Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) f, Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) g, Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) h) => Language.Hasmtlib.Iteable.Iteable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) (a, b, c, d, e, f, g, h)

module Language.Hasmtlib.Equatable

-- | Test two as on equality as SMT-Expression.
--   
--   <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 /==
class GEquatable f
(===#) :: GEquatable f => f a -> f a -> Expr BoolSort
instance (Language.Hasmtlib.Type.SMTSort.KnownSMTSort t, GHC.Classes.Eq (Language.Hasmtlib.Type.SMTSort.HaskellType t)) => Language.Hasmtlib.Equatable.Equatable (Language.Hasmtlib.Internal.Expr.Expr t)
instance Language.Hasmtlib.Equatable.Equatable a => Language.Hasmtlib.Equatable.GEquatable (GHC.Generics.K1 i a)
instance Language.Hasmtlib.Equatable.Equatable ()
instance Language.Hasmtlib.Equatable.Equatable GHC.Base.Void
instance Language.Hasmtlib.Equatable.Equatable GHC.Types.Int
instance Language.Hasmtlib.Equatable.Equatable GHC.Num.Integer.Integer
instance Language.Hasmtlib.Equatable.Equatable GHC.Num.Natural.Natural
instance Language.Hasmtlib.Equatable.Equatable GHC.Types.Word
instance Language.Hasmtlib.Equatable.Equatable GHC.Word.Word8
instance Language.Hasmtlib.Equatable.Equatable GHC.Word.Word16
instance Language.Hasmtlib.Equatable.Equatable GHC.Word.Word32
instance Language.Hasmtlib.Equatable.Equatable GHC.Word.Word64
instance Language.Hasmtlib.Equatable.Equatable GHC.Int.Int8
instance Language.Hasmtlib.Equatable.Equatable GHC.Int.Int16
instance Language.Hasmtlib.Equatable.Equatable GHC.Int.Int32
instance Language.Hasmtlib.Equatable.Equatable GHC.Int.Int64
instance Language.Hasmtlib.Equatable.Equatable GHC.Types.Char
instance Language.Hasmtlib.Equatable.Equatable GHC.Types.Float
instance Language.Hasmtlib.Equatable.Equatable GHC.Types.Double
instance Language.Hasmtlib.Equatable.Equatable GHC.Types.Ordering
instance Language.Hasmtlib.Equatable.Equatable GHC.Types.Bool
instance Language.Hasmtlib.Equatable.GEquatable GHC.Generics.U1
instance Language.Hasmtlib.Equatable.GEquatable GHC.Generics.V1
instance forall k (f :: k -> *) (g :: k -> *). (Language.Hasmtlib.Equatable.GEquatable f, Language.Hasmtlib.Equatable.GEquatable g) => Language.Hasmtlib.Equatable.GEquatable (f GHC.Generics.:*: g)
instance forall k (f :: k -> *) (g :: k -> *). (Language.Hasmtlib.Equatable.GEquatable f, Language.Hasmtlib.Equatable.GEquatable g) => Language.Hasmtlib.Equatable.GEquatable (f GHC.Generics.:+: g)
instance forall k (f :: k -> *) i (c :: GHC.Generics.Meta). Language.Hasmtlib.Equatable.GEquatable f => Language.Hasmtlib.Equatable.GEquatable (GHC.Generics.M1 i c f)

module Language.Hasmtlib.Orderable

-- | Compare two as as SMT-Expression.
--   
--   <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
class GEquatable f => GOrderable f
(<?#) :: GOrderable f => f a -> f a -> Expr BoolSort
(<=?#) :: GOrderable f => f a -> f a -> Expr BoolSort
instance Language.Hasmtlib.Orderable.Orderable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.IntSort)
instance Language.Hasmtlib.Orderable.Orderable (Language.Hasmtlib.Internal.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.RealSort)
instance GHC.TypeNats.KnownNat n => Language.Hasmtlib.Orderable.Orderable (Language.Hasmtlib.Internal.Expr.Expr ('Language.Hasmtlib.Type.SMTSort.BvSort n))
instance Language.Hasmtlib.Orderable.Orderable a => Language.Hasmtlib.Orderable.GOrderable (GHC.Generics.K1 i a)
instance Language.Hasmtlib.Orderable.Orderable ()
instance Language.Hasmtlib.Orderable.Orderable GHC.Base.Void
instance Language.Hasmtlib.Orderable.Orderable GHC.Types.Int
instance Language.Hasmtlib.Orderable.Orderable GHC.Num.Integer.Integer
instance Language.Hasmtlib.Orderable.Orderable GHC.Num.Natural.Natural
instance Language.Hasmtlib.Orderable.Orderable GHC.Types.Word
instance Language.Hasmtlib.Orderable.Orderable GHC.Word.Word8
instance Language.Hasmtlib.Orderable.Orderable GHC.Word.Word16
instance Language.Hasmtlib.Orderable.Orderable GHC.Word.Word32
instance Language.Hasmtlib.Orderable.Orderable GHC.Word.Word64
instance Language.Hasmtlib.Orderable.Orderable GHC.Int.Int8
instance Language.Hasmtlib.Orderable.Orderable GHC.Int.Int16
instance Language.Hasmtlib.Orderable.Orderable GHC.Int.Int32
instance Language.Hasmtlib.Orderable.Orderable GHC.Int.Int64
instance Language.Hasmtlib.Orderable.Orderable GHC.Types.Char
instance Language.Hasmtlib.Orderable.Orderable GHC.Types.Float
instance Language.Hasmtlib.Orderable.Orderable GHC.Types.Double
instance Language.Hasmtlib.Orderable.Orderable GHC.Types.Ordering
instance Language.Hasmtlib.Orderable.Orderable GHC.Types.Bool
instance Language.Hasmtlib.Orderable.GOrderable GHC.Generics.U1
instance Language.Hasmtlib.Orderable.GOrderable GHC.Generics.V1
instance forall k (f :: k -> *) (g :: k -> *). (Language.Hasmtlib.Orderable.GOrderable f, Language.Hasmtlib.Orderable.GOrderable g) => Language.Hasmtlib.Orderable.GOrderable (f GHC.Generics.:*: g)
instance forall k (f :: k -> *) (g :: k -> *). (Language.Hasmtlib.Orderable.GOrderable f, Language.Hasmtlib.Orderable.GOrderable g) => Language.Hasmtlib.Orderable.GOrderable (f GHC.Generics.:+: g)
instance forall k (f :: k -> *) i (c :: GHC.Generics.Meta). Language.Hasmtlib.Orderable.GOrderable f => Language.Hasmtlib.Orderable.GOrderable (GHC.Generics.M1 i c f)

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_aswJ t_asD2. Iso (SMTVar t_aswJ) (SMTVar t_asD2) Int Int

-- | A wrapper for values of <a>SMTSort</a>s.
data Value (t :: SMTSort)
[IntValue] :: HaskellType IntSort -> Value IntSort
[RealValue] :: HaskellType RealSort -> Value RealSort
[BoolValue] :: HaskellType BoolSort -> Value BoolSort
[BvValue] :: HaskellType (BvSort n) -> Value (BvSort n)
[ArrayValue] :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => HaskellType (ArraySort k v) -> Value (ArraySort k v)

-- | Unwrap a value from <a>Value</a>.
unwrapValue :: Value t -> HaskellType t

-- | Wrap a value into <a>Value</a>.
wrapValue :: forall t. KnownSMTSort t => HaskellType t -> Value t

-- | A SMT expression. For internal use only. For building expressions use
--   the corresponding instances (Num, Boolean, ...).
data Expr (t :: SMTSort)

-- | 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

-- | 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))

-- | Rotate bitvector left
bvRotL :: (KnownNat n, KnownNat i, KnownNat (Mod i n)) => Proxy i -> Expr (BvSort n) -> Expr (BvSort n)

-- | Rotate bitvector right
bvRotR :: (KnownNat n, KnownNat i, KnownNat (Mod i n)) => Proxy i -> Expr (BvSort n) -> Expr (BvSort n)

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

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

-- | Checks whether an expression of type <a>RealSort</a> may be safely
--   converted to type <a>IntSort</a>.
isIntSort :: Expr RealSort -> 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)) => 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)

module Language.Hasmtlib.Counting
count' :: forall t f. (Functor f, Foldable f, Num (Expr t)) => Proxy t -> f (Expr BoolSort) -> Expr t
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.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_aI8J. Lens' (SMTVarSol t_aI8J) (SMTVar t_aI8J)
solVal :: forall t_aI8J. Lens' (SMTVarSol t_aI8J) (Value t_aI8J)

-- | 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.Codec

-- | Compute the default <a>Decoded</a> <a>Type</a> for every
--   functor-wrapper. Useful for instances using default signatures.
type family DefaultDecoded a :: Type

-- | Lift values to SMT-Values or decode them.
class Codec a where {
    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, Traversable f, Codec b, a ~ f b, Decoded a ~ f (Decoded b)) => Solution -> a -> Maybe (Decoded a)

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

-- | Encode a value as constant.
encode :: (Codec a, Functor f, Codec b, a ~ f b, Decoded a ~ f (Decoded b)) => Decoded a -> a
instance Language.Hasmtlib.Type.SMTSort.KnownSMTSort t => Language.Hasmtlib.Codec.Codec (Language.Hasmtlib.Internal.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 (Data.IntMap.Internal.IntMap 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.Codec (GHC.Maybe.Maybe 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.Tree.Tree a)
instance (Language.Hasmtlib.Codec.Codec a, Language.Hasmtlib.Codec.Codec b) => Language.Hasmtlib.Codec.Codec (Data.Either.Either a b)

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 => Expr t -> m (Expr t)

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

-- | 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.Type.SMT

-- | The state of the SMT-problem.
data SMT
SMT :: {-# UNPACK #-} !Int -> !Seq (SomeKnownSMTSort SMTVar) -> !Seq (Expr BoolSort) -> Maybe String -> [SMTOption] -> 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]
vars :: Lens' SMT (Seq (SomeKnownSMTSort SMTVar))
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 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
[_formula] :: SoftFormula -> Expr BoolSort
[_mWeight] :: SoftFormula -> Maybe Double
[_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 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 :: 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))
parseSelect :: forall k v. (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Proxy k -> Parser (Expr v)
parseStore :: forall k v. (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Parser (Expr (ArraySort k v))
unary :: forall t r. KnownSMTSort t => ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
binary :: forall t r. KnownSMTSort t => ByteString -> (Expr t -> Expr t -> Expr r) -> Parser (Expr r)
nary :: forall t r. KnownSMTSort t => ByteString -> ([Expr t] -> Expr r) -> Parser (Expr r)
smtPi :: Parser (Expr RealSort)
toRealFun :: Parser (Expr RealSort)
toIntFun :: Parser (Expr IntSort)
isIntFun :: Parser (Expr BoolSort)
smtIte :: forall t. KnownSMTSort t => Parser (Expr t)
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 -> !Solver -> Pipe

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

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

-- | Active pipe to the backend
[_pipe] :: Pipe -> !Solver
pipe :: Lens' Pipe Solver
mPipeLogic :: Lens' Pipe (Maybe String)
lastPipeVarId :: Lens' Pipe Int
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.Solver.Common

-- | A newtype-wrapper for <a>Config</a> which configures a solver via
--   external process.
newtype ProcessSolver
ProcessSolver :: Config -> ProcessSolver
[conf] :: ProcessSolver -> Config

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

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

-- | Creates an interactive session with a solver by creating and returning
--   an alive process-handle <a>Handle</a>.
interactiveSolver :: MonadIO m => ProcessSolver -> 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
[debugState] :: Debugger s -> s -> IO ()
[debugProblem] :: Debugger s -> Seq Builder -> IO ()
[debugResultResponse] :: Debugger s -> ByteString -> IO ()
[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.Solver.Z3

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

module Language.Hasmtlib.Solver.Yices

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

module Language.Hasmtlib.Solver.OpenSMT

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

module Language.Hasmtlib.Solver.MathSAT

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

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

module Language.Hasmtlib.Solver.CVC5

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

module Language.Hasmtlib.Type.Solver

-- | Data that can have a <a>Solver</a>.
class WithSolver a
withSolver :: WithSolver a => Solver -> 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 (solver cvc5) $ do
--       setLogic "QF_LIA"
--   
--       x &lt;- var @IntSort
--   
--       assert $ x &gt;? 0
--   
--       return x
--   
--     print res
--   </pre>
solveWith :: (Monad m, Default s, 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 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 </tt>IntSort
--   
--       assert $ y &lt;? 0
--       assert $ x === y
--   
--       res' &lt;- checkSat
--       liftIO $ print res'
--       pop
--   
--       res'' &lt;- checkSat
--       liftIO $ print res''
--   
--     return ()
--   </pre>
interactiveWith :: (MonadIO m, WithSolver s) => (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.Variable

-- | Construct a variable datum of a data-type by creating variables for
--   all its fields.
--   
--   <pre>
--   data V3 a = V3 a a a
--   instance Variable a =&gt; V3 a
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; varV3 &lt;- variable @(V3 (Expr RealType)) ; varV3
--       V3 (Var RealType) (Var RealType) (Var RealType)
--   </pre>
class Variable a
variable :: (Variable a, MonadSMT s m) => m a
variable :: (Variable a, MonadSMT s m, Applicative f, Traversable f, Variable b, a ~ f b) => 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
instance Language.Hasmtlib.Type.SMTSort.KnownSMTSort t => Language.Hasmtlib.Variable.Variable (Language.Hasmtlib.Internal.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 (GHC.Maybe.Maybe a)
instance Language.Hasmtlib.Variable.Variable b => Language.Hasmtlib.Variable.Variable (Data.Either.Either a b)

module Language.Hasmtlib