{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE TemplateHaskell #-}

module Language.Hasmtlib.Internal.Expr where

import Language.Hasmtlib.Internal.Bitvec
import Language.Hasmtlib.Internal.Render
import Language.Hasmtlib.Boolean
import Data.Kind
import Data.Proxy
import Data.Coerce
import Data.ByteString.Builder
import Control.Lens
import GHC.TypeLits

-- | Sorts in SMTLib2 - used as promoted type (data-kind).
data SMTSort = IntSort | RealSort | BoolSort | BvSort Nat

-- | An internal SMT variable with a phantom-type which holds an 'Int' as it's identifier.
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)

-- | Injective type-family that computes the Haskell 'Type' of a 'SMTSort'.
type family HaskellType (t :: SMTSort) = (r :: Type) | r -> t where
  HaskellType IntSort    = Integer
  HaskellType RealSort   = Double
  HaskellType BoolSort   = Bool
  HaskellType (BvSort n) = Bitvec n

-- | A wrapper for values of 'SMTSort's.
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)

-- | Unwrap a value.
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
{-# INLINEABLE unwrapValue #-}

-- | Wrap a value.
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 (n :: Nat). HaskellType ('BvSort n) -> Value ('BvSort n)
BvValue
{-# INLINEABLE wrapValue #-}

deriving instance Show (Value t)
deriving instance Eq   (Value t)
deriving instance Ord  (Value t)

-- | Singleton for 'SMTSort'.
data SSMTSort (t :: SMTSort) where
  SIntSort  :: SSMTSort IntSort
  SRealSort :: SSMTSort RealSort
  SBoolSort :: SSMTSort BoolSort
  SBvSort   :: KnownNat n => Proxy n -> SSMTSort (BvSort n)

deriving instance Show (SSMTSort t)
deriving instance Eq   (SSMTSort t)
deriving instance Ord  (SSMTSort t)

-- | Compute singleton 'SSMTSort' from it's promoted type 'SMTSort'.
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 (n :: Nat). KnownNat n => Proxy n -> SSMTSort ('BvSort n)
SBvSort (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)

-- | An existential wrapper that hides some 'SMTSort'.
data SomeKnownSMTSort f where
  SomeKnownSMTSort :: forall (t :: SMTSort) f. KnownSMTSort t => f t -> SomeKnownSMTSort f

-- | A SMT expression.
--   For internal use only.
--   For building expressions use the corresponding instances (Num, Boolean, ...).
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

  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 (n :: Nat). HaskellType ('BvSort n) -> Value ('BvSort n)
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 (n :: Nat). HaskellType ('BvSort n) -> Value ('BvSort n)
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 (n :: Nat). HaskellType ('BvSort n) -> Value ('BvSort n)
BvValue Bitvec n
HaskellType ('BvSort n)
forall a. Bounded a => a
maxBound

instance Render (SSMTSort t) where
  render :: SSMTSort t -> Builder
render SSMTSort t
SIntSort    = Builder
"Int"
  render SSMTSort t
SRealSort   = Builder
"Real"
  render SSMTSort t
SBoolSort   = Builder
"Bool"
  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)
  {-# 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 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 (IntValue HaskellType 'IntSort
x))  = Integer -> Builder
forall a. Render a => a -> Builder
render Integer
HaskellType 'IntSort
x
  render (Constant (RealValue HaskellType 'RealSort
x)) = Double -> Builder
forall a. Render a => a -> Builder
render Double
HaskellType 'RealSort
x
  render (Constant (BoolValue HaskellType 'BoolSort
x)) = Bool -> Builder
forall a. Render a => a -> Builder
render Bool
HaskellType 'BoolSort
x
  render (Constant (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 (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 (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 (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 (IntValue HaskellType 'IntSort
x))  = Integer -> String
forall a. Show a => a -> String
show Integer
HaskellType 'IntSort
x
  show (Constant (RealValue HaskellType 'RealSort
x)) = Double -> String
forall a. Show a => a -> String
show Double
HaskellType 'RealSort
x
  show (Constant (BoolValue HaskellType 'BoolSort
x)) = Bool -> String
forall a. Show a => a -> String
show Bool
HaskellType 'BoolSort
x
  show (Constant (BvValue   HaskellType ('BvSort n)
x)) = Bitvec n -> String
forall a. Show a => a -> String
show Bitvec n
HaskellType ('BvSort n)
x
  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 (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
")"