Language.Hasmtlib.Type.Expr

Documentation

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

Generic (SMTVar t)

Defined in Language.Hasmtlib.Type.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)

Defined in Language.Hasmtlib.Type.Expr

Methods

showsPrec :: Int -> SMTVar t -> ShowS

show :: SMTVar t -> String

showList :: [SMTVar t] -> ShowS

Eq (SMTVar t)

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Ord (SMTVar t)

Defined in Language.Hasmtlib.Type.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.Type.Expr

Methods

render :: SMTVar t -> Builder

type Rep (SMTVar t)

Defined in Language.Hasmtlib.Type.Expr

type Rep (SMTVar t) = D1 ('MetaData "SMTVar" "Language.Hasmtlib.Type.Expr" "hasmtlib-2.4.0-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

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 :: KnownNat n => HaskellType (BvSort n) -> Value (BvSort n)

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

StringValue :: HaskellType StringSort -> Value StringSort

Instances

GEq Value

Defined in Language.Hasmtlib.Type.Expr

Methods

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

Show (Value t)

Defined in Language.Hasmtlib.Type.Expr

Methods

showsPrec :: Int -> Value t -> ShowS

show :: Value t -> String

showList :: [Value t] -> ShowS

Eq (HaskellType t) => Eq (Value t)

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Ord (HaskellType t) => Ord (Value t)

Defined in Language.Hasmtlib.Type.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)

Defined in Language.Hasmtlib.Type.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.

type SomeKnownSMTSort f = SomeSMTSort '[KnownSMTSort] f

An existential wrapper that hides some known SMTSort.

data Expr (t :: SMTSort) where

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), Eq (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

Just v if quantified var has been created already, Nothing otherwise

Exists :: KnownSMTSort t => Maybe (SMTVar t) -> (Expr t -> Expr BoolSort) -> Expr BoolSort

Just v if quantified var has been created already, Nothing otherwise

Instances

GNFData Expr

Defined in Language.Hasmtlib.Type.Expr

Methods

grnf :: forall (a :: k). Expr a -> ()

Uniplate1 Expr '[KnownSMTSort]

Caution for quantified expressions: uniplate1 will only be applied if quantification has taken place already.

Defined in Language.Hasmtlib.Type.Expr

Methods

uniplate1 :: forall m (b :: k). (Applicative m, AllC '[KnownSMTSort] b) => (forall (a :: k). AllC '[KnownSMTSort] a => Expr a -> m (Expr a)) -> Expr b -> m (Expr b)

IsString (Expr 'StringSort)

Defined in Language.Hasmtlib.Type.Expr

Methods

fromString :: String -> Expr 'StringSort

Monoid (Expr 'StringSort)

Defined in Language.Hasmtlib.Type.Expr

Methods

mempty :: Expr 'StringSort

mappend :: Expr 'StringSort -> Expr 'StringSort -> Expr 'StringSort

mconcat :: [Expr 'StringSort] -> Expr 'StringSort

Semigroup (Expr 'StringSort)

Defined in Language.Hasmtlib.Type.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)

Defined in Language.Hasmtlib.Type.Expr

Methods

minBound :: Expr 'BoolSort

maxBound :: Expr 'BoolSort

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

Defined in Language.Hasmtlib.Type.Expr

Methods

minBound :: Expr ('BvSort n)

maxBound :: Expr ('BvSort n)

Floating (Expr 'RealSort)

Not in the SMTLib2.6-standard. Solvers like CVC5 and MathSAT support it though.

Defined in Language.Hasmtlib.Type.Expr

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

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

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

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

Methods

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

recip :: Expr 'RealSort -> Expr 'RealSort

fromRational :: Rational -> Expr 'RealSort

KnownSMTSort t => Show (Expr t)

Defined in Language.Hasmtlib.Type.Expr

Methods

showsPrec :: Int -> Expr t -> ShowS

show :: Expr t -> String

showList :: [Expr t] -> ShowS

Boolean (Expr 'BoolSort)

Defined in Language.Hasmtlib.Type.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

(<==) :: 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.Type.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)

(<==) :: 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

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

Defined in Language.Hasmtlib.Type.Expr

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

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

Methods

render :: Expr t -> Builder

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

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

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

Defined in Language.Hasmtlib.Type.Expr

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

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

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

Orderable (Expr 'StringSort)

Lexicographic ordering for (<?) and reflexive closure of lexicographic ordering for Orderable

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

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

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

KnownSMTSort t => Variable (Expr t)

Defined in Language.Hasmtlib.Variable

Methods

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

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

Defined in Language.Hasmtlib.Type.Expr

Methods

ix :: Index (Expr ('ArraySort k v)) -> Traversal' (Expr ('ArraySort k v)) (IxValue (Expr ('ArraySort k v)))

Ixed (Expr 'StringSort)

Defined in Language.Hasmtlib.Type.Expr

Methods

ix :: Index (Expr 'StringSort) -> Traversal' (Expr 'StringSort) (IxValue (Expr 'StringSort))

AsEmpty (Expr 'StringSort)

Defined in Language.Hasmtlib.Type.Expr

Methods

_Empty :: Prism' (Expr 'StringSort) ()

KnownSMTSort t => Plated (Expr t)

Caution for quantified expressions: plate will only be applied if quantification has taken place already.

Defined in Language.Hasmtlib.Type.Expr

Methods

plate :: Traversal' (Expr t) (Expr t)

Prefixed (Expr 'StringSort)

Defined in Language.Hasmtlib.Type.Expr

Methods

prefixed :: Expr 'StringSort -> Prism' (Expr 'StringSort) (Expr 'StringSort)

Suffixed (Expr 'StringSort)

Defined in Language.Hasmtlib.Type.Expr

Methods

suffixed :: Expr 'StringSort -> Prism' (Expr 'StringSort) (Expr 'StringSort)

Iteable (Expr 'BoolSort) ()

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Defined in Language.Hasmtlib.Type.Expr

Methods

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

Iteable (Expr 'BoolSort) (Expr t)

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Defined in Language.Hasmtlib.Type.Expr

Methods

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

Cons (Expr 'StringSort) (Expr 'StringSort) (Expr 'StringSort) (Expr 'StringSort)

Defined in Language.Hasmtlib.Type.Expr

Methods

_Cons :: Prism (Expr 'StringSort) (Expr 'StringSort) (Expr 'StringSort, Expr 'StringSort) (Expr 'StringSort, Expr 'StringSort)

Snoc (Expr 'StringSort) (Expr 'StringSort) (Expr 'StringSort) (Expr 'StringSort)

Defined in Language.Hasmtlib.Type.Expr

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)

Defined in Language.Hasmtlib.Type.Expr

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

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

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

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

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

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

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

type Index (Expr ('ArraySort k v))

Defined in Language.Hasmtlib.Type.Expr

type Index (Expr ('ArraySort k v)) = Expr k

type Index (Expr 'StringSort)

Defined in Language.Hasmtlib.Type.Expr

type Index (Expr 'StringSort) = Expr 'IntSort

type IxValue (Expr ('ArraySort k v))

Defined in Language.Hasmtlib.Type.Expr

type IxValue (Expr ('ArraySort k v)) = Expr v

type IxValue (Expr 'StringSort)

Defined in Language.Hasmtlib.Type.Expr

type IxValue (Expr 'StringSort) = Expr 'StringSort

isLeaf :: Expr t -> Bool

class Iteable b a where

If condition (p :: b) then (t :: a) else (f :: a)

>>> ite true "1" "2"
    "1"
>>> ite false 100 42
    42

Minimal complete definition

Nothing

Methods

ite :: b -> a -> a -> a

default ite :: (Iteable b c, Applicative f, f c ~ a) => b -> a -> a -> a

Instances

Iteable Bool a

Defined in Language.Hasmtlib.Type.Expr

Methods

ite :: Bool -> a -> a -> a

Iteable (Expr 'BoolSort) ()

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Defined in Language.Hasmtlib.Type.Expr

Methods

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

Iteable (Expr 'BoolSort) (Expr t)

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Defined in Language.Hasmtlib.Type.Expr

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

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

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

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

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

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

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)

class Equatable a where

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

Test whether two values are equal in the SMT-Problem.

default (===) :: (Generic a, GEquatable (Rep a)) => a -> a -> Expr BoolSort

(/==) :: a -> a -> Expr BoolSort infix 4

Test whether two values are not equal in the SMT-Problem.

Instances

Equatable Void

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Equatable Int16

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Equatable Int32

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Equatable Int64

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Equatable Int8

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Equatable Word16

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Equatable Word32

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Equatable Word64

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Equatable Word8

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Equatable Ordering

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Equatable Integer

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Equatable Natural

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Equatable ()

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Equatable Bool

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Equatable Char

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Equatable Double

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Equatable Float

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Equatable Int

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Equatable Word

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Equatable a => Equatable (Identity a)

Defined in Language.Hasmtlib.Type.Expr

Methods

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

(/==) :: Identity a -> Identity a -> Expr 'BoolSort

Equatable a => Equatable (First a)

Defined in Language.Hasmtlib.Type.Expr

Methods

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

(/==) :: First a -> First a -> Expr 'BoolSort

Equatable a => Equatable (Last a)

Defined in Language.Hasmtlib.Type.Expr

Methods

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

(/==) :: Last a -> Last a -> Expr 'BoolSort

Equatable a => Equatable (Dual a)

Defined in Language.Hasmtlib.Type.Expr

Methods

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

(/==) :: Dual a -> Dual a -> Expr 'BoolSort

Equatable a => Equatable (Product a)

Defined in Language.Hasmtlib.Type.Expr

Methods

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

(/==) :: Product a -> Product a -> Expr 'BoolSort

Equatable a => Equatable (Sum a)

Defined in Language.Hasmtlib.Type.Expr

Methods

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

(/==) :: Sum a -> Sum a -> Expr 'BoolSort

Equatable a => Equatable (Tree a)

Defined in Language.Hasmtlib.Type.Expr

Methods

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

(/==) :: Tree a -> Tree a -> Expr 'BoolSort

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

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

Equatable a => Equatable (Maybe a)

Defined in Language.Hasmtlib.Type.Expr

Methods

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

(/==) :: Maybe a -> Maybe a -> Expr 'BoolSort

Equatable a => Equatable [a]

Defined in Language.Hasmtlib.Type.Expr

Methods

(===) :: [a] -> [a] -> Expr 'BoolSort

(/==) :: [a] -> [a] -> Expr 'BoolSort

(Equatable a, Equatable b) => Equatable (Either a b)

Defined in Language.Hasmtlib.Type.Expr

Methods

(===) :: Either a b -> Either a b -> Expr 'BoolSort

(/==) :: Either a b -> Either a b -> Expr 'BoolSort

(Equatable a, Equatable b) => Equatable (a, b)

Defined in Language.Hasmtlib.Type.Expr

Methods

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

(/==) :: (a, b) -> (a, b) -> Expr 'BoolSort

(Equatable a, Equatable b, Equatable c) => Equatable (a, b, c)

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

(Equatable a, Equatable b, Equatable c, Equatable d) => Equatable (a, b, c, d)

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

(Equatable a, Equatable b, Equatable c, Equatable d, Equatable e) => Equatable (a, b, c, d, e)

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

(Equatable a, Equatable b, Equatable c, Equatable d, Equatable e, Equatable f) => Equatable (a, b, c, d, e, f)

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

(Equatable a, Equatable b, Equatable c, Equatable d, Equatable e, Equatable f, Equatable g) => Equatable (a, b, c, d, e, f, g)

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

(Equatable a, Equatable b, Equatable c, Equatable d, Equatable e, Equatable f, Equatable g, Equatable h) => Equatable (a, b, c, d, e, f, g, h)

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

class GEquatable f where

Methods

(===#) :: f a -> f a -> Expr BoolSort

Instances

GEquatable (U1 :: k -> Type)

Defined in Language.Hasmtlib.Type.Expr

Methods

(===#) :: forall (a :: k0). U1 a -> U1 a -> Expr 'BoolSort

GEquatable (V1 :: k -> Type)

Defined in Language.Hasmtlib.Type.Expr

Methods

(===#) :: forall (a :: k0). V1 a -> V1 a -> Expr 'BoolSort

(GEquatable f, GEquatable g) => GEquatable (f :*: g :: k -> Type)

Defined in Language.Hasmtlib.Type.Expr

Methods

(===#) :: forall (a :: k0). (f :*: g) a -> (f :*: g) a -> Expr 'BoolSort

(GEquatable f, GEquatable g) => GEquatable (f :+: g :: k -> Type)

Defined in Language.Hasmtlib.Type.Expr

Methods

(===#) :: forall (a :: k0). (f :+: g) a -> (f :+: g) a -> Expr 'BoolSort

Equatable a => GEquatable (K1 i a :: k -> Type)

Defined in Language.Hasmtlib.Type.Expr

Methods

(===#) :: forall (a0 :: k0). K1 i a a0 -> K1 i a a0 -> Expr 'BoolSort

GEquatable f => GEquatable (M1 i c f :: k -> Type)

Defined in Language.Hasmtlib.Type.Expr

Methods

(===#) :: forall (a :: k0). M1 i c f a -> M1 i c f a -> Expr 'BoolSort

class Equatable a => Orderable a where

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

default (<=?) :: (Generic a, GOrderable (Rep a)) => a -> a -> Expr BoolSort

(>=?) :: a -> a -> Expr BoolSort infix 4

(<?) :: a -> a -> Expr BoolSort infix 4

(>?) :: a -> a -> Expr BoolSort infix 4

Instances

Orderable Void

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

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

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

Orderable Int16

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

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

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

Orderable Int32

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

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

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

Orderable Int64

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

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

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

Orderable Int8

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

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

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

Orderable Word16

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

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

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

Orderable Word32

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

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

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

Orderable Word64

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

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

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

Orderable Word8

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

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

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

Orderable Ordering

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

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

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

Orderable Integer

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

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

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

Orderable Natural

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

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

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

Orderable ()

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

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

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

Orderable Bool

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

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

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

Orderable Char

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

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

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

Orderable Double

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

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

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

Orderable Float

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

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

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

Orderable Int

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

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

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

Orderable Word

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

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

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

Orderable a => Orderable (Identity a)

Defined in Language.Hasmtlib.Type.Expr

Methods

(<=?) :: Identity a -> Identity a -> Expr 'BoolSort

(>=?) :: Identity a -> Identity a -> Expr 'BoolSort

(<?) :: Identity a -> Identity a -> Expr 'BoolSort

(>?) :: Identity a -> Identity a -> Expr 'BoolSort

Orderable a => Orderable (First a)

Defined in Language.Hasmtlib.Type.Expr

Methods

(<=?) :: First a -> First a -> Expr 'BoolSort

(>=?) :: First a -> First a -> Expr 'BoolSort

(<?) :: First a -> First a -> Expr 'BoolSort

(>?) :: First a -> First a -> Expr 'BoolSort

Orderable a => Orderable (Last a)

Defined in Language.Hasmtlib.Type.Expr

Methods

(<=?) :: Last a -> Last a -> Expr 'BoolSort

(>=?) :: Last a -> Last a -> Expr 'BoolSort

(<?) :: Last a -> Last a -> Expr 'BoolSort

(>?) :: Last a -> Last a -> Expr 'BoolSort

Orderable a => Orderable (Dual a)

Defined in Language.Hasmtlib.Type.Expr

Methods

(<=?) :: Dual a -> Dual a -> Expr 'BoolSort

(>=?) :: Dual a -> Dual a -> Expr 'BoolSort

(<?) :: Dual a -> Dual a -> Expr 'BoolSort

(>?) :: Dual a -> Dual a -> Expr 'BoolSort

Orderable a => Orderable (Product a)

Defined in Language.Hasmtlib.Type.Expr

Methods

(<=?) :: Product a -> Product a -> Expr 'BoolSort

(>=?) :: Product a -> Product a -> Expr 'BoolSort

(<?) :: Product a -> Product a -> Expr 'BoolSort

(>?) :: Product a -> Product a -> Expr 'BoolSort

Orderable a => Orderable (Sum a)

Defined in Language.Hasmtlib.Type.Expr

Methods

(<=?) :: Sum a -> Sum a -> Expr 'BoolSort

(>=?) :: Sum a -> Sum a -> Expr 'BoolSort

(<?) :: Sum a -> Sum a -> Expr 'BoolSort

(>?) :: Sum a -> Sum a -> Expr 'BoolSort

Orderable a => Orderable (Tree a)

Defined in Language.Hasmtlib.Type.Expr

Methods

(<=?) :: Tree a -> Tree a -> Expr 'BoolSort

(>=?) :: Tree a -> Tree a -> Expr 'BoolSort

(<?) :: Tree a -> Tree a -> Expr 'BoolSort

(>?) :: Tree a -> Tree a -> Expr 'BoolSort

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

Defined in Language.Hasmtlib.Type.Expr

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

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

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

Orderable (Expr 'StringSort)

Lexicographic ordering for (<?) and reflexive closure of lexicographic ordering for Orderable

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

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

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

Orderable a => Orderable (Maybe a)

Defined in Language.Hasmtlib.Type.Expr

Methods

(<=?) :: Maybe a -> Maybe a -> Expr 'BoolSort

(>=?) :: Maybe a -> Maybe a -> Expr 'BoolSort

(<?) :: Maybe a -> Maybe a -> Expr 'BoolSort

(>?) :: Maybe a -> Maybe a -> Expr 'BoolSort

Orderable a => Orderable [a]

Defined in Language.Hasmtlib.Type.Expr

Methods

(<=?) :: [a] -> [a] -> Expr 'BoolSort

(>=?) :: [a] -> [a] -> Expr 'BoolSort

(<?) :: [a] -> [a] -> Expr 'BoolSort

(>?) :: [a] -> [a] -> Expr 'BoolSort

(Orderable a, Orderable b) => Orderable (Either a b)

Defined in Language.Hasmtlib.Type.Expr

Methods

(<=?) :: Either a b -> Either a b -> Expr 'BoolSort

(>=?) :: Either a b -> Either a b -> Expr 'BoolSort

(<?) :: Either a b -> Either a b -> Expr 'BoolSort

(>?) :: Either a b -> Either a b -> Expr 'BoolSort

(Orderable a, Orderable b) => Orderable (a, b)

Defined in Language.Hasmtlib.Type.Expr

Methods

(<=?) :: (a, b) -> (a, b) -> Expr 'BoolSort

(>=?) :: (a, b) -> (a, b) -> Expr 'BoolSort

(<?) :: (a, b) -> (a, b) -> Expr 'BoolSort

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

(Orderable a, Orderable b, Orderable c) => Orderable (a, b, c)

Defined in Language.Hasmtlib.Type.Expr

Methods

(<=?) :: (a, b, c) -> (a, b, c) -> Expr 'BoolSort

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

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

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

(Orderable a, Orderable b, Orderable c, Orderable d) => Orderable (a, b, c, d)

Defined in Language.Hasmtlib.Type.Expr

Methods

(<=?) :: (a, b, c, d) -> (a, b, c, d) -> Expr 'BoolSort

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

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

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

(Orderable a, Orderable b, Orderable c, Orderable d, Orderable e) => Orderable (a, b, c, d, e)

Defined in Language.Hasmtlib.Type.Expr

Methods

(<=?) :: (a, b, c, d, e) -> (a, b, c, d, e) -> Expr 'BoolSort

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

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

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

(Orderable a, Orderable b, Orderable c, Orderable d, Orderable e, Orderable f) => Orderable (a, b, c, d, e, f)

Defined in Language.Hasmtlib.Type.Expr

Methods

(<=?) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> Expr 'BoolSort

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

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

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

(Orderable a, Orderable b, Orderable c, Orderable d, Orderable e, Orderable f, Orderable g) => Orderable (a, b, c, d, e, f, g)

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

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

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

(Orderable a, Orderable b, Orderable c, Orderable d, Orderable e, Orderable f, Orderable g, Orderable h) => Orderable (a, b, c, d, e, f, g, h)

Defined in Language.Hasmtlib.Type.Expr

Methods

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

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

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

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

min' :: (Orderable a, Iteable (Expr BoolSort) a) => a -> a -> a

Minimum of two as SMT-Expression.

max' :: (Orderable a, Iteable (Expr BoolSort) a) => a -> a -> a

Maximum of two as SMT-Expression.

class GEquatable f => GOrderable f where

Methods

(<?#) :: f a -> f a -> Expr BoolSort

(<=?#) :: f a -> f a -> Expr BoolSort

Instances

GOrderable (U1 :: k -> Type)

Defined in Language.Hasmtlib.Type.Expr

Methods

(<?#) :: forall (a :: k0). U1 a -> U1 a -> Expr 'BoolSort

(<=?#) :: forall (a :: k0). U1 a -> U1 a -> Expr 'BoolSort

GOrderable (V1 :: k -> Type)

Defined in Language.Hasmtlib.Type.Expr

Methods

(<?#) :: forall (a :: k0). V1 a -> V1 a -> Expr 'BoolSort

(<=?#) :: forall (a :: k0). V1 a -> V1 a -> Expr 'BoolSort

(GOrderable f, GOrderable g) => GOrderable (f :*: g :: k -> Type)

Defined in Language.Hasmtlib.Type.Expr

Methods

(<?#) :: forall (a :: k0). (f :*: g) a -> (f :*: g) a -> Expr 'BoolSort

(<=?#) :: forall (a :: k0). (f :*: g) a -> (f :*: g) a -> Expr 'BoolSort

(GOrderable f, GOrderable g) => GOrderable (f :+: g :: k -> Type)

Defined in Language.Hasmtlib.Type.Expr

Methods

(<?#) :: forall (a :: k0). (f :+: g) a -> (f :+: g) a -> Expr 'BoolSort

(<=?#) :: forall (a :: k0). (f :+: g) a -> (f :+: g) a -> Expr 'BoolSort

Orderable a => GOrderable (K1 i a :: k -> Type)

Defined in Language.Hasmtlib.Type.Expr

Methods

(<?#) :: forall (a0 :: k0). K1 i a a0 -> K1 i a a0 -> Expr 'BoolSort

(<=?#) :: forall (a0 :: k0). K1 i a a0 -> K1 i a a0 -> Expr 'BoolSort

GOrderable f => GOrderable (M1 i c f :: k -> Type)

Defined in Language.Hasmtlib.Type.Expr

Methods

(<?#) :: forall (a :: k0). M1 i c f a -> M1 i c f a -> Expr 'BoolSort

(<=?#) :: forall (a :: k0). M1 i c f a -> M1 i c f a -> Expr 'BoolSort

equal :: (Eq (HaskellType t), KnownSMTSort t, Foldable f) => f (Expr t) -> Expr BoolSort

Test multiple expressions on equality within in the SMT-Problem.

distinct :: (Eq (HaskellType t), KnownSMTSort t, Foldable f) => f (Expr t) -> Expr BoolSort

Test multiple expressions on distinctness within in the SMT-Problem.

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), Eq (HaskellType v)) => 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

toRealSort :: Expr IntSort -> Expr RealSort

Converts an expression of type IntSort to type RealSort.

toIntSort :: Expr RealSort -> Expr IntSort

Converts an expression of type RealSort to type IntSort.

isIntSort :: Expr RealSort -> Expr BoolSort

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

strLength :: Expr StringSort -> Expr IntSort

Length of a string.

strAt :: Expr StringSort -> Expr IntSort -> Expr StringSort

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

(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

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

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

First string contains second one (str.contains s t) iff s contains t.

strIndexOf :: Expr StringSort -> Expr StringSort -> Expr IntSort -> Expr IntSort

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

(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

(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.

renderQuantifier :: forall t. KnownSMTSort t => Builder -> Maybe (SMTVar t) -> (Expr t -> Expr BoolSort) -> Builder