{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE UndecidableInstances #-}

module Language.Hasmtlib.Internal.Expr where

import Language.Hasmtlib.Internal.Render
import Language.Hasmtlib.Type.ArrayMap
import Language.Hasmtlib.Type.SMTSort
import Language.Hasmtlib.Boolean
import Data.Map hiding (toList)
import Data.List (intercalate)
import Data.Proxy
import Data.Coerce
import Data.Foldable (toList)
import Data.ByteString.Builder
import qualified Data.Vector.Sized as V
import Control.Lens
import GHC.TypeLits

-- | 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)

-- | 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)
  ArrayValue :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => HaskellType (ArraySort k v) -> Value (ArraySort k v)

-- | Unwrap a value from '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
unwrapValue (ArrayValue HaskellType ('ArraySort k v)
v) = HaskellType t
HaskellType ('ArraySort k v)
v
{-# INLINEABLE unwrapValue #-}

-- | Wrap a value into '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 (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 #-}

-- | An existential wrapper that hides some known 'SMTSort'.
type SomeKnownSMTSort f = SomeSMTSort '[KnownSMTSort] 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, KnownNat n) => V.Vector (n + 2) (Expr t) -> Expr BoolSort
  Distinct  :: (Eq (HaskellType t), KnownSMTSort t, KnownNat n) => V.Vector (n + 2) (Expr t) -> Expr BoolSort
  GTHE      :: (Ord (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort
  GTH       :: (Ord (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort

  Not       :: Boolean (HaskellType t) => Expr t -> Expr t
  And       :: Boolean (HaskellType t) => Expr t -> Expr t -> Expr t
  Or        :: Boolean (HaskellType t) => Expr t -> Expr t -> Expr t
  Impl      :: Boolean (HaskellType t) => Expr t -> Expr t -> Expr t
  Xor       :: Boolean (HaskellType t) => Expr t -> Expr t -> Expr t

  Pi        :: Expr RealSort
  Sqrt      :: Expr RealSort -> Expr RealSort
  Exp       :: Expr RealSort -> Expr RealSort
  Sin       :: Expr RealSort -> Expr RealSort
  Cos       :: Expr RealSort -> Expr RealSort
  Tan       :: Expr RealSort -> Expr RealSort
  Asin      :: Expr RealSort -> Expr RealSort
  Acos      :: Expr RealSort -> Expr RealSort
  Atan      :: Expr RealSort -> Expr RealSort

  ToReal    :: Expr IntSort  -> Expr RealSort
  ToInt     :: Expr RealSort -> Expr IntSort
  IsInt     :: Expr RealSort -> Expr BoolSort

  Ite       :: Expr BoolSort -> Expr t -> Expr t -> Expr t

  BvNot     :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n)
  BvAnd     :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
  BvOr      :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
  BvXor     :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
  BvNand    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
  BvNor     :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
  BvNeg     :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n)
  BvAdd     :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
  BvSub     :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
  BvMul     :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
  BvuDiv    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
  BvuRem    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
  BvShL     :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
  BvLShR    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
  BvConcat  :: (KnownNat n, KnownNat m) => Expr (BvSort n) -> Expr (BvSort m) -> Expr (BvSort (n + m))
  BvRotL    :: (KnownNat n, KnownNat i, KnownNat (Mod i n)) => Proxy i -> Expr (BvSort n) -> Expr (BvSort n)
  BvRotR    :: (KnownNat n, KnownNat i, KnownNat (Mod i n)) => Proxy i -> Expr (BvSort n) -> Expr (BvSort n)
  BvuLT     :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr BoolSort
  BvuLTHE   :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr BoolSort
  BvuGTHE   :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr BoolSort
  BvuGT     :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr BoolSort

  ArrSelect :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Expr (ArraySort k v) -> Expr k -> Expr v
  ArrStore  :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Expr (ArraySort k v) -> Expr k -> Expr v -> Expr (ArraySort k v)

  -- Just v if quantified var has been created already, Nothing otherwise
  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 (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 :: * -> *).
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 :: * -> *).
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 :: * -> *).
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 :: * -> *).
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 Vector (n + 2) (Expr t)
xs)     = Builder -> [Expr t] -> Builder
forall a. Render a => Builder -> [a] -> Builder
renderNary Builder
"=" ([Expr t] -> Builder) -> [Expr t] -> Builder
forall a b. (a -> b) -> a -> b
$ Vector (n + 2) (Expr t) -> [Expr t]
forall (n :: Nat) a. Vector n a -> [a]
V.toList Vector (n + 2) (Expr t)
xs
  render (Distinct Vector (n + 2) (Expr t)
xs)= Builder -> [Expr t] -> Builder
forall a. Render a => Builder -> [a] -> Builder
renderNary Builder
"distinct" ([Expr t] -> Builder) -> [Expr t] -> Builder
forall a b. (a -> b) -> a -> b
$ Vector (n + 2) (Expr t) -> [Expr t]
forall (n :: Nat) a. Vector n a -> [a]
V.toList Vector (n + 2) (Expr t)
xs
  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 -> *).
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 -> *).
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)) -- FIXME: This is bad but easy now

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 Vector (n + 2) (Expr t)
xs)             = String
"(= " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
" " (Expr t -> String
forall a. Show a => a -> String
show (Expr t -> String) -> [Expr t] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Vector (n + 2) (Expr t) -> [Expr t]
forall a. Vector Vector (n + 2) a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Vector (n + 2) (Expr t)
xs) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
  show (Distinct Vector (n + 2) (Expr t)
xs)        = String
"(distinct " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
" " (Expr t -> String
forall a. Show a => a -> String
show (Expr t -> String) -> [Expr t] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Vector (n + 2) (Expr t) -> [Expr t]
forall a. Vector Vector (n + 2) a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Vector (n + 2) (Expr t)
xs) 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 -> *).
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 -> *).
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
")"