{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# HLINT ignore "Eta reduce" #-}
{-# 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.Coerce (coerce)
import Data.Hashable (Hashable (hashWithSalt))
import Data.List.NonEmpty (NonEmpty ((:|)), toList)
import Data.Proxy (Proxy (Proxy))
import Data.SBV (BVIsNonZero)
import qualified Data.SBV as SBV
import Data.Type.Equality ((:~:) (Refl), type (:~~:) (HRefl))
import GHC.TypeNats (KnownNat, type (<=))
import Grisette.Internal.Core.Data.Class.IEEEFP
  ( fpIsNegativeZero,
    fpIsPositiveZero,
  )
import Grisette.Internal.SymPrim.AlgReal (AlgReal, fromSBVAlgReal, toSBVAlgReal)
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.Term
  ( IsSymbolKind (decideSymbolKind),
    NonFuncSBVRep (NonFuncSBVBaseType),
    SBVRep
      ( SBVType
      ),
    SupportedNonFuncPrim
      ( conNonFuncSBVTerm,
        symNonFuncSBVTerm,
        withNonFuncPrim
      ),
    SupportedPrim
      ( castTypedSymbol,
        conSBVTerm,
        defaultValue,
        funcDummyConstraint,
        hashConWithSalt,
        parseSMTModelResult,
        pevalDistinctTerm,
        pevalEqTerm,
        pevalITETerm,
        pformatCon,
        sameCon,
        sbvDistinct,
        sbvEq,
        sbvIte,
        symSBVName,
        symSBVTerm,
        withPrim
      ),
    SupportedPrimConstraint
      ( PrimConstraint
      ),
    Term,
    TypedSymbol (unTypedSymbol),
    conTerm,
    distinctTerm,
    eqTerm,
    parseScalarSMTModelResult,
    pevalDefaultEqTerm,
    pevalITEBasicTerm,
    pevalNotTerm,
    sbvFresh,
    typedAnySymbol,
    typedConstantSymbol,
    pattern ConTerm,
  )
import Grisette.Internal.Utils.Parameterized (unsafeAxiom)

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

-- Basic Integer
instance SBVRep Integer where
  type SBVType Integer = SBV.SBV Integer

instance SupportedPrimConstraint Integer where
  type PrimConstraint Integer = (Integral (NonFuncSBVBaseType Integer))

pairwiseHasConcreteEqual :: (SupportedNonFuncPrim a) => [Term a] -> Bool
pairwiseHasConcreteEqual :: forall a. SupportedNonFuncPrim a => [Term a] -> Bool
pairwiseHasConcreteEqual [] = Bool
False
pairwiseHasConcreteEqual [Term a
_] = Bool
False
pairwiseHasConcreteEqual (Term a
x : [Term a]
xs) =
  Term a -> [Term a] -> Bool
forall {t}. Eq t => t -> [t] -> Bool
go Term a
x [Term a]
xs Bool -> Bool -> Bool
|| [Term a] -> Bool
forall a. SupportedNonFuncPrim a => [Term a] -> Bool
pairwiseHasConcreteEqual [Term a]
xs
  where
    go :: t -> [t] -> Bool
go t
_ [] = Bool
False
    go t
x (t
y : [t]
ys) = t
x t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
y Bool -> Bool -> Bool
|| t -> [t] -> Bool
go t
x [t]
ys

getAllConcrete :: [Term a] -> Maybe [a]
getAllConcrete :: forall a. [Term a] -> Maybe [a]
getAllConcrete [] = [a] -> Maybe [a]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return []
getAllConcrete (ConTerm a
x : [Term a]
xs) = (a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
:) ([a] -> [a]) -> Maybe [a] -> Maybe [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Term a] -> Maybe [a]
forall a. [Term a] -> Maybe [a]
getAllConcrete [Term a]
xs
getAllConcrete [Term a]
_ = Maybe [a]
forall a. Maybe a
Nothing

checkConcreteDistinct :: (Eq t) => [t] -> Bool
checkConcreteDistinct :: forall t. Eq t => [t] -> Bool
checkConcreteDistinct [] = Bool
True
checkConcreteDistinct (t
x : [t]
xs) = t -> [t] -> Bool
forall {t}. Eq t => t -> [t] -> Bool
check0 t
x [t]
xs Bool -> Bool -> Bool
&& [t] -> Bool
forall t. Eq t => [t] -> Bool
checkConcreteDistinct [t]
xs
  where
    check0 :: t -> [t] -> Bool
check0 t
_ [] = Bool
True
    check0 t
x (t
y : [t]
ys) = t
x t -> t -> Bool
forall a. Eq a => a -> a -> Bool
/= t
y Bool -> Bool -> Bool
&& t -> [t] -> Bool
check0 t
x [t]
ys

pevalGeneralDistinct ::
  (SupportedNonFuncPrim a) => NonEmpty (Term a) -> Term Bool
pevalGeneralDistinct :: forall a. SupportedNonFuncPrim a => NonEmpty (Term a) -> Term Bool
pevalGeneralDistinct (Term a
_ :| []) = Bool -> Term Bool
forall t. SupportedPrim t => t -> Term t
conTerm Bool
True
pevalGeneralDistinct (Term a
a :| [Term a
b]) = Term Bool -> Term Bool
pevalNotTerm (Term Bool -> Term Bool) -> Term Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term Bool
forall t. SupportedPrim t => Term t -> Term t -> Term Bool
pevalEqTerm Term a
a Term a
b
pevalGeneralDistinct NonEmpty (Term a)
l | [Term a] -> Bool
forall a. SupportedNonFuncPrim a => [Term a] -> Bool
pairwiseHasConcreteEqual ([Term a] -> Bool) -> [Term a] -> Bool
forall a b. (a -> b) -> a -> b
$ NonEmpty (Term a) -> [Term a]
forall a. NonEmpty a -> [a]
toList NonEmpty (Term a)
l = Bool -> Term Bool
forall t. SupportedPrim t => t -> Term t
conTerm Bool
False
pevalGeneralDistinct NonEmpty (Term a)
l =
  case [Term a] -> Maybe [a]
forall a. [Term a] -> Maybe [a]
getAllConcrete (NonEmpty (Term a) -> [Term a]
forall a. NonEmpty a -> [a]
toList NonEmpty (Term a)
l) of
    Maybe [a]
Nothing -> NonEmpty (Term a) -> Term Bool
forall a. NonEmpty (Term a) -> Term Bool
distinctTerm NonEmpty (Term a)
l
    Just [a]
xs -> Bool -> Term Bool
forall t. SupportedPrim t => t -> Term t
conTerm (Bool -> Term Bool) -> Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ [a] -> Bool
forall t. Eq t => [t] -> Bool
checkConcreteDistinct [a]
xs

instance SupportedPrim Integer where
  pformatCon :: Integer -> String
pformatCon = Integer -> String
forall a. Show a => a -> String
show
  defaultValue :: Integer
defaultValue = Integer
defaultValueForInteger
  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. SupportedNonFuncPrim a => Term a -> Term a -> Term Bool
pevalDefaultEqTerm
  pevalDistinctTerm :: NonEmpty (Term Integer) -> Term Bool
pevalDistinctTerm = NonEmpty (Term Integer) -> Term Bool
forall a. SupportedNonFuncPrim a => NonEmpty (Term a) -> Term Bool
pevalGeneralDistinct
  conSBVTerm :: Integer -> SBVType Integer
conSBVTerm Integer
n = Integer -> SBV Integer
forall a. Num a => Integer -> a
fromInteger Integer
n
  symSBVName :: TypedSymbol 'AnyKind Integer -> Int -> String
symSBVName TypedSymbol 'AnyKind Integer
symbol Int
_ = TypedSymbol 'AnyKind Integer -> String
forall a. Show a => a -> String
show TypedSymbol 'AnyKind Integer
symbol
  symSBVTerm :: forall (m :: * -> *).
SBVFreshMonad m =>
String -> m (SBVType Integer)
symSBVTerm String
name = 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
  parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> Integer
parseSMTModelResult Int
_ = (Integer -> Integer) -> ([([CV], CV)], CV) -> Integer
forall v r.
(SatModel r, Typeable v) =>
(r -> v) -> ([([CV], CV)], CV) -> v
parseScalarSMTModelResult Integer -> Integer
forall a. a -> a
id
  castTypedSymbol ::
    forall knd knd'.
    (IsSymbolKind knd') =>
    TypedSymbol knd Integer ->
    Maybe (TypedSymbol knd' Integer)
  castTypedSymbol :: forall (knd :: SymbolKind) (knd' :: SymbolKind).
IsSymbolKind knd' =>
TypedSymbol knd Integer -> Maybe (TypedSymbol knd' Integer)
castTypedSymbol TypedSymbol knd Integer
s =
    case forall (knd :: SymbolKind).
IsSymbolKind knd =>
Either (knd :~~: 'ConstantKind) (knd :~~: 'AnyKind)
decideSymbolKind @knd' of
      Left knd' :~~: 'ConstantKind
HRefl -> TypedSymbol knd' Integer -> Maybe (TypedSymbol knd' Integer)
forall a. a -> Maybe a
Just (TypedSymbol knd' Integer -> Maybe (TypedSymbol knd' Integer))
-> TypedSymbol knd' Integer -> Maybe (TypedSymbol knd' Integer)
forall a b. (a -> b) -> a -> b
$ Symbol -> TypedSymbol 'ConstantKind Integer
forall t.
SupportedNonFuncPrim t =>
Symbol -> TypedSymbol 'ConstantKind t
typedConstantSymbol (Symbol -> TypedSymbol 'ConstantKind Integer)
-> Symbol -> TypedSymbol 'ConstantKind Integer
forall a b. (a -> b) -> a -> b
$ TypedSymbol knd Integer -> Symbol
forall t (knd :: SymbolKind). TypedSymbol knd t -> Symbol
unTypedSymbol TypedSymbol knd Integer
s
      Right knd' :~~: 'AnyKind
HRefl -> TypedSymbol knd' Integer -> Maybe (TypedSymbol knd' Integer)
forall a. a -> Maybe a
Just (TypedSymbol knd' Integer -> Maybe (TypedSymbol knd' Integer))
-> TypedSymbol knd' Integer -> Maybe (TypedSymbol knd' Integer)
forall a b. (a -> b) -> a -> b
$ Symbol -> TypedSymbol 'AnyKind Integer
forall t. SupportedPrim t => Symbol -> TypedSymbol 'AnyKind t
typedAnySymbol (Symbol -> TypedSymbol 'AnyKind Integer)
-> Symbol -> TypedSymbol 'AnyKind Integer
forall a b. (a -> b) -> a -> b
$ TypedSymbol knd Integer -> Symbol
forall t (knd :: SymbolKind). TypedSymbol knd t -> Symbol
unTypedSymbol TypedSymbol knd Integer
s
  funcDummyConstraint :: SBVType Integer -> SBV Bool
funcDummyConstraint SBVType Integer
_ = SBV Bool
SBV.sTrue

instance NonFuncSBVRep Integer where
  type NonFuncSBVBaseType Integer = Integer

instance SupportedNonFuncPrim Integer where
  conNonFuncSBVTerm :: Integer -> SBV (NonFuncSBVBaseType Integer)
conNonFuncSBVTerm = Integer -> SBV (NonFuncSBVBaseType Integer)
Integer -> SBVType Integer
forall t. SupportedPrim t => t -> SBVType t
conSBVTerm
  symNonFuncSBVTerm :: forall (m :: * -> *).
SBVFreshMonad m =>
String -> m (SBV (NonFuncSBVBaseType Integer))
symNonFuncSBVTerm = forall t (m :: * -> *).
(SupportedPrim t, SBVFreshMonad m) =>
String -> m (SBVType t)
symSBVTerm @Integer
  withNonFuncPrim :: forall r. (NonFuncPrimConstraint Integer => r) -> r
withNonFuncPrim NonFuncPrimConstraint Integer => r
r = r
NonFuncPrimConstraint 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
  sbvDistinct :: NonEmpty (SBVType (IntN w)) -> SBV Bool
sbvDistinct = forall t a.
SupportedPrim t =>
((PrimConstraint t, SMTDefinable (SBVType t),
  Mergeable (SBVType t), Typeable (SBVType t)) =>
 a)
-> a
withPrim @(IntN w) (((PrimConstraint (IntN w), SMTDefinable (SBVType (IntN w)),
   Mergeable (SBVType (IntN w)), Typeable (SBVType (IntN w))) =>
  NonEmpty (SBVType (IntN w)) -> SBV Bool)
 -> NonEmpty (SBVType (IntN w)) -> SBV Bool)
-> ((PrimConstraint (IntN w), SMTDefinable (SBVType (IntN w)),
     Mergeable (SBVType (IntN w)), Typeable (SBVType (IntN w))) =>
    NonEmpty (SBVType (IntN w)) -> SBV Bool)
-> NonEmpty (SBVType (IntN w))
-> SBV Bool
forall a b. (a -> b) -> a -> b
$ [SBV (IntN w)] -> SBV Bool
forall a. EqSymbolic a => [a] -> SBV Bool
SBV.distinct ([SBV (IntN w)] -> SBV Bool)
-> (NonEmpty (SBV (IntN w)) -> [SBV (IntN w)])
-> NonEmpty (SBV (IntN w))
-> SBV Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty (SBV (IntN w)) -> [SBV (IntN w)]
forall a. NonEmpty a -> [a]
toList
  sbvEq :: SBVType (IntN w) -> SBVType (IntN w) -> SBV Bool
sbvEq = forall t a.
SupportedPrim t =>
((PrimConstraint t, SMTDefinable (SBVType t),
  Mergeable (SBVType t), Typeable (SBVType t)) =>
 a)
-> a
withPrim @(IntN w) SBV (IntN w) -> SBV (IntN w) -> SBV Bool
(PrimConstraint (IntN w), SMTDefinable (SBVType (IntN w)),
 Mergeable (SBVType (IntN w)), Typeable (SBVType (IntN w))) =>
SBV (IntN w) -> SBV (IntN w) -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
(SBV..==)
  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. SupportedNonFuncPrim a => Term a -> Term a -> Term Bool
pevalDefaultEqTerm
  pevalDistinctTerm :: NonEmpty (Term (IntN w)) -> Term Bool
pevalDistinctTerm = NonEmpty (Term (IntN w)) -> Term Bool
forall a. SupportedNonFuncPrim a => NonEmpty (Term a) -> Term Bool
pevalGeneralDistinct
  conSBVTerm :: IntN w -> SBVType (IntN w)
conSBVTerm IntN w
n = Proxy w -> (BVIsNonZero w => SBVType (IntN w)) -> SBVType (IntN w)
forall (w :: Natural) r (proxy :: Natural -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @w) ((BVIsNonZero w => SBVType (IntN w)) -> SBVType (IntN w))
-> (BVIsNonZero w => SBVType (IntN w)) -> SBVType (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 'AnyKind (IntN w) -> Int -> String
symSBVName TypedSymbol 'AnyKind (IntN w)
symbol Int
_ = TypedSymbol 'AnyKind (IntN w) -> String
forall a. Show a => a -> String
show TypedSymbol 'AnyKind (IntN w)
symbol
  symSBVTerm :: forall (m :: * -> *).
SBVFreshMonad m =>
String -> m (SBVType (IntN w))
symSBVTerm String
name = Proxy w
-> (BVIsNonZero w => m (SBVType (IntN w))) -> m (SBVType (IntN w))
forall (w :: Natural) r (proxy :: Natural -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @w) ((BVIsNonZero w => m (SBVType (IntN w))) -> m (SBVType (IntN w)))
-> (BVIsNonZero w => m (SBVType (IntN w))) -> m (SBVType (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 a.
((PrimConstraint (IntN w), SMTDefinable (SBVType (IntN w)),
  Mergeable (SBVType (IntN w)), Typeable (SBVType (IntN w))) =>
 a)
-> a
withPrim (PrimConstraint (IntN w), SMTDefinable (SBVType (IntN w)),
 Mergeable (SBVType (IntN w)), Typeable (SBVType (IntN w))) =>
a
r = Proxy w -> (BVIsNonZero w => a) -> a
forall (w :: Natural) r (proxy :: Natural -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @w) a
BVIsNonZero w => a
(PrimConstraint (IntN w), SMTDefinable (SBVType (IntN w)),
 Mergeable (SBVType (IntN w)), Typeable (SBVType (IntN w))) =>
a
r
  {-# INLINE withPrim #-}
  parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> IntN w
parseSMTModelResult Int
_ ([([CV], CV)], CV)
cv =
    forall t a.
SupportedPrim t =>
((PrimConstraint t, SMTDefinable (SBVType t),
  Mergeable (SBVType t), Typeable (SBVType t)) =>
 a)
-> a
withPrim @(IntN w) (((PrimConstraint (IntN w), SMTDefinable (SBVType (IntN w)),
   Mergeable (SBVType (IntN w)), Typeable (SBVType (IntN w))) =>
  IntN w)
 -> IntN w)
-> ((PrimConstraint (IntN w), SMTDefinable (SBVType (IntN w)),
     Mergeable (SBVType (IntN w)), Typeable (SBVType (IntN w))) =>
    IntN w)
-> IntN w
forall a b. (a -> b) -> a -> b
$
      (IntN w -> IntN w) -> ([([CV], CV)], CV) -> IntN w
forall v r.
(SatModel r, Typeable v) =>
(r -> v) -> ([([CV], CV)], CV) -> v
parseScalarSMTModelResult (\(IntN w
x :: SBV.IntN w) -> IntN w -> IntN w
forall a b. (Integral a, Num b) => a -> b
fromIntegral IntN w
x) ([([CV], CV)], CV)
cv
  castTypedSymbol ::
    forall knd knd'.
    (IsSymbolKind knd') =>
    TypedSymbol knd (IntN w) ->
    Maybe (TypedSymbol knd' (IntN w))
  castTypedSymbol :: forall (knd :: SymbolKind) (knd' :: SymbolKind).
IsSymbolKind knd' =>
TypedSymbol knd (IntN w) -> Maybe (TypedSymbol knd' (IntN w))
castTypedSymbol TypedSymbol knd (IntN w)
s =
    case forall (knd :: SymbolKind).
IsSymbolKind knd =>
Either (knd :~~: 'ConstantKind) (knd :~~: 'AnyKind)
decideSymbolKind @knd' of
      Left knd' :~~: 'ConstantKind
HRefl -> TypedSymbol knd' (IntN w) -> Maybe (TypedSymbol knd' (IntN w))
forall a. a -> Maybe a
Just (TypedSymbol knd' (IntN w) -> Maybe (TypedSymbol knd' (IntN w)))
-> TypedSymbol knd' (IntN w) -> Maybe (TypedSymbol knd' (IntN w))
forall a b. (a -> b) -> a -> b
$ Symbol -> TypedSymbol 'ConstantKind (IntN w)
forall t.
SupportedNonFuncPrim t =>
Symbol -> TypedSymbol 'ConstantKind t
typedConstantSymbol (Symbol -> TypedSymbol 'ConstantKind (IntN w))
-> Symbol -> TypedSymbol 'ConstantKind (IntN w)
forall a b. (a -> b) -> a -> b
$ TypedSymbol knd (IntN w) -> Symbol
forall t (knd :: SymbolKind). TypedSymbol knd t -> Symbol
unTypedSymbol TypedSymbol knd (IntN w)
s
      Right knd' :~~: 'AnyKind
HRefl -> TypedSymbol knd' (IntN w) -> Maybe (TypedSymbol knd' (IntN w))
forall a. a -> Maybe a
Just (TypedSymbol knd' (IntN w) -> Maybe (TypedSymbol knd' (IntN w)))
-> TypedSymbol knd' (IntN w) -> Maybe (TypedSymbol knd' (IntN w))
forall a b. (a -> b) -> a -> b
$ Symbol -> TypedSymbol 'AnyKind (IntN w)
forall t. SupportedPrim t => Symbol -> TypedSymbol 'AnyKind t
typedAnySymbol (Symbol -> TypedSymbol 'AnyKind (IntN w))
-> Symbol -> TypedSymbol 'AnyKind (IntN w)
forall a b. (a -> b) -> a -> b
$ TypedSymbol knd (IntN w) -> Symbol
forall t (knd :: SymbolKind). TypedSymbol knd t -> Symbol
unTypedSymbol TypedSymbol knd (IntN w)
s
  funcDummyConstraint :: SBVType (IntN w) -> SBV Bool
funcDummyConstraint SBVType (IntN w)
_ = SBV Bool
SBV.sTrue

-- | Construct the 'SBV.BVIsNonZero' constraint from the proof that the width is
-- at least 1.
bvIsNonZeroFromGEq1 ::
  forall w r proxy.
  (1 <= w) =>
  proxy w ->
  ((SBV.BVIsNonZero w) => r) ->
  r
bvIsNonZeroFromGEq1 :: forall (w :: Natural) r (proxy :: Natural -> *).
(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
{-# INLINE bvIsNonZeroFromGEq1 #-}

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 :: IntN w -> SBV (NonFuncSBVBaseType (IntN w))
conNonFuncSBVTerm = IntN w -> SBV (NonFuncSBVBaseType (IntN w))
IntN w -> SBVType (IntN w)
forall t. SupportedPrim t => t -> SBVType t
conSBVTerm
  symNonFuncSBVTerm :: forall (m :: * -> *).
SBVFreshMonad m =>
String -> m (SBV (NonFuncSBVBaseType (IntN w)))
symNonFuncSBVTerm = forall t (m :: * -> *).
(SupportedPrim t, SBVFreshMonad m) =>
String -> m (SBVType t)
symSBVTerm @(IntN w)
  withNonFuncPrim :: forall r. (NonFuncPrimConstraint (IntN w) => r) -> r
withNonFuncPrim NonFuncPrimConstraint (IntN w) => r
r = Proxy w -> (BVIsNonZero w => r) -> r
forall (w :: Natural) r (proxy :: Natural -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @w) r
NonFuncPrimConstraint (IntN w) => r
BVIsNonZero 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
  sbvDistinct :: NonEmpty (SBVType (WordN w)) -> SBV Bool
sbvDistinct = forall t a.
SupportedPrim t =>
((PrimConstraint t, SMTDefinable (SBVType t),
  Mergeable (SBVType t), Typeable (SBVType t)) =>
 a)
-> a
withPrim @(WordN w) (((PrimConstraint (WordN w), SMTDefinable (SBVType (WordN w)),
   Mergeable (SBVType (WordN w)), Typeable (SBVType (WordN w))) =>
  NonEmpty (SBVType (WordN w)) -> SBV Bool)
 -> NonEmpty (SBVType (WordN w)) -> SBV Bool)
-> ((PrimConstraint (WordN w), SMTDefinable (SBVType (WordN w)),
     Mergeable (SBVType (WordN w)), Typeable (SBVType (WordN w))) =>
    NonEmpty (SBVType (WordN w)) -> SBV Bool)
-> NonEmpty (SBVType (WordN w))
-> SBV Bool
forall a b. (a -> b) -> a -> b
$ [SBV (WordN w)] -> SBV Bool
forall a. EqSymbolic a => [a] -> SBV Bool
SBV.distinct ([SBV (WordN w)] -> SBV Bool)
-> (NonEmpty (SBV (WordN w)) -> [SBV (WordN w)])
-> NonEmpty (SBV (WordN w))
-> SBV Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty (SBV (WordN w)) -> [SBV (WordN w)]
forall a. NonEmpty a -> [a]
toList
  sbvEq :: SBVType (WordN w) -> SBVType (WordN w) -> SBV Bool
sbvEq = forall t a.
SupportedPrim t =>
((PrimConstraint t, SMTDefinable (SBVType t),
  Mergeable (SBVType t), Typeable (SBVType t)) =>
 a)
-> a
withPrim @(WordN w) SBV (WordN w) -> SBV (WordN w) -> SBV Bool
(PrimConstraint (WordN w), SMTDefinable (SBVType (WordN w)),
 Mergeable (SBVType (WordN w)), Typeable (SBVType (WordN w))) =>
SBV (WordN w) -> SBV (WordN w) -> SBV Bool
forall a. EqSymbolic a => a -> a -> SBV Bool
(SBV..==)
  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. SupportedNonFuncPrim a => Term a -> Term a -> Term Bool
pevalDefaultEqTerm
  pevalDistinctTerm :: NonEmpty (Term (WordN w)) -> Term Bool
pevalDistinctTerm = NonEmpty (Term (WordN w)) -> Term Bool
forall a. SupportedNonFuncPrim a => NonEmpty (Term a) -> Term Bool
pevalGeneralDistinct
  conSBVTerm :: WordN w -> SBVType (WordN w)
conSBVTerm WordN w
n = Proxy w
-> (BVIsNonZero w => SBVType (WordN w)) -> SBVType (WordN w)
forall (w :: Natural) r (proxy :: Natural -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @w) ((BVIsNonZero w => SBVType (WordN w)) -> SBVType (WordN w))
-> (BVIsNonZero w => SBVType (WordN w)) -> SBVType (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 'AnyKind (WordN w) -> Int -> String
symSBVName TypedSymbol 'AnyKind (WordN w)
symbol Int
_ = TypedSymbol 'AnyKind (WordN w) -> String
forall a. Show a => a -> String
show TypedSymbol 'AnyKind (WordN w)
symbol
  symSBVTerm :: forall (m :: * -> *).
SBVFreshMonad m =>
String -> m (SBVType (WordN w))
symSBVTerm String
name = Proxy w
-> (BVIsNonZero w => m (SBVType (WordN w)))
-> m (SBVType (WordN w))
forall (w :: Natural) r (proxy :: Natural -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @w) ((BVIsNonZero w => m (SBVType (WordN w))) -> m (SBVType (WordN w)))
-> (BVIsNonZero w => m (SBVType (WordN w)))
-> m (SBVType (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 a.
((PrimConstraint (WordN w), SMTDefinable (SBVType (WordN w)),
  Mergeable (SBVType (WordN w)), Typeable (SBVType (WordN w))) =>
 a)
-> a
withPrim (PrimConstraint (WordN w), SMTDefinable (SBVType (WordN w)),
 Mergeable (SBVType (WordN w)), Typeable (SBVType (WordN w))) =>
a
r = Proxy w -> (BVIsNonZero w => a) -> a
forall (w :: Natural) r (proxy :: Natural -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @w) a
BVIsNonZero w => a
(PrimConstraint (WordN w), SMTDefinable (SBVType (WordN w)),
 Mergeable (SBVType (WordN w)), Typeable (SBVType (WordN w))) =>
a
r
  {-# INLINE withPrim #-}
  parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> WordN w
parseSMTModelResult Int
_ ([([CV], CV)], CV)
cv =
    forall t a.
SupportedPrim t =>
((PrimConstraint t, SMTDefinable (SBVType t),
  Mergeable (SBVType t), Typeable (SBVType t)) =>
 a)
-> a
withPrim @(IntN w) (((PrimConstraint (IntN w), SMTDefinable (SBVType (IntN w)),
   Mergeable (SBVType (IntN w)), Typeable (SBVType (IntN w))) =>
  WordN w)
 -> WordN w)
-> ((PrimConstraint (IntN w), SMTDefinable (SBVType (IntN w)),
     Mergeable (SBVType (IntN w)), Typeable (SBVType (IntN w))) =>
    WordN w)
-> WordN w
forall a b. (a -> b) -> a -> b
$
      (WordN w -> WordN w) -> ([([CV], CV)], CV) -> WordN w
forall v r.
(SatModel r, Typeable v) =>
(r -> v) -> ([([CV], CV)], CV) -> v
parseScalarSMTModelResult (\(WordN w
x :: SBV.WordN w) -> WordN w -> WordN w
forall a b. (Integral a, Num b) => a -> b
fromIntegral WordN w
x) ([([CV], CV)], CV)
cv
  castTypedSymbol ::
    forall knd knd'.
    (IsSymbolKind knd') =>
    TypedSymbol knd (WordN w) ->
    Maybe (TypedSymbol knd' (WordN w))
  castTypedSymbol :: forall (knd :: SymbolKind) (knd' :: SymbolKind).
IsSymbolKind knd' =>
TypedSymbol knd (WordN w) -> Maybe (TypedSymbol knd' (WordN w))
castTypedSymbol TypedSymbol knd (WordN w)
s =
    case forall (knd :: SymbolKind).
IsSymbolKind knd =>
Either (knd :~~: 'ConstantKind) (knd :~~: 'AnyKind)
decideSymbolKind @knd' of
      Left knd' :~~: 'ConstantKind
HRefl -> TypedSymbol knd' (WordN w) -> Maybe (TypedSymbol knd' (WordN w))
forall a. a -> Maybe a
Just (TypedSymbol knd' (WordN w) -> Maybe (TypedSymbol knd' (WordN w)))
-> TypedSymbol knd' (WordN w) -> Maybe (TypedSymbol knd' (WordN w))
forall a b. (a -> b) -> a -> b
$ Symbol -> TypedSymbol 'ConstantKind (WordN w)
forall t.
SupportedNonFuncPrim t =>
Symbol -> TypedSymbol 'ConstantKind t
typedConstantSymbol (Symbol -> TypedSymbol 'ConstantKind (WordN w))
-> Symbol -> TypedSymbol 'ConstantKind (WordN w)
forall a b. (a -> b) -> a -> b
$ TypedSymbol knd (WordN w) -> Symbol
forall t (knd :: SymbolKind). TypedSymbol knd t -> Symbol
unTypedSymbol TypedSymbol knd (WordN w)
s
      Right knd' :~~: 'AnyKind
HRefl -> TypedSymbol knd' (WordN w) -> Maybe (TypedSymbol knd' (WordN w))
forall a. a -> Maybe a
Just (TypedSymbol knd' (WordN w) -> Maybe (TypedSymbol knd' (WordN w)))
-> TypedSymbol knd' (WordN w) -> Maybe (TypedSymbol knd' (WordN w))
forall a b. (a -> b) -> a -> b
$ Symbol -> TypedSymbol 'AnyKind (WordN w)
forall t. SupportedPrim t => Symbol -> TypedSymbol 'AnyKind t
typedAnySymbol (Symbol -> TypedSymbol 'AnyKind (WordN w))
-> Symbol -> TypedSymbol 'AnyKind (WordN w)
forall a b. (a -> b) -> a -> b
$ TypedSymbol knd (WordN w) -> Symbol
forall t (knd :: SymbolKind). TypedSymbol knd t -> Symbol
unTypedSymbol TypedSymbol knd (WordN w)
s
  funcDummyConstraint :: SBVType (WordN w) -> SBV Bool
funcDummyConstraint SBVType (WordN w)
_ = SBV Bool
SBV.sTrue

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 :: WordN w -> SBV (NonFuncSBVBaseType (WordN w))
conNonFuncSBVTerm = WordN w -> SBV (NonFuncSBVBaseType (WordN w))
WordN w -> SBVType (WordN w)
forall t. SupportedPrim t => t -> SBVType t
conSBVTerm
  symNonFuncSBVTerm :: forall (m :: * -> *).
SBVFreshMonad m =>
String -> m (SBV (NonFuncSBVBaseType (WordN w)))
symNonFuncSBVTerm = forall t (m :: * -> *).
(SupportedPrim t, SBVFreshMonad m) =>
String -> m (SBVType t)
symSBVTerm @(WordN w)
  withNonFuncPrim :: forall r. (NonFuncPrimConstraint (WordN w) => r) -> r
withNonFuncPrim NonFuncPrimConstraint (WordN w) => r
r = Proxy w -> (BVIsNonZero w => r) -> r
forall (w :: Natural) r (proxy :: Natural -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @w) r
NonFuncPrimConstraint (WordN w) => r
BVIsNonZero 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
  sameCon :: FP eb sb -> FP eb sb -> Bool
sameCon FP eb sb
a FP eb sb
b
    | FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
isNaN FP eb sb
a = FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
isNaN FP eb sb
b
    | FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsPositiveZero FP eb sb
a = FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsPositiveZero FP eb sb
b
    | FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsNegativeZero FP eb sb
a = FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
fpIsNegativeZero FP eb sb
b
    | Bool
otherwise = FP eb sb
a FP eb sb -> FP eb sb -> Bool
forall a. Eq a => a -> a -> Bool
== FP eb sb
b
  hashConWithSalt :: Int -> FP eb sb -> Int
hashConWithSalt Int
s FP eb sb
a
    | FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
isNaN FP eb sb
a = Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s (Int
2654435761 :: Int)
    | Bool
otherwise = Int -> FP eb sb -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s FP eb sb
a
  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 FP eb sb
l) (ConTerm FP eb sb
r) = Bool -> Term Bool
forall t. SupportedPrim 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 t. SupportedPrim t => Term t -> Term t -> 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. Term a -> Term a -> Term Bool
eqTerm Term (FP eb sb)
l Term (FP eb sb)
r
  pevalDistinctTerm :: NonEmpty (Term (FP eb sb)) -> Term Bool
pevalDistinctTerm (Term (FP eb sb)
_ :| []) = Bool -> Term Bool
forall t. SupportedPrim t => t -> Term t
conTerm Bool
True
  pevalDistinctTerm (Term (FP eb sb)
a :| [Term (FP eb sb)
b]) = Term Bool -> Term Bool
pevalNotTerm (Term Bool -> Term Bool) -> Term Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ Term (FP eb sb) -> Term (FP eb sb) -> Term Bool
forall t. SupportedPrim t => Term t -> Term t -> Term Bool
pevalEqTerm Term (FP eb sb)
a Term (FP eb sb)
b
  pevalDistinctTerm NonEmpty (Term (FP eb sb))
l =
    case [Term (FP eb sb)] -> Maybe [FP eb sb]
forall a. [Term a] -> Maybe [a]
getAllConcrete (NonEmpty (Term (FP eb sb)) -> [Term (FP eb sb)]
forall a. NonEmpty a -> [a]
toList NonEmpty (Term (FP eb sb))
l) of
      Maybe [FP eb sb]
Nothing -> NonEmpty (Term (FP eb sb)) -> Term Bool
forall a. NonEmpty (Term a) -> Term Bool
distinctTerm NonEmpty (Term (FP eb sb))
l
      Just [FP eb sb]
xs | (FP eb sb -> Bool) -> [FP eb sb] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any FP eb sb -> Bool
forall a. RealFloat a => a -> Bool
isNaN [FP eb sb]
xs -> NonEmpty (Term (FP eb sb)) -> Term Bool
forall a. NonEmpty (Term a) -> Term Bool
distinctTerm NonEmpty (Term (FP eb sb))
l
      Just [FP eb sb]
xs -> Bool -> Term Bool
forall t. SupportedPrim t => t -> Term t
conTerm (Bool -> Term Bool) -> Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ [FP eb sb] -> Bool
forall t. Eq t => [t] -> Bool
checkConcreteDistinct [FP eb sb]
xs
  conSBVTerm :: FP eb sb -> SBVType (FP eb sb)
conSBVTerm (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 'AnyKind (FP eb sb) -> Int -> String
symSBVName TypedSymbol 'AnyKind (FP eb sb)
symbol Int
_ = TypedSymbol 'AnyKind (FP eb sb) -> String
forall a. Show a => a -> String
show TypedSymbol 'AnyKind (FP eb sb)
symbol
  symSBVTerm :: forall (m :: * -> *).
SBVFreshMonad m =>
String -> m (SBVType (FP eb sb))
symSBVTerm 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
  parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> FP eb sb
parseSMTModelResult Int
_ ([([CV], CV)], CV)
cv =
    forall t a.
SupportedPrim t =>
((PrimConstraint t, SMTDefinable (SBVType t),
  Mergeable (SBVType t), Typeable (SBVType t)) =>
 a)
-> a
withPrim @(FP eb sb) (((PrimConstraint (FP eb sb), SMTDefinable (SBVType (FP eb sb)),
   Mergeable (SBVType (FP eb sb)), Typeable (SBVType (FP eb sb))) =>
  FP eb sb)
 -> FP eb sb)
-> ((PrimConstraint (FP eb sb), SMTDefinable (SBVType (FP eb sb)),
     Mergeable (SBVType (FP eb sb)), Typeable (SBVType (FP eb sb))) =>
    FP eb sb)
-> FP eb sb
forall a b. (a -> b) -> a -> b
$
      (FloatingPoint eb sb -> FP eb sb) -> ([([CV], CV)], CV) -> FP eb sb
forall v r.
(SatModel r, Typeable v) =>
(r -> v) -> ([([CV], CV)], CV) -> v
parseScalarSMTModelResult (\(FloatingPoint eb sb
x :: SBV.FloatingPoint eb sb) -> FloatingPoint eb sb -> FP eb sb
forall a b. Coercible a b => a -> b
coerce FloatingPoint eb sb
x) ([([CV], CV)], CV)
cv
  funcDummyConstraint :: SBVType (FP eb sb) -> SBV Bool
funcDummyConstraint SBVType (FP eb sb)
_ = SBV Bool
SBV.sTrue

  -- Workaround for sbv#702.
  sbvIte :: SBV Bool
-> SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb)
sbvIte = forall t a.
SupportedPrim t =>
((PrimConstraint t, SMTDefinable (SBVType t),
  Mergeable (SBVType t), Typeable (SBVType t)) =>
 a)
-> a
withPrim @(FP eb sb) (((PrimConstraint (FP eb sb), SMTDefinable (SBVType (FP eb sb)),
   Mergeable (SBVType (FP eb sb)), Typeable (SBVType (FP eb sb))) =>
  SBV Bool
  -> SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb))
 -> SBV Bool
 -> SBVType (FP eb sb)
 -> SBVType (FP eb sb)
 -> SBVType (FP eb sb))
-> ((PrimConstraint (FP eb sb), SMTDefinable (SBVType (FP eb sb)),
     Mergeable (SBVType (FP eb sb)), Typeable (SBVType (FP eb sb))) =>
    SBV Bool
    -> SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb))
-> SBV Bool
-> SBVType (FP eb sb)
-> SBVType (FP eb sb)
-> SBVType (FP eb sb)
forall a b. (a -> b) -> a -> b
$ \SBV Bool
c SBVType (FP eb sb)
a SBVType (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 (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 (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.
SupportedPrim t =>
SBV Bool -> SBVType t -> SBVType t -> SBVType t
sbvIte @(FP eb sb)
                    SBV Bool
c
                    (forall t. SupportedPrim t => t -> SBVType t
conSBVTerm @(FP eb sb) (FP eb sb -> SBVType (FP eb sb)) -> FP eb sb -> SBVType (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. SupportedPrim t => t -> SBVType t
conSBVTerm @(FP eb sb) (FP eb sb -> SBVType (FP eb sb)) -> FP eb sb -> SBVType (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 (FP eb sb)
a SBV (FloatingPoint eb sb)
SBVType (FP eb sb)
b
  castTypedSymbol ::
    forall knd knd'.
    (IsSymbolKind knd') =>
    TypedSymbol knd (FP eb sb) ->
    Maybe (TypedSymbol knd' (FP eb sb))
  castTypedSymbol :: forall (knd :: SymbolKind) (knd' :: SymbolKind).
IsSymbolKind knd' =>
TypedSymbol knd (FP eb sb) -> Maybe (TypedSymbol knd' (FP eb sb))
castTypedSymbol TypedSymbol knd (FP eb sb)
s =
    case forall (knd :: SymbolKind).
IsSymbolKind knd =>
Either (knd :~~: 'ConstantKind) (knd :~~: 'AnyKind)
decideSymbolKind @knd' of
      Left knd' :~~: 'ConstantKind
HRefl -> TypedSymbol knd' (FP eb sb) -> Maybe (TypedSymbol knd' (FP eb sb))
forall a. a -> Maybe a
Just (TypedSymbol knd' (FP eb sb)
 -> Maybe (TypedSymbol knd' (FP eb sb)))
-> TypedSymbol knd' (FP eb sb)
-> Maybe (TypedSymbol knd' (FP eb sb))
forall a b. (a -> b) -> a -> b
$ Symbol -> TypedSymbol 'ConstantKind (FP eb sb)
forall t.
SupportedNonFuncPrim t =>
Symbol -> TypedSymbol 'ConstantKind t
typedConstantSymbol (Symbol -> TypedSymbol 'ConstantKind (FP eb sb))
-> Symbol -> TypedSymbol 'ConstantKind (FP eb sb)
forall a b. (a -> b) -> a -> b
$ TypedSymbol knd (FP eb sb) -> Symbol
forall t (knd :: SymbolKind). TypedSymbol knd t -> Symbol
unTypedSymbol TypedSymbol knd (FP eb sb)
s
      Right knd' :~~: 'AnyKind
HRefl -> TypedSymbol knd' (FP eb sb) -> Maybe (TypedSymbol knd' (FP eb sb))
forall a. a -> Maybe a
Just (TypedSymbol knd' (FP eb sb)
 -> Maybe (TypedSymbol knd' (FP eb sb)))
-> TypedSymbol knd' (FP eb sb)
-> Maybe (TypedSymbol knd' (FP eb sb))
forall a b. (a -> b) -> a -> b
$ Symbol -> TypedSymbol 'AnyKind (FP eb sb)
forall t. SupportedPrim t => Symbol -> TypedSymbol 'AnyKind t
typedAnySymbol (Symbol -> TypedSymbol 'AnyKind (FP eb sb))
-> Symbol -> TypedSymbol 'AnyKind (FP eb sb)
forall a b. (a -> b) -> a -> b
$ TypedSymbol knd (FP eb sb) -> Symbol
forall t (knd :: SymbolKind). TypedSymbol knd t -> Symbol
unTypedSymbol TypedSymbol knd (FP eb sb)
s

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 :: FP eb sb -> SBV (NonFuncSBVBaseType (FP eb sb))
conNonFuncSBVTerm = FP eb sb -> SBV (NonFuncSBVBaseType (FP eb sb))
FP eb sb -> SBVType (FP eb sb)
forall t. SupportedPrim t => t -> SBVType t
conSBVTerm
  symNonFuncSBVTerm :: forall (m :: * -> *).
SBVFreshMonad m =>
String -> m (SBV (NonFuncSBVBaseType (FP eb sb)))
symNonFuncSBVTerm = forall t (m :: * -> *).
(SupportedPrim t, SBVFreshMonad m) =>
String -> m (SBVType t)
symSBVTerm @(FP eb sb)
  withNonFuncPrim :: forall r. (NonFuncPrimConstraint (FP eb sb) => r) -> r
withNonFuncPrim NonFuncPrimConstraint (FP eb sb) => r
r = r
NonFuncPrimConstraint (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 FPRoundingMode
l) (ConTerm FPRoundingMode
r) = Bool -> Term Bool
forall t. SupportedPrim 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 t. SupportedPrim t => Term t -> Term t -> Term Bool
pevalEqTerm Term FPRoundingMode
r Term FPRoundingMode
l
  pevalEqTerm Term FPRoundingMode
l Term FPRoundingMode
r = Term FPRoundingMode -> Term FPRoundingMode -> Term Bool
forall a. Term a -> Term a -> Term Bool
eqTerm Term FPRoundingMode
l Term FPRoundingMode
r
  pevalDistinctTerm :: NonEmpty (Term FPRoundingMode) -> Term Bool
pevalDistinctTerm = NonEmpty (Term FPRoundingMode) -> Term Bool
forall a. SupportedNonFuncPrim a => NonEmpty (Term a) -> Term Bool
pevalGeneralDistinct
  conSBVTerm :: FPRoundingMode -> SBVType FPRoundingMode
conSBVTerm FPRoundingMode
RNE = SBV RoundingMode
SBVType FPRoundingMode
SBV.sRNE
  conSBVTerm FPRoundingMode
RNA = SBV RoundingMode
SBVType FPRoundingMode
SBV.sRNA
  conSBVTerm FPRoundingMode
RTP = SBV RoundingMode
SBVType FPRoundingMode
SBV.sRTP
  conSBVTerm FPRoundingMode
RTN = SBV RoundingMode
SBVType FPRoundingMode
SBV.sRTN
  conSBVTerm FPRoundingMode
RTZ = SBV RoundingMode
SBVType FPRoundingMode
SBV.sRTZ
  symSBVName :: TypedSymbol 'AnyKind FPRoundingMode -> Int -> String
symSBVName TypedSymbol 'AnyKind FPRoundingMode
symbol Int
_ = TypedSymbol 'AnyKind FPRoundingMode -> String
forall a. Show a => a -> String
show TypedSymbol 'AnyKind FPRoundingMode
symbol
  symSBVTerm :: forall (m :: * -> *).
SBVFreshMonad m =>
String -> m (SBVType FPRoundingMode)
symSBVTerm 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
  parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> FPRoundingMode
parseSMTModelResult Int
_ ([([CV], CV)], CV)
cv =
    forall t a.
SupportedPrim t =>
((PrimConstraint t, SMTDefinable (SBVType t),
  Mergeable (SBVType t), Typeable (SBVType t)) =>
 a)
-> a
withPrim @(FPRoundingMode) (((PrimConstraint FPRoundingMode,
   SMTDefinable (SBVType FPRoundingMode),
   Mergeable (SBVType FPRoundingMode),
   Typeable (SBVType FPRoundingMode)) =>
  FPRoundingMode)
 -> FPRoundingMode)
-> ((PrimConstraint FPRoundingMode,
     SMTDefinable (SBVType FPRoundingMode),
     Mergeable (SBVType FPRoundingMode),
     Typeable (SBVType FPRoundingMode)) =>
    FPRoundingMode)
-> FPRoundingMode
forall a b. (a -> b) -> a -> b
$
      (RoundingMode -> FPRoundingMode)
-> ([([CV], CV)], CV) -> FPRoundingMode
forall v r.
(SatModel r, Typeable v) =>
(r -> v) -> ([([CV], CV)], CV) -> v
parseScalarSMTModelResult
        ( \(RoundingMode
x :: SBV.RoundingMode) -> case RoundingMode
x of
            RoundingMode
SBV.RoundNearestTiesToEven -> FPRoundingMode
RNE
            RoundingMode
SBV.RoundNearestTiesToAway -> FPRoundingMode
RNA
            RoundingMode
SBV.RoundTowardPositive -> FPRoundingMode
RTP
            RoundingMode
SBV.RoundTowardNegative -> FPRoundingMode
RTN
            RoundingMode
SBV.RoundTowardZero -> FPRoundingMode
RTZ
        )
        ([([CV], CV)], CV)
cv
  castTypedSymbol ::
    forall knd knd'.
    (IsSymbolKind knd') =>
    TypedSymbol knd FPRoundingMode ->
    Maybe (TypedSymbol knd' FPRoundingMode)
  castTypedSymbol :: forall (knd :: SymbolKind) (knd' :: SymbolKind).
IsSymbolKind knd' =>
TypedSymbol knd FPRoundingMode
-> Maybe (TypedSymbol knd' FPRoundingMode)
castTypedSymbol TypedSymbol knd FPRoundingMode
s =
    case forall (knd :: SymbolKind).
IsSymbolKind knd =>
Either (knd :~~: 'ConstantKind) (knd :~~: 'AnyKind)
decideSymbolKind @knd' of
      Left knd' :~~: 'ConstantKind
HRefl -> TypedSymbol knd' FPRoundingMode
-> Maybe (TypedSymbol knd' FPRoundingMode)
forall a. a -> Maybe a
Just (TypedSymbol knd' FPRoundingMode
 -> Maybe (TypedSymbol knd' FPRoundingMode))
-> TypedSymbol knd' FPRoundingMode
-> Maybe (TypedSymbol knd' FPRoundingMode)
forall a b. (a -> b) -> a -> b
$ Symbol -> TypedSymbol 'ConstantKind FPRoundingMode
forall t.
SupportedNonFuncPrim t =>
Symbol -> TypedSymbol 'ConstantKind t
typedConstantSymbol (Symbol -> TypedSymbol 'ConstantKind FPRoundingMode)
-> Symbol -> TypedSymbol 'ConstantKind FPRoundingMode
forall a b. (a -> b) -> a -> b
$ TypedSymbol knd FPRoundingMode -> Symbol
forall t (knd :: SymbolKind). TypedSymbol knd t -> Symbol
unTypedSymbol TypedSymbol knd FPRoundingMode
s
      Right knd' :~~: 'AnyKind
HRefl -> TypedSymbol knd' FPRoundingMode
-> Maybe (TypedSymbol knd' FPRoundingMode)
forall a. a -> Maybe a
Just (TypedSymbol knd' FPRoundingMode
 -> Maybe (TypedSymbol knd' FPRoundingMode))
-> TypedSymbol knd' FPRoundingMode
-> Maybe (TypedSymbol knd' FPRoundingMode)
forall a b. (a -> b) -> a -> b
$ Symbol -> TypedSymbol 'AnyKind FPRoundingMode
forall t. SupportedPrim t => Symbol -> TypedSymbol 'AnyKind t
typedAnySymbol (Symbol -> TypedSymbol 'AnyKind FPRoundingMode)
-> Symbol -> TypedSymbol 'AnyKind FPRoundingMode
forall a b. (a -> b) -> a -> b
$ TypedSymbol knd FPRoundingMode -> Symbol
forall t (knd :: SymbolKind). TypedSymbol knd t -> Symbol
unTypedSymbol TypedSymbol knd FPRoundingMode
s
  funcDummyConstraint :: SBVType FPRoundingMode -> SBV Bool
funcDummyConstraint SBVType FPRoundingMode
_ = SBV Bool
SBV.sTrue

instance NonFuncSBVRep FPRoundingMode where
  type NonFuncSBVBaseType FPRoundingMode = SBV.RoundingMode

instance SupportedNonFuncPrim FPRoundingMode where
  conNonFuncSBVTerm :: FPRoundingMode -> SBV (NonFuncSBVBaseType FPRoundingMode)
conNonFuncSBVTerm = FPRoundingMode -> SBV (NonFuncSBVBaseType FPRoundingMode)
FPRoundingMode -> SBVType FPRoundingMode
forall t. SupportedPrim t => t -> SBVType t
conSBVTerm
  symNonFuncSBVTerm :: forall (m :: * -> *).
SBVFreshMonad m =>
String -> m (SBV (NonFuncSBVBaseType FPRoundingMode))
symNonFuncSBVTerm = forall t (m :: * -> *).
(SupportedPrim t, SBVFreshMonad m) =>
String -> m (SBVType t)
symSBVTerm @FPRoundingMode
  withNonFuncPrim :: forall r. (NonFuncPrimConstraint FPRoundingMode => r) -> r
withNonFuncPrim NonFuncPrimConstraint FPRoundingMode => r
r = r
NonFuncPrimConstraint FPRoundingMode => r
r

-- AlgReal

instance SupportedPrimConstraint AlgReal

instance SBVRep AlgReal where
  type SBVType AlgReal = SBV.SBV SBV.AlgReal

instance SupportedPrim AlgReal where
  defaultValue :: AlgReal
defaultValue = AlgReal
0
  pevalITETerm :: Term Bool -> Term AlgReal -> Term AlgReal -> Term AlgReal
pevalITETerm = Term Bool -> Term AlgReal -> Term AlgReal -> Term AlgReal
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITEBasicTerm
  pevalEqTerm :: Term AlgReal -> Term AlgReal -> Term Bool
pevalEqTerm (ConTerm AlgReal
l) (ConTerm AlgReal
r) = Bool -> Term Bool
forall t. SupportedPrim t => t -> Term t
conTerm (Bool -> Term Bool) -> Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ AlgReal
l AlgReal -> AlgReal -> Bool
forall a. Eq a => a -> a -> Bool
== AlgReal
r
  pevalEqTerm l :: Term AlgReal
l@ConTerm {} Term AlgReal
r = Term AlgReal -> Term AlgReal -> Term Bool
forall t. SupportedPrim t => Term t -> Term t -> Term Bool
pevalEqTerm Term AlgReal
r Term AlgReal
l
  pevalEqTerm Term AlgReal
l Term AlgReal
r = Term AlgReal -> Term AlgReal -> Term Bool
forall a. Term a -> Term a -> Term Bool
eqTerm Term AlgReal
l Term AlgReal
r
  pevalDistinctTerm :: NonEmpty (Term AlgReal) -> Term Bool
pevalDistinctTerm = NonEmpty (Term AlgReal) -> Term Bool
forall a. SupportedNonFuncPrim a => NonEmpty (Term a) -> Term Bool
pevalGeneralDistinct
  conSBVTerm :: AlgReal -> SBVType AlgReal
conSBVTerm = AlgReal -> SBV AlgReal
forall a. SymVal a => a -> SBV a
SBV.literal (AlgReal -> SBV AlgReal)
-> (AlgReal -> AlgReal) -> AlgReal -> SBV AlgReal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlgReal -> AlgReal
toSBVAlgReal
  symSBVName :: TypedSymbol 'AnyKind AlgReal -> Int -> String
symSBVName TypedSymbol 'AnyKind AlgReal
symbol Int
_ = TypedSymbol 'AnyKind AlgReal -> String
forall a. Show a => a -> String
show TypedSymbol 'AnyKind AlgReal
symbol
  symSBVTerm :: forall (m :: * -> *).
SBVFreshMonad m =>
String -> m (SBVType AlgReal)
symSBVTerm String
name = String -> m (SBV AlgReal)
forall a. SymVal a => String -> m (SBV a)
forall (m :: * -> *) a.
(SBVFreshMonad m, SymVal a) =>
String -> m (SBV a)
sbvFresh String
name
  parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> AlgReal
parseSMTModelResult Int
_ ([([CV], CV)], CV)
cv =
    forall t a.
SupportedPrim t =>
((PrimConstraint t, SMTDefinable (SBVType t),
  Mergeable (SBVType t), Typeable (SBVType t)) =>
 a)
-> a
withPrim @AlgReal (((PrimConstraint AlgReal, SMTDefinable (SBVType AlgReal),
   Mergeable (SBVType AlgReal), Typeable (SBVType AlgReal)) =>
  AlgReal)
 -> AlgReal)
-> ((PrimConstraint AlgReal, SMTDefinable (SBVType AlgReal),
     Mergeable (SBVType AlgReal), Typeable (SBVType AlgReal)) =>
    AlgReal)
-> AlgReal
forall a b. (a -> b) -> a -> b
$
      (AlgReal -> AlgReal) -> ([([CV], CV)], CV) -> AlgReal
forall v r.
(SatModel r, Typeable v) =>
(r -> v) -> ([([CV], CV)], CV) -> v
parseScalarSMTModelResult AlgReal -> AlgReal
fromSBVAlgReal ([([CV], CV)], CV)
cv
  castTypedSymbol ::
    forall knd knd'.
    (IsSymbolKind knd') =>
    TypedSymbol knd AlgReal ->
    Maybe (TypedSymbol knd' AlgReal)
  castTypedSymbol :: forall (knd :: SymbolKind) (knd' :: SymbolKind).
IsSymbolKind knd' =>
TypedSymbol knd AlgReal -> Maybe (TypedSymbol knd' AlgReal)
castTypedSymbol TypedSymbol knd AlgReal
s =
    case forall (knd :: SymbolKind).
IsSymbolKind knd =>
Either (knd :~~: 'ConstantKind) (knd :~~: 'AnyKind)
decideSymbolKind @knd' of
      Left knd' :~~: 'ConstantKind
HRefl -> TypedSymbol knd' AlgReal -> Maybe (TypedSymbol knd' AlgReal)
forall a. a -> Maybe a
Just (TypedSymbol knd' AlgReal -> Maybe (TypedSymbol knd' AlgReal))
-> TypedSymbol knd' AlgReal -> Maybe (TypedSymbol knd' AlgReal)
forall a b. (a -> b) -> a -> b
$ Symbol -> TypedSymbol 'ConstantKind AlgReal
forall t.
SupportedNonFuncPrim t =>
Symbol -> TypedSymbol 'ConstantKind t
typedConstantSymbol (Symbol -> TypedSymbol 'ConstantKind AlgReal)
-> Symbol -> TypedSymbol 'ConstantKind AlgReal
forall a b. (a -> b) -> a -> b
$ TypedSymbol knd AlgReal -> Symbol
forall t (knd :: SymbolKind). TypedSymbol knd t -> Symbol
unTypedSymbol TypedSymbol knd AlgReal
s
      Right knd' :~~: 'AnyKind
HRefl -> TypedSymbol knd' AlgReal -> Maybe (TypedSymbol knd' AlgReal)
forall a. a -> Maybe a
Just (TypedSymbol knd' AlgReal -> Maybe (TypedSymbol knd' AlgReal))
-> TypedSymbol knd' AlgReal -> Maybe (TypedSymbol knd' AlgReal)
forall a b. (a -> b) -> a -> b
$ Symbol -> TypedSymbol 'AnyKind AlgReal
forall t. SupportedPrim t => Symbol -> TypedSymbol 'AnyKind t
typedAnySymbol (Symbol -> TypedSymbol 'AnyKind AlgReal)
-> Symbol -> TypedSymbol 'AnyKind AlgReal
forall a b. (a -> b) -> a -> b
$ TypedSymbol knd AlgReal -> Symbol
forall t (knd :: SymbolKind). TypedSymbol knd t -> Symbol
unTypedSymbol TypedSymbol knd AlgReal
s
  funcDummyConstraint :: SBVType AlgReal -> SBV Bool
funcDummyConstraint SBVType AlgReal
_ = SBV Bool
SBV.sTrue

instance NonFuncSBVRep AlgReal where
  type NonFuncSBVBaseType AlgReal = SBV.AlgReal

instance SupportedNonFuncPrim AlgReal where
  conNonFuncSBVTerm :: AlgReal -> SBV (NonFuncSBVBaseType AlgReal)
conNonFuncSBVTerm = AlgReal -> SBV (NonFuncSBVBaseType AlgReal)
AlgReal -> SBVType AlgReal
forall t. SupportedPrim t => t -> SBVType t
conSBVTerm
  symNonFuncSBVTerm :: forall (m :: * -> *).
SBVFreshMonad m =>
String -> m (SBV (NonFuncSBVBaseType AlgReal))
symNonFuncSBVTerm = forall t (m :: * -> *).
(SupportedPrim t, SBVFreshMonad m) =>
String -> m (SBVType t)
symSBVTerm @AlgReal
  withNonFuncPrim :: forall r. (NonFuncPrimConstraint AlgReal => r) -> r
withNonFuncPrim NonFuncPrimConstraint AlgReal => r
r = r
NonFuncPrimConstraint AlgReal => r
r