Language.Hasmtlib.Type.Expr

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

Instances

GCompare SSMTSort

Defined in Language.Hasmtlib.Internal.Expr

Methods

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

GEq SSMTSort

Defined in Language.Hasmtlib.Internal.Expr

Methods

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

newtype SMTVar (t :: SMTSort)

An internal SMT variable with a phantom-type which holds an Int as it's identifier.

Constructors

SMTVar

Fields

• _varId :: Int

Instances

Show (SMTVar t)

Defined in Language.Hasmtlib.Internal.Expr

Methods

showsPrec :: Int -> SMTVar t -> ShowS

show :: SMTVar t -> String

showList :: [SMTVar t] -> ShowS

Eq (SMTVar t)

Defined in Language.Hasmtlib.Internal.Expr

Methods

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

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

Ord (SMTVar t)

Defined in Language.Hasmtlib.Internal.Expr

Methods

compare :: SMTVar t -> SMTVar t -> Ordering

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

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

(>) :: SMTVar t -> SMTVar t -> Bool

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

max :: SMTVar t -> SMTVar t -> SMTVar t

min :: SMTVar t -> SMTVar t -> SMTVar t

Render (SMTVar t)

Defined in Language.Hasmtlib.Internal.Expr

Methods

render :: SMTVar t -> Builder

varId :: forall t t. Iso (SMTVar t) (SMTVar t) Int Int

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)

data Value (t :: SMTSort) where

A wrapper for values of SMTSorts.

Constructors

IntValue :: HaskellType IntSort -> Value IntSort

RealValue :: HaskellType RealSort -> Value RealSort

BoolValue :: HaskellType BoolSort -> Value BoolSort

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

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

Instances

Show (Value t)

Defined in Language.Hasmtlib.Internal.Expr

Methods

showsPrec :: Int -> Value t -> ShowS

show :: Value t -> String

showList :: [Value t] -> ShowS

Render (Value t)

Defined in Language.Hasmtlib.Internal.Expr

Methods

render :: Value t -> Builder

unwrapValue :: Value t -> HaskellType t

Unwrap a value from Value.

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

Wrap a value into Value.

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)) => Proxy k -> Proxy v -> SSMTSort (ArraySort k v)

Instances

GCompare SSMTSort

Defined in Language.Hasmtlib.Internal.Expr

Methods

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

GEq SSMTSort

Defined in Language.Hasmtlib.Internal.Expr

Methods

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

Show (SSMTSort t)

Defined in Language.Hasmtlib.Internal.Expr

Methods

showsPrec :: Int -> SSMTSort t -> ShowS

show :: SSMTSort t -> String

showList :: [SSMTSort t] -> ShowS

Eq (SSMTSort t)

Defined in Language.Hasmtlib.Internal.Expr

Methods

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

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

Ord (SSMTSort t)

Defined in Language.Hasmtlib.Internal.Expr

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.Internal.Expr

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.Internal.Expr

Methods

sortSing :: SSMTSort 'BoolSort

KnownSMTSort 'IntSort

Defined in Language.Hasmtlib.Internal.Expr

Methods

sortSing :: SSMTSort 'IntSort

KnownSMTSort 'RealSort

Defined in Language.Hasmtlib.Internal.Expr

Methods

sortSing :: SSMTSort 'RealSort

KnownNat n => KnownSMTSort ('BvSort n)

Defined in Language.Hasmtlib.Internal.Expr

Methods

sortSing :: SSMTSort ('BvSort n)

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

Defined in Language.Hasmtlib.Internal.Expr

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

type SomeKnownSMTSort f = SomeSMTSort '[KnownSMTSort] f

An existential wrapper that hides some known SMTSort.

type family AllC cs k :: Constraint where ...

AllC ensures that a list of constraints is applied to a poly-kinded Type k

AllC '[]       k = ()
AllC (c ': cs) k = (c k, AllC cs k)

Equations

AllC '[] k = ()

AllC (c ': cs) k = (c k, AllC cs k)

data Expr (t :: SMTSort)

A SMT expression. For internal use only. For building expressions use the corresponding instances (Num, Boolean, ...).

Instances

Bounded (Expr 'BoolSort)

Defined in Language.Hasmtlib.Internal.Expr

Methods

minBound :: Expr 'BoolSort

maxBound :: Expr 'BoolSort

KnownNat n => Bounded (Expr ('BvSort n))

Defined in Language.Hasmtlib.Internal.Expr

Methods

minBound :: Expr ('BvSort n)

maxBound :: Expr ('BvSort n)

Floating (Expr 'RealSort)

Defined in Language.Hasmtlib.Internal.Expr.Num

Methods

pi :: Expr 'RealSort

exp :: Expr 'RealSort -> Expr 'RealSort

log :: Expr 'RealSort -> Expr 'RealSort

sqrt :: Expr 'RealSort -> Expr 'RealSort

(**) :: Expr 'RealSort -> Expr 'RealSort -> Expr 'RealSort

logBase :: Expr 'RealSort -> 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

sinh :: Expr 'RealSort -> Expr 'RealSort

cosh :: Expr 'RealSort -> Expr 'RealSort

tanh :: Expr 'RealSort -> Expr 'RealSort

asinh :: Expr 'RealSort -> Expr 'RealSort

acosh :: Expr 'RealSort -> Expr 'RealSort

atanh :: Expr 'RealSort -> Expr 'RealSort

log1p :: Expr 'RealSort -> Expr 'RealSort

expm1 :: Expr 'RealSort -> Expr 'RealSort

log1pexp :: Expr 'RealSort -> Expr 'RealSort

log1mexp :: Expr 'RealSort -> Expr 'RealSort

KnownNat n => Num (Expr ('BvSort n))

Defined in Language.Hasmtlib.Internal.Expr.Num

Methods

(+) :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)

(-) :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)

(*) :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)

negate :: Expr ('BvSort n) -> Expr ('BvSort n)

abs :: Expr ('BvSort n) -> Expr ('BvSort n)

signum :: Expr ('BvSort n) -> Expr ('BvSort n)

fromInteger :: Integer -> Expr ('BvSort n)

Num (Expr 'IntSort)

Defined in Language.Hasmtlib.Internal.Expr.Num

Methods

(+) :: Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort

(-) :: Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort

(*) :: Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort

negate :: Expr 'IntSort -> Expr 'IntSort

abs :: Expr 'IntSort -> Expr 'IntSort

signum :: Expr 'IntSort -> Expr 'IntSort

fromInteger :: Integer -> Expr 'IntSort

Num (Expr 'RealSort)

Defined in Language.Hasmtlib.Internal.Expr.Num

Methods

(+) :: Expr 'RealSort -> Expr 'RealSort -> Expr 'RealSort

(-) :: Expr 'RealSort -> Expr 'RealSort -> Expr 'RealSort

(*) :: Expr 'RealSort -> Expr 'RealSort -> Expr 'RealSort

negate :: Expr 'RealSort -> Expr 'RealSort

abs :: Expr 'RealSort -> Expr 'RealSort

signum :: Expr 'RealSort -> Expr 'RealSort

fromInteger :: Integer -> Expr 'RealSort

Fractional (Expr 'RealSort)

Defined in Language.Hasmtlib.Internal.Expr.Num

Methods

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

recip :: Expr 'RealSort -> Expr 'RealSort

fromRational :: Rational -> Expr 'RealSort

Show (Expr t)

Defined in Language.Hasmtlib.Internal.Expr

Methods

showsPrec :: Int -> Expr t -> ShowS

show :: Expr t -> String

showList :: [Expr t] -> ShowS

Boolean (Expr 'BoolSort)

Defined in Language.Hasmtlib.Internal.Expr

Methods

bool :: Bool -> Expr 'BoolSort

true :: Expr 'BoolSort

false :: Expr 'BoolSort

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

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

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

not :: Expr 'BoolSort -> Expr 'BoolSort

xor :: Expr 'BoolSort -> Expr 'BoolSort -> Expr 'BoolSort

KnownNat n => Boolean (Expr ('BvSort n))

Defined in Language.Hasmtlib.Internal.Expr

Methods

bool :: Bool -> Expr ('BvSort n)

true :: Expr ('BvSort n)

false :: Expr ('BvSort n)

(&&) :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)

(||) :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)

(==>) :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)

not :: Expr ('BvSort n) -> Expr ('BvSort n)

xor :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)

KnownSMTSort t => Codec (Expr t)

Decode and evaluate expressions

Defined in Language.Hasmtlib.Codec

Associated Types

type Decoded (Expr t)

Methods

decode :: Solution -> Expr t -> Maybe (Decoded (Expr t))

encode :: Decoded (Expr t) -> Expr t

(KnownSMTSort t, Eq (HaskellType t)) => Equatable (Expr t)

Defined in Language.Hasmtlib.Equatable

Methods

(===) :: Expr t -> Expr t -> Expr 'BoolSort

(/==) :: Expr t -> Expr t -> Expr 'BoolSort

KnownNat n => Integraled (Expr ('BvSort n))

Defined in Language.Hasmtlib.Internal.Expr.Num

Methods

quot :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)

rem :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)

div :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)

mod :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)

quotRem :: Expr ('BvSort n) -> Expr ('BvSort n) -> (Expr ('BvSort n), Expr ('BvSort n))

divMod :: Expr ('BvSort n) -> Expr ('BvSort n) -> (Expr ('BvSort n), Expr ('BvSort n))

Integraled (Expr 'IntSort)

Defined in Language.Hasmtlib.Internal.Expr.Num

Methods

quot :: Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort

rem :: Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort

div :: Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort

mod :: Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort

quotRem :: Expr 'IntSort -> Expr 'IntSort -> (Expr 'IntSort, Expr 'IntSort)

divMod :: Expr 'IntSort -> Expr 'IntSort -> (Expr 'IntSort, Expr 'IntSort)

KnownSMTSort t => Render (Expr t)

Defined in Language.Hasmtlib.Internal.Expr

Methods

render :: Expr t -> Builder

KnownNat n => Orderable (Expr ('BvSort n))

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr 'BoolSort

(>=?) :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr 'BoolSort

(<?) :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr 'BoolSort

(>?) :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr 'BoolSort

Orderable (Expr 'IntSort)

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: Expr 'IntSort -> Expr 'IntSort -> Expr 'BoolSort

(>=?) :: Expr 'IntSort -> Expr 'IntSort -> Expr 'BoolSort

(<?) :: Expr 'IntSort -> Expr 'IntSort -> Expr 'BoolSort

(>?) :: Expr 'IntSort -> Expr 'IntSort -> Expr 'BoolSort

Orderable (Expr 'RealSort)

Defined in Language.Hasmtlib.Orderable

Methods

(<=?) :: Expr 'RealSort -> Expr 'RealSort -> Expr 'BoolSort

(>=?) :: Expr 'RealSort -> Expr 'RealSort -> Expr 'BoolSort

(<?) :: Expr 'RealSort -> Expr 'RealSort -> Expr 'BoolSort

(>?) :: Expr 'RealSort -> Expr 'RealSort -> Expr 'BoolSort

KnownSMTSort t => Variable (Expr t)

Defined in Language.Hasmtlib.Variable

Methods

variable :: MonadSMT s m => m (Expr t)

Iteable (Expr 'BoolSort) ()

Defined in Language.Hasmtlib.Iteable

Methods

ite :: Expr 'BoolSort -> () -> () -> ()

Iteable (Expr 'BoolSort) a => Iteable (Expr 'BoolSort) (Seq a)

Defined in Language.Hasmtlib.Iteable

Methods

ite :: Expr 'BoolSort -> Seq a -> Seq a -> Seq a

Iteable (Expr 'BoolSort) a => Iteable (Expr 'BoolSort) (Tree a)

Defined in Language.Hasmtlib.Iteable

Methods

ite :: Expr 'BoolSort -> Tree a -> Tree a -> Tree a

Iteable (Expr 'BoolSort) (Expr t)

Defined in Language.Hasmtlib.Iteable

Methods

ite :: Expr 'BoolSort -> Expr t -> Expr t -> Expr t

Iteable (Expr 'BoolSort) a => Iteable (Expr 'BoolSort) (Maybe a)

Defined in Language.Hasmtlib.Iteable

Methods

ite :: Expr 'BoolSort -> Maybe a -> Maybe a -> Maybe a

Iteable (Expr 'BoolSort) a => Iteable (Expr 'BoolSort) [a]

Defined in Language.Hasmtlib.Iteable

Methods

ite :: Expr 'BoolSort -> [a] -> [a] -> [a]

(Iteable (Expr 'BoolSort) a, Iteable (Expr 'BoolSort) b) => Iteable (Expr 'BoolSort) (a, b)

Defined in Language.Hasmtlib.Iteable

Methods

ite :: Expr 'BoolSort -> (a, b) -> (a, b) -> (a, b)

(Iteable (Expr 'BoolSort) a, Iteable (Expr 'BoolSort) b, Iteable (Expr 'BoolSort) c) => Iteable (Expr 'BoolSort) (a, b, c)

Defined in Language.Hasmtlib.Iteable

Methods

ite :: Expr 'BoolSort -> (a, b, c) -> (a, b, c) -> (a, b, c)

(Iteable (Expr 'BoolSort) a, Iteable (Expr 'BoolSort) b, Iteable (Expr 'BoolSort) c, Iteable (Expr 'BoolSort) d) => Iteable (Expr 'BoolSort) (a, b, c, d)

Defined in Language.Hasmtlib.Iteable

Methods

ite :: Expr 'BoolSort -> (a, b, c, d) -> (a, b, c, d) -> (a, b, c, d)

(Iteable (Expr 'BoolSort) a, Iteable (Expr 'BoolSort) b, Iteable (Expr 'BoolSort) c, Iteable (Expr 'BoolSort) d, Iteable (Expr 'BoolSort) e) => Iteable (Expr 'BoolSort) (a, b, c, d, e)

Defined in Language.Hasmtlib.Iteable

Methods

ite :: Expr 'BoolSort -> (a, b, c, d, e) -> (a, b, c, d, e) -> (a, b, c, d, e)

(Iteable (Expr 'BoolSort) a, Iteable (Expr 'BoolSort) b, Iteable (Expr 'BoolSort) c, Iteable (Expr 'BoolSort) d, Iteable (Expr 'BoolSort) e, Iteable (Expr 'BoolSort) f) => Iteable (Expr 'BoolSort) (a, b, c, d, e, f)

Defined in Language.Hasmtlib.Iteable

Methods

ite :: Expr 'BoolSort -> (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> (a, b, c, d, e, f)

(Iteable (Expr 'BoolSort) a, Iteable (Expr 'BoolSort) b, Iteable (Expr 'BoolSort) c, Iteable (Expr 'BoolSort) d, Iteable (Expr 'BoolSort) e, Iteable (Expr 'BoolSort) f, Iteable (Expr 'BoolSort) g) => Iteable (Expr 'BoolSort) (a, b, c, d, e, f, g)

Defined in Language.Hasmtlib.Iteable

Methods

ite :: Expr 'BoolSort -> (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g)

(Iteable (Expr 'BoolSort) a, Iteable (Expr 'BoolSort) b, Iteable (Expr 'BoolSort) c, Iteable (Expr 'BoolSort) d, Iteable (Expr 'BoolSort) e, Iteable (Expr 'BoolSort) f, Iteable (Expr 'BoolSort) g, Iteable (Expr 'BoolSort) h) => Iteable (Expr 'BoolSort) (a, b, c, d, e, f, g, h)

Defined in Language.Hasmtlib.Iteable

Methods

ite :: Expr 'BoolSort -> (a, b, c, d, e, f, g, h) -> (a, b, c, d, e, f, g, h) -> (a, b, c, d, e, f, g, h)

type Decoded (Expr t)

Defined in Language.Hasmtlib.Codec

type Decoded (Expr t) = HaskellType t

for_all :: forall t. KnownSMTSort t => (Expr t -> Expr BoolSort) -> Expr BoolSort

A universal quantification for any specific SMTSort. If the type cannot be inferred, apply a type-annotation. Nested quantifiers are also supported.

Usage:

  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.

exists :: forall t. KnownSMTSort t => (Expr t -> Expr BoolSort) -> Expr BoolSort

An existential quantification for any specific SMTSort If the type cannot be inferred, apply a type-annotation. Nested quantifiers are also supported.

Usage:

  assert $
     for_all @(BvSort 8) $ x ->
         exists $ y ->
           x - y === 0 
  

The lambdas y is existentially quantified here. It will only be scoped for the lambdas body.

select :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Expr (ArraySort k v) -> Expr k -> Expr v

Select a value from an array.

store :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Expr (ArraySort k v) -> Expr k -> Expr v -> Expr (ArraySort k v)

Store a value in an array.

bvShL :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)

Bitvector shift left

bvLShR :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)

Bitvector logical shift right

bvConcat :: (KnownNat n, KnownNat m) => Expr (BvSort n) -> Expr (BvSort m) -> Expr (BvSort (n + m))

Concat two bitvectors

bvRotL :: (KnownNat n, KnownNat i, KnownNat (Mod i n)) => Proxy i -> Expr (BvSort n) -> Expr (BvSort n)

Rotate bitvector left

bvRotR :: (KnownNat n, KnownNat i, KnownNat (Mod i n)) => Proxy i -> Expr (BvSort n) -> Expr (BvSort n)

Rotate bitvector right