| Safe Haskell | Safe-Inferred |
|---|---|
| Language | GHC2021 |
Language.Hasmtlib.Type.Expr
Description
This module provides the data-type Expr.
It represents SMTLib-expressions via an abstract syntax tree (AST), implemented as GADT.
Variables are just Ints wrapped in a newtype SMTVar with a phantom-type SMTSort.
Usually the end user of this library does not need to deal with this representation. Instead he should rely on the provided instances for building expressions. Some of the main classes of these include:
EquatableandOrderablefor symbolic comparisons,Iteablefor symbolic branching viaite,Booleanfor symbolic bool operations,- Prelude classics like:
Num,Floating,Integral,Bounded, ... for arithmetics Bitsfor BitVec-operations
Besides that, there are also some operations defined by the SMTLib-Standard Version 2.6 that do not fit into any classes
and therefore are exported as plain functions, like for_all or bvConcat.
Synopsis
- newtype SMTVar (t :: SMTSort) = SMTVar {}
- varId :: forall t t. Iso (SMTVar t) (SMTVar t) Int Int
- 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
- Rem :: 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 :: (KnownBvEnc enc, KnownNat n) => Expr (BvSort enc n) -> Expr (BvSort enc n) -> Expr (BvSort enc n)
- BvNor :: (KnownBvEnc enc, KnownNat n) => Expr (BvSort enc n) -> Expr (BvSort enc n) -> Expr (BvSort enc n)
- BvShL :: (KnownBvEnc enc, KnownNat n) => Expr (BvSort enc n) -> Expr (BvSort enc n) -> Expr (BvSort enc n)
- BvLShR :: KnownNat n => Expr (BvSort Unsigned n) -> Expr (BvSort Unsigned n) -> Expr (BvSort Unsigned n)
- BvAShR :: KnownNat n => Expr (BvSort Signed n) -> Expr (BvSort Signed n) -> Expr (BvSort Signed n)
- BvConcat :: (KnownBvEnc enc, KnownNat n, KnownNat m) => Expr (BvSort enc n) -> Expr (BvSort enc m) -> Expr (BvSort enc (n + m))
- BvRotL :: (KnownBvEnc enc, KnownNat n, Integral a) => a -> Expr (BvSort enc n) -> Expr (BvSort enc n)
- BvRotR :: (KnownBvEnc enc, KnownNat n, Integral a) => a -> Expr (BvSort enc n) -> Expr (BvSort enc 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
- 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
- exprSize :: KnownSMTSort t => Expr t -> Integer
- class Equatable a where
- 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
- class GEquatable f 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
- class GEquatable f => GOrderable f where
- class Iteable b a where
- ite :: b -> a -> a -> a
- for_all :: forall t. KnownSMTSort t => (Expr t -> Expr BoolSort) -> Expr BoolSort
- exists :: forall t. KnownSMTSort t => (Expr t -> Expr BoolSort) -> Expr BoolSort
- bvConcat :: (KnownBvEnc enc, KnownNat n, KnownNat m) => Expr (BvSort enc n) -> Expr (BvSort enc m) -> Expr (BvSort enc (n + m))
- 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)
- 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
- toRealSort :: Expr IntSort -> Expr RealSort
- toIntSort :: Expr RealSort -> Expr IntSort
- isIntSort :: Expr RealSort -> Expr BoolSort
SMTVar
newtype SMTVar (t :: SMTSort) Source #
An internal SMT variable with a phantom-type which holds an Int as it's identifier.
Expr type
data Expr (t :: SMTSort) where Source #
An SMT-Expression. For building expressions use the corresponding instances.
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
isLeaf :: Expr t -> Bool Source #
Indicates whether an expression is a leaf. All non-recursive contructors are leafs.
exprSize :: KnownSMTSort t => Expr t -> Integer Source #
Size of the expression.
Counts the amount of operations.
Examples
>>>nodeSize $ x + y === x + y3>>>nodeSize $ false0
Compare
Equatable
Class
class Equatable a where Source #
Symbolically test two values on equality.
A generic default implementation with GEquatable is possible.
Example
x <- var @RealType y <- var assert $ y === x && not (y /== x) && x === 42
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
equal :: (Eq (HaskellType t), KnownSMTSort t, Foldable f) => f (Expr t) -> Expr BoolSort Source #
Symbolically test multiple expressions on equality.
Returns true if given less than two arguments.
distinct :: (Eq (HaskellType t), KnownSMTSort t, Foldable f) => f (Expr t) -> Expr BoolSort Source #
Symbolically test multiple expressions on distinctness.
Returns true if given less than two arguments.
Generic
class GEquatable f where Source #
Instances
| GEquatable (U1 :: k -> Type) Source # | |
| GEquatable (V1 :: k -> Type) Source # | |
| (GEquatable f, GEquatable g) => GEquatable (f :*: g :: k -> Type) Source # | |
| (GEquatable f, GEquatable g) => GEquatable (f :+: g :: k -> Type) Source # | |
| Equatable a => GEquatable (K1 i a :: k -> Type) Source # | |
| GEquatable f => GEquatable (M1 i c f :: k -> Type) Source # | |
Orderable
Class
class Equatable a => Orderable a where Source #
Symbolically compare two values.
A generic default implementation with GOrderable is possible.
Example
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 #
Symbolic evaluation of the minimum of two symbolic values.
max' :: (Orderable a, Iteable (Expr BoolSort) a) => a -> a -> a Source #
Symbolic evaluation of the maximum of two symbolic values.
Generic
class GEquatable f => GOrderable f where Source #
Instances
| GOrderable (U1 :: k -> Type) Source # | |
| GOrderable (V1 :: k -> Type) Source # | |
| (GOrderable f, GOrderable g) => GOrderable (f :*: g :: k -> Type) Source # | |
| (GOrderable f, GOrderable g) => GOrderable (f :+: g :: k -> Type) Source # | |
| Orderable a => GOrderable (K1 i a :: k -> Type) Source # | |
| GOrderable f => GOrderable (M1 i c f :: k -> Type) Source # | |
Iteable
class Iteable b a where Source #
Class that allows branching on predicates of type b on branches of type a.
If predicate (p :: b) then (t :: a) else (f :: a).
There is a default implementation if your type is an Applicative.
Examples
>>>ite True "1" "2""1">>>ite False 100 4242
Minimal complete definition
Nothing
Methods
Instances
Non-class functions
Quantifier
for_all :: forall t. KnownSMTSort t => (Expr t -> Expr BoolSort) -> Expr BoolSort Source #
Universal quantification for any specific SMTSort.
Example
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 #
Existential quantification for any specific SMTSort
Example
assert $
for_all @(BvSort Unsigned 8) $ x ->
exists $ y ->
x - y === 0
The lambdas y is existentially quantified here.
It will only be scoped for the lambdas body.
BitVec
bvConcat :: (KnownBvEnc enc, KnownNat n, KnownNat m) => Expr (BvSort enc n) -> Expr (BvSort enc m) -> Expr (BvSort enc (n + m)) Source #
Concats two bitvectors.
Array
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.
String
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.
(strPrefixof 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.
(strSuffixof s t) is true iff s is a suffix of t.
strContains :: Expr StringSort -> Expr StringSort -> Expr BoolSort Source #
First string contains second one
(strContains 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.
(strIndexof 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 #
(strReplace 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 #
(strReplaceAll 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.