Language.Hasmtlib.Type.Value

Documentation

data Value (t :: SMTSort) where

A wrapper for values of SMTSorts. This wraps a Haskell-value into the SMT-Context.

Constructors

IntValue :: HaskellType IntSort -> Value IntSort

RealValue :: HaskellType RealSort -> Value RealSort

BoolValue :: HaskellType BoolSort -> Value BoolSort

BvValue :: KnownNat n => HaskellType (BvSort n) -> Value (BvSort n)

ArrayValue :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k), Ord (HaskellType v)) => HaskellType (ArraySort k v) -> Value (ArraySort k v)

StringValue :: HaskellType StringSort -> Value StringSort

Instances

GCompare Value

Defined in Language.Hasmtlib.Type.Value

Methods

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

GEq Value

Defined in Language.Hasmtlib.Type.Value

Methods

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

Show (Value t)

Defined in Language.Hasmtlib.Type.Expr

Methods

showsPrec :: Int -> Value t -> ShowS

show :: Value t -> String

showList :: [Value t] -> ShowS

Eq (HaskellType t) => Eq (Value t)

Defined in Language.Hasmtlib.Type.Value

Methods

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

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

Ord (HaskellType t) => Ord (Value t)

Defined in Language.Hasmtlib.Type.Value

Methods

compare :: Value t -> Value t -> Ordering

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

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

(>) :: Value t -> Value t -> Bool

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

max :: Value t -> Value t -> Value t

min :: Value t -> Value t -> Value t

Render (Value t)

Defined in Language.Hasmtlib.Type.Expr

Methods

render :: Value t -> Builder

wrapValue :: forall t. KnownSMTSort t => HaskellType t -> Value t

Wraps a Haskell-value into the SMT-Context-Value.

unwrapValue :: Value t -> HaskellType t

Unwraps a Haskell-value from the SMT-Context-Value.