{-# LANGUAGE LambdaCase #-}

module Language.Hasmtlib.Internal.Render where

import Language.Hasmtlib.Type.OMT
import Language.Hasmtlib.Type.SMT
import Language.Hasmtlib.Type.Expr
import Language.Hasmtlib.Type.Value
import Language.Hasmtlib.Type.Option
import Language.Hasmtlib.Type.SMTSort
import Language.Hasmtlib.Type.Bitvec
import Language.Hasmtlib.Type.ArrayMap
import Data.Ratio
import Data.Coerce
import Data.Some.Constraint
import Data.Sequence
import Data.Foldable (foldl')
import Data.Map (size, minViewWithKey)
import Data.ByteString.Builder
import Data.ByteString.Lazy.UTF8 (toString)
import qualified Data.Text as Text
import qualified Data.Text.Encoding as Text.Enc
import qualified Data.Vector.Sized as V
import Control.Lens hiding (op)
import GHC.TypeNats

render1 :: Render a => Builder -> a -> Builder
render1 :: forall a. Render a => Builder -> a -> Builder
render1 Builder
op a
x = Builder
"(" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
op Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
" " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> a -> Builder
forall a. Render a => a -> Builder
render a
x Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
{-# INLINE render1 #-}

render2 :: (Render a, Render b) => Builder -> a -> b -> Builder
render2 :: forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
render2 Builder
op a
x b
y = Builder
"(" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
op Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
" " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> a -> Builder
forall a. Render a => a -> Builder
render a
x Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
" " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> b -> Builder
forall a. Render a => a -> Builder
render b
y Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
{-# INLINE render2 #-}

render3 :: (Render a, Render b, Render c) => Builder -> a -> b -> c -> Builder
render3 :: forall a b c.
(Render a, Render b, Render c) =>
Builder -> a -> b -> c -> Builder
render3 Builder
op a
x b
y c
z = Builder
"(" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
op Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
" " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> a -> Builder
forall a. Render a => a -> Builder
render a
x Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
" " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> b -> Builder
forall a. Render a => a -> Builder
render b
y Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
" " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> c -> Builder
forall a. Render a => a -> Builder
render c
z Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
{-# INLINE render3 #-}

renderN :: Render a => Builder -> [a] -> Builder
renderN :: forall a. Render a => Builder -> [a] -> Builder
renderN Builder
op [a]
xs = Builder
"(" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
op Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
renderedXs Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
  where
    renderedXs :: Builder
renderedXs = (Builder -> a -> Builder) -> Builder -> [a] -> Builder
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\Builder
s a
x -> Builder
s Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
" " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> a -> Builder
forall a. Render a => a -> Builder
render a
x) Builder
forall a. Monoid a => a
mempty [a]
xs
{-# INLINE renderN #-}

-- | Render values to their SMTLib2-Lisp form, represented as 'Builder'.
class Render a where
  render :: a -> Builder

instance Render Bool where
  render :: Bool -> Builder
render Bool
b = if Bool
b then Builder
"true" else Builder
"false"
  {-# INLINE render #-}

instance Render Nat where
  render :: Nat -> Builder
render = Integer -> Builder
integerDec (Integer -> Builder) -> (Nat -> Integer) -> Nat -> Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral
  {-# INLINE render #-}

instance Render Integer where
  render :: Integer -> Builder
render Integer
x
    | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0     = Builder
"(- " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Integer -> Builder
integerDec (Integer -> Integer
forall a. Num a => a -> a
abs Integer
x) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
    | Bool
otherwise = Integer -> Builder
integerDec Integer
x
  {-# INLINE render #-}

instance Render Double where
  render :: Double -> Builder
render Double
x
    | Double
x Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
< Double
0     = Builder
"(- " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> FloatFormat -> Double -> Builder
formatDouble FloatFormat
standardDefaultPrecision (Double -> Double
forall a. Num a => a -> a
abs Double
x) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
    | Bool
otherwise = FloatFormat -> Double -> Builder
formatDouble FloatFormat
standardDefaultPrecision Double
x
  {-# INLINE render #-}

instance Render Rational where
  render :: Rational -> Builder
render Rational
x = if Integer
num Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0
             then Builder
"(/ " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
"(- " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Integer -> Builder
forall a. Render a => a -> Builder
render (Integer -> Integer
forall a. Num a => a -> a
abs Integer
num) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
") " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Integer -> Builder
forall a. Render a => a -> Builder
render Integer
denom Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
             else Builder
"(/ " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Integer -> Builder
forall a. Render a => a -> Builder
render Integer
num Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
" " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Integer -> Builder
forall a. Render a => a -> Builder
render Integer
denom Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
    where
      num :: Integer
num = Rational -> Integer
forall a. Ratio a -> a
numerator Rational
x
      denom :: Integer
denom = Rational -> Integer
forall a. Ratio a -> a
denominator Rational
x

instance Render Char where
  render :: Char -> Builder
render = Char -> Builder
char8
  {-# INLINE render #-}

instance Render String where
  render :: String -> Builder
render = String -> Builder
string8
  {-# INLINE render #-}

instance Render Builder where
  render :: Builder -> Builder
render = Builder -> Builder
forall a. a -> a
id
  {-# INLINE render #-}

instance Render Text.Text where
  render :: Text -> Builder
render = Text -> Builder
Text.Enc.encodeUtf8Builder
  {-# INLINE render #-}

instance Render (Bitvec enc n) where
  render :: Bitvec enc n -> Builder
render = String -> Builder
stringUtf8 (String -> Builder)
-> (Bitvec enc n -> String) -> Bitvec enc n -> Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bitvec enc n -> String
forall a. Show a => a -> String
show
  {-# INLINE render #-}

instance Render (SMTVar t) where
  render :: SMTVar t -> Builder
render SMTVar t
v = Builder
"var_" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Int -> Builder
intDec (forall a b. Coercible a b => a -> b
forall a b. Coercible a b => a -> b
coerce @(SMTVar t) @Int SMTVar t
v)
  {-# INLINE render #-}

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 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)  = Rational -> Builder
forall a. Render a => a -> Builder
render Rational
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 enc n)
v)  = Builder
"#b" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Bitvec enc n -> Builder
forall a. Render a => a -> Builder
render Bitvec enc n
HaskellType ('BvSort enc 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),
 Ord (HaskellType v)) =>
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), Ord (HaskellType v)) => ConstArray (HaskellType k) (HaskellType v) -> SSMTSort (ArraySort k v)
      goSing :: forall (k :: SMTSort) (v :: SMTSort).
(KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k),
 Ord (HaskellType v)) =>
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 => 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

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
render2 (case Expr t -> SSMTSort t
forall (prxy :: SMTSort -> *) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> SSMTSort t
sortSing' Expr t
x of SBvSort Proxy enc
_ Proxy n
_ -> Builder
"bvadd" ; SSMTSort t
_ -> Builder
"+") Expr t
x Expr t
y
  render (Minus Expr t
x Expr t
y)  = Builder -> Expr t -> Expr t -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
render2 (case Expr t -> SSMTSort t
forall (prxy :: SMTSort -> *) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> SSMTSort t
sortSing' Expr t
x of SBvSort Proxy enc
_ Proxy n
_ -> Builder
"bvsub" ; SSMTSort t
_ -> Builder
"-") Expr t
x Expr t
y
  render (Neg Expr t
x)      = Builder -> Expr t -> Builder
forall a. Render a => Builder -> a -> Builder
render1  (case Expr t -> SSMTSort t
forall (prxy :: SMTSort -> *) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> SSMTSort t
sortSing' Expr t
x of SBvSort Proxy enc
_ Proxy n
_ -> Builder
"bvneg" ; SSMTSort t
_ -> 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
render2 (case Expr t -> SSMTSort t
forall (prxy :: SMTSort -> *) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> SSMTSort t
sortSing' Expr t
x of SBvSort Proxy enc
_ Proxy n
_ -> Builder
"bvmul" ; SSMTSort t
_ -> Builder
"*") Expr t
x Expr t
y
  render (Abs Expr t
x)      = Builder -> Expr t -> Builder
forall a. Render a => Builder -> a -> Builder
render1  Builder
"abs" Expr t
x
  render (Mod Expr t
x Expr t
y)    = Builder -> Expr t -> Expr t -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
render2 Builder
opStr Expr t
x Expr t
y
    where
      opStr :: Builder
opStr = case Expr t -> SSMTSort t
forall (prxy :: SMTSort -> *) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> SSMTSort t
sortSing' Expr t
x of
        SBvSort Proxy enc
enc Proxy n
_ -> case Proxy enc -> SBvEnc enc
forall (enc :: BvEnc) (prxy :: BvEnc -> *).
KnownBvEnc enc =>
prxy enc -> SBvEnc enc
bvEncSing' Proxy enc
enc of
          SBvEnc enc
SUnsigned -> Builder
"bvurem"
          SBvEnc enc
SSigned -> Builder
"bvsmod"
        SSMTSort t
_ -> Builder
"mod"
  render (Rem Expr t
x Expr t
y)    = Builder -> Expr t -> Expr t -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
render2 Builder
opStr Expr t
x Expr t
y
    where
      opStr :: Builder
opStr = case Expr t -> SSMTSort t
forall (prxy :: SMTSort -> *) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> SSMTSort t
sortSing' Expr t
x of
        SBvSort Proxy enc
enc Proxy n
_ -> case Proxy enc -> SBvEnc enc
forall (enc :: BvEnc) (prxy :: BvEnc -> *).
KnownBvEnc enc =>
prxy enc -> SBvEnc enc
bvEncSing' Proxy enc
enc of
          SBvEnc enc
SUnsigned -> Builder
"bvurem"
          SBvEnc enc
SSigned -> Builder
"bvsrem"
        SSMTSort t
_ -> Builder
"rem"
  render (IDiv Expr t
x Expr t
y)   = Builder -> Expr t -> Expr t -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
render2 Builder
opStr Expr t
x Expr t
y
    where
      opStr :: Builder
opStr = case Expr t -> SSMTSort t
forall (prxy :: SMTSort -> *) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> SSMTSort t
sortSing' Expr t
x of
        SBvSort Proxy enc
enc Proxy n
_ -> case Proxy enc -> SBvEnc enc
forall (enc :: BvEnc) (prxy :: BvEnc -> *).
KnownBvEnc enc =>
prxy enc -> SBvEnc enc
bvEncSing' Proxy enc
enc of
          SBvEnc enc
SUnsigned -> Builder
"bvudiv"
          SBvEnc enc
SSigned -> Builder
"bvsdiv"
        SSMTSort t
_ -> Builder
"div"
  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
render2 Builder
"/" Expr 'RealSort
x Expr 'RealSort
y
  render (LTH Expr t1
x Expr t1
y)    = Builder -> Expr t1 -> Expr t1 -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
render2 Builder
opStr Expr t1
x Expr t1
y
    where
      opStr :: Builder
opStr = case Expr t1 -> SSMTSort t1
forall (prxy :: SMTSort -> *) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> SSMTSort t
sortSing' Expr t1
x of
        SBvSort Proxy enc
enc Proxy n
_ -> case Proxy enc -> SBvEnc enc
forall (enc :: BvEnc) (prxy :: BvEnc -> *).
KnownBvEnc enc =>
prxy enc -> SBvEnc enc
bvEncSing' Proxy enc
enc of
          SBvEnc enc
SUnsigned -> Builder
"bvult"
          SBvEnc enc
SSigned -> Builder
"bvslt"
        SSMTSort t1
SStringSort -> Builder
"str.<"
        SSMTSort t1
_ -> Builder
"<"
  render (LTHE Expr t1
x Expr t1
y)   = Builder -> Expr t1 -> Expr t1 -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
render2 Builder
opStr Expr t1
x Expr t1
y
    where
      opStr :: Builder
opStr = case Expr t1 -> SSMTSort t1
forall (prxy :: SMTSort -> *) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> SSMTSort t
sortSing' Expr t1
x of
        SBvSort Proxy enc
enc Proxy n
_ -> case Proxy enc -> SBvEnc enc
forall (enc :: BvEnc) (prxy :: BvEnc -> *).
KnownBvEnc enc =>
prxy enc -> SBvEnc enc
bvEncSing' Proxy enc
enc of
          SBvEnc enc
SUnsigned -> Builder
"bvule"
          SBvEnc enc
SSigned -> Builder
"bvsle"
        SSMTSort t1
SStringSort -> Builder
"str.<="
        SSMTSort t1
_ -> Builder
"<="
  render (EQU Vector (n + 2) (Expr t1)
xs)     = Builder -> [Expr t1] -> Builder
forall a. Render a => Builder -> [a] -> Builder
renderN Builder
"=" ([Expr t1] -> Builder) -> [Expr t1] -> Builder
forall a b. (a -> b) -> a -> b
$ Vector (n + 2) (Expr t1) -> [Expr t1]
forall (n :: Nat) a. Vector n a -> [a]
V.toList Vector (n + 2) (Expr t1)
xs
  render (Distinct Vector (n + 2) (Expr t1)
xs)= Builder -> [Expr t1] -> Builder
forall a. Render a => Builder -> [a] -> Builder
renderN Builder
"distinct" ([Expr t1] -> Builder) -> [Expr t1] -> Builder
forall a b. (a -> b) -> a -> b
$ Vector (n + 2) (Expr t1) -> [Expr t1]
forall (n :: Nat) a. Vector n a -> [a]
V.toList Vector (n + 2) (Expr t1)
xs
  render (GTHE Expr t1
x Expr t1
y)   = case Expr t1 -> SSMTSort t1
forall (prxy :: SMTSort -> *) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> SSMTSort t
sortSing' Expr t1
x of
    SBvSort Proxy enc
enc Proxy n
_ -> case Proxy enc -> SBvEnc enc
forall (enc :: BvEnc) (prxy :: BvEnc -> *).
KnownBvEnc enc =>
prxy enc -> SBvEnc enc
bvEncSing' Proxy enc
enc of
      SBvEnc enc
SUnsigned -> Builder -> Expr t1 -> Expr t1 -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
render2 Builder
"bvuge" Expr t1
x Expr t1
y
      SBvEnc enc
SSigned   -> Builder -> Expr t1 -> Expr t1 -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
render2 Builder
"bvsge" Expr t1
x Expr t1
y
    SSMTSort t1
SStringSort -> Builder -> Expr t1 -> Expr t1 -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
render2 Builder
"str.<=" Expr t1
y Expr t1
x
    SSMTSort t1
_           -> Builder -> Expr t1 -> Expr t1 -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
render2 Builder
">=" Expr t1
x Expr t1
y
  render (GTH Expr t1
x Expr t1
y)    = case Expr t1 -> SSMTSort t1
forall (prxy :: SMTSort -> *) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> SSMTSort t
sortSing' Expr t1
x of
    SBvSort Proxy enc
enc Proxy n
_ -> case Proxy enc -> SBvEnc enc
forall (enc :: BvEnc) (prxy :: BvEnc -> *).
KnownBvEnc enc =>
prxy enc -> SBvEnc enc
bvEncSing' Proxy enc
enc of
      SBvEnc enc
SUnsigned -> Builder -> Expr t1 -> Expr t1 -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
render2 Builder
"bvugt" Expr t1
x Expr t1
y
      SBvEnc enc
SSigned   -> Builder -> Expr t1 -> Expr t1 -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
render2 Builder
"bvsgt" Expr t1
x Expr t1
y
    SSMTSort t1
SStringSort -> Builder -> Expr t1 -> Expr t1 -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
render2 Builder
"str.<" Expr t1
y Expr t1
x
    SSMTSort t1
_           -> Builder -> Expr t1 -> Expr t1 -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
render2 Builder
">" Expr t1
x Expr t1
y
  render (Not Expr t
x)      = Builder -> Expr t -> Builder
forall a. Render a => Builder -> a -> Builder
render1  (case Expr t -> SSMTSort t
forall (prxy :: SMTSort -> *) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> SSMTSort t
sortSing' Expr t
x of SBvSort Proxy enc
_ Proxy n
_ -> Builder
"bvnot" ; SSMTSort t
_ -> 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
render2 (case Expr t -> SSMTSort t
forall (prxy :: SMTSort -> *) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> SSMTSort t
sortSing' Expr t
x of SBvSort Proxy enc
_ Proxy n
_ -> Builder
"bvand" ; SSMTSort t
_ -> 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
render2 (case Expr t -> SSMTSort t
forall (prxy :: SMTSort -> *) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> SSMTSort t
sortSing' Expr t
x of SBvSort Proxy enc
_ Proxy n
_ -> Builder
"bvor" ; SSMTSort t
_ -> 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
render2 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
render2 (case Expr t -> SSMTSort t
forall (prxy :: SMTSort -> *) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> SSMTSort t
sortSing' Expr t
x of SBvSort Proxy enc
_ Proxy n
_ -> Builder
"bvxor" ; SSMTSort t
_ -> 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
render1 Builder
"sqrt" Expr 'RealSort
x
  render (Exp Expr 'RealSort
x)      = Builder -> Expr 'RealSort -> Builder
forall a. Render a => Builder -> a -> Builder
render1 Builder
"exp" Expr 'RealSort
x
  render (Sin Expr 'RealSort
x)      = Builder -> Expr 'RealSort -> Builder
forall a. Render a => Builder -> a -> Builder
render1 Builder
"sin" Expr 'RealSort
x
  render (Cos Expr 'RealSort
x)      = Builder -> Expr 'RealSort -> Builder
forall a. Render a => Builder -> a -> Builder
render1 Builder
"cos" Expr 'RealSort
x
  render (Tan Expr 'RealSort
x)      = Builder -> Expr 'RealSort -> Builder
forall a. Render a => Builder -> a -> Builder
render1 Builder
"tan" Expr 'RealSort
x
  render (Asin Expr 'RealSort
x)     = Builder -> Expr 'RealSort -> Builder
forall a. Render a => Builder -> a -> Builder
render1 Builder
"arcsin" Expr 'RealSort
x
  render (Acos Expr 'RealSort
x)     = Builder -> Expr 'RealSort -> Builder
forall a. Render a => Builder -> a -> Builder
render1 Builder
"arccos" Expr 'RealSort
x
  render (Atan Expr 'RealSort
x)     = Builder -> Expr 'RealSort -> Builder
forall a. Render a => Builder -> a -> Builder
render1 Builder
"arctan" Expr 'RealSort
x
  render (ToReal Expr 'IntSort
x)   = Builder -> Expr 'IntSort -> Builder
forall a. Render a => Builder -> a -> Builder
render1 Builder
"to_real" Expr 'IntSort
x
  render (ToInt Expr 'RealSort
x)    = Builder -> Expr 'RealSort -> Builder
forall a. Render a => Builder -> a -> Builder
render1 Builder
"to_int" Expr 'RealSort
x
  render (IsInt Expr 'RealSort
x)    = Builder -> Expr 'RealSort -> Builder
forall a. Render a => Builder -> a -> Builder
render1 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
render3 Builder
"ite" Expr 'BoolSort
p Expr t
t Expr t
f
  render (BvNand Expr ('BvSort enc n)
x Expr ('BvSort enc n)
y)       = Builder -> Builder -> Builder -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
render2 Builder
"bvnand" (Expr ('BvSort enc n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort enc n)
x) (Expr ('BvSort enc n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort enc n)
y)
  render (BvNor Expr ('BvSort enc n)
x Expr ('BvSort enc n)
y)        = Builder -> Builder -> Builder -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
render2 Builder
"bvnor"  (Expr ('BvSort enc n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort enc n)
x) (Expr ('BvSort enc n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort enc n)
y)
  render (BvShL Expr ('BvSort enc n)
x Expr ('BvSort enc n)
y)        = Builder -> Builder -> Builder -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
render2 Builder
"bvshl"  (Expr ('BvSort enc n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort enc n)
x) (Expr ('BvSort enc n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort enc n)
y)
  render (BvLShR Expr ('BvSort 'Unsigned n)
x Expr ('BvSort 'Unsigned n)
y)       = Builder -> Builder -> Builder -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
render2 Builder
"bvlshr" (Expr ('BvSort 'Unsigned n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort 'Unsigned n)
x) (Expr ('BvSort 'Unsigned n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort 'Unsigned n)
y)
  render (BvAShR Expr ('BvSort 'Signed n)
x Expr ('BvSort 'Signed n)
y)       = Builder -> Builder -> Builder -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
render2 Builder
"bvashr" (Expr ('BvSort 'Signed n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort 'Signed n)
x) (Expr ('BvSort 'Signed n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort 'Signed n)
y)
  render (BvConcat Expr ('BvSort enc n)
x Expr ('BvSort enc m)
y)     = Builder -> Builder -> Builder -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
render2 Builder
"concat" (Expr ('BvSort enc n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort enc n)
x) (Expr ('BvSort enc m) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort enc m)
y)
  render (BvRotL a
i Expr ('BvSort enc n)
x)       = Builder -> Builder -> Builder
forall a. Render a => Builder -> a -> Builder
render1 (Builder -> Builder -> Builder -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
render2 Builder
"_" (Builder
"rotate_left"  :: Builder) (Integer -> Builder
forall a. Render a => a -> Builder
render (Integer -> Builder) -> Integer -> Builder
forall a b. (a -> b) -> a -> b
$ a -> Integer
forall a. Integral a => a -> Integer
toInteger a
i)) (Expr ('BvSort enc n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort enc n)
x)
  render (BvRotR a
i Expr ('BvSort enc n)
x)       = Builder -> Builder -> Builder
forall a. Render a => Builder -> a -> Builder
render1 (Builder -> Builder -> Builder -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
render2 Builder
"_" (Builder
"rotate_right" :: Builder) (Integer -> Builder
forall a. Render a => a -> Builder
render (Integer -> Builder) -> Integer -> Builder
forall a b. (a -> b) -> a -> b
$ a -> Integer
forall a. Integral a => a -> Integer
toInteger a
i)) (Expr ('BvSort enc n) -> Builder
forall a. Render a => a -> Builder
render Expr ('BvSort enc n)
x)
  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
render2  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
render3 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
render2 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
render1  Builder
"str.len" (Expr 'StringSort -> Builder
forall a. Render a => a -> Builder
render Expr 'StringSort
x)
  render (StrAt Expr 'StringSort
x Expr 'IntSort
i)            = Builder -> Builder -> Builder -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
render2 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
render3 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
render2 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
render2 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
render2 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
render3 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
render3 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
render3 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 t1)
mQvar Expr t1 -> Expr 'BoolSort
f) = Builder
-> Maybe (SMTVar t1) -> (Expr t1 -> Expr 'BoolSort) -> Builder
forall (t :: SMTSort).
KnownSMTSort t =>
Builder
-> Maybe (SMTVar t) -> (Expr t -> Expr 'BoolSort) -> Builder
renderQuantifier Builder
"forall" Maybe (SMTVar t1)
mQvar Expr t1 -> Expr 'BoolSort
f
  render (Exists Maybe (SMTVar t1)
mQvar Expr t1 -> Expr 'BoolSort
f) = Builder
-> Maybe (SMTVar t1) -> (Expr t1 -> Expr 'BoolSort) -> Builder
forall (t :: SMTSort).
KnownSMTSort t =>
Builder
-> Maybe (SMTVar t) -> (Expr t -> Expr 'BoolSort) -> Builder
renderQuantifier Builder
"exists" Maybe (SMTVar t1)
mQvar Expr t1 -> 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
render2
    Builder
qname
    (Builder
"(" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder -> SSMTSort t -> Builder
forall a. Render a => Builder -> a -> Builder
render1 (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). KnownSMTSort t => 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 Render (SSMTSort t) where
  render :: SSMTSort t -> Builder
render SSMTSort t
SBoolSort   = Builder
"Bool"
  render SSMTSort t
SIntSort    = Builder
"Int"
  render SSMTSort t
SRealSort   = Builder
"Real"
  render (SBvSort Proxy enc
_ Proxy n
p) = Builder -> Builder -> Nat -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
render2 Builder
"_" (Builder
"BitVec" :: Builder) (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal Proxy n
p)
  render (SArraySort Proxy k
k Proxy v
v) = Builder -> SSMTSort k -> SSMTSort v -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
render2 Builder
"Array" (Proxy k -> SSMTSort k
forall (prxy :: SMTSort -> *) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> SSMTSort t
sortSing' Proxy k
k) (Proxy v -> SSMTSort v
forall (prxy :: SMTSort -> *) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> SSMTSort t
sortSing' Proxy v
v)
  render SSMTSort t
SStringSort   = Builder
"String"
  {-# INLINE render #-}

instance Render SMTOption where
  render :: SMTOption -> Builder
render (PrintSuccess  Bool
b) = Builder -> Builder -> Bool -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
render2 Builder
"set-option" (Builder
":print-success"  :: Builder) Bool
b
  render (ProduceModels Bool
b) = Builder -> Builder -> Bool -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
render2 Builder
"set-option" (Builder
":produce-models" :: Builder) Bool
b
  render (Incremental   Bool
b) = Builder -> Builder -> Bool -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
render2 Builder
"set-option" (Builder
":incremental"    :: Builder) Bool
b
  render (Custom String
k String
v)      = Builder -> Builder -> Builder -> Builder
forall a b. (Render a, Render b) => Builder -> a -> b -> Builder
render2 Builder
"set-option" (Builder
":" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> String -> Builder
forall a. Render a => a -> Builder
render String
k) (String -> Builder
forall a. Render a => a -> Builder
render String
v)

instance Render SoftFormula where
  render :: SoftFormula -> Builder
render SoftFormula
sf = Builder
"(assert-soft " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Expr 'BoolSort -> Builder
forall a. Render a => a -> Builder
render (SoftFormula
sfSoftFormula
-> Getting (Expr 'BoolSort) SoftFormula (Expr 'BoolSort)
-> Expr 'BoolSort
forall s a. s -> Getting a s a -> a
^.Getting (Expr 'BoolSort) SoftFormula (Expr 'BoolSort)
Lens' SoftFormula (Expr 'BoolSort)
formula) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
" :weight " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder -> (Double -> Builder) -> Maybe Double -> Builder
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Builder
"1" Double -> Builder
forall a. Render a => a -> Builder
render (SoftFormula
sfSoftFormula
-> Getting (Maybe Double) SoftFormula (Maybe Double)
-> Maybe Double
forall s a. s -> Getting a s a -> a
^.Getting (Maybe Double) SoftFormula (Maybe Double)
Lens' SoftFormula (Maybe Double)
mWeight) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Maybe String -> Builder
forall {a}. Render a => Maybe a -> Builder
renderGroupId (SoftFormula
sfSoftFormula
-> Getting (Maybe String) SoftFormula (Maybe String)
-> Maybe String
forall s a. s -> Getting a s a -> a
^.Getting (Maybe String) SoftFormula (Maybe String)
Lens' SoftFormula (Maybe String)
mGroupId) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
    where
      renderGroupId :: Maybe a -> Builder
renderGroupId Maybe a
Nothing = Builder
forall a. Monoid a => a
mempty
      renderGroupId (Just a
groupId) = Builder
" :id " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> a -> Builder
forall a. Render a => a -> Builder
render a
groupId

instance KnownSMTSort t => Render (Minimize t) where
  render :: Minimize t -> Builder
render (Minimize Expr t
expr) = Builder
"(minimize " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Expr t -> Builder
forall a. Render a => a -> Builder
render Expr t
expr Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"

instance KnownSMTSort t => Render (Maximize t) where
  render :: Maximize t -> Builder
render (Maximize Expr t
expr) = Builder
"(maximize " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Expr t -> Builder
forall a. Render a => a -> Builder
render Expr t
expr Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"

renderSetLogic :: Builder -> Builder
renderSetLogic :: Builder -> Builder
renderSetLogic = Builder -> Builder -> Builder
forall a. Render a => Builder -> a -> Builder
render1 Builder
"set-logic"
{-# INLINE renderSetLogic #-}

renderDeclareVar :: forall t. KnownSMTSort t => SMTVar t -> Builder
renderDeclareVar :: forall (t :: SMTSort). KnownSMTSort t => SMTVar t -> Builder
renderDeclareVar SMTVar t
v = Builder -> SMTVar t -> Builder -> SSMTSort t -> Builder
forall a b c.
(Render a, Render b, Render c) =>
Builder -> a -> b -> c -> Builder
render3 Builder
"declare-fun" SMTVar t
v (Builder
"()" :: Builder) (forall (t :: SMTSort). KnownSMTSort t => SSMTSort t
sortSing @t)
{-# INLINE renderDeclareVar #-}

renderAssert :: Expr BoolSort -> Builder
renderAssert :: Expr 'BoolSort -> Builder
renderAssert = Builder -> Expr 'BoolSort -> Builder
forall a. Render a => Builder -> a -> Builder
render1 Builder
"assert"
{-# INLINE renderAssert #-}

renderGetValue :: SMTVar t -> Builder
renderGetValue :: forall (t :: SMTSort). SMTVar t -> Builder
renderGetValue SMTVar t
x = Builder -> Builder -> Builder
forall a. Render a => Builder -> a -> Builder
render1 Builder
"get-value" (Builder -> Builder) -> Builder -> Builder
forall a b. (a -> b) -> a -> b
$ Builder
"(" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> SMTVar t -> Builder
forall a. Render a => a -> Builder
render SMTVar t
x Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
{-# INLINE renderGetValue #-}

renderPush :: Integer -> Builder
renderPush :: Integer -> Builder
renderPush Integer
i = Builder
"(push "Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Integer -> Builder
forall a. Render a => a -> Builder
render Integer
i Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>Builder
")"
{-# INLINE renderPush #-}

renderPop :: Integer -> Builder
renderPop :: Integer -> Builder
renderPop Integer
i = Builder
"(pop "Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Integer -> Builder
forall a. Render a => a -> Builder
render Integer
i Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>Builder
")"
{-# INLINE renderPop #-}

renderCheckSat :: Builder
renderCheckSat :: Builder
renderCheckSat = Builder
"(check-sat)"
{-# INLINE renderCheckSat #-}

renderGetModel :: Builder
renderGetModel :: Builder
renderGetModel = Builder
"(get-model)"
{-# INLINE renderGetModel #-}

class RenderProblem s where
  renderOptions        :: s -> Seq Builder
  renderLogic          :: s -> Builder
  renderDeclareVars    :: s -> Seq Builder
  renderAssertions     :: s -> Seq Builder
  renderSoftAssertions :: s -> Seq Builder
  renderMinimizations  :: s -> Seq Builder
  renderMaximizations  :: s -> Seq Builder

instance RenderProblem SMT where
  renderOptions :: SMT -> Seq Builder
renderOptions = [Builder] -> Seq Builder
forall a. [a] -> Seq a
fromList ([Builder] -> Seq Builder)
-> (SMT -> [Builder]) -> SMT -> Seq Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SMTOption -> Builder) -> [SMTOption] -> [Builder]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SMTOption -> Builder
forall a. Render a => a -> Builder
render ([SMTOption] -> [Builder])
-> (SMT -> [SMTOption]) -> SMT -> [Builder]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting [SMTOption] SMT [SMTOption] -> SMT -> [SMTOption]
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting [SMTOption] SMT [SMTOption]
Lens' SMT [SMTOption]
options
  renderLogic :: SMT -> Builder
renderLogic = Builder -> (String -> Builder) -> Maybe String -> Builder
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Builder
forall a. Monoid a => a
mempty (Builder -> Builder
renderSetLogic (Builder -> Builder) -> (String -> Builder) -> String -> Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Builder
stringUtf8) (Maybe String -> Builder)
-> (SMT -> Maybe String) -> SMT -> Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting (Maybe String) SMT (Maybe String) -> SMT -> Maybe String
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting (Maybe String) SMT (Maybe String)
Lens' SMT (Maybe String)
mlogic
  renderDeclareVars :: SMT -> Seq Builder
renderDeclareVars = (SomeKnownSMTSort SMTVar -> Builder)
-> Seq (SomeKnownSMTSort SMTVar) -> Seq Builder
forall a b. (a -> b) -> Seq a -> Seq b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Some1 f a
v) -> SMTVar a -> Builder
forall (t :: SMTSort). KnownSMTSort t => SMTVar t -> Builder
renderDeclareVar f a
SMTVar a
v) (Seq (SomeKnownSMTSort SMTVar) -> Seq Builder)
-> (SMT -> Seq (SomeKnownSMTSort SMTVar)) -> SMT -> Seq Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting
  (Seq (SomeKnownSMTSort SMTVar)) SMT (Seq (SomeKnownSMTSort SMTVar))
-> SMT -> Seq (SomeKnownSMTSort SMTVar)
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting
  (Seq (SomeKnownSMTSort SMTVar)) SMT (Seq (SomeKnownSMTSort SMTVar))
Lens' SMT (Seq (SomeKnownSMTSort SMTVar))
vars
  renderAssertions :: SMT -> Seq Builder
renderAssertions = (Expr 'BoolSort -> Builder) -> Seq (Expr 'BoolSort) -> Seq Builder
forall a b. (a -> b) -> Seq a -> Seq b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr 'BoolSort -> Builder
renderAssert (Seq (Expr 'BoolSort) -> Seq Builder)
-> (SMT -> Seq (Expr 'BoolSort)) -> SMT -> Seq Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting (Seq (Expr 'BoolSort)) SMT (Seq (Expr 'BoolSort))
-> SMT -> Seq (Expr 'BoolSort)
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting (Seq (Expr 'BoolSort)) SMT (Seq (Expr 'BoolSort))
Lens' SMT (Seq (Expr 'BoolSort))
formulas
  renderSoftAssertions :: SMT -> Seq Builder
renderSoftAssertions SMT
_ = Seq Builder
forall a. Monoid a => a
mempty
  renderMinimizations :: SMT -> Seq Builder
renderMinimizations SMT
_ = Seq Builder
forall a. Monoid a => a
mempty
  renderMaximizations :: SMT -> Seq Builder
renderMaximizations SMT
_ = Seq Builder
forall a. Monoid a => a
mempty

instance RenderProblem OMT where
  renderOptions :: OMT -> Seq Builder
renderOptions = SMT -> Seq Builder
forall s. RenderProblem s => s -> Seq Builder
renderOptions (SMT -> Seq Builder) -> (OMT -> SMT) -> OMT -> Seq Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting SMT OMT SMT -> OMT -> SMT
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting SMT OMT SMT
Lens' OMT SMT
smt
  renderLogic :: OMT -> Builder
renderLogic = SMT -> Builder
forall s. RenderProblem s => s -> Builder
renderLogic (SMT -> Builder) -> (OMT -> SMT) -> OMT -> Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting SMT OMT SMT -> OMT -> SMT
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting SMT OMT SMT
Lens' OMT SMT
smt
  renderDeclareVars :: OMT -> Seq Builder
renderDeclareVars = SMT -> Seq Builder
forall s. RenderProblem s => s -> Seq Builder
renderDeclareVars (SMT -> Seq Builder) -> (OMT -> SMT) -> OMT -> Seq Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting SMT OMT SMT -> OMT -> SMT
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting SMT OMT SMT
Lens' OMT SMT
smt
  renderAssertions :: OMT -> Seq Builder
renderAssertions = SMT -> Seq Builder
forall s. RenderProblem s => s -> Seq Builder
renderAssertions (SMT -> Seq Builder) -> (OMT -> SMT) -> OMT -> Seq Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting SMT OMT SMT -> OMT -> SMT
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting SMT OMT SMT
Lens' OMT SMT
smt
  renderSoftAssertions :: OMT -> Seq Builder
renderSoftAssertions = (SoftFormula -> Builder) -> Seq SoftFormula -> Seq Builder
forall a b. (a -> b) -> Seq a -> Seq b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SoftFormula -> Builder
forall a. Render a => a -> Builder
render (Seq SoftFormula -> Seq Builder)
-> (OMT -> Seq SoftFormula) -> OMT -> Seq Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting (Seq SoftFormula) OMT (Seq SoftFormula)
-> OMT -> Seq SoftFormula
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting (Seq SoftFormula) OMT (Seq SoftFormula)
Lens' OMT (Seq SoftFormula)
softFormulas
  renderMinimizations :: OMT -> Seq Builder
renderMinimizations = (SomeKnownSMTSort Minimize -> Builder)
-> Seq (SomeKnownSMTSort Minimize) -> Seq Builder
forall a b. (a -> b) -> Seq a -> Seq b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\case Some1 f a
minExpr -> f a -> Builder
forall a. Render a => a -> Builder
render f a
minExpr) (Seq (SomeKnownSMTSort Minimize) -> Seq Builder)
-> (OMT -> Seq (SomeKnownSMTSort Minimize)) -> OMT -> Seq Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting
  (Seq (SomeKnownSMTSort Minimize))
  OMT
  (Seq (SomeKnownSMTSort Minimize))
-> OMT -> Seq (SomeKnownSMTSort Minimize)
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting
  (Seq (SomeKnownSMTSort Minimize))
  OMT
  (Seq (SomeKnownSMTSort Minimize))
Lens' OMT (Seq (SomeKnownSMTSort Minimize))
targetMinimize
  renderMaximizations :: OMT -> Seq Builder
renderMaximizations = (SomeKnownSMTSort Maximize -> Builder)
-> Seq (SomeKnownSMTSort Maximize) -> Seq Builder
forall a b. (a -> b) -> Seq a -> Seq b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\case Some1 f a
maxExpr -> f a -> Builder
forall a. Render a => a -> Builder
render f a
maxExpr) (Seq (SomeKnownSMTSort Maximize) -> Seq Builder)
-> (OMT -> Seq (SomeKnownSMTSort Maximize)) -> OMT -> Seq Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting
  (Seq (SomeKnownSMTSort Maximize))
  OMT
  (Seq (SomeKnownSMTSort Maximize))
-> OMT -> Seq (SomeKnownSMTSort Maximize)
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting
  (Seq (SomeKnownSMTSort Maximize))
  OMT
  (Seq (SomeKnownSMTSort Maximize))
Lens' OMT (Seq (SomeKnownSMTSort Maximize))
targetMaximize