{-# 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 Debug.Trace (trace)
import GHC.TypeNats (KnownNat, type (<=))
import Grisette.Internal.SymPrim.BV (IntN, WordN)
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,
        symSBVName,
        symSBVTerm,
        withPrim
      ),
    SupportedPrimConstraint
      ( PrimConstraint
      ),
    parseSMTModelResultError,
    pevalDefaultEqTerm,
    pevalITEBasicTerm,
    sbvFresh,
  )
import Grisette.Internal.SymPrim.Prim.ModelValue (ModelValue, toModelValue)
import Grisette.Internal.Utils.Parameterized (unsafeAxiom)
import Type.Reflection (typeRep)

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 = String -> Integer -> Integer
forall a. String -> a -> a
trace (([([CV], CV)], CV) -> String
forall a. Show a => a -> String
show ([([CV], CV)], CV)
cv) (Integer -> Integer) -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ TypeRep Integer -> ([([CV], CV)], CV) -> Integer
forall a. 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. 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. 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