Language.Hasmtlib.Type.SMTSort

Documentation

data SMTSort

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

Constructors

BoolSort

Sort of Bool

IntSort

Sort of Int

RealSort

Sort of Real

BvSort Nat

Sort of BitVec with length n

ArraySort SMTSort SMTSort

Sort of Array with indices k and values v

StringSort

Sort of String

Instances

GNFData Expr

Defined in Language.Hasmtlib.Type.Expr

Methods

grnf :: forall (a :: k). Expr a -> ()

GCompare SSMTSort

Defined in Language.Hasmtlib.Type.SMTSort

Methods

gcompare :: forall (a :: k) (b :: k). SSMTSort a -> SSMTSort b -> GOrdering a b

GEq Value

Defined in Language.Hasmtlib.Type.Expr

Methods

geq :: forall (a :: k) (b :: k). Value a -> Value b -> Maybe (a :~: b)

GEq SSMTSort

Defined in Language.Hasmtlib.Type.SMTSort

Methods

geq :: forall (a :: k) (b :: k). SSMTSort a -> SSMTSort b -> Maybe (a :~: b)

Uniplate1 Expr '[KnownSMTSort]

Caution for quantified expressions: uniplate1 will only be applied if quantification has taken place already.

Defined in Language.Hasmtlib.Type.Expr

Methods

uniplate1 :: forall m (b :: k). (Applicative m, AllC '[KnownSMTSort] b) => (forall (a :: k). AllC '[KnownSMTSort] a => Expr a -> m (Expr a)) -> Expr b -> m (Expr b)

type family HaskellType (t :: SMTSort) = (r :: Type) | r -> t where ...

Injective type-family that computes the Haskell Type of an SMTSort.

Equations

HaskellType IntSort = Integer

HaskellType RealSort = Double

HaskellType BoolSort = Bool

HaskellType (BvSort n) = Bitvec n

HaskellType (ArraySort k v) = ConstArray (HaskellType k) (HaskellType v)

HaskellType StringSort = Text

data SSMTSort (t :: SMTSort) where

Singleton for SMTSort.

Constructors

SIntSort :: SSMTSort IntSort

SRealSort :: SSMTSort RealSort

SBoolSort :: SSMTSort BoolSort

SBvSort :: KnownNat n => Proxy n -> SSMTSort (BvSort n)

SArraySort :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k), Eq (HaskellType v)) => Proxy k -> Proxy v -> SSMTSort (ArraySort k v)

SStringSort :: SSMTSort StringSort

Instances

GCompare SSMTSort

Defined in Language.Hasmtlib.Type.SMTSort

Methods

gcompare :: forall (a :: k) (b :: k). SSMTSort a -> SSMTSort b -> GOrdering a b

GEq SSMTSort

Defined in Language.Hasmtlib.Type.SMTSort

Methods

geq :: forall (a :: k) (b :: k). SSMTSort a -> SSMTSort b -> Maybe (a :~: b)

Show (SSMTSort t)

Defined in Language.Hasmtlib.Type.SMTSort

Methods

showsPrec :: Int -> SSMTSort t -> ShowS

show :: SSMTSort t -> String

showList :: [SSMTSort t] -> ShowS

Eq (SSMTSort t)

Defined in Language.Hasmtlib.Type.SMTSort

Methods

(==) :: SSMTSort t -> SSMTSort t -> Bool

(/=) :: SSMTSort t -> SSMTSort t -> Bool

Ord (SSMTSort t)

Defined in Language.Hasmtlib.Type.SMTSort

Methods

compare :: SSMTSort t -> SSMTSort t -> Ordering

(<) :: SSMTSort t -> SSMTSort t -> Bool

(<=) :: SSMTSort t -> SSMTSort t -> Bool

(>) :: SSMTSort t -> SSMTSort t -> Bool

(>=) :: SSMTSort t -> SSMTSort t -> Bool

max :: SSMTSort t -> SSMTSort t -> SSMTSort t

min :: SSMTSort t -> SSMTSort t -> SSMTSort t

Render (SSMTSort t)

Defined in Language.Hasmtlib.Type.SMTSort

Methods

render :: SSMTSort t -> Builder

class KnownSMTSort (t :: SMTSort) where

Compute singleton SSMTSort from it's promoted type SMTSort.

Methods

sortSing :: SSMTSort t

Instances

KnownSMTSort 'BoolSort

Defined in Language.Hasmtlib.Type.SMTSort

Methods

sortSing :: SSMTSort 'BoolSort

KnownSMTSort 'IntSort

Defined in Language.Hasmtlib.Type.SMTSort

Methods

sortSing :: SSMTSort 'IntSort

KnownSMTSort 'RealSort

Defined in Language.Hasmtlib.Type.SMTSort

Methods

sortSing :: SSMTSort 'RealSort

KnownSMTSort 'StringSort

Defined in Language.Hasmtlib.Type.SMTSort

Methods

sortSing :: SSMTSort 'StringSort

Uniplate1 Expr '[KnownSMTSort]

Caution for quantified expressions: uniplate1 will only be applied if quantification has taken place already.

Defined in Language.Hasmtlib.Type.Expr

Methods

uniplate1 :: forall m (b :: k). (Applicative m, AllC '[KnownSMTSort] b) => (forall (a :: k). AllC '[KnownSMTSort] a => Expr a -> m (Expr a)) -> Expr b -> m (Expr b)

KnownNat n => KnownSMTSort ('BvSort n)

Defined in Language.Hasmtlib.Type.SMTSort

Methods

sortSing :: SSMTSort ('BvSort n)

(KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k), Eq (HaskellType v)) => KnownSMTSort ('ArraySort k v)

Defined in Language.Hasmtlib.Type.SMTSort

Methods

sortSing :: SSMTSort ('ArraySort k v)

sortSing' :: forall prxy t. KnownSMTSort t => prxy t -> SSMTSort t

Wrapper for sortSing which takes a Proxy

data SomeSMTSort cs f where

An existential wrapper that hides some SMTSort and a list of Constraints holding for it.

Constructors

SomeSMTSort :: forall cs f (t :: SMTSort). AllC cs t => f t -> SomeSMTSort cs f

Instances

(forall (t :: SMTSort). Show (f t)) => Show (SomeSMTSort cs f)

Defined in Language.Hasmtlib.Type.SMTSort

Methods

showsPrec :: Int -> SomeSMTSort cs f -> ShowS

show :: SomeSMTSort cs f -> String

showList :: [SomeSMTSort cs f] -> ShowS