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


-- | This module provides a more generic version of bool-like algebras than
--   what the Prelude does for <a>Bool</a>.
--   
--   The class <a>Boolean</a> therefore overloads most of the Preludes
--   operators like <a>(&amp;&amp;)</a>.
--   
--   However, as <a>Bool</a> also features an instance of <a>Boolean</a>,
--   you can simply hide the Prelude ones - not having to import either
--   qualified.
--   
--   <h4><b>Example</b></h4>
--   
--   <pre>
--   import Prelude hiding (not, any, all, (&amp;&amp;), (||), and, or)
--   import Language.Hasmtlib
--   
--   problem :: MonadSMT s m =&gt; StateT s m (Expr BoolSort, Expr BoolSort)
--   problem = do
--     x &lt;- var @BoolSort
--     y &lt;- var
--     let b = False || True
--     assert $ x &amp;&amp; y &lt;==&gt; and [x, y, true] &amp;&amp; encode b ==&gt; x &amp;&amp; y
--     return (x,y)
--   </pre>
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.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


-- | This module provides a class <a>ArrayMap</a> and a concrete
--   implementation with <a>ConstArray</a> for McCarthy's basic array
--   theory.
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 (arrStore i x) == x</li>
--   <li>forall A i j x: i /= j ==&gt; (arrSelect (arrStore i x) j ===
--   arrSelect A j)</li>
--   </ol>
class ArrayMap f k v

-- | Construct an <a>ArrayMap</a> via it's const value.
asConst' :: ArrayMap f k v => Proxy f -> Proxy k -> v -> f k v

-- | View the const value of the <a>ArrayMap</a>.
viewConst :: ArrayMap f k v => f k v -> v

-- | Select a value from the <a>ArrayMap</a>.
--   
--   Returns the specific value for given key if there is one. Returns the
--   const value otherwise.
arrSelect :: ArrayMap f k v => f k v -> k -> v

-- | Store a specific value at a given key in an <a>ArrayMap</a>.
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
arrConst :: forall k_aeOA v_aeOB. Lens' (ConstArray k_aeOA v_aeOB) v_aeOB
stored :: forall k_aeOA v_aeOB k_agmZ. Lens (ConstArray k_aeOA v_aeOB) (ConstArray k_agmZ v_aeOB) (Map k_aeOA v_aeOB) (Map k_agmZ v_aeOB)
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)


-- | This module provides the type-level length-indexed and MSB-first
--   bitvector <a>Bitvec</a> built on top of the package <tt>bitvec</tt>
--   and <a>Vector</a>.
--   
--   It also holds it's type of encoding as a phantom-type via
--   <a>BvEnc</a>.
--   
--   <h4><b>Examples</b></h4>
--   
--   <pre>
--   &gt;&gt;&gt; minBound @(Bitvec Unsigned 8)
--   00000000
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; maxBound @(Bitvec Signed 8)
--   01111111
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; (5 :: Bitvec Unsigned 4) + 10
--   1111
--   </pre>
module Language.Hasmtlib.Type.Bitvec

-- | Type of Bitvector encoding - used as promoted type (data-kind).
data BvEnc
Unsigned :: BvEnc
Signed :: BvEnc

-- | Singleton for <a>BvEnc</a>.
data SBvEnc (enc :: BvEnc)
[SUnsigned] :: SBvEnc Unsigned
[SSigned] :: SBvEnc Signed

-- | Compute singleton <a>SBvEnc</a> from it's promoted type <a>BvEnc</a>.
class KnownBvEnc (enc :: BvEnc)
bvEncSing :: KnownBvEnc enc => SBvEnc enc

-- | Wrapper for <a>bvEncSing</a> which takes a <a>Proxy</a>.
bvEncSing' :: forall enc prxy. KnownBvEnc enc => prxy enc -> SBvEnc enc

-- | Wrapper for <a>bvEncSing</a> which takes a <a>Proxy</a> and some
--   ballast. This is helpful for singing on values of type <a>Bitvec</a>
--   where the ballst is a <a>Nat</a>.
bvEncSing'' :: forall enc a prxy. KnownBvEnc enc => prxy enc a -> SBvEnc enc

-- | Length-indexed bitvector (<a>Vector</a>) carrying a phantom type-level
--   <a>BvEnc</a>.
--   
--   Most significant bit is first (index 0) for unsigned bitvectors.
--   Signed bitvectors have their sign bit first (index 0) and their most
--   significant bit second (index 1).
newtype Bitvec (enc :: BvEnc) (n :: Nat)
Bitvec :: Vector n Bit -> Bitvec (enc :: BvEnc) (n :: Nat)
[unBitvec] :: Bitvec (enc :: BvEnc) (n :: Nat) -> Vector n Bit

-- | Concatenation of two bitvectors.
bitvecConcat :: Bitvec enc n -> Bitvec enc m -> Bitvec enc (n + m)

-- | Convert <a>Bitvec</a> with any encoding <a>BvEnc</a> to
--   <a>Unsigned</a>.
asUnsigned :: forall enc n. Bitvec enc n -> Bitvec Unsigned n

-- | Convert <a>Bitvec</a> with any encoding <a>BvEnc</a> to <a>Signed</a>.
asSigned :: forall enc n. Bitvec enc n -> Bitvec Signed n

-- | Constructing a bitvector from a list.
bitvecFromListN :: forall n enc. KnownNat n => [Bit] -> Maybe (Bitvec enc n)

-- | Constructing a bitvector from a list with length given as
--   <a>Proxy</a>.
bitvecFromListN' :: KnownNat n => Proxy n -> [Bit] -> Maybe (Bitvec enc n)

-- | A Lens on the sign-bit of a signed bitvector.
_signBit :: KnownNat (n + 1) => Lens' (Bitvec Signed (n + 1)) Bit
instance GHC.Classes.Ord Language.Hasmtlib.Type.Bitvec.BvEnc
instance GHC.Classes.Eq Language.Hasmtlib.Type.Bitvec.BvEnc
instance GHC.Show.Show Language.Hasmtlib.Type.Bitvec.BvEnc
instance GHC.TypeNats.KnownNat n => Language.Hasmtlib.Boolean.Boolean (Language.Hasmtlib.Type.Bitvec.Bitvec enc n)
instance GHC.Classes.Ord (Language.Hasmtlib.Type.Bitvec.Bitvec enc n)
instance GHC.Classes.Eq (Language.Hasmtlib.Type.Bitvec.Bitvec enc n)
instance GHC.Show.Show (Language.Hasmtlib.Type.Bitvec.SBvEnc enc)
instance GHC.Classes.Eq (Language.Hasmtlib.Type.Bitvec.SBvEnc enc)
instance GHC.Classes.Ord (Language.Hasmtlib.Type.Bitvec.SBvEnc enc)
instance GHC.Show.Show (Language.Hasmtlib.Type.Bitvec.Bitvec enc n)
instance Language.Hasmtlib.Internal.Render.Render (Language.Hasmtlib.Type.Bitvec.Bitvec enc n)
instance (Language.Hasmtlib.Type.Bitvec.KnownBvEnc enc, GHC.TypeNats.KnownNat n) => GHC.Bits.Bits (Language.Hasmtlib.Type.Bitvec.Bitvec enc n)
instance (Language.Hasmtlib.Type.Bitvec.KnownBvEnc enc, GHC.TypeNats.KnownNat n) => GHC.Num.Num (Language.Hasmtlib.Type.Bitvec.Bitvec enc n)
instance (Language.Hasmtlib.Type.Bitvec.KnownBvEnc enc, GHC.TypeNats.KnownNat n) => GHC.Enum.Bounded (Language.Hasmtlib.Type.Bitvec.Bitvec enc n)
instance (Language.Hasmtlib.Type.Bitvec.KnownBvEnc enc, GHC.TypeNats.KnownNat n) => GHC.Enum.Enum (Language.Hasmtlib.Type.Bitvec.Bitvec enc n)
instance (Language.Hasmtlib.Type.Bitvec.KnownBvEnc enc, GHC.TypeNats.KnownNat n) => GHC.Real.Real (Language.Hasmtlib.Type.Bitvec.Bitvec enc n)
instance (Language.Hasmtlib.Type.Bitvec.KnownBvEnc enc, GHC.TypeNats.KnownNat n) => GHC.Real.Integral (Language.Hasmtlib.Type.Bitvec.Bitvec enc n)
instance Language.Hasmtlib.Type.Bitvec.KnownBvEnc 'Language.Hasmtlib.Type.Bitvec.Unsigned
instance Language.Hasmtlib.Type.Bitvec.KnownBvEnc 'Language.Hasmtlib.Type.Bitvec.Signed
instance Data.GADT.Internal.GEq Language.Hasmtlib.Type.Bitvec.SBvEnc
instance Data.GADT.Internal.GCompare Language.Hasmtlib.Type.Bitvec.SBvEnc


-- | This module provides the data-type <a>SMTOption</a> for adjusting a
--   SMT-Solvers options.
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


-- | This module provides the data-type <a>SMTSort</a> and some
--   singleton-operations for it.
--   
--   The type <a>SMTSort</a> is only used as promoted type (data-kind) in
--   dependent-like contexts such as GADTs.
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 type of encoding enc and length n
BvSort :: BvEnc -> 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] :: (KnownBvEnc enc, KnownNat n) => Proxy enc -> Proxy n -> SSMTSort (BvSort enc 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 (Language.Hasmtlib.Type.Bitvec.KnownBvEnc enc, GHC.TypeNats.KnownNat n) => Language.Hasmtlib.Type.SMTSort.KnownSMTSort ('Language.Hasmtlib.Type.SMTSort.BvSort enc 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)


-- | This module provides the wrapper <a>Value</a> for embedding
--   Haskell-Values into the SMT-Context.
--   
--   The Direction <tt>Haskell-Value =&gt; SMT-Value</tt> is the creation
--   of a constant in the SMT-Problem.
--   
--   The other way around <tt>SMT-Value =&gt; Haskell-Value</tt> is mainly
--   used when decoding a solvers solutions for variables.
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] :: (KnownBvEnc enc, KnownNat n) => HaskellType (BvSort enc n) -> Value (BvSort enc 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
instance (Language.Hasmtlib.Type.SMTSort.KnownSMTSort t, GHC.Num.Num (Language.Hasmtlib.Type.SMTSort.HaskellType t)) => GHC.Num.Num (Language.Hasmtlib.Type.Value.Value t)
instance GHC.Real.Fractional (Language.Hasmtlib.Type.Value.Value 'Language.Hasmtlib.Type.SMTSort.RealSort)
instance Language.Hasmtlib.Boolean.Boolean (Language.Hasmtlib.Type.Value.Value 'Language.Hasmtlib.Type.SMTSort.BoolSort)


-- | This module provides the data-type <a>Expr</a>.
--   
--   It represents SMTLib-expressions via an abstract syntax tree (AST),
--   implemented as GADT.
--   
--   Variables are just <a>Int</a>s wrapped in a newtype <a>SMTVar</a> with
--   a phantom-type <a>SMTSort</a>.
--   
--   Usually the end user of this library does not need to deal with this
--   representation. Instead he should rely on the provided instances for
--   building expressions. Some of the main classes of these include:
--   
--   <ol>
--   <li><a>Equatable</a> and <a>Orderable</a> for symbolic
--   comparisons,</li>
--   <li><a>Iteable</a> for symbolic branching via <a>ite</a>,</li>
--   <li><a>Boolean</a> for symbolic bool operations,</li>
--   <li>Prelude classics like: <a>Num</a>, <a>Floating</a>,
--   <a>Integral</a>, <a>Bounded</a>, ... for arithmetics</li>
--   <li><a>Bits</a> for BitVec-operations</li>
--   </ol>
--   
--   Besides that, there are also some operations defined by the
--   SMTLib-Standard Version 2.6 that do not fit into any classes and
--   therefore are exported as plain functions, like <a>for_all</a> or
--   <a>bvConcat</a>.
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_awiz t_axe5. Iso (SMTVar t_awiz) (SMTVar t_axe5) Int Int

-- | An SMT-Expression. For building expressions use the corresponding
--   instances.
--   
--   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
[Rem] :: 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] :: (KnownBvEnc enc, KnownNat n) => Expr (BvSort enc n) -> Expr (BvSort enc n) -> Expr (BvSort enc n)
[BvNor] :: (KnownBvEnc enc, KnownNat n) => Expr (BvSort enc n) -> Expr (BvSort enc n) -> Expr (BvSort enc n)
[BvShL] :: (KnownBvEnc enc, KnownNat n) => Expr (BvSort enc n) -> Expr (BvSort enc n) -> Expr (BvSort enc n)
[BvLShR] :: KnownNat n => Expr (BvSort Unsigned n) -> Expr (BvSort Unsigned n) -> Expr (BvSort Unsigned n)
[BvAShR] :: KnownNat n => Expr (BvSort Signed n) -> Expr (BvSort Signed n) -> Expr (BvSort Signed n)
[BvConcat] :: (KnownBvEnc enc, KnownNat n, KnownNat m) => Expr (BvSort enc n) -> Expr (BvSort enc m) -> Expr (BvSort enc (n + m))
[BvRotL] :: (KnownBvEnc enc, KnownNat n, Integral a) => a -> Expr (BvSort enc n) -> Expr (BvSort enc n)
[BvRotR] :: (KnownBvEnc enc, KnownNat n, Integral a) => a -> Expr (BvSort enc n) -> Expr (BvSort enc 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
[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

-- | Indicates whether an expression is a leaf. All non-recursive
--   contructors are leafs.
isLeaf :: Expr t -> Bool

-- | Symbolically test two values on equality.
--   
--   A generic default implementation with <a>GEquatable</a> is possible.
--   
--   <h4><b>Example</b></h4>
--   
--   <pre>
--   x &lt;- var @RealType
--   y &lt;- var
--   assert $ y === x &amp;&amp; not (y /== x) &amp;&amp; x === 42
--   </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 /==

-- | Symbolically test multiple expressions on equality.
--   
--   Returns <a>true</a> if given less than two arguments.
equal :: (Eq (HaskellType t), KnownSMTSort t, Foldable f) => f (Expr t) -> Expr BoolSort

-- | Symbolically test multiple expressions on distinctness.
--   
--   Returns <a>true</a> if given less than two arguments.
distinct :: (Eq (HaskellType t), KnownSMTSort t, Foldable f) => f (Expr t) -> Expr BoolSort
class GEquatable f
(===#) :: GEquatable f => f a -> f a -> Expr BoolSort

-- | Symbolically compare two values.
--   
--   A generic default implementation with <a>GOrderable</a> is possible.
--   
--   <h4><b>Example</b></h4>
--   
--   <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 >?

-- | Symbolic evaluation of the minimum of two symbolic values.
min' :: (Orderable a, Iteable (Expr BoolSort) a) => a -> a -> a

-- | Symbolic evaluation of the maximum of two symbolic values.
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

-- | Class that allows branching on predicates of type <tt>b</tt> on
--   branches of type <tt>a</tt>.
--   
--   If predicate (p :: b) then (t :: a) else (f :: a).
--   
--   There is a default implementation if your type is an
--   <a>Applicative</a>.
--   
--   <h4><b>Examples</b></h4>
--   
--   <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

-- | Universal quantification for any specific <a>SMTSort</a>.
--   
--   <h4><b>Example</b></h4>
--   
--   <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

-- | Existential quantification for any specific <a>SMTSort</a>
--   
--   <h4><b>Example</b></h4>
--   
--   <pre>
--   assert $
--      for_all @(BvSort Unsigned 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

-- | Concats two bitvectors.
bvConcat :: (KnownBvEnc enc, KnownNat n, KnownNat m) => Expr (BvSort enc n) -> Expr (BvSort enc m) -> Expr (BvSort enc (n + m))

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

-- | 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>(strPrefixof 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>(strSuffixof 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>(strContains 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>(strIndexof 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>(strReplace 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>(strReplaceAll 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

-- | 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
instance (Language.Hasmtlib.Type.SMTSort.KnownSMTSort t, GHC.Classes.Ord (Language.Hasmtlib.Type.SMTSort.HaskellType t)) => Language.Hasmtlib.Type.Expr.Orderable (Language.Hasmtlib.Type.Expr.Expr t)
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 (Language.Hasmtlib.Type.SMTSort.KnownSMTSort t, GHC.Num.Num (Language.Hasmtlib.Type.SMTSort.HaskellType t), GHC.Classes.Ord (Language.Hasmtlib.Type.SMTSort.HaskellType t)) => GHC.Num.Num (Language.Hasmtlib.Type.Expr.Expr t)
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.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 (Language.Hasmtlib.Type.SMTSort.KnownSMTSort t, GHC.Real.Real (Language.Hasmtlib.Type.SMTSort.HaskellType t)) => GHC.Real.Real (Language.Hasmtlib.Type.Expr.Expr t)
instance (Language.Hasmtlib.Type.SMTSort.KnownSMTSort t, GHC.Enum.Enum (Language.Hasmtlib.Type.SMTSort.HaskellType t)) => GHC.Enum.Enum (Language.Hasmtlib.Type.Expr.Expr t)
instance (Language.Hasmtlib.Type.SMTSort.KnownSMTSort t, GHC.Real.Integral (Language.Hasmtlib.Type.SMTSort.HaskellType t)) => GHC.Real.Integral (Language.Hasmtlib.Type.Expr.Expr t)
instance (Language.Hasmtlib.Type.Bitvec.KnownBvEnc enc, GHC.TypeNats.KnownNat n) => Language.Hasmtlib.Boolean.Boolean (Language.Hasmtlib.Type.Expr.Expr ('Language.Hasmtlib.Type.SMTSort.BvSort enc n))
instance GHC.Enum.Bounded (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort)
instance (Language.Hasmtlib.Type.Bitvec.KnownBvEnc enc, GHC.TypeNats.KnownNat n) => GHC.Enum.Bounded (Language.Hasmtlib.Type.Expr.Expr ('Language.Hasmtlib.Type.SMTSort.BvSort enc n))
instance GHC.Bits.Bits (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort)
instance (Language.Hasmtlib.Type.Bitvec.KnownBvEnc enc, GHC.TypeNats.KnownNat n) => GHC.Bits.Bits (Language.Hasmtlib.Type.Expr.Expr ('Language.Hasmtlib.Type.SMTSort.BvSort enc 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)


-- | This module provides the types <a>Solution</a> and <a>Result</a>.
--   
--   External SMT-Solvers responses are parsed into these types.
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
type Solution = DMap SSMTSort IntValueMap

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

-- | 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_a1dOP. Lens' (SMTVarSol t_a1dOP) (SMTVar t_a1dOP)
solVal :: forall t_a1dOP. Lens' (SMTVarSol t_a1dOP) (Value t_a1dOP)
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)


-- | This module provides functions for counting symbolic formulas and
--   creating cardinality-constraints.
--   
--   Internally this converts each given <a>Expr</a> <a>BoolSort</a> into a
--   numerical <a>Expr</a> using <a>ite</a>, then sums them up:
--   
--   <pre>
--   count :: forall t f. (Functor f, Foldable f, Num (Expr t)) =&gt; f (Expr BoolSort) -&gt; Expr t
--   count = sum . fmap (\b -&gt; ite b 1 0)
--   </pre>
--   
--   Therefore additional information for the temporal summation may need
--   to be provided.
--   
--   E.g. if your logic is "QF_LIA" you would want <tt>count @IntSort $
--   ...</tt>
module Language.Hasmtlib.Counting

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

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

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


-- | This module provides the class <a>Codec</a> which takes care of
--   marshalling data to and from external SMT-Solvers.
--   
--   A generic default implementation with <a>GCodec</a> is possible.
--   
--   <h4><b>Example</b></h4>
--   
--   <pre>
--   data V3 a = V3 a a a deriving Generic
--   instance Codec a =&gt; Codec (V3 a)
--   
--   constantV3 :: V3 (Expr RealSort)
--   constantV3 = encode $ V3 7 69 42
--   </pre>
module Language.Hasmtlib.Codec

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

-- | Computes a default <a>Decoded</a> <a>Type</a> by distributing
--   <a>Decoded</a> over it's type arguments.
type family DefaultDecoded a :: Type
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 (GHC.Ix.Ix i, Language.Hasmtlib.Codec.Codec e) => Language.Hasmtlib.Codec.Codec (GHC.Arr.Array i e)
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)


-- | This module provides MTL-Style-classes for building SMT-problems.
--   
--   The following three classes form the core of this module:
--   
--   <ol>
--   <li><a>MonadSMT</a> for plain SMT-problems. Create variables using
--   <a>var</a> and assert formulas via <a>assert</a>.</li>
--   <li><a>MonadIncrSMT</a> for plain SMT-problems with addtional access
--   to the external solvers incremental stack and it's operations.</li>
--   <li><a>MonadOMT</a> for SMT-problems with optimization. Optimize via
--   <a>minimize</a> and <a>maximize</a> and softly assert formulas via
--   <a>assertSoft</a>.</li>
--   </ol>
module Language.Hasmtlib.Type.MonadSMT

-- | A <a>MonadState</a> that holds an SMT-Problem.
--   
--   <h4><b>Example</b></h4>
--   
--   <pre>
--   problem :: MonadSMT s m =&gt; StateT s m (Expr IntSort)
--   problem = do
--     setLogic "QF_LIA"
--     x &lt;- var @IntSort
--     assert $ x + 2 === x * 2
--     return x
--   </pre>
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.
smtvar' :: forall t. (MonadSMT s m, KnownSMTSort t) => Proxy t -> m (SMTVar t)

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

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

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

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

-- | Wrapper for <a>var'</a> which hides the <a>Proxy</a>.
--   
--   <h4><b>Example</b></h4>
--   
--   <pre>
--   x &lt;- var @BoolSort
--   </pre>
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.
--   
--   <h4><b>Examples</b></h4>
--   
--   <pre>
--   &gt;&gt;&gt; constant True
--       Constant (BoolValue True)
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; constant (10 :: Integer)
--       Constant (IntValue 10)
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; constant @RealSort 5
--       Constant (RealValue 5.0)
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; constant @(BvSort Unsigned 8) 14
--       Constant (BvValue 00001110)
--   </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.
--   
--   Quantifies bottom-up.
--   
--   This is intended for internal use. Usually before rendering an assert.
quantify :: MonadSMT s m => KnownSMTSort t => Expr t -> m (Expr t)

-- | A <a>MonadSMT</a> that addtionally allows incremental solving with
--   access to a solvers incremental stack.
--   
--   Some solvers require to have <a>SMTOption</a> <a>Incremental</a> set
--   first.
--   
--   <h4><b>Example</b></h4>
--   
--   <pre>
--   problem :: MonadIncrSMT s m =&gt; StateT s m ()
--   problem = do
--     setOption $ Incremental True
--     setLogic "QF_LIA"
--     x &lt;- var @IntSort
--     push
--     assert $ x + 2 === x * 2
--     res &lt;- checkSat
--     case res of
--       Sat -&gt; do
--         x' &lt;- getValue x
--         ...
--       _ -&gt; pop ...
--     return ()
--   </pre>
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 <tt>check-sat</tt> 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.
--   
--   <h4><b>Example</b></h4>
--   
--   <pre>
--   x &lt;- var @RealSort
--   y &lt;- var
--   assert $ x &gt;? y &amp;&amp; y &lt;? (-1)
--   res &lt;- checkSat
--   case res of
--     Sat -&gt; do
--       model &lt;- getModel
--       liftIO $ print $ decode model x
--     r -&gt; print $ show r &lt;&gt; ": Cannot get model."
--   </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.
--   
--   <h4><b>Example</b></h4>
--   
--   <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.
--   
--   <h4><b>Example</b></h4>
--   
--   <pre>
--   x &lt;- var @BoolSort
--   assert $ x <tt>xor</tt> false
--   (res, sol) &lt;- solve
--   case res of
--     Sat -&gt; do
--       x' &lt;- getValue x
--       liftIO $ print $ decode sol x
--     r -&gt; print r
--   </pre>
solve :: (MonadIncrSMT s m, MonadIO m) => m (Result, Solution)

-- | A <a>MonadSMT</a> that addtionally allows optimization targets.
--   
--   <h4><b>Example</b></h4>
--   
--   <pre>
--   problem :: MonadOMT s m =&gt; StateT s m (Expr (BvSort Unsigned 8))
--   problem = do
--     setLogic "QF_BV"
--     x &lt;- var @(BvSort Unsigned 8)
--     assertSoftWeighted (x &lt;? maxBound) 2.0
--     maximize x
--     return x
--   </pre>
class MonadSMT s m => MonadOMT s m

-- | Minimizes a numerical expression within the OMT-Problem.
--   
--   <h4><b>Example</b></h4>
--   
--   <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.
--   
--   <h4><b>Example</b></h4>
--   
--   <pre>
--   x &lt;- var @(BvSort Signed 4)
--   assert $ x &lt;? 2
--   maximize x
--   </pre>
--   
--   will give <tt>x := 0001</tt> as solution.
maximize :: (MonadOMT s m, KnownSMTSort t, Num (Expr t)) => Expr t -> m ()

-- | Softly asserts a boolean expression.
--   
--   May take a weight and an identifier for grouping.
--   
--   <h4><b>Example</b></h4>
--   
--   <pre>
--   x &lt;- var @BoolSort
--   assertSoft x (Just 0.5) (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 ()


-- | This module provides the data-type <a>Relation</a> for encoding binary
--   relations as SMT-problems.
--   
--   <h4><b>Example</b></h4>
--   
--   <pre>
--   problem :: MonadSMT s m =&gt; StateT s m (Relation Int Int)
--       setLogic "QF_LIA"
--   
--       r &lt;- relation ((2,1), (6,5))
--   
--       forM_ (image r &lt;$&gt; domain r) (assert . exactly @IntSort 1)
--       forM_ (preimage r &lt;$&gt; codomain r) (assert . exactly @IntSort 1)
--   
--       assertMaybe $ do
--         item &lt;- r^?ix (3,3)
--         return $ item === true
--   
--       return r
--   </pre>
module Language.Hasmtlib.Type.Relation

-- | <tt>Relation a b</tt> represents a binary relation &lt;math&gt;, where
--   the domain &lt;math&gt; is a finite subset of the type <tt>a</tt>, and
--   the codomain &lt;math&gt; is a finite subset of the type <tt>b</tt>.
--   
--   A relation is stored internally as <tt>Array (a,b) Expr BoolSort</tt>,
--   so <tt>a</tt> and <tt>b</tt> have to be instances of <a>Ix</a>, and
--   both &lt;math&gt; and &lt;math&gt; are intervals.
newtype Relation a b
Relation :: Array (a, b) (Expr BoolSort) -> Relation a b

-- | <tt>relation ((amin,bmin),(amax,mbax))</tt> constructs an
--   indeterminate relation &lt;math&gt; where &lt;math&gt; is <tt>{amin ..
--   amax}</tt> and &lt;math&gt; is <tt>{bmin .. bmax}</tt>.
relation :: (Ix a, Ix b, MonadSMT s m) => ((a, b), (a, b)) -> m (Relation a b)

-- | Constructs an indeterminate relation &lt;math&gt; that is symmetric,
--   i.e., &lt;math&gt;.
symmetric_relation :: (MonadSMT s m, Ix b) => ((b, b), (b, b)) -> m (Relation b b)

-- | Constructs a relation &lt;math&gt; from a list.
build :: (Ix a, Ix b) => ((a, b), (a, b)) -> [((a, b), Expr BoolSort)] -> Relation a b

-- | Constructs a relation &lt;math&gt; from a function.
buildFrom :: (Ix a, Ix b) => ((a, b), (a, b)) -> ((a, b) -> Expr BoolSort) -> Relation a b

-- | Constructs an indeterminate relation &lt;math&gt; from a function.
buildFromM :: (Ix a, Ix b, MonadSMT s m) => ((a, b), (a, b)) -> ((a, b) -> m (Expr BoolSort)) -> m (Relation a b)

-- | Constructs the identity relation &lt;math&gt;.
identity :: Ix a => ((a, a), (a, a)) -> Relation a a

-- | <a>Maybe</a> (<a>Expr</a> <a>BoolSort</a>) for a given element
--   &lt;math&gt; and a given relation &lt;math&gt; that indicates if
--   &lt;math&gt; or not.
--   
--   <a>Just</a> if given element is in <a>bounds</a> of the relation.
--   <a>Nothing</a> otherwise.
(!?) :: (Ix a, Ix b) => Relation a b -> (a, b) -> Maybe (Expr BoolSort)

-- | Unsafe version of <a>(!?)</a>. Produces an array-indexing-error if
--   given element is not within the <a>bounds</a> of the relation.
(!) :: (Ix a, Ix b) => Relation a b -> (a, b) -> Expr BoolSort

-- | The bounds of the array that correspond to the matrix representation
--   of the given relation.
bounds :: Relation a b -> ((a, b), (a, b))

-- | The list of indices, where each index represents an element
--   &lt;math&gt; that may be contained in the given relation &lt;math&gt;.
indices :: (Ix a, Ix b) => Relation a b -> [(a, b)]

-- | The list of elements of the array that correspond to the matrix
--   representation of the given relation.
elems :: Relation a b -> [Expr BoolSort]

-- | The list of tuples for the given relation &lt;math&gt;, where the
--   first element represents an element &lt;math&gt; and the second
--   element indicates via a <a>Expr</a> <a>BoolSort</a> , if &lt;math&gt;
--   or not.
assocs :: (Ix a, Ix b) => Relation a b -> [((a, b), Expr BoolSort)]

-- | The domain &lt;math&gt; of a relation &lt;math&gt;.
domain :: Ix a => Relation a b -> [a]

-- | The codomain &lt;math&gt; of a relation &lt;math&gt;.
codomain :: Ix b => Relation a b -> [b]

-- | Returns a list of <a>Expr</a> <a>BoolSort</a> indicating whether the
--   projection on given element &lt;math&gt; holds for every element in
--   the codomain:
--   
--   &lt;math&gt;
image :: (Ix a, Ix b) => Relation a b -> a -> [Expr BoolSort]

-- | Returns a list of <a>Expr</a> <a>BoolSort</a> indicating whether the
--   projection on given element &lt;math&gt; holds for every element in
--   the domain:
--   
--   &lt;math&gt;
preimage :: (Ix a, Ix b) => Relation a b -> b -> [Expr BoolSort]

-- | Print a satisfying assignment from an SMT solver, where the assignment
--   is interpreted as a relation. <tt>putStrLn $ table
--   &lt;<i>assignment</i>&gt;</tt> corresponds to the matrix
--   representation of this relation.
table :: (Ix a, Ix b) => Array (a, b) Bool -> String
instance (GHC.Ix.Ix a, GHC.Ix.Ix b, GHC.Show.Show a, GHC.Show.Show b) => GHC.Show.Show (Language.Hasmtlib.Type.Relation.Relation a b)
instance (GHC.Ix.Ix a, GHC.Ix.Ix b) => Language.Hasmtlib.Codec.Codec (Language.Hasmtlib.Type.Relation.Relation a b)
instance (GHC.Ix.Ix a, GHC.Ix.Ix b, a GHC.Types.~ c, b GHC.Types.~ d) => Control.Lens.Each.Each (Language.Hasmtlib.Type.Relation.Relation a b) (Language.Hasmtlib.Type.Relation.Relation c d) (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort) (Language.Hasmtlib.Type.Expr.Expr 'Language.Hasmtlib.Type.SMTSort.BoolSort)
instance (GHC.Ix.Ix a, GHC.Ix.Ix b) => Control.Lens.At.Ixed (Language.Hasmtlib.Type.Relation.Relation a b)

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


-- | This module provides a concrete implementation for <a>MonadSMT</a>
--   with it's state <a>SMT</a>.
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)
lastVarId :: Lens' SMT Int
vars :: Lens' SMT (Seq (SomeKnownSMTSort SMTVar))
formulas :: Lens' SMT (Seq (Expr 'BoolSort))
mlogic :: Lens' SMT (Maybe String)
options :: Lens' SMT [SMTOption]
sharingMode :: Lens' SMT SharingMode
stableMap :: Lens' SMT (HashMap (StableName ()) (SomeKnownSMTSort Expr))
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


-- | This module provides a concrete implementation for <a>MonadOMT</a>
--   with it's state <a>OMT</a>.
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

-- | 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
smt :: Lens' OMT SMT
targetMinimize :: Lens' OMT (Seq (SomeKnownSMTSort Minimize))
targetMaximize :: Lens' OMT (Seq (SomeKnownSMTSort Maximize))
softFormulas :: Lens' OMT (Seq SoftFormula)
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 :: (KnownBvEnc enc, KnownNat n) => Proxy n -> Parser (Bitvec enc n)
binBitvector :: KnownNat n => Proxy n -> Parser (Bitvec enc n)
hexBitvector :: (KnownBvEnc enc, KnownNat n) => Proxy n -> Parser (Bitvec enc n)
literalBitvector :: (KnownBvEnc enc, KnownNat n) => Proxy n -> Parser (Bitvec enc 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)


-- | This module provides an IO-<a>Pipe</a> to external SMT-Solvers and
--   ships with implementations for <a>MonadSMT</a>, <a>MonadOMT</a> and
--   <a>MonadIncrSMT</a>.
--   
--   The <a>Pipe</a> is based on a <a>Solver</a> from Tweag's package
--   <tt>smtlib-backends</tt> and in reality is just an IO-Handle.
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
lastPipeVarId :: Lens' Pipe Int
mPipeLogic :: Lens' Pipe (Maybe String)
pipeSharingMode :: Lens' Pipe SharingMode
pipeStableMap :: Lens' Pipe (HashMap (StableName ()) (SomeKnownSMTSort Expr))
incrSharedAuxs :: Lens' Pipe (Seq (Seq (StableName ())))
pipeSolver :: Lens' Pipe Solver
isDebugging :: Lens' Pipe Bool
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


-- | This module provides functions for having SMT-Problems solved by
--   external solvers.
module Language.Hasmtlib.Type.Solver

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

-- | Create a value with a <a>Solver</a> and a <a>Bool</a> 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>
--   
--   <h4><b>Example</b></h4>
--   
--   <pre>
--   import Language.Hasmtlib
--   
--   main :: IO ()
--   main = do
--     res &lt;- solveWith @SMT (solver cvc5) $ do
--       setLogic "QF_LIA"
--   
--       x &lt;- var @IntSort
--   
--       assert $ x &gt;? 0
--   
--       return x
--   
--     print res
--   </pre>
--   
--   The solver will probably answer with <tt>x := 1</tt>.
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.
--   
--   <h4><b>Example</b></h4>
--   
--   <pre>
--   import Language.Hasmtlib
--   import Control.Monad.IO.Class
--   
--   main :: IO ()
--   main = do
--     cvc5Living &lt;- interactiveSolver cvc5
--     interactiveWith @Pipe cvc5Living $ do
--       setOption $ Incremental True
--       setOption $ ProduceModels True
--       setLogic "QF_LRA"
--   
--       x &lt;- var @RealSort
--   
--       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.
--   
--   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.
--   
--   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


-- | This module handles common IO interaction with external SMT-Solvers
--   via external processes.
--   
--   It is built on top of Tweag's package <tt>smtlib-backends</tt>.
--   
--   Although there already are several concrete solvers like <tt>Z3</tt>
--   in <tt>Language.Hasmtlib.Solver.Z3</tt>, you may use this module to
--   create your own solver bindings.
module Language.Hasmtlib.Solver.Common

-- | 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,</li>
--   <li>close the process and clean up all resources and</li>
--   <li>return the decoded solution.</li>
--   </ol>
processSolver :: (RenderSeq s, MonadIO m) => Config -> Maybe (Debugger s) -> Solver s m

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

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

-- | The default value for this type.
def :: Default a => a
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)


-- | This module provides the class <a>Variable</a> which lets you create
--   symbolical values of a data-type.
--   
--   A generic default implementation with <a>GVariable</a> is possible.
--   
--   <h4><b>Example</b></h4>
--   
--   <pre>
--   data V3 a = V3 a a a deriving Generic
--   instance Codec a =&gt; Codec (V3 a)
--   instance Equatable a =&gt; Codec (V3 a)
--   
--   problem :: MonadSMT s m =&gt; StateT s m (V3 (Expr RealSort))
--   problem = do
--     let constantV3 = encode $ V3 7 69 42
--     symbolicV3 &lt;- variable @(V3 (Expr RealSort))
--     assert $ symbolicV3 /== constantV3
--     return symbolicV3
--   </pre>
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.
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 ()