{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# HLINT ignore "Eta reduce" #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

-- |
-- Module      :   Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim
-- Copyright   :   (c) Sirui Lu 2024
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim
  ( bvIsNonZeroFromGEq1,
  )
where

import Data.Proxy (Proxy (Proxy))
import Data.SBV (BVIsNonZero, FiniteBits (finiteBitSize))
import qualified Data.SBV as SBV
import qualified Data.SBV.Dynamic as SBVD
import Data.Type.Bool (If)
import Data.Type.Equality ((:~:) (Refl))
import GHC.TypeNats (KnownNat, natVal, type (<=))
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.FP
  ( FP (FP),
    FPRoundingMode (RNA, RNE, RTN, RTP, RTZ),
    ValidFP,
  )
import Grisette.Internal.SymPrim.Prim.Internal.IsZero
  ( IsZero,
    IsZeroCases (IsZeroEvidence, NonZeroEvidence),
    KnownIsZero (isZero),
  )
import Grisette.Internal.SymPrim.Prim.Internal.Term
  ( NonFuncSBVRep (NonFuncSBVBaseType),
    SBVRep
      ( SBVType
      ),
    SupportedNonFuncPrim (conNonFuncSBVTerm, symNonFuncSBVTerm, withNonFuncPrim),
    SupportedPrim
      ( conSBVTerm,
        defaultValue,
        defaultValueDynamic,
        parseSMTModelResult,
        pevalEqTerm,
        pevalITETerm,
        pformatCon,
        sbvIte,
        symSBVName,
        symSBVTerm,
        withPrim
      ),
    SupportedPrimConstraint
      ( PrimConstraint
      ),
    Term (ConTerm),
    conTerm,
    eqTerm,
    parseSMTModelResultError,
    pevalDefaultEqTerm,
    pevalITEBasicTerm,
    sbvFresh,
  )
import Grisette.Internal.SymPrim.Prim.ModelValue (ModelValue, toModelValue)
import Grisette.Internal.Utils.Parameterized (unsafeAxiom)
import Type.Reflection (typeRep)
import Unsafe.Coerce (unsafeCoerce)

defaultValueForInteger :: Integer
defaultValueForInteger :: Integer
defaultValueForInteger = Integer
0

defaultValueForIntegerDyn :: ModelValue
defaultValueForIntegerDyn :: ModelValue
defaultValueForIntegerDyn = Integer -> ModelValue
forall a. (Show a, Eq a, Hashable a, Typeable a) => a -> ModelValue
toModelValue Integer
defaultValueForInteger

-- Basic Integer
instance SBVRep Integer where
  type SBVType n Integer = SBV.SBV (If (IsZero n) (Integer) (SBV.IntN n))

instance SupportedPrimConstraint Integer

instance SupportedPrim Integer where
  pformatCon :: Integer -> String
pformatCon = Integer -> String
forall a. Show a => a -> String
show
  defaultValue :: Integer
defaultValue = Integer
defaultValueForInteger
  defaultValueDynamic :: forall (proxy :: * -> *). proxy Integer -> ModelValue
defaultValueDynamic proxy Integer
_ = ModelValue
defaultValueForIntegerDyn
  pevalITETerm :: Term Bool -> Term Integer -> Term Integer -> Term Integer
pevalITETerm = Term Bool -> Term Integer -> Term Integer -> Term Integer
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITEBasicTerm
  pevalEqTerm :: Term Integer -> Term Integer -> Term Bool
pevalEqTerm = Term Integer -> Term Integer -> Term Bool
forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalDefaultEqTerm
  conSBVTerm :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n -> Integer -> SBVType n Integer
conSBVTerm proxy n
p Integer
n = case proxy n -> IsZeroCases n
forall (a :: Nat) (proxy :: Nat -> *).
KnownIsZero a =>
proxy a -> IsZeroCases a
forall (proxy :: Nat -> *). proxy n -> IsZeroCases n
isZero proxy n
p of
    IsZeroCases n
IsZeroEvidence -> Integer -> SBV Integer
forall a. Num a => Integer -> a
fromInteger Integer
n
    IsZeroCases n
NonZeroEvidence -> Integer -> SBV (IntN n)
forall a. Num a => Integer -> a
fromInteger Integer
n
  symSBVName :: TypedSymbol Integer -> Int -> String
symSBVName TypedSymbol Integer
symbol Int
_ = TypedSymbol Integer -> String
forall a. Show a => a -> String
show TypedSymbol Integer
symbol
  symSBVTerm :: forall (m :: * -> *) (n :: Nat) (proxy :: Nat -> *).
(SBVFreshMonad m, KnownIsZero n) =>
proxy n -> String -> m (SBVType n Integer)
symSBVTerm proxy n
p String
name = case proxy n -> IsZeroCases n
forall (a :: Nat) (proxy :: Nat -> *).
KnownIsZero a =>
proxy a -> IsZeroCases a
forall (proxy :: Nat -> *). proxy n -> IsZeroCases n
isZero proxy n
p of
    IsZeroCases n
IsZeroEvidence -> String -> m (SBV Integer)
forall a. SymVal a => String -> m (SBV a)
forall (m :: * -> *) a.
(SBVFreshMonad m, SymVal a) =>
String -> m (SBV a)
sbvFresh String
name
    IsZeroCases n
NonZeroEvidence -> String -> m (SBV (IntN n))
forall a. SymVal a => String -> m (SBV a)
forall (m :: * -> *) a.
(SBVFreshMonad m, SymVal a) =>
String -> m (SBV a)
sbvFresh String
name
  withPrim :: forall (n :: Nat) (p :: Nat -> *) a.
KnownIsZero n =>
p n
-> ((PrimConstraint n Integer, SMTDefinable (SBVType n Integer),
     Mergeable (SBVType n Integer), Typeable (SBVType n Integer)) =>
    a)
-> a
withPrim p n
p (PrimConstraint n Integer, SMTDefinable (SBVType n Integer),
 Mergeable (SBVType n Integer), Typeable (SBVType n Integer)) =>
a
r = case p n -> IsZeroCases n
forall (a :: Nat) (proxy :: Nat -> *).
KnownIsZero a =>
proxy a -> IsZeroCases a
forall (proxy :: Nat -> *). proxy n -> IsZeroCases n
isZero p n
p of
    IsZeroCases n
IsZeroEvidence -> a
(PrimConstraint n Integer, SMTDefinable (SBVType n Integer),
 Mergeable (SBVType n Integer), Typeable (SBVType n Integer)) =>
a
r
    IsZeroCases n
NonZeroEvidence -> a
(PrimConstraint n Integer, SMTDefinable (SBVType n Integer),
 Mergeable (SBVType n Integer), Typeable (SBVType n Integer)) =>
a
r
  parseSMTModelResult :: Int -> ([([SBVD.CV], SBVD.CV)], SBVD.CV) -> Integer
  parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> Integer
parseSMTModelResult Int
_ ([], SBVD.CV Kind
SBVD.KUnbounded (SBVD.CInteger Integer
i)) = Integer
i
  parseSMTModelResult Int
_ ([([], SBVD.CV Kind
SBVD.KUnbounded (SBVD.CInteger Integer
i))], CV
_) = Integer
i
  parseSMTModelResult Int
_ ([([CV], CV)], CV)
cv = TypeRep Integer -> ([([CV], CV)], CV) -> Integer
forall a. HasCallStack => TypeRep a -> ([([CV], CV)], CV) -> a
parseSMTModelResultError (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @Integer) ([([CV], CV)], CV)
cv

instance NonFuncSBVRep Integer where
  type NonFuncSBVBaseType n Integer = If (IsZero n) Integer (SBV.IntN n)

instance SupportedNonFuncPrim Integer where
  conNonFuncSBVTerm :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n -> Integer -> SBV (NonFuncSBVBaseType n Integer)
conNonFuncSBVTerm = proxy n -> Integer -> SBV (NonFuncSBVBaseType n Integer)
proxy n -> Integer -> SBVType n Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n -> Integer -> SBVType n Integer
forall t (n :: Nat) (proxy :: Nat -> *).
(SupportedPrim t, KnownIsZero n) =>
proxy n -> t -> SBVType n t
conSBVTerm
  symNonFuncSBVTerm :: forall (m :: * -> *) (n :: Nat) (proxy :: Nat -> *).
(SBVFreshMonad m, KnownIsZero n) =>
proxy n -> String -> m (SBV (NonFuncSBVBaseType n Integer))
symNonFuncSBVTerm = forall t (m :: * -> *) (n :: Nat) (proxy :: Nat -> *).
(SupportedPrim t, SBVFreshMonad m, KnownIsZero n) =>
proxy n -> String -> m (SBVType n t)
symSBVTerm @Integer
  withNonFuncPrim :: forall (n :: Nat) (proxy :: Nat -> *) r.
KnownIsZero n =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n Integer),
     EqSymbolic (SBVType n Integer), Mergeable (SBVType n Integer),
     SMTDefinable (SBVType n Integer), Mergeable (SBVType n Integer),
     SBVType n Integer ~ SBV (NonFuncSBVBaseType n Integer),
     PrimConstraint n Integer) =>
    r)
-> r
withNonFuncPrim proxy n
p (SymVal (NonFuncSBVBaseType n Integer),
 EqSymbolic (SBVType n Integer), Mergeable (SBVType n Integer),
 SMTDefinable (SBVType n Integer), Mergeable (SBVType n Integer),
 SBVType n Integer ~ SBV (NonFuncSBVBaseType n Integer),
 PrimConstraint n Integer) =>
r
r = case proxy n -> IsZeroCases n
forall (a :: Nat) (proxy :: Nat -> *).
KnownIsZero a =>
proxy a -> IsZeroCases a
forall (proxy :: Nat -> *). proxy n -> IsZeroCases n
isZero proxy n
p of
    IsZeroCases n
IsZeroEvidence -> r
(SymVal (NonFuncSBVBaseType n Integer),
 EqSymbolic (SBVType n Integer), Mergeable (SBVType n Integer),
 SMTDefinable (SBVType n Integer), Mergeable (SBVType n Integer),
 SBVType n Integer ~ SBV (NonFuncSBVBaseType n Integer),
 PrimConstraint n Integer) =>
r
r
    IsZeroCases n
NonZeroEvidence -> proxy n -> (BVIsNonZero n => r) -> r
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 proxy n
p r
BVIsNonZero n => r
(SymVal (NonFuncSBVBaseType n Integer),
 EqSymbolic (SBVType n Integer), Mergeable (SBVType n Integer),
 SMTDefinable (SBVType n Integer), Mergeable (SBVType n Integer),
 SBVType n Integer ~ SBV (NonFuncSBVBaseType n Integer),
 PrimConstraint n Integer) =>
r
r

-- Signed BV
instance (KnownNat w, 1 <= w) => SupportedPrimConstraint (IntN w) where
  type PrimConstraint _ (IntN w) = (KnownNat w, 1 <= w, BVIsNonZero w)

instance (KnownNat w, 1 <= w) => SBVRep (IntN w) where
  type SBVType _ (IntN w) = SBV.SBV (SBV.IntN w)

instance (KnownNat w, 1 <= w) => SupportedPrim (IntN w) where
  pformatCon :: IntN w -> String
pformatCon = IntN w -> String
forall a. Show a => a -> String
show
  defaultValue :: IntN w
defaultValue = IntN w
0
  pevalITETerm :: Term Bool -> Term (IntN w) -> Term (IntN w) -> Term (IntN w)
pevalITETerm = Term Bool -> Term (IntN w) -> Term (IntN w) -> Term (IntN w)
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITEBasicTerm
  pevalEqTerm :: Term (IntN w) -> Term (IntN w) -> Term Bool
pevalEqTerm = Term (IntN w) -> Term (IntN w) -> Term Bool
forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalDefaultEqTerm
  conSBVTerm :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n -> IntN w -> SBVType n (IntN w)
conSBVTerm proxy n
_ IntN w
n = Proxy w
-> (BVIsNonZero w => SBVType n (IntN w)) -> SBVType n (IntN w)
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @w) ((BVIsNonZero w => SBVType n (IntN w)) -> SBVType n (IntN w))
-> (BVIsNonZero w => SBVType n (IntN w)) -> SBVType n (IntN w)
forall a b. (a -> b) -> a -> b
$ IntN w -> SBV (IntN w)
forall a b. (Integral a, Num b) => a -> b
fromIntegral IntN w
n
  symSBVName :: TypedSymbol (IntN w) -> Int -> String
symSBVName TypedSymbol (IntN w)
symbol Int
_ = TypedSymbol (IntN w) -> String
forall a. Show a => a -> String
show TypedSymbol (IntN w)
symbol
  symSBVTerm :: forall (m :: * -> *) (n :: Nat) (proxy :: Nat -> *).
(SBVFreshMonad m, KnownIsZero n) =>
proxy n -> String -> m (SBVType n (IntN w))
symSBVTerm proxy n
_ String
name = Proxy w
-> (BVIsNonZero w => m (SBVType n (IntN w)))
-> m (SBVType n (IntN w))
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @w) ((BVIsNonZero w => m (SBVType n (IntN w)))
 -> m (SBVType n (IntN w)))
-> (BVIsNonZero w => m (SBVType n (IntN w)))
-> m (SBVType n (IntN w))
forall a b. (a -> b) -> a -> b
$ String -> m (SBV (IntN w))
forall a. SymVal a => String -> m (SBV a)
forall (m :: * -> *) a.
(SBVFreshMonad m, SymVal a) =>
String -> m (SBV a)
sbvFresh String
name
  withPrim :: forall (n :: Nat) (p :: Nat -> *) a.
KnownIsZero n =>
p n
-> ((PrimConstraint n (IntN w), SMTDefinable (SBVType n (IntN w)),
     Mergeable (SBVType n (IntN w)), Typeable (SBVType n (IntN w))) =>
    a)
-> a
withPrim p n
_ (PrimConstraint n (IntN w), SMTDefinable (SBVType n (IntN w)),
 Mergeable (SBVType n (IntN w)), Typeable (SBVType n (IntN w))) =>
a
r = Proxy w -> (BVIsNonZero w => a) -> a
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @w) a
BVIsNonZero w => a
(PrimConstraint n (IntN w), SMTDefinable (SBVType n (IntN w)),
 Mergeable (SBVType n (IntN w)), Typeable (SBVType n (IntN w))) =>
a
r
  parseSMTModelResult :: Int -> ([([SBVD.CV], SBVD.CV)], SBVD.CV) -> IntN w
  parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> IntN w
parseSMTModelResult
    Int
_
    ([], SBVD.CV (SBVD.KBounded Bool
_ Int
bitWidth) (SBVD.CInteger Integer
i))
      | Int
bitWidth Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== IntN w -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize (IntN w
forall a. HasCallStack => a
undefined :: IntN w) = Integer -> IntN w
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
i
  parseSMTModelResult
    Int
_
    ([([], SBVD.CV (SBVD.KBounded Bool
_ Int
bitWidth) (SBVD.CInteger Integer
i))], CV
_)
      | Int
bitWidth Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== IntN w -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize (IntN w
forall a. HasCallStack => a
undefined :: IntN w) = Integer -> IntN w
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
i
  parseSMTModelResult Int
_ ([([CV], CV)], CV)
cv = TypeRep (IntN w) -> ([([CV], CV)], CV) -> IntN w
forall a. HasCallStack => TypeRep a -> ([([CV], CV)], CV) -> a
parseSMTModelResultError (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(IntN w)) ([([CV], CV)], CV)
cv

bvIsNonZeroFromGEq1 ::
  forall w r proxy.
  (1 <= w) =>
  proxy w ->
  ((SBV.BVIsNonZero w) => r) ->
  r
bvIsNonZeroFromGEq1 :: forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 proxy w
_ BVIsNonZero w => r
r1 = case w :~: 1
forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom :: w :~: 1 of
  w :~: 1
Refl -> r
BVIsNonZero w => r
r1

instance (KnownNat w, 1 <= w) => NonFuncSBVRep (IntN w) where
  type NonFuncSBVBaseType _ (IntN w) = SBV.IntN w

instance (KnownNat w, 1 <= w) => SupportedNonFuncPrim (IntN w) where
  conNonFuncSBVTerm :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n -> IntN w -> SBV (NonFuncSBVBaseType n (IntN w))
conNonFuncSBVTerm = proxy n -> IntN w -> SBV (NonFuncSBVBaseType n (IntN w))
proxy n -> IntN w -> SBVType n (IntN w)
forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n -> IntN w -> SBVType n (IntN w)
forall t (n :: Nat) (proxy :: Nat -> *).
(SupportedPrim t, KnownIsZero n) =>
proxy n -> t -> SBVType n t
conSBVTerm
  symNonFuncSBVTerm :: forall (m :: * -> *) (n :: Nat) (proxy :: Nat -> *).
(SBVFreshMonad m, KnownIsZero n) =>
proxy n -> String -> m (SBV (NonFuncSBVBaseType n (IntN w)))
symNonFuncSBVTerm = forall t (m :: * -> *) (n :: Nat) (proxy :: Nat -> *).
(SupportedPrim t, SBVFreshMonad m, KnownIsZero n) =>
proxy n -> String -> m (SBVType n t)
symSBVTerm @(IntN w)
  withNonFuncPrim :: forall (n :: Nat) (proxy :: Nat -> *) r.
KnownIsZero n =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n (IntN w)),
     EqSymbolic (SBVType n (IntN w)), Mergeable (SBVType n (IntN w)),
     SMTDefinable (SBVType n (IntN w)), Mergeable (SBVType n (IntN w)),
     SBVType n (IntN w) ~ SBV (NonFuncSBVBaseType n (IntN w)),
     PrimConstraint n (IntN w)) =>
    r)
-> r
withNonFuncPrim proxy n
_ (SymVal (NonFuncSBVBaseType n (IntN w)),
 EqSymbolic (SBVType n (IntN w)), Mergeable (SBVType n (IntN w)),
 SMTDefinable (SBVType n (IntN w)), Mergeable (SBVType n (IntN w)),
 SBVType n (IntN w) ~ SBV (NonFuncSBVBaseType n (IntN w)),
 PrimConstraint n (IntN w)) =>
r
r = Proxy w -> (BVIsNonZero w => r) -> r
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @w) r
BVIsNonZero w => r
(SymVal (NonFuncSBVBaseType n (IntN w)),
 EqSymbolic (SBVType n (IntN w)), Mergeable (SBVType n (IntN w)),
 SMTDefinable (SBVType n (IntN w)), Mergeable (SBVType n (IntN w)),
 SBVType n (IntN w) ~ SBV (NonFuncSBVBaseType n (IntN w)),
 PrimConstraint n (IntN w)) =>
r
r

-- Unsigned BV
instance (KnownNat w, 1 <= w) => SupportedPrimConstraint (WordN w) where
  type PrimConstraint _ (WordN w) = (KnownNat w, 1 <= w, BVIsNonZero w)

instance (KnownNat w, 1 <= w) => SBVRep (WordN w) where
  type SBVType _ (WordN w) = SBV.SBV (SBV.WordN w)

instance (KnownNat w, 1 <= w) => SupportedPrim (WordN w) where
  pformatCon :: WordN w -> String
pformatCon = WordN w -> String
forall a. Show a => a -> String
show
  defaultValue :: WordN w
defaultValue = WordN w
0
  pevalITETerm :: Term Bool -> Term (WordN w) -> Term (WordN w) -> Term (WordN w)
pevalITETerm = Term Bool -> Term (WordN w) -> Term (WordN w) -> Term (WordN w)
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITEBasicTerm
  pevalEqTerm :: Term (WordN w) -> Term (WordN w) -> Term Bool
pevalEqTerm = Term (WordN w) -> Term (WordN w) -> Term Bool
forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalDefaultEqTerm
  conSBVTerm :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n -> WordN w -> SBVType n (WordN w)
conSBVTerm proxy n
_ WordN w
n = Proxy w
-> (BVIsNonZero w => SBVType n (WordN w)) -> SBVType n (WordN w)
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @w) ((BVIsNonZero w => SBVType n (WordN w)) -> SBVType n (WordN w))
-> (BVIsNonZero w => SBVType n (WordN w)) -> SBVType n (WordN w)
forall a b. (a -> b) -> a -> b
$ WordN w -> SBV (WordN w)
forall a b. (Integral a, Num b) => a -> b
fromIntegral WordN w
n
  symSBVName :: TypedSymbol (WordN w) -> Int -> String
symSBVName TypedSymbol (WordN w)
symbol Int
_ = TypedSymbol (WordN w) -> String
forall a. Show a => a -> String
show TypedSymbol (WordN w)
symbol
  symSBVTerm :: forall (m :: * -> *) (n :: Nat) (proxy :: Nat -> *).
(SBVFreshMonad m, KnownIsZero n) =>
proxy n -> String -> m (SBVType n (WordN w))
symSBVTerm proxy n
_ String
name = Proxy w
-> (BVIsNonZero w => m (SBVType n (WordN w)))
-> m (SBVType n (WordN w))
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @w) ((BVIsNonZero w => m (SBVType n (WordN w)))
 -> m (SBVType n (WordN w)))
-> (BVIsNonZero w => m (SBVType n (WordN w)))
-> m (SBVType n (WordN w))
forall a b. (a -> b) -> a -> b
$ String -> m (SBV (WordN w))
forall a. SymVal a => String -> m (SBV a)
forall (m :: * -> *) a.
(SBVFreshMonad m, SymVal a) =>
String -> m (SBV a)
sbvFresh String
name
  withPrim :: forall (n :: Nat) (p :: Nat -> *) a.
KnownIsZero n =>
p n
-> ((PrimConstraint n (WordN w),
     SMTDefinable (SBVType n (WordN w)),
     Mergeable (SBVType n (WordN w)), Typeable (SBVType n (WordN w))) =>
    a)
-> a
withPrim p n
_ (PrimConstraint n (WordN w), SMTDefinable (SBVType n (WordN w)),
 Mergeable (SBVType n (WordN w)), Typeable (SBVType n (WordN w))) =>
a
r = Proxy w -> (BVIsNonZero w => a) -> a
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @w) a
BVIsNonZero w => a
(PrimConstraint n (WordN w), SMTDefinable (SBVType n (WordN w)),
 Mergeable (SBVType n (WordN w)), Typeable (SBVType n (WordN w))) =>
a
r
  parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> WordN w
parseSMTModelResult
    Int
_
    ([], SBVD.CV (SBVD.KBounded Bool
_ Int
bitWidth) (SBVD.CInteger Integer
i))
      | Int
bitWidth Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== WordN w -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize (WordN w
forall a. HasCallStack => a
undefined :: WordN w) = Integer -> WordN w
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
i
  parseSMTModelResult
    Int
_
    ([([], SBVD.CV (SBVD.KBounded Bool
_ Int
bitWidth) (SBVD.CInteger Integer
i))], CV
_)
      | Int
bitWidth Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== WordN w -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize (WordN w
forall a. HasCallStack => a
undefined :: WordN w) = Integer -> WordN w
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
i
  parseSMTModelResult Int
_ ([([CV], CV)], CV)
cv = TypeRep (WordN w) -> ([([CV], CV)], CV) -> WordN w
forall a. HasCallStack => TypeRep a -> ([([CV], CV)], CV) -> a
parseSMTModelResultError (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(WordN w)) ([([CV], CV)], CV)
cv

instance (KnownNat w, 1 <= w) => NonFuncSBVRep (WordN w) where
  type NonFuncSBVBaseType _ (WordN w) = SBV.WordN w

instance (KnownNat w, 1 <= w) => SupportedNonFuncPrim (WordN w) where
  conNonFuncSBVTerm :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n -> WordN w -> SBV (NonFuncSBVBaseType n (WordN w))
conNonFuncSBVTerm = proxy n -> WordN w -> SBV (NonFuncSBVBaseType n (WordN w))
proxy n -> WordN w -> SBVType n (WordN w)
forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n -> WordN w -> SBVType n (WordN w)
forall t (n :: Nat) (proxy :: Nat -> *).
(SupportedPrim t, KnownIsZero n) =>
proxy n -> t -> SBVType n t
conSBVTerm
  symNonFuncSBVTerm :: forall (m :: * -> *) (n :: Nat) (proxy :: Nat -> *).
(SBVFreshMonad m, KnownIsZero n) =>
proxy n -> String -> m (SBV (NonFuncSBVBaseType n (WordN w)))
symNonFuncSBVTerm = forall t (m :: * -> *) (n :: Nat) (proxy :: Nat -> *).
(SupportedPrim t, SBVFreshMonad m, KnownIsZero n) =>
proxy n -> String -> m (SBVType n t)
symSBVTerm @(WordN w)
  withNonFuncPrim :: forall (n :: Nat) (proxy :: Nat -> *) r.
KnownIsZero n =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n (WordN w)),
     EqSymbolic (SBVType n (WordN w)), Mergeable (SBVType n (WordN w)),
     SMTDefinable (SBVType n (WordN w)),
     Mergeable (SBVType n (WordN w)),
     SBVType n (WordN w) ~ SBV (NonFuncSBVBaseType n (WordN w)),
     PrimConstraint n (WordN w)) =>
    r)
-> r
withNonFuncPrim proxy n
_ (SymVal (NonFuncSBVBaseType n (WordN w)),
 EqSymbolic (SBVType n (WordN w)), Mergeable (SBVType n (WordN w)),
 SMTDefinable (SBVType n (WordN w)),
 Mergeable (SBVType n (WordN w)),
 SBVType n (WordN w) ~ SBV (NonFuncSBVBaseType n (WordN w)),
 PrimConstraint n (WordN w)) =>
r
r = Proxy w -> (BVIsNonZero w => r) -> r
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @w) r
BVIsNonZero w => r
(SymVal (NonFuncSBVBaseType n (WordN w)),
 EqSymbolic (SBVType n (WordN w)), Mergeable (SBVType n (WordN w)),
 SMTDefinable (SBVType n (WordN w)),
 Mergeable (SBVType n (WordN w)),
 SBVType n (WordN w) ~ SBV (NonFuncSBVBaseType n (WordN w)),
 PrimConstraint n (WordN w)) =>
r
r

-- FP
instance (ValidFP eb sb) => SupportedPrimConstraint (FP eb sb) where
  type PrimConstraint _ (FP eb sb) = ValidFP eb sb

instance (ValidFP eb sb) => SBVRep (FP eb sb) where
  type SBVType _ (FP eb sb) = SBV.SBV (SBV.FloatingPoint eb sb)

instance (ValidFP eb sb) => SupportedPrim (FP eb sb) where
  defaultValue :: FP eb sb
defaultValue = FP eb sb
0
  pevalITETerm :: Term Bool -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)
pevalITETerm = Term Bool -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITEBasicTerm
  pevalEqTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term Bool
pevalEqTerm (ConTerm Int
_ FP eb sb
l) (ConTerm Int
_ FP eb sb
r) = Bool -> Term Bool
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (Bool -> Term Bool) -> Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ FP eb sb
l FP eb sb -> FP eb sb -> Bool
forall a. Eq a => a -> a -> Bool
== FP eb sb
r
  pevalEqTerm l :: Term (FP eb sb)
l@ConTerm {} Term (FP eb sb)
r = Term (FP eb sb) -> Term (FP eb sb) -> Term Bool
forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalEqTerm Term (FP eb sb)
r Term (FP eb sb)
l
  pevalEqTerm Term (FP eb sb)
l Term (FP eb sb)
r = Term (FP eb sb) -> Term (FP eb sb) -> Term Bool
forall a. SupportedPrim a => Term a -> Term a -> Term Bool
eqTerm Term (FP eb sb)
l Term (FP eb sb)
r
  conSBVTerm :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n -> FP eb sb -> SBVType n (FP eb sb)
conSBVTerm proxy n
_ (FP FloatingPoint eb sb
fp) = FloatingPoint eb sb -> SBV (FloatingPoint eb sb)
forall a. SymVal a => a -> SBV a
SBV.literal FloatingPoint eb sb
fp
  symSBVName :: TypedSymbol (FP eb sb) -> Int -> String
symSBVName TypedSymbol (FP eb sb)
symbol Int
_ = TypedSymbol (FP eb sb) -> String
forall a. Show a => a -> String
show TypedSymbol (FP eb sb)
symbol
  symSBVTerm :: forall (m :: * -> *) (n :: Nat) (proxy :: Nat -> *).
(SBVFreshMonad m, KnownIsZero n) =>
proxy n -> String -> m (SBVType n (FP eb sb))
symSBVTerm proxy n
_ String
name = String -> m (SBV (FloatingPoint eb sb))
forall a. SymVal a => String -> m (SBV a)
forall (m :: * -> *) a.
(SBVFreshMonad m, SymVal a) =>
String -> m (SBV a)
sbvFresh String
name
  withPrim :: forall (n :: Nat) (p :: Nat -> *) a.
KnownIsZero n =>
p n
-> ((PrimConstraint n (FP eb sb),
     SMTDefinable (SBVType n (FP eb sb)),
     Mergeable (SBVType n (FP eb sb)),
     Typeable (SBVType n (FP eb sb))) =>
    a)
-> a
withPrim p n
_ (PrimConstraint n (FP eb sb), SMTDefinable (SBVType n (FP eb sb)),
 Mergeable (SBVType n (FP eb sb)),
 Typeable (SBVType n (FP eb sb))) =>
a
r = a
(PrimConstraint n (FP eb sb), SMTDefinable (SBVType n (FP eb sb)),
 Mergeable (SBVType n (FP eb sb)),
 Typeable (SBVType n (FP eb sb))) =>
a
r
  parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> FP eb sb
parseSMTModelResult
    Int
_
    ([], SBVD.CV (SBVD.KFP Int
eb Int
sb) (SBVD.CFP FP
fp))
      | Int
eb Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy eb -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @eb))
          Bool -> Bool -> Bool
&& Int
sb Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy sb -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @sb)) =
          -- Assumes that in SBV, FloatingPoint is a newtype of FP as the
          -- constructor isn't exposed
          Integer -> FP eb sb
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> FP eb sb) -> Integer -> FP eb sb
forall a b. (a -> b) -> a -> b
$ FP -> Integer
forall a b. a -> b
unsafeCoerce FP
fp
  parseSMTModelResult
    Int
_
    ([([], SBVD.CV (SBVD.KFP Int
eb Int
sb) (SBVD.CFP FP
fp))], CV
_)
      | Int
eb Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy eb -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @eb))
          Bool -> Bool -> Bool
&& Int
sb Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy sb -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @sb)) =
          -- Assumes that in SBV, FloatingPoint is a newtype of FP as the
          -- constructor isn't exposed
          Integer -> FP eb sb
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> FP eb sb) -> Integer -> FP eb sb
forall a b. (a -> b) -> a -> b
$ FP -> Integer
forall a b. a -> b
unsafeCoerce FP
fp
  parseSMTModelResult Int
_ ([([CV], CV)], CV)
cv = TypeRep (FP eb sb) -> ([([CV], CV)], CV) -> FP eb sb
forall a. HasCallStack => TypeRep a -> ([([CV], CV)], CV) -> a
parseSMTModelResultError (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(FP eb sb)) ([([CV], CV)], CV)
cv

  -- Workaround for sbv#702.
  sbvIte :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n
-> SBV Bool
-> SBVType n (FP eb sb)
-> SBVType n (FP eb sb)
-> SBVType n (FP eb sb)
sbvIte proxy n
p = forall t (n :: Nat) (p :: Nat -> *) a.
(SupportedPrim t, KnownIsZero n) =>
p n
-> ((PrimConstraint n t, SMTDefinable (SBVType n t),
     Mergeable (SBVType n t), Typeable (SBVType n t)) =>
    a)
-> a
withPrim @(FP eb sb) proxy n
p (((PrimConstraint n (FP eb sb),
   SMTDefinable (SBVType n (FP eb sb)),
   Mergeable (SBVType n (FP eb sb)),
   Typeable (SBVType n (FP eb sb))) =>
  SBV Bool
  -> SBVType n (FP eb sb)
  -> SBVType n (FP eb sb)
  -> SBVType n (FP eb sb))
 -> SBV Bool
 -> SBVType n (FP eb sb)
 -> SBVType n (FP eb sb)
 -> SBVType n (FP eb sb))
-> ((PrimConstraint n (FP eb sb),
     SMTDefinable (SBVType n (FP eb sb)),
     Mergeable (SBVType n (FP eb sb)),
     Typeable (SBVType n (FP eb sb))) =>
    SBV Bool
    -> SBVType n (FP eb sb)
    -> SBVType n (FP eb sb)
    -> SBVType n (FP eb sb))
-> SBV Bool
-> SBVType n (FP eb sb)
-> SBVType n (FP eb sb)
-> SBVType n (FP eb sb)
forall a b. (a -> b) -> a -> b
$ \SBV Bool
c SBVType n (FP eb sb)
a SBVType n (FP eb sb)
b ->
    case (SBV (FloatingPoint eb sb) -> Maybe (FloatingPoint eb sb)
forall a. SymVal a => SBV a -> Maybe a
SBV.unliteral SBV (FloatingPoint eb sb)
SBVType n (FP eb sb)
a, SBV (FloatingPoint eb sb) -> Maybe (FloatingPoint eb sb)
forall a. SymVal a => SBV a -> Maybe a
SBV.unliteral SBV (FloatingPoint eb sb)
SBVType n (FP eb sb)
b) of
      (Just FloatingPoint eb sb
a', Just FloatingPoint eb sb
b')
        | FloatingPoint eb sb -> Bool
forall a. RealFloat a => a -> Bool
isInfinite FloatingPoint eb sb
a' Bool -> Bool -> Bool
&& FloatingPoint eb sb -> Bool
forall a. RealFloat a => a -> Bool
isInfinite FloatingPoint eb sb
b' ->
            let correspondingZero :: a -> a
correspondingZero a
x = if a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
0 then a
0 else -a
0
             in SBV (FloatingPoint eb sb)
1
                  SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb) -> SBV (FloatingPoint eb sb)
forall a. Fractional a => a -> a -> a
/ forall t (n :: Nat) (proxy :: Nat -> *).
(SupportedPrim t, KnownIsZero n) =>
proxy n -> SBV Bool -> SBVType n t -> SBVType n t -> SBVType n t
sbvIte @(FP eb sb)
                    proxy n
p
                    SBV Bool
c
                    (forall t (n :: Nat) (proxy :: Nat -> *).
(SupportedPrim t, KnownIsZero n) =>
proxy n -> t -> SBVType n t
conSBVTerm @(FP eb sb) proxy n
p (FP eb sb -> SBVType n (FP eb sb))
-> FP eb sb -> SBVType n (FP eb sb)
forall a b. (a -> b) -> a -> b
$ FloatingPoint eb sb -> FP eb sb
forall {a} {a}. (Ord a, Num a, Num a) => a -> a
correspondingZero FloatingPoint eb sb
a')
                    (forall t (n :: Nat) (proxy :: Nat -> *).
(SupportedPrim t, KnownIsZero n) =>
proxy n -> t -> SBVType n t
conSBVTerm @(FP eb sb) proxy n
p (FP eb sb -> SBVType n (FP eb sb))
-> FP eb sb -> SBVType n (FP eb sb)
forall a b. (a -> b) -> a -> b
$ FloatingPoint eb sb -> FP eb sb
forall {a} {a}. (Ord a, Num a, Num a) => a -> a
correspondingZero FloatingPoint eb sb
b')
      (Maybe (FloatingPoint eb sb), Maybe (FloatingPoint eb sb))
_ -> SBV Bool
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
-> SBV (FloatingPoint eb sb)
forall a. Mergeable a => SBV Bool -> a -> a -> a
SBV.ite SBV Bool
c SBV (FloatingPoint eb sb)
SBVType n (FP eb sb)
a SBV (FloatingPoint eb sb)
SBVType n (FP eb sb)
b

instance (ValidFP eb sb) => NonFuncSBVRep (FP eb sb) where
  type NonFuncSBVBaseType _ (FP eb sb) = SBV.FloatingPoint eb sb

instance (ValidFP eb sb) => SupportedNonFuncPrim (FP eb sb) where
  conNonFuncSBVTerm :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n -> FP eb sb -> SBV (NonFuncSBVBaseType n (FP eb sb))
conNonFuncSBVTerm = proxy n -> FP eb sb -> SBV (NonFuncSBVBaseType n (FP eb sb))
proxy n -> FP eb sb -> SBVType n (FP eb sb)
forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n -> FP eb sb -> SBVType n (FP eb sb)
forall t (n :: Nat) (proxy :: Nat -> *).
(SupportedPrim t, KnownIsZero n) =>
proxy n -> t -> SBVType n t
conSBVTerm
  symNonFuncSBVTerm :: forall (m :: * -> *) (n :: Nat) (proxy :: Nat -> *).
(SBVFreshMonad m, KnownIsZero n) =>
proxy n -> String -> m (SBV (NonFuncSBVBaseType n (FP eb sb)))
symNonFuncSBVTerm = forall t (m :: * -> *) (n :: Nat) (proxy :: Nat -> *).
(SupportedPrim t, SBVFreshMonad m, KnownIsZero n) =>
proxy n -> String -> m (SBVType n t)
symSBVTerm @(FP eb sb)
  withNonFuncPrim :: forall (n :: Nat) (proxy :: Nat -> *) r.
KnownIsZero n =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n (FP eb sb)),
     EqSymbolic (SBVType n (FP eb sb)),
     Mergeable (SBVType n (FP eb sb)),
     SMTDefinable (SBVType n (FP eb sb)),
     Mergeable (SBVType n (FP eb sb)),
     SBVType n (FP eb sb) ~ SBV (NonFuncSBVBaseType n (FP eb sb)),
     PrimConstraint n (FP eb sb)) =>
    r)
-> r
withNonFuncPrim proxy n
_ (SymVal (NonFuncSBVBaseType n (FP eb sb)),
 EqSymbolic (SBVType n (FP eb sb)),
 Mergeable (SBVType n (FP eb sb)),
 SMTDefinable (SBVType n (FP eb sb)),
 Mergeable (SBVType n (FP eb sb)),
 SBVType n (FP eb sb) ~ SBV (NonFuncSBVBaseType n (FP eb sb)),
 PrimConstraint n (FP eb sb)) =>
r
r = r
(SymVal (NonFuncSBVBaseType n (FP eb sb)),
 EqSymbolic (SBVType n (FP eb sb)),
 Mergeable (SBVType n (FP eb sb)),
 SMTDefinable (SBVType n (FP eb sb)),
 Mergeable (SBVType n (FP eb sb)),
 SBVType n (FP eb sb) ~ SBV (NonFuncSBVBaseType n (FP eb sb)),
 PrimConstraint n (FP eb sb)) =>
r
r

-- FPRoundingMode
instance SupportedPrimConstraint FPRoundingMode

instance SBVRep FPRoundingMode where
  type SBVType _ FPRoundingMode = SBV.SBV SBV.RoundingMode

instance SupportedPrim FPRoundingMode where
  defaultValue :: FPRoundingMode
defaultValue = FPRoundingMode
RNE
  pevalITETerm :: Term Bool
-> Term FPRoundingMode
-> Term FPRoundingMode
-> Term FPRoundingMode
pevalITETerm = Term Bool
-> Term FPRoundingMode
-> Term FPRoundingMode
-> Term FPRoundingMode
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITEBasicTerm
  pevalEqTerm :: Term FPRoundingMode -> Term FPRoundingMode -> Term Bool
pevalEqTerm (ConTerm Int
_ FPRoundingMode
l) (ConTerm Int
_ FPRoundingMode
r) = Bool -> Term Bool
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (Bool -> Term Bool) -> Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ FPRoundingMode
l FPRoundingMode -> FPRoundingMode -> Bool
forall a. Eq a => a -> a -> Bool
== FPRoundingMode
r
  pevalEqTerm l :: Term FPRoundingMode
l@ConTerm {} Term FPRoundingMode
r = Term FPRoundingMode -> Term FPRoundingMode -> Term Bool
forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalEqTerm Term FPRoundingMode
r Term FPRoundingMode
l
  pevalEqTerm Term FPRoundingMode
l Term FPRoundingMode
r = Term FPRoundingMode -> Term FPRoundingMode -> Term Bool
forall a. SupportedPrim a => Term a -> Term a -> Term Bool
eqTerm Term FPRoundingMode
l Term FPRoundingMode
r
  conSBVTerm :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n -> FPRoundingMode -> SBVType n FPRoundingMode
conSBVTerm proxy n
_ FPRoundingMode
RNE = SBV RoundingMode
SBVType n FPRoundingMode
SBV.sRNE
  conSBVTerm proxy n
_ FPRoundingMode
RNA = SBV RoundingMode
SBVType n FPRoundingMode
SBV.sRNA
  conSBVTerm proxy n
_ FPRoundingMode
RTP = SBV RoundingMode
SBVType n FPRoundingMode
SBV.sRTP
  conSBVTerm proxy n
_ FPRoundingMode
RTN = SBV RoundingMode
SBVType n FPRoundingMode
SBV.sRTN
  conSBVTerm proxy n
_ FPRoundingMode
RTZ = SBV RoundingMode
SBVType n FPRoundingMode
SBV.sRTZ
  symSBVName :: TypedSymbol FPRoundingMode -> Int -> String
symSBVName TypedSymbol FPRoundingMode
symbol Int
_ = TypedSymbol FPRoundingMode -> String
forall a. Show a => a -> String
show TypedSymbol FPRoundingMode
symbol
  symSBVTerm :: forall (m :: * -> *) (n :: Nat) (proxy :: Nat -> *).
(SBVFreshMonad m, KnownIsZero n) =>
proxy n -> String -> m (SBVType n FPRoundingMode)
symSBVTerm proxy n
_ String
name = String -> m (SBV RoundingMode)
forall a. SymVal a => String -> m (SBV a)
forall (m :: * -> *) a.
(SBVFreshMonad m, SymVal a) =>
String -> m (SBV a)
sbvFresh String
name
  withPrim :: forall (n :: Nat) (p :: Nat -> *) a.
KnownIsZero n =>
p n
-> ((PrimConstraint n FPRoundingMode,
     SMTDefinable (SBVType n FPRoundingMode),
     Mergeable (SBVType n FPRoundingMode),
     Typeable (SBVType n FPRoundingMode)) =>
    a)
-> a
withPrim p n
_ (PrimConstraint n FPRoundingMode,
 SMTDefinable (SBVType n FPRoundingMode),
 Mergeable (SBVType n FPRoundingMode),
 Typeable (SBVType n FPRoundingMode)) =>
a
r = a
(PrimConstraint n FPRoundingMode,
 SMTDefinable (SBVType n FPRoundingMode),
 Mergeable (SBVType n FPRoundingMode),
 Typeable (SBVType n FPRoundingMode)) =>
a
r
  parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> FPRoundingMode
parseSMTModelResult Int
_ ([([CV], CV)], CV)
cv =
    TypeRep FPRoundingMode -> ([([CV], CV)], CV) -> FPRoundingMode
forall a. HasCallStack => TypeRep a -> ([([CV], CV)], CV) -> a
parseSMTModelResultError (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @FPRoundingMode) ([([CV], CV)], CV)
cv

instance NonFuncSBVRep FPRoundingMode where
  type NonFuncSBVBaseType _ FPRoundingMode = SBV.RoundingMode

instance SupportedNonFuncPrim FPRoundingMode where
  conNonFuncSBVTerm :: forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n
-> FPRoundingMode -> SBV (NonFuncSBVBaseType n FPRoundingMode)
conNonFuncSBVTerm = proxy n
-> FPRoundingMode -> SBV (NonFuncSBVBaseType n FPRoundingMode)
proxy n -> FPRoundingMode -> SBVType n FPRoundingMode
forall (n :: Nat) (proxy :: Nat -> *).
KnownIsZero n =>
proxy n -> FPRoundingMode -> SBVType n FPRoundingMode
forall t (n :: Nat) (proxy :: Nat -> *).
(SupportedPrim t, KnownIsZero n) =>
proxy n -> t -> SBVType n t
conSBVTerm
  symNonFuncSBVTerm :: forall (m :: * -> *) (n :: Nat) (proxy :: Nat -> *).
(SBVFreshMonad m, KnownIsZero n) =>
proxy n -> String -> m (SBV (NonFuncSBVBaseType n FPRoundingMode))
symNonFuncSBVTerm = forall t (m :: * -> *) (n :: Nat) (proxy :: Nat -> *).
(SupportedPrim t, SBVFreshMonad m, KnownIsZero n) =>
proxy n -> String -> m (SBVType n t)
symSBVTerm @FPRoundingMode
  withNonFuncPrim :: forall (n :: Nat) (proxy :: Nat -> *) r.
KnownIsZero n =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n FPRoundingMode),
     EqSymbolic (SBVType n FPRoundingMode),
     Mergeable (SBVType n FPRoundingMode),
     SMTDefinable (SBVType n FPRoundingMode),
     Mergeable (SBVType n FPRoundingMode),
     SBVType n FPRoundingMode
     ~ SBV (NonFuncSBVBaseType n FPRoundingMode),
     PrimConstraint n FPRoundingMode) =>
    r)
-> r
withNonFuncPrim proxy n
_ (SymVal (NonFuncSBVBaseType n FPRoundingMode),
 EqSymbolic (SBVType n FPRoundingMode),
 Mergeable (SBVType n FPRoundingMode),
 SMTDefinable (SBVType n FPRoundingMode),
 Mergeable (SBVType n FPRoundingMode),
 SBVType n FPRoundingMode
 ~ SBV (NonFuncSBVBaseType n FPRoundingMode),
 PrimConstraint n FPRoundingMode) =>
r
r = r
(SymVal (NonFuncSBVBaseType n FPRoundingMode),
 EqSymbolic (SBVType n FPRoundingMode),
 Mergeable (SBVType n FPRoundingMode),
 SMTDefinable (SBVType n FPRoundingMode),
 Mergeable (SBVType n FPRoundingMode),
 SBVType n FPRoundingMode
 ~ SBV (NonFuncSBVBaseType n FPRoundingMode),
 PrimConstraint n FPRoundingMode) =>
r
r