Safe Haskell	Safe-Inferred
Language	GHC2021

Language.Hasmtlib.Type.Expr

Synopsis

newtype SMTVar (t :: SMTSort) = SMTVar {
- _varId :: Int
}
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)
- 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 :: SMTVar t -> Expr t
- Constant :: Value t -> Expr t
- Plus :: 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 :: Expr IntSort -> Expr IntSort -> Expr IntSort
- IDiv :: Expr IntSort -> Expr IntSort -> Expr IntSort
- 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
- BvNot :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n)
- BvAnd :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
- BvOr :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
- BvXor :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
- BvNand :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
- BvNor :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
- BvNeg :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n)
- BvAdd :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
- BvSub :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
- BvMul :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
- BvuDiv :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
- BvuRem :: 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, 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)
- BvuLT :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr BoolSort
- BvuLTHE :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr BoolSort
- BvuGTHE :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr BoolSort
- BvuGT :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr BoolSort
- ArrSelect :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => 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
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)
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.

Constructors

SMTVar
Fields _varId :: Int

Instances

Instances details

Generic (SMTVar t) Source #
Instance details Defined in Language.Hasmtlib.Internal.Expr Associated Types type Rep (SMTVar t) :: Type -> Type # Methods from :: SMTVar t -> Rep (SMTVar t) x # to :: Rep (SMTVar t) x -> SMTVar t #
Show (SMTVar t) Source #
Instance details Defined in Language.Hasmtlib.Internal.Expr Methods showsPrec :: Int -> SMTVar t -> ShowS # show :: SMTVar t -> String # showList :: [SMTVar t] -> ShowS #
Eq (SMTVar t) Source #
Instance details Defined in Language.Hasmtlib.Internal.Expr Methods (==) :: SMTVar t -> SMTVar t -> Bool # (/=) :: SMTVar t -> SMTVar t -> Bool #
Ord (SMTVar t) Source #
Instance details 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) Source #
Instance details Defined in Language.Hasmtlib.Internal.Expr Methods render :: SMTVar t -> Builder Source #
type Rep (SMTVar t) Source #
Instance details Defined in Language.Hasmtlib.Internal.Expr type Rep (SMTVar t) = D1 ('MetaData "SMTVar" "Language.Hasmtlib.Internal.Expr" "hasmtlib-2.3.2-inplace" 'True) (C1 ('MetaCons "SMTVar" 'PrefixI 'True) (S1 ('MetaSel ('Just "_varId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)))

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

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)
StringValue :: HaskellType StringSort -> Value StringSort

Instances

Instances details

Show (Value t) Source #
Instance details Defined in Language.Hasmtlib.Internal.Expr Methods showsPrec :: Int -> Value t -> ShowS # show :: Value t -> String # showList :: [Value t] -> ShowS #
Eq (HaskellType t) => Eq (Value t) Source #
Instance details Defined in Language.Hasmtlib.Internal.Expr Methods (==) :: Value t -> Value t -> Bool # (/=) :: Value t -> Value t -> Bool #
Ord (HaskellType t) => Ord (Value t) Source #
Instance details Defined in Language.Hasmtlib.Internal.Expr 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 #
Render (Value t) Source #
Instance details Defined in Language.Hasmtlib.Internal.Expr Methods render :: Value t -> Builder Source #

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) where Source #

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

Constructors

Var :: SMTVar t -> Expr t
Constant :: Value t -> Expr t
Plus :: 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 :: Expr IntSort -> Expr IntSort -> Expr IntSort
IDiv :: Expr IntSort -> Expr IntSort -> Expr IntSort
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
BvNot :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n)
BvAnd :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
BvOr :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
BvXor :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
BvNand :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
BvNor :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
BvNeg :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n)
BvAdd :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
BvSub :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
BvMul :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
BvuDiv :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
BvuRem :: 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, 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)
BvuLT :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr BoolSort
BvuLTHE :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr BoolSort
BvuGTHE :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr BoolSort
BvuGT :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr BoolSort
ArrSelect :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => 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

Instances

Instances details

IsString (Expr 'StringSort) Source #
Instance details Defined in Language.Hasmtlib.Internal.Expr Methods fromString :: String -> Expr 'StringSort #
Monoid (Expr 'StringSort) Source #
Instance details Defined in Language.Hasmtlib.Internal.Expr Methods mempty :: Expr 'StringSort # mappend :: Expr 'StringSort -> Expr 'StringSort -> Expr 'StringSort # mconcat :: [Expr 'StringSort] -> Expr 'StringSort #
Semigroup (Expr 'StringSort) Source #
Instance details Defined in Language.Hasmtlib.Internal.Expr Methods (<>) :: Expr 'StringSort -> Expr 'StringSort -> Expr 'StringSort # sconcat :: NonEmpty (Expr 'StringSort) -> Expr 'StringSort # stimes :: Integral b => b -> Expr 'StringSort -> Expr 'StringSort #
Bounded (Expr 'BoolSort) Source #
Instance details Defined in Language.Hasmtlib.Internal.Expr Methods minBound :: Expr 'BoolSort # maxBound :: Expr 'BoolSort #
KnownNat n => Bounded (Expr ('BvSort n)) Source #
Instance details Defined in Language.Hasmtlib.Internal.Expr Methods minBound :: Expr ('BvSort n) # maxBound :: Expr ('BvSort n) #
Floating (Expr 'RealSort) Source #
Instance details 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)) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details Defined in Language.Hasmtlib.Internal.Expr.Num Methods (/) :: Expr 'RealSort -> Expr 'RealSort -> Expr 'RealSort # recip :: Expr 'RealSort -> Expr 'RealSort # fromRational :: Rational -> Expr 'RealSort #
KnownSMTSort t => Show (Expr t) Source #
Instance details Defined in Language.Hasmtlib.Internal.Expr Methods showsPrec :: Int -> Expr t -> ShowS # show :: Expr t -> String # showList :: [Expr t] -> ShowS #
Boolean (Expr 'BoolSort) Source #
Instance details Defined in Language.Hasmtlib.Internal.Expr Methods bool :: Bool -> Expr 'BoolSort Source # true :: Expr 'BoolSort Source # false :: Expr 'BoolSort Source # (&&) :: Expr 'BoolSort -> Expr 'BoolSort -> Expr 'BoolSort Source # (\|\|) :: Expr 'BoolSort -> Expr 'BoolSort -> Expr 'BoolSort Source # (==>) :: Expr 'BoolSort -> Expr 'BoolSort -> Expr 'BoolSort Source # (<==) :: Expr 'BoolSort -> Expr 'BoolSort -> Expr 'BoolSort Source # (<==>) :: Expr 'BoolSort -> Expr 'BoolSort -> Expr 'BoolSort Source # not :: Expr 'BoolSort -> Expr 'BoolSort Source # xor :: Expr 'BoolSort -> Expr 'BoolSort -> Expr 'BoolSort Source #
KnownNat n => Boolean (Expr ('BvSort n)) Source #
Instance details Defined in Language.Hasmtlib.Internal.Expr Methods bool :: Bool -> Expr ('BvSort n) Source # true :: Expr ('BvSort n) Source # false :: Expr ('BvSort n) Source # (&&) :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n) Source # (\|\|) :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n) Source # (==>) :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n) Source # (<==) :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n) Source # (<==>) :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n) Source # not :: Expr ('BvSort n) -> Expr ('BvSort n) Source # xor :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n) Source #
KnownSMTSort t => Codec (Expr t) Source #	Decode and evaluate expressions
Instance details Defined in Language.Hasmtlib.Codec Associated Types type Decoded (Expr t) Source # Methods decode :: Solution -> Expr t -> Maybe (Decoded (Expr t)) Source # encode :: Decoded (Expr t) -> Expr t Source #
(KnownSMTSort t, Eq (HaskellType t)) => Equatable (Expr t) Source #
Instance details Defined in Language.Hasmtlib.Equatable Methods (===) :: Expr t -> Expr t -> Expr 'BoolSort Source # (/==) :: Expr t -> Expr t -> Expr 'BoolSort Source #
KnownNat n => Integraled (Expr ('BvSort n)) Source #
Instance details Defined in Language.Hasmtlib.Internal.Expr.Num Methods quot :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n) Source # rem :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n) Source # div :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n) Source # mod :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n) Source # quotRem :: Expr ('BvSort n) -> Expr ('BvSort n) -> (Expr ('BvSort n), Expr ('BvSort n)) Source # divMod :: Expr ('BvSort n) -> Expr ('BvSort n) -> (Expr ('BvSort n), Expr ('BvSort n)) Source #
Integraled (Expr 'IntSort) Source #
Instance details Defined in Language.Hasmtlib.Internal.Expr.Num Methods quot :: Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort Source # rem :: Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort Source # div :: Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort Source # mod :: Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort Source # quotRem :: Expr 'IntSort -> Expr 'IntSort -> (Expr 'IntSort, Expr 'IntSort) Source # divMod :: Expr 'IntSort -> Expr 'IntSort -> (Expr 'IntSort, Expr 'IntSort) Source #
KnownSMTSort t => Render (Expr t) Source #
Instance details Defined in Language.Hasmtlib.Internal.Expr Methods render :: Expr t -> Builder Source #
KnownNat n => Orderable (Expr ('BvSort n)) Source #
Instance details Defined in Language.Hasmtlib.Orderable Methods (<=?) :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr 'BoolSort Source # (>=?) :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr 'BoolSort Source # (<?) :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr 'BoolSort Source # (>?) :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr 'BoolSort Source #
Orderable (Expr 'IntSort) Source #
Instance details Defined in Language.Hasmtlib.Orderable Methods (<=?) :: Expr 'IntSort -> Expr 'IntSort -> Expr 'BoolSort Source # (>=?) :: Expr 'IntSort -> Expr 'IntSort -> Expr 'BoolSort Source # (<?) :: Expr 'IntSort -> Expr 'IntSort -> Expr 'BoolSort Source # (>?) :: Expr 'IntSort -> Expr 'IntSort -> Expr 'BoolSort Source #
Orderable (Expr 'RealSort) Source #
Instance details Defined in Language.Hasmtlib.Orderable Methods (<=?) :: Expr 'RealSort -> Expr 'RealSort -> Expr 'BoolSort Source # (>=?) :: Expr 'RealSort -> Expr 'RealSort -> Expr 'BoolSort Source # (<?) :: Expr 'RealSort -> Expr 'RealSort -> Expr 'BoolSort Source # (>?) :: Expr 'RealSort -> Expr 'RealSort -> Expr 'BoolSort Source #
Orderable (Expr 'StringSort) Source #	Lexicographic ordering for `(<?)` and reflexive closure of lexicographic ordering for `Orderable`
Instance details Defined in Language.Hasmtlib.Orderable Methods (<=?) :: Expr 'StringSort -> Expr 'StringSort -> Expr 'BoolSort Source # (>=?) :: Expr 'StringSort -> Expr 'StringSort -> Expr 'BoolSort Source # (<?) :: Expr 'StringSort -> Expr 'StringSort -> Expr 'BoolSort Source # (>?) :: Expr 'StringSort -> Expr 'StringSort -> Expr 'BoolSort Source #
KnownSMTSort t => Variable (Expr t) Source #
Instance details Defined in Language.Hasmtlib.Variable Methods variable :: MonadSMT s m => m (Expr t) Source #
(KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Ixed (Expr ('ArraySort k v)) Source #
Instance details Defined in Language.Hasmtlib.Lens Methods ix :: Index (Expr ('ArraySort k v)) -> Traversal' (Expr ('ArraySort k v)) (IxValue (Expr ('ArraySort k v))) #
Ixed (Expr 'StringSort) Source #
Instance details Defined in Language.Hasmtlib.Lens Methods ix :: Index (Expr 'StringSort) -> Traversal' (Expr 'StringSort) (IxValue (Expr 'StringSort)) #
AsEmpty (Expr 'StringSort) Source #
Instance details Defined in Language.Hasmtlib.Lens Methods _Empty :: Prism' (Expr 'StringSort) () #
KnownSMTSort t => Plated (Expr t) Source #	Caution for quantified expressions:* 'plate-function' `f` will only be applied if quantification already has taken place.(&&) Therefore make sure `quantify` has been run before. Otherwise the quantified expression and therefore all it's sub-expressions will not have `f` applied.
Instance details Defined in Language.Hasmtlib.Lens Methods plate :: Traversal' (Expr t) (Expr t) #
Prefixed (Expr 'StringSort) Source #
Instance details Defined in Language.Hasmtlib.Lens Methods prefixed :: Expr 'StringSort -> Prism' (Expr 'StringSort) (Expr 'StringSort) #
Suffixed (Expr 'StringSort) Source #
Instance details Defined in Language.Hasmtlib.Lens Methods suffixed :: Expr 'StringSort -> Prism' (Expr 'StringSort) (Expr 'StringSort) #
Iteable (Expr 'BoolSort) () Source #
Instance details Defined in Language.Hasmtlib.Iteable Methods ite :: Expr 'BoolSort -> () -> () -> () Source #
Iteable (Expr 'BoolSort) a => Iteable (Expr 'BoolSort) (Identity a) Source #
Instance details Defined in Language.Hasmtlib.Iteable Methods ite :: Expr 'BoolSort -> Identity a -> Identity a -> Identity a Source #
Iteable (Expr 'BoolSort) a => Iteable (Expr 'BoolSort) (First a) Source #
Instance details Defined in Language.Hasmtlib.Iteable Methods ite :: Expr 'BoolSort -> First a -> First a -> First a Source #
Iteable (Expr 'BoolSort) a => Iteable (Expr 'BoolSort) (Last a) Source #
Instance details Defined in Language.Hasmtlib.Iteable Methods ite :: Expr 'BoolSort -> Last a -> Last a -> Last a Source #
Iteable (Expr 'BoolSort) a => Iteable (Expr 'BoolSort) (Dual a) Source #
Instance details Defined in Language.Hasmtlib.Iteable Methods ite :: Expr 'BoolSort -> Dual a -> Dual a -> Dual a Source #
Iteable (Expr 'BoolSort) a => Iteable (Expr 'BoolSort) (Product a) Source #
Instance details Defined in Language.Hasmtlib.Iteable Methods ite :: Expr 'BoolSort -> Product a -> Product a -> Product a Source #
Iteable (Expr 'BoolSort) a => Iteable (Expr 'BoolSort) (Sum a) Source #
Instance details Defined in Language.Hasmtlib.Iteable Methods ite :: Expr 'BoolSort -> Sum a -> Sum a -> Sum a Source #
Iteable (Expr 'BoolSort) a => Iteable (Expr 'BoolSort) (Seq a) Source #
Instance details Defined in Language.Hasmtlib.Iteable Methods ite :: Expr 'BoolSort -> Seq a -> Seq a -> Seq a Source #
Iteable (Expr 'BoolSort) a => Iteable (Expr 'BoolSort) (Tree a) Source #
Instance details Defined in Language.Hasmtlib.Iteable Methods ite :: Expr 'BoolSort -> Tree a -> Tree a -> Tree a Source #
Iteable (Expr 'BoolSort) (Expr t) Source #
Instance details Defined in Language.Hasmtlib.Iteable Methods ite :: Expr 'BoolSort -> Expr t -> Expr t -> Expr t Source #
Iteable (Expr 'BoolSort) a => Iteable (Expr 'BoolSort) (Maybe a) Source #
Instance details Defined in Language.Hasmtlib.Iteable Methods ite :: Expr 'BoolSort -> Maybe a -> Maybe a -> Maybe a Source #
Iteable (Expr 'BoolSort) a => Iteable (Expr 'BoolSort) [a] Source #
Instance details Defined in Language.Hasmtlib.Iteable Methods ite :: Expr 'BoolSort -> [a] -> [a] -> [a] Source #
Cons (Expr 'StringSort) (Expr 'StringSort) (Expr 'StringSort) (Expr 'StringSort) Source #
Instance details Defined in Language.Hasmtlib.Lens Methods _Cons :: Prism (Expr 'StringSort) (Expr 'StringSort) (Expr 'StringSort, Expr 'StringSort) (Expr 'StringSort, Expr 'StringSort) #
Snoc (Expr 'StringSort) (Expr 'StringSort) (Expr 'StringSort) (Expr 'StringSort) Source #
Instance details Defined in Language.Hasmtlib.Lens Methods _Snoc :: Prism (Expr 'StringSort) (Expr 'StringSort) (Expr 'StringSort, Expr 'StringSort) (Expr 'StringSort, Expr 'StringSort) #
(Iteable (Expr 'BoolSort) a, Iteable (Expr 'BoolSort) b) => Iteable (Expr 'BoolSort) (a, b) Source #
Instance details Defined in Language.Hasmtlib.Iteable Methods ite :: Expr 'BoolSort -> (a, b) -> (a, b) -> (a, b) Source #
(Iteable (Expr 'BoolSort) a, Iteable (Expr 'BoolSort) b, Iteable (Expr 'BoolSort) c) => Iteable (Expr 'BoolSort) (a, b, c) Source #
Instance details Defined in Language.Hasmtlib.Iteable Methods ite :: Expr 'BoolSort -> (a, b, c) -> (a, b, c) -> (a, b, c) Source #
(Iteable (Expr 'BoolSort) a, Iteable (Expr 'BoolSort) b, Iteable (Expr 'BoolSort) c, Iteable (Expr 'BoolSort) d) => Iteable (Expr 'BoolSort) (a, b, c, d) Source #
Instance details Defined in Language.Hasmtlib.Iteable Methods ite :: Expr 'BoolSort -> (a, b, c, d) -> (a, b, c, d) -> (a, b, c, d) Source #
(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) Source #
Instance details Defined in Language.Hasmtlib.Iteable Methods ite :: Expr 'BoolSort -> (a, b, c, d, e) -> (a, b, c, d, e) -> (a, b, c, d, e) Source #
(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) Source #
Instance details 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) Source #
(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) Source #
Instance details 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) Source #
(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) Source #
Instance details 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) Source #
type Decoded (Expr t) Source #
Instance details Defined in Language.Hasmtlib.Codec type Decoded (Expr t) = HaskellType t
type Index (Expr ('ArraySort k v)) Source #
Instance details Defined in Language.Hasmtlib.Lens type Index (Expr ('ArraySort k v)) = Expr k
type Index (Expr 'StringSort) Source #
Instance details Defined in Language.Hasmtlib.Lens type Index (Expr 'StringSort) = Expr 'IntSort
type IxValue (Expr ('ArraySort k v)) Source #
Instance details Defined in Language.Hasmtlib.Lens type IxValue (Expr ('ArraySort k v)) = Expr v
type IxValue (Expr 'StringSort) Source #
Instance details Defined in Language.Hasmtlib.Lens type IxValue (Expr 'StringSort) = Expr 'StringSort

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

toIntSort :: Expr RealSort -> Expr IntSort Source #

Converts an expression of type RealSort to type IntSort.

toRealSort :: Expr IntSort -> Expr RealSort Source #

Converts an expression of type IntSort to type RealSort.

isIntSort :: Expr RealSort -> Expr BoolSort Source #

Checks whether an expression of type RealSort may be safely converted to type IntSort.

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.

strLength :: Expr StringSort -> Expr IntSort Source #

Length of a 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. (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.