Language.Hasmtlib.Type.Value

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.

Type

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

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)

(KnownSMTSort t, Num (HaskellType t)) => Num (Value t)

Defined in Language.Hasmtlib.Type.Value

Methods

(+) :: Value t -> Value t -> Value t

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

(*) :: Value t -> Value t -> Value t

negate :: Value t -> Value t

abs :: Value t -> Value t

signum :: Value t -> Value t

fromInteger :: Integer -> Value t

Fractional (Value 'RealSort)

Defined in Language.Hasmtlib.Type.Value

Methods

(/) :: Value 'RealSort -> Value 'RealSort -> Value 'RealSort

recip :: Value 'RealSort -> Value 'RealSort

fromRational :: Rational -> Value 'RealSort

Show (Value t)

Defined in Language.Hasmtlib.Internal.Render

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

Boolean (Value 'BoolSort)

Defined in Language.Hasmtlib.Type.Value

Methods

bool :: Bool -> Value 'BoolSort

true :: Value 'BoolSort

false :: Value 'BoolSort

(&&) :: Value 'BoolSort -> Value 'BoolSort -> Value 'BoolSort

(||) :: Value 'BoolSort -> Value 'BoolSort -> Value 'BoolSort

(==>) :: Value 'BoolSort -> Value 'BoolSort -> Value 'BoolSort

(<==) :: Value 'BoolSort -> Value 'BoolSort -> Value 'BoolSort

(<==>) :: Value 'BoolSort -> Value 'BoolSort -> Value 'BoolSort

not :: Value 'BoolSort -> Value 'BoolSort

xor :: Value 'BoolSort -> Value 'BoolSort -> Value 'BoolSort

Render (Value t)

Defined in Language.Hasmtlib.Internal.Render

Methods

render :: Value t -> Builder

Conversion

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.