{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE UndecidableInstances #-}
module Language.Hasmtlib.Internal.Expr where
import Language.Hasmtlib.Internal.Bitvec
import Language.Hasmtlib.Internal.Render
import Language.Hasmtlib.Type.ArrayMap
import Language.Hasmtlib.Boolean
import Data.GADT.Compare
import Data.Map
import Data.Kind
import Data.Proxy
import Data.Coerce
import Data.ByteString.Builder
import Control.Lens
import GHC.TypeLits
data SMTSort =
BoolSort
| IntSort
| RealSort
| BvSort Nat
| ArraySort SMTSort SMTSort
type role SMTVar phantom
newtype SMTVar (t :: SMTSort) = SMTVar { forall (t :: SMTSort). SMTVar t -> Int
_varId :: Int } deriving (Int -> SMTVar t -> ShowS
[SMTVar t] -> ShowS
SMTVar t -> String
(Int -> SMTVar t -> ShowS)
-> (SMTVar t -> String) -> ([SMTVar t] -> ShowS) -> Show (SMTVar t)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (t :: SMTSort). Int -> SMTVar t -> ShowS
forall (t :: SMTSort). [SMTVar t] -> ShowS
forall (t :: SMTSort). SMTVar t -> String
$cshowsPrec :: forall (t :: SMTSort). Int -> SMTVar t -> ShowS
showsPrec :: Int -> SMTVar t -> ShowS
$cshow :: forall (t :: SMTSort). SMTVar t -> String
show :: SMTVar t -> String
$cshowList :: forall (t :: SMTSort). [SMTVar t] -> ShowS
showList :: [SMTVar t] -> ShowS
Show, SMTVar t -> SMTVar t -> Bool
(SMTVar t -> SMTVar t -> Bool)
-> (SMTVar t -> SMTVar t -> Bool) -> Eq (SMTVar t)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (t :: SMTSort). SMTVar t -> SMTVar t -> Bool
$c== :: forall (t :: SMTSort). SMTVar t -> SMTVar t -> Bool
== :: SMTVar t -> SMTVar t -> Bool
$c/= :: forall (t :: SMTSort). SMTVar t -> SMTVar t -> Bool
/= :: SMTVar t -> SMTVar t -> Bool
Eq, Eq (SMTVar t)
Eq (SMTVar t) =>
(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)
-> (SMTVar t -> SMTVar t -> SMTVar t)
-> (SMTVar t -> SMTVar t -> SMTVar t)
-> Ord (SMTVar t)
SMTVar t -> SMTVar t -> Bool
SMTVar t -> SMTVar t -> Ordering
SMTVar t -> SMTVar t -> SMTVar t
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall (t :: SMTSort). Eq (SMTVar t)
forall (t :: SMTSort). SMTVar t -> SMTVar t -> Bool
forall (t :: SMTSort). SMTVar t -> SMTVar t -> Ordering
forall (t :: SMTSort). SMTVar t -> SMTVar t -> SMTVar t
$ccompare :: forall (t :: SMTSort). SMTVar t -> SMTVar t -> Ordering
compare :: SMTVar t -> SMTVar t -> Ordering
$c< :: forall (t :: SMTSort). SMTVar t -> SMTVar t -> Bool
< :: SMTVar t -> SMTVar t -> Bool
$c<= :: forall (t :: SMTSort). SMTVar t -> SMTVar t -> Bool
<= :: SMTVar t -> SMTVar t -> Bool
$c> :: forall (t :: SMTSort). SMTVar t -> SMTVar t -> Bool
> :: SMTVar t -> SMTVar t -> Bool
$c>= :: forall (t :: SMTSort). SMTVar t -> SMTVar t -> Bool
>= :: SMTVar t -> SMTVar t -> Bool
$cmax :: forall (t :: SMTSort). SMTVar t -> SMTVar t -> SMTVar t
max :: SMTVar t -> SMTVar t -> SMTVar t
$cmin :: forall (t :: SMTSort). SMTVar t -> SMTVar t -> SMTVar t
min :: SMTVar t -> SMTVar t -> SMTVar t
Ord)
$(makeLenses ''SMTVar)
type family HaskellType (t :: SMTSort) = (r :: Type) | r -> t where
HaskellType IntSort = Integer
HaskellType RealSort = Double
HaskellType BoolSort = Bool
HaskellType (BvSort n) = Bitvec n
HaskellType (ArraySort k v) = ConstArray (HaskellType k) (HaskellType v)
data Value (t :: SMTSort) where
IntValue :: HaskellType IntSort -> Value IntSort
RealValue :: HaskellType RealSort -> Value RealSort
BoolValue :: HaskellType BoolSort -> Value BoolSort
BvValue :: HaskellType (BvSort n) -> Value (BvSort n)
ArrayValue :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => HaskellType (ArraySort k v) -> Value (ArraySort k v)
unwrapValue :: Value t -> HaskellType t
unwrapValue :: forall (t :: SMTSort). Value t -> HaskellType t
unwrapValue (IntValue HaskellType 'IntSort
v) = HaskellType t
HaskellType 'IntSort
v
unwrapValue (RealValue HaskellType 'RealSort
v) = HaskellType t
HaskellType 'RealSort
v
unwrapValue (BoolValue HaskellType 'BoolSort
v) = HaskellType t
HaskellType 'BoolSort
v
unwrapValue (BvValue HaskellType ('BvSort n)
v) = HaskellType t
HaskellType ('BvSort n)
v
unwrapValue (ArrayValue HaskellType ('ArraySort k v)
v) = HaskellType t
HaskellType ('ArraySort k v)
v
{-# INLINEABLE unwrapValue #-}
wrapValue :: forall t. KnownSMTSort t => HaskellType t -> Value t
wrapValue :: forall (t :: SMTSort). KnownSMTSort t => HaskellType t -> Value t
wrapValue = case forall (t :: SMTSort). KnownSMTSort t => SSMTSort t
sortSing @t of
SSMTSort t
SIntSort -> HaskellType t -> Value t
HaskellType 'IntSort -> Value 'IntSort
IntValue
SSMTSort t
SRealSort -> HaskellType t -> Value t
HaskellType 'RealSort -> Value 'RealSort
RealValue
SSMTSort t
SBoolSort -> HaskellType t -> Value t
HaskellType 'BoolSort -> Value 'BoolSort
BoolValue
SBvSort Proxy n
_ -> HaskellType t -> Value t
HaskellType ('BvSort n) -> Value ('BvSort n)
forall (k :: Nat). HaskellType ('BvSort k) -> Value ('BvSort k)
BvValue
SArraySort Proxy k
_ Proxy v
_ -> HaskellType t -> Value t
HaskellType ('ArraySort k v) -> Value ('ArraySort k v)
forall (k :: SMTSort) (v :: SMTSort).
(KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) =>
HaskellType ('ArraySort k v) -> Value ('ArraySort k v)
ArrayValue
{-# INLINEABLE wrapValue #-}
data SSMTSort (t :: SMTSort) where
SIntSort :: SSMTSort IntSort
SRealSort :: SSMTSort RealSort
SBoolSort :: SSMTSort BoolSort
SBvSort :: KnownNat n => Proxy n -> SSMTSort (BvSort n)
SArraySort :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Proxy k -> Proxy v -> SSMTSort (ArraySort k v)
deriving instance Show (SSMTSort t)
deriving instance Eq (SSMTSort t)
deriving instance Ord (SSMTSort t)
instance GEq SSMTSort where
geq :: forall (a :: SMTSort) (b :: SMTSort).
SSMTSort a -> SSMTSort b -> Maybe (a :~: b)
geq SSMTSort a
SIntSort SSMTSort b
SIntSort = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
geq SSMTSort a
SRealSort SSMTSort b
SRealSort = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
geq SSMTSort a
SBoolSort SSMTSort b
SBoolSort = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
geq (SBvSort Proxy n
n) (SBvSort Proxy n
m) = case Proxy n -> Proxy n -> Maybe (n :~: n)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> Type)
(proxy2 :: Nat -> Type).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat Proxy n
n Proxy n
m of
Just n :~: n
Refl -> (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
Maybe (n :~: n)
Nothing -> Maybe (a :~: b)
forall a. Maybe a
Nothing
geq SSMTSort a
_ SSMTSort b
_ = Maybe (a :~: b)
forall a. Maybe a
Nothing
instance GCompare SSMTSort where
gcompare :: forall (a :: SMTSort) (b :: SMTSort).
SSMTSort a -> SSMTSort b -> GOrdering a b
gcompare SSMTSort a
SBoolSort SSMTSort b
SBoolSort = GOrdering a a
GOrdering a b
forall {k} (a :: k). GOrdering a a
GEQ
gcompare SSMTSort a
SIntSort SSMTSort b
SIntSort = GOrdering a a
GOrdering a b
forall {k} (a :: k). GOrdering a a
GEQ
gcompare SSMTSort a
SRealSort SSMTSort b
SRealSort = GOrdering a a
GOrdering a b
forall {k} (a :: k). GOrdering a a
GEQ
gcompare (SBvSort Proxy n
n) (SBvSort Proxy n
m) = case Proxy n -> Proxy n -> OrderingI n n
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> Type)
(proxy2 :: Nat -> Type).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat Proxy n
n Proxy n
m of
OrderingI n n
LTI -> GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GLT
OrderingI n n
EQI -> GOrdering a a
GOrdering a b
forall {k} (a :: k). GOrdering a a
GEQ
OrderingI n n
GTI -> GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GGT
gcompare (SArraySort Proxy k
k Proxy v
v) (SArraySort Proxy k
k' Proxy v
v') = case SSMTSort k -> SSMTSort k -> GOrdering k k
forall k (f :: k -> Type) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> GOrdering a b
forall (a :: SMTSort) (b :: SMTSort).
SSMTSort a -> SSMTSort b -> GOrdering a b
gcompare (Proxy k -> SSMTSort k
forall (prxy :: SMTSort -> Type) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> SSMTSort t
sortSing' Proxy k
k) (Proxy k -> SSMTSort k
forall (prxy :: SMTSort -> Type) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> SSMTSort t
sortSing' Proxy k
k') of
GOrdering k k
GLT -> GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GLT
GOrdering k k
GEQ -> case SSMTSort v -> SSMTSort v -> GOrdering v v
forall k (f :: k -> Type) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> GOrdering a b
forall (a :: SMTSort) (b :: SMTSort).
SSMTSort a -> SSMTSort b -> GOrdering a b
gcompare (Proxy v -> SSMTSort v
forall (prxy :: SMTSort -> Type) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> SSMTSort t
sortSing' Proxy v
v) (Proxy v -> SSMTSort v
forall (prxy :: SMTSort -> Type) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> SSMTSort t
sortSing' Proxy v
v') of
GOrdering v v
GLT -> GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GLT
GOrdering v v
GEQ -> GOrdering a a
GOrdering a b
forall {k} (a :: k). GOrdering a a
GEQ
GOrdering v v
GGT -> GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GGT
GOrdering k k
GGT -> GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GGT
gcompare SSMTSort a
SBoolSort SSMTSort b
_ = GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GLT
gcompare SSMTSort a
_ SSMTSort b
SBoolSort = GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GGT
gcompare SSMTSort a
SIntSort SSMTSort b
_ = GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GLT
gcompare SSMTSort a
_ SSMTSort b
SIntSort = GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GGT
gcompare SSMTSort a
SRealSort SSMTSort b
_ = GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GLT
gcompare SSMTSort a
_ SSMTSort b
SRealSort = GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GGT
gcompare (SArraySort Proxy k
_ Proxy v
_) SSMTSort b
_ = GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GLT
gcompare SSMTSort a
_ (SArraySort Proxy k
_ Proxy v
_) = GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GGT
class KnownSMTSort (t :: SMTSort) where sortSing :: SSMTSort t
instance KnownSMTSort IntSort where sortSing :: SSMTSort 'IntSort
sortSing = SSMTSort 'IntSort
SIntSort
instance KnownSMTSort RealSort where sortSing :: SSMTSort 'RealSort
sortSing = SSMTSort 'RealSort
SRealSort
instance KnownSMTSort BoolSort where sortSing :: SSMTSort 'BoolSort
sortSing = SSMTSort 'BoolSort
SBoolSort
instance KnownNat n => KnownSMTSort (BvSort n) where sortSing :: SSMTSort ('BvSort n)
sortSing = Proxy n -> SSMTSort ('BvSort n)
forall (k :: Nat). KnownNat k => Proxy k -> SSMTSort ('BvSort k)
SBvSort (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)
instance (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => KnownSMTSort (ArraySort k v) where
sortSing :: SSMTSort ('ArraySort k v)
sortSing = Proxy k -> Proxy v -> SSMTSort ('ArraySort k v)
forall (k :: SMTSort) (v :: SMTSort).
(KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) =>
Proxy k -> Proxy v -> SSMTSort ('ArraySort k v)
SArraySort (forall {k} (t :: k). Proxy t
forall (t :: SMTSort). Proxy t
Proxy @k) (forall {k} (t :: k). Proxy t
forall (t :: SMTSort). Proxy t
Proxy @v)
sortSing' :: forall prxy t. KnownSMTSort t => prxy t -> SSMTSort t
sortSing' :: forall (prxy :: SMTSort -> Type) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> SSMTSort t
sortSing' prxy t
_ = forall (t :: SMTSort). KnownSMTSort t => SSMTSort t
sortSing @t
type AllC :: [k -> Constraint] -> k -> Constraint
type family AllC cs k :: Constraint where
AllC '[] k = ()
AllC (c ': cs) k = (c k, AllC cs k)
data SomeSMTSort cs f where
SomeSMTSort :: forall cs f (t :: SMTSort). AllC cs t => f t -> SomeSMTSort cs f
type SomeKnownSMTSort f = SomeSMTSort '[KnownSMTSort] f
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) => Expr t -> Expr t -> Expr BoolSort
Distinct :: (Eq (HaskellType t), KnownSMTSort t) => Expr t -> 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)
ForAll :: KnownSMTSort t => Maybe (SMTVar t) -> (Expr t -> Expr BoolSort) -> Expr BoolSort
Exists :: KnownSMTSort t => Maybe (SMTVar t) -> (Expr t -> Expr BoolSort) -> Expr BoolSort
instance Boolean (Expr BoolSort) where
bool :: Bool -> Expr 'BoolSort
bool = Value 'BoolSort -> Expr 'BoolSort
forall (t :: SMTSort). Value t -> Expr t
Constant (Value 'BoolSort -> Expr 'BoolSort)
-> (Bool -> Value 'BoolSort) -> Bool -> Expr 'BoolSort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Value 'BoolSort
HaskellType 'BoolSort -> Value 'BoolSort
BoolValue
{-# INLINE bool #-}
&& :: Expr 'BoolSort -> Expr 'BoolSort -> Expr 'BoolSort
(&&) = Expr 'BoolSort -> Expr 'BoolSort -> Expr 'BoolSort
forall (t :: SMTSort).
Boolean (HaskellType t) =>
Expr t -> Expr t -> Expr t
And
{-# INLINE (&&) #-}
|| :: Expr 'BoolSort -> Expr 'BoolSort -> Expr 'BoolSort
(||) = Expr 'BoolSort -> Expr 'BoolSort -> Expr 'BoolSort
forall (t :: SMTSort).
Boolean (HaskellType t) =>
Expr t -> Expr t -> Expr t
Or
{-# INLINE (||) #-}
not :: Expr 'BoolSort -> Expr 'BoolSort
not = Expr 'BoolSort -> Expr 'BoolSort
forall (t :: SMTSort). Boolean (HaskellType t) => Expr t -> Expr t
Not
{-# INLINE not #-}
xor :: Expr 'BoolSort -> Expr 'BoolSort -> Expr 'BoolSort
xor = Expr 'BoolSort -> Expr 'BoolSort -> Expr 'BoolSort
forall (t :: SMTSort).
Boolean (HaskellType t) =>
Expr t -> Expr t -> Expr t
Xor
{-# INLINE xor #-}
instance KnownNat n => Boolean (Expr (BvSort n)) where
bool :: Bool -> Expr ('BvSort n)
bool = Value ('BvSort n) -> Expr ('BvSort n)
forall (t :: SMTSort). Value t -> Expr t
Constant (Value ('BvSort n) -> Expr ('BvSort n))
-> (Bool -> Value ('BvSort n)) -> Bool -> Expr ('BvSort n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bitvec n -> Value ('BvSort n)
HaskellType ('BvSort n) -> Value ('BvSort n)
forall (k :: Nat). HaskellType ('BvSort k) -> Value ('BvSort k)
BvValue (Bitvec n -> Value ('BvSort n))
-> (Bool -> Bitvec n) -> Bool -> Value ('BvSort n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bitvec n
forall b. Boolean b => Bool -> b
bool
{-# INLINE bool #-}
&& :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
(&&) = Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvAnd
{-# INLINE (&&) #-}
|| :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
(||) = Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvOr
{-# INLINE (||) #-}
not :: Expr ('BvSort n) -> Expr ('BvSort n)
not = Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n)
BvNot
{-# INLINE not #-}
xor :: Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
xor = Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Nat).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvXor
{-# INLINE xor #-}
instance Bounded (Expr BoolSort) where
minBound :: Expr 'BoolSort
minBound = Expr 'BoolSort
forall b. Boolean b => b
false
maxBound :: Expr 'BoolSort
maxBound = Expr 'BoolSort
forall b. Boolean b => b
true
instance KnownNat n => Bounded (Expr (BvSort n)) where
minBound :: Expr ('BvSort n)
minBound = Value ('BvSort n) -> Expr ('BvSort n)
forall (t :: SMTSort). Value t -> Expr t
Constant (Value ('BvSort n) -> Expr ('BvSort n))
-> Value ('BvSort n) -> Expr ('BvSort n)
forall a b. (a -> b) -> a -> b
$ HaskellType ('BvSort n) -> Value ('BvSort n)
forall (k :: Nat). HaskellType ('BvSort k) -> Value ('BvSort k)
BvValue Bitvec n
HaskellType ('BvSort n)
forall a. Bounded a => a
minBound
maxBound :: Expr ('BvSort n)
maxBound = Value ('BvSort n) -> Expr ('BvSort n)
forall (t :: SMTSort). Value t -> Expr t
Constant (Value ('BvSort n) -> Expr ('BvSort n))
-> Value ('BvSort n) -> Expr ('BvSort n)
forall a b. (a -> b) -> a -> b
$ HaskellType ('BvSort n) -> Value ('BvSort n)
forall (k :: Nat). HaskellType ('BvSort k) -> Value ('BvSort k)
BvValue Bitvec n
HaskellType ('BvSort n)
forall a. Bounded a => a
maxBound
instance Render (SSMTSort t) where
render :: SSMTSort t -> Builder
render SSMTSort t
SBoolSort = Builder
"Bool"
render SSMTSort t
SIntSort = Builder
"Int"
render SSMTSort t
SRealSort = Builder
"Real"
render (SBvSort Proxy n
p) = Builder -> Builder -> Integer -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"_" (Builder
"BitVec" :: Builder) (Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal Proxy n
p)
render (SArraySort Proxy k
k Proxy v
v) = Builder -> SSMTSort k -> SSMTSort v -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"Array" (Proxy k -> SSMTSort k
forall (prxy :: SMTSort -> Type) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> SSMTSort t
sortSing' Proxy k
k) (Proxy v -> SSMTSort v
forall (prxy :: SMTSort -> Type) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> SSMTSort t
sortSing' Proxy v
v)
{-# INLINEABLE render #-}
instance Render (SMTVar t) where
render :: SMTVar t -> Builder
render SMTVar t
v = Builder
"var_" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Int -> Builder
intDec (forall a b. Coercible a b => a -> b
forall a b. Coercible a b => a -> b
coerce @(SMTVar t) @Int SMTVar t
v)
{-# INLINEABLE render #-}
instance Render (Value t) where
render :: Value t -> Builder
render (IntValue HaskellType 'IntSort
x) = Integer -> Builder
forall a. Render a => a -> Builder
render Integer
HaskellType 'IntSort
x
render (RealValue HaskellType 'RealSort
x) = Double -> Builder
forall a. Render a => a -> Builder
render Double
HaskellType 'RealSort
x
render (BoolValue HaskellType 'BoolSort
x) = Bool -> Builder
forall a. Render a => a -> Builder
render Bool
HaskellType 'BoolSort
x
render (BvValue HaskellType ('BvSort n)
v) = Builder
"#b" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Bitvec n -> Builder
forall a. Render a => a -> Builder
render Bitvec n
HaskellType ('BvSort n)
v
render (ArrayValue HaskellType ('ArraySort k v)
arr) = case Map (HaskellType k) (HaskellType v)
-> Maybe
((HaskellType k, HaskellType v),
Map (HaskellType k) (HaskellType v))
forall k a. Map k a -> Maybe ((k, a), Map k a)
minViewWithKey (ConstArray (HaskellType k) (HaskellType v)
HaskellType ('ArraySort k v)
arrConstArray (HaskellType k) (HaskellType v)
-> Getting
(Map (HaskellType k) (HaskellType v))
(ConstArray (HaskellType k) (HaskellType v))
(Map (HaskellType k) (HaskellType v))
-> Map (HaskellType k) (HaskellType v)
forall s a. s -> Getting a s a -> a
^.Getting
(Map (HaskellType k) (HaskellType v))
(ConstArray (HaskellType k) (HaskellType v))
(Map (HaskellType k) (HaskellType v))
forall k1 v k2 (f :: Type -> Type).
Functor f =>
(Map k1 v -> f (Map k2 v))
-> ConstArray k1 v -> f (ConstArray k2 v)
stored) of
Maybe
((HaskellType k, HaskellType v),
Map (HaskellType k) (HaskellType v))
Nothing -> HaskellType v -> Builder
constRender (HaskellType v -> Builder) -> HaskellType v -> Builder
forall a b. (a -> b) -> a -> b
$ ConstArray (HaskellType k) (HaskellType v)
HaskellType ('ArraySort k v)
arrConstArray (HaskellType k) (HaskellType v)
-> Getting
(HaskellType v)
(ConstArray (HaskellType k) (HaskellType v))
(HaskellType v)
-> HaskellType v
forall s a. s -> Getting a s a -> a
^.Getting
(HaskellType v)
(ConstArray (HaskellType k) (HaskellType v))
(HaskellType v)
forall k v (f :: Type -> Type).
Functor f =>
(v -> f v) -> ConstArray k v -> f (ConstArray k v)
arrConst
Just ((HaskellType k
k,HaskellType v
v), Map (HaskellType k) (HaskellType v)
stored')
| Map (HaskellType k) (HaskellType v) -> Int
forall k a. Map k a -> Int
size (ConstArray (HaskellType k) (HaskellType v)
HaskellType ('ArraySort k v)
arrConstArray (HaskellType k) (HaskellType v)
-> Getting
(Map (HaskellType k) (HaskellType v))
(ConstArray (HaskellType k) (HaskellType v))
(Map (HaskellType k) (HaskellType v))
-> Map (HaskellType k) (HaskellType v)
forall s a. s -> Getting a s a -> a
^.Getting
(Map (HaskellType k) (HaskellType v))
(ConstArray (HaskellType k) (HaskellType v))
(Map (HaskellType k) (HaskellType v))
forall k1 v k2 (f :: Type -> Type).
Functor f =>
(Map k1 v -> f (Map k2 v))
-> ConstArray k1 v -> f (ConstArray k2 v)
stored) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1 -> Expr ('ArraySort k v) -> Builder
forall a. Render a => a -> Builder
render (Expr ('ArraySort k v) -> Builder)
-> Expr ('ArraySort k v) -> Builder
forall a b. (a -> b) -> a -> b
$ Expr ('ArraySort k v) -> Expr k -> Expr v -> Expr ('ArraySort k v)
forall (k :: SMTSort) (v :: SMTSort).
(KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) =>
Expr ('ArraySort k v) -> Expr k -> Expr v -> Expr ('ArraySort k v)
ArrStore (Value ('ArraySort k v) -> Expr ('ArraySort k v)
forall (t :: SMTSort). Value t -> Expr t
Constant (HaskellType ('ArraySort k v) -> Value ('ArraySort k v)
forall (t :: SMTSort). KnownSMTSort t => HaskellType t -> Value t
wrapValue (ConstArray (HaskellType k) (HaskellType v)
HaskellType ('ArraySort k v)
arr ConstArray (HaskellType k) (HaskellType v)
-> (ConstArray (HaskellType k) (HaskellType v)
-> ConstArray (HaskellType k) (HaskellType v))
-> ConstArray (HaskellType k) (HaskellType v)
forall a b. a -> (a -> b) -> b
& (Map (HaskellType k) (HaskellType v)
-> Identity (Map (HaskellType k) (HaskellType v)))
-> ConstArray (HaskellType k) (HaskellType v)
-> Identity (ConstArray (HaskellType k) (HaskellType v))
forall k1 v k2 (f :: Type -> Type).
Functor f =>
(Map k1 v -> f (Map k2 v))
-> ConstArray k1 v -> f (ConstArray k2 v)
stored ((Map (HaskellType k) (HaskellType v)
-> Identity (Map (HaskellType k) (HaskellType v)))
-> ConstArray (HaskellType k) (HaskellType v)
-> Identity (ConstArray (HaskellType k) (HaskellType v)))
-> Map (HaskellType k) (HaskellType v)
-> ConstArray (HaskellType k) (HaskellType v)
-> ConstArray (HaskellType k) (HaskellType v)
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Map (HaskellType k) (HaskellType v)
stored'))) (Value k -> Expr k
forall (t :: SMTSort). Value t -> Expr t
Constant (HaskellType k -> Value k
forall (t :: SMTSort). KnownSMTSort t => HaskellType t -> Value t
wrapValue HaskellType k
k)) (Value v -> Expr v
forall (t :: SMTSort). Value t -> Expr t
Constant (HaskellType v -> Value v
forall (t :: SMTSort). KnownSMTSort t => HaskellType t -> Value t
wrapValue HaskellType v
v))
| Bool
otherwise -> HaskellType v -> Builder
constRender HaskellType v
v
where
constRender :: HaskellType v -> Builder
constRender HaskellType v
v = Builder
"((as const " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> SSMTSort ('ArraySort k v) -> Builder
forall a. Render a => a -> Builder
render (ConstArray (HaskellType k) (HaskellType v)
-> SSMTSort ('ArraySort k v)
forall (k :: SMTSort) (v :: SMTSort).
(KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) =>
ConstArray (HaskellType k) (HaskellType v)
-> SSMTSort ('ArraySort k v)
goSing ConstArray (HaskellType k) (HaskellType v)
HaskellType ('ArraySort k v)
arr) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
") " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Value v -> Builder
forall a. Render a => a -> Builder
render (HaskellType v -> Value v
forall (t :: SMTSort). KnownSMTSort t => HaskellType t -> Value t
wrapValue HaskellType v
v) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
goSing :: forall k v. (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => ConstArray (HaskellType k) (HaskellType v) -> SSMTSort (ArraySort k v)
goSing :: forall (k :: SMTSort) (v :: SMTSort).
(KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) =>
ConstArray (HaskellType k) (HaskellType v)
-> SSMTSort ('ArraySort k v)
goSing ConstArray (HaskellType k) (HaskellType v)
_ = forall (t :: SMTSort). KnownSMTSort t => SSMTSort t
sortSing @(ArraySort k v)
instance KnownSMTSort t => Render (Expr t) where
render :: Expr t -> Builder
render (Var SMTVar t
v) = SMTVar t -> Builder
forall a. Render a => a -> Builder
render SMTVar t
v
render (Constant Value t
c) = Value t -> Builder
forall a. Render a => a -> Builder
render Value t
c
render (Plus Expr t
x Expr t
y) = Builder -> Expr t -> Expr t -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"+" Expr t
x Expr t
y
render (Neg Expr t
x) = Builder -> Expr t -> Builder
forall a. Render a => Builder -> a -> Builder
renderUnary Builder
"-" Expr t
x
render (Mul Expr t
x Expr t
y) = Builder -> Expr t -> Expr t -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"*" Expr t
x Expr t
y
render (Abs Expr t
x) = Builder -> Expr t -> Builder
forall a. Render a => Builder -> a -> Builder
renderUnary Builder
"abs" Expr t
x
render (Mod Expr 'IntSort
x Expr 'IntSort
y) = Builder -> Expr 'IntSort -> Expr 'IntSort -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"mod" Expr 'IntSort
x Expr 'IntSort
y
render (IDiv Expr 'IntSort
x Expr 'IntSort
y) = Builder -> Expr 'IntSort -> Expr 'IntSort -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"div" Expr 'IntSort
x Expr 'IntSort
y
render (Div Expr 'RealSort
x Expr 'RealSort
y) = Builder -> Expr 'RealSort -> Expr 'RealSort -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"/" Expr 'RealSort
x Expr 'RealSort
y
render (LTH Expr t
x Expr t
y) = Builder -> Expr t -> Expr t -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"<" Expr t
x Expr t
y
render (LTHE Expr t
x Expr t
y) = Builder -> Expr t -> Expr t -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"<=" Expr t
x Expr t
y
render (EQU Expr t
x Expr t
y) = Builder -> Expr t -> Expr t -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"=" Expr t
x Expr t
y
render (Distinct Expr t
x Expr t
y) = Builder -> Expr t -> Expr t -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"distinct" Expr t
x Expr t
y
render (GTHE Expr t
x Expr t
y) = Builder -> Expr t -> Expr t -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
">=" Expr t
x Expr t
y
render (GTH Expr t
x Expr t
y) = Builder -> Expr t -> Expr t -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
">" Expr t
x Expr t
y
render (Not Expr t
x) = Builder -> Expr t -> Builder
forall a. Render a => Builder -> a -> Builder
renderUnary Builder
"not" Expr t
x
render (And Expr t
x Expr t
y) = Builder -> Expr t -> Expr t -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"and" Expr t
x Expr t
y
render (Or Expr t
x Expr t
y) = Builder -> Expr t -> Expr t -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"or" Expr t
x Expr t
y
render (Impl Expr t
x Expr t
y) = Builder -> Expr t -> Expr t -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"=>" Expr t
x Expr t
y
render (Xor Expr t
x Expr t
y) = Builder -> Expr t -> Expr t -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"xor" Expr t
x Expr t
y
render Expr t
Pi = Builder
"real.pi"
render (Sqrt Expr 'RealSort
x) = Builder -> Expr 'RealSort -> Builder
forall a. Render a => Builder -> a -> Builder
renderUnary Builder
"sqrt" Expr 'RealSort
x
render (Exp Expr 'RealSort
x) = Builder -> Expr 'RealSort -> Builder
forall a. Render a => Builder -> a -> Builder
renderUnary Builder
"exp" Expr 'RealSort
x
render (Sin Expr 'RealSort
x) = Builder -> Expr 'RealSort -> Builder
forall a. Render a => Builder -> a -> Builder
renderUnary Builder
"sin" Expr 'RealSort
x
render (Cos Expr 'RealSort
x) = Builder -> Expr 'RealSort -> Builder
forall a. Render a => Builder -> a -> Builder
renderUnary Builder
"cos" Expr 'RealSort
x
render (Tan Expr 'RealSort
x) = Builder -> Expr 'RealSort -> Builder
forall a. Render a => Builder -> a -> Builder
renderUnary Builder
"tan" Expr 'RealSort
x
render (Asin Expr 'RealSort
x) = Builder -> Expr 'RealSort -> Builder
forall a. Render a => Builder -> a -> Builder
renderUnary Builder
"arcsin" Expr 'RealSort
x
render (Acos Expr 'RealSort
x) = Builder -> Expr 'RealSort -> Builder
forall a. Render a => Builder -> a -> Builder
renderUnary Builder
"arccos" Expr 'RealSort
x
render (Atan Expr 'RealSort
x) = Builder -> Expr 'RealSort -> Builder
forall a. Render a => Builder -> a -> Builder
renderUnary Builder
"arctan" Expr 'RealSort
x
render (ToReal Expr 'IntSort
x) = Builder -> Expr 'IntSort -> Builder
forall a. Render a => Builder -> a -> Builder
renderUnary Builder
"to_real" Expr 'IntSort
x
render (ToInt Expr 'RealSort
x) = Builder -> Expr 'RealSort -> Builder
forall a. Render a => Builder -> a -> Builder
renderUnary Builder
"to_int" Expr 'RealSort
x
render (IsInt Expr 'RealSort
x) = Builder -> Expr 'RealSort -> Builder
forall a. Render a => Builder -> a -> Builder
renderUnary Builder
"is_int" Expr 'RealSort
x
render (Ite Expr 'BoolSort
p Expr t
t Expr t
f) = Builder -> Expr 'BoolSort -> Expr t -> Expr t -> Builder
forall a b c.
(Render a, Render b, Render c) =>
Builder -> a -> b -> c -> Builder
renderTernary Builder
"ite" Expr 'BoolSort
p Expr t
t Expr t
f
render (BvNot Expr ('BvSort n)
x) = Builder -> Builder -> Builder
forall a. Render a => Builder -> a -> Builder
renderUnary Builder
"bvnot" (Expr ('BvSort n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort n)
x)
render (BvAnd Expr ('BvSort n)
x Expr ('BvSort n)
y) = Builder -> Builder -> Builder -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"bvand" (Expr ('BvSort n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort n)
x) (Expr ('BvSort n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort n)
y)
render (BvOr Expr ('BvSort n)
x Expr ('BvSort n)
y) = Builder -> Builder -> Builder -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"bvor" (Expr ('BvSort n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort n)
x) (Expr ('BvSort n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort n)
y)
render (BvXor Expr ('BvSort n)
x Expr ('BvSort n)
y) = Builder -> Builder -> Builder -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"bvxor" (Expr ('BvSort n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort n)
x) (Expr ('BvSort n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort n)
y)
render (BvNand Expr ('BvSort n)
x Expr ('BvSort n)
y) = Builder -> Builder -> Builder -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"bvnand" (Expr ('BvSort n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort n)
x) (Expr ('BvSort n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort n)
y)
render (BvNor Expr ('BvSort n)
x Expr ('BvSort n)
y) = Builder -> Builder -> Builder -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"bvnor" (Expr ('BvSort n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort n)
x) (Expr ('BvSort n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort n)
y)
render (BvNeg Expr ('BvSort n)
x) = Builder -> Builder -> Builder
forall a. Render a => Builder -> a -> Builder
renderUnary Builder
"bvneg" (Expr ('BvSort n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort n)
x)
render (BvAdd Expr ('BvSort n)
x Expr ('BvSort n)
y) = Builder -> Builder -> Builder -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"bvadd" (Expr ('BvSort n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort n)
x) (Expr ('BvSort n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort n)
y)
render (BvSub Expr ('BvSort n)
x Expr ('BvSort n)
y) = Builder -> Builder -> Builder -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"bvsub" (Expr ('BvSort n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort n)
x) (Expr ('BvSort n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort n)
y)
render (BvMul Expr ('BvSort n)
x Expr ('BvSort n)
y) = Builder -> Builder -> Builder -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"bvmul" (Expr ('BvSort n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort n)
x) (Expr ('BvSort n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort n)
y)
render (BvuDiv Expr ('BvSort n)
x Expr ('BvSort n)
y) = Builder -> Builder -> Builder -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"bvudiv" (Expr ('BvSort n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort n)
x) (Expr ('BvSort n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort n)
y)
render (BvuRem Expr ('BvSort n)
x Expr ('BvSort n)
y) = Builder -> Builder -> Builder -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"bvurem" (Expr ('BvSort n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort n)
x) (Expr ('BvSort n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort n)
y)
render (BvShL Expr ('BvSort n)
x Expr ('BvSort n)
y) = Builder -> Builder -> Builder -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"bvshl" (Expr ('BvSort n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort n)
x) (Expr ('BvSort n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort n)
y)
render (BvLShR Expr ('BvSort n)
x Expr ('BvSort n)
y) = Builder -> Builder -> Builder -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"bvlshr" (Expr ('BvSort n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort n)
x) (Expr ('BvSort n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort n)
y)
render (BvConcat Expr ('BvSort n)
x Expr ('BvSort m)
y) = Builder -> Builder -> Builder -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"concat" (Expr ('BvSort n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort n)
x) (Expr ('BvSort m) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort m)
y)
render (BvRotL Proxy i
i Expr ('BvSort n)
x) = Builder -> Builder -> Builder
forall a. Render a => Builder -> a -> Builder
renderUnary (Builder -> Builder -> Builder -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"_" (Builder
"rotate_left" :: Builder) (Integer -> Builder
forall a. Render a => a -> Builder
render (Proxy i -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal Proxy i
i))) (Expr ('BvSort n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort n)
x)
render (BvRotR Proxy i
i Expr ('BvSort n)
x) = Builder -> Builder -> Builder
forall a. Render a => Builder -> a -> Builder
renderUnary (Builder -> Builder -> Builder -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"_" (Builder
"rotate_right" :: Builder) (Integer -> Builder
forall a. Render a => a -> Builder
render (Proxy i -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal Proxy i
i))) (Expr ('BvSort n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort n)
x)
render (BvuLT Expr ('BvSort n)
x Expr ('BvSort n)
y) = Builder -> Builder -> Builder -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"bvult" (Expr ('BvSort n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort n)
x) (Expr ('BvSort n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort n)
y)
render (BvuLTHE Expr ('BvSort n)
x Expr ('BvSort n)
y) = Builder -> Builder -> Builder -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"bvule" (Expr ('BvSort n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort n)
x) (Expr ('BvSort n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort n)
y)
render (BvuGTHE Expr ('BvSort n)
x Expr ('BvSort n)
y) = Builder -> Builder -> Builder -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"bvuge" (Expr ('BvSort n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort n)
x) (Expr ('BvSort n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort n)
y)
render (BvuGT Expr ('BvSort n)
x Expr ('BvSort n)
y) = Builder -> Builder -> Builder -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"bvugt" (Expr ('BvSort n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort n)
x) (Expr ('BvSort n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort n)
y)
render (ArrSelect Expr ('ArraySort k t)
a Expr k
i) = Builder -> Builder -> Builder -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"select" (Expr ('ArraySort k t) -> Builder
forall a. Render a => a -> Builder
render Expr ('ArraySort k t)
a) (Expr k -> Builder
forall a. Render a => a -> Builder
render Expr k
i)
render (ArrStore Expr ('ArraySort k v)
a Expr k
i Expr v
v) = Builder -> Builder -> Builder -> Builder -> Builder
forall a b c.
(Render a, Render b, Render c) =>
Builder -> a -> b -> c -> Builder
renderTernary Builder
"store" (Expr ('ArraySort k v) -> Builder
forall a. Render a => a -> Builder
render Expr ('ArraySort k v)
a) (Expr k -> Builder
forall a. Render a => a -> Builder
render Expr k
i) (Expr v -> Builder
forall a. Render a => a -> Builder
render Expr v
v)
render (ForAll Maybe (SMTVar t)
mQvar Expr t -> Expr 'BoolSort
f) = Builder
-> Maybe (SMTVar t) -> (Expr t -> Expr 'BoolSort) -> Builder
forall (t :: SMTSort).
KnownSMTSort t =>
Builder
-> Maybe (SMTVar t) -> (Expr t -> Expr 'BoolSort) -> Builder
renderQuantifier Builder
"forall" Maybe (SMTVar t)
mQvar Expr t -> Expr 'BoolSort
f
render (Exists Maybe (SMTVar t)
mQvar Expr t -> Expr 'BoolSort
f) = Builder
-> Maybe (SMTVar t) -> (Expr t -> Expr 'BoolSort) -> Builder
forall (t :: SMTSort).
KnownSMTSort t =>
Builder
-> Maybe (SMTVar t) -> (Expr t -> Expr 'BoolSort) -> Builder
renderQuantifier Builder
"exists" Maybe (SMTVar t)
mQvar Expr t -> Expr 'BoolSort
f
renderQuantifier :: forall t. KnownSMTSort t => Builder -> Maybe (SMTVar t) -> (Expr t -> Expr BoolSort) -> Builder
renderQuantifier :: forall (t :: SMTSort).
KnownSMTSort t =>
Builder
-> Maybe (SMTVar t) -> (Expr t -> Expr 'BoolSort) -> Builder
renderQuantifier Builder
qname (Just SMTVar t
qvar) Expr t -> Expr 'BoolSort
f =
Builder -> Builder -> Builder -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary
Builder
qname
(Builder
"(" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder -> SSMTSort t -> Builder
forall a. Render a => Builder -> a -> Builder
renderUnary (SMTVar t -> Builder
forall a. Render a => a -> Builder
render SMTVar t
qvar) (forall (t :: SMTSort). KnownSMTSort t => SSMTSort t
sortSing @t) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")")
Builder
expr
where
expr :: Builder
expr = Expr 'BoolSort -> Builder
forall a. Render a => a -> Builder
render (Expr 'BoolSort -> Builder) -> Expr 'BoolSort -> Builder
forall a b. (a -> b) -> a -> b
$ Expr t -> Expr 'BoolSort
f (Expr t -> Expr 'BoolSort) -> Expr t -> Expr 'BoolSort
forall a b. (a -> b) -> a -> b
$ SMTVar t -> Expr t
forall (t :: SMTSort). SMTVar t -> Expr t
Var SMTVar t
qvar
renderQuantifier Builder
_ Maybe (SMTVar t)
Nothing Expr t -> Expr 'BoolSort
_ = Builder
forall a. Monoid a => a
mempty
instance Show (Value t) where
show :: Value t -> String
show (IntValue HaskellType 'IntSort
x) = String
"IntValue " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
HaskellType 'IntSort
x
show (RealValue HaskellType 'RealSort
x) = String
"RealValue " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Double -> String
forall a. Show a => a -> String
show Double
HaskellType 'RealSort
x
show (BoolValue HaskellType 'BoolSort
x) = String
"BoolValue " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Bool -> String
forall a. Show a => a -> String
show Bool
HaskellType 'BoolSort
x
show (BvValue HaskellType ('BvSort n)
x) = String
"BvValue " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Bitvec n -> String
forall a. Show a => a -> String
show Bitvec n
HaskellType ('BvSort n)
x
show (ArrayValue HaskellType ('ArraySort k v)
x) = String
"ArrValue: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Builder -> String
forall a. Show a => a -> String
show (Value ('ArraySort k v) -> Builder
forall a. Render a => a -> Builder
render (HaskellType ('ArraySort k v) -> Value ('ArraySort k v)
forall (k :: SMTSort) (v :: SMTSort).
(KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) =>
HaskellType ('ArraySort k v) -> Value ('ArraySort k v)
ArrayValue HaskellType ('ArraySort k v)
x))
instance Show (Expr t) where
show :: Expr t -> String
show (Var SMTVar t
v) = SMTVar t -> String
forall a. Show a => a -> String
show SMTVar t
v
show (Constant Value t
c) = Value t -> String
forall a. Show a => a -> String
show Value t
c
show (Plus Expr t
x Expr t
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr t -> String
forall a. Show a => a -> String
show Expr t
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" + " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr t -> String
forall a. Show a => a -> String
show Expr t
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (Neg Expr t
x) = String
"(- " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr t -> String
forall a. Show a => a -> String
show Expr t
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (Mul Expr t
x Expr t
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr t -> String
forall a. Show a => a -> String
show Expr t
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" * " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr t -> String
forall a. Show a => a -> String
show Expr t
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (Abs Expr t
x) = String
"(abs " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr t -> String
forall a. Show a => a -> String
show Expr t
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (Mod Expr 'IntSort
x Expr 'IntSort
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr 'IntSort -> String
forall a. Show a => a -> String
show Expr 'IntSort
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" mod " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr 'IntSort -> String
forall a. Show a => a -> String
show Expr 'IntSort
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (IDiv Expr 'IntSort
x Expr 'IntSort
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr 'IntSort -> String
forall a. Show a => a -> String
show Expr 'IntSort
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" div " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr 'IntSort -> String
forall a. Show a => a -> String
show Expr 'IntSort
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (Div Expr 'RealSort
x Expr 'RealSort
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr 'RealSort -> String
forall a. Show a => a -> String
show Expr 'RealSort
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" / " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr 'RealSort -> String
forall a. Show a => a -> String
show Expr 'RealSort
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (LTH Expr t
x Expr t
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr t -> String
forall a. Show a => a -> String
show Expr t
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" < " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr t -> String
forall a. Show a => a -> String
show Expr t
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (LTHE Expr t
x Expr t
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr t -> String
forall a. Show a => a -> String
show Expr t
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" <= " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr t -> String
forall a. Show a => a -> String
show Expr t
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (EQU Expr t
x Expr t
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr t -> String
forall a. Show a => a -> String
show Expr t
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" == " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr t -> String
forall a. Show a => a -> String
show Expr t
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (Distinct Expr t
x Expr t
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr t -> String
forall a. Show a => a -> String
show Expr t
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" /= " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr t -> String
forall a. Show a => a -> String
show Expr t
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (GTHE Expr t
x Expr t
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr t -> String
forall a. Show a => a -> String
show Expr t
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" >= " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr t -> String
forall a. Show a => a -> String
show Expr t
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (GTH Expr t
x Expr t
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr t -> String
forall a. Show a => a -> String
show Expr t
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" > " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr t -> String
forall a. Show a => a -> String
show Expr t
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (Not Expr t
x) = String
"(not " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr t -> String
forall a. Show a => a -> String
show Expr t
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (And Expr t
x Expr t
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr t -> String
forall a. Show a => a -> String
show Expr t
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" && " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr t -> String
forall a. Show a => a -> String
show Expr t
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (Or Expr t
x Expr t
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr t -> String
forall a. Show a => a -> String
show Expr t
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" || " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr t -> String
forall a. Show a => a -> String
show Expr t
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (Impl Expr t
x Expr t
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr t -> String
forall a. Show a => a -> String
show Expr t
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" ==> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr t -> String
forall a. Show a => a -> String
show Expr t
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (Xor Expr t
x Expr t
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr t -> String
forall a. Show a => a -> String
show Expr t
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" xor " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr t -> String
forall a. Show a => a -> String
show Expr t
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show Expr t
Pi = String
"pi"
show (Sqrt Expr 'RealSort
x) = String
"(sqrt " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr 'RealSort -> String
forall a. Show a => a -> String
show Expr 'RealSort
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (Exp Expr 'RealSort
x) = String
"(exp " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr 'RealSort -> String
forall a. Show a => a -> String
show Expr 'RealSort
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (Sin Expr 'RealSort
x) = String
"(sin " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr 'RealSort -> String
forall a. Show a => a -> String
show Expr 'RealSort
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (Cos Expr 'RealSort
x) = String
"(cos " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr 'RealSort -> String
forall a. Show a => a -> String
show Expr 'RealSort
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (Tan Expr 'RealSort
x) = String
"(tan " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr 'RealSort -> String
forall a. Show a => a -> String
show Expr 'RealSort
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (Asin Expr 'RealSort
x) = String
"(arcsin " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr 'RealSort -> String
forall a. Show a => a -> String
show Expr 'RealSort
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (Acos Expr 'RealSort
x) = String
"(arccos " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr 'RealSort -> String
forall a. Show a => a -> String
show Expr 'RealSort
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (Atan Expr 'RealSort
x) = String
"(arctan " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr 'RealSort -> String
forall a. Show a => a -> String
show Expr 'RealSort
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (ToReal Expr 'IntSort
x) = String
"(to_real " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr 'IntSort -> String
forall a. Show a => a -> String
show Expr 'IntSort
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (ToInt Expr 'RealSort
x) = String
"(to_int " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr 'RealSort -> String
forall a. Show a => a -> String
show Expr 'RealSort
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (IsInt Expr 'RealSort
x) = String
"(is_int " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr 'RealSort -> String
forall a. Show a => a -> String
show Expr 'RealSort
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (Ite Expr 'BoolSort
p Expr t
t Expr t
f) = String
"(ite " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr 'BoolSort -> String
forall a. Show a => a -> String
show Expr 'BoolSort
p String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr t -> String
forall a. Show a => a -> String
show Expr t
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr t -> String
forall a. Show a => a -> String
show Expr t
f String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (BvNot Expr ('BvSort n)
x) = String
"(not " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr ('BvSort n) -> String
forall a. Show a => a -> String
show Expr ('BvSort n)
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (BvAnd Expr ('BvSort n)
x Expr ('BvSort n)
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr ('BvSort n) -> String
forall a. Show a => a -> String
show Expr ('BvSort n)
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" && " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr ('BvSort n) -> String
forall a. Show a => a -> String
show Expr ('BvSort n)
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (BvOr Expr ('BvSort n)
x Expr ('BvSort n)
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr ('BvSort n) -> String
forall a. Show a => a -> String
show Expr ('BvSort n)
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" || " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr ('BvSort n) -> String
forall a. Show a => a -> String
show Expr ('BvSort n)
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (BvXor Expr ('BvSort n)
x Expr ('BvSort n)
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr ('BvSort n) -> String
forall a. Show a => a -> String
show Expr ('BvSort n)
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" xor " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr ('BvSort n) -> String
forall a. Show a => a -> String
show Expr ('BvSort n)
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (BvNand Expr ('BvSort n)
x Expr ('BvSort n)
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr ('BvSort n) -> String
forall a. Show a => a -> String
show Expr ('BvSort n)
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" nand " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr ('BvSort n) -> String
forall a. Show a => a -> String
show Expr ('BvSort n)
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (BvNor Expr ('BvSort n)
x Expr ('BvSort n)
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr ('BvSort n) -> String
forall a. Show a => a -> String
show Expr ('BvSort n)
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" nor " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr ('BvSort n) -> String
forall a. Show a => a -> String
show Expr ('BvSort n)
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (BvNeg Expr ('BvSort n)
x) = String
"(- " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr ('BvSort n) -> String
forall a. Show a => a -> String
show Expr ('BvSort n)
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (BvAdd Expr ('BvSort n)
x Expr ('BvSort n)
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr ('BvSort n) -> String
forall a. Show a => a -> String
show Expr ('BvSort n)
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" + " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr ('BvSort n) -> String
forall a. Show a => a -> String
show Expr ('BvSort n)
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (BvSub Expr ('BvSort n)
x Expr ('BvSort n)
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr ('BvSort n) -> String
forall a. Show a => a -> String
show Expr ('BvSort n)
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" - " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr ('BvSort n) -> String
forall a. Show a => a -> String
show Expr ('BvSort n)
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (BvMul Expr ('BvSort n)
x Expr ('BvSort n)
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr ('BvSort n) -> String
forall a. Show a => a -> String
show Expr ('BvSort n)
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" * " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr ('BvSort n) -> String
forall a. Show a => a -> String
show Expr ('BvSort n)
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (BvuDiv Expr ('BvSort n)
x Expr ('BvSort n)
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr ('BvSort n) -> String
forall a. Show a => a -> String
show Expr ('BvSort n)
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" udiv " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr ('BvSort n) -> String
forall a. Show a => a -> String
show Expr ('BvSort n)
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (BvuRem Expr ('BvSort n)
x Expr ('BvSort n)
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr ('BvSort n) -> String
forall a. Show a => a -> String
show Expr ('BvSort n)
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" urem " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr ('BvSort n) -> String
forall a. Show a => a -> String
show Expr ('BvSort n)
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (BvShL Expr ('BvSort n)
x Expr ('BvSort n)
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr ('BvSort n) -> String
forall a. Show a => a -> String
show Expr ('BvSort n)
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" bvshl " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr ('BvSort n) -> String
forall a. Show a => a -> String
show Expr ('BvSort n)
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (BvLShR Expr ('BvSort n)
x Expr ('BvSort n)
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr ('BvSort n) -> String
forall a. Show a => a -> String
show Expr ('BvSort n)
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" bvlshr " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr ('BvSort n) -> String
forall a. Show a => a -> String
show Expr ('BvSort n)
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (BvConcat Expr ('BvSort n)
x Expr ('BvSort m)
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr ('BvSort n) -> String
forall a. Show a => a -> String
show Expr ('BvSort n)
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" bvconcat " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr ('BvSort m) -> String
forall a. Show a => a -> String
show Expr ('BvSort m)
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (BvRotL Proxy i
i Expr ('BvSort n)
x) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr ('BvSort n) -> String
forall a. Show a => a -> String
show Expr ('BvSort n)
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" bvrotl " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (Proxy i -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal Proxy i
i) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (BvRotR Proxy i
i Expr ('BvSort n)
x) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr ('BvSort n) -> String
forall a. Show a => a -> String
show Expr ('BvSort n)
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" bvrotr " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (Proxy i -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal Proxy i
i) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (BvuLT Expr ('BvSort n)
x Expr ('BvSort n)
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr ('BvSort n) -> String
forall a. Show a => a -> String
show Expr ('BvSort n)
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" bvult " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr ('BvSort n) -> String
forall a. Show a => a -> String
show Expr ('BvSort n)
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (BvuLTHE Expr ('BvSort n)
x Expr ('BvSort n)
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr ('BvSort n) -> String
forall a. Show a => a -> String
show Expr ('BvSort n)
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" bvule " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr ('BvSort n) -> String
forall a. Show a => a -> String
show Expr ('BvSort n)
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (BvuGTHE Expr ('BvSort n)
x Expr ('BvSort n)
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr ('BvSort n) -> String
forall a. Show a => a -> String
show Expr ('BvSort n)
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" bvuge " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr ('BvSort n) -> String
forall a. Show a => a -> String
show Expr ('BvSort n)
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (BvuGT Expr ('BvSort n)
x Expr ('BvSort n)
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr ('BvSort n) -> String
forall a. Show a => a -> String
show Expr ('BvSort n)
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" bvugt " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr ('BvSort n) -> String
forall a. Show a => a -> String
show Expr ('BvSort n)
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (ForAll (Just SMTVar t
qv) Expr t -> Expr 'BoolSort
f) = String
"(forall " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SMTVar t -> String
forall a. Show a => a -> String
show SMTVar t
qv String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr 'BoolSort -> String
forall a. Show a => a -> String
show (Expr t -> Expr 'BoolSort
f (SMTVar t -> Expr t
forall (t :: SMTSort). SMTVar t -> Expr t
Var SMTVar t
qv)) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (ForAll Maybe (SMTVar t)
Nothing Expr t -> Expr 'BoolSort
f) = String
"(forall var_-1: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr 'BoolSort -> String
forall a. Show a => a -> String
show (Expr t -> Expr 'BoolSort
f (SMTVar t -> Expr t
forall (t :: SMTSort). SMTVar t -> Expr t
Var (Int -> SMTVar t
forall (t :: SMTSort). Int -> SMTVar t
SMTVar (-Int
1)))) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (ArrSelect Expr ('ArraySort k t)
i Expr k
arr) = String
"(select " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr ('ArraySort k t) -> String
forall a. Show a => a -> String
show Expr ('ArraySort k t)
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr k -> String
forall a. Show a => a -> String
show Expr k
arr String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (ArrStore Expr ('ArraySort k v)
i Expr k
x Expr v
arr) = String
"(select " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr ('ArraySort k v) -> String
forall a. Show a => a -> String
show Expr ('ArraySort k v)
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr k -> String
forall a. Show a => a -> String
show Expr k
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr v -> String
forall a. Show a => a -> String
show Expr v
arr String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (Exists (Just SMTVar t
qv) Expr t -> Expr 'BoolSort
f) = String
"(exists " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SMTVar t -> String
forall a. Show a => a -> String
show SMTVar t
qv String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr 'BoolSort -> String
forall a. Show a => a -> String
show (Expr t -> Expr 'BoolSort
f (SMTVar t -> Expr t
forall (t :: SMTSort). SMTVar t -> Expr t
Var SMTVar t
qv)) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (Exists Maybe (SMTVar t)
Nothing Expr t -> Expr 'BoolSort
f) = String
"(exists var_-1: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr 'BoolSort -> String
forall a. Show a => a -> String
show (Expr t -> Expr 'BoolSort
f (SMTVar t -> Expr t
forall (t :: SMTSort). SMTVar t -> Expr t
Var (Int -> SMTVar t
forall (t :: SMTSort). Int -> SMTVar t
SMTVar (-Int
1)))) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"