{-# 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
( 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
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
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
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