| Safe Haskell | Safe-Inferred |
|---|---|
| Language | GHC2021 |
Language.Hasmtlib.Type.Expr
Synopsis
- newtype SMTVar (t :: SMTSort) = SMTVar {}
- varId :: forall t t. Iso (SMTVar t) (SMTVar t) Int Int
- data Value (t :: SMTSort) where
- 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)
- unwrapValue :: Value t -> HaskellType t
- wrapValue :: forall t. KnownSMTSort t => HaskellType t -> Value t
- data Expr (t :: SMTSort)
- equal :: (Eq (HaskellType t), KnownSMTSort t, Foldable f) => f (Expr t) -> Expr BoolSort
- distinct :: (Eq (HaskellType t), KnownSMTSort t, Foldable f) => f (Expr t) -> Expr BoolSort
- bvShL :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
- bvLShR :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
- bvConcat :: (KnownNat n, KnownNat m) => Expr (BvSort n) -> Expr (BvSort m) -> Expr (BvSort (n + m))
- bvRotL :: (KnownNat n, KnownNat i, KnownNat (Mod i n)) => Proxy i -> Expr (BvSort n) -> Expr (BvSort n)
- bvRotR :: (KnownNat n, KnownNat i, KnownNat (Mod i n)) => Proxy i -> Expr (BvSort n) -> Expr (BvSort n)
- toIntSort :: Expr RealSort -> Expr IntSort
- toRealSort :: Expr IntSort -> Expr RealSort
- isIntSort :: Expr RealSort -> Expr BoolSort
- for_all :: forall t. KnownSMTSort t => (Expr t -> Expr BoolSort) -> Expr BoolSort
- exists :: forall t. KnownSMTSort t => (Expr t -> Expr BoolSort) -> Expr BoolSort
- select :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Expr (ArraySort k v) -> Expr k -> Expr v
- store :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Expr (ArraySort k v) -> Expr k -> Expr v -> Expr (ArraySort k v)
Documentation
newtype SMTVar (t :: SMTSort) Source #
An internal SMT variable with a phantom-type which holds an Int as it's identifier.
data Value (t :: SMTSort) where Source #
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) |
unwrapValue :: Value t -> HaskellType t Source #
Unwrap a value from Value.
wrapValue :: forall t. KnownSMTSort t => HaskellType t -> Value t Source #
Wrap a value into Value.
data Expr (t :: SMTSort) Source #
A SMT expression. For internal use only. For building expressions use the corresponding instances (Num, Boolean, ...).
Instances
equal :: (Eq (HaskellType t), KnownSMTSort t, Foldable f) => f (Expr t) -> Expr BoolSort Source #
Test multiple expressions on equality within in the SMT-Problem.
distinct :: (Eq (HaskellType t), KnownSMTSort t, Foldable f) => f (Expr t) -> Expr BoolSort Source #
Test multiple expressions on distinctness within in the SMT-Problem.
bvShL :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n) Source #
Bitvector shift left
bvLShR :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n) Source #
Bitvector logical shift right
bvConcat :: (KnownNat n, KnownNat m) => Expr (BvSort n) -> Expr (BvSort m) -> Expr (BvSort (n + m)) Source #
Concat two bitvectors
bvRotL :: (KnownNat n, KnownNat i, KnownNat (Mod i n)) => Proxy i -> Expr (BvSort n) -> Expr (BvSort n) Source #
Rotate bitvector left
bvRotR :: (KnownNat n, KnownNat i, KnownNat (Mod i n)) => Proxy i -> Expr (BvSort n) -> Expr (BvSort n) Source #
Rotate bitvector right
for_all :: forall t. KnownSMTSort t => (Expr t -> Expr BoolSort) -> Expr BoolSort Source #
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 Source #
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 Source #
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) Source #
Store a value in an array.