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

module Language.Hasmtlib.Internal.Expr where

import Prelude hiding (not)
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.Proxy
import Data.Coerce
import Data.String (IsString(..))
import Data.Text (pack)
import Data.ByteString.Builder
import Data.ByteString.Lazy.UTF8 (toString)
import qualified Data.Vector.Sized as V
import Control.Lens
import GHC.TypeLits
import GHC.Generics

-- | 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, (forall x. SMTVar t -> Rep (SMTVar t) x)
-> (forall x. Rep (SMTVar t) x -> SMTVar t) -> Generic (SMTVar t)
forall x. Rep (SMTVar t) x -> SMTVar t
forall x. SMTVar t -> Rep (SMTVar t) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (t :: SMTSort) x. Rep (SMTVar t) x -> SMTVar t
forall (t :: SMTSort) x. SMTVar t -> Rep (SMTVar t) x
$cfrom :: forall (t :: SMTSort) x. SMTVar t -> Rep (SMTVar t) x
from :: forall x. SMTVar t -> Rep (SMTVar t) x
$cto :: forall (t :: SMTSort) x. Rep (SMTVar t) x -> SMTVar t
to :: forall x. Rep (SMTVar t) x -> SMTVar t
Generic)
$(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)
  StringValue :: HaskellType StringSort -> Value StringSort

deriving instance Eq (HaskellType t) => Eq (Value t)
deriving instance Ord (HaskellType t) => Ord (Value t)

-- | 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
unwrapValue (StringValue HaskellType 'StringSort
v) = HaskellType t
HaskellType 'StringSort
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
  SSMTSort t
SStringSort    -> HaskellType t -> Value t
HaskellType 'StringSort -> Value 'StringSort
StringValue
{-# INLINEABLE wrapValue #-}

-- | An existential wrapper that hides some known 'SMTSort'.
type SomeKnownSMTSort f = SomeSMTSort '[KnownSMTSort] f

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

  StrConcat     :: Expr StringSort -> Expr StringSort -> Expr StringSort
  StrLength     :: Expr StringSort -> Expr IntSort
  StrLT         :: Expr StringSort -> Expr StringSort -> Expr BoolSort
  StrLTHE       :: Expr StringSort -> Expr StringSort -> Expr BoolSort
  StrAt         :: Expr StringSort -> Expr IntSort -> Expr StringSort
  StrSubstring  :: Expr StringSort -> Expr IntSort -> Expr IntSort -> Expr StringSort
  StrPrefixOf   :: Expr StringSort -> Expr StringSort -> Expr BoolSort
  StrSuffixOf   :: Expr StringSort -> Expr StringSort -> Expr BoolSort
  StrContains   :: Expr StringSort -> Expr StringSort -> Expr BoolSort
  StrIndexOf    :: Expr StringSort -> Expr StringSort -> Expr IntSort -> Expr IntSort
  StrReplace    :: Expr StringSort -> Expr StringSort -> Expr StringSort -> Expr StringSort
  StrReplaceAll :: Expr StringSort -> Expr StringSort -> Expr StringSort -> Expr StringSort

  -- 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 #-}
  (Constant (BoolValue HaskellType 'BoolSort
x)) && :: Expr 'BoolSort -> Expr 'BoolSort -> Expr 'BoolSort
&& Expr 'BoolSort
y = if Bool
HaskellType 'BoolSort
x then Expr 'BoolSort
y else Expr 'BoolSort
forall b. Boolean b => b
false
  Expr 'BoolSort
x && (Constant (BoolValue HaskellType 'BoolSort
y)) = if Bool
HaskellType 'BoolSort
y then Expr 'BoolSort
x else Expr 'BoolSort
forall b. Boolean b => b
false
  Expr 'BoolSort
x && Expr 'BoolSort
y = Expr 'BoolSort -> Expr 'BoolSort -> Expr 'BoolSort
forall (t :: SMTSort).
Boolean (HaskellType t) =>
Expr t -> Expr t -> Expr t
And Expr 'BoolSort
x Expr 'BoolSort
y
  {-# INLINE (&&) #-}
  (Constant (BoolValue HaskellType 'BoolSort
x)) || :: Expr 'BoolSort -> Expr 'BoolSort -> Expr 'BoolSort
|| Expr 'BoolSort
y = if Bool
HaskellType 'BoolSort
x then Expr 'BoolSort
forall b. Boolean b => b
true else Expr 'BoolSort
y
  Expr 'BoolSort
x || (Constant (BoolValue HaskellType 'BoolSort
y)) = if Bool
HaskellType 'BoolSort
y then Expr 'BoolSort
forall b. Boolean b => b
true else Expr 'BoolSort
x
  Expr 'BoolSort
x || Expr 'BoolSort
y = Expr 'BoolSort -> Expr 'BoolSort -> Expr 'BoolSort
forall (t :: SMTSort).
Boolean (HaskellType t) =>
Expr t -> Expr t -> Expr t
Or Expr 'BoolSort
x Expr 'BoolSort
y
  {-# INLINE (||) #-}
  not :: Expr 'BoolSort -> Expr 'BoolSort
not (Constant (BoolValue HaskellType 'BoolSort
x)) = Bool -> Expr 'BoolSort
forall b. Boolean b => Bool -> b
bool (Bool -> Expr 'BoolSort)
-> (HaskellType 'BoolSort -> Bool)
-> HaskellType 'BoolSort
-> Expr 'BoolSort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
HaskellType 'BoolSort -> Bool
forall b. Boolean b => b -> b
not (HaskellType 'BoolSort -> Expr 'BoolSort)
-> HaskellType 'BoolSort -> Expr 'BoolSort
forall a b. (a -> b) -> a -> b
$ HaskellType 'BoolSort
x
  not Expr 'BoolSort
x = Expr 'BoolSort -> Expr 'BoolSort
forall (t :: SMTSort). Boolean (HaskellType t) => Expr t -> Expr t
Not Expr 'BoolSort
x
  {-# INLINE not #-}
  xor :: Expr 'BoolSort -> Expr 'BoolSort -> Expr 'BoolSort
xor (Constant (BoolValue HaskellType 'BoolSort
x)) Expr 'BoolSort
y = if Bool
HaskellType 'BoolSort
x then Expr 'BoolSort -> Expr 'BoolSort
forall b. Boolean b => b -> b
not Expr 'BoolSort
y else Expr 'BoolSort
y
  xor Expr 'BoolSort
x (Constant (BoolValue HaskellType 'BoolSort
y)) = if Bool
HaskellType 'BoolSort
y then Expr 'BoolSort -> Expr 'BoolSort
forall b. Boolean b => b -> b
not Expr 'BoolSort
x else Expr 'BoolSort
x
  xor Expr 'BoolSort
x Expr 'BoolSort
y = Expr 'BoolSort -> Expr 'BoolSort -> Expr 'BoolSort
forall (t :: SMTSort).
Boolean (HaskellType t) =>
Expr t -> Expr t -> Expr t
Xor Expr 'BoolSort
x Expr 'BoolSort
y
  {-# 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 Semigroup (Expr StringSort) where
  <> :: Expr 'StringSort -> Expr 'StringSort -> Expr 'StringSort
(<>) = Expr 'StringSort -> Expr 'StringSort -> Expr 'StringSort
StrConcat

instance Monoid (Expr StringSort) where
  mempty :: Expr 'StringSort
mempty = Value 'StringSort -> Expr 'StringSort
forall (t :: SMTSort). Value t -> Expr t
Constant (Value 'StringSort -> Expr 'StringSort)
-> Value 'StringSort -> Expr 'StringSort
forall a b. (a -> b) -> a -> b
$ HaskellType 'StringSort -> Value 'StringSort
StringValue Text
HaskellType 'StringSort
forall a. Monoid a => a
mempty
  mappend :: Expr 'StringSort -> Expr 'StringSort -> Expr 'StringSort
mappend = Expr 'StringSort -> Expr 'StringSort -> Expr 'StringSort
forall a. Semigroup a => a -> a -> a
(<>)

instance IsString (Expr StringSort) where
  fromString :: String -> Expr 'StringSort
fromString = Value 'StringSort -> Expr 'StringSort
forall (t :: SMTSort). Value t -> Expr t
Constant (Value 'StringSort -> Expr 'StringSort)
-> (String -> Value 'StringSort) -> String -> Expr 'StringSort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Value 'StringSort
HaskellType 'StringSort -> Value 'StringSort
StringValue (Text -> Value 'StringSort)
-> (String -> Text) -> String -> Value 'StringSort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
pack

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)
  render (StringValue HaskellType 'StringSort
x) = Builder
"\"" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Text -> Builder
forall a. Render a => a -> Builder
render Text
HaskellType 'StringSort
x Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
"\""

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 (StrConcat Expr 'StringSort
x Expr 'StringSort
y)        = Builder -> Builder -> Builder -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"str.++"  (Expr 'StringSort -> Builder
forall a. Render a => a -> Builder
render Expr 'StringSort
x) (Expr 'StringSort -> Builder
forall a. Render a => a -> Builder
render Expr 'StringSort
y)
  render (StrLength Expr 'StringSort
x)          = Builder -> Builder -> Builder
forall a. Render a => Builder -> a -> Builder
renderUnary  Builder
"str.len" (Expr 'StringSort -> Builder
forall a. Render a => a -> Builder
render Expr 'StringSort
x)
  render (StrLT Expr 'StringSort
x Expr 'StringSort
y)            = Builder -> Builder -> Builder -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"str.<"   (Expr 'StringSort -> Builder
forall a. Render a => a -> Builder
render Expr 'StringSort
x) (Expr 'StringSort -> Builder
forall a. Render a => a -> Builder
render Expr 'StringSort
y)
  render (StrLTHE Expr 'StringSort
x Expr 'StringSort
y)          = Builder -> Builder -> Builder -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"str.<="  (Expr 'StringSort -> Builder
forall a. Render a => a -> Builder
render Expr 'StringSort
x) (Expr 'StringSort -> Builder
forall a. Render a => a -> Builder
render Expr 'StringSort
y)
  render (StrAt Expr 'StringSort
x Expr 'IntSort
i)            = Builder -> Builder -> Builder -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"str.at"  (Expr 'StringSort -> Builder
forall a. Render a => a -> Builder
render Expr 'StringSort
x) (Expr 'IntSort -> Builder
forall a. Render a => a -> Builder
render Expr 'IntSort
i)
  render (StrSubstring Expr 'StringSort
x Expr 'IntSort
i Expr 'IntSort
j)   = Builder -> Builder -> Builder -> Builder -> Builder
forall a b c.
(Render a, Render b, Render c) =>
Builder -> a -> b -> c -> Builder
renderTernary Builder
"str.substr"  (Expr 'StringSort -> Builder
forall a. Render a => a -> Builder
render Expr 'StringSort
x) (Expr 'IntSort -> Builder
forall a. Render a => a -> Builder
render Expr 'IntSort
i) (Expr 'IntSort -> Builder
forall a. Render a => a -> Builder
render Expr 'IntSort
j)
  render (StrPrefixOf Expr 'StringSort
x Expr 'StringSort
y)      = Builder -> Builder -> Builder -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"str.prefixof" (Expr 'StringSort -> Builder
forall a. Render a => a -> Builder
render Expr 'StringSort
x) (Expr 'StringSort -> Builder
forall a. Render a => a -> Builder
render Expr 'StringSort
y)
  render (StrSuffixOf Expr 'StringSort
x Expr 'StringSort
y)      = Builder -> Builder -> Builder -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"str.suffixof" (Expr 'StringSort -> Builder
forall a. Render a => a -> Builder
render Expr 'StringSort
x) (Expr 'StringSort -> Builder
forall a. Render a => a -> Builder
render Expr 'StringSort
y)
  render (StrContains Expr 'StringSort
x Expr 'StringSort
y)      = Builder -> Builder -> Builder -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
renderBinary Builder
"str.contains" (Expr 'StringSort -> Builder
forall a. Render a => a -> Builder
render Expr 'StringSort
x) (Expr 'StringSort -> Builder
forall a. Render a => a -> Builder
render Expr 'StringSort
y)
  render (StrIndexOf Expr 'StringSort
x Expr 'StringSort
y Expr 'IntSort
i)     = Builder -> Builder -> Builder -> Builder -> Builder
forall a b c.
(Render a, Render b, Render c) =>
Builder -> a -> b -> c -> Builder
renderTernary Builder
"str.indexof"     (Expr 'StringSort -> Builder
forall a. Render a => a -> Builder
render Expr 'StringSort
x) (Expr 'StringSort -> Builder
forall a. Render a => a -> Builder
render Expr 'StringSort
y) (Expr 'IntSort -> Builder
forall a. Render a => a -> Builder
render Expr 'IntSort
i)
  render (StrReplace Expr 'StringSort
x Expr 'StringSort
y Expr 'StringSort
y')    = Builder -> Builder -> Builder -> Builder -> Builder
forall a b c.
(Render a, Render b, Render c) =>
Builder -> a -> b -> c -> Builder
renderTernary Builder
"str.replace"     (Expr 'StringSort -> Builder
forall a. Render a => a -> Builder
render Expr 'StringSort
x) (Expr 'StringSort -> Builder
forall a. Render a => a -> Builder
render Expr 'StringSort
y) (Expr 'StringSort -> Builder
forall a. Render a => a -> Builder
render Expr 'StringSort
y')
  render (StrReplaceAll Expr 'StringSort
x Expr 'StringSort
y Expr 'StringSort
y') = Builder -> Builder -> Builder -> Builder -> Builder
forall a b c.
(Render a, Render b, Render c) =>
Builder -> a -> b -> c -> Builder
renderTernary Builder
"str.replace_all" (Expr 'StringSort -> Builder
forall a. Render a => a -> Builder
render Expr 'StringSort
x) (Expr 'StringSort -> Builder
forall a. Render a => a -> Builder
render Expr 'StringSort
y) (Expr 'StringSort -> Builder
forall a. Render a => a -> Builder
render Expr 'StringSort
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 (Value t) where
  show :: Value t -> String
show = ByteString -> String
toString (ByteString -> String)
-> (Value t -> ByteString) -> Value t -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Builder -> ByteString
toLazyByteString (Builder -> ByteString)
-> (Value t -> Builder) -> Value t -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value t -> Builder
forall a. Render a => a -> Builder
render

instance KnownSMTSort t => Show (Expr t) where
  show :: Expr t -> String
show = ByteString -> String
toString (ByteString -> String)
-> (Expr t -> ByteString) -> Expr t -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Builder -> ByteString
toLazyByteString (Builder -> ByteString)
-> (Expr t -> Builder) -> Expr t -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr t -> Builder
forall a. Render a => a -> Builder
render