| Safe Haskell | Safe-Inferred |
|---|---|
| Language | GHC2021 |
Language.Hasmtlib.Type.Expr
Contents
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 :: 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
- unwrapValue :: Value t -> HaskellType t
- wrapValue :: forall t. KnownSMTSort t => HaskellType t -> Value t
- data Expr (t :: SMTSort) where
- Var :: KnownSMTSort t => SMTVar t -> Expr t
- Constant :: Value t -> Expr t
- Plus :: Num (HaskellType t) => Expr t -> Expr t -> Expr t
- Minus :: Num (HaskellType t) => Expr t -> Expr t -> Expr t
- Neg :: Num (HaskellType t) => Expr t -> Expr t
- Mul :: Num (HaskellType t) => Expr t -> Expr t -> Expr t
- Abs :: Num (HaskellType t) => Expr t -> Expr t
- Mod :: Integral (HaskellType t) => Expr t -> Expr t -> Expr t
- IDiv :: Integral (HaskellType t) => Expr t -> Expr t -> Expr t
- Div :: Expr RealSort -> Expr RealSort -> Expr RealSort
- LTH :: (Ord (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort
- LTHE :: (Ord (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort
- EQU :: (Eq (HaskellType t), KnownSMTSort t, KnownNat n) => Vector (n + 2) (Expr t) -> Expr BoolSort
- Distinct :: (Eq (HaskellType t), KnownSMTSort t, KnownNat n) => Vector (n + 2) (Expr t) -> Expr BoolSort
- GTHE :: (Ord (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort
- GTH :: (Ord (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort
- Not :: Boolean (HaskellType t) => Expr t -> Expr t
- And :: Boolean (HaskellType t) => Expr t -> Expr t -> Expr t
- Or :: Boolean (HaskellType t) => Expr t -> Expr t -> Expr t
- Impl :: Boolean (HaskellType t) => Expr t -> Expr t -> Expr t
- Xor :: Boolean (HaskellType t) => Expr t -> Expr t -> Expr t
- Pi :: Expr RealSort
- Sqrt :: Expr RealSort -> Expr RealSort
- Exp :: 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
- ToReal :: Expr IntSort -> Expr RealSort
- ToInt :: Expr RealSort -> Expr IntSort
- IsInt :: Expr RealSort -> Expr BoolSort
- Ite :: Expr BoolSort -> Expr t -> Expr t -> Expr t
- BvNand :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
- BvNor :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
- 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, Integral a) => a -> Expr (BvSort n) -> Expr (BvSort n)
- BvRotR :: (KnownNat n, Integral a) => a -> Expr (BvSort n) -> Expr (BvSort n)
- ArrSelect :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k), Ord (HaskellType v)) => Expr (ArraySort k v) -> Expr k -> Expr v
- ArrStore :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Expr (ArraySort k v) -> Expr k -> Expr v -> Expr (ArraySort k v)
- StrConcat :: Expr StringSort -> Expr StringSort -> Expr StringSort
- StrLength :: Expr StringSort -> Expr IntSort
- StrLT :: Expr StringSort -> Expr StringSort -> Expr BoolSort
- StrLTHE :: Expr StringSort -> Expr StringSort -> Expr BoolSort
- StrAt :: Expr StringSort -> Expr IntSort -> Expr StringSort
- StrSubstring :: Expr StringSort -> Expr IntSort -> Expr IntSort -> Expr StringSort
- StrPrefixOf :: Expr StringSort -> Expr StringSort -> Expr BoolSort
- StrSuffixOf :: Expr StringSort -> Expr StringSort -> Expr BoolSort
- StrContains :: Expr StringSort -> Expr StringSort -> Expr BoolSort
- StrIndexOf :: Expr StringSort -> Expr StringSort -> Expr IntSort -> Expr IntSort
- StrReplace :: Expr StringSort -> Expr StringSort -> Expr StringSort -> Expr StringSort
- StrReplaceAll :: Expr StringSort -> Expr StringSort -> Expr StringSort -> Expr StringSort
- ForAll :: KnownSMTSort t => Maybe (SMTVar t) -> (Expr t -> Expr BoolSort) -> Expr BoolSort
- Exists :: KnownSMTSort t => Maybe (SMTVar t) -> (Expr t -> Expr BoolSort) -> Expr BoolSort
- isLeaf :: Expr t -> Bool
- class Iteable b a where
- ite :: b -> a -> a -> a
- class Equatable a where
- class Equatable a => Orderable a where
- min' :: (Orderable a, Iteable (Expr BoolSort) a) => a -> a -> a
- max' :: (Orderable a, Iteable (Expr BoolSort) a) => a -> a -> a
- 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
- 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), Ord (HaskellType v)) => 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)
- 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))
- toRealSort :: Expr IntSort -> Expr RealSort
- toIntSort :: Expr RealSort -> Expr IntSort
- isIntSort :: Expr RealSort -> Expr BoolSort
- strLength :: Expr StringSort -> Expr IntSort
- strAt :: Expr StringSort -> Expr IntSort -> Expr StringSort
- strSubstring :: Expr StringSort -> Expr IntSort -> Expr IntSort -> Expr StringSort
- strPrefixOf :: Expr StringSort -> Expr StringSort -> Expr BoolSort
- strSuffixOf :: Expr StringSort -> Expr StringSort -> Expr BoolSort
- strContains :: Expr StringSort -> Expr StringSort -> Expr BoolSort
- strIndexOf :: Expr StringSort -> Expr StringSort -> Expr IntSort -> Expr IntSort
- strReplace :: Expr StringSort -> Expr StringSort -> Expr StringSort -> Expr StringSort
- strReplaceAll :: Expr StringSort -> Expr StringSort -> Expr StringSort -> Expr StringSort
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.
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 |
unwrapValue :: Value t -> HaskellType t Source #
Unwraps a Haskell-value from the SMT-Context-Value.
wrapValue :: forall t. KnownSMTSort t => HaskellType t -> Value t Source #
Wraps a Haskell-value into the SMT-Context-Value.
data Expr (t :: SMTSort) where Source #
An SMT-Expression.
For building expressions use the corresponding instances: Boolean, Num, Equatable, ...
With a lot of criminal energy you may build invalid expressions regarding the SMTLib Version 2.6 - Specification. Therefore it is highly recommended to rely on the instances.
Constructors
Instances
class Iteable b a where Source #
If condition (p :: b) then (t :: a) else (f :: a)
>>>ite true "1" "2""1">>>ite false 100 4242
Minimal complete definition
Nothing
Methods
Instances
class Equatable a where Source #
Test two as on equality as SMT-Expression.
You can derive an instance of this class if your type is Generic.
x <- var @RealType
y <- var
assert $ y === x && not (y /== x)
Minimal complete definition
Nothing
Methods
(===) :: a -> a -> Expr BoolSort infix 4 Source #
Test whether two values are equal in the SMT-Problem.
(/==) :: a -> a -> Expr BoolSort infix 4 Source #
Test whether two values are not equal in the SMT-Problem.
Instances
class Equatable a => Orderable a where Source #
Compare two as as SMT-Expression.
You can derive an instance of this class if your type is Generic.
x <- var @RealSort y <- var assert $ x >? y assert $ x === min' 42 100
Minimal complete definition
Nothing
Methods
(<=?) :: a -> a -> Expr BoolSort infix 4 Source #
(>=?) :: a -> a -> Expr BoolSort infix 4 Source #
Instances
min' :: (Orderable a, Iteable (Expr BoolSort) a) => a -> a -> a Source #
Minimum of two as SMT-Expression.
max' :: (Orderable a, Iteable (Expr BoolSort) a) => a -> a -> a Source #
Maximum of two as SMT-Expression.
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.
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), Ord (HaskellType v)) => 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.
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
strAt :: Expr StringSort -> Expr IntSort -> Expr StringSort Source #
Singleton string containing a character at given position or empty string when position is out of range. The leftmost position is 0.
strSubstring :: Expr StringSort -> Expr IntSort -> Expr IntSort -> Expr StringSort Source #
(strSubstring s i n) evaluates to the longest (unscattered) substring
of s of length at most n starting at position i.
It evaluates to the empty string if n is negative or i is not in
the interval [0,l-1] where l is the length of s.
strPrefixOf :: Expr StringSort -> Expr StringSort -> Expr BoolSort Source #
First string is a prefix of second one.
(str.prefixof s t) is true iff s is a prefix of t.
strSuffixOf :: Expr StringSort -> Expr StringSort -> Expr BoolSort Source #
First string is a suffix of second one.
(str.suffixof s t) is true iff s is a suffix of t.
strContains :: Expr StringSort -> Expr StringSort -> Expr BoolSort Source #
First string contains second one
(str.contains s t) iff s contains t.
strIndexOf :: Expr StringSort -> Expr StringSort -> Expr IntSort -> Expr IntSort Source #
Index of first occurrence of second string in first one starting at the position specified by the third argument.
(str.indexof s t i), with 0 <= i <= |s| is the position of the first
occurrence of t in s at or after position i, if any.
Otherwise, it is -1. Note that the result is i whenever i is within
the range [0, |s|] and t is empty.
strReplace :: Expr StringSort -> Expr StringSort -> Expr StringSort -> Expr StringSort Source #
(str.replace s t t') is the string obtained by replacing the first
occurrence of t in s, if any, by t'. Note that if t is empty, the
result is to prepend t' to s; also, if t does not occur in s then
the result is s.
strReplaceAll :: Expr StringSort -> Expr StringSort -> Expr StringSort -> Expr StringSort Source #
(str.replace_all s t t’) is s if t is the empty string. Otherwise, it
is the string obtained from s by replacing all occurrences of t in s
by t’, starting with the first occurrence and proceeding in left-to-right order.