-- 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.7.2
-- | This module provides a more generic version of bool-like algebras than
-- what the Prelude does for Bool.
--
-- The class Boolean therefore overloads most of the Preludes
-- operators like (&&).
--
-- However, as Bool also features an instance of Boolean,
-- you can simply hide the Prelude ones - not having to import either
-- qualified.
--
-- Example
--
--
-- import Prelude hiding (not, any, all, (&&), (||), and, or)
-- import Language.Hasmtlib
--
-- problem :: MonadSMT s m => StateT s m (Expr BoolSort, Expr BoolSort)
-- problem = do
-- x <- var @BoolSort
-- y <- var
-- let b = False || True
-- assert $ x && y <==> and [x, y, true] && encode b ==> x && y
-- return (x,y)
--
module Language.Hasmtlib.Boolean
class Boolean b
-- | Lift a Bool.
bool :: Boolean b => Bool -> b
-- | The true constant. true = bool True
true :: Boolean b => b
-- | The false constant. false = bool False
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.
--
--
-- forall x y. (x ==> y) === (y <== x)
--
(<==) :: 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.
--
--
-- nand = not . and
--
nand :: (Foldable t, Boolean b) => t b -> b
-- | The negated logical disjunction of several values.
--
--
-- nor = not . or
--
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.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)
transform1 :: (Uniplate1 f cs, AllC cs b) => (forall a. AllC cs a => f a -> f a) -> f b -> 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)
-- | This module provides a class ArrayMap and a concrete
-- implementation with ConstArray 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:
--
--
-- - forall A i x: arrSelect (arrStore i x) == x
-- - forall A i j x: i /= j ==> (arrSelect (arrStore i x) j ===
-- arrSelect A j)
--
class ArrayMap f k v
-- | Construct an ArrayMap via it's const value.
asConst' :: ArrayMap f k v => Proxy f -> Proxy k -> v -> f k v
-- | View the const value of the ArrayMap.
viewConst :: ArrayMap f k v => f k v -> v
-- | Select a value from the ArrayMap.
--
-- 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 ArrayMap.
arrStore :: ArrayMap f k v => f k v -> k -> v -> f k v
-- | Wrapper for asConst' which hides the Proxy.
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_adQ6 v_adQ7. Lens' (ConstArray k_adQ6 v_adQ7) v_adQ7
stored :: forall k_adQ6 v_adQ7 k_afpM. Lens (ConstArray k_adQ6 v_adQ7) (ConstArray k_afpM v_adQ7) (Map k_adQ6 v_adQ7) (Map k_afpM v_adQ7)
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 Bitvec built on top of the package bitvec
-- and Vector.
--
-- It also holds it's type of encoding as a phantom-type via
-- BvEnc.
--
-- Examples
--
--
-- >>> minBound @(Bitvec Unsigned 8)
-- 00000000
--
--
--
-- >>> maxBound @(Bitvec Signed 8)
-- 01111111
--
--
--
-- >>> (5 :: Bitvec Unsigned 4) + 10
-- 1111
--
module Language.Hasmtlib.Type.Bitvec
-- | Type of Bitvector encoding - used as promoted type (data-kind).
data BvEnc
Unsigned :: BvEnc
Signed :: BvEnc
-- | Singleton for BvEnc.
data SBvEnc (enc :: BvEnc)
[SUnsigned] :: SBvEnc Unsigned
[SSigned] :: SBvEnc Signed
-- | Compute singleton SBvEnc from it's promoted type BvEnc.
class KnownBvEnc (enc :: BvEnc)
bvEncSing :: KnownBvEnc enc => SBvEnc enc
-- | Wrapper for bvEncSing which takes a Proxy.
bvEncSing' :: forall enc prxy. KnownBvEnc enc => prxy enc -> SBvEnc enc
-- | Wrapper for bvEncSing which takes a Proxy and some
-- ballast. This is helpful for singing on values of type Bitvec
-- where the ballst is a Nat.
bvEncSing'' :: forall enc a prxy. KnownBvEnc enc => prxy enc a -> SBvEnc enc
-- | Length-indexed bitvector (Vector) carrying a phantom type-level
-- BvEnc.
--
-- 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 Bitvec with any encoding BvEnc to
-- Unsigned.
asUnsigned :: forall enc n. Bitvec enc n -> Bitvec Unsigned n
-- | Convert Bitvec with any encoding BvEnc to Signed.
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
-- Proxy.
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.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 SMTOption 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
-- | This module provides the data-type SMTSort and some
-- singleton-operations for it.
--
-- The type SMTSort 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 Type of an
-- SMTSort.
type family HaskellType (t :: SMTSort) = (r :: Type) | r -> t
-- | Singleton for SMTSort.
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 SSMTSort from it's promoted type
-- SMTSort.
class KnownSMTSort (t :: SMTSort)
sortSing :: KnownSMTSort t => SSMTSort t
-- | Wrapper for sortSing which takes a Proxy.
sortSing' :: forall prxy t. KnownSMTSort t => prxy t -> SSMTSort t
-- | An existential wrapper that hides some known SMTSort.
type SomeKnownSMTSort f = Some1 ((~) f) KnownSMTSort
instance GHC.Show.Show (Language.Hasmtlib.Type.SMTSort.SSMTSort t)
instance GHC.Classes.Eq (Language.Hasmtlib.Type.SMTSort.SSMTSort t)
instance GHC.Classes.Ord (Language.Hasmtlib.Type.SMTSort.SSMTSort t)
instance Data.GADT.Internal.GEq Language.Hasmtlib.Type.SMTSort.SSMTSort
instance Data.GADT.Internal.GCompare Language.Hasmtlib.Type.SMTSort.SSMTSort
instance Language.Hasmtlib.Type.SMTSort.KnownSMTSort 'Language.Hasmtlib.Type.SMTSort.IntSort
instance Language.Hasmtlib.Type.SMTSort.KnownSMTSort 'Language.Hasmtlib.Type.SMTSort.RealSort
instance Language.Hasmtlib.Type.SMTSort.KnownSMTSort 'Language.Hasmtlib.Type.SMTSort.BoolSort
instance (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
-- | This module provides the wrapper Value for embedding
-- Haskell-Values into the SMT-Context.
--
-- The Direction Haskell-Value => SMT-Value is the creation
-- of a constant in the SMT-Problem.
--
-- The other way around SMT-Value => Haskell-Value is mainly
-- used when decoding a solvers solutions for variables.
module Language.Hasmtlib.Type.Value
-- | A wrapper for values of SMTSorts. 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-Value.
wrapValue :: forall t. KnownSMTSort t => HaskellType t -> Value t
-- | Unwraps a Haskell-value from the SMT-Context-Value.
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 Expr.
--
-- It represents SMTLib-expressions via an abstract syntax tree (AST),
-- implemented as GADT.
--
-- Variables are just Ints wrapped in a newtype SMTVar with
-- a phantom-type SMTSort.
--
-- 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:
--
--
-- - Equatable and Orderable for symbolic
-- comparisons,
-- - Iteable for symbolic branching via ite,
-- - Boolean for symbolic bool operations,
-- - Prelude classics like: Num, Floating,
-- Integral, Bounded, ... for arithmetics
-- - Bits for BitVec-operations
--
--
-- 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 for_all or
-- bvConcat.
module Language.Hasmtlib.Type.Expr
-- | An internal SMT variable with a phantom-type which holds an Int
-- as it's identifier.
newtype SMTVar (t :: SMTSort)
SMTVar :: Int -> SMTVar (t :: SMTSort)
[_varId] :: SMTVar (t :: SMTSort) -> Int
varId :: forall t_av3c t_avYL. Iso (SMTVar t_av3c) (SMTVar t_avYL) 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
-- | Size of the expression.
--
-- Counts the amount of operations.
--
-- Examples
--
--
-- >>> nodeSize $ x + y === x + y
-- 3
--
-- >>> nodeSize $ false
-- 0
--
exprSize :: KnownSMTSort t => Expr t -> Integer
-- | Symbolically test two values on equality.
--
-- A generic default implementation with GEquatable is possible.
--
-- Example
--
--
-- x <- var @RealType
-- y <- var
-- assert $ y === x && not (y /== x) && x === 42
--
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 true 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 true 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 GOrderable is possible.
--
-- Example
--
--
-- x <- var @RealSort
-- y <- var
-- assert $ x >? y
-- assert $ x === min' 42 100
--
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
( a -> a -> Expr BoolSort
(>?) :: Orderable a => a -> a -> Expr BoolSort
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
( f a -> f a -> Expr BoolSort
(<=?#) :: GOrderable f => f a -> f a -> Expr BoolSort
-- | Class that allows branching on predicates of type b on
-- branches of type a.
--
-- If predicate (p :: b) then (t :: a) else (f :: a).
--
-- There is a default implementation if your type is an
-- Applicative.
--
-- Examples
--
--
-- >>> ite True "1" "2"
-- "1"
--
-- >>> ite False 100 42
-- 42
--
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 SMTSort.
--
-- Example
--
--
-- assert $
-- for_all @IntSort $ x ->
-- x + 0 === x && 0 + x === x
--
--
--
-- The lambdas x 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 SMTSort
--
-- Example
--
--
-- assert $
-- for_all @(BvSort Unsigned 8) $ x ->
-- exists $ y ->
-- x - y === 0
--
--
--
-- The lambdas y 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
-- | (strSubstring s i n) evaluates to the longest (unscattered)
-- substring of s of length at most n starting at
-- position i. It evaluates to the empty string if n is
-- negative or i is not in the interval [0,l-1] where
-- l is the length of s.
strSubstring :: Expr StringSort -> Expr IntSort -> Expr IntSort -> Expr StringSort
-- | First string is a prefix of second one. (strPrefixof s t) is
-- true iff s is a prefix of t.
strPrefixOf :: Expr StringSort -> Expr StringSort -> Expr BoolSort
-- | First string is a suffix of second one. (strSuffixof s t) is
-- true iff s is a suffix of t.
strSuffixOf :: Expr StringSort -> Expr StringSort -> Expr BoolSort
-- | First string contains second one (strContains s t) iff
-- s contains t.
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. (strIndexof s t
-- i), with 0 <= i <= |s| is the position of the
-- first occurrence of t in s at or after position
-- i, if any. Otherwise, it is -1. Note that the result
-- is i whenever i is within the range [0,
-- |s|] and t is empty.
strIndexOf :: Expr StringSort -> Expr StringSort -> Expr IntSort -> Expr IntSort
-- | (strReplace s t t') is the string obtained by replacing the
-- first occurrence of t in s, if any, by t'.
-- Note that if t is empty, the result is to prepend t'
-- to s; also, if t does not occur in s then
-- the result is s.
strReplace :: Expr StringSort -> Expr StringSort -> Expr StringSort -> Expr StringSort
-- | (strReplaceAll s t t’) is s if t is the
-- empty string. Otherwise, it is the string obtained from s by
-- replacing all occurrences of t in s by t’,
-- 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 IntSort to type RealSort.
toRealSort :: Expr IntSort -> Expr RealSort
-- | Converts an expression of type RealSort to type IntSort.
toIntSort :: Expr RealSort -> Expr IntSort
-- | Checks whether an expression of type RealSort may be safely
-- converted to type IntSort.
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 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 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 Solution and Result.
--
-- External SMT-Solvers responses are parsed into these types.
module Language.Hasmtlib.Type.Solution
-- | Results of check-sat commands.
data Result
Unsat :: Result
Unknown :: Result
Sat :: Result
type Solution = DMap SSMTSort IntValueMap
-- | Alias class for constraint Ord (HaskellType t)
class Ord (HaskellType t) => OrdHaskellType t
-- | An existential wrapper that hides some known SMTSort with an
-- Ord HaskellType
type SomeKnownOrdSMTSort f = Somes1 '[(~) f] '[KnownSMTSort, OrdHaskellType]
-- | Create a Solution from some SMTVarSols.
fromSomeVarSols :: [SomeKnownOrdSMTSort SMTVarSol] -> Solution
-- | Newtype for IntMap Value so we can use it as
-- right-hand-side of DMap.
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_a196j. Lens' (SMTVarSol t_a196j) (SMTVar t_a196j)
solVal :: forall t_a196j. Lens' (SMTVarSol t_a196j) (Value t_a196j)
instance GHC.Show.Show (Language.Hasmtlib.Type.Value.Value t) => GHC.Show.Show (Language.Hasmtlib.Type.Solution.SMTVarSol t)
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.Value.Value t) => GHC.Show.Show (Language.Hasmtlib.Type.Solution.IntValueMap t)
-- | This module provides functions for counting symbolic formulas and
-- creating cardinality-constraints.
--
-- Internally this converts each given Expr BoolSort into a
-- numerical Expr using ite, then sums them up:
--
--
-- count :: forall t f. (Functor f, Foldable f, Num (Expr t)) => f (Expr BoolSort) -> Expr t
-- count = sum . fmap (\b -> ite b 1 0)
--
--
-- Therefore additional information for the temporal summation may need
-- to be provided.
--
-- E.g. if your logic is "QF_LIA" you would want count'
-- @IntSort $ ...
--
-- It is worth noting that some cardinality constraints use optimized
-- encodings for special cases.
module Language.Hasmtlib.Counting
-- | Out of many bool-expressions build a formula which encodes how many of
-- them are true.
count :: forall t f. (Functor f, Foldable f, Num (Expr t)) => f (Expr BoolSort) -> Expr t
-- | Wrapper for count which takes a Proxy.
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 at
-- least k of them are true.
--
-- atLeast is defined as follows:
--
--
-- atLeast 0 = const true
-- atLeast 1 = or
-- atLeast k = (>=? k) . count
--
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
-- exactly k of them are true.
--
-- exactly is defined as follows:
--
--
-- exactly 0 xs = nand xs
-- exactly 1 xs = atLeast @t 1 xs && atMost @t 1 xs
-- exactly k xs = count xs === k
--
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 at
-- most k of them are true.
--
-- atMost is defined as follows:
--
--
-- atMost 0 = nand
-- atMost 1 = amoSqrt
-- atMost k = (<=? k) . count
--
atMost :: forall t f. (Functor f, Foldable f, Num (Expr t), Orderable (Expr t)) => Expr t -> f (Expr BoolSort) -> Expr BoolSort
-- | The squareroot-encoding, also called product-encoding, is a special
-- encoding for atMost 1.
--
-- The original product-encoding provided by Jingchao Chen in A
-- New SAT Encoding of the At-Most-One Constraint (2010) used
-- auxiliary variables and would therefore be monadic. It requires
-- <math> auxiliary variables and <math> clauses.
--
-- To make this encoding pure, all auxiliary variables are replaced with
-- a disjunction of size <math>. Therefore zero auxiliary variables
-- are required and technically clause-count remains the same, although
-- the clauses get bigger.
amoSqrt :: (Foldable f, Boolean b) => f b -> b
-- | The quadratic-encoding, also called pairwise-encoding, is a special
-- encoding for atMost 1.
--
-- It's the naive encoding for the at-most-one-constraint and produces
-- <math> clauses and no auxiliary variables..
amoQuad :: Boolean b => [b] -> b
-- | This module provides the class Codec which takes care of
-- marshalling data to and from external SMT-Solvers.
--
-- A generic default implementation with GCodec is possible.
--
-- Example
--
--
-- data V3 a = V3 a a a deriving Generic
-- instance Codec a => Codec (V3 a)
--
-- constantV3 :: V3 (Expr RealSort)
-- constantV3 = encode $ V3 7 69 42
--
module Language.Hasmtlib.Codec
-- | Lift values to SMT-Values or decode them.
--
-- You can derive an instance of this class if your type is
-- Generic.
class Codec a where {
-- | Result of decoding a.
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 Decoded Type by distributing
-- Decoded 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 GHC.Types.Int
instance Language.Hasmtlib.Codec.Codec GHC.Num.Integer.Integer
instance Language.Hasmtlib.Codec.Codec GHC.Num.Natural.Natural
instance Language.Hasmtlib.Codec.Codec GHC.Types.Word
instance Language.Hasmtlib.Codec.Codec GHC.Word.Word8
instance Language.Hasmtlib.Codec.Codec GHC.Word.Word16
instance Language.Hasmtlib.Codec.Codec GHC.Word.Word32
instance Language.Hasmtlib.Codec.Codec GHC.Word.Word64
instance Language.Hasmtlib.Codec.Codec GHC.Int.Int8
instance Language.Hasmtlib.Codec.Codec GHC.Int.Int16
instance Language.Hasmtlib.Codec.Codec GHC.Int.Int32
instance Language.Hasmtlib.Codec.Codec GHC.Int.Int64
instance Language.Hasmtlib.Codec.Codec GHC.Types.Char
instance Language.Hasmtlib.Codec.Codec GHC.Types.Float
instance Language.Hasmtlib.Codec.Codec GHC.Types.Double
instance Language.Hasmtlib.Codec.Codec GHC.Types.Ordering
instance Language.Hasmtlib.Codec.Codec GHC.Types.Bool
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:
--
--
-- - MonadSMT for plain SMT-problems. Create variables using
-- var and assert formulas via assert.
-- - MonadIncrSMT for plain SMT-problems with addtional access
-- to the external solvers incremental stack and it's operations.
-- - MonadOMT for SMT-problems with optimization. Optimize via
-- minimize and maximize and softly assert formulas via
-- assertSoft.
--
module Language.Hasmtlib.Type.MonadSMT
-- | A MonadState that holds an SMT-Problem.
--
-- Example
--
--
-- problem :: MonadSMT s m => StateT s m (Expr IntSort)
-- problem = do
-- setLogic "QF_LIA"
-- x <- var @IntSort
-- assert $ x + 2 === x * 2
-- return x
--
class MonadState s m => MonadSMT s m
-- | Construct a variable. This is mainly intended for internal use. In the
-- API use var' instead.
smtvar' :: forall t. (MonadSMT s m, KnownSMTSort t) => Proxy t -> m (SMTVar t)
-- | Construct a variable as expression.
--
-- Example
--
--
-- x <- var' (Proxy @RealType)
--
var' :: forall t. (MonadSMT s m, KnownSMTSort t) => Proxy t -> m (Expr t)
-- | Assert a boolean expression.
--
-- Example
--
--
-- x <- var @IntType
-- assert $ x - 27 === 42
--
assert :: MonadSMT s m => Expr BoolSort -> m ()
-- | Set an SMT-Solver-Option.
--
-- Example
--
--
-- setOption $ Incremental True
--
setOption :: MonadSMT s m => SMTOption -> m ()
-- | Set the logic for the SMT-Solver to use.
--
-- Example
--
--
-- setLogic "QF_LRA"
--
setLogic :: MonadSMT s m => String -> m ()
-- | Wrapper for var' which hides the Proxy.
--
-- Example
--
--
-- x <- var @BoolSort
--
var :: forall t s m. (KnownSMTSort t, MonadSMT s m) => m (Expr t)
-- | Wrapper for smtvar' which hides the Proxy. This is
-- mainly intended for internal use. In the API use var instead.
smtvar :: forall t s m. (KnownSMTSort t, MonadSMT s m) => m (SMTVar t)
-- | Create a constant.
--
-- Examples
--
--
-- >>> constant True
-- Constant (BoolValue True)
--
--
--
-- >>> constant (10 :: Integer)
-- Constant (IntValue 10)
--
--
--
-- >>> constant @RealSort 5
-- Constant (RealValue 5.0)
--
--
--
-- >>> constant @(BvSort Unsigned 8) 14
-- Constant (BvValue 00001110)
--
constant :: KnownSMTSort t => HaskellType t -> Expr t
-- | Maybe assert a boolean expression.
--
-- Asserts given expression if Maybe is a Just. 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 MonadSMT that addtionally allows incremental solving with
-- access to a solvers incremental stack.
--
-- Some solvers require to have SMTOption Incremental set
-- first.
--
-- Example
--
--
-- problem :: MonadIncrSMT s m => StateT s m ()
-- problem = do
-- setOption $ Incremental True
-- setLogic "QF_LIA"
-- x <- var @IntSort
-- push
-- assert $ x + 2 === x * 2
-- res <- checkSat
-- case res of
-- Sat -> do
-- x' <- getValue x
-- ...
-- _ -> pop ...
-- return ()
--
class MonadSMT s m => MonadIncrSMT s m
-- | Push a new context (one) to the solvers context-stack.
push :: MonadIncrSMT s m => m ()
-- | Pop the solvers context-stack by one.
pop :: MonadIncrSMT s m => m ()
-- | Run check-sat on the current problem.
checkSat :: MonadIncrSMT s m => m Result
-- | Run get-model on the current problem. This can be used to decode
-- temporary models within the SMT-Problem.
--
-- Example
--
--
-- x <- var @RealSort
-- y <- var
-- assert $ x >? y && y <? (-1)
-- res <- checkSat
-- case res of
-- Sat -> do
-- model <- getModel
-- liftIO $ print $ decode model x
-- r -> print $ show r <> ": Cannot get model."
--
getModel :: MonadIncrSMT s m => m Solution
-- | Evaluate any expressions value in the solvers model. Requires a
-- Sat or Unknown check-sat response beforehand.
--
-- Example
--
--
-- x <- var @RealSort
-- assert $ x >? 10
-- res <- checkSat
-- case res of
-- Unsat -> print "Unsat. Cannot get value for x."
-- r -> do
-- x' <- getValue x
-- liftIO $ print $ show r ++ ": x = " ++ show x'
--
getValue :: (MonadIncrSMT s m, KnownSMTSort t) => Expr t -> m (Maybe (Decoded (Expr t)))
-- | First run checkSat and then getModel on the current
-- problem.
--
-- Example
--
--
-- x <- var @BoolSort
-- assert $ x xor false
-- (res, sol) <- solve
-- case res of
-- Sat -> do
-- liftIO $ print $ decode sol x
-- r -> print r
--
solve :: (MonadIncrSMT s m, MonadIO m) => m (Result, Solution)
-- | A MonadSMT that addtionally allows optimization targets.
--
-- Example
--
--
-- problem :: MonadOMT s m => StateT s m (Expr (BvSort Unsigned 8))
-- problem = do
-- setLogic "QF_BV"
-- x <- var @(BvSort Unsigned 8)
-- assertSoftWeighted (x <? maxBound) 2.0
-- maximize x
-- return x
--
class MonadSMT s m => MonadOMT s m
-- | Minimizes a numerical expression within the OMT-Problem.
--
-- Example
--
--
-- x <- var @IntSort
-- assert $ x >? -2
-- minimize x
--
--
-- will give x := -1 as solution.
minimize :: (MonadOMT s m, KnownSMTSort t, Num (Expr t)) => Expr t -> m ()
-- | Maximizes a numerical expression within the OMT-Problem.
--
-- Example
--
--
-- x <- var @(BvSort Signed 4)
-- assert $ x <? 2
-- maximize x
--
--
-- will give x := 0001 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.
--
-- Example
--
--
-- x <- var @BoolSort
-- assertSoft x (Just 0.5) (Just "myId")
--
assertSoft :: MonadOMT s m => Expr BoolSort -> Maybe Double -> Maybe String -> m ()
-- | Like assertSoft but forces a weight and omits the group-id.
assertSoftWeighted :: MonadOMT s m => Expr BoolSort -> Double -> m ()
-- | This module provides the data-type Relation for encoding binary
-- relations as SMT-problems.
--
-- Example
--
--
-- problem :: MonadSMT s m => StateT s m (Relation Int Int)
-- setLogic "QF_LIA"
--
-- r <- relation ((2,1), (6,5))
--
-- forM_ (image r <$> domain r) (assert . exactly @IntSort 1)
-- forM_ (preimage r <$> codomain r) (assert . exactly @IntSort 1)
--
-- assertMaybe $ do
-- item <- r^?ix (3,3)
-- return $ item === true
--
-- return r
--
module Language.Hasmtlib.Type.Relation
-- | Relation a b represents a binary relation <math>, where
-- the domain <math> is a finite subset of the type a, and
-- the codomain <math> is a finite subset of the type b.
--
-- A relation is stored internally as Array (a,b) Expr BoolSort,
-- so a and b have to be instances of Ix, and
-- both <math> and <math> are intervals.
newtype Relation a b
Relation :: Array (a, b) (Expr BoolSort) -> Relation a b
-- | relation ((amin,bmin),(amax,mbax)) constructs an
-- indeterminate relation <math> where <math> is {amin ..
-- amax} and <math> is {bmin .. bmax}.
relation :: (Ix a, Ix b, MonadSMT s m) => ((a, b), (a, b)) -> m (Relation a b)
-- | Constructs an indeterminate relation <math> that is symmetric,
-- i.e., <math>.
symmetric_relation :: (MonadSMT s m, Ix b) => ((b, b), (b, b)) -> m (Relation b b)
-- | Constructs a relation <math> from a list.
build :: (Ix a, Ix b) => ((a, b), (a, b)) -> [((a, b), Expr BoolSort)] -> Relation a b
-- | Constructs a relation <math> from a function.
buildFrom :: (Ix a, Ix b) => ((a, b), (a, b)) -> ((a, b) -> Expr BoolSort) -> Relation a b
-- | Constructs an indeterminate relation <math> 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 <math>.
identity :: Ix a => ((a, a), (a, a)) -> Relation a a
-- | Maybe (Expr BoolSort) for a given element
-- <math> and a given relation <math> that indicates if
-- <math> or not.
--
-- Just if given element is in bounds of the relation.
-- Nothing otherwise.
(!?) :: (Ix a, Ix b) => Relation a b -> (a, b) -> Maybe (Expr BoolSort)
-- | Unsafe version of (!?). Produces an array-indexing-error if
-- given element is not within the bounds 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
-- <math> that may be contained in the given relation <math>.
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 <math>, where the
-- first element represents an element <math> and the second
-- element indicates via a Expr BoolSort , if <math>
-- or not.
assocs :: (Ix a, Ix b) => Relation a b -> [((a, b), Expr BoolSort)]
-- | The domain <math> of a relation <math>.
domain :: Ix a => Relation a b -> [a]
-- | The codomain <math> of a relation <math>.
codomain :: Ix b => Relation a b -> [b]
-- | Returns a list of Expr BoolSort indicating whether the
-- projection on given element <math> holds for every element in
-- the codomain:
--
-- <math>
image :: (Ix a, Ix b) => Relation a b -> a -> [Expr BoolSort]
-- | Returns a list of Expr BoolSort indicating whether the
-- projection on given element <math> holds for every element in
-- the domain:
--
-- <math>
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. putStrLn $ table
-- <assignment> 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) => 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
-- StableNames.
class Sharing s where {
-- | A constraint on the monad used when asserting the shared node in
-- assertSharedNode.
type SharingMonad s :: (Type -> Type) -> Constraint;
}
-- | A Lens' on a mapping between a StableName and it's
-- Expr 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: nodeExpr :: Expr t === nodeVar. Also gives
-- access to the StableName 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
-- StableNames.
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 StableName 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
-- x y where makeStableName x == makeStableName
-- y 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.Internal.Default Language.Hasmtlib.Internal.Sharing.SharingMode
-- | This module provides a concrete implementation for MonadSMT
-- with it's state SMT.
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 StableName and it's Expr 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))
instance Data.Default.Internal.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
-- | This module provides a concrete implementation for MonadOMT
-- with it's state OMT.
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
formula :: Lens' SoftFormula (Expr 'BoolSort)
mWeight :: Lens' SoftFormula (Maybe Double)
mGroupId :: Lens' 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 SMT-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.Internal.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
-- | This module provides debugging capabilites for the problem definition
-- and communication with the external solver.
module Language.Hasmtlib.Type.Debugger
-- | A type holding actions for debugging states holding SMT-Problems.
data Debugger s
Debugger :: (s -> IO ()) -> (Builder -> IO ()) -> (Builder -> IO ()) -> (Builder -> IO ()) -> (Builder -> IO ()) -> (Builder -> IO ()) -> (Builder -> IO ()) -> (Builder -> IO ()) -> (Builder -> IO ()) -> (Builder -> IO ()) -> (Builder -> IO ()) -> (Builder -> IO ()) -> (Builder -> IO ()) -> (ByteString -> IO ()) -> (ByteString -> IO ()) -> Debugger s
-- | Debug the entire state
[debugState] :: Debugger s -> s -> IO ()
[debugOption] :: Debugger s -> Builder -> IO ()
[debugLogic] :: Debugger s -> Builder -> IO ()
[debugVar] :: Debugger s -> Builder -> IO ()
[debugAssert] :: Debugger s -> Builder -> IO ()
[debugPush] :: Debugger s -> Builder -> IO ()
[debugPop] :: Debugger s -> Builder -> IO ()
[debugCheckSat] :: Debugger s -> Builder -> IO ()
[debugGetModel] :: Debugger s -> Builder -> IO ()
[debugGetValue] :: Debugger s -> Builder -> IO ()
[debugMinimize] :: Debugger s -> Builder -> IO ()
[debugMaximize] :: Debugger s -> Builder -> IO ()
[debugAssertSoft] :: Debugger s -> Builder -> IO ()
-- | Debug the solvers raw response for (check-sat)
[debugResultResponse] :: Debugger s -> ByteString -> IO ()
-- | Debug the solvers raw response for (get-model)
[debugModelResponse] :: Debugger s -> ByteString -> IO ()
-- | A class that allows debugging states.
class StateDebugger s
-- | Debugs information about the problem like the amount of variables and
-- assertions.
statistically :: StateDebugger s => Debugger s
-- | The silent Debugger. Does not debug at all.
silently :: Debugger s
-- | The noisy Debugger.
--
-- Debugs the entire problem definition.
noisy :: Debugger s
-- | The verbose Debugger.
--
-- Debugs all communication between Haskell and the external solver.
verbosely :: Debugger s
-- | A Debugger for debugging all rendered options that have been
-- set.
optionish :: Debugger s
-- | A Debugger for debugging the logic that has been set.
logicish :: Debugger s
-- | A Debugger for debugging all variable declarations.
varish :: Debugger s
-- | A Debugger for debugging all assertions.
assertionish :: Debugger s
-- | A Debugger for debugging every push/pop-interaction with the
-- solvers incremental stack.
incrementalStackish :: Debugger s
-- | A Debugger for debugging every (get-value) call to the
-- solver.
getValueish :: Debugger s
-- | A Debugger for debugging the entire and raw responses of a
-- solver for the commands (check-sat) and (get-model).
responseish :: Debugger s
instance Language.Hasmtlib.Type.Debugger.StateDebugger Language.Hasmtlib.Type.SMT.SMT
instance Language.Hasmtlib.Type.Debugger.StateDebugger Language.Hasmtlib.Type.OMT.OMT
instance Data.Default.Internal.Default (Language.Hasmtlib.Type.Debugger.Debugger s)
module Language.Hasmtlib.Internal.Render
render1 :: Render a => Builder -> a -> Builder
render2 :: (Render a, Render b) => Builder -> a -> b -> Builder
render3 :: (Render a, Render b, Render c) => Builder -> a -> b -> c -> Builder
renderN :: Render a => Builder -> [a] -> Builder
-- | Render values to their SMTLib2-Lisp form, represented as
-- Builder.
class Render a
render :: Render a => a -> Builder
renderQuantifier :: forall t. KnownSMTSort t => Builder -> Maybe (SMTVar t) -> (Expr t -> Expr BoolSort) -> Builder
renderSetLogic :: Builder -> Builder
renderDeclareVar :: forall t. KnownSMTSort t => SMTVar t -> Builder
renderAssert :: Expr BoolSort -> Builder
renderGetValue :: SMTVar t -> Builder
renderPush :: Integer -> Builder
renderPop :: Integer -> Builder
renderCheckSat :: Builder
renderGetModel :: Builder
class RenderProblem s
renderOptions :: RenderProblem s => s -> Seq Builder
renderLogic :: RenderProblem s => s -> Builder
renderDeclareVars :: RenderProblem s => s -> Seq Builder
renderAssertions :: RenderProblem s => s -> Seq Builder
renderSoftAssertions :: RenderProblem s => s -> Seq Builder
renderMinimizations :: RenderProblem s => s -> Seq Builder
renderMaximizations :: RenderProblem s => s -> Seq Builder
instance Language.Hasmtlib.Internal.Render.RenderProblem Language.Hasmtlib.Type.SMT.SMT
instance Language.Hasmtlib.Internal.Render.RenderProblem Language.Hasmtlib.Type.OMT.OMT
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
instance Language.Hasmtlib.Internal.Render.Render (Language.Hasmtlib.Type.Bitvec.Bitvec enc n)
instance Language.Hasmtlib.Internal.Render.Render (Language.Hasmtlib.Type.Expr.SMTVar t)
instance GHC.Show.Show (Language.Hasmtlib.Type.Value.Value t)
instance Language.Hasmtlib.Internal.Render.Render (Language.Hasmtlib.Type.Value.Value t)
instance Language.Hasmtlib.Type.SMTSort.KnownSMTSort t => GHC.Show.Show (Language.Hasmtlib.Type.Expr.Expr t)
instance Language.Hasmtlib.Type.SMTSort.KnownSMTSort t => Language.Hasmtlib.Internal.Render.Render (Language.Hasmtlib.Type.Expr.Expr t)
instance Language.Hasmtlib.Internal.Render.Render (Language.Hasmtlib.Type.SMTSort.SSMTSort t)
instance Language.Hasmtlib.Internal.Render.Render Language.Hasmtlib.Type.Option.SMTOption
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)
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-Pipe to external SMT-Solvers and
-- ships with implementations for MonadSMT, MonadOMT and
-- MonadIncrSMT.
--
-- The Pipe is based on a Solver from Tweag's package
-- smtlib-backends and in reality is just an IO-Handle.
module Language.Hasmtlib.Type.Pipe
-- | A pipe to the solver. If Solver is Queuing 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 Solver is not
-- Queuing, all commands are sent to the solver immediately.
data Pipe
Pipe :: {-# UNPACK #-} !Int -> Maybe String -> !SharingMode -> !HashMap (StableName ()) (SomeKnownSMTSort Expr) -> !Seq (Seq (StableName ())) -> !Solver -> Maybe (Debugger Pipe) -> 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 StableName and it's Expr we may share
[_pipeStableMap] :: Pipe -> !HashMap (StableName ()) (SomeKnownSMTSort Expr)
-- | Index of each Seq (StableName ()) is incremental stack
-- height where StableName representing auxiliary var that has
-- been shared
[_incrSharedAuxs] :: Pipe -> !Seq (Seq (StableName ()))
-- | Active pipe to the backend
[_pipeSolver] :: Pipe -> !Solver
-- | Debugger for communication with the external solver
[_mPipeDebugger] :: Pipe -> Maybe (Debugger Pipe)
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
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.
--
-- The base type for every solver is the SolverConfig. It
-- describes where the solver executable is located and how it should
-- behave. You can provide a time-out using the decorator
-- timingout. Another decorator - debugging - allows you to
-- debug all the information you want. The actual debuggers can be found
-- in Language.Hasmtlib.Type.Debugger.
module Language.Hasmtlib.Type.Solver
-- | Configuration for solver processes.
data SolverConfig s
SolverConfig :: Config -> Maybe Int -> Maybe (Debugger s) -> SolverConfig s
-- | The underlying config of the process
[_processConfig] :: SolverConfig s -> Config
-- | Timeout in microseconds
[_mTimeout] :: SolverConfig s -> Maybe Int
-- | Debugger for communication with external solver
[_mDebugger] :: SolverConfig s -> Maybe (Debugger s)
-- | Decorates a SolverConfig with a Debugger.
debugging :: Debugger s -> SolverConfig s -> SolverConfig s
-- | Decorates a SolverConfig with a timeout. The timeout is given
-- as an Int which specifies after how many microseconds
-- the entire problem including problem construction, solver interaction
-- and solving time may time out.
--
-- When timing out, the Result will always be Unknown.
--
-- This uses timeout internally.
timingout :: Int -> SolverConfig s -> SolverConfig s
processConfig :: forall s_a22N2. Lens' (SolverConfig s_a22N2) Config
mTimeout :: forall s_a22N2. Lens' (SolverConfig s_a22N2) (Maybe Int)
mDebugger :: forall s_a22N2 s_a22NZ. Lens (SolverConfig s_a22N2) (SolverConfig s_a22NZ) (Maybe (Debugger s_a22N2)) (Maybe (Debugger s_a22NZ))
-- | Function that turns a state into a Result and a
-- Solution.
type Solver s m = s -> m (Result, Solution)
-- | Creates a Solver which holds an external process with a
-- SMT-Solver.
--
-- This will:
--
--
-- - Encode the SMT-problem,
-- - start a new external process for the SMT-Solver,
-- - send the problem to the SMT-Solver,
-- - wait for an answer and parse it,
-- - close the process and clean up all resources and
-- - return the decoded solution.
--
solver :: (RenderProblem s, MonadIO m) => SolverConfig s -> Solver s m
-- | solveWith solver prob solves a SMT problem
-- prob with the given solver. It returns a pair
-- consisting of:
--
--
-- - A Result that indicates if prob is satisfiable
-- (Sat), unsatisfiable (Unsat), or if the solver could not
-- determine any results (Unknown).
-- - A Decoded answer that was decoded using the solution to
-- prob. Note that this answer is only meaningful if the
-- Result is Sat or Unknown and the answer value is
-- in a Just.
--
--
-- Example
--
--
-- import Language.Hasmtlib
--
-- main :: IO ()
-- main = do
-- res <- solveWith @SMT (solver cvc5) $ do
-- setLogic "QF_LIA"
--
-- x <- var @IntSort
--
-- assert $ x >? 0
--
-- return x
--
-- print res
--
--
-- The solver will probably answer with x := 1.
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.
--
-- Example
--
--
-- import Language.Hasmtlib
-- import Control.Monad.IO.Class
--
-- main :: IO ()
-- main = do
-- interactiveWith z3 $ do
-- setOption $ ProduceModels True
-- setLogic "QF_LRA"
--
-- x <- var @RealSort
--
-- assert $ x >? 0
--
-- (res, sol) <- solve
-- liftIO $ print res
-- liftIO $ print $ decode sol x
--
-- push
-- y <- var @IntSort
--
-- assert $ y <? 0
-- assert $ x === y
--
-- res' <- checkSat
-- liftIO $ print res'
-- pop
--
-- res'' <- checkSat
-- liftIO $ print res''
--
-- return ()
--
interactiveWith :: (MonadIO m, MonadBaseControl IO m) => SolverConfig Pipe -> StateT Pipe m a -> m (Maybe a)
-- | Solves the current problem with respect to a minimal solution for a
-- given numerical expression.
--
-- This is done by incrementally refining the upper bound for a given
-- target. Terminates, when setting the last intermediate result as new
-- upper bound results in Unsat. Then removes that last assertion
-- and returns the previous (now confirmed minimal) result.
--
-- You can also provide a step-size. You do not have to worry about
-- stepping over the optimal result. This implementation takes care of
-- it.
--
-- Access to intermediate results is also possible via an
-- IO-Action.
--
-- Examples
--
--
-- x <- var @IntSort
-- assert $ x >? 4
-- solveMinimized x Nothing Nothing
--
--
-- The solver will return x := 5.
--
-- The first Nothing indicates that each intermediate result will
-- be set as next upper bound. The second Nothing shows that we do
-- not care about intermediate, but only the final (minimal) result.
--
--
-- x <- var @IntSort
-- assert $ x >? 4
-- solveMinimized x (Just (\r -> r-1)) (Just print)
--
--
-- The solver will still return x := 5.
--
-- However, here we want the next bound of each refinement to be
-- lastResult - 1. Also, every intermediate result is printed.
solveMinimized :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t, Orderable (Expr t)) => Expr t -> Maybe (Expr t -> Expr t) -> Maybe (Solution -> IO ()) -> m (Result, Solution)
-- | Solves the current problem with respect to a maximal solution for a
-- given numerical expression.
--
-- This is done by incrementally refining the lower bound for a given
-- target. Terminates, when setting the last intermediate result as new
-- lower bound results in Unsat. Then removes that last assertion
-- and returns the previous (now confirmed maximal) result.
--
-- You can also provide a step-size. You do not have to worry about
-- stepping over the optimal result. This implementation takes care of
-- it.
--
-- Access to intermediate results is also possible via an
-- IO-Action.
--
-- Examples
--
--
-- x <- var @IntSort
-- assert $ x <? 4
-- solveMaximized x Nothing Nothing
--
--
-- The solver will return x := 3.
--
-- The first Nothing indicates that each intermediate result will
-- be set as next lower bound. The second Nothing shows that we do
-- not care about intermediate, but only the final (maximal) result.
--
--
-- x <- var @IntSort
-- assert $ x <? 4
-- solveMinimized x (Just (+1)) (Just print)
--
--
-- The solver will still return x := 3.
--
-- However, here we want the next bound of each refinement to be
-- lastResult + 1. Also, every intermediate result is printed.
solveMaximized :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t, Orderable (Expr t)) => Expr t -> Maybe (Expr t -> Expr t) -> Maybe (Solution -> IO ()) -> m (Result, Solution)
module Language.Hasmtlib.Solver.Z3
-- | A SolverConfig for Z3. Requires binary z3 to be in
-- path.
z3 :: SolverConfig s
module Language.Hasmtlib.Solver.Yices
-- | A SolverConfig for Yices. Requires binary yices-smt2
-- to be in path.
yices :: SolverConfig s
module Language.Hasmtlib.Solver.OpenSMT
-- | A SolverConfig for OpenSMT. Requires binary opensmt to
-- be in path.
opensmt :: SolverConfig s
module Language.Hasmtlib.Solver.MathSAT
-- | A SolverConfig for MathSAT. Requires binary mathsat to
-- be in path.
mathsat :: SolverConfig s
-- | A SolverConfig for OptiMathSAT. Requires binary
-- optimathsat to be in path.
optimathsat :: SolverConfig s
module Language.Hasmtlib.Solver.CVC5
-- | A SolverConfig for CVC5. Requires binary cvc5 to be in
-- path.
cvc5 :: SolverConfig s
module Language.Hasmtlib.Solver.Bitwuzla
-- | A SolverConfig for Bitwuzla. Requires binary bitwuzla
-- 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 cadical - is in
-- path too.
bitwuzla :: SolverConfig s
-- | A SolverConfig for Bitwuzla with Kissat as underlying
-- sat-solver.
--
-- Requires binary bitwuzla and to be in path. Will use the
-- kissat shipped with bitwuzla.
--
-- It is recommended to build bitwuzla from source for this to
-- work as expected.
bitwuzlaKissat :: SolverConfig s
-- | This module provides the class Variable which lets you create
-- symbolical values of a data-type.
--
-- A generic default implementation with GVariable is possible.
--
-- Example
--
--
-- data V3 a = V3 a a a deriving Generic
-- instance Codec a => Codec (V3 a)
-- instance Equatable a => Codec (V3 a)
--
-- problem :: MonadSMT s m => StateT s m (V3 (Expr RealSort))
-- problem = do
-- let constantV3 = encode $ V3 7 69 42
-- symbolicV3 <- variable @(V3 (Expr RealSort))
-- assert $ symbolicV3 /== constantV3
-- return symbolicV3
--
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
-- Generic 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 variable which takes a Proxy
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 StableName are shared
StableNames :: SharingMode
-- | Sets the mode used for sharing common expressions. Defaults to
-- StableNames.
setSharingMode :: (Sharing s, MonadState s m) => SharingMode -> m ()